{-# LANGUAGE PatternGuards #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE TupleSections #-} {- | Module : Web.Theory Description : Pretty-printing security protocol theories into HTML code. Copyright : (c) 2011, 2012 Simon Meier & Cedric Staub License : GPL-3 Maintainer : Simon Meier Stability : experimental Portability : non-portable -} module Web.Theory ( htmlThyPath -- , htmlThyDbgPath , imgThyPath , titleThyPath , theoryIndex , nextThyPath , prevThyPath , nextSmartThyPath , prevSmartThyPath , applyMethodAtPath , applyProverAtPath ) where import Debug.Trace (trace) import Data.Char (toUpper) import Data.List import qualified Data.Map as M import Data.Maybe import Data.Monoid import qualified Data.Set as S import qualified Data.Text as T import Data.Time.Format (formatTime) import Control.Basics import Control.Concurrent (threadDelay) import System.Directory import System.FilePath import System.Locale (defaultTimeLocale) import Extension.Data.Label import Text.Blaze.Html (preEscapedToMarkup, toHtml) import qualified Text.Dot as D import Text.Hamlet (Html, hamlet) import Text.PrettyPrint.Html import Utils.Misc (stringSHA256) import System.Exit import System.Process import Logic.Connectives import Theory import Theory.Constraint.System.Dot (nonEmptyGraph) import Theory.Text.Pretty import Web.Settings import Web.Types ------------------------------------------------------------------------------ -- Various other functions ------------------------------------------------------------------------------ applyMethodAtPath :: ClosedTheory -> String -> ProofPath -> Heuristic -- ^ How to extract/order the proof methods. -> Int -- What proof method to use. -> Maybe ClosedTheory applyMethodAtPath thy lemmaName proofPath heuristic i = do lemma <- lookupLemma lemmaName thy subProof <- get lProof lemma `atPath` proofPath let ctxt = getProofContext lemma thy sys = psInfo (root subProof) ranking = useHeuristic heuristic (length proofPath) methods <- (map fst . rankProofMethods ranking ctxt) <$> sys method <- if length methods >= i then Just (methods !! (i-1)) else Nothing applyProverAtPath thy lemmaName proofPath (oneStepProver method `mappend` replaceSorryProver (oneStepProver Simplify) `mappend` replaceSorryProver (contradictionProver) `mappend` replaceSorryProver (oneStepProver Solved) ) 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 => RenderUrl -> TheoryIdx -> TheoryPath -> d refDotPath renderUrl tidx path = closedTag "img" [("class", "graph"), ("src", imgPath)] where imgPath = T.unpack $ renderUrl (TheoryGraphR tidx path) getDotPath :: String -> FilePath getDotPath code = imageDir addExtension (stringSHA256 code) "dot" -- | Create a link to a given theory path. linkToPath :: HtmlDocument d => RenderUrl -- ^ Url rendering function. -> Route WebUI -- ^ Route that should be linked. -> [String] -- ^ Additional class -> d -- ^ Document that carries the link. -> d linkToPath renderUrl route cls = withTag "a" [("class", classes), ("href", linkPath)] where classes = unwords $ "internal-link" : cls linkPath = T.unpack $ renderUrl route -- | 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 => RenderUrl -> (ProofPath -> Route WebUI) -- ^ Relative addressing function -> Proof (Maybe System, Maybe Bool) -- ^ The annotated incremental proof -> d proofIndex renderUrl mkRoute = prettyProofWith ppStep ppCase . insertPaths where ppCase step = markStatus (fst $ psInfo step) ppStep step = case fst $ psInfo step of (Nothing, _) -> superfluousStep (_, Nothing) -> stepLink ["sorry-step"] (_, Just True) -> stepLink ["hl_good"] (_, Just False) -> stepLink ["hl_bad"] <> case psMethod step of Sorry _ -> emptyDoc _ -> removeStep where ppMethod = prettyProofMethod $ psMethod step stepLink cls = linkToPath renderUrl (mkRoute . snd . psInfo $ step) ("proof-step" : cls) ppMethod superfluousStep = withTag "span" [("class","hl_superfluous")] ppMethod removeStep = linkToPath renderUrl (mkRoute . snd . psInfo $ step) ["remove-step"] emptyDoc -- | Render the indexing links for a single lemma lemmaIndex :: HtmlDocument d => RenderUrl -- ^ The url rendering function -> TheoryIdx -- ^ The theory index -> Lemma IncrementalProof -- ^ The lemma -> d lemmaIndex renderUrl tidx l = ( markStatus (psInfo $ root annPrf) $ (kwLemma <-> prettyLemmaName l <> colon) -- FIXME: Reactivate theory editing. -- <-> -- (linkToPath renderUrl lemmaRoute ["edit-link"] editPng <-> -- linkToPath renderUrl lemmaRoute ["delete-link"] deletePng) $-$ nest 2 ( sep [ prettyTraceQuantifier $ get lTraceQuantifier l , doubleQuotes $ prettyLNFormula $ get lFormula l ] ) ) $-$ proofIndex renderUrl mkRoute annPrf where -- editPng = png "/static/img/edit.png" -- deletePng = png "/static/img/delete.png" -- png path = closedTag "img" [("class","icon"),("src",path)] -- lemmaRoute = TheoryPathMR tidx (TheoryLemma $ get lName l) annPrf = annotateLemmaProof l mkRoute proofPath = TheoryPathMR tidx (TheoryProof (get lName l) proofPath) -- | Render the theory index. theoryIndex :: HtmlDocument d => RenderUrl -> TheoryIdx -> ClosedTheory -> d theoryIndex renderUrl tidx thy = foldr1 ($-$) [ kwTheoryHeader $ linkToPath renderUrl (TheoryPathMR tidx TheoryHelp) ["help"] $ text $ 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 lemmaIndex' lemma = lemmaIndex renderUrl tidx 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 renderUrl (TheoryPathMR tidx p) [] (bold n <-> info) messageLink = overview "Message theory" (text "") TheoryMessage ruleLink = overview ruleLinkMsg rulesInfo TheoryRules ruleLinkMsg = "Multiset rewriting rules" ++ if null(theoryAxioms thy) then "" else " and axioms" 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 => System -- ^ System to pretty print. -> TheoryPath -- ^ The sequents path (NOT the path to its PNG) -> d sequentSnippet se path = refDotPath path $-$ preformatted Nothing (prettySystem se) -} -- | A snippet that explains a sub-proof by displaying its proof state, the -- open-goals, and the new cases. subProofSnippet :: HtmlDocument d => RenderUrl -> TheoryIdx -- ^ The theory index. -> TheoryInfo -- ^ The theory info of this index. -> String -- ^ The lemma. -> ProofPath -- ^ The proof path. -> ProofContext -- ^ The proof context. -> IncrementalProof -- ^ The sub-proof. -> d subProofSnippet renderUrl tidx ti lemma proofPath ctxt prf = case psInfo $ root prf of Nothing -> text $ "no annotated constraint system / " ++ nCases ++ " sub-case(s)" Just se -> vcat $ prettyApplicableProofMethods se ++ [ text "" , withTag "h3" [] (text "Constraint system") ] ++ [ refDotPath renderUrl tidx (TheoryProof lemma proofPath) | nonEmptyGraph se ] ++ [ preformatted (Just "sequent") (prettyNonGraphSystem se) , withTag "h3" [] (text $ nCases ++ " sub-case(s)") ] ++ subCases where prettyApplicableProofMethods sys = case proofMethods sys of [] -> [ withTag "h3" [] (text "Constraint System is Solved") ] pms -> [ withTag "h3" [] (text "Applicable Proof Methods:" <-> comment_ (goalRankingName ranking)) , preformatted (Just "methods") (numbered' $ map prettyPM $ zip [1..] pms) , autoProverLinks 'a' "" emptyDoc 0 , autoProverLinks 'b' "bounded-" boundDesc bound ] where boundDesc = text $ " with proof-depth bound " ++ show bound bound = fromMaybe 5 $ apBound $ tiAutoProver ti autoProverLinks key classPrefix nameSuffix bound = hsep [ text (key : ".") , linkToPath renderUrl (AutoProverR tidx CutDFS bound (TheoryProof lemma proofPath)) [classPrefix ++ "autoprove"] (keyword_ $ "autoprove") , parens $ text (toUpper key : ".") <-> linkToPath renderUrl (AutoProverR tidx CutNothing bound (TheoryProof lemma proofPath)) [classPrefix ++ "characterization"] (keyword_ "for all solutions") , nameSuffix ] prettyPM (i, (m, (_cases, expl))) = linkToPath renderUrl (TheoryPathMR tidx (TheoryMethod lemma proofPath i)) ["proof-method"] (prettyProofMethod m) <-> (if null expl then emptyDoc else lineComment_ expl) nCases = show $ M.size $ children prf depth = length proofPath ranking = useHeuristic (apHeuristic $ tiAutoProver ti) depth proofMethods = rankProofMethods ranking ctxt subCases = concatMap refSubCase $ M.toList $ children prf refSubCase (name, prf') = [ withTag "h4" [] (text "Case" <-> text name) , maybe (text "no proof state available") (const $ refDotPath renderUrl tidx $ TheoryProof lemma (proofPath ++ [name])) (psInfo $ root prf') ] -- | A Html document representing the requires case splitting theorem. htmlCaseDistinction :: HtmlDocument d => RenderUrl -> TheoryIdx -> CaseDistKind -> (Int, CaseDistinction) -> d htmlCaseDistinction renderUrl tidx 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 $ prettyGoal $ get cdGoal th ppHeader = hsep [ text "Sources of" <-> ppPrem , parens $ nCases <-> text "cases" ] ppCase (i, (names, se)) = [ withTag "h3" [] $ fsep [ text "Source", int i, text "of", nCases , text " / named ", doubleQuotes (text name) ] , refDotPath renderUrl tidx (TheoryCaseDist kind j i) , withTag "p" [] $ ppPrem , wrapP $ prettyNonGraphSystem se ] where name = intercalate "_" names -- | Build the Html document showing the source cases distinctions. reqCasesSnippet :: HtmlDocument d => RenderUrl -> TheoryIdx -> CaseDistKind -> ClosedTheory -> d reqCasesSnippet renderUrl tidx kind thy = vcat $ htmlCaseDistinction renderUrl tidx kind <$> zip [1..] (getCaseDistinction kind thy) -- | Build the Html document showing the rules of the theory. rulesSnippet :: HtmlDocument d => ClosedTheory -> d rulesSnippet thy = vcat [ ppWithHeader "Fact Symbols with Injective Instances" $ fsepList (text . showFactTagArity) injFacts , ppWithHeader "Multiset Rewriting Rules" $ vsep $ map prettyRuleAC msrRules , ppWithHeader "Axioms Restricting the Set of Traces" $ vsep $ map prettyAxiom $ theoryAxioms thy ] where msrRules = get crProtocol $ getClassifiedRules thy injFacts = S.toList $ getInjectiveFactInsts thy ppWithHeader header body = caseEmptyDoc emptyDoc ( withTag "h2" [] (text header) $$ withTag "p" [("class","monospace rules")] body ) body -- | 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) ] 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 :: RenderUrl -- ^ The function for rendering Urls. -> TheoryInfo -- ^ The info of the theory to render -> TheoryPath -- ^ Path to render -> Html htmlThyPath renderUrl info path = go path where thy = tiTheory info tidx = tiIndex info -- Rendering a HtmlDoc to Html pp :: HtmlDoc Doc -> Html pp d = case renderHtmlDoc d of [] -> toHtml "Trying to render document yielded empty string. This is a bug." cs -> preEscapedToMarkup cs go (TheoryMethod _ _ _) = pp $ text "Cannot display theory method." go TheoryRules = pp $ rulesSnippet thy go TheoryMessage = pp $ messageSnippet thy go (TheoryCaseDist kind _ _) = pp $ reqCasesSnippet renderUrl tidx kind thy go (TheoryProof l p) = pp $ fromMaybe (text "No such lemma or proof path.") $ do lemma <- lookupLemma l thy subProofSnippet renderUrl tidx info l p (getProofContext lemma thy) <$> resolveProofPath thy l p go (TheoryLemma _) = pp $ text "Implement lemma pretty printing!" go TheoryHelp = [hamlet| $newline never

Theory: #{get thyName $ tiTheory info} \ (Loaded at #{formatTime defaultTimeLocale "%T" $ tiTime info} \ from #{show $ tiOrigin info})

Quick introduction