Merge pull request #1871 from GaloisInc/fix_1870

Add types for `newtype` constructors. Fixes #1870
GaloisInc · May 23, 2023 · b89b8df · b89b8df
2 parents 29363db + 831e35d
commit b89b8df
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 3 deletions.
diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
@@ -297,9 +297,12 @@ mkCryEnv env =
      (types, _) <-
        liftModuleM modEnv $
        do prims <- MB.getPrimMap
-          -- noIfaceParams because we don't support translating functors yet
-          TM.inpVars `fmap` MB.genInferInput P.emptyRange prims
-            MI.noIfaceParams ifaceDecls
+          infInp <- MB.genInferInput P.emptyRange prims MI.noIfaceParams ifaceDecls
+          let newtypeCons = Map.fromList
+                              [ (T.ntName nt, T.newtypeConType nt)
+                              | nt <- Map.elems (TM.inpNewtypes infInp)
+                              ]
+          pure (newtypeCons `Map.union` TM.inpVars infInp)
      let types' = Map.union (eExtraTypes env) types
      let terms = eTermEnv env
      let cryEnv = C.emptyEnv

diff --git a/intTests/test_1870/A.cry b/intTests/test_1870/A.cry
@@ -0,0 +1,4 @@
+module A where
+
+newtype A = { x : [8] }
+
diff --git a/intTests/test_1870/test.saw b/intTests/test_1870/test.saw
@@ -0,0 +1,5 @@
+import "A.cry";
+
+// Make sure that `newtypes` work.
+// Specifically, that `A` is in scope.
+print {{ A { x = 2 } }};
diff --git a/intTests/test_1870/test.sh b/intTests/test_1870/test.sh
@@ -0,0 +1,2 @@
+set -e
+$SAW test.saw