Make things build with the sum-types branch of cryptol

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

@@ -39,7 +39,7 @@ module Verifier.SAW.Cryptol
   , exportValueWithSchema
   ) where
 
-import Control.Monad (foldM, join, unless)
+import Control.Monad (foldM, join, unless,forM)
 import Control.Exception (catch, SomeException)
 import Data.Bifunctor (first)
 import qualified Data.Foldable as Fold
@@ -268,8 +268,9 @@ importType sc env ty =
 
     C.TNewtype nt ts ->
       do let s = C.listSubst (zip (map C.TVBound (C.ntParams nt)) ts)
-         let t = plainSubst s (C.TRec (C.ntFields nt))
-         go t
+         case ntDef nt of
+           C.Struct stru -> go (plainSubst s (C.TRec (C.ntFields stru)))
+           C.Enum {} -> error "importTyp: `enum` is not yet supported"
 
     C.TCon tcon tyargs ->
       case tcon of
@@ -1009,7 +1010,10 @@ importExpr sc env expr =
                       (elemIndex x (map fst (C.canonicalFields fm)))
                     scTupleSelector sc e' (i+1) (length (C.canonicalFields fm))
                C.TNewtype nt _args ->
-                 do let fs = C.ntFields nt
+                 do let fs = case C.ntDef nt of
+                               C.Struct s -> C.ntFields s
+                               C.Enum {} ->
+                                 panic "importExpr" ["Select from enum"]
                     i <- the ("Expected field " ++ show x ++ " in Newtype Record Sel")
                           (elemIndex x (map fst (C.canonicalFields fs)))
                     scTupleSelector sc e' (i+1) (length (C.canonicalFields fs))
@@ -1632,14 +1636,26 @@ proveEq sc env t1 t2
       (C.tIsRec -> Just tm1, C.tIsRec -> Just tm2)
         | map fst (C.canonicalFields tm1) == map fst (C.canonicalFields tm2) ->
           proveEq sc env (C.tTuple (map snd (C.canonicalFields tm1))) (C.tTuple (map snd (C.canonicalFields tm2)))
+
+      -- XXX: add a case for `enum`
+      -- 1. Match constructors by names, and prove fields as tuples
+      -- 2. We need some way to combine the proofs of equality of
+      -- the fields, into a proof for equality of the wholte type
+      -- for sums
+
       (_, _) ->
         panic "proveEq" ["Internal type error:", pretty t1, pretty t2]
 
+
 -- | Resolve user types (type aliases and newtypes) to their simpler SAW-compatible forms.
 tNoUser :: C.Type -> C.Type
 tNoUser initialTy =
   case C.tNoUser initialTy of
-    C.TNewtype nt _ -> C.TRec $ C.ntFields nt
+    C.TNewtype nt params
+      | C.Struct fs <- C.ntDef nt ->
+        if null params then C.TRec (C.ntFields fs)
+                       else error "tNoUser: Newtype with parameters"
+                        -- XXX: We should instantiate, see #2019
     t -> t
 
 
@@ -1904,7 +1920,9 @@ exportValue ty v = case ty of
 
   -- newtypes
   TV.TVNewtype _ _ fields ->
-    exportValue (TV.TVRec fields) v
+    case fields of
+      TV.TVStruct fs -> exportValue (TV.TVRec fs) v
+      TV.TVEnum {}   -> error "exportValue: TODO enum"
 
 
 exportTupleValue :: [TV.TValue] -> SC.CValue -> [V.Eval V.Value]
@@ -1988,22 +2006,28 @@ genNewtypeConstructors sc newtypes env0 =
   where
     genConstr :: Env -> Newtype -> IO Env
     genConstr env nt = do
-      constr <- importExpr sc env (newtypeConstr nt)
-      let env' = env { envE = Map.insert (ntConName nt) (constr, 0) (envE env)
-                     , envC = Map.insert (ntConName nt) (newtypeSchema nt) (envC env)
+      let conTs = C.newtypeConTypes nt
+      constrs <- forM (newtypeConstrs nt) $ \(x,e) ->
+        do e' <- importExpr sc env e
+           pure (x,(e',0))
+      let env' = env { envE = foldr (uncurry Map.insert) (envE env) constrs
+                     , envC = foldr (uncurry Map.insert) (envC env) conTs
                      }
       return env'
-    newtypeConstr :: Newtype -> C.Expr
-    newtypeConstr nt = foldr tFn fn (C.ntParams nt)
+
+    newtypeConstrs :: Newtype -> [(C.Name,C.Expr)]
+    newtypeConstrs nt =
+      case C.ntDef nt of
+        C.Struct fs ->
+          let recTy = C.TRec (C.ntFields fs)
+              fn    = C.EAbs paramName recTy (C.EVar paramName)
+              con   = C.ntConName fs
+              paramName = C.asLocal C.NSValue con
+           in [(con, foldr tFn fn (C.ntParams nt))]
+        C.Enum {} -> error "genNewtypeConstrurctrs: `enum` is not yet supported"
       where
-        paramName = C.asLocal C.NSValue (ntConName nt)
 
-        recTy = C.TRec $ ntFields nt
-        fn = C.EAbs paramName recTy (C.EVar paramName) -- EAbs Name Type Expr -- ETAbs TParam Expr
         tFn tp body =
           if elem (C.tpKind tp) [C.KType, C.KNum]
             then C.ETAbs tp body
             else panic "genNewtypeConstructors" ["illegal newtype parameter kind", show (C.tpKind tp)]
-    newtypeSchema :: Newtype -> C.Schema
-    newtypeSchema nt = C.Forall (ntParams nt) (ntConstraints nt)
-                       $ C.TRec (ntFields nt) `C.tFun` C.TRec (ntFields nt)

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

@@ -313,8 +313,9 @@ mkCryEnv env =
           -- noIfaceParams because we don't support translating functors yet
           infInp <- MB.genInferInput P.emptyRange prims NoParams ifaceDecls
           let newtypeCons = Map.fromList
-                              [ (T.ntConName nt, T.newtypeConType nt)
+                              [ con
                               | nt <- Map.elems (TM.inpNewtypes infInp)
+                              , con <- T.newtypeConTypes nt
                               ]
           pure (newtypeCons `Map.union` TM.inpVars infInp)
      let types' = Map.union (eExtraTypes env) types

src/SAWScript/Crucible/LLVM/FFI.hs

@@ -75,7 +75,7 @@ import           Verifier.SAW.CryptolEnv
 import           Verifier.SAW.OpenTerm
 import           Verifier.SAW.Prelude
 import           Verifier.SAW.Recognizer
-import           Verifier.SAW.SharedTerm
+import           Verifier.SAW.SharedTerm as Term
 import           Verifier.SAW.TypedTerm
 
 -- | Commonly used things that need to be passed around.
@@ -142,7 +142,7 @@ llvm_ffi_setup TypedTerm { ttTerm = appTerm } = do
   cryEnv <- lll $ rwCryptol <$> getMergedEnv
   case asConstant funTerm of
     Just (ec, funDef)
-      | Just FFIFunType {..} <- Map.lookup (ecName ec) (eFFITypes cryEnv) -> do
+      | Just FFIFunType {..} <- Map.lookup (Term.ecName ec) (eFFITypes cryEnv) -> do
         when (isNothing funDef) do
           throwFFISetup
             "Cannot verify foreign function with no Cryptol implementation"