Merge pull request #1315 from nano-o/hoist_ifs

add `hoist_ifs_in_goal`

intTests/test_hoist_ifs_in_goal/test.saw

@@ -0,0 +1,22 @@
+enable_experimental;
+
+let {{
+  f : Integer -> Integer
+  f x = undefined
+  g : Integer -> Integer
+  g x = undefined
+}};
+
+let prop = {{ \c x y -> f (if c then g x else g y) == if c then x else y }};
+
+l1 <- prove_print assume_unsat {{ \x -> f (g x) == x }};
+
+prove
+  (do {
+    hoist_ifs_in_goal;
+    simplify (addsimps [l1] empty_ss);
+    w4;
+  })
+  prop;
+
+print "Done";

intTests/test_hoist_ifs_in_goal/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

src/SAWScript/Builtins.hs

@@ -501,6 +501,13 @@ simplifyGoal ss =
      (_,prop') <- io (simplifyProp sc ss (goalProp goal))
      return (prop', RewriteEvidence ss)
 
+hoistIfsInGoalPrim :: ProofScript ()
+hoistIfsInGoalPrim =
+  execTactic $ tacticChange $ \goal ->
+    do sc <- getSharedContext
+       p <- io $ hoistIfsInGoal sc (goalProp goal)
+       return (p, HoistIfsEvidence)
+
 goal_eval :: [String] -> ProofScript ()
 goal_eval unints =
   execTactic $ tacticChange $ \goal ->

src/SAWScript/Interpreter.hs

@@ -1199,6 +1199,11 @@ primitives = Map.fromList
     Current
     [ "Apply the given simplifier rule set to the current goal." ]
 
+  , prim "hoist_ifs_in_goal"            "ProofScript ()"
+    (pureVal hoistIfsInGoalPrim)
+    Experimental
+    [ "hoist ifs in the current proof goal" ]
+
   , prim "goal_eval"           "ProofScript ()"
     (pureVal (goal_eval []))
     Current

src/SAWScript/Proof.hs

@@ -17,6 +17,7 @@ module SAWScript.Proof
   , splitProp
   , unfoldProp
   , simplifyProp
+  , hoistIfsInGoal
   , evalProp
   , betaReduceProp
   , falseProp
@@ -197,6 +198,21 @@ simplifyProp sc ss (Prop tm) =
   do (a, tm') <- rewriteSharedTerm sc ss tm
      return (a, Prop tm')
 
+hoistIfsInGoal :: SharedContext -> Prop -> IO Prop
+hoistIfsInGoal sc (Prop p) = do
+  let (args, body) = asPiList p
+  body' <-
+    case asEqTrue body of
+      Just t -> pure t
+      Nothing -> fail "hoistIfsInGoal: expected EqTrue"
+  ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args
+  vars <- traverse (scExtCns sc) ecs
+  t0 <- instantiateVarList sc 0 (reverse vars) body'
+  t1 <- hoistIfs sc t0
+  t2 <- scEqTrue sc t1
+  t3 <- scGeneralizeExts sc ecs t2
+  return (Prop t3)
+
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will
 --   perform a variety of simplifications and rewrites.
@@ -426,6 +442,10 @@ data Evidence
     --   evidence is use to check the modified goal.
   | EvalEvidence (Set VarIndex) Evidence
 
+    -- | This type of evidence is used to modify a goal to prove by applying
+    -- 'hoistIfsInGoal'.
+  | HoistIfsEvidence Evidence
+
 -- | The the proposition proved by a given theorem.
 thmProp :: Theorem -> Prop
 thmProp (LocalAssumption p _loc _n) = p
@@ -785,6 +805,10 @@ checkEvidence sc db = \e p -> do hyps <- Map.keysSet <$> readIORef (theoremMap d
            (d2,sy) <- check hyps e' p'
            return (Set.union d1 d2, sy)
 
+      HoistIfsEvidence e' ->
+        do p' <- hoistIfsInGoal sc p
+           check hyps e' p'
+
       EvalEvidence vars e' ->
         do p' <- evalProp sc vars p
            check hyps e' p'