Skip to content

Commit 04597a9

Browse files
brianhuffmanbrianhuffman
authored
Merge pull request #2664 from GaloisInc/bh/simplify-recursor
Further simplify representation of recursors in saw-core terms
2 parents 0356e3e + 5ac3fa0 commit 04597a9

File tree

18 files changed

+304
-362
lines changed

18 files changed

+304
-362
lines changed

‎CHANGES.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,12 @@ This release supports [version
66

77
## Changes
88

9+
* In SAWCore syntax (as used by `parse_core`, `prove_core`, and
10+
`read_core`) partially-applied recursors are no longer an error.
11+
Elimination sorts for recursors are now specified by suffix:
12+
`TypeName#ind` eliminates to `Prop`, `TypeName#rec` eliminates
13+
to `sort 0`, and `TypeName#rec<n>` eliminates to `sort n`.
14+
915
* The experimental command `extract_uninterp` has been removed.
1016

1117
* The `normalize_term_opaque` and `goal_normalize` commands have been

‎cryptol-saw-core/saw/Cryptol.sawcore‎

Lines changed: 64 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ data Num : sort 0 where {
3737

3838
Num_rec : (p: Num -> sort 1) -> ((n:Nat) -> p (TCNum n)) -> p TCInf ->
3939
(n:Num) -> p n;
40-
Num_rec p f1 f2 n = Num#rec p f1 f2 n;
40+
Num_rec p f1 f2 n = Num#rec1 p f1 f2 n;
4141

4242
-- Check whether a 'Num' is finite
4343
tcFin : Num -> Bool;
@@ -54,7 +54,7 @@ getFinNat n =
5454
finNumRec : (p: Num -> isort 1) -> ((n:Nat) -> p (TCNum n)) ->
5555
(n:Num) -> p n;
5656
finNumRec p f n =
57-
Num#rec p f (error (p TCInf) "Unexpected Fin constraint violation!") n;
57+
Num#rec1 p f (error (p TCInf) "Unexpected Fin constraint violation!") n;
5858

5959
-- Helper function: destruct two Nums that we expect to be finite
6060
finNumRec2 : (p: Num -> Num -> isort 1) ->
@@ -219,7 +219,7 @@ tcLt = binaryNumPred ltNat (\ (x:Nat) -> True) (\ (y:Nat) -> False) True;
219219

220220
seq : Num -> sort 0 -> sort 0;
221221
seq num a =
222-
Num#rec (\ (num:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream a) num;
222+
Num#rec1 (\ (num:Num) -> sort 0) (\ (n:Nat) -> Vec n a) (Stream a) num;
223223

224224
-- FIXME: this rule should be derived by scDefRewriteRules
225225
seq_TCNum : (n:Nat) -> (a:sort 0) -> Eq (sort 0) (seq (TCNum n) a) (Vec n a);
@@ -233,7 +233,7 @@ seqMap a b num f =
233233

234234
seqConst : (n : Num) -> (a : sort 0) -> a -> seq n a;
235235
seqConst n =
236-
Num#rec (\ (n:Num) -> (a : sort 0) -> a -> seq n a) replicate streamConst n;
236+
Num#rec1 (\ (n:Num) -> (a : sort 0) -> a -> seq n a) replicate streamConst n;
237237

238238
seqInhabited : (n:Num) -> (a: sort 0) -> (x:a) -> seq n a;
239239
seqInhabited =
@@ -249,7 +249,7 @@ injectCode "Coq"
249249

250250
IntModNum : (num : Num) -> sort 0;
251251
IntModNum num =
252-
Num#rec (\ (n : Num) -> sort 0) IntMod Integer num;
252+
Num#rec1 (\ (n : Num) -> sort 0) IntMod Integer num;
253253

254254
-------------------------------------------------------------------------------
255255
-- Rationals (TODO)
@@ -561,27 +561,27 @@ PEqIntMod n = { eq = intModEq n };
561561

562562
PEqIntModNum : (num : Num) -> PEq (IntModNum num);
563563
PEqIntModNum num =
564-
Num#rec (\ (n : Num) -> PEq (IntModNum n)) PEqIntMod PEqInteger num;
564+
Num#rec1 (\ (n : Num) -> PEq (IntModNum n)) PEqIntMod PEqInteger num;
565565

566566
PEqVec : (n : Nat) -> (a : isort 0) -> PEq a -> PEq (Vec n a);
567567
PEqVec n a pa = { eq = vecEq n a pa.eq };
568568

569569
PEqSeq : (n : Num) -> (a : isort 0) -> PEq a -> PEq (seq n a);
570570
PEqSeq n =
571-
Num#rec (\ (n:Num) -> (a : isort 0) -> PEq a -> PEq (seq n a))
572-
(\ (n:Nat) -> PEqVec n)
573-
(\ (a:isort 0) (pa : PEq a) -> error (PEq (Stream a)) "invalid Eq instance")
574-
n;
571+
Num#rec1 (\ (n:Num) -> (a : isort 0) -> PEq a -> PEq (seq n a))
572+
(\ (n:Nat) -> PEqVec n)
573+
(\ (a:isort 0) (pa : PEq a) -> error (PEq (Stream a)) "invalid Eq instance")
574+
n;
575575

576576
PEqWord : (n : Nat) -> PEq (Vec n Bool);
577577
PEqWord n = { eq = bvEq n };
578578

579579
PEqSeqBool : (n : Num) -> PEq (seq n Bool);
580580
PEqSeqBool n =
581-
Num#rec (\ (n : Num) -> PEq (seq n Bool))
582-
(\ (n:Nat) -> PEqWord n)
583-
(error (PEq (Stream Bool)) "invalid Eq instance")
584-
n;
581+
Num#rec1 (\ (n : Num) -> PEq (seq n Bool))
582+
(\ (n:Nat) -> PEqWord n)
583+
(error (PEq (Stream Bool)) "invalid Eq instance")
584+
n;
585585

586586
PEqUnit : PEq #();
587587
PEqUnit = { eq = \ (x y : #()) -> True };
@@ -620,20 +620,20 @@ PCmpVec n a pa =
620620

621621
PCmpSeq : (n : Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a);
622622
PCmpSeq n =
623-
Num#rec (\ (n:Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a))
624-
(\ (n:Nat) -> PCmpVec n)
625-
(\ (a:isort 0) (pa : PCmp a) -> error (PCmp (Stream a)) "invalid Cmp instance")
626-
n;
623+
Num#rec1 (\ (n:Num) -> (a : isort 0) -> PCmp a -> PCmp (seq n a))
624+
(\ (n:Nat) -> PCmpVec n)
625+
(\ (a:isort 0) (pa : PCmp a) -> error (PCmp (Stream a)) "invalid Cmp instance")
626+
n;
627627

628628
PCmpWord : (n : Nat) -> PCmp (Vec n Bool);
629629
PCmpWord n = { cmpEq = PEqWord n, cmp = bvCmp n, le = bvule n, lt = bvult n };
630630

631631
PCmpSeqBool : (n : Num) -> PCmp (seq n Bool);
632632
PCmpSeqBool n =
633-
Num#rec (\ (n : Num) -> PCmp (seq n Bool))
634-
(\ (n:Nat) -> PCmpWord n)
635-
(error (PCmp (Stream Bool)) "invalid Cmp instance")
636-
n;
633+
Num#rec1 (\ (n : Num) -> PCmp (seq n Bool))
634+
(\ (n:Nat) -> PCmpWord n)
635+
(error (PCmp (Stream Bool)) "invalid Cmp instance")
636+
n;
637637

638638
PCmpUnit : PCmp #();
639639
PCmpUnit = { cmpEq = PEqUnit, cmp = unitCmp, le = unitLe, lt = unitLt };
@@ -667,20 +667,20 @@ PSignedCmpVec n a pa =
667667

668668
PSignedCmpSeq : (n : Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a);
669669
PSignedCmpSeq n =
670-
Num#rec (\ (n:Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a))
671-
(\ (n:Nat) -> PSignedCmpVec n)
672-
(\ (a:isort 0) (pa : PSignedCmp a) -> error (PSignedCmp (Stream a)) "invalid SignedCmp instance")
673-
n;
670+
Num#rec1 (\ (n:Num) -> (a : isort 0) -> PSignedCmp a -> PSignedCmp (seq n a))
671+
(\ (n:Nat) -> PSignedCmpVec n)
672+
(\ (a:isort 0) (pa : PSignedCmp a) -> error (PSignedCmp (Stream a)) "invalid SignedCmp instance")
673+
n;
674674

675675
PSignedCmpWord : (n : Nat) -> PSignedCmp (Vec n Bool);
676676
PSignedCmpWord n = { signedCmpEq = PEqWord n, scmp = bvSCmp n, sle = bvsle n, slt = bvslt n };
677677

678678
PSignedCmpSeqBool : (n : Num) -> PSignedCmp (seq n Bool);
679679
PSignedCmpSeqBool n =
680-
Num#rec (\ (n : Num) -> PSignedCmp (seq n Bool))
681-
(\ (n:Nat) -> PSignedCmpWord n)
682-
(error (PSignedCmp (Stream Bool)) "invalid SignedCmp instance")
683-
n;
680+
Num#rec1 (\ (n : Num) -> PSignedCmp (seq n Bool))
681+
(\ (n:Nat) -> PSignedCmpWord n)
682+
(error (PSignedCmp (Stream Bool)) "invalid SignedCmp instance")
683+
n;
684684

685685
PSignedCmpUnit : PSignedCmp #();
686686
PSignedCmpUnit = { signedCmpEq = PEqUnit, scmp = unitCmp, sle = unitLe, slt = unitLt };
@@ -712,17 +712,17 @@ PZeroRational : PZero Rational;
712712
PZeroRational = integerToRational (natToInt 0);
713713

714714
PZeroIntModNum : (num : Num) -> PZero (IntModNum num);
715-
PZeroIntModNum num = Num#rec (\ (n : Num) -> PZero (IntModNum n)) PZeroIntMod PZeroInteger num;
715+
PZeroIntModNum num = Num#rec1 (\ (n : Num) -> PZero (IntModNum n)) PZeroIntMod PZeroInteger num;
716716

717717
PZeroSeq : (n : Num) -> (a : sort 0) -> PZero a -> PZero (seq n a);
718718
PZeroSeq n a pa = seqConst n a pa;
719719

720720
PZeroSeqBool : (n : Num) -> PZero (seq n Bool);
721721
PZeroSeqBool n =
722-
Num#rec (\ (n:Num) -> PZero (seq n Bool))
723-
(\ (n:Nat) -> bvNat n 0)
724-
(streamConst Bool False)
725-
n;
722+
Num#rec1 (\ (n:Num) -> PZero (seq n Bool))
723+
(\ (n:Nat) -> bvNat n 0)
724+
(streamConst Bool False)
725+
n;
726726

727727
PZeroFun : (a b : sort 0) -> PZero b -> PZero (a -> b);
728728
PZeroFun a b pb = (\(_ : a) -> pb);
@@ -767,10 +767,10 @@ PLogicStream a pa =
767767

768768
PLogicSeq : (n : Num) -> (a : isort 0) -> PLogic a -> PLogic (seq n a);
769769
PLogicSeq n =
770-
Num#rec (\ (n:Num) -> (a:isort 0) -> PLogic a -> PLogic (seq n a))
771-
(\ (n:Nat) -> PLogicVec n)
772-
(\ (a:isort 0) -> PLogicStream a)
773-
n;
770+
Num#rec1 (\ (n:Num) -> (a:isort 0) -> PLogic a -> PLogic (seq n a))
771+
(\ (n:Nat) -> PLogicVec n)
772+
(\ (a:isort 0) -> PLogicStream a)
773+
n;
774774

775775
PLogicWord : (n : Nat) -> PLogic (Vec n Bool);
776776
PLogicWord n =
@@ -783,8 +783,8 @@ PLogicWord n =
783783

784784
PLogicSeqBool : (n : Num) -> PLogic (seq n Bool);
785785
PLogicSeqBool n =
786-
Num#rec (\ (n:Num) -> PLogic (seq n Bool))
787-
(\ (n:Nat) -> PLogicWord n) (PLogicStream Bool PLogicBit) n;
786+
Num#rec1 (\ (n:Num) -> PLogic (seq n Bool))
787+
(\ (n:Nat) -> PLogicWord n) (PLogicStream Bool PLogicBit) n;
788788

789789
PLogicFun : (a b : sort 0) -> PLogic b -> PLogic (a -> b);
790790
PLogicFun a b pb =
@@ -847,7 +847,7 @@ PRingIntMod n =
847847

848848
PRingIntModNum : (num : Num) -> PRing (IntModNum num);
849849
PRingIntModNum num =
850-
Num#rec (\ (n : Num) -> PRing (IntModNum n)) PRingIntMod PRingInteger num;
850+
Num#rec1 (\ (n : Num) -> PRing (IntModNum n)) PRingIntMod PRingInteger num;
851851

852852
PRingRational : PRing Rational;
853853
PRingRational =
@@ -881,10 +881,10 @@ PRingStream a pa =
881881

882882
PRingSeq : (n : Num) -> (a : isort 0) -> PRing a -> PRing (seq n a);
883883
PRingSeq n =
884-
Num#rec (\ (n : Num) -> (a : isort 0) -> PRing a -> PRing (seq n a))
885-
(\ (n:Nat) -> PRingVec n)
886-
(\ (a:isort 0) -> PRingStream a)
887-
n;
884+
Num#rec1 (\ (n : Num) -> (a : isort 0) -> PRing a -> PRing (seq n a))
885+
(\ (n:Nat) -> PRingVec n)
886+
(\ (a:isort 0) -> PRingStream a)
887+
n;
888888

889889
PRingWord : (n : Nat) -> PRing (Vec n Bool);
890890
PRingWord n =
@@ -898,10 +898,10 @@ PRingWord n =
898898

899899
PRingSeqBool : (n : Num) -> PRing (seq n Bool);
900900
PRingSeqBool n =
901-
Num#rec (\ (n:Num) -> PRing (seq n Bool))
902-
(\ (n:Nat) -> PRingWord n)
903-
(error (PRing (Stream Bool)) "PRingSeqBool: no instance for streams")
904-
n;
901+
Num#rec1 (\ (n:Num) -> PRing (seq n Bool))
902+
(\ (n:Nat) -> PRingWord n)
903+
(error (PRing (Stream Bool)) "PRingSeqBool: no instance for streams")
904+
n;
905905

906906
PRingFun : (a b : sort 0) -> PRing b -> PRing (a -> b);
907907
PRingFun a b pb =
@@ -971,10 +971,10 @@ PIntegralWord n =
971971

972972
PIntegralSeqBool : (n : Num) -> PIntegral (seq n Bool);
973973
PIntegralSeqBool n =
974-
Num#rec (\ (n:Num) -> PIntegral (seq n Bool))
975-
(\ (n:Nat) -> PIntegralWord n)
976-
(error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
977-
n;
974+
Num#rec1 (\ (n:Num) -> PIntegral (seq n Bool))
975+
(\ (n:Nat) -> PIntegralWord n)
976+
(error (PIntegral (Stream Bool)) "PIntegralSeqBool: no instance for streams")
977+
n;
978978

979979

980980
-- Field class
@@ -1003,7 +1003,7 @@ PFieldIntMod n =
10031003

10041004
PFieldIntModNum : (n : Num) -> PField (IntModNum n);
10051005
PFieldIntModNum num =
1006-
Num#rec (\ (n : Num) -> PField (IntModNum n))
1006+
Num#rec1 (\ (n : Num) -> PField (IntModNum n))
10071007
PFieldIntMod
10081008
(error (PField (IntModNum TCInf)) "PFieldIntModNum: no instance for inf")
10091009
num;
@@ -1047,8 +1047,8 @@ PLiteralLessThan a = Nat -> a;
10471047

10481048
PLiteralSeqBool : (n : Num) -> PLiteral (seq n Bool);
10491049
PLiteralSeqBool n =
1050-
Num#rec (\ (n : Num) -> PLiteral (seq n Bool)) bvNat
1051-
(error (PLiteral (Stream Bool)) "PLiteralSeqBool: no instance for streams") n;
1050+
Num#rec1 (\ (n : Num) -> PLiteral (seq n Bool)) bvNat
1051+
(error (PLiteral (Stream Bool)) "PLiteralSeqBool: no instance for streams") n;
10521052

10531053
PLiteralBit : PLiteral Bool;
10541054
PLiteralBit = Nat_cases Bool False (\ (n:Nat) -> \ (b:Bool) -> True);
@@ -1061,7 +1061,7 @@ PLiteralIntMod n = \ (x : Nat) -> toIntMod n (natToInt x);
10611061

10621062
PLiteralIntModNum : (num : Num) -> PLiteral (IntModNum num);
10631063
PLiteralIntModNum num =
1064-
Num#rec (\ (n : Num) -> PLiteral (IntModNum n)) PLiteralIntMod PLiteralInteger num;
1064+
Num#rec1 (\ (n : Num) -> PLiteral (IntModNum n)) PLiteralIntMod PLiteralInteger num;
10651065

10661066
PLiteralRational : PLiteral Rational;
10671067
PLiteralRational = \ (x : Nat) -> error Rational "Unimplemented: Literal Rational";
@@ -1226,7 +1226,7 @@ ecFraction a = error a "Unimplemented: fraction";
12261226
ecShiftL : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
12271227
seq m a -> ix -> seq m a;
12281228
ecShiftL m =
1229-
Num#rec
1229+
Num#rec1
12301230
(\ (m:Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> seq m a -> ix -> seq m a)
12311231

12321232
-- Case for (TCNum m)
@@ -1246,7 +1246,7 @@ ecShiftL m =
12461246
ecShiftR : (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a ->
12471247
seq m a -> ix -> seq m a;
12481248
ecShiftR m =
1249-
Num#rec
1249+
Num#rec1
12501250
(\ (m : Num) -> (ix a : sort 0) -> PIntegral ix -> PZero a -> seq m a -> ix -> seq m a)
12511251

12521252
-- Case for (TCNum m)
@@ -1343,7 +1343,7 @@ ecDrop =
13431343

13441344
ecJoin : (m n : Num) -> (a : isort 0) -> seq m (seq n a) -> seq (tcMul m n) a;
13451345
ecJoin m =
1346-
Num#rec
1346+
Num#rec1
13471347
(\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq m (seq n a) ->
13481348
seq (tcMul m n) a)
13491349
(\ (m:Nat) ->
@@ -1371,7 +1371,7 @@ ecJoin m =
13711371
ecSplit : (m n : Num) -> (a : isort 0) -> seq (tcMul m n) a ->
13721372
seq m (seq n a);
13731373
ecSplit m =
1374-
Num#rec
1374+
Num#rec1
13751375
(\ (m:Num) -> (n:Num) -> (a:isort 0) -> seq (tcMul m n) a ->
13761376
seq m (seq n a))
13771377
(\ (m:Nat) ->
@@ -1432,7 +1432,7 @@ ecTranspose m n a =
14321432

14331433
ecAt : (n : Num) -> (a : isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a;
14341434
ecAt n =
1435-
Num#rec
1435+
Num#rec1
14361436
(\ (n:Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a)
14371437
(\ (n:Nat) -> \ (a:isort 0) -> \ (ix:sort 0) -> \ (pix:PIntegral ix) -> \ (xs:Vec n a) ->
14381438
pix.posNegCases a
@@ -1770,7 +1770,7 @@ fpSqrt e p r x = error (TCFloat e p) "Unimplemented: fpSqrt";
17701770
-- Array update
17711771
ecUpdate : (n : Num) -> (a:isort 0) -> (ix: sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a;
17721772
ecUpdate n =
1773-
Num#rec
1773+
Num#rec1
17741774
(\ (n:Num) -> (a:isort 0) -> (ix : sort 0) -> PIntegral ix -> seq n a -> ix -> a -> seq n a)
17751775
(\ (n:Nat) -> \ (a:isort 0) -> \ (ix : sort 0) -> \ (pix:PIntegral ix) -> \ (xs : Vec n a) ->
17761776
-- Case for (TCNum n, TCNum w)

‎intTests/test_sawcore_type_errors/test.log.good‎

Lines changed: 8 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -21,17 +21,8 @@ Stack trace:
2121
.:1:0:
2222
No such data type: ModuleIdentifier Cryptol.String
2323

24-
Recursor not fully applied
25-
== Anticipated failure message ==
26-
Stack trace:
27-
(builtin) in parse_core
28-
test.saw:4:36-4:50 in (callback)
29-
(builtin) in fails
30-
test.saw:4:17-4:54 in parse
31-
test.saw:13:1-13:73 (at top level)
32-
.:1:0:
33-
Recursor not fully applied: ModuleIdentifier Prelude.Either
34-
24+
Partially-applied recursors are permitted
25+
Either#rec Nat
3526
Not a sort (lambda)
3627
== Anticipated failure message ==
3728
Stack trace:
@@ -124,21 +115,18 @@ While typechecking term:
124115
Not a sort
125116
Prelude.Bool
126117

127-
Not a sort (recursor)
118+
Disallowed propositional elimination
128119
== Anticipated failure message ==
129120
Stack trace:
130121
(builtin) in parse_core
131122
test.saw:4:36-4:50 in (callback)
132123
(builtin) in fails
133124
test.saw:4:17-4:54 in parse
134-
test.saw:34:1-34:59 (at top level)
135-
.:1:15:
136-
While typechecking term:
137-
(arg : Prelude.Void)
138-
-> (\(_ : Prelude.Void) -> Prelude.True) arg
139-
.:1:15:
140-
Not a sort
141-
Prelude.Bool
125+
test.saw:34:1-34:20 (at top level)
126+
.:1:0:
127+
Malformed recursor
128+
Prelude.IsLeNat#rec
129+
Disallowed propositional elimination
142130

143131
Function application with non-function type
144132
== Anticipated failure message ==

0 commit comments

Comments
 (0)