aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Collapse)AuthorAge
* Fixing the 3 cases of a "Stream.Error" ended with two periods.Gravatar Hugo Herbelin2018-04-12
| | | | | The "Stream.Error" printer does add a period, so, the messages themselves should not.
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | | | | The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now.
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
| | | | | | | | | | | We continue with the work of #402 and #6745 and update most of the remaining parts of the AST: - module declarations - intro patterns - top-level sentences Now, parsed documents should be full annotated by `CAst` nodes.
* Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
|
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit was motivated by true spurious conversions arising in my `to_constr` debug branch. The changes here need careful review as the tradeoffs are subtle and still a lot of clean up remains to be done in `vernac/*`. We have opted for penalize [minimally] the few users coming from true `Constr`-land, but I am sure we can tweak code in a much better way. In particular, it is not clear if internalization should take an `evar_map` even in the cases where it is not triggered, see the changes under `plugins` for a good example. Also, the new return type of `Pretyping.understand` should undergo careful review. We don't touch `Impargs` as it is not clear how to proceed, however, the current type of `compute_implicits_gen` looks very suspicious as it is called often with free evars. Some TODOs are: - impargs was calling whd_all, the Econstr equivalent can be either + Reductionops.whd_all [which does refolding and no sharing] + Reductionops.clos_whd_flags with all as a flag.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| | | | | | | | | We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
| | | | For compatibility, the default is to parse as ident and not as pattern.
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
| | | | | | | | | | | | Concretely, we provide "constr as ident", "constr as strict pattern" and "constr as pattern". This tells to parse a binder as a constr, restricting to only ident or to only a strict pattern, or to a pattern which can also be an ident. The "strict pattern" modifier allows to restrict the use of patterns in printing rules. This allows e.g. to select the appropriate rule for printing between {x|P} and {'pat|P}.
* Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
| | | | | This now works not only for parsing of fun/forall (as in 8.6), but also for arbitraty notations with binders and for printing.
* Respecting the ident/pattern distinction in notation modifiers.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 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.
* 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.
* Notations: Do not consider a non-occurring variable as a binder-only variable.Gravatar Hugo Herbelin2018-02-20
|
* 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 #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\
* | Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
| | | | | | | | | | | | | | | | | | | | | | | | | | There is no way today to distinguish primitive projections from compatibility constants, at least in the case of a record without parameters. We remedy to this by always using the r.(p) syntax when printing primitive projections, even with Set Printing All. The input syntax r.(p) is still elaborated to GApp, so that we can preserve the compatibility layer. Hopefully we can make up a plan to get rid of that layer, but it will require fixing a few problems.
| * Support universe instances on the literal TypeGravatar Tej Chajed2018-01-26
|/ | | | Fixes BZ#5726.
* Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\
* \ Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Gravatar Maxime Dénès2017-12-15
|\ \
| | * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
| |/ | | | | | | | | We remove a lot of uses of `evar_map` ref in `vernac`, cleanup step desirable to progress with EConstr there.
| * [econstr] Cleanup in `vernac/classes.ml`.Gravatar Emilio Jesus Gallego Arias2017-12-13
| | | | | | | | | | | | | | | | We fix quite a few types, and perform some cleanup wrt to the evar_map, in particular we prefer to thread it now as otherwise it may become trickier to check when we are using the correct one. Thanks to @SkySkimmer for lots of comments and bug-finding.
* | Removing cumbersome location in multiple patterns.Gravatar Hugo Herbelin2017-12-12
|/ | | | This is to have a better symmetry between CCases and GCases.
* Merge PR #6185: [parser] Remove unnecessary statically initialized hook.Gravatar Maxime Dénès2017-11-21
|\
* \ Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 ↵Gravatar Maxime Dénès2017-11-20
|\ \ | | | | | | | | | (clause "where" with implicit arguments)
| | * [parser] Remove unnecessary statically initialized hook.Gravatar Emilio Jesus Gallego Arias2017-11-19
| |/ |/| | | | | | | | | | | | | | | | | | | | | | | Addded by c6d9d4fb142ef42634be25b60c0995b541e86629 ["Adding ability to put any pattern in binders, prefixed by a quote."] its current placement as well as the hook don't make a lot of sense. In particular, they prevent parts of Coq working without linking the parser. To this purpose, we need to consolidate the `Constrexpr` utilities. While we are at it we do so and remove the `Topconstr` module which is fully redundant with `Constrexpr_ops`.
| * One more step in fixing #5762 ("where" clause).Gravatar Hugo Herbelin2017-11-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We improve one step further the heuristics to sort out if a variable is a notation variable or a named variable. This allows to support the following which was still failing. Reserved Notation "# x" (at level 0). Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I). We rely here on the property that a binding variable of same name as a notation variables is itself considered bound by the notation. This becomes however to be a bit tricky for sorting out if the variable has to be output to the glob file or not.
* | [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|/
* Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" ↵Gravatar Maxime Dénès2017-10-20
|\ | | | | | | clause of an inductive definitions
| * Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).Gravatar Hugo Herbelin2017-10-05
| | | | | | | | | | | | | | | | | | | | | | | | | | This allows e.g. the following to work: Reserved Notation "* a" (at level 70). Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m). We seize this opportunity to make main calls to Metasyntax to depend on an arbitrary env rather than on Global.env. Incidentally, this fixes a little coqdoc bug in classifying the inductive type referred to in the "where" clause.
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
|/ | | | | The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| | | | | | | | | | | | | | | | | | | The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager.
* Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
| | | | Use the functional interface understand_tcc instead.
* Fixing a little location bug with recursive binders.Gravatar Hugo Herbelin2017-07-18
| | | | | | | | | | | | Note that localisation cannot be perfect anyways, as in the following example, where there is no way to highlight in the original input a syntactically stand-alone subterm where the error occurs. > Check forall (y:nat) (x:=0), y. > ^^^^^^^^^^^^^^^^^^^^^^^^ Error: In environment y : nat The term "let x := 0 in y" has type "nat" which should be Set, Prop or Type.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#719: Constrexpr.Numeral without bigintGravatar Maxime Dénès2017-06-15
|\
| * Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)Gravatar Pierre Letouzey2017-06-14
| | | | | | | | | | | | This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml
* | Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* \ Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a ↵Gravatar Maxime Dénès2017-06-06
|\ \ | | | | | | | | | short econstr-cleaning of record.ml