diff --git a/saw-central/src/SAWCentral/Bisimulation.hs b/saw-central/src/SAWCentral/Bisimulation.hs index 142f45b51b..4040d0c728 100644 --- a/saw-central/src/SAWCentral/Bisimulation.hs +++ b/saw-central/src/SAWCentral/Bisimulation.hs @@ -110,7 +110,7 @@ import SAWCentral.BisimulationTheorem import SAWCentral.Builtins (unfold_term) import SAWCentral.Options (Verbosity(..)) import SAWCentral.Panic (panic) -import SAWCentral.Proof +import SAWCentral.Proof hiding (applyTheorem) import SAWCentral.Prover.Util (checkBooleanSchema) import SAWCentral.Value @@ -154,10 +154,10 @@ proveAll script ts = do , goalName = "prove_bisim" , goalLoc = show pos , goalDesc = "" - , goalSequent = propToSequent prop + , goalProp = prop , goalTags = mempty } - res <- runProofScript script prop goal Nothing "prove_bisim" True False + res <- runProofScript script prop goal Nothing "prove_bisim" True case res of UnfinishedProof {} -> failProof res ValidProof _ thm -> recordTheoremProof thm diff --git a/saw-central/src/SAWCentral/Builtins.hs b/saw-central/src/SAWCentral/Builtins.hs index 50f7f536a8..4850de4120 100644 --- a/saw-central/src/SAWCentral/Builtins.hs +++ b/saw-central/src/SAWCentral/Builtins.hs @@ -31,7 +31,6 @@ module SAWCentral.Builtins ( assumeUnsat, admitProof, trivial, - split_goal, show_term, print_term, print_term_depth, @@ -39,7 +38,6 @@ module SAWCentral.Builtins ( print_goal, print_goal_inline, print_goal_summary, - print_focus, goal_num, print_goal_depth, printGoalConsts, @@ -49,19 +47,9 @@ module SAWCentral.Builtins ( normalize_term, normalize_term_opaque, goal_normalize, - unfocus, - focus_concl, - focus_hyp, - delete_hyps, - retain_hyps, - delete_concl, - retain_concl, - goal_cut, - normalize_sequent, unfoldGoal, unfoldFixOnceGoal, simplifyGoal, - simplifyGoalWithLocals, hoistIfsInGoalPrim, term_type, goal_eval, @@ -69,14 +57,8 @@ module SAWCentral.Builtins ( beta_reduce_goal, goal_apply, goal_exact, - goal_intro_hyp, - goal_intro_hyps, - goal_revert_hyp, goal_intro, goal_insert, - goal_insert_and_specialize, - goal_specialize_hyp, - goal_apply_hyp, goal_num_when, goal_when, goal_has_tags, @@ -196,7 +178,9 @@ module SAWCentral.Builtins ( prove_core, core_axiom, core_thm, + term_thm, specialize_theorem, + apply_thm, get_opt, get_nopts, get_env, @@ -280,7 +264,6 @@ import SAWCore.Recognizer import SAWCore.Prelude (scEq) import SAWCore.SharedTerm import SAWCore.Typechecker (tcInsertModule, inferCompleteTerm) -import SAWCore.Term.Functor import qualified SAWCore.TermNet as Net import CryptolSAWCore.TypedTerm @@ -576,13 +559,13 @@ quickcheckGoal sc n = do execTactic $ tacticSolve $ \goal -> io $ do printOutLn opts Warn $ "WARNING: using quickcheck to prove goal..." hFlush stdout - satq <- sequentToSATQuery sc mempty (goalSequent goal) + satq <- propToSATQuery sc mempty (goalProp goal) testGen <- prepareSATQuery sc satq - let stats = solverStats "quickcheck" (sequentSharedSize (goalSequent goal)) + let stats = solverStats "quickcheck" (propSharedSize (goalProp goal)) runManyTests testGen n >>= \case Nothing -> do printOutLn opts Info $ "checked " ++ show n ++ " cases." - return (stats, SolveSuccess (QuickcheckEvidence n (goalSequent goal))) + return (stats, SolveSuccess (QuickcheckEvidence n (goalProp goal))) Just cex -> return (stats, SolveCounterexample cex) assumeValid :: ProofScript () @@ -591,8 +574,8 @@ assumeValid = do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is valid" pos <- SV.getPosition let admitMsg = "assumeValid: " <> Text.pack (goalName goal) - let stats = solverStats "ADMITTED" (sequentSharedSize (goalSequent goal)) - return (stats, SolveSuccess (Admitted admitMsg pos (goalSequent goal))) + let stats = solverStats "ADMITTED" (propSharedSize (goalProp goal)) + return (stats, SolveSuccess (Admitted admitMsg pos (goalProp goal))) assumeUnsat :: ProofScript () assumeUnsat = @@ -600,27 +583,22 @@ assumeUnsat = do printOutLnTop Warn $ "WARNING: assuming goal " ++ goalName goal ++ " is unsat" pos <- SV.getPosition let admitMsg = "assumeUnsat: " <> Text.pack (goalName goal) - let stats = solverStats "ADMITTED" (sequentSharedSize (goalSequent goal)) - return (stats, SolveSuccess (Admitted admitMsg pos (goalSequent goal))) + let stats = solverStats "ADMITTED" (propSharedSize (goalProp goal)) + return (stats, SolveSuccess (Admitted admitMsg pos (goalProp goal))) admitProof :: Text -> ProofScript () admitProof msg = execTactic $ tacticSolve $ \goal -> do printOutLnTop Warn $ "WARNING: admitting goal " ++ goalName goal pos <- SV.getPosition - let stats = solverStats "ADMITTED" (sequentSharedSize (goalSequent goal)) - return (stats, SolveSuccess (Admitted msg pos (goalSequent goal))) + let stats = solverStats "ADMITTED" (propSharedSize (goalProp goal)) + return (stats, SolveSuccess (Admitted msg pos (goalProp goal))) trivial :: ProofScript () trivial = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticTrivial sc) -split_goal :: ProofScript () -split_goal = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticSplit sc) - show_term :: Term -> TopLevel Text show_term t = do sc <- getSharedContext @@ -657,7 +635,7 @@ write_goal fp = sc <- getSharedContext liftIO $ do nenv <- scGetNamingEnv sc - let output = ppSequent opts nenv (goalSequent goal) + let output = ppProp opts nenv (goalProp goal) writeFile fp (unlines [goalSummary goal, output]) print_goal :: ProofScript () @@ -666,7 +644,7 @@ print_goal = do opts <- SV.getPPOpts sc <- getSharedContext nenv <- io (scGetNamingEnv sc) - let output = ppSequent opts nenv (goalSequent goal) + let output = ppProp opts nenv (goalProp goal) printOutLnTop Info (unlines [goalSummary goal, output]) -- | Print the current goal that a proof script is attempting to prove, without @@ -686,7 +664,7 @@ print_goal_inline noInline = PPS.Hash _ -> warnIncremental >> pure opts sc <- getSharedContext nenv <- io (scGetNamingEnv sc) - let output = ppSequent opts' nenv (goalSequent goal) + let output = ppProp opts' nenv (goalProp goal) printOutLnTop Info (unlines [goalSummary goal, output]) where warnIncremental = @@ -701,23 +679,6 @@ print_goal_summary = execTactic $ tacticId $ \goal -> printOutLnTop Info (goalSummary goal) -print_focus :: ProofScript () -print_focus = - execTactic $ tacticId $ \goal -> - do opts <- SV.getPPOpts - sc <- getSharedContext - nenv <- io (scGetNamingEnv sc) - case sequentGetFocus (goalSequent goal) of - Nothing -> - printOutLnTop Warn "Sequent is not focused" - Just (Left (i,h)) -> - let output = ppProp opts nenv h in - printOutLnTop Info (unlines ["Hypothesis " ++ show i, show output]) - Just (Right (i,c)) -> - let output = ppProp opts nenv c in - printOutLnTop Info (unlines ["Conclusion " ++ show i, show output]) - - goal_num :: ProofScript Int goal_num = execTactic $ tacticId $ \goal -> @@ -730,7 +691,7 @@ print_goal_depth n = sc <- getSharedContext let opts' = opts { PPS.ppMaxDepth = Just n } nenv <- io (scGetNamingEnv sc) - let output = ppSequent opts' nenv (goalSequent goal) + let output = ppProp opts' nenv (goalProp goal) printOutLnTop Info (unlines [goalSummary goal, output]) printGoalConsts :: ProofScript () @@ -738,7 +699,7 @@ printGoalConsts = execTactic $ tacticId $ \goal -> do opts <- SV.getPPOpts sc <- getSharedContext - let cs = sequentConstantSet (goalSequent goal) + let cs = propConstantSet (goalProp goal) printOne (idnum, info) = do let nm = Name idnum info nm' <- liftIO $ ppName sc opts nm @@ -748,8 +709,8 @@ printGoalConsts = printGoalSize :: ProofScript () printGoalSize = execTactic $ tacticId $ \goal -> - do printOutLnTop Info $ "Goal shared size: " ++ show (sequentSharedSize (goalSequent goal)) - printOutLnTop Info $ "Goal unshared size: " ++ show (sequentTreeSize (goalSequent goal)) + do printOutLnTop Info $ "Goal shared size: " ++ show (propSharedSize (goalProp goal)) + printOutLnTop Info $ "Goal unshared size: " ++ show (propTreeSize (goalProp goal)) resolveNames :: [Text] -> TopLevel (Set VarIndex) resolveNames nms = @@ -818,86 +779,15 @@ goal_normalize opaque = let primQualNames = map moduleIdentToQualName (Map.keys constMap) primIdxs <- io $ traverse (scResolveQualName sc) primQualNames let opaqueSet = Set.fromList (catMaybes primIdxs ++ idxs) - sqt' <- io $ traverseSequentWithFocus (normalizeProp sc opaqueSet) (goalSequent goal) + sqt' <- io $ normalizeProp sc opaqueSet (goalProp goal) return (sqt', NormalizePropEvidence opaqueSet) -unfocus :: ProofScript () -unfocus = - execTactic $ tacticChange $ \goal -> - do let sqt' = unfocusSequent (goalSequent goal) - return (sqt', structuralEvidence sqt') - -focus_concl :: Integer -> ProofScript () -focus_concl i = - execTactic $ tacticChange $ \goal -> - case focusOnConcl i (goalSequent goal) of - Nothing -> fail "focus_concl : not enough conclusions" - Just sqt' -> return (sqt', structuralEvidence sqt') - -focus_hyp :: Integer -> ProofScript () -focus_hyp i = - execTactic $ tacticChange $ \goal -> - case focusOnHyp i (goalSequent goal) of - Nothing -> fail "focus_hyp : not enough hypotheses" - Just sqt' -> return (sqt', structuralEvidence sqt') - -delete_hyps :: [Integer] -> ProofScript () -delete_hyps hs = - execTactic $ tacticChange $ \goal -> - let sqt' = filterHyps (BlackList (Set.fromList hs)) (goalSequent goal) - in return (sqt', structuralEvidence sqt') - -retain_hyps :: [Integer] -> ProofScript () -retain_hyps hs = - execTactic $ tacticChange $ \goal -> - let sqt' = filterHyps (WhiteList (Set.fromList hs)) (goalSequent goal) - in return (sqt', structuralEvidence sqt') - -delete_concl :: [Integer] -> ProofScript () -delete_concl gs = - execTactic $ tacticChange $ \goal -> - let sqt' = filterConcls (BlackList (Set.fromList gs)) (goalSequent goal) - in return (sqt', structuralEvidence sqt') - -retain_concl :: [Integer] -> ProofScript () -retain_concl gs = - execTactic $ tacticChange $ \goal -> - let sqt' = filterConcls (WhiteList (Set.fromList gs)) (goalSequent goal) - in return (sqt', structuralEvidence sqt') - - -goal_cut :: Term -> ProofScript () -goal_cut tm = - do -- TODO? Theres a bit of duplicated work here - -- and in boolToProp, termToProp. - -- maybe we can consolatate - sc <- SV.scriptTopLevel getSharedContext - p <- SV.scriptTopLevel $ io $ - do tp <- scWhnf sc =<< scTypeOf sc tm - case () of - _ | Just () <- asBoolType tp - -> boolToProp sc [] tm - - | Just s <- asSort tp, s == propSort - -> termToProp sc tm - - | otherwise - -> fail "goal_cut: expected Bool or Prop term" - execTactic (tacticCut sc p) - -normalize_sequent :: ProofScript () -normalize_sequent = - execTactic $ tacticChange $ \goal -> - do sc <- getSharedContext - sqt' <- io $ normalizeSequent sc (goalSequent goal) - return (sqt', NormalizeSequentEvidence sqt') - unfoldGoal :: [Text] -> ProofScript () unfoldGoal unints = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext unints' <- resolveNames unints - sqt' <- traverseSequentWithFocus (io . unfoldProp sc unints') (goalSequent goal) + sqt' <- io $ unfoldProp sc unints' (goalProp goal) return (sqt', UnfoldEvidence unints') unfoldFixOnceGoal :: [Text] -> ProofScript () @@ -905,30 +795,21 @@ unfoldFixOnceGoal unints = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext unints' <- resolveNames unints - sqt' <- traverseSequentWithFocus (io . unfoldFixOnceProp sc unints') (goalSequent goal) + sqt' <- io $ unfoldFixOnceProp sc unints' (goalProp goal) return (sqt', UnfoldFixOnceEvidence unints') simplifyGoal :: SV.SAWSimpset -> ProofScript () simplifyGoal ss = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext - sqt' <- traverseSequentWithFocus (\p -> snd <$> io (simplifyProp sc ss p)) (goalSequent goal) - return (sqt', RewriteEvidence [] ss) - -simplifyGoalWithLocals :: [Integer] -> SV.SAWSimpset -> ProofScript () -simplifyGoalWithLocals hs ss = - execTactic $ tacticChange $ \goal -> - do sc <- getSharedContext - ss' <- io (localHypSimpset sc (goalSequent goal) hs ss) - sqt' <- traverseSequentWithFocus - (\p -> snd <$> io (simplifyProp sc ss' p)) (goalSequent goal) - return (sqt', RewriteEvidence hs ss) + sqt' <- snd <$> io (simplifyProp sc ss (goalProp goal)) + return (sqt', RewriteEvidence ss) hoistIfsInGoalPrim :: ProofScript () hoistIfsInGoalPrim = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext - sqt' <- traverseSequentWithFocus (io . hoistIfsInProp sc) (goalSequent goal) + sqt' <- io $ hoistIfsInProp sc (goalProp goal) return (sqt', HoistIfsEvidence) term_type :: TypedTerm -> TopLevel C.Schema @@ -947,7 +828,7 @@ goal_eval unints = do sc <- getSharedContext unintSet <- resolveNames unints what4PushMuxOps <- gets rwWhat4PushMuxOps - sqt' <- traverseSequentWithFocus (io . evalProp sc what4PushMuxOps unintSet) (goalSequent goal) + sqt' <- io $ evalProp sc what4PushMuxOps unintSet (goalProp goal) return (sqt', EvalEvidence unintSet) congruence_for :: TypedTerm -> TopLevel TypedTerm @@ -1003,7 +884,7 @@ beta_reduce_goal :: ProofScript () beta_reduce_goal = execTactic $ tacticChange $ \goal -> do sc <- getSharedContext - sqt' <- traverseSequentWithFocus (io . betaReduceProp sc) (goalSequent goal) + sqt' <- io $ betaReduceProp sc (goalProp goal) return (sqt', ConversionEvidence sqt') goal_apply :: Theorem -> ProofScript () @@ -1016,21 +897,6 @@ goal_exact tm = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticExact sc (ttTerm tm)) -goal_intro_hyp :: ProofScript () -goal_intro_hyp = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticIntroHyps sc 1) - -goal_intro_hyps :: Integer -> ProofScript () -goal_intro_hyps n = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticIntroHyps sc n) - -goal_revert_hyp :: Integer -> ProofScript () -goal_revert_hyp i = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticRevertHyp sc i) - goal_intro :: Text -> ProofScript TypedTerm goal_intro s = do sc <- SV.scriptTopLevel getSharedContext @@ -1039,22 +905,23 @@ goal_intro s = goal_insert :: Theorem -> ProofScript () goal_insert thm = do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticInsert sc thm []) - -goal_insert_and_specialize :: Theorem -> [TypedTerm] -> ProofScript () -goal_insert_and_specialize thm tms = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticInsert sc thm (map ttTerm tms)) - -goal_specialize_hyp :: [TypedTerm] -> ProofScript () -goal_specialize_hyp ts = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticSpecializeHyp sc (map ttTerm ts)) - -goal_apply_hyp :: Integer -> ProofScript () -goal_apply_hyp n = - do sc <- SV.scriptTopLevel getSharedContext - execTactic (tacticApplyHyp sc n) + let p = unProp (thmProp thm) + -- Build the term `\(x : p) (q : Prop) (f : p -> q) -> f x` + -- which has type `p -> (q : Prop) -> (p -> q) -> q`. + prf <- + liftIO $ + do x <- scFreshVariable sc "x" p + qt <- scSort sc Un.propSort + q <- scFreshVariable sc "q" qt + ft <- scFun sc p q + f <- scFreshVariable sc "f" ft + fx <- scApply sc f x + scAbstractTerms sc [x, q, f] fx + -- Create theorem `p -> (q : Prop) -> (p -> q) -> q` + rule1 <- SV.scriptTopLevel $ term_thm prf + -- Create theorem `(q : Prop) -> (p -> q) -> q` + rule2 <- SV.scriptTopLevel $ apply_thm rule1 [thm] + execTactic (tacticApply sc rule2) goal_num_when :: Int -> ProofScript () -> ProofScript () goal_num_when n script = @@ -1113,7 +980,7 @@ satArbitrary doCNF execName args = args' = map Text.unpack args (mb, stats) <- Prover.abcSatExternal proxy sc doCNF execName' args' g case mb of - Nothing -> return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) + Nothing -> return (stats, SolveSuccess (SolverEvidence stats (goalProp g))) Just a -> return (stats, SolveCounterexample a) writeAIGPrim :: Text -> Term -> TopLevel () @@ -1160,18 +1027,18 @@ proveUnintSBV conf unints = (Prover.proveUnintSBV conf to) unintSet -- | Given a continuation which calls a prover, call the continuation on the --- given 'Sequent' and return a 'SolveResult'. If there is a 'SolverCache', +-- given 'Prop' and return a 'SolveResult'. If there is a 'SolverCache', -- do not call the continuation if the goal has an already cached result, -- and otherwise save the result of the call to the cache. applyProverToGoal :: [SolverBackend] -> [SolverBackendOption] -> (SATQuery -> TopLevel (Maybe CEX, Text)) - -> Set VarIndex -> Sequent + -> Set VarIndex -> Prop -> TopLevel (SolverStats, SolveResult) applyProverToGoal backends opts f unintSet sqt = do sc <- getSharedContext let opt_backends = concatMap optionBackends opts vs <- io $ getSolverBackendVersions (backends ++ opt_backends) - satq <- io $ sequentToSATQuery sc unintSet sqt + satq <- io $ propToSATQuery sc unintSet sqt k <- io $ mkSolverCacheKey sc vs opts satq (mb, solver_name) <- SV.onSolverCache (lookupInSolverCache k) >>= \case -- Use a cached result if one exists (and it's valid w.r.t our query) @@ -1181,7 +1048,7 @@ applyProverToGoal backends opts f unintSet sqt = do Just v -> SV.onSolverCache (insertInSolverCache k v) >> return res Nothing -> return res - let stats = solverStats solver_name (sequentSharedSize sqt) + let stats = solverStats solver_name (propSharedSize sqt) case mb of Nothing -> return (stats, SolveSuccess (SolverEvidence stats sqt)) Just a -> return (stats, SolveCounterexample a) @@ -1192,7 +1059,7 @@ wrapProver :: Set VarIndex -> ProofScript () wrapProver backends opts f unints = - execTactic $ tacticSolve $ applyProverToGoal backends opts f unints . goalSequent + execTactic $ tacticSolve $ applyProverToGoal backends opts f unints . goalProp wrapW4Prover :: SolverBackend -> [SolverBackendOption] -> @@ -1216,10 +1083,10 @@ wrapW4ProveExporter f unints path ext = do execTactic $ tacticSolve $ \g -> do let file = path ++ "." ++ goalType g ++ show (goalNum g) ++ ext sc <- getSharedContext - satq <- io $ sequentToSATQuery sc unintSet (goalSequent g) + satq <- io $ propToSATQuery sc unintSet (goalProp g) (_, solver_name) <- f hashConsing file satq - let stats = solverStats solver_name (sequentSharedSize (goalSequent g)) - return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) + let stats = solverStats solver_name (propSharedSize (goalProp g)) + return (stats, SolveSuccess (SolverEvidence stats (goalProp g))) -------------------------------------------------- proveABC_SBV :: ProofScript () @@ -1352,8 +1219,8 @@ proveWithSATExporter :: proveWithSATExporter exporter unintSet path sep ext = execTactic $ tacticSolve $ \g -> do let file = path ++ sep ++ goalType g ++ show (goalNum g) ++ ext - stats <- Prover.proveWithSATExporter exporter unintSet file (goalSequent g) - return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) + stats <- Prover.proveWithSATExporter exporter unintSet file (goalProp g) + return (stats, SolveSuccess (SolverEvidence stats (goalProp g))) proveWithPropExporter :: (FilePath -> Prop -> TopLevel a) -> @@ -1364,10 +1231,9 @@ proveWithPropExporter :: proveWithPropExporter exporter path sep ext = execTactic $ tacticSolve $ \g -> do let file = path ++ sep ++ goalType g ++ show (goalNum g) ++ ext - sc <- getSharedContext - p <- io $ sequentToProp sc (goalSequent g) + let p = goalProp g stats <- Prover.proveWithPropExporter exporter file p - return (stats, SolveSuccess (SolverEvidence stats (goalSequent g))) + return (stats, SolveSuccess (SolverEvidence stats (goalProp g))) offline_aig :: FilePath -> ProofScript () offline_aig path = @@ -1431,10 +1297,10 @@ provePrim script t = do , goalName = "prove_prim" , goalLoc = show pos , goalDesc = "" - , goalSequent = propToSequent prop + , goalProp = prop , goalTags = mempty } - res <- SV.runProofScript script prop goal Nothing "prove_prim" True False + res <- SV.runProofScript script prop goal Nothing "prove_prim" True case res of UnfinishedProof pst -> printOutLnTop Info $ "prove: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)" @@ -1457,11 +1323,11 @@ proveHelper nm script t f = do , goalName = nm , goalLoc = show pos , goalDesc = "" - , goalSequent = propToSequent prop + , goalProp = prop , goalTags = mempty } opts <- SV.getPPOpts - res <- SV.runProofScript script prop goal Nothing (Text.pack nm) True False + res <- SV.runProofScript script prop goal Nothing (Text.pack nm) True let failProof pst = fail $ "prove: " ++ show (length (psGoals pst)) ++ " unsolved subgoal(s)\n" ++ Text.unpack (ppProofResult opts res) @@ -1506,10 +1372,10 @@ satPrim script t = do , goalName = "sat" , goalLoc = show pos , goalDesc = "" - , goalSequent = propToSequent prop + , goalProp = prop , goalTags = mempty } - res <- SV.runProofScript script prop goal Nothing "sat" False False + res <- SV.runProofScript script prop goal Nothing "sat" False case res of InvalidProof stats cex _ -> return (SV.Sat stats cex) ValidProof stats _thm -> return (SV.Unsat stats) @@ -1690,7 +1556,7 @@ check_goal = g : _ -> SV.scriptTopLevel $ do sc <- getSharedContext - io $ checkSequent sc (goalSequent g) + io $ checkProp sc (goalProp g) freshSymbolicPrim :: Text -> C.Schema -> TopLevel TypedTerm freshSymbolicPrim x schema@(C.Forall [] [] ct) = do @@ -1964,7 +1830,7 @@ term_theories unints t = do unintSet <- resolveNames unints hashConsing <- gets SV.rwWhat4HashConsing prop <- io (predicateToProp sc Universal (ttTerm t)) - Prover.what4Theories unintSet hashConsing (propToSequent prop) + Prover.what4Theories unintSet hashConsing prop default_typed_term :: TypedTerm -> TopLevel TypedTerm default_typed_term tt = do @@ -2150,6 +2016,15 @@ core_thm input = SV.putTheoremDB db' SV.returnTheoremProof thm +term_thm :: Term -> TopLevel Theorem +term_thm t = + do sc <- getSharedContext + pos <- SV.getPosition + db <- SV.getTheoremDB + (thm, db') <- io (proofByTerm sc db t pos "term_thm") + SV.putTheoremDB db' + SV.returnTheoremProof thm + specialize_theorem :: Theorem -> [TypedTerm] -> TopLevel Theorem specialize_theorem thm ts = do sc <- getSharedContext @@ -2160,6 +2035,16 @@ specialize_theorem thm ts = SV.putTheoremDB db' SV.returnTheoremProof thm' +apply_thm :: Theorem -> [Theorem] -> TopLevel Theorem +apply_thm thm thms = + do sc <- getSharedContext + db <- SV.getTheoremDB + pos <- SV.getPosition + what4PushMuxOps <- gets rwWhat4PushMuxOps + (thm', db') <- io (applyTheorem sc what4PushMuxOps db pos "apply_thm" thm thms) + SV.putTheoremDB db' + SV.returnTheoremProof thm' + get_opt :: Int -> TopLevel Text get_opt n = do argv <- asks roArgv diff --git a/saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs b/saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs index d2680ee781..ebc7618cdf 100644 --- a/saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs +++ b/saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs @@ -75,11 +75,11 @@ assumptionsContainContradiction sym methodSpec tactic assumptions = , goalName = show (methodSpec^.MS.csMethod) , goalLoc = show (W4.plSourceLoc ploc) ++ " in " ++ show (W4.plFunction ploc) , goalDesc = "vacuousness check" - , goalSequent = propToSequent goal' + , goalProp = goal' , goalTags = mempty }) res <- runProofScript tactic goal' pgl Nothing - "vacuousness check" False False + "vacuousness check" False case res of ValidProof _ _ -> return True InvalidProof _ _ _ -> return False diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs index 804eb106d0..a3c0b8e898 100644 --- a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs @@ -337,14 +337,13 @@ verifyObligations cc mspec tactic assumes asserts = , goalName = nm , goalLoc = gloc , goalDesc = msg - , goalSequent = propToSequent goal' + , goalProp = goal' , goalTags = MS.conditionTags md } res <- runProofScript tactic goal' proofgoal (Just ploc) (Text.unwords ["JVM verification condition:", Text.pack (show n), Text.pack goalname]) False -- do not record in the theorem database - False -- TODO, useSequentGoals... case res of ValidProof stats thm -> return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm)) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs index 49fdc437bf..1f7d6dce7a 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs @@ -784,7 +784,6 @@ verifyObligations :: LLVMCrucibleContext arch -> TopLevel (SolverStats, [MS.VCStats]) verifyObligations cc mspec tactic assumes asserts = do let sc = sawCoreSharedContext (cc ^. ccSym) - useSequentGoals <- rwSequentGoals <$> getTopLevelRW let assumeTerms = toListOf (folded . Crucible.labeledPred) assumes assume <- io $ scAndList sc assumeTerms let nm = mspec ^. csName @@ -793,10 +792,6 @@ verifyObligations cc mspec tactic assumes asserts = do let msg' = Text.pack msg goal <- io $ scImplies sc assume assert goal' <- io $ boolToProp sc [] goal - sqt <- if useSequentGoals then - io $ booleansToSequent sc assumeTerms [assert] - else - return (propToSequent goal') let ploc = MS.conditionLoc md let gloc = (unwords [show (W4.plSourceLoc ploc) ,"in" @@ -810,14 +805,13 @@ verifyObligations cc mspec tactic assumes asserts = , goalName = Text.unpack nm , goalLoc = gloc , goalDesc = msg - , goalSequent = sqt + , goalProp = goal' , goalTags = MS.conditionTags md } res <- runProofScript tactic goal' proofgoal (Just ploc) (Text.unwords ["LLVM verification condition", Text.pack (show n), goalname]) False -- do not record this theorem in the database - useSequentGoals case res of ValidProof stats thm -> return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm)) diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs index 7c62a84f8e..9a0f5cafe4 100644 --- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs +++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs @@ -1613,14 +1613,13 @@ checkGoals bak opts nm loc sc tactic mdMap invSubst loopFunEquivConds = do , goalName = Text.unpack nm , goalLoc = gloc , goalDesc = msg - , goalSequent = propToSequent g + , goalProp = g , goalTags = MS.conditionTags md } res <- runProofScript tactic g proofgoal (Just ploc) (Text.unwords ["X86 verification condition", Text.pack (show n), Text.pack msg]) False -- do not record this theorem in the database - False -- TODO! useSequentGoals case res of ValidProof stats thm -> return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm)) diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs index c9a1eab087..51eb37767d 100644 --- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs +++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs @@ -1502,14 +1502,13 @@ verifyObligations cc mspec tactic assumes asserts = , goalName = nm , goalLoc = gloc , goalDesc = msg - , goalSequent = propToSequent goal' + , goalProp = goal' , goalTags = MS.conditionTags md } res <- runProofScript tactic goal' proofgoal (Just ploc) (Text.unwords ["MIR verification condition:", Text.pack (show n), Text.pack goalname]) False -- do not record in the theorem database - False -- TODO, useSequentGoals... case res of ValidProof stats thm -> return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm)) diff --git a/saw-central/src/SAWCentral/Proof.hs b/saw-central/src/SAWCentral/Proof.hs index c3a3af1eb2..1f27682843 100644 --- a/saw-central/src/SAWCentral/Proof.hs +++ b/saw-central/src/SAWCentral/Proof.hs @@ -34,30 +34,9 @@ module SAWCentral.Proof , normalizeProp , checkProp , unProp - - , Sequent - , sequentGetFocus - , sequentToProp - , sequentToSATQuery - , sequentSharedSize - , sequentTreeSize - , prettySequent - , ppSequent - , propToSequent - , traverseSequent - , traverseSequentWithFocus - , checkSequent - , sequentConstantSet - , booleansToSequent - , unfocusSequent - , focusOnConcl - , focusOnHyp - , normalizeSequent - , filterHyps - , filterConcls - , localHypSimpset - , SequentState(..) - , sequentState + , propSharedSize + , propTreeSize + , propConstantSet , CofinSet(..) , cofinSetMember @@ -89,28 +68,21 @@ module SAWCentral.Proof , constructTheorem , validateTheorem , specializeTheorem + , applyTheorem , Evidence(..) , checkEvidence - , structuralEvidence , leafEvidence , Tactic(..) , withFirstGoal , tacticIntro , tacticApply - , tacticApplyHyp - , tacticSplit - , tacticCut , tacticTrivial , tacticId , tacticChange , tacticSolve , tacticExact - , tacticIntroHyps - , tacticRevertHyp - , tacticInsert - , tacticSpecializeHyp , Quantification(..) , predicateToProp @@ -135,18 +107,16 @@ module SAWCentral.Proof ) where import Control.Lens ( (^.) ) -import Control.Monad (foldM, forM_, unless) +import Control.Monad (foldM, unless) import qualified Control.Monad.Fail as F import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.Except (ExceptT, MonadError(..), runExceptT) import Control.Monad.State (MonadState(..)) import Control.Monad.Trans.Class (MonadTrans(..)) -import qualified Data.Foldable as Fold import Data.HashSet (HashSet) import qualified Data.HashSet as HashSet import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet -import Data.List (genericDrop, genericLength, genericSplitAt) import Data.Map (Map) import qualified Data.Map as Map import Data.Set (Set) @@ -175,7 +145,7 @@ import SAWCore.SharedTerm import SAWCore.Term.Functor import SAWCore.FiniteValue (FirstOrderValue, prettyFirstOrderValue) import qualified SAWCore.Term.Certified as TC -import SAWCore.Term.Pretty (prettyTermWithEnv, prettyTermContainerWithEnv) +import SAWCore.Term.Pretty (prettyTermWithEnv) import SAWCore.Simulator.Concrete (evalSharedTerm) import SAWCore.Simulator.Value (asFirstOrderTypeValue, Value(..), TValue(..)) @@ -255,22 +225,6 @@ propToTerm _sc (Prop tm) = pure tm propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a)) propToRewriteRule sc (Prop tm) = ruleOfProp sc tm --- | Attempt to split an if/then/else proposition. --- If it succeeds to find a term like "EqTrue (ite Bool b x y)", --- then it returns two pairs consisting of "(EqTrue b, EqTrue x)" --- and "(EqTrue (not b), EqTrue y)" -splitIte :: SharedContext -> Prop -> IO (Maybe ((Prop, Prop), (Prop, Prop))) -splitIte sc (Prop p) = - case (isGlobalDef "Prelude.ite" <@> return <@> return <@> return <@> return) =<< asEqTrue p of - Nothing -> pure Nothing - Just (_ :*: _tp :*: b :*: x :*: y) -> -- tp must be "Bool" - do nb <- scNot sc b - b' <- scEqTrue sc b - nb' <- scEqTrue sc nb - x' <- scEqTrue sc x - y' <- scEqTrue sc y - return (Just ((Prop b', Prop x'), (Prop nb', Prop y'))) - -- | Attempt to split a conjunctive proposition into two propositions. splitConj :: SharedContext -> Prop -> IO (Maybe (Prop, Prop)) splitConj sc (Prop p) = @@ -293,104 +247,6 @@ splitDisj sc (Prop p) = t2 <- scPiList sc vars =<< scEqTrue sc p2 return (Just (Prop t1,Prop t2)) --- | Attempt to split an implication into a hypothesis and a conclusion -splitImpl :: SharedContext -> Prop -> IO (Maybe (Prop, Prop)) -splitImpl sc (Prop p) - | Just ( _ :*: h :*: c) <- (isGlobalDef "Prelude.implies" <@> return <@> return) =<< asEqTrue p - = do h' <- scEqTrue sc h - c' <- scEqTrue sc c - return (Just (Prop h', Prop c')) - - -- or (not h) c == implies h c - | Just ( _ :*: (_ :*: h) :*: c) <- (isGlobalDef "Prelude.or" <@> (isGlobalDef "Prelude.not" <@> return) <@> return) =<< asEqTrue p - = do h' <- scEqTrue sc h - c' <- scEqTrue sc c - return (Just (Prop h', Prop c')) - - -- or c (not h) == implies h c - | Just ( _ :*: c :*: (_ :*: h)) <- (isGlobalDef "Prelude.or" <@> return <@> (isGlobalDef "Prelude.not" <@> return)) =<< asEqTrue p - = do h' <- scEqTrue sc h - c' <- scEqTrue sc c - return (Just (Prop h', Prop c')) - - -- Handle the case of (H1 -> H2), where H1 and H2 are in Prop - | Just (nm, arg, c) <- asPi p - , IntSet.notMember (vnIndex nm) (freeVars c) -- make sure this is a nondependent Pi (AKA arrow type) - = termToMaybeProp sc arg >>= \case - Nothing -> return Nothing - Just h -> return (Just (h, Prop c)) - - | otherwise - = return Nothing - - --- | Attempt to split a sequent into two subgoals. This will only work --- on focused sequents. If the sequent is focused on a hypothesis, --- the hypothesis must be a disjunction, if/then/else, or implication term. --- If the sequent is focused on a conclusion, the conclusion must be --- a conjunction or if/then/else. --- --- If this process succeeds, then a proof of the two included sequents --- should be sufficient to prove the input sequent. -splitSequent :: SharedContext -> Sequent -> IO (Maybe (Sequent, Sequent)) -splitSequent sc sqt = - case sqt of - ConclFocusedSequent hs (FB gs1 g gs2) -> - splitConj sc g >>= \case - -- HS |- GS1, X, GS2 - -- HS |- GS1, Y, GS2 - -- --------------------------- (Conj-R) - -- HS |- GS1, X /\ Y, GS2 - Just (x, y) -> - return (Just ( ConclFocusedSequent hs (FB gs1 x gs2) - , ConclFocusedSequent hs (FB gs1 y gs2) - )) - Nothing -> - splitIte sc g >>= \case - -- HS, B |- GS1, X, GS2 - -- HS, not B |- GS1, Y, GS2 - -- -------------------------------------- (Ite-R) - -- HS |- GS1, if B then X else Y, GS2 - Just ((b, x), (nb, y)) -> - return (Just ( ConclFocusedSequent (hs ++ [b]) (FB gs1 x gs2) - , ConclFocusedSequent (hs ++ [nb]) (FB gs1 y gs2) - )) - Nothing -> return Nothing - - HypFocusedSequent (FB hs1 h hs2) gs -> - splitDisj sc h >>= \case - -- HS1, X, HS2 |- GS - -- HS1, Y, HS2 |- GS - -- --------------------------- (Disj-L) - -- HS1, X \/ Y, HS2 |- GS - Just (x, y) -> - return (Just ( HypFocusedSequent (FB hs1 x hs2) gs - , HypFocusedSequent (FB hs1 y hs2) gs - )) - Nothing -> - -- HS1, X, HS2, B |- GS - -- HS1, Y, HS2, not B |- GS - -- ------------------------------------- (Ite-L) - -- HS1, if B then X else Y, HS2 |- GS - splitIte sc h >>= \case - Just ((b,x), (nb, y)) -> - return (Just ( HypFocusedSequent (FB hs1 x (hs2 ++ [b])) gs - , HypFocusedSequent (FB hs1 y (hs2 ++ [nb])) gs - )) - Nothing -> - -- HS1, Y, HS2 |- GS - -- HS1, X -> Y, HS2 |- GS, X - -- ------------------------------ (Impl-L) AKA modus ponens - -- HS1, X -> Y, HS2 |- GS - splitImpl sc h >>= \case - Just (x, y) -> - return (Just ( HypFocusedSequent (FB hs1 y hs2) gs - , ConclFocusedSequent (hs1 ++ [h] ++ hs2) (FB gs x []) - )) - Nothing -> return Nothing - - UnfocusedSequent _ _ -> return Nothing - -- | Unfold all the constants appearing in the proposition -- whose VarIndex is found in the given set. unfoldProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop @@ -412,46 +268,6 @@ simplifyProp sc ss (Prop tm) = do (a, tm') <- rewriteSharedTerm sc ss tm return (a, Prop tm') --- | Rewrite the propositions using the provided Simpset -simplifyProps :: Monoid a => SharedContext -> Simpset a -> [Prop] -> IO (a, [Prop]) -simplifyProps _sc _ss [] = return (mempty, []) -simplifyProps sc ss (p:ps) = - do (a, p') <- simplifyProp sc ss p - (b, ps') <- simplifyProps sc ss ps - return (a <> b, p' : ps') - --- | Add hypotheses from the given sequent as rewrite rules --- to the given simpset. -localHypSimpset :: SharedContext -> Sequent -> [Integer] -> Simpset a -> IO (Simpset a) -localHypSimpset sc sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps - - where - processHyp ss (n,h) = - ruleOfProp sc (unProp h) Nothing >>= \case - Nothing -> fail $ "Hypothesis " ++ show n ++ "cannot be used as a rewrite rule." - Just r -> return (addRule r ss) - - nhyps = [ (n,h) - | (n,h) <- zip [0..] hyps - , Set.member n hset - ] - RawSequent hyps _ = sequentToRawSequent sqt - hset = Set.fromList hs - --- | Rewrite in the sequent using the provided Simpset -simplifySequent :: Monoid a => SharedContext -> Simpset a -> Sequent -> IO (a, Sequent) -simplifySequent sc ss (UnfocusedSequent hs gs) = - do (a, hs') <- simplifyProps sc ss hs - (b, gs') <- simplifyProps sc ss gs - return (a <> b, UnfocusedSequent hs' gs') -simplifySequent sc ss (ConclFocusedSequent hs (FB gs1 g gs2)) = - do (a, g') <- simplifyProp sc ss g - return (a, ConclFocusedSequent hs (FB gs1 g' gs2)) -simplifySequent sc ss (HypFocusedSequent (FB hs1 h hs2) gs) = - do (a, h') <- simplifyProp sc ss h - return (a, HypFocusedSequent (FB hs1 h' hs2) gs) - - hoistIfsInProp :: SharedContext -> Prop -> IO Prop hoistIfsInProp sc (Prop p) = do let (vars, body) = asPiList p @@ -548,205 +364,11 @@ prettyTheorem opts nenv thm , "|-" <+> prettyProp opts nenv (thmProp thm) ] --- TODO, I'd like to add metadata here -type SequentBranch = Prop +propConstantSet :: Prop -> Map VarIndex NameInfo +propConstantSet p = getConstantSet (unProp p) --- | The representation of either hypotheses or conclusions with a focus --- point. A @FB xs y zs@ represents a collection of propositions --- where @xs@ come before the focus point @y@, and @zs@ is the --- collection of propositions following the focus point. -data FocusedBranch = FB ![SequentBranch] !SequentBranch ![SequentBranch] - --- | This datatype represents sequents in the style of Gentzen. Sequents --- are used to represent the intermediate states of a proof, and are the --- primary objects manipulated by the proof tactic system. --- --- A sequent essentially represents a logical claim which is in the process --- of being proved. A sequent has some (possibly 0) number of --- "hypotheses" and some number (possibly 0) of "conclusions". In mathematical --- notation, the hypotheses are separated from the conclusions by a turnstile --- character, and the individual hypotheses and conclusions are separated from --- each other by a comma. So, a typical sequent may look like: --- --- H1, H2, H3, |- C1, C2 --- --- The logical meaning of a sequent is that the conjunction of all the hypotheses --- implies the disjunction of the conclusions. The multi-conclusion form --- of sequent (as is presented here) is typical of a classical logic. --- --- In a Gentzen-style proof system (such as the sequent calculus), the method by --- which proof proceeds is to apply inference rules. Each rule applies to a goal --- sequent (the thing to be proved) and has 0 or more subgoals that must be proved --- to apply the rule. Part of a proof is completed when a rule is applied which has 0 --- subgoals. When doing proofs in SAW using the tactic system, there is a stack of --- currently outstanding proof goals (each in the form of a sequent to be proved). --- Executing a tactic will modify or apply a proof rule to the top goal on the stack; --- if that subgoal is finished, then the next subgoal becomes active. --- If applying a rule causes more than one subgoal to be generated, the remaining --- ones are pushed onto the stack of goals to be proved. An entire proof is completed --- when the stack of outstanding goals to prove is empty. --- --- This particular presentation of sequents is a "focused" sequent calculus. --- This means that a sequent may optionally have a focus on a particular --- hypothesis or conclusion. Some manipulations of sequents require a focus --- point to indicate where some manipulation should be carried out, and others --- will apply in both focused or unfocused states. -data Sequent - = -- | A sequent in the unfocused state - UnfocusedSequent ![SequentBranch] ![SequentBranch] - -- | A sequent focused on a particular conclusion - | ConclFocusedSequent ![SequentBranch] !FocusedBranch - -- | A sequent focused on a particular hypothesis - | HypFocusedSequent !FocusedBranch ![SequentBranch] - --- | A RawSequent is a data-structure representing a sequent, but without --- the ability to focus on a particular hypothesis or conclusion. --- --- This data-structure is parametric in the type of propositions, --- which enables some convenient patterns using traversals, etc. -data RawSequent a = RawSequent [a] [a] - -instance Functor RawSequent where - fmap f (RawSequent hs gs) = RawSequent (fmap f hs) (fmap f gs) -instance Foldable RawSequent where - foldMap f (RawSequent hs gs) = Fold.foldMap f (hs ++ gs) -instance Traversable RawSequent where - traverse f (RawSequent hs gs) = RawSequent <$> traverse f hs <*> traverse f gs - -sequentToRawSequent :: Sequent -> RawSequent Prop -sequentToRawSequent sqt = - case sqt of - UnfocusedSequent hs gs -> RawSequent hs gs - ConclFocusedSequent hs (FB gs1 g gs2) -> RawSequent hs (gs1 ++ g : gs2) - HypFocusedSequent (FB hs1 h hs2) gs -> RawSequent (hs1 ++ h : hs2) gs - -unfocusSequent :: Sequent -> Sequent -unfocusSequent sqt = UnfocusedSequent hs gs - where RawSequent hs gs = sequentToRawSequent sqt - -focusOnConcl :: Integer -> Sequent -> Maybe Sequent -focusOnConcl i sqt = - let RawSequent hs gs = sequentToRawSequent sqt in - case genericSplitAt i gs of - (gs1, g:gs2) -> Just (ConclFocusedSequent hs (FB gs1 g gs2)) - (_ , []) -> Nothing - -focusOnHyp :: Integer -> Sequent -> Maybe Sequent -focusOnHyp i sqt = - let RawSequent hs gs = sequentToRawSequent sqt in - case genericSplitAt i hs of - (hs1,h:hs2) -> Just (HypFocusedSequent (FB hs1 h hs2) gs) - (_ , []) -> Nothing - -sequentConstantSet :: Sequent -> Map VarIndex NameInfo -sequentConstantSet sqt = foldr (\p m -> Map.union (getConstantSet (unProp p)) m) mempty (hs++gs) - where - RawSequent hs gs = sequentToRawSequent sqt - -convertibleProps :: SharedContext -> [Prop] -> [Prop] -> IO Bool -convertibleProps _sc [] [] = return True -convertibleProps sc (p1:ps1) (p2:ps2) = - do ok1 <- scConvertible sc (unProp p1) (unProp p2) - ok2 <- convertibleProps sc ps1 ps2 - return (ok1 && ok2) -convertibleProps _sc _ _ = return False - -convertibleSequents :: SharedContext -> Sequent -> Sequent -> IO Bool -convertibleSequents sc sqt1 sqt2 = - do ok1 <- convertibleProps sc hs1 hs2 - ok2 <- convertibleProps sc gs1 gs2 - return (ok1 && ok2) - where - RawSequent hs1 gs1 = sequentToRawSequent sqt1 - RawSequent hs2 gs2 = sequentToRawSequent sqt2 - - --- | A helper data structure for working with sequents when a focus --- point is expected. When a conclusion or hypothesis is focused, --- return the focused proposition; and return a function which --- allows building a new sequent by replacing the proposition under --- focus. -data SequentState - = Unfocused - | ConclFocus Prop (Prop -> Sequent) - | HypFocus Prop (Prop -> Sequent) - --- | Build a sequent with the given proposition as the --- only conclusion, and place it under focus. -propToSequent :: Prop -> Sequent -propToSequent p = ConclFocusedSequent [] (FB [] p []) - --- | Give in a collection of boolean terms, construct a sequent --- with corresponding hypotheses and conclusions. If there --- is exactly one conclusion term, put it under focus. -booleansToSequent :: SharedContext -> [Term] -> [Term] -> IO Sequent -booleansToSequent sc hs gs = - do hs' <- mapM (boolToProp sc []) hs - gs' <- mapM (boolToProp sc []) gs - case gs' of - [g] -> return (ConclFocusedSequent hs' (FB [] g [])) - _ -> return (UnfocusedSequent hs' gs') - --- | Given a sequent, render its semantics as a proposition. --- --- Currently this can only handle sequents with 0 or 1 conclusion --- (this is not a fundamental limitation, but we need a Prop-level disjunction --- in SAWCore to fix this). --- --- Given a sequent like @H1, H2 ..., Hn |- C@, this will build a corresponding --- proposition @H1 -> H2 -> ... Hn -> C@. If the list of conclusions is empty, --- the proposition will be @H1 -> H2 -> ... Hn -> False@. -sequentToProp :: SharedContext -> Sequent -> IO Prop -sequentToProp sc sqt = - do let RawSequent hs gs = sequentToRawSequent sqt - case gs of - [] -> do g <- boolToProp sc [] =<< scBool sc False - loop hs g - [g] -> loop hs g - -- TODO, we should add a prop-level disjunction to the SAWCore prelude - _ -> fail "seqentToProp: cannot handle multi-conclusion sequents" - - where - loop [] g = return g - loop (h:hs) g = - do g' <- loop hs g - Prop <$> scFun sc (unProp h) (unProp g') - --- | Pretty print the given proposition as a string. -ppSequent :: PPS.Opts -> DisplayNameEnv -> Sequent -> String -ppSequent opts nenv sqt = PPS.render opts (prettySequent opts nenv sqt) - --- | Pretty print the given proposition as a @PPS.Doc@. -prettySequent :: PPS.Opts -> DisplayNameEnv -> Sequent -> PPS.Doc -prettySequent opts nenv sqt = - prettyTermContainerWithEnv - (prettyRawSequent sqt) - opts - nenv - (fmap unProp (sequentToRawSequent sqt)) - -prettyRawSequent :: Sequent -> RawSequent PPS.Doc -> PPS.Doc -prettyRawSequent _sqt (RawSequent [] [g]) = g -prettyRawSequent sqt (RawSequent hs gs) = - align (vcat (map ppHyp (zip [0..] hs) ++ turnstile ++ map ppConcl (zip [0..] gs))) - where - turnstile = [ pretty (take 40 (repeat '=')) ] - focused doc = "<<" <> doc <> ">>" - ppHyp (i, tm) - | HypFocusedSequent (FB hs1 _h _hs2) _gs <- sqt - , length hs1 == i - = focused ("H" <> pretty i) <+> tm - - | otherwise - = "H" <> pretty i <> ":" <+> tm - - ppConcl (i, tm) - | ConclFocusedSequent _hs (FB gs1 _g _gs2) <- sqt - , length gs1 == i - = focused ("C" <> pretty i) <+> tm - - | otherwise - = "C" <> pretty i <> ":" <+> tm +convertibleProps :: SharedContext -> Prop -> Prop -> IO Bool +convertibleProps sc g1 g2 = scConvertible sc (unProp g1) (unProp g2) -- | A datatype for representing finte or cofinite sets. @@ -761,141 +383,11 @@ cofinSetMember :: Ord a => a -> CofinSet a -> Bool cofinSetMember a (WhiteList xs) = Set.member a xs cofinSetMember a (BlackList xs) = not (Set.member a xs) --- | Given a set of positions, filter the given list --- so that it retains just those values that are in --- positions contained in the set. The given integer --- indicates what position to start counting at. -filterPosList :: CofinSet Integer -> Integer -> [a] -> [a] -filterPosList pss start xs = map snd $ filter f $ zip [start..] xs - where - f (i,_) = cofinSetMember i pss - --- | Given a set of positions, filter the given focused branch --- and retain just those positions in the set. --- If the given branch was focused and the focus point was retained, --- return a @Right@ value with the new focused branch. If the --- given branch was unfocused to start, or of the focused point --- was removed, return a @Left@ value with a bare list. -filterFocusedList :: CofinSet Integer -> FocusedBranch -> Either [SequentBranch] FocusedBranch -filterFocusedList pss (FB xs1 x xs2) = - if cofinSetMember idx pss then - Right (FB xs1' x xs2') - else - Left (xs1' ++ xs2') - where - idx = genericLength xs1 - xs1' = filterPosList pss 0 xs1 - xs2' = filterPosList pss (idx+1) xs2 - --- | Filter the list of hypotheses in a sequent, retaining --- only those in the given set. -filterHyps :: CofinSet Integer -> Sequent -> Sequent -filterHyps pss (UnfocusedSequent hs gs) = - UnfocusedSequent (filterPosList pss 0 hs) gs -filterHyps pss (ConclFocusedSequent hs gs) = - ConclFocusedSequent (filterPosList pss 0 hs) gs -filterHyps pss (HypFocusedSequent hs gs) = - case filterFocusedList pss hs of - Left hs' -> UnfocusedSequent hs' gs - Right hs' -> HypFocusedSequent hs' gs - --- | Filter the list of conclusions in a sequent, retaining --- only those in the given set. -filterConcls :: CofinSet Integer -> Sequent -> Sequent -filterConcls pss (UnfocusedSequent hs gs) = - UnfocusedSequent hs (filterPosList pss 0 gs) -filterConcls pss (HypFocusedSequent hs gs) = - HypFocusedSequent hs (filterPosList pss 0 gs) -filterConcls pss (ConclFocusedSequent hs gs) = - case filterFocusedList pss gs of - Left gs' -> UnfocusedSequent hs gs' - Right gs' -> ConclFocusedSequent hs gs' - --- | Add a new hypothesis to the list of hypotheses in a sequent -addHypothesis :: Prop -> Sequent -> Sequent -addHypothesis p (UnfocusedSequent hs gs) = UnfocusedSequent (hs ++ [p]) gs -addHypothesis p (ConclFocusedSequent hs gs) = ConclFocusedSequent (hs ++ [p]) gs -addHypothesis p (HypFocusedSequent (FB hs1 h hs2) gs) = HypFocusedSequent (FB hs1 h (hs2++[p])) gs - --- | Add a new conclusion to the end of the conclusion list and focus on it -addNewFocusedConcl :: Prop -> Sequent -> Sequent -addNewFocusedConcl p sqt = - let RawSequent hs gs = sequentToRawSequent sqt - in ConclFocusedSequent hs (FB gs p []) - --- | If the sequent is focused, return the prop under focus, --- together with its index value. --- A @Left@ value indicates a hypothesis under focus, and --- a @Right@ value is a conclusion under focus. -sequentGetFocus :: Sequent -> Maybe (Either (Integer,Prop) (Integer, Prop)) -sequentGetFocus (UnfocusedSequent _ _) = - Nothing -sequentGetFocus (HypFocusedSequent (FB hs1 h _) _) = - Just (Left (genericLength hs1, h)) -sequentGetFocus (ConclFocusedSequent _ (FB gs1 g _)) = - Just (Right (genericLength gs1, g)) - -sequentState :: Sequent -> SequentState -sequentState (UnfocusedSequent _ _) = Unfocused -sequentState (ConclFocusedSequent hs (FB gs1 g gs2)) = - ConclFocus g (\g' -> ConclFocusedSequent hs (FB gs1 g' gs2)) -sequentState (HypFocusedSequent (FB hs1 h hs2) gs) = - HypFocus h (\h' -> HypFocusedSequent (FB hs1 h' hs2) gs) - -sequentSharedSize :: Sequent -> Integer -sequentSharedSize sqt = scSharedSizeMany (map unProp (hs ++ gs)) - where - RawSequent hs gs = sequentToRawSequent sqt +propSharedSize :: Prop -> Integer +propSharedSize p = scSharedSizeMany [unProp p] -sequentTreeSize :: Sequent -> Integer -sequentTreeSize sqt = scTreeSizeMany (map unProp (hs ++ gs)) - where - RawSequent hs gs = sequentToRawSequent sqt - --- | Given an operation on propositions, apply the operation to the sequent. --- If the sequent is focused, apply the operation just to the focused --- hypothesis or conclusion. If the sequent is unfocused, apply the operation --- to all the hypotheses and conclusions in the sequent. -traverseSequentWithFocus :: Applicative m => (Prop -> m Prop) -> Sequent -> m Sequent -traverseSequentWithFocus f (UnfocusedSequent hs gs) = - UnfocusedSequent <$> traverse f hs <*> traverse f gs -traverseSequentWithFocus f (ConclFocusedSequent hs (FB gs1 g gs2)) = - (\g' -> ConclFocusedSequent hs (FB gs1 g' gs2)) <$> f g -traverseSequentWithFocus f (HypFocusedSequent (FB hs1 h hs2) gs) = - (\h' -> HypFocusedSequent (FB hs1 h' hs2) gs) <$> f h - --- | Given an operation on propositions, apply the operation to all the --- hypotheses and conclusions in the sequent. -traverseSequent :: Applicative m => (Prop -> m Prop) -> Sequent -> m Sequent -traverseSequent f (UnfocusedSequent hs gs) = - UnfocusedSequent <$> traverse f hs <*> traverse f gs -traverseSequent f (ConclFocusedSequent hs (FB gs1 g gs2)) = - ConclFocusedSequent <$> - (traverse f hs) <*> - ( FB <$> traverse f gs1 <*> f g <*> traverse f gs2) -traverseSequent f (HypFocusedSequent (FB hs1 h hs2) gs) = - HypFocusedSequent <$> - ( FB <$> traverse f hs1 <*> f h <*> traverse f hs2) <*> - (traverse f gs) - --- | Typecheck a sequent. This will typecheck all the terms --- appearing in the sequent to ensure that they are propositions. --- This check should always succeed, unless some programming --- mistake has allowed us to build an ill-typed sequent. -checkSequent :: SharedContext -> Sequent -> IO () -checkSequent sc (UnfocusedSequent hs gs) = - do forM_ hs (checkProp sc) - forM_ gs (checkProp sc) -checkSequent sc (ConclFocusedSequent hs (FB gs1 g gs2)) = - do forM_ hs (checkProp sc) - forM_ gs1 (checkProp sc) - checkProp sc g - forM_ gs2 (checkProp sc) -checkSequent sc (HypFocusedSequent (FB hs1 h hs2) gs) = - do forM_ hs1 (checkProp sc) - checkProp sc h - forM_ hs2 (checkProp sc) - forM_ gs (checkProp sc) +propTreeSize :: Prop -> Integer +propTreeSize p = scTreeSizeMany [unProp p] -- | Check that a @Prop@ value is actually a proposition. -- This check should always succeed, unless some programming @@ -920,13 +412,6 @@ termHypotheses t = HashSet.fromList (IntMap.elems (varTypes t)) propHypotheses :: Prop -> Hypotheses propHypotheses p = termHypotheses (unProp p) -rawSequentHypotheses :: RawSequent Prop -> Hypotheses -rawSequentHypotheses (RawSequent hs gs) = - Fold.foldMap propHypotheses (hs ++ gs) - -sequentHypotheses :: Sequent -> Hypotheses -sequentHypotheses sqt = rawSequentHypotheses (sequentToRawSequent sqt) - type TheoremNonce = Nonce GlobalNonceGenerator Theorem -- | A theorem is a proposition which has been wrapped in a @@ -1045,112 +530,77 @@ data Evidence -- statement matches the type of the given term. ProofTerm !Term - -- | This type of evidence is produced when the given sequent + -- | This type of evidence is produced when the given goal -- has been dispatched to a solver which has indicated that it - -- was able to prove the sequent. The included @SolverStats@ + -- was able to prove the goal. The included @SolverStats@ -- give some details about the solver run. - | SolverEvidence !SolverStats !Sequent + | SolverEvidence !SolverStats !Prop - -- | This type of evidence is produced when the given sequent + -- | This type of evidence is produced when the given goal -- has been randomly tested against input vectors in the style -- of quickcheck. The included number is the number of successfully -- passed test vectors. - | QuickcheckEvidence !Integer !Sequent + | QuickcheckEvidence !Integer !Prop - -- | This type of evidence is produced when the given sequent + -- | This type of evidence is produced when the given goal -- has been explicitly assumed without other evidence, at the -- user's direction. - | Admitted !Text !Pos !Sequent - - -- | This type of evidence is produced when the focused hypothesis - -- or conclusion proposition can be deconstructed (along a - -- conjunction, disjunction, if/then/else or implication) into - -- two subgoals, each of which is supported by the included - -- evidence. - | SplitEvidence !Evidence !Evidence + | Admitted !Text !Pos !Prop -- | This type of evidence is produced when a previously-proved - -- theorem is applied via backward reasoning to prove a focused - -- conclusion. Pi-quantified variables of the theorem may be - -- specialized either by giving an explicit @Term@ to - -- instantiate the variable, or by giving @Evidence@ for @Prop@ - -- hypotheses. After specializing the given @Theorem@ the - -- result must match the current focued conclusion. + -- theorem is applied via backward reasoning to prove a goal. + -- Pi-quantified variables of the theorem may be specialized + -- either by giving an explicit @Term@ to instantiate the + -- variable, or by giving @Evidence@ for @Prop@ hypotheses. + -- After specializing the given @Theorem@ the result must match + -- the current goal. | ApplyEvidence !Theorem ![Either Term Evidence] - -- | This type of evidence is produced when a local hypothesis is - -- applied via backward reasoning to prove a focused conclusion. - -- Pi-quantified variables of the hypothesis may be specialized - -- either by giving an explicit @Term@ to instantiate the - -- variable, or by giving @Evidence@ for @Prop@ hypotheses. - -- After specializing the given @Theorem@ the result must match - -- the current focused conclusion. - | ApplyHypEvidence Integer ![Either Term Evidence] - - -- | This type of evidence is used to prove a universally-quantified conclusion. - -- The included 'VarName' should be a fresh variable used to instantiate the - -- quantified proposition. + -- | This type of evidence is used to prove a universally- + -- quantified goal. + -- The included 'VarName' should be a fresh variable used to + -- instantiate the quantified goal. | IntroEvidence !VarName !Term !Evidence - -- | This type of evidence is used to apply the "cut rule" of sequent calculus. - -- The given proposition is added to the hypothesis list in the first - -- derivation, and into the conclusion list in the second, where it is focused. - | CutEvidence !Prop !Evidence !Evidence - - -- | This type of evidence is used to modify a sequent to prove via - -- rewriting. The sequent is rewritten by the given - -- simpset; then the provided evidence is used to check the - -- modified sequent. The list of integers indicate local - -- hypotheses that should also be treated as rewrite rules. - | RewriteEvidence ![Integer] !(Simpset TheoremAnnotation) !Evidence - - -- | This type of evidence is used to modify a sequent via unfolding - -- constant definitions. The sequent is modified by unfolding - -- constants identified via the given set of @VarIndex@; then the provided - -- evidence is used to check the modified sequent. + -- | This type of evidence is used to modify a goal to prove via + -- rewriting. + -- The property is rewritten by the given simpset; then the + -- provided evidence is used to check the modified goal. + | RewriteEvidence !(Simpset TheoremAnnotation) !Evidence + + -- | This type of evidence is used to modify a goal via unfolding + -- constant definitions. + -- The goal is modified by unfolding constants identified via the + -- given set of @VarIndex@; then the provided evidence is used to + -- check the modified goal. | UnfoldEvidence !(Set VarIndex) !Evidence - -- | This type of evidence is used to modify a sequent via unfolding fixpoint - -- constant definitions once. The sequent is modified by unfolding - -- constants identified via the given set of @VarIndex@; then the provided - -- evidence is used to check the modified sequent. + -- | This type of evidence is used to modify a goal via unfolding + -- fixpoint constant definitions once. + -- The goal is modified by unfolding constants identified via the + -- given set of @VarIndex@; then the provided evidence is used to + -- check the modified goal. | UnfoldFixOnceEvidence !(Set VarIndex) !Evidence - -- | This type of evidence is used to modify a sequent via evaluation - -- into the the What4 formula representation. During evaluation, the - -- constants identified by the given set of @VarIndex@ are held - -- uninterpreted (i.e., will not be unfolded). Then, the provided - -- evidence is use to check the modified sequent. + -- | This type of evidence is used to modify a goal via evaluation + -- into the the What4 formula representation. + -- During evaluation, the constants identified by the given set of + -- @VarIndex@ are held uninterpreted (i.e., will not be unfolded). + -- Then, the provided evidence is use to check the modified goal. | EvalEvidence !(Set VarIndex) !Evidence - -- | This type of evidence is used to modify a focused part of the sequent. - -- The modified sequent should be equivalent up to conversion. - | ConversionEvidence !Sequent !Evidence + -- | This type of evidence is used to modify a goal. + -- The modified goal should be equivalent up to conversion. + | ConversionEvidence !Prop !Evidence -- | This type of evidence is used to modify a goal to prove by applying - -- 'hoistIfsInProp'. + -- 'hoistIfsInProp'. | HoistIfsEvidence !Evidence - -- | Change the state of the sequent in some "structural" way. This - -- can involve changing focus, reordering or applying weakening rules. - | StructuralEvidence !Sequent !Evidence - - -- | Change the state of the sequent in some way that is governed by - -- the "reversible" L/R rules of the sequent calculus, e.g., - -- conjunctions in hypotheses can be split into multiple hypotheses, - -- negated conclusions become positive hypotheses, etc. - | NormalizeSequentEvidence !Sequent !Evidence - - -- | Change the state of the sequent by invoking the term evaluator - -- on the focused sequent branch (or all branches, if unfocused). - -- Treat the given variable indexes as opaque. + -- | Modify the goal by invoking the term evaluator on it. + -- Treat the given variable indexes as opaque. | NormalizePropEvidence !(Set VarIndex) !Evidence - -- | This type of evidence is used when the current sequent, after - -- applying structural rules, is an instance of the basic - -- sequent calculus axiom, which connects a hypothesis to a conclusion. - | AxiomEvidence - -- | The the proposition proved by a given theorem. thmProp :: Theorem -> Prop thmProp Theorem{ _thmProp = p } = p @@ -1195,32 +645,10 @@ thmElapsedTime Theorem{ _thmElapsedTime = tm } = tm thmSummary :: Theorem -> TheoremSummary thmSummary Theorem { _thmSummary = sy } = sy -splitEvidence :: [Evidence] -> IO Evidence -splitEvidence [e1,e2] = pure (SplitEvidence e1 e2) -splitEvidence _ = fail "splitEvidence: expected two evidence values" - introEvidence :: VarName -> Term -> [Evidence] -> IO Evidence introEvidence x t [e] = pure (IntroEvidence x t e) introEvidence _ _ _ = fail "introEvidence: expected one evidence value" -cutEvidence :: Prop -> [Evidence] -> IO Evidence -cutEvidence p [e1,e2] = pure (CutEvidence p e1 e2) -cutEvidence _ _ = fail "cutEvidence: expected two evidence values" - -insertEvidence :: Theorem -> Prop -> [Term] -> [Evidence] -> IO Evidence -insertEvidence thm h ts [e] = pure (CutEvidence h e (ApplyEvidence thm (map Left ts))) -insertEvidence _ _ _ _ = fail "insertEvidence: expected one evidence value" - -specializeHypEvidence :: Integer -> Prop -> [Term] -> [Evidence] -> IO Evidence -specializeHypEvidence n h ts [e] = pure (CutEvidence h e (ApplyHypEvidence n (map Left ts))) -specializeHypEvidence _ _ _ _ = fail "specializeHypEvidence: expected one evidence value" - -structuralEvidence :: Sequent -> Evidence -> Evidence --- If we apply some structural evidence to an already existing structural evidence, we can --- just omit the new one because the checking procedure doesn't need the intermediate state. -structuralEvidence _sqt (StructuralEvidence sqt' e) = StructuralEvidence sqt' e -structuralEvidence sqt e = StructuralEvidence sqt e - -- | Construct a theorem directly via a proof term. proofByTerm :: SharedContext -> TheoremDB -> Term -> Pos -> Text -> IO (Theorem, TheoremDB) proofByTerm sc db prf loc rsn = @@ -1310,6 +738,47 @@ specializeProp sc (Prop p0) ts0 = do p' <- TC.scmApply p t loop p' ts +-- | Given a theorem with quantified variables, build a new theorem that +-- specializes the leading quantifiers with the given terms or theorems. +-- This will fail if the given terms to not match the quantifier structure +-- of the given theorem. +applyTheorem :: + SharedContext -> Bool -> TheoremDB -> Pos -> Text -> + Theorem -> [Theorem] -> IO (Theorem, TheoremDB) +applyTheorem _sc _what4PushMuxOps db _loc _rsn thm [] = pure (thm, db) +applyTheorem sc what4PushMuxOps db loc rsn thm thms = + do p' <- loop (thmProp thm) (map thmProp thms) + let ev = ApplyEvidence thm (map (Right . thmEvidence) thms) + constructTheorem sc what4PushMuxOps db p' ev loc Nothing rsn 0 + where + loop :: Prop -> [Prop] -> IO Prop + loop p [] = pure p + loop (Prop p) (Prop t : ps) = + do p' <- scWhnf sc p + case asPi p' of + Just (x, a, b) + | IntMap.notMember (vnIndex x) (varTypes b) -> + do ok <- scConvertible sc t a + unless ok $ + do ppopts <- scGetPPOpts sc + ppt <- prettyTerm sc t + ppa <- prettyTerm sc a + fail $ PPS.render ppopts $ PP.vsep + [ "apply_thm: failed to apply" + , "Expected:" + , PP.indent 2 ppa + , "Found:" + , PP.indent 2 ppt + ] + loop (Prop b) ps + _ -> + do ppopts <- scGetPPOpts sc + pp <- prettyTerm sc p + fail $ PPS.render ppopts $ PP.vsep + [ "apply_thm: not an implication" + , PP.indent 2 pp + ] + -- | Admit the given theorem without evidence. -- The provided message allows the user to -- explain why this proposition is being admitted. @@ -1327,7 +796,7 @@ admitTheorem db msg p loc rsn = { _thmProp = p , _thmHyps = propHypotheses p , _thmStats = solverStats "ADMITTED" (propSize p) - , _thmEvidence = Admitted msg loc (propToSequent p) + , _thmEvidence = Admitted msg loc p , _thmLocation = loc , _thmProgramLoc = Nothing , _thmReason = rsn @@ -1355,7 +824,7 @@ solverTheorem db p stats loc rsn elapsed = { _thmProp = p , _thmHyps = propHypotheses p , _thmStats = stats - , _thmEvidence = SolverEvidence stats (propToSequent p) + , _thmEvidence = SolverEvidence stats p , _thmLocation = loc , _thmReason = rsn , _thmProgramLoc = Nothing @@ -1377,7 +846,7 @@ data ProofGoal = , goalLoc :: String , goalDesc :: String , goalTags :: Set String - , goalSequent :: !Sequent + , goalProp :: !Prop } @@ -1425,7 +894,7 @@ predicateToProp sc quant = loop data ProofState = ProofState { _psGoals :: ![ProofGoal] - , _psConcl :: (Sequent,Pos,Maybe ProgramLoc,Text) + , _psConcl :: (Prop, Pos, Maybe ProgramLoc, Text) , _psStats :: SolverStats , _psTimeout :: Maybe Integer , _psEvidence :: [Evidence] -> IO Evidence @@ -1457,156 +926,12 @@ propsElem :: SharedContext -> Prop -> [Prop] -> IO Bool propsElem sc x ps = or <$> sequence [ scConvertible sc (unProp x) (unProp y) | y <- ps ] --- | Test if a sequent is an instance of the sequent calculus axiom. --- This occurs precisely when some hypothesis is convertible --- to some conclusion. -sequentIsAxiom :: SharedContext -> Sequent -> IO Bool -sequentIsAxiom sc sqt = - do let RawSequent hs gs = sequentToRawSequent sqt - or <$> sequence [ scConvertible sc (unProp x) (unProp y) | x <- hs, y <- gs ] - --- | Test if the first given sequent subsumes the --- second given sequent. This is a shallow syntactic --- check that is sufficient to show that a proof --- of the first sequent is sufficient to prove the second -sequentSubsumes :: SharedContext -> Sequent -> Sequent -> IO Bool -sequentSubsumes sc sqt1 sqt2 = - do let s1 = sequentToRawSequent sqt1 - let s2 = sequentToRawSequent sqt2 - rawSequentSubsumes sc s1 s2 - --- | Test if the first given sequent subsumes the --- second given sequent. This is a shallow syntactic --- check that is sufficient to show that a proof --- of the first sequent is sufficient to prove the second -normalizeSequentSubsumes :: SharedContext -> Sequent -> Sequent -> IO Bool -normalizeSequentSubsumes sc sqt1 sqt2 = - do s1 <- normalizeRawSequent sc (sequentToRawSequent sqt1) - s2 <- normalizeRawSequent sc (sequentToRawSequent sqt2) - rawSequentSubsumes sc s1 s2 - --- | Tests that the first raw sequent subsumes the second. +-- | Tests that the first prop subsumes the second. -- This is a shallow syntactic check that is sufficient to show that a proof --- of the first sequent is sufficient to prove the second -rawSequentSubsumes :: SharedContext -> RawSequent Prop -> RawSequent Prop -> IO Bool -rawSequentSubsumes sc (RawSequent hs1 gs1) (RawSequent hs2 gs2) = - do hypsOK <- propsSubset sc hs1 hs2 -- assumes no *more* - conclOK <- propsSubset sc gs2 gs1 -- proves no *less* - return (hypsOK && conclOK) - --- | Computes a "normalized" sequent. This applies the reversible --- L/R sequent calculus rules listed below. The resulting sequent --- is always unfocused. --- --- HS1, X, Y, HS2 |- GS --- ---------------------- (Conj-L) --- HS1, X /\ Y, HS2 |- GS --- --- HS |- GS1, X, Y, GS2 --- ---------------------- (Disj-R) --- HS |- GS1, X \/ Y, GS2 --- --- HS, X |- GS1, GS2 --- -------------------------- (Neg-R) --- HS |- GS1, not X, GS2 --- --- HS1, HS2 |- GS, X --- -------------------------- (Neg-L) --- HS1, not X, HS2 |- GS --- --- HS, X |- GS1, Y, GS2 --- -------------------------- (Impl-R) --- HS |- GS1, X -> Y, GS2 -normalizeSequent :: SharedContext -> Sequent -> IO Sequent -normalizeSequent sc sqt = - -- TODO, if/when we add metadata to sequent branches, this will need to change - do RawSequent hs gs <- normalizeRawSequent sc (sequentToRawSequent sqt) - return (UnfocusedSequent hs gs) - -normalizeRawSequent :: SharedContext -> RawSequent Prop -> IO (RawSequent Prop) -normalizeRawSequent sc (RawSequent hs gs) = - do hs' <- mapM (normalizeHyp sc) hs - gs' <- mapM (normalizeConcl sc) gs - return (joinSequents (hs' ++ gs')) - -joinSequent :: RawSequent Prop -> RawSequent Prop -> RawSequent Prop -joinSequent (RawSequent hs1 gs1) (RawSequent hs2 gs2) = RawSequent (hs1 ++ hs2) (gs1 ++ gs2) - -joinSequents :: [RawSequent Prop] -> RawSequent Prop -joinSequents = foldl joinSequent (RawSequent [] []) - - -normalizeHyp :: SharedContext -> Prop -> IO (RawSequent Prop) -normalizeHyp sc p = - do t <- scWhnf sc (unProp p) - case asEqTrue t of - Just b -> normalizeHypBool sc b >>= \case - Just sqt -> return sqt - Nothing -> return (RawSequent [p] []) - _ -> return (RawSequent [p] []) - -normalizeConcl :: SharedContext -> Prop -> IO (RawSequent Prop) -normalizeConcl sc p = - do t <- scWhnf sc (unProp p) - case asEqTrue t of - Just b -> normalizeConclBool sc b >>= \case - Just sqt -> return sqt - Nothing -> return (RawSequent [] [p]) - _ -> - -- handle the case of (H1 -> H2), where H1 and H2 are in Prop - case asPi t of - Just (nm, arg, body) - -- check that this is non-dependent Pi (AKA arrow type) - | IntSet.notMember (vnIndex nm) (freeVars body) -> - termToMaybeProp sc arg >>= \case - Nothing -> return (RawSequent [] [p]) - Just h -> - do hsqt <- normalizeHyp sc h - gsqt <- normalizeConcl sc (Prop body) - return (joinSequent hsqt gsqt) - _ -> return (RawSequent [] [p]) - -normalizeHypBool :: SharedContext -> Term -> IO (Maybe (RawSequent Prop)) -normalizeHypBool sc b - -- Don't evaluate to WHNF. That would unfold Prelude.not and Prelude.and - | Just (_ :*: p1) <- (isGlobalDef "Prelude.not" <@> return) b - = Just <$> normalizeConclBoolCommit sc p1 - - | Just (_ :*: p1 :*: p2) <- (isGlobalDef "Prelude.and" <@> return <@> return) b - = Just <$> (joinSequent <$> normalizeHypBoolCommit sc p1 <*> normalizeHypBoolCommit sc p2) - - | otherwise - = return Nothing - -normalizeHypBoolCommit :: SharedContext -> Term -> IO (RawSequent Prop) -normalizeHypBoolCommit sc b = - normalizeHypBool sc b >>= \case - Just sqt -> return sqt - Nothing -> do p <- boolToProp sc [] b - return (RawSequent [p] []) - -normalizeConclBool :: SharedContext -> Term -> IO (Maybe (RawSequent Prop)) -normalizeConclBool sc b - -- Don't evaluate to WHNF. That would unfold Prelude.not, Prelude.or and Prelude.implies - | Just (_ :*: p1) <- (isGlobalDef "Prelude.not" <@> return) b - = Just <$> normalizeHypBoolCommit sc p1 - - | Just (_ :*: p1 :*: p2) <- (isGlobalDef "Prelude.or" <@> return <@> return) b - = Just <$> (joinSequent <$> normalizeConclBoolCommit sc p1 <*> normalizeConclBoolCommit sc p2) - - | Just (_ :*: p1 :*: p2) <- (isGlobalDef "Prelude.implies" <@> return <@> return) b - = Just <$> (joinSequent <$> normalizeHypBoolCommit sc p1 <*> normalizeConclBoolCommit sc p2) - - | otherwise - = return Nothing - -normalizeConclBoolCommit :: SharedContext -> Term -> IO (RawSequent Prop) -normalizeConclBoolCommit sc b = - normalizeConclBool sc b >>= \case - Just sqt -> return sqt - Nothing -> do p <- boolToProp sc [] b - return (RawSequent [] [p]) - +-- of the first prop is sufficient to prove the second. +propSubsumes :: SharedContext -> Prop -> Prop -> IO Bool +propSubsumes sc g1 g2 = + propsSubset sc [g2] [g1] -- proves no *less* -- | Verify that the given evidence in fact supports the given proposition. -- Returns the identifiers of all the theorems depended on while checking evidence @@ -1616,20 +941,20 @@ checkEvidence :: IO (Set TheoremNonce, TheoremSummary, Hypotheses) checkEvidence sc what4PushMuxOps = \e p -> do nenv <- scGetNamingEnv sc - check nenv e (propToSequent p) + check nenv e p where - checkApply _nenv _mkSqt (Prop p) [] = return (mempty, mempty, p, termHypotheses p) + checkApply _nenv (Prop p) [] = return (mempty, mempty, p, termHypotheses p) -- Check a theorem applied to "Evidence". -- The given prop must be an implication -- (i.e., nondependent Pi quantifying over a Prop) -- and the given evidence must match the expected prop. - checkApply nenv mkSqt (Prop p) (Right e:es) + checkApply nenv (Prop p) (Right e:es) | Just (lnm, tp, body) <- asPi p , IntSet.notMember (vnIndex lnm) (freeVars body) - = do (d1, sy1, hyps1) <- check nenv e . mkSqt =<< termToProp sc tp - (d2, sy2, p', hyps2) <- checkApply nenv mkSqt (Prop body) es + = do (d1, sy1, hyps1) <- check nenv e =<< termToProp sc tp + (d2, sy2, p', hyps2) <- checkApply nenv (Prop body) es return (Set.union d1 d2, sy1 <> sy2, p', hyps1 <> hyps2) | otherwise = do p' <- ppTerm sc p @@ -1640,20 +965,20 @@ checkEvidence sc what4PushMuxOps = \e p -> do -- Check a theorem applied to a term. This explicitly instantiates -- a Pi binder with the given term. - checkApply nenv mkSqt (Prop p) (Left tm:es) = + checkApply nenv (Prop p) (Left tm:es) = do p1 <- reducePi sc p tm - (deps, sy, p2, hyps) <- checkApply nenv mkSqt (Prop p1) es + (deps, sy, p2, hyps) <- checkApply nenv (Prop p1) es pure (deps, sy, p2, hyps <> termHypotheses tm) check :: DisplayNameEnv -> Evidence -> - Sequent -> + Prop -> IO (Set TheoremNonce, TheoremSummary, HashSet Term) check nenv e sqt = case e of ProofTerm tm -> - case sequentState sqt of - ConclFocus (Prop ptm) _ -> + case sqt of + Prop ptm -> do ty <- scTypeOf sc tm ok <- scConvertible sc ptm ty unless ok $ do @@ -1665,90 +990,46 @@ checkEvidence sc what4PushMuxOps = \e p -> do tm' ] return (mempty, ProvedTheorem mempty, termHypotheses tm) - _ -> fail "Sequent must be conclusion-focused for proof term evidence" SolverEvidence stats sqt' -> - do ok <- sequentSubsumes sc sqt' sqt + do ok <- propSubsumes sc sqt' sqt unless ok $ do ppopts <- scGetPPOpts sc fail $ PPS.render ppopts $ PP.vsep [ "Solver proof does not prove the required sequent" - , prettySequent ppopts nenv sqt - , prettySequent ppopts nenv sqt' + , prettyProp ppopts nenv sqt + , prettyProp ppopts nenv sqt' ] - return (mempty, ProvedTheorem stats, sequentHypotheses sqt') + return (mempty, ProvedTheorem stats, propHypotheses sqt') Admitted msg pos sqt' -> - do ok <- sequentSubsumes sc sqt' sqt + do ok <- propSubsumes sc sqt' sqt unless ok $ do ppopts <- scGetPPOpts sc let pos' = prettyPosition pos fail $ PPS.render ppopts $ PP.vsep [ "Admitted proof does not match the required sequent" <+> pos' , pretty msg - , prettySequent ppopts nenv sqt - , prettySequent ppopts nenv sqt' + , prettyProp ppopts nenv sqt + , prettyProp ppopts nenv sqt' ] - return (mempty, AdmittedTheorem msg, sequentHypotheses sqt') + return (mempty, AdmittedTheorem msg, propHypotheses sqt') QuickcheckEvidence n sqt' -> - do ok <- sequentSubsumes sc sqt' sqt + do ok <- propSubsumes sc sqt' sqt unless ok $ do ppopts <- scGetPPOpts sc fail $ PPS.render ppopts $ PP.vsep [ "Quickcheck evidence does not match the required sequent" - , prettySequent ppopts nenv sqt - , prettySequent ppopts nenv sqt' + , prettyProp ppopts nenv sqt + , prettyProp ppopts nenv sqt' ] - return (mempty, TestedTheorem n, sequentHypotheses sqt') - - SplitEvidence e1 e2 -> - splitSequent sc sqt >>= \case - Nothing -> do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep - [ "Split evidence does not apply" - , prettySequent ppopts nenv sqt - ] - Just (sqt1,sqt2) -> - do d1 <- check nenv e1 sqt1 - d2 <- check nenv e2 sqt2 - return (d1 <> d2) - - ApplyHypEvidence n es -> - case sqt of - ConclFocusedSequent hs (FB gs1 g gs2) -> - case genericDrop n hs of - (h:_) -> - do (d, sy, p', hyps) <- checkApply nenv (\g' -> ConclFocusedSequent hs (FB gs1 g' gs2)) h es - ok <- scConvertible sc (unProp g) p' - unless ok $ do - g' <- ppTerm sc (unProp g) - p'' <- ppTerm sc p' - fail $ unlines [ - "Apply evidence does not match the required proposition", - g', - p'' - ] - return (d, sy, hyps) - - _ -> do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep - [ "Not enough hypotheses in apply hypothesis:" <+> PP.viaShow n - , prettySequent ppopts nenv sqt - ] - _ -> do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep - [ "Apply hypothesis evidence requires a conclusion-focused sequent." - , prettySequent ppopts nenv sqt - ] + return (mempty, TestedTheorem n, propHypotheses sqt') ApplyEvidence thm es -> - case sequentState sqt of - ConclFocus p mkSqt -> - do (d, sy, p', hyps) <- checkApply nenv mkSqt (thmProp thm) es + case sqt of + p -> + do (d, sy, p', hyps) <- checkApply nenv (thmProp thm) es ok <- scConvertible sc (unProp p) p' unless ok $ do sp <- ppTerm sc (unProp p) @@ -1759,87 +1040,43 @@ checkEvidence sc what4PushMuxOps = \e p -> do sp' ] return (Set.insert (thmNonce thm) d, sy, thmHyps thm <> hyps) - _ -> do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep - [ "Apply evidence requires a conclusion-focused sequent" - , prettySequent ppopts nenv sqt - ] UnfoldEvidence vars e' -> - do sqt' <- traverseSequentWithFocus (unfoldProp sc vars) sqt + do sqt' <- unfoldProp sc vars sqt check nenv e' sqt' UnfoldFixOnceEvidence vars e' -> - do sqt' <- traverseSequentWithFocus (unfoldFixOnceProp sc vars) sqt + do sqt' <- unfoldFixOnceProp sc vars sqt check nenv e' sqt' NormalizePropEvidence opqueSet e' -> - do sqt' <- traverseSequentWithFocus (normalizeProp sc opqueSet) sqt + do sqt' <- normalizeProp sc opqueSet sqt check nenv e' sqt' - RewriteEvidence hs ss e' -> - do ss' <- localHypSimpset sc sqt hs ss - (TheoremAnnotation d1 h1 s1, sqt') <- simplifySequent sc ss' sqt + RewriteEvidence ss e' -> + do (TheoremAnnotation d1 h1 s1, sqt') <- simplifyProp sc ss sqt (d2, s2, h2) <- check nenv e' sqt' return (d1 <> d2, s1 <> s2, h1 <> h2) HoistIfsEvidence e' -> - do sqt' <- traverseSequentWithFocus (hoistIfsInProp sc) sqt + do sqt' <- hoistIfsInProp sc sqt check nenv e' sqt' EvalEvidence vars e' -> - do sqt' <- traverseSequentWithFocus (evalProp sc what4PushMuxOps vars) sqt + do sqt' <- evalProp sc what4PushMuxOps vars sqt check nenv e' sqt' ConversionEvidence sqt' e' -> - do ok <- convertibleSequents sc sqt sqt' + do ok <- convertibleProps sc sqt sqt' unless ok $ do ppopts <- scGetPPOpts sc fail $ PPS.render ppopts $ PP.vsep [ "Converted sequent does not match goal", - prettySequent ppopts nenv sqt, - prettySequent ppopts nenv sqt' + prettyProp ppopts nenv sqt, + prettyProp ppopts nenv sqt' ] check nenv e' sqt' - NormalizeSequentEvidence sqt' e' -> - do ok <- normalizeSequentSubsumes sc sqt' sqt - unless ok $ do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep [ - "Normalized sequent does not subsume goal", - prettySequent ppopts nenv sqt, - prettySequent ppopts nenv sqt' - ] - check nenv e' sqt' - - StructuralEvidence sqt' e' -> - do ok <- sequentSubsumes sc sqt' sqt - unless ok $ do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep [ - "Sequent does not subsume goal", - prettySequent ppopts nenv sqt, - prettySequent ppopts nenv sqt' - ] - check nenv e' sqt' - - AxiomEvidence -> - do ok <- sequentIsAxiom sc sqt - unless ok $ do - ppopts <- scGetPPOpts sc - fail $ PPS.render ppopts $ PP.vsep [ - "Sequent is not an instance of the sequent calculus axiom", - prettySequent ppopts nenv sqt - ] - return (mempty, ProvedTheorem mempty, mempty) - - CutEvidence p ehyp egl -> - do d1 <- check nenv ehyp (addHypothesis p sqt) - d2 <- check nenv egl (addNewFocusedConcl p sqt) - return (d1 <> d2) - IntroEvidence x xty e' -> -- TODO! Check that the given VarName is fresh for the sequent. -- @@ -1853,10 +1090,8 @@ checkEvidence sc what4PushMuxOps = \e p -> do -- quite a bit of additional infrastructure to do the necessary replacements, and we -- will need to be pretty careful if we want to avoid repeated traversals (which -- could cause substantial performance issues). - case sequentState sqt of - Unfocused -> fail "Intro evidence requires a focused sequent" - HypFocus _ _ -> fail "Intro evidence apply in hypothesis" - ConclFocus (Prop ptm) mkSqt -> + case sqt of + Prop ptm -> case asPi ptm of Nothing -> do ptm' <- ppTerm sc ptm @@ -1873,7 +1108,7 @@ checkEvidence sc what4PushMuxOps = \e p -> do ] x' <- scVariable sc x xty body' <- scInstantiate sc (IntMap.singleton (vnIndex nm) x') body - (deps, sy, hyps) <- check nenv e' (mkSqt (Prop body')) + (deps, sy, hyps) <- check nenv e' (Prop body') let hyps' = HashSet.delete xty hyps pure (deps, sy, hyps') @@ -1896,7 +1131,7 @@ setProofTimeout to ps = ps { _psTimeout = Just to } startProof :: ProofGoal -> Pos -> Maybe ProgramLoc -> Text -> IO ProofState startProof g pos ploc rsn = do start <- getCurrentTime - pure (ProofState [g] (goalSequent g,pos,ploc,rsn) mempty Nothing passthroughEvidence start) + pure (ProofState [g] (goalProp g,pos,ploc,rsn) mempty Nothing passthroughEvidence start) -- | Attempt to complete a proof by checking that all subgoals have been discharged, -- and validate the computed evidence to ensure that it supports the original @@ -1922,20 +1157,16 @@ finishProof :: Prop -> ProofState -> Bool {- ^ should we record the theorem in the database? -} -> - Bool {- ^ do we need to normalize the sequent to match the final goal ? -} -> Bool {- ^ If 'True', push certain @ExprBuilder@ operations (e.g., @zext@) down to the branches of @ite@ expressions -} -> IO (ProofResult, TheoremDB) finishProof sc db conclProp - ps@(ProofState gs (concl,loc,ploc,rsn) stats _ checkEv start) - recordThm useSequentGoals what4PushMuxOps = + ps@(ProofState gs (_concl,loc,ploc,rsn) stats _ checkEv start) + recordThm what4PushMuxOps = case gs of [] -> do e <- checkEv [] - let e' = if useSequentGoals - then NormalizeSequentEvidence concl e - else e - (deps, sy, hyps) <- checkEvidence sc what4PushMuxOps e' conclProp + (deps, sy, hyps) <- checkEvidence sc what4PushMuxOps e conclProp -- Fail if hyps includes any types that do not correspond to a -- free variable in the conclusion let extraHyps = HashSet.difference hyps (propHypotheses conclProp) @@ -1949,7 +1180,7 @@ finishProof sc db conclProp { _thmProp = conclProp , _thmHyps = hyps , _thmStats = stats - , _thmEvidence = e' + , _thmEvidence = e , _thmLocation = loc , _thmProgramLoc = ploc , _thmReason = rsn @@ -2100,20 +1331,11 @@ predicateToSATQuery sc unintSet tm0 = -- | Given a proposition, compute a SAT query which will prove the proposition -- iff the SAT query is unsatisfiable. propToSATQuery :: SharedContext -> Set VarIndex -> Prop -> IO SATQuery -propToSATQuery sc unintSet prop = sequentToSATQuery sc unintSet (propToSequent prop) - --- | Given a proposition, compute a SAT query which will prove the proposition --- iff the SAT query is unsatisfiable. -sequentToSATQuery :: SharedContext -> Set VarIndex -> Sequent -> IO SATQuery -sequentToSATQuery sc unintSet sqt = - do let RawSequent hs gs = sequentToRawSequent sqt - mmap <- scGetModuleMap sc - let frees = foldMap getAllVarsMap (map unProp (hs ++ gs)) +propToSATQuery sc unintSet g = + do mmap <- scGetModuleMap sc + let frees = getAllVarsMap (unProp g) (initVars, abstractVars) <- filterFirstOrderVars mmap mempty mempty (Map.toList frees) - -- NB, the following reversals make the order of assertions more closely match the input sequent, - -- but should otherwise not be semantically relevant - hypAsserts <- mapM (processAssert mmap) (reverse (map unProp hs)) - (finalVars, asserts) <- foldM (processConcl mmap) (initVars, hypAsserts) (map unProp gs) + (finalVars, asserts) <- foldM (processConcl mmap) (initVars, []) [unProp g] return SATQuery { satVariables = finalVars , satUninterp = Set.union unintSet abstractVars @@ -2245,8 +1467,8 @@ tacticIntro :: (F.MonadFail m, MonadIO m) => Text {- ^ Name to give to the variable. If empty, will be chosen automatically from the goal. -} -> Tactic m TypedTerm tacticIntro sc usernm = Tactic \goal -> - case sequentState (goalSequent goal) of - ConclFocus p mkSqt -> + case goalProp goal of + p -> case asPi (unProp p) of Just (vn, tp, body) -> do let nm = vnName vn @@ -2255,98 +1477,22 @@ tacticIntro sc usernm = Tactic \goal -> x <- liftIO $ scVariable sc vn' tp tt <- liftIO $ mkTypedTerm sc x body' <- liftIO $ scInstantiate sc (IntMap.singleton (vnIndex vn) x) body - let goal' = goal { goalSequent = mkSqt (Prop body') } + let goal' = goal { goalProp = Prop body' } return (tt, mempty, [goal'], introEvidence vn' tp) _ -> fail "intro tactic failed: not a function" - _ -> fail "intro tactic: conclusion focus required" - --- | Given a focused conclusion, decompose the conclusion along implications by --- introducing new hypotheses. The given integer indicates how many hypotheses --- to introduce. -tacticIntroHyps :: (F.MonadFail m, MonadIO m) => SharedContext -> Integer -> Tactic m () -tacticIntroHyps sc n = Tactic \goal -> - case goalSequent goal of - ConclFocusedSequent hs (FB gs1 g gs2) -> - do (newhs, g') <- liftIO (loop n g) - let sqt' = ConclFocusedSequent (hs ++ newhs) (FB gs1 g' gs2) - let goal' = goal{ goalSequent = sqt' } - return ((), mempty, [goal'], updateEvidence (NormalizeSequentEvidence sqt')) - _ -> fail "goal_intro_hyps: conclusion focus required" - - where - loop i g - | i <= 0 = return ([],g) - | otherwise = - splitImpl sc g >>= \case - Nothing -> fail "intro_hyps: could not find enough hypotheses to introduce" - Just (h,g') -> - do (hs,g'') <- loop (i-1) g' - return (h:hs, g'') - -tacticRevertHyp :: (F.MonadFail m, MonadIO m) => SharedContext -> Integer -> Tactic m () -tacticRevertHyp sc i = Tactic \goal -> - case goalSequent goal of - ConclFocusedSequent hs (FB gs1 g gs2) -> - case genericDrop i hs of - (h:_) -> - case (asEqTrue (unProp h), asEqTrue (unProp g)) of - (Just h', Just g') -> - do g'' <- liftIO (Prop <$> (scEqTrue sc =<< scImplies sc h' g')) - let sqt' = ConclFocusedSequent hs (FB gs1 g'' gs2) - let goal' = goal{ goalSequent = sqt' } - return ((), mempty, [goal'], updateEvidence (NormalizeSequentEvidence sqt')) - - _ -> fail "goal_revert_hyp: expected EqTrue props" - _ -> fail "goal_revert_hyp: not enough hypotheses" - _ -> fail "goal_revert_hyp: conclusion focus required" - - --- | Attempt to prove a goal by applying a local hypothesis. Any hypotheses of --- the applied proposition will generate additional subgoals. -tacticApplyHyp :: (F.MonadFail m, MonadIO m) => SharedContext -> Integer -> Tactic m () -tacticApplyHyp sc n = Tactic \goal -> - case goalSequent goal of - UnfocusedSequent{} -> fail "apply hyp tactic: focus required" - HypFocusedSequent{} -> fail "apply hyp tactic: cannot apply in a hypothesis" - ConclFocusedSequent hs (FB gs1 g gs2) -> - case genericDrop n hs of - (h:_) -> - liftIO (propApply sc h g) >>= \case - Nothing -> fail "apply hyp tactic: no match" - Just newterms -> - let newgoals = - [ goal{ goalSequent = ConclFocusedSequent hs (FB gs1 p gs2) - , goalType = goalType goal ++ ".subgoal" ++ show i - } - | Right p <- newterms - | i <- [0::Integer ..] - ] in - return ((), mempty, newgoals, \es -> ApplyHypEvidence n <$> processEvidence newterms es) - _ -> fail "apply hyp tactic: not enough hypotheses" - - where - processEvidence :: [Either Term Prop] -> [Evidence] -> IO [Either Term Evidence] - processEvidence (Left tm : xs) es = (Left tm :) <$> processEvidence xs es - processEvidence (Right _ : xs) (e:es) = (Right e :) <$> processEvidence xs es - processEvidence [] [] = pure [] - processEvidence _ _ = fail "apply hyp tactic failed: evidence mismatch" - - -- | Attempt to prove a goal by applying the given theorem. Any hypotheses of -- the theorem will generate additional subgoals. tacticApply :: (F.MonadFail m, MonadIO m) => SharedContext -> Theorem -> Tactic m () tacticApply sc thm = Tactic \goal -> - case sequentState (goalSequent goal) of - Unfocused -> fail "apply tactic: focus required" - HypFocus _ _ -> fail "apply tactic: cannot apply in a hypothesis" - ConclFocus gl mkSqt -> + case goalProp goal of + gl -> liftIO (propApply sc (thmProp thm) gl) >>= \case Nothing -> fail "apply tactic failed: no match" Just newterms -> let newgoals = - [ goal{ goalSequent = mkSqt p, goalType = goalType goal ++ ".subgoal" ++ show i } + [ goal{ goalProp = p, goalType = goalType goal ++ ".subgoal" ++ show i } | Right p <- newterms | i <- [0::Integer ..] ] in @@ -2359,83 +1505,11 @@ tacticApply sc thm = Tactic \goal -> processEvidence [] [] = pure [] processEvidence _ _ = fail "apply tactic failed: evidence mismatch" --- | Attempt to simplify a goal by splitting it along conjunctions, disjunctions, --- implication or if/then/else. If successful, two subgoals will be produced, --- representing the two subgoals that must be proved. -tacticSplit :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m () -tacticSplit sc = Tactic \gl -> - liftIO (splitSequent sc (goalSequent gl)) >>= \case - Just (sqt1, sqt2) -> - do let g1 = gl{ goalType = goalType gl ++ ".l", goalSequent = sqt1 } - let g2 = gl{ goalType = goalType gl ++ ".r", goalSequent = sqt2 } - return ((), mempty, [g1,g2], splitEvidence) - Nothing -> fail "split tactic failed" - --- | Specialize a focused hypothesis with the given terms. A new specialized --- hypothesis will be added to the sequent; the original hypothesis will --- remain focused. -tacticSpecializeHyp :: - (F.MonadFail m, MonadIO m) => SharedContext -> [Term] -> Tactic m () -tacticSpecializeHyp sc ts = Tactic \gl -> - case goalSequent gl of - HypFocusedSequent (FB hs1 h hs2) gs -> - do res <- liftIO (specializeProp sc h ts) - case res of - Left err -> do - ppopts <- liftIO $ scGetPPOpts sc - err' <- liftIO $ prettyTermError sc err - fail $ PPS.render ppopts $ PP.vsep [ - "specialize_hyp tactic: failed to specialize", - err' - ] - Right h' -> - do let gl' = gl{ goalSequent = HypFocusedSequent (FB hs1 h (hs2++[h'])) gs } - return ((), mempty, [gl'], specializeHypEvidence (genericLength hs1) h' ts) - _ -> fail "specialize_hyp tactic failed: requires hypothesis focus" - - --- | This tactic adds a new hypothesis to the current goal by first specializing the --- given theorem with the list of terms provided and then using cut to add the --- hypothesis, discharging the produced additional goal by applying the theorem. -tacticInsert :: (F.MonadFail m, MonadIO m) => SharedContext -> Theorem -> [Term] -> Tactic m () -tacticInsert sc thm ts = Tactic \gl -> - do res <- liftIO (specializeProp sc (_thmProp thm) ts) - case res of - Left err -> do - ppopts <- liftIO $ scGetPPOpts sc - err' <- liftIO $ prettyTermError sc err - fail $ PPS.render ppopts $ PP.vsep [ - "goal_insert_and_specialize tactic: failed to specialize:", - err' - ] - Right h -> - do let gl' = gl{ goalSequent = addHypothesis h (goalSequent gl) } - return ((), mempty, [gl'], insertEvidence thm h ts) - --- | This tactic implements the "cut rule" of sequent calculus. The given --- proposition is used to split the current goal into two goals, one where --- the given proposition is assumed as a new hypothesis, and a second --- where the proposition is added as a new conclusion to prove. --- --- HS, X |- GS --- HS |- GS, X --- ------------------ (Cut) --- HS |- GS -tacticCut :: (F.MonadFail m, MonadIO m) => SharedContext -> Prop -> Tactic m () -tacticCut _sc p = Tactic \gl -> - let sqt1 = addHypothesis p (goalSequent gl) - sqt2 = addNewFocusedConcl p (goalSequent gl) - g1 = gl{ goalType = goalType gl ++ ".cutH", goalSequent = sqt1 } - g2 = gl{ goalType = goalType gl ++ ".cutG", goalSequent = sqt2 } - in return ((), mempty, [g1, g2], cutEvidence p) - -- | Attempt to solve a goal by recognizing it as a trivially true proposition. tacticTrivial :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m () tacticTrivial sc = Tactic \goal -> - case sequentState (goalSequent goal) of - Unfocused -> fail "trivial tactic: focus required" - HypFocus _ _ -> fail "trivial tactic: cannot apply trivial in a hypothesis" - ConclFocus g _ -> + case goalProp goal of + g -> liftIO (trivialProofTerm sc g) >>= \case Left err -> fail err Right pf -> @@ -2453,10 +1527,8 @@ tacticTrivial sc = Tactic \goal -> -- | Attempt to prove a goal by giving a direct proof term. tacticExact :: (F.MonadFail m, MonadIO m) => SharedContext -> Term -> Tactic m () tacticExact sc tm = Tactic \goal -> - case sequentState (goalSequent goal) of - Unfocused -> fail "tactic exact: focus required" - HypFocus _ _ -> fail "tactic exact: cannot apply exact in a hypothesis" - ConclFocus g _ -> + case goalProp goal of + g -> do let gp = unProp g ty <- liftIO $ scTypeOf sc tm ok <- liftIO $ scConvertible sc gp ty @@ -2502,7 +1574,7 @@ tacticSolve f = Tactic \gl -> -- The tactic should return a new proposition to prove and a method for -- transferring evidence for the modified proposition into a evidence for -- the original goal. -tacticChange :: Monad m => (ProofGoal -> m (Sequent, Evidence -> Evidence)) -> Tactic m () +tacticChange :: Monad m => (ProofGoal -> m (Prop, Evidence -> Evidence)) -> Tactic m () tacticChange f = Tactic \gl -> - do (sqt, ef) <- lift (f gl) - return ((), mempty, [ gl{ goalSequent = sqt } ], updateEvidence ef) + do (p, ef) <- lift (f gl) + return ((), mempty, [ gl{ goalProp = p } ], updateEvidence ef) diff --git a/saw-central/src/SAWCentral/Prover/ABC.hs b/saw-central/src/SAWCentral/Prover/ABC.hs index 4ae17ae037..2751bba03c 100644 --- a/saw-central/src/SAWCentral/Prover/ABC.hs +++ b/saw-central/src/SAWCentral/Prover/ABC.hs @@ -32,9 +32,9 @@ import qualified SAWCoreAIG.BitBlast as BBSim import SAWCentral.Panic (panic) import SAWCentral.Proof - ( sequentToSATQuery, goalSequent, ProofGoal + ( propToSATQuery, goalProp, ProofGoal , goalType, goalNum, CEX - , sequentSharedSize + , propSharedSize ) import SAWCentral.Prover.SolverStats (SolverStats, solverStats) import qualified SAWCentral.Prover.Exporter as Exporter @@ -171,7 +171,7 @@ abcSatExternal :: MonadIO m => ProofGoal -> m (Maybe CEX, SolverStats) abcSatExternal proxy sc doCNF execName args g = liftIO $ - do satq <- sequentToSATQuery sc mempty (goalSequent g) + do satq <- propToSATQuery sc mempty (goalProp g) let cnfName = goalType g ++ show (goalNum g) ++ ".cnf" (path, fh) <- openTempFile "." cnfName hClose fh -- Yuck. TODO: allow writeCNF et al. to work on handles. @@ -189,7 +189,7 @@ abcSatExternal proxy sc doCNF execName args g = liftIO $ let ls = lines out sls = filter ("s " `isPrefixOf`) ls vls = filter ("v " `isPrefixOf`) ls - let stats = solverStats ("external SAT: " <> Text.pack execName) (sequentSharedSize (goalSequent g)) + let stats = solverStats ("external SAT: " <> Text.pack execName) (propSharedSize (goalProp g)) case (sls, vls) of (["s SATISFIABLE"], _) -> do let bs = parseDimacsSolution variables vls diff --git a/saw-central/src/SAWCentral/Prover/Exporter.hs b/saw-central/src/SAWCentral/Prover/Exporter.hs index 2a6544cbee..bcafac6ef5 100644 --- a/saw-central/src/SAWCentral/Prover/Exporter.hs +++ b/saw-central/src/SAWCentral/Prover/Exporter.hs @@ -96,7 +96,7 @@ import SAWCoreWhat4.ReturnTrip (newSAWCoreExprBuilder, sawCoreState) import qualified SAWCore.Parser.AST as Un import SAWCentral.Proof - (Prop, Sequent, propSize, sequentSharedSize, propToTerm, predicateToSATQuery, sequentToSATQuery) + (Prop, propSize, propSharedSize, propToTerm, predicateToSATQuery, propToSATQuery) import SAWCentral.Prover.SolverStats import SAWCentral.Prover.Util import SAWCentral.Prover.What4 @@ -116,13 +116,13 @@ proveWithSATExporter :: (FilePath -> SATQuery -> TopLevel a) -> Set VarIndex -> FilePath -> - Sequent -> + Prop -> TopLevel SolverStats proveWithSATExporter exporter unintSet path goal = do sc <- getSharedContext - satq <- io $ sequentToSATQuery sc unintSet goal + satq <- io $ propToSATQuery sc unintSet goal _ <- exporter path satq - let stats = solverStats ("offline: " <> Text.pack path) (sequentSharedSize goal) + let stats = solverStats ("offline: " <> Text.pack path) (propSharedSize goal) return stats diff --git a/saw-central/src/SAWCentral/Prover/What4.hs b/saw-central/src/SAWCentral/Prover/What4.hs index 56c76628c4..903ab07edf 100644 --- a/saw-central/src/SAWCentral/Prover/What4.hs +++ b/saw-central/src/SAWCentral/Prover/What4.hs @@ -45,7 +45,7 @@ import SAWCore.SharedTerm import SAWCore.FiniteValue import SAWCore.SATQuery (SATQuery(..)) -import SAWCentral.Proof(Sequent, sequentToSATQuery, CEX) +import SAWCentral.Proof(Prop, propToSATQuery, CEX) import SAWCentral.Value (TopLevel, io, getSharedContext, rwWhat4PushMuxOps) import Data.Parameterized.Nonce @@ -92,14 +92,14 @@ setupWhat4_sym hashConsing what4PushMuxOps = what4Theories :: Set VarIndex -> Bool -> - Sequent -> + Prop -> TopLevel [Text] what4Theories unintSet hashConsing goal = do sc <- getSharedContext what4PushMuxOps <- gets rwWhat4PushMuxOps io $ do sym <- setupWhat4_sym hashConsing what4PushMuxOps - satq <- sequentToSATQuery sc unintSet goal + satq <- propToSATQuery sc unintSet goal (_varMap, lits) <- W.w4Solve sym sc satq let pf lit = (predicateVarInfo lit)^.problemFeatures return (nub (concatMap evalTheories (map pf lits))) diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs index 44ce8d7d78..7d9f8fff27 100644 --- a/saw-central/src/SAWCentral/Value.hs +++ b/saw-central/src/SAWCentral/Value.hs @@ -1129,7 +1129,6 @@ data TopLevelRW = , rwPathSatSolver :: Common.PathSatSolver , rwSkipSafetyProofs :: Bool , rwSingleOverrideSpecialCase :: Bool - , rwSequentGoals :: Bool } newtype TopLevel a = @@ -1636,9 +1635,8 @@ runProofScript :: Maybe ProgramLoc -> Text -> Bool {- ^ record the theorem in the database? -} -> - Bool {- ^ do we need to normalize the sequent goal? -} -> TopLevel ProofResult -runProofScript (ProofScript m) concl gl ploc rsn recordThm useSequentGoals = +runProofScript (ProofScript m) concl gl ploc rsn recordThm = do pos <- getPosition ps <- io (startProof gl pos ploc rsn) (r,pstate) <- runStateT (runExceptT m) ps @@ -1648,7 +1646,7 @@ runProofScript (ProofScript m) concl gl ploc rsn recordThm useSequentGoals = do sc <- getSharedContext db <- getTheoremDB what4PushMuxOps <- gets rwWhat4PushMuxOps - (thmResult, db') <- io (finishProof sc db concl pstate recordThm useSequentGoals what4PushMuxOps) + (thmResult, db') <- io (finishProof sc db concl pstate recordThm what4PushMuxOps) putTheoremDB db' pure thmResult diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs index f56a0b9720..0a4987cccf 100644 --- a/saw-script/src/SAWScript/Interpreter.hs +++ b/saw-script/src/SAWScript/Interpreter.hs @@ -1324,7 +1324,6 @@ buildTopLevelEnv opts scriptArgv tlhook pshook = do , rwPathSatSolver = CC.PathSat_Z3 , rwSkipSafetyProofs = False , rwSingleOverrideSpecialCase = False - , rwSequentGoals = False , rwJavaCodebase = JavaUninitialized } return (ro0, rw0) @@ -2071,16 +2070,6 @@ disable_safety_proofs = do rw <- getTopLevelRW putTopLevelRW rw{ rwSkipSafetyProofs = True } -enable_sequent_goals :: TopLevel () -enable_sequent_goals = do - rw <- getTopLevelRW - putTopLevelRW rw{ rwSequentGoals = True } - -disable_sequent_goals :: TopLevel () -disable_sequent_goals = do - rw <- getTopLevelRW - putTopLevelRW rw{ rwSequentGoals = False } - enable_smt_array_memory_model :: TopLevel () enable_smt_array_memory_model = do rw <- getTopLevelRW @@ -3187,23 +3176,6 @@ primitives = Map.fromList $ Current [ "Disable the SMT array memory model." ] - , prim "enable_sequent_goals" "TopLevel ()" - (pureVal enable_sequent_goals) - Experimental - [ "When verifying proof obligations arising from 'llvm_verify' and" - , "similar commands, generate sequents (that is, multiple separate" - , "goals) for the resulting proof obligations instead of a single" - , "overarching goal." - ] - - , prim "disable_sequent_goals" "TopLevel ()" - (pureVal disable_sequent_goals) - Experimental - [ "Restore the default behavior, which is to generate single" - , "boolean goals for proof obligations arising from verification" - , "commands." - ] - , prim "enable_safety_proofs" "TopLevel ()" (pureVal enable_safety_proofs) Experimental @@ -3927,6 +3899,15 @@ primitives = Map.fromList $ , "the proof fails." ] + , prim "subproof" "ProofScript () -> ProofScript ()" + (pureVal subProofScript) + Current + [ "Run the given proof script as a subproof starting from a state" + , "where only the first subgoal is visible. The inner proof script" + , "must discharge its goal, leaving no remaining subgoals; otherwise" + , "the proof fails." + ] + , prim "core_axiom" "String -> Theorem" (funVal1 core_axiom) Current @@ -3941,6 +3922,13 @@ primitives = Map.fromList $ Current [ "Create a theorem from the type of the given core expression." ] + , prim "apply_thm" "Theorem -> [Theorem] -> Theorem" + (funVal2 apply_thm) + Experimental + [ "Apply a theorem of the form `P1 -> P2 -> ... Pn -> Q` to list" + , "of theorems `P1`, `P2` ... `Pn` to yield a theorem `Q`." + ] + , prim "specialize_theorem" "Theorem -> [Term] -> TopLevel Theorem" (pureVal specialize_theorem) Experimental @@ -3948,6 +3936,20 @@ primitives = Map.fromList $ , "the given list of terms." ] + , prim "specialize_thm" "Theorem -> [Term] -> Theorem" + (funVal2 specialize_theorem) + Experimental + [ "Specialize a theorem by instantiating universal quantifiers with" + , "the given list of terms." + ] + + , prim "term_thm" "Term -> Theorem" + (funVal1 term_thm) + Current + [ "Create a theorem from the the given proof term, whose type must" + , "be of sort `Prop`." + ] + , prim "prove_bisim" ("ProofScript () -> [BisimTheorem] -> " <> "Term -> Term -> Term -> Term -> " <> "TopLevel BisimTheorem") @@ -4168,27 +4170,6 @@ primitives = Map.fromList $ , "ill-typed. Also see 'check_term'." ] - ------------------------------------------------------------ - -- Decomposition-related proof tactics - - , prim "split_goal" "ProofScript ()" - (pureVal split_goal) - Experimental - [ "Split a goal of the form 'Prelude.and prop1 prop2' into two" - , "separate goals 'prop1' and 'prop2'." - ] - - , prim "goal_cut" "Term -> ProofScript ()" - (pureVal goal_cut) - Experimental - [ "Given a term provided by the user (which must be a boolean" - , "expression or a Prop) the current goal is split into two" - , "subgoals. In the first subgoal, the given proposition is assumed" - , "as a new hypothesis. In the second subgoal, the given" - , "proposition is a new focused, conclusion. This implements the" - , "usual cut rule of sequent calculus." - ] - ------------------------------------------------------------ -- Evaluation-related proof tactics @@ -4212,13 +4193,6 @@ primitives = Map.fromList $ Current [ "Apply the given simplification rule set to the current goal." ] - , prim "simplify_local" "[Int] -> Simpset -> ProofScript ()" - (pureVal simplifyGoalWithLocals) - Current - [ "Apply the given simplification rule set to the current goal." - , "Also, use the given numbered hypotheses as rewrites." - ] - , prim "goal_normalize" "[String] -> ProofScript ()" (pureVal goal_normalize) Experimental @@ -4263,6 +4237,9 @@ primitives = Map.fromList $ Current [ "Reduce the current goal to beta-normal form." ] + ------------------------------------------------------------ + -- Fundamental proof tactics + , prim "goal_intro" "String -> ProofScript Term" (pureVal goal_intro) Experimental @@ -4270,52 +4247,11 @@ primitives = Map.fromList $ , "returning the variable as a Term." ] - , prim "normalize_sequent" "ProofScript ()" - (pureVal normalize_sequent) - Experimental - [ "Normalize the current goal sequent by applying reversable" - , "sequent calculus rules. The resulting sequent will be unfocused." - ] - - ------------------------------------------------------------ - -- Premise-related proof tactics - - , prim "retain_hyps" "[Int] -> ProofScript ()" - (pureVal retain_hyps) - Experimental - [ "Remove all hypotheses from the current sequent other than the" - , " ones listed." - ] - - , prim "delete_hyps" "[Int] -> ProofScript ()" - (pureVal delete_hyps) - Experimental - [ "Remove the numbered hypotheses from the current sequent." ] - - , prim "goal_intro_hyp" "ProofScript ()" - (pureVal goal_intro_hyp) - Experimental - [ "When focused on a conclusion that represents an implication," - , "simplify the conclusion by removing the implication and" - , "introducing a new sequent hypothesis instead." - ] - - , prim "goal_intro_hyps" "Int -> ProofScript ()" - (pureVal goal_intro_hyps) - Experimental - [ "When focused on a conclusion that represents an implication," - , "simplify the conclusion by removing the implication and" - , "introducing a new sequent hypothesis instead. The argument gives" - , "how many hypotheses to introduce." - ] - - , prim "goal_revert_hyp" "Int -> ProofScript ()" - (pureVal goal_revert_hyp) + , prim "goal_apply" "Theorem -> ProofScript ()" + (pureVal goal_apply) Experimental - [ "When focused on a conclusion, weaken the focused conclusion" - , "by introducing an implication using the numbered sequent" - , "hypothesis. This is essentially the reverse of" - , "'goal_intro_hyp'." + [ "Apply an introduction rule to the current goal. Depending on the" + , "rule, this will result in zero or more new subgoals." ] , prim "goal_insert" "Theorem -> ProofScript ()" @@ -4324,34 +4260,6 @@ primitives = Map.fromList $ [ "Insert a Theorem as a new hypothesis in the current proof goal." ] - , prim "goal_insert_and_specialize" "Theorem -> [Term] -> ProofScript ()" - (pureVal goal_insert_and_specialize) - Experimental - [ "Insert a Theorem as a new hypothesis in the current proof goal," - , "after specializing some of its universal quantifiers using the" - , "given terms." - ] - - , prim "goal_specialize_hyp" "[Term] -> ProofScript ()" - (pureVal goal_specialize_hyp) - Experimental - [ "Specialize the focused local hypothesis by supplying the values" - , "for universal quantifiers. A new specialized hypothesis will be" - , "added to the sequent." - ] - - , prim "goal_apply_hyp" "Int -> ProofScript ()" - (pureVal goal_apply_hyp) - Experimental - [ "Apply the numbered local hypothesis to the focused conclusion." ] - - , prim "goal_apply" "Theorem -> ProofScript ()" - (pureVal goal_apply) - Experimental - [ "Apply an introduction rule to the current goal. Depending on the" - , "rule, this will result in zero or more new subgoals." - ] - ------------------------------------------------------------ -- Automation-related proof tactics @@ -4397,35 +4305,6 @@ primitives = Map.fromList $ , "specification setup phase." ] - ------------------------------------------------------------ - -- Focus-related proof tactics - - , prim "unfocus" "ProofScript ()" - (pureVal unfocus) - Experimental - [ "Remove any sequent focus point." ] - - , prim "focus_concl" "Int -> ProofScript ()" - (pureVal focus_concl) - Experimental - [ "Focus on the numbered conclusion within a sequent. This will" - , "fail if there are not enough conclusions." - ] - - , prim "focus_hyp" "Int -> ProofScript ()" - (pureVal focus_hyp) - Experimental - [ "Focus on the numbered hypothesis with a sequent. This will fail" - , "if there are not enough hypotheses." - ] - - , prim "print_focus" "ProofScript ()" - (pureVal print_focus) - Experimental - [ "Print just the focused part of the current goal. Prints a" - , "message without failing if there is no current focus." - ] - ------------------------------------------------------------ -- Miscellaneous proof tactics @@ -4477,18 +4356,6 @@ primitives = Map.fromList $ , "to admit this goal." ] - , prim "retain_concl" "[Int] -> ProofScript ()" - (pureVal retain_concl) - Experimental - [ "Remove all conclusions from the current sequent other than the" - , " ones listed." - ] - - , prim "delete_concl" "[Int] -> ProofScript ()" - (pureVal delete_concl) - Experimental - [ "Remove the numbered conclusions from the current sequent." ] - ------------------------------------------------------------ -- Solvers diff --git a/saw-server/src/SAWServer/SAWServer.hs b/saw-server/src/SAWServer/SAWServer.hs index d4c4484d7d..b36f9c8c46 100644 --- a/saw-server/src/SAWServer/SAWServer.hs +++ b/saw-server/src/SAWServer/SAWServer.hs @@ -361,7 +361,6 @@ initialState readFileFn = , rwPathSatSolver = CC.PathSat_Z3 , rwSkipSafetyProofs = False , rwSingleOverrideSpecialCase = False - , rwSequentGoals = False , rwJavaCodebase = JavaUninitialized } return (SAWState emptyEnv bic [] ro rw Map.empty)