diff --git a/deps/cryptol b/deps/cryptol index 63f0ac6968..3973b15236 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 63f0ac6968967fb7898333778b5206083fdcb375 +Subproject commit 3973b15236ace5c11fdfabbf811d97daee7885ed diff --git a/intTests/test_constraint_guards/Instantiated.cry b/intTests/test_constraint_guards/Instantiated.cry new file mode 100644 index 0000000000..ac08d2ab35 --- /dev/null +++ b/intTests/test_constraint_guards/Instantiated.cry @@ -0,0 +1,3 @@ +module Instantiated = Parameterized where + +type gamma = 3 diff --git a/intTests/test_constraint_guards/Parameterized.cry b/intTests/test_constraint_guards/Parameterized.cry new file mode 100644 index 0000000000..0cb7b8b00a --- /dev/null +++ b/intTests/test_constraint_guards/Parameterized.cry @@ -0,0 +1,9 @@ +module Parameterized where + +parameter + type gamma : # + type constraint (fin gamma, gamma >= 2, 32 >= width gamma) + +// Constraint guard with type dependent on module parameter value +v : [gamma] +v | () => 0 diff --git a/intTests/test_constraint_guards/test.saw b/intTests/test_constraint_guards/test.saw index e2b443bb91..138ca32ea5 100644 --- a/intTests/test_constraint_guards/test.saw +++ b/intTests/test_constraint_guards/test.saw @@ -16,3 +16,7 @@ fails (prove_print z3 {{ \(x : [64]) -> incomplete x }}); prove_print z3 {{ dependent`{1} == [True] }}; prove_print z3 {{ dependent`{3} == [False, False, False] }}; prove_print z3 {{ dependent`{0} == [] }}; + +// Test constraint guards dependently typed on module parameters +import "Instantiated.cry"; +prove_print z3 {{ v == 0 }};