Candle: Kernel.compute and record syntax #906
Merged
Commits on May 4, 2022
Commits on May 5, 2022
Commits on May 6, 2022
Commits on May 9, 2022
Commits on May 10, 2022
Commits on May 11, 2022
-
-
-
-
-
Rename NPR and num_pair types/values/defs
The new primitive is called 'compute' and operates on the 'compute_val' type, which is shortened _CVAL in the proofs about the deep embeddings.
-
Commits on May 13, 2022
-
Updates to compute theorem statements + fixes
- Updates the required compute theorems to have variable names match verbatim with what is defined in HOL Light - Removes the unused list items (we won't use them) but keeps some Bool items (as we'll use conditionals in v3). - Fixes a few annoying theorems
-
Commits on May 16, 2022
-
-
Add syntax for bools, chars and strings
Characters are defined from booleans, and strings are char lists as usual.
-
-
-
Commits on May 17, 2022
Commits on May 18, 2022
Commits on May 23, 2022
-
Move to substitution semantics
The substitution semantics gives a nicer theorem statement, as both sides of the equation share the same set of free variables.
Commits on May 25, 2022
-
-
Split theories into several files
Separates implementations from proofs
-
Commits on May 28, 2022
Commits on May 31, 2022
Commits on Jun 2, 2022
-
-
-
Move compute expressions + semantics into own dir
This division looks a bit awkward (compute_syntax/ and compute/) but the idea is this: the actual compute expressions and their interpreter code do not depend on Candle functions, and are to be translated /before/ Candle. The rest of the compute code (under compute/) does depend on Candle, however, and must be translated after the Candle functions. With this change, the type, term and theorem types will be translated before the usual place in the Candle ml_hol_kernel_funsProgScript.sml
-
-
-
-
-
-
-
-
-
-
-
-
Commits on Jun 3, 2022
Commits on Jun 4, 2022
-
Prove compute_eval always succeeds or diverges
compute_eval will either succeed or raise a <<timeout>> exception. Unfortunately the type checks in compute raises all sorts of exceptions if the type check fails, so this fact is not visible in the top-level theorem.
Commits on Jun 7, 2022
Commits on Jul 7, 2022
Commits on Aug 5, 2022
Commits on Aug 13, 2022
Commits on Aug 15, 2022
Commits on Aug 16, 2022
Commits on Aug 17, 2022
-
Write tests for Candle record syntax
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 *) -
-
-
-
Change the record constructor rule in the PEG
The previous rule was missing the constructor name, which is needed to figure out what constructor function to call.
-
Commits on Aug 18, 2022
-
Create record funs in TypeDefinition function
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.
-
-
-
-
-
-
-
-
-
-
-
Commits on Aug 19, 2022
Commits on Aug 21, 2022
-
Give record constructor arguments in correct order
A FOLDL had snuck in where a FOLDR was needed, meaning that the record constructor functions were defined with their arguments appearing backwards.
-
Commits on Aug 22, 2022
-
Wrap record constructor arguments in tuples if n>1
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.
Commits on Aug 23, 2022
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.