Add some additional ways to construct terms; in particular,

we can now construct integer and natural number terms directly
from SAWCore `Int` values, or `TCNum` values from Cryptol
sizes. In addition, there is now a `term_apply` operation which
will construct application terms.

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

@@ -23,6 +23,7 @@ import Verifier.SAW.Cryptol (scCryptolType)
 import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer (asExtCns)
 import Verifier.SAW.SharedTerm
+import Verifier.SAW.SCTypeCheck (scTypeCheckError)
 
 -- Typed terms -----------------------------------------------------------------
 
@@ -67,22 +68,35 @@ mkTypedTerm sc trm = do
         Just (Right t) -> TypedTermSchema (C.tMono t)
   return (TypedTerm ttt trm)
 
--- | Apply a function-typed 'TypedTerm' to an argument. This operation
--- fails if the first 'TypedTerm' does not have a monomorphic function
--- type.
+-- | Apply a function-typed 'TypedTerm' to an argument.
+--   This operation fails if the type of the argument does
+--   not match the function.
 applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm
-applyTypedTerm sc (TypedTerm tp t1) (TypedTerm _ t2)
-  | Just (_,cty') <- C.tIsFun =<< ttIsMono tp
-  = TypedTerm (TypedTermSchema (C.tMono cty')) <$> scApply sc t1 t2
-
--- TODO? extend this to allow explicit application of types?
-applyTypedTerm _ _ _ = fail "applyTypedTerm: not a (monomorphic) function type"
+applyTypedTerm sc (TypedTerm _tp t1) (TypedTerm _ t2) =
+  do trm <- scApply sc t1 t2
+     ty <- scTypeCheckError sc trm
+     ct <- scCryptolType sc ty
+     let ttt = case ct of
+           Nothing        -> TypedTermOther ty
+           Just (Left k)  -> TypedTermKind k
+           Just (Right t) -> TypedTermSchema (C.tMono t)
+     return (TypedTerm ttt trm)
 
 -- | Apply a 'TypedTerm' to a list of arguments. This operation fails
 -- if the first 'TypedTerm' does not have a function type of
--- sufficient arity.
+-- sufficient arity, or if the types of the arguments do not match
+-- the type of the function.
 applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
-applyTypedTerms sc = foldM (applyTypedTerm sc)
+applyTypedTerms sc (TypedTerm _ fn) args =
+  do trm <- foldM (scApply sc) fn (map ttTerm args)
+     ty <- scTypeCheckError sc trm
+     ct <- scCryptolType sc ty
+     let ttt = case ct of
+           Nothing        -> TypedTermOther ty
+           Just (Left k)  -> TypedTermKind k
+           Just (Right t) -> TypedTermSchema (C.tMono t)
+     return (TypedTerm ttt trm)
+
 
 -- | Create an abstract defined constant with the specified name and body.
 defineTypedTerm :: SharedContext -> Text -> TypedTerm -> IO TypedTerm

src/SAWScript/Builtins.hs

@@ -1246,6 +1246,11 @@ abstractSymbolicPrim (TypedTerm _ t) = do
 bindAllExts :: SharedContext -> Term -> IO Term
 bindAllExts sc body = scAbstractExts sc (getAllExts body) body
 
+term_apply :: TypedTerm -> [TypedTerm] -> TopLevel TypedTerm
+term_apply fn args =
+  do sc <- getSharedContext
+     io $ applyTypedTerms sc fn args
+
 lambda :: TypedTerm -> TypedTerm -> TopLevel TypedTerm
 lambda x = lambdas [x]
 
@@ -1509,6 +1514,44 @@ eval_size s =
         Right _        -> fail "eval_size: not a numeric type"
     _ -> fail "eval_size: unsupported polymorphic type"
 
+int_to_term :: Int -> TopLevel TypedTerm
+int_to_term i
+  | i < 0 =
+     do sc  <- getSharedContext
+        tm  <- io (scNat sc (fromInteger (negate (toInteger i))))
+        tm' <- io (scIntNeg sc =<< scNatToInt sc tm)
+        io (mkTypedTerm sc tm')
+  | otherwise =
+     do sc  <- getSharedContext
+        tm  <- io (scNat sc (fromIntegral i))
+        tm' <- io (scNatToInt sc tm)
+        io (mkTypedTerm sc tm')
+
+nat_to_term :: Int -> TopLevel TypedTerm
+nat_to_term i
+  | i >= 0 =
+      do sc <- getSharedContext
+         tm <- io $ scNat sc (fromIntegral i)
+         io $ mkTypedTerm sc tm
+
+  | otherwise =
+      fail ("nat_to_term: negative value " ++ show i)
+
+
+size_to_term :: C.Schema -> TopLevel TypedTerm
+size_to_term s =
+  do sc <- getSharedContext
+     tm <- io $ case s of
+                  C.Forall [] [] t ->
+                    case C.evalType mempty t of
+                      Left (C.Nat x) | x >= 0 ->
+                        scCtorApp sc "Cryptol.TCNum" =<< sequence [scNat sc (fromInteger x)]
+                      Left C.Inf -> scCtorApp sc "Cryptol.TCInf" []
+                      _ -> fail "size_to_term: not a numeric type"
+                  _ -> fail "size_to_term: unsupported polymorphic type"
+
+     return (TypedTerm (TypedTermKind C.KNum) tm)
+
 nthPrim :: [a] -> Int -> TopLevel a
 nthPrim [] _ = fail "nth: index too large"
 nthPrim (x : _) 0 = return x

src/SAWScript/Interpreter.hs

@@ -1075,6 +1075,13 @@ primitives = Map.fromList
     , "is used only for pretty-printing."
     ]
 
+  , prim "term_apply"          "Term -> [Term] -> Term"
+    (funVal2 term_apply)
+    Current
+    [ "Build a term application node that applies the first term"
+    , "(which much be a term representing a function) to given list of arguments."
+    ]
+
   , prim "lambda"              "Term -> Term -> Term"
     (funVal2 lambda)
     Current
@@ -1090,6 +1097,22 @@ primitives = Map.fromList
     , "variables."
     ]
 
+  , prim "size_to_term"      "Type -> Term"
+    (funVal1 size_to_term)
+    Current
+    [ "Convert a Cryptol size type into a Term representation."
+    ]
+
+  , prim "int_to_term"      "Int -> Term"
+    (funVal1 int_to_term)
+    Current
+    [ "Convert a concrete integer value into an integer term." ]
+
+  , prim "nat_to_term"      "Int -> Term"
+    (funVal1 nat_to_term)
+    Current
+    [ "Convert a non-negative integer value into a natural number term." ]
+
   , prim "term_theories" "[String] -> Term -> [String]"
     (funVal2 term_theories)
     Experimental