PFE_Certs.hs

module PFE_Certs(module PFE_Certs,CertServers,CertServer(..)) where
import Prelude hiding (putStrLn,ioError,catch,writeFile)
import Maybe(fromMaybe)

import HsModule
import HasPropStruct
import HsPropStruct(PD(..))
import PFE0(projectDir,moduleInfoPath,getSubGraph)
import CertServers

import AbstractIO
import DirUtils(getModificationTimeMaybe)
import MUtils

type CertType = String
type CertName = String
data QCertName = QCertName ModuleName CertName deriving (Eq,Show,Read)

-- Extract the named assertions from the top-level of a module:
assertions mod =
  [(n,pa)|Just (HsAssertion s (Just n) pa)<-map propstruct (hsModDecls mod)]

getCertServers = getCertServers' =<< getProgramaticaDir

getCertServers' = readCertServers . certTypesDir

getProgramaticaDir =
  do pdir <- fromMaybe defaultPDir # maybeM (getEnv pDirVar)
     unlessM (doesDirectoryExist pdir) $
       fail $ "Didn't find the Programatica directory "++pdir
     let pdir' = if take 1 (reverse pdir) == "/" then pdir else pdir++"/"
     return pdir'

type CertStatus = Maybe (Bool,ClockTime) -- (valid?,when)
--certStatus :: ... => Module -> CertName -> m CertStatus
certStatus m cert =
    do optdir <- projectDir
       case optdir of
         Nothing -> return Nothing
	 Just dir ->
	   status # getModificationTimeMaybe (certValidWhenPath m cert dir)
		 <# getModificationTimeMaybe (certInvalidWhenPath m cert dir)
  where
    status optvalid optinvalid =
      case (optvalid,optinvalid) of
	(Just v,Just inv) -> if v>inv then Just (True,v) else Just (False,inv)
	(Just v,_) -> Just (True,v)
	(_,Just inv) -> Just (False,inv)
	_ -> Nothing

type CertInfo = (CertName,(Maybe Attrs,CertStatus))

--certInfo :: ... => Module -> CertName -> CertInfo
certInfo m cert =
  do optdir <- projectDir
     (,) cert # case optdir of
	         Nothing -> return (Nothing,Nothing)
                 Just dir -> (,) # certAttrs dir <# certStatus m cert
  where
    certAttrs dir = maybeM (readAttrs path)
      where path = certAttrsPath m cert dir

markValid m cert =
  do optdir <- projectDir
     case optdir of
       Just dir -> do now <- getClockTime
                      writeFile (certValidWhenPath m cert dir) (show now)
		      srcfiles <- map fst # getSubGraph (Just [m])
		      writeFile (certSrcListPath m cert dir) (unlines srcfiles)
       _ -> done

--optCertsDir = certsDir # projectDir

--------------------------------------------------------------------------------

certsDir dir = dir++"cert/" -- or just "cert/", or "evidence/"? (dir="hi")
certModuleDir m dir = certsDir dir++moduleInfoPath m
certDir m f dir = certModuleDir m dir++"/"++f
--certIconPath m f = certDir m f++"/icon.gif"
certAttrsPath m f dir = certDir m f dir++"/cert.attr"
--certTextPath m f dir = certDir m f dir++"/cert.txt"
certDiagnosticsPath m f dir = certDir m f dir++"/output.txt"
badCertIconPath pdir = pdir++"icons/smiley.sad.gif"
--certDatestampPath m = certDir m "when"
certValidWhenPath m c dir = certDir m c dir++"/valid"
certInvalidWhenPath m c dir = certDir m c dir++"/invalid"
certSrcListPath m c dir = certDir m c dir++"/srclist.txt"
-- Programatica directory:
pDirVar = "PROGRAMATICA"
certTypesDir pdir = pdir++"types/certificate/"

-- Suitable builtin default for the PacSoft servers:
defaultPDir = "/home/projects/pacsoft/tools/lib/Programatica/"