Candle: Kernel.compute and record syntax #906
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Record syntax will be implemented as syntactic sugar in the parser.
Declaring a record is done like this:
type my_rec = Constr of { f1: t1; f2: t2; ...; fN: tN };;
The above declaration is parsed into a datatype declaration and a series
of function declarations for projection, update and construction:
type my_rec = Constr t1 t2 ... tN
(* Here, we assume that f1 < f2 < ... < fN; otherwise field names and
types are sorted and re-ordered *)
let __f1_record_upd (Constr f1 f2 ... fN) f1 = Constr f1 f2 ... fN;;
let __f2_record_upd (Constr f1 f2 ... fN) f2 = ...;;
...
let __f1_record_proj (Constr f1 f2 ... fN) = f1;;
let __f2_record_proj (Constr f1 f2 ... fN) = f2;;
...
let __record_constr_Constr_f1_f2_..._fN =
fun f1 -> fun f2 -> ... -> fun fN -> Constr f1 f2 ... fN;;
Records with non-distinct field names are rejected. The fields and types
are ordered by the names of the fields. Internally, all records are
regular datatypes. This makes it possible (but unreliable) to pattern
match. For example:
type myrec = Foo { b: int; a: bool };;
let foo (Foo a b) = ... (* correct *) ;;
let foo' (Foo b a) = ... (* incorrect *) ;;
Projection is done with a dot:
myRecValue . foo (* becomes __foo_record_proj myRecValue *)
'with' updates:
myRecValue with foo := bar
(* becomes __foo_record_upd myRecValue bar *)
The previous rule was missing the constructor name, which is needed to figure out what constructor function to call.
Changed the function that deals with type definitions to also generate a sequence of projection/update/constructor functions for record type constructors. The functions are given names that are readable (in case they pop up in an error message) but impossible to get past the parser. Some syntactic criteria are checked (e.g., all field names under a single record constructor must be distinct), but other than that, the standard semantics is to simply overshadow previous definitions with the same name.
A FOLDL had snuck in where a FOLDR was needed, meaning that the record constructor functions were defined with their arguments appearing backwards.
Without this it isn't possible to detect multi-argument records in pattern matching, because the parser does not accept multi-argument constructor patterns/expressions.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR contributes two new features to the Candle theorem prover:
Kernel.computeDocumentation of these features will appear in the Candle repository README once this PR is merged.