Change saw-core tuple representation. #1612
Conversation
We now have an explicit AST constructor for arbitrary-size tuple values.
Tuple types are formalized as a type constructor that takes a list
of types as an argument:
data TypeList : sort 1 where {
TypeNil : TypeList;
TypeCons : sort 0 -> TypeList -> TypeList;
}
primitive Tuple : TypeList -> sort 0;
Additional primitives allow constructing and deconstructing tuples
in a nested fashion:
primitive headTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> t;
primitive tailTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> Tuple ts;
primitive consTuple : (t : sort 0) -> (ts : TypeList) -> t -> Tuple ts -> Tuple (TypeCons t ts);
NOTE: This commit makes the cryptol-saw-core test suite pass, but
saw-core-coq fails to compile. Further changes will be necessary.
|
The plan is to use a similar encoding for record types as well. The end goal is to get an injective mapping of Cryptol types into saw-core. @eddywestbrook I will need your assistance to figure out how to translate the new tuple encoding into Coq. |
These functions are now just the tuple functions specialized to tuples of size 2.
brianhuffman
force-pushed
the
saw-tuples
branch
from
78b546e
to
ff072a8
Compare
brianhuffman
force-pushed
the
saw-tuples
branch
from
ff072a8
to
4854f0d
Compare
With the new tuple representation, a single tuple type is represented as not a single AST node, but a whole pile of constructor applications (`Tuple`, `TypeCons`, `TypeNil`). A single call to WHNF followed by running the syntactic recognizer is not sufficient; we may need to evaluate to WHNF separately on each constructor.
With the new tuple representation the distinction between "x.1" and "x.(1)" is no longer needed.
brianhuffman
force-pushed
the
saw-tuples
branch
from
b4b33c8
to
0b43f8f
Compare
This avoids construction of 1-tuples. This makes many of the example proof scripts work again.
brianhuffman
force-pushed
the
saw-tuples
branch
from
b8fa170
to
e29f98f
Compare
We now have an explicit AST constructor for arbitrary-size tuple values.
Tuple types are formalized as a type constructor that takes a list
of types as an argument:
data TypeList : sort 1 where {
TypeNil : TypeList;
TypeCons : sort 0 -> TypeList -> TypeList;
}
primitive Tuple : TypeList -> sort 0;
Additional primitives allow constructing and deconstructing tuples
in a nested fashion:
primitive headTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> t;
primitive tailTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> Tuple ts;
primitive consTuple : (t : sort 0) -> (ts : TypeList) -> t -> Tuple ts -> Tuple (TypeCons t ts);
NOTE: This commit makes the cryptol-saw-core test suite pass, but
saw-core-coq fails to compile. Further changes will be necessary.
These functions are now just the tuple functions specialized to tuples of size 2.
With the new tuple representation, a single tuple type is represented as not a single AST node, but a whole pile of constructor applications (`Tuple`, `TypeCons`, `TypeNil`). A single call to WHNF followed by running the syntactic recognizer is not sufficient; we may need to evaluate to WHNF separately on each constructor.
With the new tuple representation the distinction between "x.1" and "x.(1)" is no longer needed.
This avoids construction of 1-tuples. This makes many of the example proof scripts work again.
These still need to be associated with the corresponding SAW primitives in `Translation/Coq/SpecialTreatment.hs`. Note that the definitions also expect the SAW type `TypeList` to be translated to `list Type` in Coq.
brianhuffman
force-pushed
the
saw-tuples
branch
from
17a545f
to
6d50ea7
Compare
|
I added some Coq code to Some of the saw-script files in
The other saw-script files fail on saw-script/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs Lines 4869 to 4870 in bc564dd The type error (once you simplify all the type functions involved) seems to always involves a mismatch between a type Unfortunately I have not yet implemented the syntax for tuple types in the saw-core pretty-printer, so types like |
…g pairs instead of building one big tuple; changd foldBlockMapLetRec to mapBlockMapLetRec to facilitate this
We now have an explicit AST constructor for arbitrary-size tuple values.
Tuple types are formalized as a type constructor that takes a list
of types as an argument:
data TypeList : sort 1 where {
TypeNil : TypeList;
TypeCons : sort 0 -> TypeList -> TypeList;
}
primitive Tuple : TypeList -> sort 0;
Additional primitives allow constructing and deconstructing tuples
in a nested fashion:
primitive headTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> t;
primitive tailTuple : (t : sort 0) -> (ts : TypeList) -> Tuple (TypeCons t ts) -> Tuple ts;
primitive consTuple : (t : sort 0) -> (ts : TypeList) -> t -> Tuple ts -> Tuple (TypeCons t ts);
NOTE: This commit makes the cryptol-saw-core test suite pass, but
saw-core-coq fails to compile. Further changes will be necessary.