From cbd03dfd4a3d8028531c410d8daa5fc9835b6898 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 16 May 2023 11:23:58 -0700 Subject: [PATCH 1/2] Add types for `newtype` constructors. Fixes #1870 --- cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs | 9 ++++++--- intTests/test_1870/A.cry | 4 ++++ intTests/test_1870/test.saw | 5 +++++ 3 files changed, 15 insertions(+), 3 deletions(-) create mode 100644 intTests/test_1870/A.cry create mode 100644 intTests/test_1870/test.saw diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 7abfd4e72f..1f26acca70 100644 --- 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 new file mode 100644 index 0000000000..cd9a5e814c --- /dev/null +++ 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 new file mode 100644 index 0000000000..5986959782 --- /dev/null +++ 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 } }}; From 831e35d71d60f033b5416e79b59b40b93dae9fa6 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 16 May 2023 13:32:24 -0700 Subject: [PATCH 2/2] Add forgotten file --- intTests/test_1870/test.sh | 2 ++ 1 file changed, 2 insertions(+) create mode 100644 intTests/test_1870/test.sh diff --git a/intTests/test_1870/test.sh b/intTests/test_1870/test.sh new file mode 100644 index 0000000000..f7eeb6ad15 --- /dev/null +++ b/intTests/test_1870/test.sh @@ -0,0 +1,2 @@ +set -e +$SAW test.saw