{- | Module : Web.Theory Description : Pretty-printing security protocol theories into HTML code. Copyright : (c) 2011, 2012 Simon Meier & Cedric Staub License : GPL-3 Maintainer : Cedric Staub Stability : experimental Portability : non-portable -} {-# LANGUAGE PatternGuards, TupleSections #-} module Web.Theory ( htmlThyPath , htmlThyDbgPath , pngThyPath , titleThyPath , theoryIndex , nextThyPath , prevThyPath , nextSmartThyPath , prevSmartThyPath , checkProofs , applyMethodAtPath , applyProverAtPath ) where import Theory import Theory.Pretty import Web.Types import Web.Settings import Data.Maybe import Data.List import Data.Monoid import qualified Data.Map as M import Control.Basics import System.Directory import System.FilePath import Extension.Data.Label import qualified Text.Dot as D import Text.Isar import Text.PrettyPrint.Html import Utils.Misc (stringSHA256) import System.Process import System.Exit ------------------------------------------------------------------------------ -- Various other functions ------------------------------------------------------------------------------ checkProofs :: ClosedTheory -> ClosedTheory checkProofs = proveTheory checkedProver where checkedProver = checkAndExtendProver (sorryProver "not yet proven") applyMethodAtPath :: ClosedTheory -> String -> ProofPath -> Int -> Maybe ClosedTheory applyMethodAtPath thy lemmaName proofPath i = do lemma <- lookupLemma lemmaName thy subProof <- get lProof lemma `atPath` proofPath methods <- applicableProofMethods thy <$> psInfo (root subProof) method <- if length methods >= i then Just (methods !! (i-1)) else Nothing applyProverAtPath thy lemmaName proofPath (oneStepProver method `mappend` replaceSorryProver (oneStepProver Simplify) `mappend` replaceSorryProver (contradictionAndClauseProver) ) applyProverAtPath :: ClosedTheory -> String -> ProofPath -> Prover -> Maybe ClosedTheory applyProverAtPath thy lemmaName proofPath prover = modifyLemmaProof (focus proofPath prover) lemmaName thy ------------------------------------------------------------------------------ -- Pretty printing ------------------------------------------------------------------------------ -- | Reference a dot graph for the given path. refDotPath :: HtmlDocument d => TheoryPath -> d refDotPath path = closedTag "img" [("class", "graph"), ("src", imgPath)] where imgPath = "graph/" ++ joinPath' (renderPath path) getDotPath :: String -> FilePath getDotPath code = imageDir addExtension (stringSHA256 code) "dot" -- | Create a link to a given theory path. linkToPath :: HtmlDocument d => TheoryPath -- ^ Path to link to. -> [String] -- ^ Additional class -> d -- ^ Document that carries the link. -> d linkToPath path cls = withTag "a" [("class", classes), ("href", linkPath)] where classes = unwords $ "internal-link" : cls linkPath = joinPath' $ renderPath path -- | Output some preformatted text. preformatted :: HtmlDocument d => Maybe String -> d -> d preformatted cl = withTag "div" [("class", classes cl)] where classes (Just cls) = "preformatted " ++ cls classes (Nothing) = "preformatted" -- | Render a proof index relative to a theory path constructor. proofIndex :: HtmlDocument d => (ProofPath -> TheoryPath) -- ^ Relative addressing function -> Proof (Maybe Sequent, Bool) -- ^ The annotated incremental proof -> d proofIndex mkPath = prettyProofWith ppStep ppCase . insertPaths where isSolved = snd . fst . psInfo isAnnotated = isJust . fst . fst . psInfo isSorry ps | Sorry _ <- psMethod ps = True | otherwise = False markSolved = withTag "span" [("class", "hl_solved")] ppStep ps | not (isAnnotated ps) = superfluousStep ps | isSolved ps = (markSolved $ linkToStep ["solved"] ps) <> removeStep ps | isSorry ps = linkToStep ["unsolved", "sorry-step"] ps | otherwise = linkToStep ["unsolved"] ps <> removeStep ps removeStep ps = linkToPath (mkPath $ snd $ psInfo ps) ["remove-step"] emptyDoc ppCase ps | isSolved ps = markSolved | otherwise = id superfluousStep ps = withTag "span" [("class","hl_superfluous unsolved")] (prettyProofMethod $ psMethod ps) linkToStep cls ps = linkToPath (mkPath $ snd $ psInfo ps) ("proof-step" : cls) (prettyProofMethod $ psMethod ps) -- | Render the indexing links for a single lemma lemmaIndex :: HtmlDocument d => (ProofPath -> TheoryPath) -- ^ Relative addressing function -> Lemma IncrementalProof -- ^ The lemma -> d lemmaIndex mkPath l = markSolved (kwLemmaModulo "E" <-> prettyLemmaName l <> colon) <-> (linkToPath (TheoryLemma $ get lName l) ["edit-link"] editPng <-> linkToPath (TheoryLemma $ get lName l) ["delete-link"] deletePng) $-$ nest 2 (markSolved $ doubleQuotes $ prettyFormulaE $ get lFormulaE l) $-$ proofIndex mkPath annotatedProof where editPng = png "/static/img/edit.png" deletePng = png "/static/img/delete.png" png path = closedTag "img" [("class","icon"),("src",path)] annotatedProof = annotateProof $ get lProof l markSolved doc | solved = withTag "span" [("class", "hl_solved")] doc | otherwise = doc where solved = snd $ psInfo $ root annotatedProof -- | Render the theory index. theoryIndex :: HtmlDocument d => ClosedTheory -> d theoryIndex thy = foldr1 ($-$) [ kwTheoryHeader $ get thyName thy , text "" , messageLink , text "" , ruleLink , text "" , reqCasesLink "Untyped case distinctions" UntypedCaseDist , text "" , reqCasesLink "Typed case distinctions " TypedCaseDist , text "" , vcat $ intersperse (text "") lemmas , text "" , kwEnd ] where mkPath path lemma = path $ get lName lemma lemmaIndex' lemma = lemmaIndex (mkPath TheoryProof lemma) lemma lemmas = map lemmaIndex' (getLemmas thy) rules = getClassifiedRules thy rulesInfo = parens $ int $ length $ get crProtocol rules casesInfo kind = parens $ nCases <> comma <-> text chainInfo where cases = getCaseDistinction kind thy nChains = sum $ map (sum . unsolvedChainConstraints) cases nCases = int (length cases) <-> text "cases" chainInfo | nChains == 0 = "all chains solved" | otherwise = show nChains ++ " chains left" bold = withTag "strong" [] . text overview n info p = linkToPath p [] (bold n <-> info) messageLink = overview "Message theory" (text "") TheoryMessage ruleLink = overview "Multiset rewriting rules" rulesInfo TheoryRules reqCasesLink name k = overview name (casesInfo k) (TheoryCaseDist k 0 0) {- -- | A snippet that explains a sequent using a rendered graph and the pretty -- printed sequent. sequentSnippet :: HtmlDocument d => Sequent -- ^ Sequent to pretty print. -> TheoryPath -- ^ The sequents path (NOT the path to its PNG) -> d sequentSnippet se path = refDotPath path $-$ preformatted Nothing (prettySequent se) -} -- | A snippet that explains a sub-proof by displaying its proof state, the -- open-goals, and the new cases. subProofSnippet :: HtmlDocument d => ClosedTheory -- ^ The theory context. -> (ProofPath -> TheoryPath) -- ^ Relative proof adressing -> (Int -> TheoryPath) -- ^ Relative proof method addressing -> IncrementalProof -- ^ The sub-proof. -> d subProofSnippet thy mkProofPath mkPrfMethodPath prf = case psInfo $ root prf of Nothing -> text $ "no annotated sequent / " ++ nCases ++ " sub-case(s)" Just se -> vcat $ [ withTag "h3" [] (text "Graph Part of Sequent") , refDotPath (mkProofPath []) , text "" , withTag "h3" [] (text "Applicable Proof Methods") , preformatted (Just "methods") (numbered' $ proofMethods se) , withTag "h3" [] (text "Pretty-Printed Sequent") , preformatted (Just "sequent") (prettyNonGraphSequent se) , withTag "h3" [] (text $ nCases ++ " sub-case(s)") ] ++ subCases where prettyPM (i, m) = linkToPath (mkPrfMethodPath i) ["proof-method"] (prettyProofMethod m) nCases = show $ M.size $ children prf proofMethods = map prettyPM . zip [1..] . applicableProofMethods thy subCases = concatMap refSubCase $ M.toList $ children prf refSubCase (name, prf') = [ withTag "h4" [] (text "Case" <-> text name) , maybe (text "no proof state available") (const $ refDotPath $ mkProofPath [name]) (psInfo $ root prf') ] -- | A Html document representing the requires case splitting theorem. htmlCaseDistinction :: HtmlDocument d => CaseDistKind -> (Int, CaseDistinction) -> d htmlCaseDistinction kind (j, th) = if null cases then withTag "h2" [] ppHeader $-$ withTag "h3" [] (text "No cases.") else vcat $ withTag "h2" [] ppHeader : cases where cases = concatMap ppCase $ zip [1..] $ getDisj $ get cdCases th wrapP = withTag "p" [("class","monospace cases")] nCases = int $ length $ getDisj $ get cdCases th ppPrem = nest 2 $ doubleQuotes $ prettyBigStepGoal $ get cdGoal th ppHeader = hsep [ text "Sources of" <-> ppPrem , parens $ nCases <-> text "cases" ] ppCase (i, (names, (conc, se))) = [ withTag "h3" [] $ fsep [ text "Source", int i, text "of", nCases , text " / named ", doubleQuotes (text name) ] , refDotPath (TheoryCaseDist kind j i) , withTag "p" [] $ ppPrem <-> text "provided by conclusion" <-> prettyNodeConc conc , wrapP $ prettyNonGraphSequent se ] where name = intercalate "_" names -- | Build the Html document showing the source cases distinctions. reqCasesSnippet :: HtmlDocument d => CaseDistKind -> ClosedTheory -> d reqCasesSnippet kind thy = vcat $ htmlCaseDistinction kind <$> zip [1..] (getCaseDistinction kind thy) -- | Build the Html document showing the rules of the theory. rulesSnippet :: HtmlDocument d => ClosedTheory -> d rulesSnippet thy = vcat [ ppRules "Multiset Rewriting Rules" crProtocol ] where rules = getClassifiedRules thy ppRules header l = withTag "h2" [] (text header) $$ withTag "p" [("class","monospace rules")] (vcat (intersperse (text "") $ map prettyRuleAC $ get l rules)) -- | Build the Html document showing the message theory. messageSnippet :: HtmlDocument d => ClosedTheory -> d messageSnippet thy = vcat [ ppSection "Signature" [prettySignatureWithMaude (get thySignature thy)] , ppSection "Construction Rules" (ppRules crConstruct) , ppSection "Destruction Rules" (ppRules crDestruct) -- , ppSection "Special Rules" (ppRules crSpecial) ] where ppRules l = map prettyRuleAC $ get l $ getClassifiedRules thy ppSection header s = withTag "h2" [] (text header) $$ withTag "p" [("class","monospace rules")] (vcat (intersperse (text "") $ s)) -- | Render the item in the given theory given by the supplied path. htmlThyPath :: HtmlDocument d => ClosedTheory -- ^ The theory to render -> TheoryPath -- ^ Path to render -> d htmlThyPath thy path = go path where go TheoryRules = rulesSnippet thy go TheoryMessage = messageSnippet thy go (TheoryCaseDist kind _ _) = reqCasesSnippet kind thy go (TheoryProof l p) = fromMaybe (text "No such lemma or proof path.") (subProofSnippet thy (mkProofPath l p) (TheoryMethod l p) <$> resolveProofPath thy l p) go (TheoryLemma _) = text "Implement theory item pretty printing!" go _ = text "Unhandled theory path. This is a bug." mkProofPath lemma path' subPath = TheoryProof lemma (path' ++ subPath) -- | Render debug information for the item in the theory given by the path. htmlThyDbgPath :: HtmlDocument d => ClosedTheory -- ^ The theory to render -> TheoryPath -- ^ Path to render -> Maybe d htmlThyDbgPath thy path = go path where go (TheoryProof l p) = do proof <- resolveProofPath thy l p prettySequent <$> psInfo (root proof) go _ = Nothing -- | Render the image corresponding to the given theory path. pngThyPath :: FilePath -> (Sequent -> D.Dot ()) -> ClosedTheory -> TheoryPath -> IO FilePath pngThyPath dir compact thy path = go path where go (TheoryCaseDist k i j) = renderDotCode (casesDotCode k i j) go (TheoryProof l p) = renderDotCode (proofPathDotCode l p) go _ = error "Unhandled theory path. This is a bug." -- Get dot code for required cases casesDotCode k i j = D.showDot $ compact $ snd $ snd $ cases !! (i-1) !! (j-1) where cases = map (getDisj . get cdCases) (getCaseDistinction k thy) -- Get dot code for proof path in lemma proofPathDotCode lemma proofPath = D.showDot $ fromMaybe (return ()) $ do subProof <- resolveProofPath thy lemma proofPath sequent <- psInfo $ root subProof return $ compact sequent -- Render a piece of dot code renderDotCode code = do let dotPath = dir getDotPath code pngPath = addExtension dotPath "png" pngGenerated <- firstSuccess [ doesFileExist pngPath , writeFile dotPath code >> dotToPng "dot" dotPath pngPath , dotToPng "fdp" dotPath pngPath ] return (if pngGenerated then pngPath else imageDir ++ "/img/delete.png") dotToPng dotCmd dotFile pngFile = do (ecode,_out,err) <- readProcessWithExitCode dotCmd ["-Tpng","-o",pngFile,dotFile] "" case ecode of ExitSuccess -> return True ExitFailure i -> do putStrLn $ "dotToPng: "++dotCmd++" failed with code " ++show i++" for file "++dotFile++":\n"++err return False firstSuccess [] = return False firstSuccess (m:ms) = do s <- m if s then return True else firstSuccess ms -- | Get title to display for a given proof path. titleThyPath :: ClosedTheory -> TheoryPath -> String titleThyPath thy path = go path where go TheoryRules = "Rewriting rules" go TheoryMessage = "Message theory" go (TheoryCaseDist UntypedCaseDist _ _) = "Untyped case distinctions" go (TheoryCaseDist TypedCaseDist _ _) = "Typed case distinctions" go (TheoryLemma l) = "Lemma: " ++ l go (TheoryProof l []) = "Lemma: " ++ l go (TheoryProof l p) | null (last p) = "Method: " ++ methodName l p | otherwise = "Case: " ++ last p go _ = "Unhandled theory path" methodName l p = case resolveProofPath thy l p of Nothing -> "None" Just proof -> renderHtmlDoc $ prettyProofMethod $ psMethod $ root proof -- | Resolve a proof path. resolveProofPath :: ClosedTheory -- ^ Theory to resolve in -> String -- ^ Name of lemma -> ProofPath -- ^ Path to resolve -> Maybe IncrementalProof resolveProofPath thy lemmaName path = do lemma <- lookupLemma lemmaName thy get lProof lemma `atPath` path ------------------------------------------------------------------------------ -- Moving to next/prev proof path ------------------------------------------------------------------------------ -- | Get 'next' theory path. nextThyPath :: ClosedTheory -> TheoryPath -> TheoryPath nextThyPath thy = go where go TheoryMain = TheoryMessage go TheoryMessage = TheoryRules go TheoryRules = TheoryCaseDist UntypedCaseDist 0 0 go (TheoryCaseDist UntypedCaseDist _ _) = TheoryCaseDist TypedCaseDist 0 0 go (TheoryCaseDist TypedCaseDist _ _) = fromMaybe TheoryMain firstLemma go (TheoryLemma lemma) = TheoryProof lemma [] go (TheoryProof l p) | Just nextPath <- getNextPath l p = TheoryProof l nextPath | Just nextLemma <- getNextLemma l = TheoryProof nextLemma [] | otherwise = TheoryMain go _ = TheoryMain lemmas = map (\l -> (get lName l, l)) $ getLemmas thy firstLemma = flip TheoryProof [] . fst <$> listToMaybe lemmas getNextPath lemmaName path = do lemma <- lookupLemma lemmaName thy let paths = map fst $ getProofPaths $ get lProof lemma getNextElement (== path) paths getNextLemma lemmaName = getNextElement (== lemmaName) (map fst lemmas) -- | Get 'prev' theory path. prevThyPath :: ClosedTheory -> TheoryPath -> TheoryPath prevThyPath thy = go where go TheoryMessage = TheoryMain go TheoryRules = TheoryMessage go (TheoryCaseDist UntypedCaseDist _ _) = TheoryRules go (TheoryCaseDist TypedCaseDist _ _) = TheoryCaseDist UntypedCaseDist 0 0 go (TheoryLemma l) | Just prevLemma <- getPrevLemma l = TheoryProof prevLemma (lastPath prevLemma) | otherwise = TheoryCaseDist TypedCaseDist 0 0 go (TheoryProof l p) | Just prevPath <- getPrevPath l p = TheoryProof l prevPath | Just prevLemma <- getPrevLemma l = TheoryProof prevLemma (lastPath prevLemma) | otherwise = TheoryCaseDist TypedCaseDist 0 0 go _ = TheoryMain lemmas = map (\l -> (get lName l, l)) $ getLemmas thy getPrevPath lemmaName path = do lemma <- lookupLemma lemmaName thy let paths = map fst $ getProofPaths $ get lProof lemma getPrevElement (== path) paths lastPath lemmaName = last $ map fst $ getProofPaths $ get lProof $ fromJust $ lookupLemma lemmaName thy getPrevLemma lemmaName = getPrevElement (== lemmaName) (map fst lemmas) -- Get 'next' smart theory path. nextSmartThyPath :: ClosedTheory -> TheoryPath -> TheoryPath nextSmartThyPath thy = go where go TheoryMain = TheoryMessage go TheoryMessage = TheoryRules go TheoryRules = TheoryCaseDist UntypedCaseDist 0 0 go (TheoryCaseDist UntypedCaseDist _ _) = TheoryCaseDist TypedCaseDist 0 0 go (TheoryCaseDist TypedCaseDist _ _) = fromMaybe TheoryMain firstLemma go (TheoryLemma lemma) = TheoryProof lemma [] go (TheoryProof l p) | Just nextPath <- getNextPath l p = TheoryProof l nextPath | Just nextLemma <- getNextLemma l = TheoryProof nextLemma [] | otherwise = TheoryMain go _ = TheoryMain lemmas = map (\l -> (get lName l, l)) $ getLemmas thy firstLemma = flip TheoryProof [] . fst <$> listToMaybe lemmas getNextPath lemmaName path = do lemma <- lookupLemma lemmaName thy let paths = getProofPaths $ get lProof lemma let nextSteps = snd $ break ((== path) . fst) paths if null nextSteps then Nothing else listToMaybe $ map fst $ filter snd $ tail nextSteps getNextLemma lemmaName = getNextElement (== lemmaName) (map fst lemmas) -- Get 'prev' smart theory path. prevSmartThyPath :: ClosedTheory -> TheoryPath -> TheoryPath prevSmartThyPath thy = go where go TheoryMessage = TheoryMain go TheoryRules = TheoryMessage go (TheoryCaseDist UntypedCaseDist _ _) = TheoryRules go (TheoryCaseDist TypedCaseDist _ _) = TheoryCaseDist UntypedCaseDist 0 0 go (TheoryLemma l) | Just prevLemma <- getPrevLemma l = TheoryProof prevLemma (lastPath prevLemma) | otherwise = TheoryCaseDist TypedCaseDist 0 0 go (TheoryProof l p) | Just prevPath <- getPrevPath l p = TheoryProof l prevPath | Just firstPath <- getFirstPath l p = TheoryProof l firstPath | Just prevLemma <- getPrevLemma l = TheoryProof prevLemma (lastPath prevLemma) | otherwise = TheoryCaseDist TypedCaseDist 0 0 go _ = TheoryMain lemmas = map (\l -> (get lName l, l)) $ getLemmas thy getFirstPath lemmaName current = do lemma <- lookupLemma lemmaName thy let paths = map fst $ getProofPaths $ get lProof lemma if null paths || (head paths == current) then Nothing else Just $ head paths getPrevPath lemmaName path = do lemma <- lookupLemma lemmaName thy let paths = getProofPaths $ get lProof lemma let prevSteps = filter snd $ fst $ break ((== path) . fst) paths if null prevSteps then Nothing else Just $ fst $ last prevSteps lastPath lemmaName = last $ map fst $ getProofPaths $ get lProof $ fromJust $ lookupLemma lemmaName thy getPrevLemma lemmaName = getPrevElement (== lemmaName) (map fst lemmas) -- | Extract proof paths out of a proof. -- Boolean value in tuple indicates if path is sorry step. getProofPaths :: LTree CaseName (ProofStep a) -> [([String], Bool)] getProofPaths proof = ([], isSorry proof) : go proof where go = concatMap paths . M.toList . children paths (lbl, prf) = ([lbl], isSorry prf) : map (first (lbl:)) (go prf) isSorry ps | Sorry _ <- psMethod (root ps) = True | otherwise = False -- | Get element _after_ the matching element in the list. getNextElement :: (a -> Bool) -> [a] -> Maybe a getNextElement _ [] = Nothing getNextElement f (x:xs) | f x = listToMaybe xs | otherwise = getNextElement f xs -- | Get element _before_ the matching element in the list. getPrevElement :: (a -> Bool) -> [a] -> Maybe a getPrevElement _ [] = Nothing getPrevElement f (x:xs) = go x xs where go _ [] = Nothing go old (z:zs) | f z = Just old | otherwise = go z zs -- | Annotate a proof for pretty printing. -- The boolean flag indicates that the given proof step's children -- are (a) all annotated and (b) contain no sorry steps. annotateProof :: Proof (Maybe Sequent) -> Proof (Maybe Sequent, Bool) annotateProof (LNode (ProofStep method sequent) children') | Nothing <- sequent = LNode (proofStep False) annotatedChildren | Sorry _ <- method = LNode (proofStep False) annotatedChildren | otherwise = LNode (proofStep checkChildren) annotatedChildren where annotatedChildren = M.map annotateProof children' proofStep bool = ProofStep method (sequent, bool) checkChildren = all (snd . psInfo . root . snd) $ M.toList annotatedChildren ------------------------------------------------------------------------------ -- Html file generation ------------------------------------------------------------------------------ {- TO BE REDONE, once interactive visualization is finished. Corresponds to - a pre-rendering of all relevant data. data Viewport = LeftView | MainView | DebugView | PopupView deriving( Eq, Ord, Show ) type Link = (Viewport, HtmlSnippetId) type LinkId = Int type HtmlSnippet = String type HtmlSnippetId = Int type DotCode = String data ThHtmlState = ThHtmlState { _thsDots :: M.Map FilePath DotCode , _thsSnippets :: M.Map HtmlSnippet HtmlSnippetId , _thsLinks :: M.Map LinkId [Link] } deriving( Eq, Ord, Show ) emptyThHtmlState :: ThHtmlState emptyThHtmlState = ThHtmlState M.empty M.empty M.empty $(mkLabels [''ThHtmlState]) type ThHtml = ReaderT (Sequent -> Sequent) (StateT ThHtmlState Fresh) runThHtml :: (Sequent -> Sequent) -> ThHtml a -> (a, ThHtmlState) runThHtml compress = (`evalFresh` nothingUsed) . (`runStateT` emptyThHtmlState) . (`runReaderT` compress) instance JSON Viewport where readJSON (JSString name) = case fromJSString name of "Left" -> return LeftView "Main" -> return MainView "Debug" -> return DebugView "Popup" -> return PopupView cs -> Error $ "readJSSON (Viewport): " ++ cs readJSON _ = Error "readJSSon (Viewport)" showJSON LeftView = JSString $ toJSString "Left" showJSON MainView = JSString $ toJSString "Main" showJSON DebugView = JSString $ toJSString "Debug" showJSON PopupView = JSString $ toJSString "Popup" -- | Input for generation process that needs to be supplied from a caller of -- @theoryToHtml@. data GenerationInput = GenerationInput { giHeader :: String -- ^ Arbitrary html for the header , giTime :: UTCTime -- ^ Generation time. , giSystem :: String -- ^ Description of the system we run on. , giInputFile :: FilePath -- ^ Path to input file. , giTemplate :: FilePath -- ^ Path to template index. , giOutDir :: FilePath -- ^ Path to the output directory. , giTheory :: ClosedTheory -- ^ Theory to output. , giCmdLine :: String -- ^ The command line that was used in this call to -- tamarin. , giCompress :: Bool -- ^ True if sequents should be compressed -- before visualization by unsoundly dropping -- information. } deriving( Show ) -- | Information about various paths relevant for generating the HTML output. data PathInfo = PathInfo { inputFileCopy :: FilePath -- ^ Path of input file copy. , proofScriptFile :: FilePath -- ^ Path of generated Isabelle proof script. , outDir :: FilePath -- ^ Output directory. , filesDir :: FilePath -- ^ Relative directory for input and output files. } deriving( Show ) -- | Compute the path info from the generation input. pathInfo :: GenerationInput -> PathInfo pathInfo input = info where info = PathInfo { inputFileCopy = extendBaseName "_original" , proofScriptFile = extendBaseName "_processed" , outDir = giOutDir input , filesDir = "files" } extendBaseName ext = filesDir info addExtension (takeBaseName (giInputFile input) ++ ext) "spthy" -- | Make a path that is specified relative to the output directory absolute. mkAbsolute :: PathInfo -> FilePath -> FilePath mkAbsolute info = (outDir info ) -- | Compute the list of absolute paths to directories required for generating -- this HTML output. requiredDirs :: PathInfo -> [FilePath] requiredDirs info = map (mkAbsolute info) [".", imageDir, filesDir info] -- | Prepare information gathered during the generation of the resulting -- theories for exporting as JSON. jsGenerationInfo :: GenerationInput -> NominalDiffTime -- ^ Proof script generation time. -> JSObject JSValue jsGenerationInfo input genTime = toJSObject $ [ ("header", showJSON . toJSString $ giHeader input) , ("time", showJSON . toJSString . show $ giTime input) , ("system", showJSON . toJSString $ giSystem input) , ("inputFile", showJSON . fileLink $ inputFileCopy paths) , ("proofScript", showJSON . fileLink $ proofScriptFile paths) , ("commandLine", showJSON . toJSString $ giCmdLine input) , ("certificateStatus", showJSON . toJSString $ genTimeString) ] where paths = pathInfo input fileLink file = (toJSString (takeFileName file), toJSString file) genTimeString = "generated in " ++ show genTime -- | Convert a security protocol theory to a HTML file visualizing it. theoryToHtml :: GenerationInput -> IO () theoryToHtml input = do putStrLn "" putStrLn $ " copying template to output directory: " ++ outDir paths mapM_ (createDirectoryIfMissing True) $ requiredDirs paths copyTemplate (giTemplate input) $ outDir paths copyFile (giInputFile input) (mkAbsolute paths $ inputFileCopy paths) -- timed proof script generation putStr " generating proof script: " >> hFlush stdout genTime <- timed_ $ writeAbsolute (proofScriptFile paths) (render $ prettyClosedTheory $ giTheory input) putStrLn $ show genTime -- json output let thyJSON = mkThyJSON (jsGenerationInfo input genTime) writeAbsolute "theory.js" (("scytherP_theory_JSON = "++) . show $ showJSObject thyJSON "") -- graph generation putStrLn " generating visualizations using GraphViz:" parMkGraphs $ M.toList $ get thsDots thSt where paths = pathInfo input writeAbsolute = writeFile . mkAbsolute paths compress | giCompress input = compressSequent | otherwise = id (thId, thSt) = runThHtml compress $ do thy <- htmlTheory $ giTheory input return $ renderHtmlDoc thy mkThyJSON :: JSObject JSValue -> JSObject JSValue mkThyJSON genInfo = toJSObject [ ("theory", showJSON $ thId ) , ("generationInfo", showJSON $ genInfo ) , ("snippets", showJSON $ invertMap $ get thsSnippets thSt ) , ("links", showJSON $ get thsLinks thSt ) ] invertMap = M.fromList . map (uncurry $ flip (,)) . M.toList -- create the graph corresponding to the given formula mkGraph (path, dotCode) msgChan = do let outFile = mkAbsolute paths path pngFile = addExtension outFile "png" ifM (doesFileExist pngFile) (writeChan msgChan $ "using cached file: " ++ pngFile) (do writeFile outFile dotCode graphvizDotToPng outFile pngFile msgChan removeFile outFile) -- | Convert a list of dot strings in parallel to png files, using the number of -- cores+1 parallel executions of the dot tool. parMkGraphs = parCmd_ display . map mkGraph where display n i msg = hPutStrLn stdout $ " ["++showPadded i++" of "++show n++"] "++msg where showPadded x = flushRight (length (show n)) (show x) -- | Copy all the files referenced in the template index file to the output -- directory. copyTemplate :: FilePath -- ^ Path of template index file. -> FilePath -- ^ Output directory. -> IO () copyTemplate templateFile targetDir = do let templateDir = takeDirectory templateFile template <- readFile templateFile let files = filter (not.null) $ lines template copy file = do let outPath = targetDir file createDirectoryIfMissing True (takeDirectory outPath) copyFile (templateDir file) outPath mapM_ copy files -}