Merge pull request #1597 from GaloisInc/fix-newtype-translation

fix Cryptol to SAW newtype translation

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

@@ -46,14 +46,15 @@ import Cryptol.Eval.Type (evalValType)
 import qualified Cryptol.TypeCheck.AST as C
 import qualified Cryptol.TypeCheck.Subst as C (Subst, apSubst, listSubst, singleTParamSubst)
 import qualified Cryptol.ModuleSystem.Name as C
-  (asPrim, nameUnique, nameIdent, nameInfo, NameInfo(..))
+  (asPrim, asParamName, nameUnique, nameIdent, nameInfo, NameInfo(..))
 import qualified Cryptol.Utils.Ident as C
   ( Ident, PrimIdent(..), mkIdent
   , prelPrim, floatPrim, arrayPrim, suiteBPrim, primeECPrim
   , ModName, modNameToText, identText, interactiveName
   , ModPath(..), modPathSplit
   )
 import qualified Cryptol.Utils.RecordMap as C
+import Cryptol.TypeCheck.Type as C (Newtype(..))
 import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf)
 import Cryptol.Utils.PP (pretty)
 
@@ -1424,7 +1425,7 @@ proveEq sc env t1 t2
        t' <- importType sc env t1
        scCtorApp sc "Prelude.Refl" [s, t']
   | otherwise =
-    case (C.tNoUser t1, C.tNoUser t2) of
+    case (tNoUser t1, tNoUser t2) of
       (C.tIsSeq -> Just (n1, a1), C.tIsSeq -> Just (n2, a2)) ->
         do n1' <- importType sc env n1
            n2' <- importType sc env n2
@@ -1472,6 +1473,14 @@ proveEq sc env t1 t2
       (_, _) ->
         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
+    t -> t
+
+
 -- | Deconstruct a cryptol tuple type as a pair according to the
 -- saw-core tuple type encoding.
 tIsPair :: C.Type -> Maybe (C.Type, C.Type)
@@ -1804,3 +1813,30 @@ importFirstOrderValue t0 v0 = V.runEval mempty (go t0 v0)
 
     _ -> panic "importFirstOrderValue"
                 ["Expected finite value of type:", show t, "but got", show v]
+
+-- | Generate functions to construct newtypes in the term environment.
+-- (I.e., make identity functions that take the record the newtype wraps.)
+genNewtypeConstructors :: SharedContext -> Map C.Name Newtype -> Env -> IO Env
+genNewtypeConstructors sc newtypes env0 =
+  foldM genConstr env0 newtypes
+  where
+    genConstr :: Env -> Newtype -> IO Env
+    genConstr env nt = do
+      constr <- importExpr sc env (newtypeConstr nt)
+      let env' = env { envE = Map.insert (ntName nt) (constr, 0) (envE env)
+                     , envC = Map.insert (ntName nt) (newtypeSchema nt) (envC env)
+                     }
+      return env'
+    newtypeConstr :: Newtype -> C.Expr
+    newtypeConstr nt = foldr tFn fn (C.ntParams nt)
+      where
+        paramName = C.asParamName (ntName 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

@@ -373,7 +373,9 @@ loadCryptolModule sc primOpts env path = do
   let isNew m' = T.mName m' `notElem` oldModNames
   let newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv''
   let newDeclGroups = concatMap T.mDecls newModules
-  newCryEnv <- C.importTopLevelDeclGroups sc primOpts oldCryEnv newDeclGroups
+  let newNewtypes = Map.difference (ME.loadedNewtypes modEnv') (ME.loadedNewtypes modEnv)
+  newCryEnv <- C.genNewtypeConstructors sc newNewtypes oldCryEnv >>= \cEnv ->
+               C.importTopLevelDeclGroups sc primOpts cEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
   let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name
@@ -434,7 +436,9 @@ importModule sc env src as vis imps = do
   let isNew m' = T.mName m' `notElem` oldModNames
   let newModules = filter isNew $ map ME.lmModule $ ME.lmLoadedModules $ ME.meLoadedModules modEnv'
   let newDeclGroups = concatMap T.mDecls newModules
-  newCryEnv <- C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions oldCryEnv newDeclGroups
+  let newNewtypes = Map.difference (ME.loadedNewtypes modEnv') (ME.loadedNewtypes modEnv)
+  newCryEnv <- C.genNewtypeConstructors sc newNewtypes oldCryEnv >>= \cEnv ->
+               C.importTopLevelDeclGroups sc C.defaultPrimitiveOptions cEnv newDeclGroups
   newTermEnv <- traverse (\(t, j) -> incVars sc 0 j t) (C.envE newCryEnv)
 
   return env { eImports = (vis, P.Import (T.mName m) as imps) : eImports env

intTests/test_newtype/complex.cry

@@ -0,0 +1,40 @@
+// This is a development of rational complex numbers
+
+type Int = Integer
+
+// Complex rational numbers in rectangular coordinates
+newtype CplxInt =
+  { real : Int, imag : Int }
+
+embedQ : Int -> CplxInt
+embedQ x = CplxInt{ real = x, imag = 0 }
+
+cplxAdd : CplxInt -> CplxInt -> CplxInt
+cplxAdd x y = CplxInt { real = r, imag = i }
+  where
+  r = x.real + y.real
+  i = x.imag + y.imag
+
+cplxMul : CplxInt -> CplxInt -> CplxInt
+cplxMul x y = CplxInt { real = r, imag = i }
+  where
+  r = x.real * y.real - x.imag * y.imag
+  i = x.real * y.imag + x.imag * y.real
+
+cplxEq : CplxInt -> CplxInt -> Bit
+cplxEq x y = (x.real == y.real) && (x.imag == y.imag)
+
+cplxAddAssoc : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxAddAssoc x y z =
+  cplxEq (cplxAdd (cplxAdd x y) z)
+         (cplxAdd x (cplxAdd y z))
+
+cplxMulAssoc : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxMulAssoc x y z =
+  cplxEq (cplxMul (cplxMul x y) z)
+         (cplxMul x (cplxMul y z))
+
+cplxMulDistrib : CplxInt -> CplxInt -> CplxInt -> Bit
+cplxMulDistrib x y z =
+  cplxEq (cplxMul x (cplxAdd y z))
+         (cplxAdd (cplxMul x y) (cplxMul x z))

intTests/test_newtype/complex_newtype.saw

@@ -0,0 +1,8 @@
+import "complex.cry";
+
+prove_print cvc4 {{ \ x y z -> cplxAddAssoc x y z}};
+
+prove_print cvc4 {{ \ x y z -> cplxMulAssoc x y z}};
+
+prove_print cvc4 {{ \ x y z -> cplxMulDistrib x y z}};
+

intTests/test_newtype/test.sh

@@ -0,0 +1,4 @@
+#!/bin/sh
+set -e
+
+$SAW complex_newtype.saw