hermit 0.7.0.0 → 0.7.1.0

raw patch · 15 files changed

+181/−161 lines, 15 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• hermit.cabal +5/−5
• src/HERMIT/Dictionary/GHC.hs +52/−19
• src/HERMIT/Dictionary/Local/Case.hs +1/−1
• src/HERMIT/Dictionary/Reasoning.hs +3/−49
• src/HERMIT/Dictionary/WorkerWrapper/Common.hs +2/−2
• src/HERMIT/Kure.hs +21/−0
• src/HERMIT/Lemma.hs +17/−13
• src/HERMIT/Libraries/Int.hs +1/−1
• src/HERMIT/Shell/Command.hs +12/−11
• src/HERMIT/Shell/Externals.hs +11/−11
• src/HERMIT/Shell/KernelEffect.hs +5/−0
• src/HERMIT/Shell/Proof.hs +23/−28
• src/HERMIT/Shell/ScriptToRewrite.hs +0/−5
• src/HERMIT/Shell/ShellEffect.hs +11/−6
• src/HERMIT/Shell/Types.hs +17/−10

@@ -1,5 +1,5 @@ Name:                hermit-Version:             0.7.0.0+Version:             0.7.1.0 Synopsis:            Haskell Equational Reasoning Model-to-Implementation Tunnel Description:   HERMIT is a Haskell-specific toolkit designed to mechanize@@ -15,12 +15,12 @@   .   @    $ hermit Reverse.hs Reverse.hss resume-   [starting HERMIT v0.7.0.0 on Reverse.hs]+   [starting HERMIT v0.7.1.0 on Reverse.hs]    % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:Main:Reverse.hss -fplugin-opt=HERMIT:Main:resume    [1 of 2] Compiling HList            ( HList.hs, HList.o )    Loading package ghc-prim ... linking ... done.    ...-   Loading package hermit-0.7.0.0 ... linking ... done.+   Loading package hermit-0.7.1.0 ... linking ... done.    [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )    Linking Reverse ...    $ ./Reverse@@ -31,12 +31,12 @@   .   @    $ hermit Reverse.hs-   [starting HERMIT v0.7.0.0 on Reverse.hs]+   [starting HERMIT v0.7.1.0 on Reverse.hs]    % ghc Reverse.hs -fforce-recomp -O2 -dcore-lint -fexpose-all-unfoldings -fsimple-list-literals -fplugin=HERMIT -fplugin-opt=HERMIT:*:    [1 of 2] Compiling HList            ( HList.hs, HList.o )    Loading package ghc-prim ... linking ... done.    ...-   Loading package hermit-0.7.0.0 ... linking ... done.+   Loading package hermit-0.7.1.0 ... linking ... done.    [2 of 2] Compiling Main             ( Reverse.hs, Reverse.o )    ===================== Welcome to HERMIT =====================    HERMIT is a toolkit for the interactive transformation of GHC

@@ -1,4 +1,6 @@-{-# LANGUAGE CPP, FlexibleContexts #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE LambdaCase #-} module HERMIT.Dictionary.GHC     ( -- * GHC-based Transformations       -- | This module contains transformations that are reflections of GHC functions, or derived from GHC functions.@@ -15,6 +17,8 @@       -- A zombie is an identifer that has 'OccInfo' 'IAmDead', but still has occurrences.     , lintExprT     , lintModuleT+    , lintQuantifiedT+    , lintClauseT     , occurAnalyseR     , occurAnalyseChangedR     , occurAnalyseExprChangedR@@ -29,9 +33,11 @@ import qualified CoreLint  import           Control.Arrow+import           Control.Monad import           Control.Monad.IO.Class  import           Data.Char (isSpace)+import           Data.Either (partitionEithers) import           Data.List (mapAccumL) import qualified Data.Map as M import           Data.String@@ -64,8 +70,12 @@         , "will catch that however."] .+ Deep .+ Debug .+ Query     , external "lint-module" (promoteModGutsT lintModuleT :: TransformH LCoreTC String)         [ "Runs GHC's Core Lint, which typechecks the current module."] .+ Deep .+ Debug .+ Query-    , external "load-lemma-library" (loadLemmaLibraryT :: HermitName -> TransformH LCore ())+    , external "lint" (promoteT lintQuantifiedT :: TransformH LCoreTC String)+        [ "Lint check a quantified clause." ]+    , external "load-lemma-library" (flip loadLemmaLibraryT Nothing :: HermitName -> TransformH LCore String)         [ "Dynamically load a library of lemmas." ]+    , external "load-lemma-library" ((\nm -> loadLemmaLibraryT nm . Just) :: HermitName -> LemmaName -> TransformH LCore String)+        [ "Dynamically load a specific lemma from a library of lemmas." ]     ]  ------------------------------------------------------------------------@@ -180,16 +190,6 @@ occurrenceAnalysisR :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, HasEmptyContext c, MonadCatch m, Walker c LCore) => Rewrite c m LCore occurrenceAnalysisR = occurAnalyseAndDezombifyR -{- Does not work (no export)--- Here is a hook into the occur analysis, and a way of looking at the result-occAnalysis ::  CoreExpr -> UsageDetails-occAnalysis = fst . occAnal (initOccEnv all_active_rules)--lookupUsageDetails :: UsageDetails -> Var -> Maybe OccInfo-lookupUsageDetails = lookupVarEnv---}- ----------------------------------------------------------------------  -- TODO: this is mostly an example, move somewhere?@@ -227,19 +227,52 @@                 [NonRec v e] | i == v -> e -- the common case that we would have gotten a single non-recursive let                 _ -> mkCoreLets bnds (varToCoreExpr i) +----------------------------------------------------------------------++lintQuantifiedT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)+                => Transform c m Quantified String+lintQuantifiedT = lintQuantifiedWorkT []++lintQuantifiedWorkT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)+                    => [Var] -> Transform c m Quantified String+lintQuantifiedWorkT bs = readerT $ \ (Quantified bs' _) -> quantifiedT successT (lintClauseT (bs++bs')) (flip const)++lintClauseT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)+            => [Var] -> Transform c m Clause String+lintClauseT bs = do+    t <- readerT $ \case Equiv {} -> return $ promoteT ({- arr (mkCoreLams bs) >>> -} lintExprT) -- TODO: why does this break core lint?!+                         _        -> return $ promoteT (lintQuantifiedWorkT bs)+    (w1,w2) <- clauseT t t (const (,))+    return $ unlines [w1,w2]++----------------------------------------------------------------------+ -- | A LemmaLibrary is a transformation that produces a set of lemmas, -- which are then added to the lemma store. It is not allowed to insert -- its own lemmas directly (if it tries they are throw away), but can -- certainly read the existing store. type LemmaLibrary = TransformH () Lemmas -loadLemmaLibraryT :: HermitName -> TransformH x ()-loadLemmaLibraryT nm = contextonlyT $ \ c -> do-    hscEnv <- getHscEnv-    comp <- liftAndCatchIO $ loadLemmaLibrary hscEnv nm-    m' <- applyT comp c () -- TODO: discard side effects-    m <- getLemmas-    putLemmas $ m' `M.union` m+loadLemmaLibraryT :: HermitName -> Maybe LemmaName -> TransformH x String+loadLemmaLibraryT nm mblnm = prefixFailMsg "Loading lemma library failed: " $+    contextonlyT $ \ c -> do+        hscEnv <- getHscEnv+        comp <- liftAndCatchIO $ loadLemmaLibrary hscEnv nm+        ls <- applyT comp c () -- TODO: discard side effects+        nls <- maybe (return $ M.toList ls)+                     (\lnm -> maybe (fail $ show lnm ++ " not found in library.")+                                    (\ l -> return [(lnm,l)])+                                    (M.lookup lnm ls))+                     mblnm+        r <- forM nls $ \ nl@(n, l) -> do+                    er <- attemptM $ applyT lintQuantifiedT c $ lemmaQ l+                    case er of+                        Left msg -> return $ Left $ "Not adding lemma " ++ show n ++ " because lint failed.\n" ++ msg+                        Right _  -> return $ Right nl+        let (fs,nls') = partitionEithers r+        m <- getLemmas+        putLemmas $ (M.fromList nls') `M.union` m+        return $ unlines (fs ++ ["Successfully loaded library " ++ show nm])  loadLemmaLibrary :: HscEnv -> HermitName -> IO LemmaLibrary loadLemmaLibrary hscEnv hnm = do

@@ -226,7 +226,7 @@             appAllR idR (caseAllR idR idR idR (\ n -> let vs = varSetElems (altCaptures !! n)                                                       in if null vs then idR else alphaAltVarsR vs                                               )-                        ) >>> caseFloatArgR Nothing Nothing+                        ) >>> caseFloatArgLemmaR u nm  -- | case (case s1 of alt11 -> e11; alt12 -> e12) of alt21 -> e21; alt22 -> e22 --   ==>

@@ -25,8 +25,7 @@     , lemmaBiR     , lemmaConsequentR     , markLemmaUsedT-    , markLemmaProvedT-    , markLemmaAssumedT+    , markLemmaProvenT     , modifyLemmaT     , showLemmaT     , showLemmasT@@ -40,11 +39,9 @@     , lhsR     , rhsR     , bothR-    , forallVarsT     , verifyQuantifiedT     , verifyEquivalentT     , verifyOrCreateT-    , lintQuantifiedT     , verifyEqualityLeftToRightT     , verifyEqualityCommonTargetT     , verifyIsomorphismT@@ -119,8 +116,6 @@         [ "disjunt new-name lhs-name rhs-name" ]     , external "imply" (\n1 n2 n3 -> implyLemmasT n1 n2 n3 :: TransformH LCore ())         [ "imply new-name antecedent-name consequent-name" ]-    , external "lint" (promoteT lintQuantifiedT :: TransformH LCoreTC String)-        [ "Lint check a quantified clause." ]     , external "lemma-birewrite" (promoteExprBiR . lemmaBiR Obligation :: LemmaName -> BiRewriteH LCore)         [ "Generate a bi-directional rewrite from a lemma." ]     , external "lemma-forward" (forwardT . promoteExprBiR . lemmaBiR Obligation :: LemmaName -> RewriteH LCore)@@ -261,27 +256,6 @@  ------------------------------------------------------------------------------ --- | Original clause passed to function so it can decide how to handle connective.-clauseT :: (Monad m, ExtendPath c Crumb) => Transform c m LCore a -> Transform c m LCore b -> (Clause -> a -> b -> d) -> Transform c m Clause d-clauseT t1 t2 f = readerT $ \ cl -> case cl of-                                      Conj{}  -> conjT  (extractT t1) (extractT t2) (f cl)-                                      Disj{}  -> disjT  (extractT t1) (extractT t2) (f cl)-                                      Impl{}  -> implT  (extractT t1) (extractT t2) (f cl)-                                      Equiv{} -> equivT (extractT t1) (extractT t2) (f cl)--clauseR :: (Monad m, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m LCore -> Rewrite c m Clause-clauseR r1 r2 = readerT $ \case-                             Conj{}  -> conjAllR (extractR r1) (extractR r2)-                             Disj{}  -> disjAllR (extractR r1) (extractR r2)-                             Impl{}  -> implAllR (extractR r1) (extractR r2)-                             Equiv{} -> equivAllR (extractR r1) (extractR r2)---- | Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a 'Quantified'.-forallVarsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m [Var] b -> Transform c m Quantified b-forallVarsT t = quantifiedT t successT const--------------------------------------------------------------------------------- showLemmasT :: Maybe LemmaName -> PrettyPrinter -> PrettyH a showLemmasT mnm pp = do     ls <- getLemmasT@@ -350,24 +324,6 @@  ------------------------------------------------------------------------------ -lintQuantifiedT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)-                => Transform c m Quantified String-lintQuantifiedT = lintQuantifiedWorkT []--lintQuantifiedWorkT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)-                    => [Var] -> Transform c m Quantified String-lintQuantifiedWorkT bs = readerT $ \ (Quantified bs' _) -> quantifiedT successT (lintClauseT (bs++bs')) (flip const)--lintClauseT :: (AddBindings c, BoundVars c, ReadPath c Crumb, ExtendPath c Crumb, HasDynFlags m, MonadCatch m)-            => [Var] -> Transform c m Clause String-lintClauseT bs = do-    t <- readerT $ \case Equiv {} -> return $ promoteT ({- arr (mkCoreLams bs) >>> -} lintExprT) -- TODO: why does this break core lint?!-                         _        -> return $ promoteT (lintQuantifiedWorkT bs)-    (w1,w2) <- clauseT t t (const (,))-    return $ unlines [w1,w2]--------------------------------------------------------------------------------- -- TODO: everything between here and instantiateDictsR needs to be rethought/removed  -- TODO: this is used in century plugin, but otherwise should be removed@@ -691,11 +647,9 @@ markLemmaUsedT :: (HasLemmas m, Monad m) => LemmaName -> Used -> Transform c m a () markLemmaUsedT nm u = modifyLemmaT nm id idR id (const u) -markLemmaProvedT :: (HasLemmas m, Monad m) => LemmaName -> Transform c m a ()-markLemmaProvedT nm = modifyLemmaT nm id idR (const Proven) id+markLemmaProvenT :: (HasLemmas m, Monad m) => LemmaName -> Proven -> Transform c m a ()+markLemmaProvenT nm p = modifyLemmaT nm id idR (const p) id -markLemmaAssumedT :: (HasLemmas m, Monad m) => Bool -> LemmaName -> Transform c m a ()-markLemmaAssumedT user nm = modifyLemmaT nm id idR (const (Assumed user)) id ------------------------------------------------------------------------------  lemmaNameToQuantifiedT :: (HasLemmas m, Monad m) => LemmaName -> Transform c m x Quantified

@@ -157,7 +157,7 @@     verifyOrCreateT u (fromString (show nm ++ "-assumption")) $ Lemma assumptionQ NotProven u False -- unproven, used, permanent      wwFusionQ <- wwFusionQuantifiedT absE repE workRhs-    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ (Assumed False) NotUsed False -- assumed, unused, permanent+    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ BuiltIn NotUsed False -- assumed, unused, permanent      return $ mkCoreLets [NonRec gId g, NonRec workId workRhs] newRhs @@ -177,6 +177,6 @@     verifyOrCreateT u (fromString (show nm ++ "-assumption")) $ Lemma assumptionQ NotProven u False -- unproven, used, permanent      wwFusionQ <- wwFusionQuantifiedT absE repE (varToCoreExpr workId)-    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ (Assumed False) NotUsed False -- assumed, unused, permanent+    insertLemmaT (fromString (show nm ++ "-fusion")) $ Lemma wwFusionQ BuiltIn NotUsed False -- assumed, unused, permanent      return $ mkCoreLets [NonRec workId repFixFE] newRhs

@@ -86,6 +86,7 @@     , implT, implAllR     , equivT, equivAllR     , quantifiedT, quantifiedR+    , clauseT, clauseR, forallVarsT       -- * Applicative       -- | Remove in 7.10     , (<$>)@@ -1359,3 +1360,23 @@     getDynFlags = constT getDynFlags  ---------------------------------------------------------------------++-- | Original clause passed to function so it can decide how to handle connective.+clauseT :: (Monad m, ExtendPath c Crumb) => Transform c m LCore a -> Transform c m LCore b -> (Clause -> a -> b -> d) -> Transform c m Clause d+clauseT t1 t2 f = readerT $ \ cl -> case cl of+                                      Conj{}  -> conjT  (extractT t1) (extractT t2) (f cl)+                                      Disj{}  -> disjT  (extractT t1) (extractT t2) (f cl)+                                      Impl{}  -> implT  (extractT t1) (extractT t2) (f cl)+                                      Equiv{} -> equivT (extractT t1) (extractT t2) (f cl)++clauseR :: (Monad m, ExtendPath c Crumb) => Rewrite c m LCore -> Rewrite c m LCore -> Rewrite c m Clause+clauseR r1 r2 = readerT $ \case+                             Conj{}  -> conjAllR (extractR r1) (extractR r2)+                             Disj{}  -> disjAllR (extractR r1) (extractR r2)+                             Impl{}  -> implAllR (extractR r1) (extractR r2)+                             Equiv{} -> equivAllR (extractR r1) (extractR r2)++-- | Lift a transformation over '[Var]' into a transformation over the universally quantified variables of a 'Quantified'.+forallVarsT :: (AddBindings c, ReadPath c Crumb, ExtendPath c Crumb, Monad m) => Transform c m [Var] b -> Transform c m Quantified b+forallVarsT t = quantifiedT t successT const+

@@ -102,28 +102,32 @@                    }  data Proven = Proven-            | Assumed Bool -- ^ True = assumed by user, False = assumed by library/HERMIT for good reason+            | Assumed -- ^ Assumed by user+            | BuiltIn -- ^ Assumed by library/HERMIT             | NotProven     deriving (Eq, Typeable)  instance Show Proven where     show Proven = "Proven"-    show (Assumed _) = "Assumed"+    show Assumed = "Assumed"+    show BuiltIn = "Built In"     show NotProven = "Not Proven" --- Ordering: NotProven < Assumed True < Assumed False < Proven+instance Enum Proven where+    toEnum 1 = Assumed+    toEnum 2 = BuiltIn+    toEnum 3 = Proven+    toEnum _ = NotProven++    fromEnum NotProven = 0+    fromEnum Assumed = 1+    fromEnum BuiltIn = 2+    fromEnum Proven = 3++-- Ordering: NotProven < Assumed < BuiltIn < Proven instance Ord Proven where     compare :: Proven -> Proven -> Ordering-    compare Proven    Proven    = EQ-    compare (Assumed l) (Assumed r)-        | l && (not r) = LT-        | (not l) && r = GT-        | otherwise = EQ-    compare NotProven NotProven = EQ-    compare Proven    _         = GT-    compare _         Proven    = LT-    compare NotProven _         = LT-    compare _         NotProven = GT+    compare p1 p2 = compare (fromEnum p1) (fromEnum p2)  -- When conjuncting, result is as proven as the least of the two andP :: Proven -> Proven -> Proven

@@ -49,7 +49,7 @@         appMN e = mkCoreApps e [m,n]         appNM e = mkCoreApps e [n,m]         mkEL l r = mkL (Equiv l r)-        mkL cl = Lemma (Quantified [mId,nId] cl) (Assumed False) NotUsed False+        mkL cl = Lemma (Quantified [mId,nId] cl) BuiltIn NotUsed False         mkIL al ar cl cr = mkL (Impl (Quantified [] $ Equiv al ar) (Quantified [] $ Equiv cl cr))      eqE <- findIdT "Data.Eq.==" >>= appToInt >>= appToDict

@@ -124,7 +124,7 @@ #endif      -- Load and run any scripts-    setRunningScript $ Just []+    setRunningScript $ Just [] -- suppress all output until after first scripts run     sequence_ [ case fileName of                  "abort"  -> parseScriptCLT "abort" >>= pushScript                  "resume" -> parseScriptCLT "resume" >>= pushScript@@ -134,8 +134,8 @@               ] `catchFailHard` \ msg -> cl_putStrLn $ "Booting Failure: " ++ msg      let -- Main proof input loop-        loop :: InputT m ()-        loop = do+        loop :: Bool -> InputT m ()+        loop firstInput = do             el <- lift $ do tryM () announceProven                             tryM () forceProofs                             attemptM currentLemma@@ -143,8 +143,7 @@             mExpr <- lift popScriptLine             case mExpr of                 Nothing -> do -- no script running-                    lift $ ifM isRunningScript (return ()) (showWindow Nothing)-                            `catchFailHard` (cl_putStrLn . ("cannot showWindow: " ++))+                    when firstInput $ lift $ showWindow Nothing                     st <- lift get                     mLine <- if cl_nav st                              then liftIO getNavCmd@@ -152,15 +151,17 @@                      case mLine of                         Nothing          -> lift $ performShellEffect Resume-                        Just ('-':'-':_) -> loop+                        Just ('-':'-':_) -> loop False                         Just line        -> if all isSpace line-                                            then loop-                                            else lift (evalScript line `catchFailHard` cl_putStrLn) >> loop-                Just e -> lift (runExprH e `catchFailHard` (\ msg -> setRunningScript Nothing >> cl_putStrLn msg)) >> loop+                                            then loop False+                                            else lift (evalScript line `catchFailHard` cl_putStrLn) >> loop False+                Just e -> do+                    lift (runExprH e `catchFailHard` (\ msg -> setRunningScript Nothing >> cl_putStrLn msg))+                    loop True      -- Start the CLI     let settings = setComplete (completeWordWithPrev Nothing ws_complete completer) defaultSettings-    runInputT settings loop+    runInputT settings (loop True)  -- | Like 'catchM', but checks the 'cl_failhard' setting and does so if needed. catchFailHard :: (MonadCatch m, CLMonad m) => m () -> (String -> m ()) -> m ()@@ -190,7 +191,7 @@   , interpM  $ \ (effect :: ShellEffect)        -> performShellEffect effect   , interpM  $ \ (effect :: ScriptEffect)       -> performScriptEffect effect   , interpEM $ \ (query :: QueryFun)            -> performQuery query-  , interpEM $ \ (t :: UserProofTechnique)      -> performProofShellCommand $ PCUser t+  , interpEM $ \ (t :: UserProofTechnique)      -> performProofShellCommand $ PCEnd $ UserProof t   , interpEM $ \ (cmd :: ProofShellCommand)     -> performProofShellCommand cmd   , interpEM $ \ (TransformLCoreStringBox tt)   -> performQuery (QueryString tt)   , interpEM $ \ (TransformLCoreTCStringBox tt) -> performQuery (QueryString tt)

@@ -51,25 +51,25 @@         [ "switch to navigate mode" ]     , external "command-line"    (CLSModify $ \ st -> return $ Right $ st { cl_nav = False })         [ "switch to command line mode" ]-    , external "set-window"      (CLSModify setWindow)+    , external "set-window"      (CLSModifyAndShow setWindow)         [ "fix the window to the current focus" ]     , external "top"             (Direction T)         [ "move to root of current scope" ]     , external "log"             (Inquiry showDerivationTree)         [ "go back in the derivation" ]                                          .+ VersionControl-    , external "back"            (CLSModify $ versionCmd Back)+    , external "back"            (CLSModifyAndShow $ versionCmd Back)         [ "go back in the derivation" ]                                          .+ VersionControl-    , external "step"            (CLSModify $ versionCmd Step)+    , external "step"            (CLSModifyAndShow $ versionCmd Step)         [ "step forward in the derivation" ]                                     .+ VersionControl-    , external "goto"            (CLSModify . versionCmd . Goto)+    , external "goto"            (CLSModifyAndShow . versionCmd . Goto)         [ "goto a specific step in the derivation" ]                             .+ VersionControl-    , external "goto"            (CLSModify . versionCmd . GotoTag)+    , external "goto"            (CLSModifyAndShow . versionCmd . GotoTag)         [ "goto a specific step in the derivation by tag name" ]                 .+ VersionControl     , external "tag"             (CLSModify . versionCmd . Tag)         [ "name the current step in the derivation" ]                            .+ VersionControl     , external "diff"            Diff         [ "show diff of two ASTs" ]                                              .+ VersionControl-    , external "set-pp-diffonly" (\ bStr -> CLSModify $ \ st ->+    , external "set-pp-diffonly" (\ bStr -> CLSModifyAndShow $ \ st ->         case reads bStr of             [(b,"")] -> return $ Right $ setDiffOnly st b             _        -> return $ Left $ CLError "valid arguments are True and False" )@@ -87,7 +87,7 @@             _        -> return $ Left $ CLError "valid arguments are True and False" )         [ "set-auto-corelint <True|False>; False by default"         , "run core lint type-checker after every rewrite, reverting on failure" ]-    , external "set-pp"          (\ name -> CLSModify $ \ st ->+    , external "set-pp"          (\ name -> CLSModifyAndShow $ \ st ->         case M.lookup name pp_dictionary of             Nothing -> return $ Left $ CLError $ "List of Pretty Printers: " ++ intercalate ", " (M.keys pp_dictionary)             Just pp -> return $ Right $ flip setPrettyOpts (cl_pretty_opts st) $ setPretty st pp) -- careful to preserve the current options@@ -108,20 +108,20 @@     , external "dump-lemma" ((\pp nm fp r w -> getLemmaByNameT nm >>> liftPrettyH (pOptions pp) (ppLemmaT pp nm) >>> dumpT fp pp r w) :: PrettyPrinter -> LemmaName -> FilePath -> String -> Int -> TransformH LCoreTC ())         [ "Dump named lemma to a file."         , "dump-lemma <lemma-name> <filename> <pretty-printer> <renderer> <width>" ]-    , external "set-pp-width" (\ w -> CLSModify $ \ st ->+    , external "set-pp-width" (\ w -> CLSModifyAndShow $ \ st ->             return $ Right $ setPrettyOpts st (updateWidthOption w (cl_pretty_opts st)))         ["set the width of the screen"]-    , external "set-pp-type" (\ str -> CLSModify $ \ st ->+    , external "set-pp-type" (\ str -> CLSModifyAndShow $ \ st ->         case reads str :: [(ShowOption,String)] of             [(opt,"")] -> return $ Right $ setPrettyOpts st (updateTypeShowOption opt (cl_pretty_opts st))             _          -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")         ["set how to show expression-level types (Show|Abstact|Omit)"]-    , external "set-pp-coercion" (\ str -> CLSModify $ \ st ->+    , external "set-pp-coercion" (\ str -> CLSModifyAndShow $ \ st ->         case reads str :: [(ShowOption,String)] of             [(opt,"")] -> return $ Right $ setPrettyOpts st (updateCoShowOption opt (cl_pretty_opts st))             _          -> return $ Left $ CLError "valid arguments are Show, Abstract, and Omit")         ["set how to show coercions (Show|Abstact|Omit)"]-    , external "set-pp-uniques" (\ str -> CLSModify $ \ st ->+    , external "set-pp-uniques" (\ str -> CLSModifyAndShow $ \ st ->         case reads str of             [(b,"")] -> return $ Right $ setPrettyOpts st ((cl_pretty_opts st) { po_showUniques = b } )             _        -> return $ Left $ CLError "valid arguments are True and False")

@@ -69,11 +69,13 @@                 putStrToConsole warns              addAST ast'+    ifM isRunningScript (return ()) (showWindow Nothing)  setPath :: (Injection a LCoreTC, MonadCatch m, CLMonad m) => TransformH a LocalPathH -> ExprH -> m () setPath t expr = do     p <- prefixFailMsg "Cannot find path: " $ queryInContext (promoteT t) Never     modifyLocalPath (<> p) expr+    ifM isRunningScript (return ()) (showWindow Nothing)  goUp :: (MonadCatch m, CLMonad m) => Direction -> ExprH -> m () goUp T expr = modifyLocalPath (const mempty) expr@@ -82,6 +84,7 @@     case rel of         SnocPath [] -> fail "cannot move up, at root of scope."         SnocPath (_:cs) -> modifyLocalPath (const $ SnocPath cs) expr+    ifM isRunningScript (return ()) (showWindow Nothing)  beginScope :: (MonadCatch m, CLMonad m) => ExprH -> m () beginScope expr = do@@ -99,6 +102,7 @@             let todos' = Unproven nm l c ls (p : base, mempty) : todos             modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }         _ -> fail "beginScope: impossible case!"+    ifM isRunningScript (return ()) (showWindow Nothing)  endScope :: (MonadCatch m, CLMonad m) => ExprH -> m () endScope expr = do@@ -122,6 +126,7 @@                     let todos' = Unproven nm l c ls (base', p) : todos                     modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) todos' (cl_proofstack st) }         _ -> fail "endScope: impossible case!"+    ifM isRunningScript (return ()) (showWindow Nothing)  deleteAST :: (MonadCatch m, CLMonad m) => AST -> m () deleteAST ast = gets cl_kernel >>= flip deleteK ast

@@ -17,11 +17,12 @@     , withProofExternals     , performProofShellCommand     , forceProofs-    , ProofShellCommand(PCUser)+    , ProofShellCommand(PCEnd)+    , ProofReason(UserProof)     ) where  import Control.Arrow hiding (loop, (<+>))-import Control.Monad (forM, forM_, liftM, unless)+import Control.Monad (forM, forM_, liftM) import Control.Monad.Error.Class (MonadError(..)) import Control.Monad.State (MonadState, modify, gets) @@ -57,16 +58,16 @@ -- | Externals that get us into the prover shell. externals :: [External] externals = map (.+ Proof)-    [ external "prove-lemma" (CLSModify . interactiveProofIO)+    [ external "prove-lemma" (CLSModifyAndShow . interactiveProofIO)         [ "Proof a lemma interactively." ]     ]  -- | Externals that are added to the dictionary only when in interactive proof mode. proof_externals :: [External] proof_externals = map (.+ Proof)-    [ external "lemma" (PCEnd . Right . (Obligation,))+    [ external "lemma" (PCEnd . LemmaProof Obligation)         [ "Prove lemma by asserting it is alpha-equivalent to an already proven lemma." ]-    , external "lemma-unsafe" (PCEnd . Right . (UnsafeUsed,))+    , external "lemma-unsafe" (PCEnd . LemmaProof UnsafeUsed)         [ "Prove lemma by asserting it is alpha-equivalent to an already proven lemma." ] .+ Unsafe     , external "induction" (PCInduction . cmpString2Var :: String -> ProofShellCommand)         [ "Perform induction on given universally quantified variable."@@ -84,11 +85,11 @@         [ "Split an assumed lemma which is a conjunction/disjunction." ]     , external "split-assumed" PCSplitAssumed         [ "Split an assumed lemma which is a conjunction/disjunction." ]-    , external "end-proof" (PCEnd (Left False))+    , external "end-proof" (PCEnd Reflexivity)         [ "check for alpha-equality, marking the lemma as proven" ]-    , external "end-case" (PCEnd (Left False))+    , external "end-case" (PCEnd Reflexivity)         [ "check for alpha-equality, marking the proof case as proven" ]-    , external "assume" (PCEnd (Left True))+    , external "assume" (PCEnd UserAssume)         [ "mark lemma as assumed" ]     ] @@ -136,16 +137,17 @@         forM_ nls' $ \ (nm,l) -> pushProofStack (Unproven nm l c' [] mempty)  -- | Verify that the lemma has been proven. Throws an exception if it has not.-endProof :: (MonadCatch m, CLMonad m) => Either Bool (Used,LemmaName) -> ExprH -> m ()+endProof :: (MonadCatch m, CLMonad m) => ProofReason -> ExprH -> m () endProof reason expr = do     Unproven nm (Lemma q _ _ temp) c ls _ : _ <- getProofStack     let msg = "The two sides of " ++ quoteShow nm ++ " are not alpha-equivalent."         deleteOr tr = if temp then constT (deleteLemma nm) else tr         t = case reason of-                Left assumed-                    | assumed   -> deleteOr (markLemmaAssumedT True nm)-                    | otherwise -> setFailMsg msg verifyQuantifiedT >> deleteOr (markLemmaProvedT nm)-                Right (u,nm') -> verifyEquivalentT u nm' >> deleteOr (markLemmaProvedT nm)+                UserAssume -> deleteOr (markLemmaProvenT nm Assumed)+                Reflexivity -> setFailMsg msg verifyQuantifiedT >> deleteOr (markLemmaProvenT nm Proven)+                LemmaProof u nm' -> verifyEquivalentT u nm' >> deleteOr (markLemmaProvenT nm Proven)+                UserProof up -> let UserProofTechnique tr = up+                                in extractT tr >> deleteOr (markLemmaProvenT nm Proven)     queryInFocus (constT (withLemmas (M.fromList ls) $ applyT t c q) :: TransformH Core ())                  (Always $ unparseExprH expr ++ " -- proven " ++ quoteShow nm)     _ <- popProofStack@@ -165,15 +167,6 @@           go PCConjunction        = proveConjunction str           go (PCInstAssumed i v cs) = instAssumed i v cs str           go (PCSplitAssumed i)   = splitAssumed i str-          go (PCUser prf)         = do-                let UserProofTechnique t = prf -- may add more constructors later-                -- note: we assume that if 't' completes without failing,-                -- the lemma is proved, we don't actually check-                todo : _ <- getProofStack-                queryInFocus (inProofFocusT todo t >> unless (lemmaT $ ptLemma todo) (markLemmaProvedT (ptName todo)))-                             (Changed str)-                _ <- popProofStack-                cl_putStrLn $ "Successfully proven: " ++ show (ptName todo)           go (PCEnd why)          = endProof why expr  proveConsequent :: (MonadCatch m, CLMonad m) => String -> m ()@@ -182,7 +175,7 @@     (c, Impl ante con) <- setFailMsg "not an implication" $                           queryInFocus (inProofFocusT todo (contextT &&& projectT)) Never     let nm = ptName todo-        ls = (nm <> "-antecedent", Lemma ante (Assumed False) NotUsed True) : ptAssumed todo+        ls = (nm <> "-antecedent", Lemma ante BuiltIn NotUsed True) : ptAssumed todo     (k,ast) <- gets (cl_kernel &&& cl_cursor)     addAST =<< tellK k expr ast     _ <- popProofStack@@ -269,7 +262,7 @@                 -- TODO rethink the discardUniVars          let nms = [ fromString ("ind-hyp-" ++ show n) | n :: Int <- [0..] ]-            hypLemmas = zip nms $ zipWith4 Lemma qs (repeat (Assumed False)) (repeat NotUsed) (repeat True)+            hypLemmas = zip nms $ zipWith4 Lemma qs (repeat BuiltIn) (repeat NotUsed) (repeat True)             lemmaName = fromString $ show nm ++ "-induction-case-" ++ caseName             caseLemma = Lemma (mkQuantified (delete i bs ++ vs) lhsE rhsE) NotProven Obligation True @@ -306,11 +299,13 @@     | PCConjunction     | PCSplitAssumed Int     | PCInstAssumed Int (Var -> Bool) CoreString-    | PCUser UserProofTechnique-    | PCEnd (Either Bool (Used,LemmaName)) -- ^ Left True = assume this lemma-                                           --   Left False = check for alpha-equivalence-                                           --   Right (u,nm) = try to prove with given lemma, marking it u+    | PCEnd ProofReason     deriving Typeable++data ProofReason = UserProof UserProofTechnique -- ^ Run the technique, mark Proven if succeeds+                 | UserAssume                   -- ^ Assume+                 | Reflexivity                  -- ^ Check for alpha-equivalence first+                 | LemmaProof Used LemmaName    -- ^ Used should be 'UnsafeUsed' or 'Obligation'  -- keep abstract to avoid breaking things if we modify this later newtype UserProofTechnique = UserProofTechnique (TransformH LCoreTC ())

@@ -11,7 +11,6 @@     , popScriptLine     , pushScriptLine     , pushScript-    , runScript     , fileToScript     , scriptToRewrite     , ScriptEffect(..)@@ -65,10 +64,6 @@ --   The script is given the same name as the filepath. loadAndRun :: FilePath -> ScriptEffect loadAndRun fp = SeqMeta [LoadFile fp fp, RunScript fp]--runScript :: MonadState CommandLineState m => (ExprH -> m ()) -> m ()-runScript run = go-    where go = popScriptLine >>= maybe (return ()) (\e -> run e >> go)  popScriptLine :: MonadState CommandLineState m => m (Maybe ExprH) popScriptLine = gets cl_running_script >>= maybe (return Nothing)

@@ -36,11 +36,12 @@ ----------------------------------------------------------------------------------  data ShellEffect :: * where-    Abort      :: ShellEffect-    CLSModify  :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect-    PluginComp :: PluginM () -> ShellEffect-    Continue   :: ShellEffect-    Resume     :: ShellEffect+    Abort             :: ShellEffect+    CLSModify         :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect+    CLSModifyAndShow  :: (CommandLineState -> IO (Either CLException CommandLineState)) -> ShellEffect+    PluginComp        :: PluginM () -> ShellEffect+    Continue          :: ShellEffect+    Resume            :: ShellEffect     deriving Typeable  instance Extern ShellEffect where@@ -55,7 +56,11 @@ performShellEffect Resume = announceUnprovens >> gets cl_cursor >>= resume performShellEffect Continue = announceUnprovens >> get >>= continue -performShellEffect (CLSModify f)  = get >>= liftAndCatchIO . f >>= either throwError put+performShellEffect (CLSModify f) = get >>= liftAndCatchIO . f >>= either throwError put++performShellEffect (CLSModifyAndShow f) = do+    get >>= liftAndCatchIO . f >>= either throwError put+    ifM isRunningScript (return ()) (showWindow Nothing)  performShellEffect (PluginComp m) = pluginM m 

@@ -25,6 +25,7 @@ import Control.Monad.Trans.Except (ExceptT(..), runExceptT)  import Data.Dynamic+import Data.List (intercalate) import qualified Data.Map as M import Data.Maybe (fromMaybe, isJust) import Data.Monoid (mempty, (<>))@@ -507,14 +508,20 @@         _ -> fail "currentLemma: unproven lemma not on top of stack!"  announceProven :: (MonadCatch m, CLMonad m) => m ()-announceProven = getProofStack >>= go-    where go (MarkProven nm temp : r) = do-            queryInFocus (if temp then constT (deleteLemma nm) else modifyLemmaT nm id idR (const Proven) id :: TransformH Core ())-                         (Always $ "-- proven " ++ quoteShow nm) -- comment in script-            -- take it off the stack for the new AST-            modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) r (cl_proofstack st) }-            cl_putStrLn ("Successfully proven: " ++ show nm) >> go r-          go _ = return ()+announceProven = getProofStackEmpty >>= go []+    where go ps (MarkProven nm temp : r) = do+            let t = if temp then constT (deleteLemma nm) else modifyLemmaT nm id idR (const Proven) id+            go ((nm,t):ps) r+          go ps r = case ps of+                        [] -> return ()+                        _  -> do -- adjust the stack for the existing AST, because we don't want+                                 -- to replay these after a 'goto'!+                                 let (nms, ts) = unzip $ reverse ps+                                     commaNames f = intercalate ", " (map f nms)+                                 modify $ \ st -> st { cl_proofstack = M.insert (cl_cursor st) r (cl_proofstack st) }+                                 queryInFocus (sequence_ ts :: TransformH Core ())+                                              (Always $ "-- proven " ++ commaNames quoteShow)+                                 cl_putStrLn ("Successfully proven: " ++ commaNames show)  announceUnprovens :: (MonadCatch m, CLMonad m) => m () announceUnprovens = do@@ -522,7 +529,7 @@     sf <- gets cl_safety     case sf of         StrictSafety -> do-            let ls = [ nl | nl@(_,Lemma _ p u _) <- M.toList m, p `elem` [NotProven, Assumed True], u /= NotUsed ]+            let ls = [ nl | nl@(_,Lemma _ p u _) <- M.toList m, p `elem` [NotProven, Assumed], u /= NotUsed ]             forM_ ls $ \ nl@(nm,_) -> do                 cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."                 printLemma stdout c mempty nl@@ -533,7 +540,7 @@                 cl_putStrLn $ "Fatal: Lemma " ++ show nm ++ " has not been proven, but was used."                 printLemma stdout c mempty nl             unless (null np) abort -- don't finish if this happens-            let as = [ nl | nl@(_,Lemma _ (Assumed True) u _) <- M.toList m, u /= NotUsed ]+            let as = [ nl | nl@(_,Lemma _ Assumed u _) <- M.toList m, u /= NotUsed ]             forM_ as $ \ nl@(nm,_) -> do                 cl_putStrLn $ "Warning: Lemma " ++ show nm ++ " was assumed but not proven."                 printLemma stdout c mempty nl