Add unfolding_fix_once. (#2008)

* Add unfolding_fix_once.

* Address comments.

* Address comments.

intTests/test_unfold_fix_once/test.saw

@@ -0,0 +1,12 @@
+let {{
+  f : [64] -> [64]
+  f x = if x <$ 0 then 0 else 2 * (f (x + 1))
+}};
+
+prove_print
+  (do {
+    unfolding_fix_once ["f"];
+    w4_unint_z3 ["f"];
+  })
+  {{ \x -> (f x) % 2 == 0 }};
+

intTests/test_unfold_fix_once/test.sh

@@ -0,0 +1,4 @@
+set -e
+
+$SAW test.saw
+

saw-core/src/Verifier/SAW/SharedTerm.hs

@@ -270,6 +270,7 @@ module Verifier.SAW.SharedTerm
   , scUnfoldConstants'
   , scUnfoldConstantSet
   , scUnfoldConstantSet'
+  , scUnfoldOnceFixConstantSet
   , scSharedSize
   , scSharedSizeAux
   , scSharedSizeMany
@@ -2622,6 +2623,34 @@ scUnfoldConstantSet sc b names t0 = do
           _ -> scTermF sc =<< traverse go tf
   go t0
 
+-- | Unfold one time fixpoint constants.
+--
+-- Specifically, if @c = fix a f@, then replace @c@ with @f c@, that is replace
+-- @(fix a f)@ with @f (fix a f)@ while preserving the constant name.  The
+-- signature of @fix@ is @primitive fix : (a : sort 1) -> (a -> a) -> a;@.
+scUnfoldOnceFixConstantSet :: SharedContext
+                           -> Bool  -- ^ True: unfold constants in set. False: unfold constants NOT in set
+                           -> Set VarIndex -- ^ Set of constant names
+                           -> Term
+                           -> IO Term
+scUnfoldOnceFixConstantSet sc b names t0 = do
+  cache <- newCache
+  let unfold t idx rhs
+        | Set.member idx names == b
+        , (isGlobalDef "Prelude.fix" -> Just (), [_, f]) <- asApplyAll rhs =
+          betaNormalize sc =<< scApply sc f t
+        | otherwise =
+          return t
+  let go :: Term -> IO Term
+      go t@(Unshared tf) =
+        case tf of
+          Constant (EC idx _ _) (Just rhs) -> unfold t idx rhs
+          _ -> Unshared <$> traverse go tf
+      go t@(STApp{ stAppIndex = idx, stAppTermF = tf }) = useCache cache idx $
+        case tf of
+          Constant (EC ecidx _ _) (Just rhs) -> unfold t ecidx rhs
+          _ -> scTermF sc =<< traverse go tf
+  go t0
 
 -- | TODO: test whether this version is slower or faster.
 scUnfoldConstantSet' :: SharedContext

src/SAWScript/Builtins.hs

@@ -672,6 +672,14 @@ unfoldGoal unints =
      sqt' <- traverseSequentWithFocus (io . unfoldProp sc unints') (goalSequent goal)
      return (sqt', UnfoldEvidence unints')
 
+unfoldFixOnceGoal :: [String] -> ProofScript ()
+unfoldFixOnceGoal unints =
+  execTactic $ tacticChange $ \goal ->
+  do sc <- getSharedContext
+     unints' <- resolveNames unints
+     sqt' <- traverseSequentWithFocus (io . unfoldFixOnceProp sc unints') (goalSequent goal)
+     return (sqt', UnfoldFixOnceEvidence unints')
+
 simplifyGoal :: SV.SAWSimpset -> ProofScript ()
 simplifyGoal ss =
   execTactic $ tacticChange $ \goal ->

src/SAWScript/Interpreter.hs

@@ -1732,6 +1732,14 @@ primitives = Map.fromList
     Current
     [ "Unfold the named subterm(s) within the current goal." ]
 
+  , prim "unfolding_fix_once" "[String] -> ProofScript ()"
+    (pureVal unfoldFixOnceGoal)
+    Current
+    [ "Unfold the named recursive constants once within the current goal."
+    , "Like `unfolding`, except that the recursive constants are unfolded"
+    , "only once, avoiding possible infinite evaluation."
+    ]
+
   , prim "simplify"            "Simpset -> ProofScript ()"
     (pureVal simplifyGoal)
     Current

src/SAWScript/Proof.hs

@@ -18,6 +18,7 @@ module SAWScript.Proof
   , splitConj
   , splitDisj
   , unfoldProp
+  , unfoldFixOnceProp
   , simplifyProp
   , hoistIfsInProp
   , evalProp
@@ -378,6 +379,13 @@ unfoldProp sc unints (Prop tm) =
   do tm' <- scUnfoldConstantSet sc True unints tm
      return (Prop tm')
 
+-- | Unfold one time all the fixpoint constants appearing in the proposition
+-- whose VarIndex is found in the given set.
+unfoldFixOnceProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop
+unfoldFixOnceProp sc unints (Prop tm) =
+  do tm' <- scUnfoldOnceFixConstantSet sc True unints tm
+     return (Prop tm')
+
 -- | Rewrite the proposition using the provided Simpset
 simplifyProp :: Ord a => SharedContext -> Simpset a -> Prop -> IO (Set a, Prop)
 simplifyProp sc ss (Prop tm) =
@@ -1040,6 +1048,12 @@ data Evidence
     --   evidence is used to check the modified sequent.
   | 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.
+  | 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
@@ -1649,6 +1663,10 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc
         do sqt' <- traverseSequentWithFocus (unfoldProp sc vars) sqt
            check nenv e' sqt'
 
+      UnfoldFixOnceEvidence vars e' ->
+        do sqt' <- traverseSequentWithFocus (unfoldFixOnceProp sc vars) sqt
+           check nenv e' sqt'
+
       NormalizePropEvidence opqueSet e' ->
         do modmap <- scGetModuleMap sc
            sqt' <- traverseSequentWithFocus (normalizeProp sc modmap opqueSet) sqt