aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
|
* A first step at refreshing and documenting the new feature.Gravatar Hugo Herbelin2018-02-20
|
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | This allows in particular to define notations with 'pat style binders. E.g.: A non-trivial change in this commit is storing binders and patterns separately from terms. This is not strictly necessary but has some advantages. However, it is relatively common to have binders also used as terms, or binders parsed as terms. Thus, it is already relatively common to embed binders into terms (see e.g. notation for ETA in output test Notations3.v) or to coerce terms to idents (see e.g. the notation for {x|P} where x is parsed as a constr). So, it is as simple to always store idents (and eventually patterns) as terms.
* Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | For instance, the following is now possible: Check {(x,y)|x+y=0}. Some questions remains. Maybe, by consistency, the notation should be "{'(x,y)|x+y=0}"...
* Preliminary work before adding general support for patterns in notations II.Gravatar Hugo Herbelin2018-02-20
| | | | | | Reordering the maps for binders and terms while uninterpreting a notation the same way it will be at the time of interpreting a notation.
* Preliminary work before adding general support for patterns in notations I.Gravatar Hugo Herbelin2018-02-20
| | | | | Factorizing the place where the different form of extended binders (i.e. possibly including the 'pat form) are matched.
* Preliminary work before extending support for binders in notationsGravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | (binders shall be substitutable by arbitrary cases patterns). Giving a proper status to the functions unifying different instance of the same notation variable (up to alpha-renaming). Note: The a priori change of semantics in "bind_binding_as_term_env" which now apply renaming from "unify_id" (as it did in "bind_bindinglist_as_term_env") should not have an effect since, as the former comment said, this corresponds to a "Anonymous" case which should not occur, since the term would have to be bound upwards.
* Preliminary steps before adding general support for patterns in notations.Gravatar Hugo Herbelin2018-02-20
| | | | Moving earlier functions which will be needed earlier.
* In printing notations with "match", reasoning up to the order of clauses.Gravatar Hugo Herbelin2018-02-20
|
* Preliminary work before extending support for binders in notationsGravatar Hugo Herbelin2018-02-20
| | | | (binders shall be substitutable by arbitrary cases patterns).
* Make pattern variables of "match" substitutable in notations.Gravatar Hugo Herbelin2018-02-20
|
* Supporting recursive notations reversing the left-to-right order.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | Seizing this opportunity to generalize the possibility for different associativity into simply reversing the order or not. Also dropping some dead code. Example of recursive notation now working: Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
* Allowing variables used in recursive notation to occur several times in pattern.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | This allows for instance to support recursive notations of the form: Notation "! x .. y # A #" := (((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..) (at level 200, x binder).
* Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | This makes treatment of recursive binders closer to the one of recursive terms. It is unclear whether there are interesting notations liable to use this, but this shall make easier mixing recursive binders and recursive terms as in next commits. Example of (artificial) notation that this commit supports: Notation "! x .. y # A #" := (.. (A,(forall x, True)) ..,(forall y, True)) (at level 200, x binder).
* Fixing/improving notations with recursive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - The "terminator" of a recursive notation is now interpreted in the environment in which it occurs rather than the environment at the beginning of the recursive patterns. Note that due to a tolerance in checking unbound variables of notations, a variable unbound in the environment was still working ok as long as no user-given variable was shadowing a private variable of the notation - see the "exists_mixed" example in test-suite. Conversely, in a notation such as: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! a b # a=b #. The unbound "a" was detected only at pretyping and not as expected at internalizing time, due to "a=b" interpreted in context containing a and b. - Similarly, each binder is now interpreted in the environment in which it occurs rather than as if the sequence of binders was dependent from the left to the right (such a dependency was ok for "forall" or "exists" but not in general). For instance, in: Notation "!! x .. y # A #" := ((forall x, True), .. ((forall y, True), A) ..) (at level 200, x binder). Check !! (a:nat) (b:a=a) # True #. The illegal dependency of the type of b in a was detected only at pretyping time. - If a let-in occurs in the sequence of binders of a notation with a recursive pattern, it is now inserted in between the occurrences of the iterator rather than glued with the forall/fun of the iterator. For instance, in: Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0), x=y. We now get exists '(x, y), True /\ (let u := 0 in True /\ x = y) while we had before the let-in breaking the repeated pattern: exists '(x, y), (let u := 0 in True /\ x = y) This is more compositional, and, in particular, the printer algorithm now recognizes the pattern which is otherwise broken.
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
|
* Notations: documenting structure collecting variables occurring in notation.Gravatar Hugo Herbelin2018-02-20
|
* Renaming binders into binderlists in egramcoq.ml.Gravatar Hugo Herbelin2018-02-20
|
* Introducing an intermediary type "constr_prod_entry_key" for grammar ↵Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | productions. This type describes the grammar non-terminal. It typically contains ETConstrList (now renamed ETProdConstrList) but not ETBinder. It is the type for metasyntax.ml and egramcoq.ml to communicate together. The type constr_prod_entry_key with ETConstr, ETBinder, is now used only in metasyntax.ml. This allows to get rid of some "assert false" in uselessly matching over ETConstrList in metasyntax.ml and of some "assert false" in uselessly matching over ETBinder in egramcoq.ml. Also exporting less of extend.mli in API.
* Canonically add an encoding in glob_constr of "as" operator for cases_pattern.Gravatar Hugo Herbelin2018-02-20
|
* Minor clarifying of name variables in constrintern.ml.Gravatar Hugo Herbelin2018-02-20
| | | | | | - renaming lvar into ntnvars when relevant, for consistency - renaming sometimes genv into env (intern_env) so as to remain consistent with other parts of the code
* Using name given by user to name a 'pat, if any.Gravatar Hugo Herbelin2018-02-20
| | | | This works for contexts in Definition and co, but not yet for "fun" and co.
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | | | | | | | | | The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed.
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
|
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
|
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
|
* Adding support for re-folding notation referring to isolated "forall '(x,y), t".Gravatar Hugo Herbelin2018-02-20
| | | | Was apparently forgotten in a67bd7f9.
* Again one more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2018-02-20
| | | | | | | | We enforce that variables of the notation hide the variables in the implicit-arguments map. Will be useful when there will be a special map of single binders when interpreting notations.
* Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Gravatar Maxime Dénès2018-02-19
|\ | | | | | | constraints.
* \ Merge PR #6761: Remove unused argument in Record.declare_structureGravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\ \ \
* \ \ \ Merge PR #6753: [toplevel] Make toplevel state into a record.Gravatar Maxime Dénès2018-02-19
|\ \ \ \
* \ \ \ \ Merge PR #6230: Better Cemitcodes API + compact relocation representationGravatar Maxime Dénès2018-02-19
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6759: detype_case predicate is not optionalGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6772: Cleanup inferCumulativityGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6648: [tactics] make apply_type safeGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | camlp4
* \ \ \ \ \ \ \ \ \ Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6571: Fix ci-all targetGravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \ \ \ \ \ \ \
| | | | * | | | | | | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | | | | * | | | | | | | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| |_|_|_|/ / / / / / / / |/| | | | | | | | | | |
| | | | | * | | | | | | Cleaner treatment of parameters in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | No using a mutable counter to skip them, instead we keep them in the environment.
| | | | | * | | | | | | Fix reduction flags in inferCumulativityGravatar Gaëtan Gilbert2018-02-16
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The only difference is when we have a rel local definition in the initial environment, which isn't actually possible. However that depends on the specific way we treat parameters.
| | | | | | | | | | * Adding a test for the construction that was broken in Coccinelle.Gravatar Pierre-Marie Pédrot2018-02-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There was no test in the test-suite checking for double with-def constraints in module typing.
| | | | | | | | | | * Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
| | | | | | | * | | [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We organize the toplevel execution as a record and pass it around. This will be used by future PRs as to for example decouple goal printing from the classifier.
| | | | | | | * | | [ide] Localize a IDE-specific flag.Gravatar Emilio Jesus Gallego Arias2018-02-15
| |_|_|_|_|_|/ / / |/| | | | | | | |
* | | | | | | | | Merge PR #1073: new quick2vo target: like vio2vo, but smarterGravatar Maxime Dénès2018-02-15
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | disable tests: vio2vo is broken in WindowsGravatar Ralf Jung2018-02-15
| | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 16:59:28 +0000