module PfeBrowserCerts where
import Prelude hiding (putStr,putStrLn,print,readFile,ioError,catch,readIO)
import AllFudgets as Fud hiding (getModificationTime)
import FudDraw
import Maybe(isJust,listToMaybe,mapMaybe)
import MUtils
import AbstractIO
import FileUtils(readFileNow)
import DirUtils(latestModTime)
import List((\\))

import PfePlumbing
import PfeBrowserMonad
import PPU(pp{-,ppi,ppu,withPPEnv,($$),(<>),(<+>),PPHsMode-})
import PFE0
import PFE_Certs
import CertCmd
import CertServers(certFiles,lookupServer)
import PfePropCmds(tassertionSignature)
import CertAttrs(label)
import DrawLex(cstatusIcon,certIcon)
import QualNames(getQualified)
import TypedIds
import HsIdent(HsIdentI(..))
import TiNames(topName)

{-+ #evidenceGfx#: this function computes the table that is shown in the
Evidence window. Every existing certificate, certificate annotation and
assertion will be mentioned in one of the table entries.
-}
evidenceGfx m dir (bad,icons) certs asserts =
    htableD hdrs (concatMap certD certs++concatMap missingD missing)
  where
    hdrs = ["Icon","Name","Sequent (or other info)"]
    missing = [a|(a,_)<-asserts,pp a `notElem` concs]
    concs = mapMaybe (lookup "conc" @@ fst.snd) certs

    missingD a = [g bad,createCertD "" s,"?" |- HsCon a]
      where s = pp a

    certD (cert,(optattrs,status)) =
      case optattrs of
	Nothing -> [g bad,certNameD cert,
		    g "certificate does not exist (not created yet?)"]
	Just attrs ->
	  case (`lookup` icons) =<< lookup "type" attrs of
	    Just cicons ->
		[certIconD cert icon,certNameD cert, hyp |- a]
	      where
		icon = cstatusIcon cicons status
	    _ -> [g bad,certNameD cert,g "bad cert/unknown cert type"]
	  where
	    conc = fromMaybe "-" (lookup "conc" attrs)
	    hyp = fromMaybe "" (lookup "hyp" attrs)
	    --sequent = conc++" -| "++hyp
	    a = HsCon (topName Nothing m conc Assertion)

    certIconD cert icon = labelD (CertLbl cert) (g icon)

    hyp |- conc = hboxcD [g hyp,g "|-", assertionD conc]

    assertionD a = labelD (DefLbl a) (ulinkD (g (pp a)))

{-+ #getAssertionInfo#: compute the extra info that is shown when the user
clicks on an assertion name.
-}
getAssertionInfo (n,Assertion) =
  do allcs <- certs # getStBr
     cicons <- icons # getStBr
     let a = pp (getQualified n)
	 certs = [c|c@(_,(Just attrs,_))<-allcs,lookup "conc" attrs==Just a]
	 newc = head ((a:[a++show n|n<-[1..]])\\map fst allcs)
	 cis = [(cert,certIcon cicons cert)|cert<-certs]
     return [hboxcD' 10 (g "Certificates:":
			 (if null certs
			 then [g "none."]
			 else map certNameIconD cis)
			 ++[createCertD newc a])]
getAssertionInfo _ = return []


{-+ #visibleStatusChange#: calling #showCertInfo# or #showQCertInfo# can
cause the status of a certificate to be updated. This function returns true
when the status of a certificate in the current module changed, in which
case certificate icons should be redrawn and the internal state should be
updated.
-}
statusChange cert =
  do m <- modname # getStBr
     newstatus <- fmap fst # certStatus m cert
     oldstatus <- ((fmap fst . snd) # ) . lookup cert . certs # getStBr
     return $ Just newstatus/=oldstatus

{-+ #showCertInfo#: computes the certificate information displayed when the
user clicks on a certificate icon. This includes checking whether the
certificate is valid, invalid or outofdate.
-}
showCertInfo cert =
  do m <- modname # getStBr
     showQCertInfo (QCertName m cert)

showQCertInfo qcert =
    maybe idle inProgress . listToMaybe . certInProgress =<< getStBr
  where
    idle = showQCertInfo' qcert
    inProgress cmd =
      case cmdCert cmd of
        Just qcert' -> inProgress' cmd qcert'
	_ -> idle
    inProgress' cmd qcert' =
      if qcert'==qcert
      then popupCertInfo qcert $
	     spacedD centerS $
	     vboxD [g $ "Certificate server command in progress:",
		    g (shellCmd cmd)]
      else idle

showQCertInfo' qcert =
    do certinfo <- getCertDescription qcert
       pfePut (toRefs (linesD (briefTxt certinfo)))
       popupCertInfo qcert (fullGfx certinfo)
  where
    briefTxt (Left (msg,actionD)) = [g msg,actionD]
    briefTxt (Right (fields,_)) = map (g.join) (take 3 fields)
      where join (x,y) = x++": "++y

    fullGfx (Left (msg,actionD)) = vboxD [Fud.g msg,actionD]
    fullGfx (Right (fields,actionD)) =
	vboxD [htableD ["Field","Value"] flatfields,actionD]
      where flatfields = concatMap (\(x,y)->[g x,g y]) fields

    getCertDescription (QCertName m cert) =
      withWaitCursor $ 
      do let msg =g ("Checking status of certificate "++cert)
         putInfoWindow (CertInfo,msg)
	 pfePut (toRefs msg)
         dir <- checkProject
	 servers <- certServers # getStBr
	 (revalidate,status,info) <- certUpdStatus dir m =<< certInfo m cert
	 --let status = "Unknown"
	 optlogfile <- do let logfile = certDiagnosticsPath m cert dir
			  r <- try (readFileNow logfile)
			  return $ case r of
			             Right txt@(_:_) -> Just txt
			             _ -> Nothing

         return (certDescription (m,revalidate,optlogfile,status,servers) info)

    certDescription _ (cert,(Nothing,_)) =
        Left (cert++": certificate does not exist (not created yet?)", actionD)
      where
        actionD = createCertD cert ""

    certDescription (m,revalidate,optlogfile,status',servers)
                    (cert,(Just attrs,status)) =
      Right ([("Certificate",(cert++" :: "++ctype)),
              ("Current Status",status')]
--	     ++ cfield "Certifies" "conc"
--	     ++ cfield "Depends on" "hyp"
	     ++ showStatus status
	     ++ concat [cfield (label attrs) name|(name,attrs)<-cattrs]
	     ++ cfield "Created by" "who"
	     ++ sfield "About this certificate type" "description",
	     actionD)
      where
	showStatus Nothing = cfield "Date" "date"
	showStatus (Just (valid,when)) =
          [("Marked "++(if valid then "" else "in")++"valid on",show when)]

        ctype = fromMaybe "missing!!" (lookup "type" attrs)
	optserver = lookupServer servers ctype
	sattrs = maybe [] serverAttrs optserver
	cattrs = maybe [] certAttrs optserver
        cfield = field attrs
	sfield = field sattrs
        field attrs hdr name = maybe [] ((:[]).((,) hdr)) (lookup name attrs)

        actionD = hboxD' 20 (revalD++editD++logfileD++removeD)
          where
	    revalD  = if revalidate then [cmdD reval "Validate"] else []
	    removeD = [cmdD rm "Remove"]
	    logfileD = maybe [] logfile optlogfile
	      where
                logfile txt= [cmdD' (CertShowText txt) "View diagnostic output"]
	    editD =
	      if isJust optserver
	      then [cmdD' (CertEdit (ctype,(cert,attrs))) "Edit"]
	      else []

            cmdD  = cmdD' . CertCmd
            cmdD' cmd lbl = labelD cmd (ulinkD (g lbl))

            reval = ValidateCert mcert
	    rm    = RemoveCert mcert
	    mcert = QCertName m cert

    --showType = pfePut . toRefs @@ getType

revalidateAll =
    withWaitCursor $
    do dir <- checkProject
       m <- modname # getStBr
       mapM_ (certUpdStatus dir m @@ certInfo m . fst) . certs =<< getStBr

certUpdStatus dir m info@(cert,(a@(Just attrs),Just (valid,when))) =
    ifM auxchange (revalidate "auxiliary file changed/missing") $
    ifM srcchange
	(if valid
	 then certStatusFromSig
	 else revalidate "was invalid, some source file has been changed") $
    return (not valid,if valid then "Valid" else "Invalid",info)
  where
    auxchange = let auxfiles = certAuxFiles m cert attrs dir
		in anyChangeSince when auxfiles
    srcchange = do srcfiles <- map fst # getSubGraph (Just [m])
		   anyChangeSince when srcfiles -- not cached??

    revalidate why = return (True,"Needs revalidation ("++why++")",info)

    isUnconditionalCert =
      case (lookup "conc" attrs,lookup "hyp" attrs) of
	(Just conc,Just "..") -> Just conc
	_ -> lookup "test" attrs -- TestCase

    certStatusFromSig =
	maybe unknownStatus uncondCertStatusFromSig isUnconditionalCert

    unknownStatus = return (True,"unknown",info)

    uncondCertStatusFromSig conc =
      do optcertsig <-
	   maybeM (readIO =<< readFile (certDir m cert dir++"/deps"))
	 case optcertsig of
	   Nothing -> return (True,"New, not yet validated",info)
	   Just certsig ->
	     do srcsig <- tassertionSignature ((m,conc),Nothing)
		if certsig==srcsig
		  then do markValid m cert
			  st <- certStatus m cert
			  return (False,"Valid",(cert,(a,st)))
		  else revalidate "source changed"

    -- vaid/invalid status missing:
certUpdStatus _ _ info@(_,(Just _,_)) =
    return (True,"New, not yet validated",info)

    -- attributes missing:
certUpdStatus _ _ info = return (False,"unknown (attributes missing?!)",info)

quickCertsStatus m certs dir =
  do srcdate <- latestModTime . map fst =<< getSubGraph (Just [m])
     mapM (quickCertStatus m srcdate dir) certs

quickCertStatus m srcdate dir cert =
  do (optattrs,status) <- snd # certInfo m cert
     case (,) # optattrs <# status of
       Nothing -> return Nothing
       Just (attrs,status@(valid,when)) ->
	 if srcdate>when
	 then return Nothing
	 else ifM (anyChangeSince when (certAuxFiles m cert attrs dir))
		  (return Nothing)
		  (return (Just status))

--allCertFiles m cert dir = (++) # certAuxFiles m cert dir <# certSrcFiles m
certAuxFiles m cert attrs dir = certAttrsPath m cert dir:certFiles attrs
--certSrcFiles m = map fst # getSubGraph [m]

createCertD cert concl = labelD (CreateCert (cert,concl))
			        (ulinkD (g "Create a new certificate!"))

certNameD cert = labelD (CertLbl cert) (ulinkD (g cert))

certNameIconD ((c,_),icon) = labelD (CertLbl c) (hboxD [ulinkD (g c),g icon])

htableD hdrs cells = tableD' 0 (length hdrs) (map b hdrs++map f cells)
  where
    b x = stackD [fgD "grey" (g $ filler False False 5),padD 3 (g x)]
    f x = stackD [fgD "grey" (g frame),padD 3 x]
    --f x = padD 3 x

linesD = fontD defaultFont . vboxlD' 0 -- . map g

anyChangeSince when paths =
   ifM (allM doesFileExist paths)
       ((when<) # latestModTime paths)
       (return True) -- a file has been deleted