Merge pull request #2429 from GaloisInc/bh/simplify-recursor

Simplify representation of recursors in saw-core terms

Author: brianhuffman

cryptol-saw-core/src/CryptolSAWCore/Cryptol.hs

@@ -2028,7 +2028,6 @@ scCryptolType sc t =
       SC.VPiType _nm _v1 (SC.VDependentPi _) -> Nothing
       SC.VStringType -> Nothing
       SC.VRecordType{} -> Nothing
-      SC.VRecursorType{} -> Nothing
       SC.VTyTerm{} -> Nothing
 
 --------------------------------------------------------------------------------

intTests/test_sawcore_type_errors/test.log.good

@@ -124,7 +124,7 @@ While typechecking term:
 Not a sort
   Prelude.Bool
 
- Motive function should return a sort
+ Not a sort (recursor)
 == Anticipated failure message ==
 Stack trace:
    (builtin) in parse_core
@@ -133,9 +133,12 @@ Stack trace:
    test.saw:4:17-4:54 in parse
    test.saw:34:1-34:59 (at top level)
 .:1:15:
-Malformed recursor
-  Prelude.Void#rec (\(_ : Prelude.Void) -> Prelude.True) ()
-Motive function should return a sort
+While typechecking term:
+  (arg : Prelude.Void)
+  -> (\(_ : Prelude.Void) -> Prelude.True) arg
+.:1:15:
+Not a sort
+  Prelude.Bool
 
  Function application with non-function type
 == Anticipated failure message ==

intTests/test_sawcore_type_errors/test.saw

@@ -30,7 +30,7 @@ parse "#(Bool, 5)";
 print "Not a sort (record type)";
 parse "#{ foo : Bool, bar : False }";
 
-print "Motive function should return a sort";
+print "Not a sort (recursor)";
 parse "\\(v : Void) -> Void#rec (\\ (_ : Void) -> True) v";
 
 print "Function application with non-function type";

saw-core-coq/src/SAWCoreCoq/Term.hs

@@ -418,21 +418,8 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
     PairRight t   ->
       Coq.App <$> pure (Coq.Var "snd") <*> traverse translateTerm [t]
 
-    RecursorType _d _params motive motiveTy ->
-      -- type of the motive looks like
-      --      (ix1 : _) -> ... -> (ixn : _) -> d ps ixs -> sort
-      -- to get the type of the recursor, we compute
-      --      (ix1 : _) -> ... -> (ixn : _) -> (x:d ps ixs) -> motive ixs x
-      let (bs, _srt) = asPiList motiveTy in
-      translateBinders bs $ \bndrs ->
-      do let varsT = map (Coq.Var . bindTransIdent) bndrs
-         let bindersT = concat $ map bindTransToPiBinder bndrs
-         motiveT <- translateTerm motive
-         let bodyT = Coq.App motiveT varsT
-         return $ Coq.Pi bindersT bodyT
-
     -- TODO: support this next!
-    Recursor (CompiledRecursor d parameters motive _motiveTy eliminators elimOrder) ->
+    Recursor (CompiledRecursor d parameters _nixs motive _motiveTy eliminators elimOrder _ty) ->
       do maybe_d_trans <-
            case nameInfo d of
              ModuleIdentifier ident -> translateIdentToIdent ident
@@ -455,11 +442,6 @@ flatTermFToExpr tf = -- traceFTermF "flatTermFToExpr" tf $
 
          pure (Coq.App rect_var (ps ++ [m] ++ elimlist))
 
-    RecursorApp r indices termEliminated ->
-      do r' <- translateTerm r
-         let args = indices ++ [termEliminated]
-         Coq.App r' <$> mapM translateTerm args
-
     Sort s _h -> pure (Coq.Sort (translateSort s))
     NatLit i -> pure (Coq.NatLit (toInteger i))
     ArrayValue (asBoolType -> Just ()) (traverse asBool -> Just bits)

saw-core-what4/src/SAWCoreWhat4/What4.hs

@@ -1471,8 +1471,6 @@ rebuildTerm sym st sc tv sv =
       scString sc s
     VRecordValue _ ->
       chokeOn "records (VRecordValue)"
-    VRecursor {} ->
-      chokeOn "recursors (VRecursor)"
     VExtra _ ->
       chokeOn "VExtra"
     TValue _tval ->

saw-core/src/SAWCore/ExternalFormat.hs

@@ -48,11 +48,6 @@ separateArgs args =
     Just i -> Just (take i args, drop (i+1) args)
     Nothing -> Nothing
 
--- | Split the last element from the rest of a list, for non-empty lists
-splitLast :: [a] -> Maybe ([a], a)
-splitLast [] = Nothing
-splitLast xs = Just (take (length xs - 1) xs, last xs)
-
 type WriteM = State.State (Map TermIndex Int, Map VarIndex (Either Text NameInfo), [String], Int)
 
 renderNames :: Map VarIndex (Either Text NameInfo) -> String
@@ -148,25 +143,17 @@ scWriteExternal t0 =
             PairLeft e          -> pure $ unwords ["ProjL", show e]
             PairRight e         -> pure $ unwords ["ProjR", show e]
 
-            RecursorType d ps motive motive_ty ->
-              do stashName d
-                 pure $ unwords
-                     (["RecursorType", show (nameIndex d)] ++
-                      map show ps ++
-                      [argsep, show motive, show motive_ty])
-            Recursor (CompiledRecursor d ps motive motive_ty cs_fs ctorOrder) ->
+            Recursor (CompiledRecursor d ps nixs motive motive_ty cs_fs ctorOrder ty) ->
               do stashName d
                  mapM_ stashName ctorOrder
                  pure $ unwords
-                      (["Recursor" , show (nameIndex d)] ++
+                      (["Recursor" , show (nameIndex d), show nixs] ++
                        map show ps ++
                        [ argsep, show motive, show motive_ty
                        , show (Map.toList cs_fs)
                        , show (map nameIndex ctorOrder)
+                       , show ty
                        ])
-            RecursorApp r ixs e -> pure $
-              unwords (["RecursorApp", show r] ++
-                       map show ixs ++ [show e])
 
             RecordType elem_tps -> pure $ unwords ["RecordType", show elem_tps]
             RecordValue elems   -> pure $ unwords ["Record", show elems]
@@ -300,32 +287,19 @@ scReadExternal sc input =
         ["ProjL", x]        -> FTermF <$> (PairLeft <$> readIdx x)
         ["ProjR", x]        -> FTermF <$> (PairRight <$> readIdx x)
 
-        ("RecursorType" : i :
-         (separateArgs ->
-          Just (ps, [motive,motive_ty]))) ->
-            do tp <- RecursorType <$>
-                       readName i <*>
-                       traverse readIdx ps <*>
-                       readIdx motive <*>
-                       readIdx motive_ty
-               pure (FTermF tp)
-        ("Recursor" : i :
+        ("Recursor" : i : nixs :
          (separateArgs ->
-          Just (ps, [motive, motiveTy, elims, ctorOrder]))) ->
-            do rec <- CompiledRecursor <$>
+          Just (ps, [motive, motiveTy, elims, ctorOrder, ty]))) ->
+            do crec <- CompiledRecursor <$>
                         readName i <*>
                         traverse readIdx ps <*>
+                        pure (read nixs) <*>
                         readIdx motive <*>
                         readIdx motiveTy <*>
                         readElimsMap elims <*>
-                        readCtorList ctorOrder
-               pure (FTermF (Recursor rec))
-        ("RecursorApp" : r : (splitLast -> Just (ixs, arg))) ->
-            do app <- RecursorApp <$>
-                        readIdx r <*>
-                        traverse readIdx ixs <*>
-                        readIdx arg
-               pure (FTermF app)
+                        readCtorList ctorOrder <*>
+                        readIdx ty
+               pure (FTermF (Recursor crec))
 
         ["RecordType", elem_tps] ->
           FTermF <$> (RecordType <$> (traverse (traverse getTerm) =<< readM elem_tps))

saw-core/src/SAWCore/Recognizer.hs

@@ -38,7 +38,6 @@ module SAWCore.Recognizer
   , asRecordValue
   , asRecordSelector
   , asRecursorApp
-  , asRecursorType
   , asNat
   , asBvNat
   , asUnsignedConcreteBv
@@ -249,16 +248,10 @@ asRecordSelector t = do
   RecordProj u s <- asFTermF t
   return (u, s)
 
-asRecursorType :: Recognizer Term (Name, [Term], Term, Term)
-asRecursorType t =
-  do RecursorType d ps motive motive_ty <- asFTermF t
-     return (d,ps,motive,motive_ty)
-
-asRecursorApp :: Recognizer Term (Term, CompiledRecursor Term, [Term], Term)
+asRecursorApp :: Recognizer Term (Term, CompiledRecursor Term)
 asRecursorApp t =
-  do RecursorApp rc ixs arg <- asFTermF t
-     Recursor crec <- asFTermF rc
-     return (rc, crec, ixs, arg)
+  do Recursor crec <- asFTermF t
+     pure (t, crec)
 
 asNat :: Recognizer Term Natural
 asNat (unwrapTermF -> FTermF (NatLit i)) = pure i

saw-core/src/SAWCore/Rewriter.hs

@@ -481,7 +481,8 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
                   return (mkRewriteRule ctxt l x shallow ann)
          Just <$> traverse mkRule (Map.assocs m)
     (R.asApplyAll ->
-     (R.asRecursorApp -> Just (rec, crec, _ixs, R.asVariable -> Just ec), more))
+     (R.asRecursorApp -> Just (r, crec),
+      splitAt (recursorNumIxs crec) -> (_ixs, (R.asVariable -> Just ec) : more)))
       | (ctxt1, _ : ctxt2) <- break (== ec) ctxt ->
       do -- ti is the type of the value being scrutinized
          ti <- scWhnf sc (ecType ec)
@@ -505,11 +506,11 @@ scExpandRewriteRule sc (RewriteRule ctxt lhs rhs _ shallow ann) =
                   -- new lhs and rhs in context @ctxt'@.
                   lhs' <- adjust lhs
 
-                  rec'  <- adjust rec
+                  r'  <- adjust r
                   crec' <- traverse adjust crec
                   more' <- traverse adjust more
 
-                  rhs1 <- scReduceRecursor sc rec' crec' (ctorName ctor) args
+                  rhs1 <- scReduceRecursor sc r' crec' (ctorName ctor) args
                   rhs2 <- scApplyAll sc rhs1 more'
                   rhs3 <- betaReduce rhs2
                   -- re-fold recursive occurrences of the original rhs
@@ -641,9 +642,10 @@ asRecordRedex t =
 --   > RecursorApp rec _ n
 asNatIotaRedex :: R.Recognizer Term (Term, CompiledRecursor Term, Natural)
 asNatIotaRedex t =
-  do (rec, crec, _, arg) <- R.asRecursorApp t
+  do (f, arg) <- R.asApp t
+     (r, crec) <- R.asRecursorApp f
      n <- R.asNat arg
-     return (rec, crec, n)
+     return (r, crec, n)
 
 ----------------------------------------------------------------------
 -- Bottom-up rewriting
@@ -693,17 +695,18 @@ reduceSharedTerm :: SharedContext -> Term -> IO (Maybe Term)
 reduceSharedTerm sc (asBetaRedex -> Just (_, _, body, arg)) = Just <$> instantiateVar sc 0 arg body
 reduceSharedTerm _ (asPairRedex -> Just t) = pure (Just t)
 reduceSharedTerm _ (asRecordRedex -> Just t) = pure (Just t)
-reduceSharedTerm sc (asNatIotaRedex -> Just (rec, crec, n)) =
-  Just <$> scReduceNatRecursor sc rec crec n
-reduceSharedTerm sc (R.asRecursorApp -> Just (rec, crec, _, arg)) =
+reduceSharedTerm sc (asNatIotaRedex -> Just (r, crec, n)) =
+  Just <$> scReduceNatRecursor sc r crec n
+reduceSharedTerm sc (R.asApp -> Just (R.asApplyAll -> (R.asRecursorApp -> Just (r, crec), ixs), arg))
+  | recursorNumIxs crec == length ixs =
   do let (f, args) = R.asApplyAll arg
      mm <- scGetModuleMap sc
      case R.asConstant f of
        Nothing -> pure Nothing
        Just c ->
          case lookupVarIndexInMap (nameIndex c) mm of
            Just (ResolvedCtor ctor) ->
-             Just <$> scReduceRecursor sc rec crec c (drop (ctorNumParams ctor) args)
+             Just <$> scReduceRecursor sc r crec c (drop (ctorNumParams ctor) args)
            _ -> pure Nothing
 reduceSharedTerm _ _ = pure Nothing
 
@@ -833,9 +836,7 @@ rewriteSharedTermTypeSafe sc ss t0 =
           -- NOTE: we don't rewrite arguments of constructors, datatypes, or
           -- recursors because of dependent types, as we could potentially cause
           -- a term to become ill-typed
-          RecursorType{}   -> return ftf
           Recursor{}       -> return ftf
-          RecursorApp{}    -> return ftf -- could treat same as CtorApp
 
           RecordType{}     -> traverse rewriteAll ftf
           RecordValue{}    -> traverse rewriteAll ftf