Add types for newtype constructors. Fixes #1870

GaloisInc · May 16, 2023 · cbd03df · cbd03df
1 parent df95bf4
commit cbd03df
Show file tree

Hide file tree

Showing 3 changed files with 15 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 } }};