Unfold bare Cryptol properties when interpreting them as rewrite rules

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1213,6 +1213,20 @@ cryptolURI (p:ps) (Just uniq) =
        , uriFragment = Just frag
        }
 
+-- | Tests if the given 'NameInfo' represents a name imported
+--   from Cryptol. If so, return the unqualified identifier
+--   associated with that 'NameInfo'.
+isCryptolName :: NameInfo -> Maybe Text
+isCryptolName (ImportedName uri _)
+  | Just sch <- uriScheme uri
+  , unRText sch == "cryptol"
+  , Left True <- uriAuthority uri
+  , Just (False, x :| xs) <- uriPath uri
+  , [] <- uriQuery uri
+  , Nothing <- uriFragment uri
+  = Just (unRText (last (x:xs)))
+isCryptolName _ = Nothing
+
 -- | Tests if the given 'NameInfo' represents a name imported
 --   from the given Cryptol module name.  If so, it returns
 --   the identifier within that module.  Note, this does

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

@@ -30,6 +30,7 @@ module Verifier.SAW.Rewriter
   , ruleOfTerm
   , ruleOfTerms
   , ruleOfProp
+  , unfoldableTerm
   , scDefRewriteRules
   , scEqsRewriteRules
   , scEqRewriteRule
@@ -395,6 +396,27 @@ scEqRewriteRule sc i = ruleOfTerm <$> scTypeOfGlobal sc i <*> pure Nothing
 scEqsRewriteRules :: SharedContext -> [Ident] -> IO [RewriteRule a]
 scEqsRewriteRules sc = mapM (scEqRewriteRule sc)
 
+-- | Finds the first named constant in the term that may be amenable to
+-- unfolding
+unfoldableTerm :: Term -> Either NameInfo ()
+unfoldableTerm t
+  | Just _ <- R.asFTermF t =
+    Right ()
+  | Just _ <- R.asLocalVar t =
+    Right ()
+  | Just (EC _ nmi _, Just _body) <- R.asConstant t =
+    -- is matching (Just _body) too strict?
+    Left nmi
+  | Just (_, _, body) <- R.asLambda t =
+    unfoldableTerm body
+  | Just (_, _, body) <- R.asPi t =
+    unfoldableTerm body
+  | Just body <- R.asEqTrue t =
+    unfoldableTerm body
+  | Just (f, x) <- R.asApp t =
+    unfoldableTerm f >> unfoldableTerm x
+  | otherwise = Right ()
+
 -- | Transform the given rewrite rule to a set of one or more
 -- equivalent rewrite rules, if possible.
 --

src/SAWScript/Builtins.hs

@@ -1523,19 +1523,29 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
+addSimpWith :: (forall a. RewriteRule a -> RewriteRule a) -> Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
+addSimpWith f thm ss =
+  do  sc <- getSharedContext
+      mkRule sc (thmProp thm)
+  where
+    mkRule sc prop =
+      io (propToRewriteRule sc prop (Just (thmNonce thm))) >>= \case
+        Right Nothing -> fail "addsimp: cannot interpret theorem as equation"
+        Right (Just rule) -> pure (addRule (f rule) ss)
+        Left nmi ->
+          case Cryptol.isCryptolName nmi of
+            Nothing -> fail "addsimp: cannot unfold a non-cryptol term"
+            Just name ->
+              do  idx <- resolveName sc (Text.unpack name)
+                  prop' <- io $ unfoldProp sc (Set.fromList idx) prop
+                  prop'' <- io $ betaReduceProp sc prop'
+                  mkRule sc prop''
+
 addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp thm ss =
-  do sc <- getSharedContext
-     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
-       Nothing -> fail "addsimp: theorem not an equation"
-       Just rule -> pure (addRule rule ss)
+addsimp = addSimpWith id
 
 addsimp_shallow :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
-addsimp_shallow thm ss =
-  do sc <- getSharedContext
-     io (propToRewriteRule sc (thmProp thm) (Just (thmNonce thm))) >>= \case
-       Nothing -> fail "addsimp: theorem not an equation"
-       Just rule -> pure (addRule (shallowRule rule) ss)
+addsimp_shallow = addSimpWith shallowRule
 
 -- TODO: remove this, it implicitly adds axioms
 addsimp' :: Term -> SV.SAWSimpset -> TopLevel SV.SAWSimpset

src/SAWScript/Proof.hs

@@ -224,12 +224,16 @@ boolToProp sc vars tm =
 propToTerm :: SharedContext -> Prop -> IO Term
 propToTerm _sc (Prop tm) = pure tm
 
--- | Attempt to interpret a proposition as a rewrite rule.
-propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Maybe (RewriteRule a))
+-- | Attempt to interpret a proposition as a rewrite rule. If interpretation
+-- fails, check if a (sub)term can be unfolded.
+propToRewriteRule :: SharedContext -> Prop -> Maybe a -> IO (Either NameInfo (Maybe (RewriteRule a)))
 propToRewriteRule _sc (Prop tm) ann =
   case ruleOfProp tm ann of
-    Nothing -> pure Nothing
-    Just r  -> pure (Just r)
+    Just r  -> pure (Right (Just r))
+    Nothing ->
+      case unfoldableTerm tm of
+        Left nmi -> pure (Left nmi)
+        Right () -> pure (Right Nothing)
 
 -- | Attempt to split an if/then/else proposition.
 --   If it succeeds to find a term like "EqTrue (ite Bool b x y)",
@@ -397,6 +401,7 @@ localHypSimpset sqt hs ss0 = Fold.foldlM processHyp ss0 nhyps
     processHyp ss (n,h) =
       case ruleOfProp (unProp h) Nothing of
         Nothing -> fail $ "Hypothesis " ++ show n ++ "cannot be used as a rewrite rule."
+        -- check `unfoldableTerm`?
         Just r  -> return (addRule r ss)
 
     nhyps = [ (n,h)