From 113d241b3171a857e4d87670c64f6d5fd4960869 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 11 Aug 2020 10:38:36 -0700
Subject: [PATCH 1/7] Turn comments into haddock comments.

---
 cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index 7d971de031..5713154d58 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -19,9 +19,10 @@ import Verifier.SAW.SharedTerm
 
 -- Typed terms -----------------------------------------------------------------
 
-{- Within SAWScript, we represent an object language term as a SAWCore
-shared term paired with a Cryptol type schema. The Cryptol type is
-used for type inference/checking of inline Cryptol expressions. -}
+-- | Within SAWScript, we represent an object language term as a
+-- SAWCore shared term paired with a Cryptol type schema. The Cryptol
+-- type is used for type inference/checking of inline Cryptol
+-- expressions.
 
 data TypedTerm =
   TypedTerm
@@ -41,9 +42,9 @@ mkTypedTerm sc trm = do
 
 -- Typed modules ---------------------------------------------------------------
 
-{- In SAWScript, we can refer to a Cryptol module as a first class
-value. These are represented simply as maps from names to typed
-terms. -}
+-- | In SAWScript, we can refer to a Cryptol module as a first class
+-- value. These are represented simply as maps from names to typed
+-- terms.
 
 data CryptolModule =
   CryptolModule (Map C.Name C.TySyn) (Map C.Name TypedTerm)

From 1af493e7b89d5aefb8a8647d1d71de052cc97f50 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 11 Aug 2020 10:39:16 -0700
Subject: [PATCH 2/7] Add `TypedExtCns` datatype and `abstractTypedExts`
 function.

---
 .../src/Verifier/SAW/TypedTerm.hs             | 26 +++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index 5713154d58..81f5cab30e 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -15,6 +15,7 @@ import qualified Cryptol.TypeCheck.AST as C
 import Cryptol.Utils.PP (pretty)
 
 import Verifier.SAW.Cryptol (scCryptolType)
+import Verifier.SAW.Recognizer (asExtCns)
 import Verifier.SAW.SharedTerm
 
 -- Typed terms -----------------------------------------------------------------
@@ -34,12 +35,37 @@ data TypedTerm =
 ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm
 ttTermLens f tt = tt `seq` fmap (\x -> tt{ttTerm = x}) (f (ttTerm tt))
 
+-- | Deprecated.
 mkTypedTerm :: SharedContext -> Term -> IO TypedTerm
 mkTypedTerm sc trm = do
   ty <- scTypeOf sc trm
   ct <- scCryptolType sc ty
   return $ TypedTerm (C.Forall [] [] ct) trm
 
+-- Typed external constants ----------------------------------------------------
+
+data TypedExtCns =
+  TypedExtCns
+  { tecType :: C.Type
+  , tecExt :: ExtCns Term
+  }
+  deriving Show
+
+-- | Recognize 'TypedTerm's that are external constants.
+asTypedExtCns :: TypedTerm -> Maybe TypedExtCns
+asTypedExtCns (TypedTerm schema t) =
+  do cty <- C.isMono schema
+     ec <- asExtCns t
+     pure $ TypedExtCns cty ec
+
+abstractTypedExts :: SharedContext -> [TypedExtCns] -> TypedTerm -> IO TypedTerm
+abstractTypedExts sc tecs (TypedTerm (C.Forall params props ty) trm) =
+  do let tys = map tecType tecs
+     let exts = map tecExt tecs
+     let ty' = foldr C.tFun ty tys
+     trm' <- scAbstractExts sc exts trm
+     pure $ TypedTerm (C.Forall params props ty') trm'
+
 -- Typed modules ---------------------------------------------------------------
 
 -- | In SAWScript, we can refer to a Cryptol module as a first class

From b263cd7bf579687b506d266528cd3c149031af4d Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Wed, 19 Aug 2020 11:47:43 -0700
Subject: [PATCH 3/7] Add functions for making `TypedTerm`s from
 `FirstOrderValue`s.

---
 .../src/Verifier/SAW/TypedTerm.hs             | 29 +++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index 81f5cab30e..ea346a94d3 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -13,8 +13,11 @@ import qualified Data.Map as Map
 import Cryptol.ModuleSystem.Name (nameIdent)
 import qualified Cryptol.TypeCheck.AST as C
 import Cryptol.Utils.PP (pretty)
+import qualified Cryptol.Utils.Ident as C (packIdent)
+import qualified Cryptol.Utils.RecordMap as C (recordFromFields)
 
 import Verifier.SAW.Cryptol (scCryptolType)
+import Verifier.SAW.FiniteValue
 import Verifier.SAW.Recognizer (asExtCns)
 import Verifier.SAW.SharedTerm
 
@@ -42,6 +45,32 @@ mkTypedTerm sc trm = do
   ct <- scCryptolType sc ty
   return $ TypedTerm (C.Forall [] [] ct) trm
 
+-- First order types and values ------------------------------------------------
+
+cryptolTypeOfFirstOrderType :: FirstOrderType -> C.Type
+cryptolTypeOfFirstOrderType fot =
+  case fot of
+    FOTBit -> C.tBit
+    FOTInt -> C.tInteger
+    FOTVec n t -> C.tSeq (C.tNum n) (cryptolTypeOfFirstOrderType t)
+    FOTTuple ts -> C.tTuple (map cryptolTypeOfFirstOrderType ts)
+    FOTArray a b ->
+      C.tArray
+      (cryptolTypeOfFirstOrderType a)
+      (cryptolTypeOfFirstOrderType b)
+    FOTRec m ->
+      C.tRec $
+      C.recordFromFields $
+      [ (C.packIdent l, cryptolTypeOfFirstOrderType t)
+      | (l, t) <- Map.assocs m ]
+
+typedTermOfFirstOrderValue :: SharedContext -> FirstOrderValue -> IO TypedTerm
+typedTermOfFirstOrderValue sc fov =
+  do let fot = firstOrderTypeOf fov
+     let cty = cryptolTypeOfFirstOrderType fot
+     t <- scFirstOrderValue sc fov
+     pure $ TypedTerm (C.tMono cty) t
+
 -- Typed external constants ----------------------------------------------------
 
 data TypedExtCns =

From e8e0ea856b498ad3dbf94cbdf9742a7eee03f884 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 20 Aug 2020 10:01:00 -0700
Subject: [PATCH 4/7] Document `scCryptolType` and `scCryptolEq` as deprecated.

---
 cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
index d110232051..ccfd0d5246 100644
--- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1391,6 +1391,7 @@ asCryptolTypeValue v =
           return (C.tFun t1 t2)
     _ -> Nothing
 
+-- | Deprecated.
 scCryptolType :: SharedContext -> Term -> IO C.Type
 scCryptolType sc t =
   do modmap <- scGetModuleMap sc
@@ -1398,6 +1399,7 @@ scCryptolType sc t =
        Just ty -> return ty
        Nothing -> panic "scCryptolType" ["scCryptolType: unsupported type " ++ showTerm t]
 
+-- | Deprecated.
 scCryptolEq :: SharedContext -> Term -> Term -> IO Term
 scCryptolEq sc x y =
   do rules <- concat <$> traverse defRewrites (defs1 ++ defs2)

From 593cd3eaec199fa60c8662b22be790f8a25ddbdd Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 20 Aug 2020 10:01:27 -0700
Subject: [PATCH 5/7] Add function `scExtCns` to SharedTerm library.

---
 saw-core/src/Verifier/SAW/SharedTerm.hs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs
index d02d7aefd5..63aaf775bb 100644
--- a/saw-core/src/Verifier/SAW/SharedTerm.hs
+++ b/saw-core/src/Verifier/SAW/SharedTerm.hs
@@ -54,6 +54,7 @@ module Verifier.SAW.SharedTerm
   , scDefTerm
   , scFreshGlobalVar
   , scFreshGlobal
+  , scExtCns
   , scGlobalDef
     -- ** Recursors and datatypes
   , scRecursorElimTypes
@@ -308,11 +309,15 @@ data SharedContext = SharedContext
 scFlatTermF :: SharedContext -> FlatTermF Term -> IO Term
 scFlatTermF sc ftf = scTermF sc (FTermF ftf)
 
+-- | Create a 'Term' from an 'ExtCns'.
+scExtCns :: SharedContext -> ExtCns Term -> IO Term
+scExtCns sc ec = scFlatTermF sc (ExtCns ec)
+
 -- | Create a global variable with the given identifier (which may be "_") and type.
 scFreshGlobal :: SharedContext -> String -> Term -> IO Term
 scFreshGlobal sc sym tp = do
   i <- scFreshGlobalVar sc
-  scFlatTermF sc (ExtCns (EC i sym tp))
+  scExtCns sc (EC i sym tp)
 
 -- | Returns shared term associated with ident.
 -- Does not check module namespace.

From b4d14e3b106c8e46d2c5a294fa4b191bca26aa20 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 20 Aug 2020 10:02:32 -0700
Subject: [PATCH 6/7] Add function `typedTermOfExtCns`.

---
 cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index ea346a94d3..24e68c47a0 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -87,6 +87,11 @@ asTypedExtCns (TypedTerm schema t) =
      ec <- asExtCns t
      pure $ TypedExtCns cty ec
 
+-- | Make a 'TypedTerm' from a 'TypedExtCns'.
+typedTermOfExtCns :: SharedContext -> TypedExtCns -> IO TypedTerm
+typedTermOfExtCns sc (TypedExtCns cty ec) =
+  TypedTerm (C.tMono cty) <$> scExtCns sc ec
+
 abstractTypedExts :: SharedContext -> [TypedExtCns] -> TypedTerm -> IO TypedTerm
 abstractTypedExts sc tecs (TypedTerm (C.Forall params props ty) trm) =
   do let tys = map tecType tecs

From 0fe4d004617554130c86896cb035a452729af0e3 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 20 Aug 2020 10:03:54 -0700
Subject: [PATCH 7/7] Add several new operations on `TypedTerm`s.

* applyTypedTerm
* applyTypedTerms
* defineTypedTerm
* tupleTypedTerm
* destTupleTypedTerm
---
 .../src/Verifier/SAW/TypedTerm.hs             | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
index 24e68c47a0..4a92aee2b1 100644
--- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
+++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs
@@ -7,6 +7,7 @@ Stability   : provisional
 -}
 module Verifier.SAW.TypedTerm where
 
+import Control.Monad (foldM)
 import Data.Map (Map)
 import qualified Data.Map as Map
 
@@ -45,6 +46,49 @@ mkTypedTerm sc trm = do
   ct <- scCryptolType sc ty
   return $ TypedTerm (C.Forall [] [] ct) trm
 
+-- | Apply a function-typed 'TypedTerm' to an argument. This operation
+-- fails if the first 'TypedTerm' does not have a monomorphic function
+-- type.
+applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm
+applyTypedTerm sc (TypedTerm schema1 t1) (TypedTerm _schema2 t2) =
+  case C.tIsFun =<< C.isMono schema1 of
+    Nothing -> fail "applyTypedTerm: not a function type"
+    Just (_, cty') -> TypedTerm (C.tMono cty') <$> scApply sc t1 t2
+
+-- | Apply a 'TypedTerm' to a list of arguments. This operation fails
+-- if the first 'TypedTerm' does not have a function type of
+-- sufficient arity.
+applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
+applyTypedTerms sc = foldM (applyTypedTerm sc)
+
+-- | Create an abstract defined constant with the specified name and body.
+defineTypedTerm :: SharedContext -> String -> TypedTerm -> IO TypedTerm
+defineTypedTerm sc name (TypedTerm schema t) =
+  do ty <- scTypeOf sc t
+     TypedTerm schema <$> scConstant sc name t ty
+
+-- | Make a tuple value from a list of 'TypedTerm's. This operation
+-- fails if any 'TypedTerm' in the list has a polymorphic type.
+tupleTypedTerm :: SharedContext -> [TypedTerm] -> IO TypedTerm
+tupleTypedTerm sc tts =
+  case traverse (C.isMono . ttSchema) tts of
+    Nothing -> fail "tupleTypedTerm: invalid polymorphic term"
+    Just ctys ->
+      TypedTerm (C.tMono (C.tTuple ctys)) <$> scTuple sc (map ttTerm tts)
+
+-- | Given a 'TypedTerm' with a tuple type, return a list of its
+-- projected components. This operation fails if the 'TypedTerm' does
+-- not have a tuple type.
+destTupleTypedTerm :: SharedContext -> TypedTerm -> IO [TypedTerm]
+destTupleTypedTerm sc (TypedTerm schema t) =
+  case C.tIsTuple =<< C.isMono schema of
+    Nothing -> fail "asTupleTypedTerm: not a tuple type"
+    Just ctys ->
+      do let len = length ctys
+         let idxs = take len [1 ..]
+         ts <- traverse (\i -> scTupleSelector sc t i len) idxs
+         pure $ zipWith TypedTerm (map C.tMono ctys) ts
+
 -- First order types and values ------------------------------------------------
 
 cryptolTypeOfFirstOrderType :: FirstOrderType -> C.Type