aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Collapse)AuthorAge
* Move solve_constraint_system near its only use site (comInductive)Gravatar Gaëtan Gilbert2018-05-17
|
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
|
* Split off Universes functions dealing with names.Gravatar Gaëtan Gilbert2018-05-17
| | | | This API is a bit strange, I expect it will change at some point.
* Make set minimization option internal to UniversesGravatar Gaëtan Gilbert2018-05-17
|
* Merge PR #7359: Reduce usage of evar_map referencesGravatar Pierre-Marie Pédrot2018-05-17
|\
| * Use evd_combX in Cases.Gravatar Gaëtan Gilbert2018-05-14
| |
| * Convert clear_hyps_in_evi to state passing style.Gravatar Gaëtan Gilbert2018-05-11
| |
| * Deprecate most evarutil evdref functionsGravatar Gaëtan Gilbert2018-05-11
| | | | | | | | clear_hyps remain with no alternative
* | Don't use ref universe_opt_substGravatar Gaëtan Gilbert2018-05-08
|/
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* Merge PR #7375: Implement to_constr with nf_evars_and_universes_opt_substGravatar Pierre-Marie Pédrot2018-05-03
|\
* \ Merge PR #6935: Separate universe minimization and evar normalization functionsGravatar Pierre-Marie Pédrot2018-04-30
|\ \
| | * Implement to_constr with nf_evars_and_universes_opt_substGravatar Gaëtan Gilbert2018-04-29
| | |
| | * Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evarsGravatar Gaëtan Gilbert2018-04-28
| |/ |/|
* | Merge PR #6892: Cleanup implementation of normalize_context_set a bitGravatar Pierre-Marie Pédrot2018-04-28
|\ \
* \ \ Merge PR #6866: Slight improvement of messages related to direct and ↵Gravatar Pierre-Marie Pédrot2018-04-25
|\ \ \ | | | | | | | | | | | | indirect uses of tactic `clear`.
* \ \ \ Merge PR #307: Adding a flag to support different naming modes for evar ↵Gravatar Pierre-Marie Pédrot2018-04-24
|\ \ \ \ | | | | | | | | | | | | | | | hypotheses.
| | * | | Improving error message for clear tactic (and indirect uses of it).Gravatar Hugo Herbelin2018-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Be more precise when trying to clear an hypothesis which occurs implicitly in a global constant. - Warns if destruct/induction cannot clear an hypothesis occurring implicitly in a global. In the first case, the change in situation Section A. Variable a:nat. Definition b:=a=a. Goal b=b. clear a. is: - before: "a is used in conclusion" - after: "a is used implicitly in b in conclusion" In the second case: Section A. Variable a:nat. Definition b:=a=a. Goal b=b. destruct a. produces a warning: "Cannot remove a, it is used implicitly in b".
| * | | | Adding a flag to support different naming modes for evar hypotheses.Gravatar Hugo Herbelin2018-04-24
| |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Four modes currently supported to deal with clashes: 1. Failing in case of clash 2. Renaming the most recent one 3. Renaming the previous hypothesis of same name if not a section variable 4. Renaming the previous hypothesis of same name even if a section variable The current mode is 3. Keeping it active by default
* / / / [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In a component-based source code organization of Coq `intf` doesn't fit very well, as it sits in bit of "limbo" between different components, and indeed, encourages developers to place types in sometimes random places wrt the hierarchy. For example, lower parts of the system reference `Vernacexpr`, which morally lives in a pretty higher part of the system. We move all the files in `intf` to the lowest place their dependencies can accommodate: - `Misctypes`: is used by Declaremod, thus it has to go in `library` or below. Ideally, this file would disappear. - `Evar_kinds`: it is used by files in `engine`, so that seems its proper placement. - `Decl_kinds`: used in `library`, seems like the right place. [could also be merged. - `Glob_term`: belongs to pretyping, where it is placed. - `Locus`: ditto. - `Pattern`: ditto. - `Genredexpr`: depended by a few modules in `pretyping`, seems like the righ place. - `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and could be fixed, as this module should be declared in `interp` which is the one eliminating it. - `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed as it contains stuff it shouldn't. The right place should be `parsing`. - `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`. - `Notation_term`: First place used is `interp`, seems like the right place. Additionally, for some files it could be worth to merge files of the form `Foo` with `Foo_ops` in the medium term, as to create proper ADT modules as done in the kernel with `Name`, etc...
| | * Deprecate mixing univ minimization and evm normalization functions.Gravatar Gaëtan Gilbert2018-04-17
| |/ |/| | | | | Normalization sounds like it should be semantically noop.
| * univ minimization: comment [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization [enforce_upper]: replace Option.get with matchGravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: Partially let-lift [enforce_uppers]Gravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: rename acc' -> enforce_uppersGravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: use shadowing moreGravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | This avoids having multiple highly similar things in scope when we only want one of them.
| * univ minimization: let-lift [not_lower]Gravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: simplify try-with block around find_instsGravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/Gravatar Gaëtan Gilbert2018-04-13
| |
| * univ minimization: simplify try-with block around [find u left]Gravatar Gaëtan Gilbert2018-04-13
| | | | | | | | This makes it clear where the Not_found can come from.
| * univ minimization: comment compare_constraint_typeGravatar Gaëtan Gilbert2018-04-13
| |
| * niv minimization: remove [remove_lower] abbreviationGravatar Gaëtan Gilbert2018-04-13
| | | | | | | | | | It's not long, used only once and it's easier to understand what it does when it's inlined.
| * minimize_univ_variables: bool*bool*univ*lowermap replaced by recordGravatar Gaëtan Gilbert2018-04-13
| |
| * minimize_univ_variables: remove [and right] abbreviation.Gravatar Gaëtan Gilbert2018-04-13
| |
| * universe normalisation: put equivalence class partition in UGraphGravatar Gaëtan Gilbert2018-04-13
| | | | | | | | ie don't go through having Eq constraints but directly to the unionfind.
| * universe minimization: cleanup using standard combinators, open UnivGravatar Gaëtan Gilbert2018-04-13
| | | | | | | | eg Constraint.partition + filter instead of a complicated fold.
* | Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
|/ | | | | | We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr.
* Merge PR #6454: [econstr] Flag to make `to_constr` fail if its output ↵Gravatar Pierre-Marie Pédrot2018-04-13
|\ | | | | | | contains evars
* \ Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Gravatar Maxime Dénès2018-04-12
|\ \
| | * [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
| * | [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
| |/
* | Export Proofview.undefined as "unsafe" primitive.Gravatar Hugo Herbelin2018-03-27
| |
* | Adding informative variant of shelve_unifiable returning set of shelved evars.Gravatar Hugo Herbelin2018-03-27
|/
* Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| | | | For instance, error in "Goal forall a f, f a = 0" is now located.
* [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.
* Adjust EConstr.cmp_constructors for relaxed constructor cumulativityGravatar Gaëtan Gilbert2018-03-09
|
* Delayed weak constraints for cumulative inductive types.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | When comparing 2 irrelevant universes [u] and [v] we add a "weak constraint" [UWeak(u,v)] to the UState. Then at minimization time a weak constraint between unrelated universes where one is flexible causes them to be unified.
* Statically enforce that ULub is only between levels.Gravatar Gaëtan Gilbert2018-03-09
|
* Option for messing with inference of irrelevant constraintsGravatar Gaëtan Gilbert2018-03-09
|
* Cumulativity: improve treatment of irrelevant universes.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | In Reductionops.infer_conv we did not have enough information to properly try to unify irrelevant universes. This requires changing the Reduction.universe_compare type a bit.