aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
Commit message (Collapse)AuthorAge
* Swapping Context and Constr: defining declarations on constr in Constr.Gravatar Hugo Herbelin2018-06-27
| | | | | | | | | This shall eventually allow to use contexts of declarations in the definition of the "Case" constructor. Basically, this means that Constr now includes Context and that the "t" types of Context which were specialized on constr are not defined in Constr (unfortunately using a heavy boilerplate).
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
|
* Define and use UGraph.enforce_leq_alg for subtyping inferenceGravatar Gaëtan Gilbert2018-06-22
| | | | Not sure if worth using in other places.
* Define rec_declaration in terms of prec_declaration.Gravatar SimonBoulier2018-06-05
| | | | And similarly for fixpoint and cofixpoint.
* Fix #7631: native_compute fails to compile an example in Coq 8.8Gravatar Maxime Dénès2018-06-04
| | | | | Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
* Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.Gravatar Hugo Herbelin2018-05-23
|
* Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
|
* [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.
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
| | | | | | | | | | | | | | | | | | | | | | | | Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative inductive would try to generate a constraint [i = j] and use cumulativity only if this resulted in an inconsistency. This is confusingly different from the behaviour with [Type] and means cumulativity can only be used to lift between universes related by strict inequalities. (This isn't a kernel restriction so there might be some workaround to send the kernel the right constraints, but not in a nice way.) See modified test for more details of what is now possible. Technical notes: When universe constraints were inferred by comparing the shape of terms without reduction, cumulativity was not used and so too-strict equality constraints were generated. Then in order to use cumulativity we had to make this comparison fail to fall back to full conversion. When unifiying 2 instances of a cumulative inductive type, if there are any Irrelevant universes we try to unify them if they are flexible.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Safer VM interfacesGravatar Maxime Dénès2018-01-26
| | | | | | | | | | | | We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.
* Merge PR #486: Make some functions on terms more robust w.r.t new term ↵Gravatar Maxime Dénès2017-11-24
|\ | | | | | | constructs.
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
| | | | | | | | | | | | Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* | [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
|/ | | | | | | We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | This will allow to merge back `Names` with `API.Names`
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
|\
* | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| |
* | Fix for bug 5507. Mispelt de Bruijn.Gravatar Théo Zimmermann2017-05-01
| |
* | Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
|\ \ | | | | | | | | | let-ins
| | * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| |/ |/|
| * Documenting how the recursive indices of a fixpoint are computed.Gravatar Hugo Herbelin2017-04-09
| | | | | | | | Also documenting how the implicit arguments by position are computed.
* | Make the Constr.kind_of_term type parametric in sorts and universes.Gravatar Pierre-Marie Pédrot2017-03-31
| |
* | Introducing a new EConstr.t type to perform the nf_evar operation on demand.Gravatar Pierre-Marie Pédrot2016-11-08
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2016-03-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | COMMENTS: of "Constr.case_info" type were updated.Gravatar Matej Kosik2016-01-11
| |
* | COMMENTS: added to the "Constr.case_info" type.Gravatar Matej Kosik2015-12-18
| |
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
| | | | | | | | | | 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
| * Adding eq/compare/hash for syntactic view atGravatar Hugo Herbelin2015-08-02
|/ | | | | | | | | | | | | | | constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same.
* Tactical `progress` compares term up to potentially equalisable universes.Gravatar Arnaud Spiwack2015-04-22
| | | | | Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
* New function [Constr.equal_with] to compare terms up to variants of ↵Gravatar Arnaud Spiwack2015-02-24
| | | | | | | | [kind_of_term]. To be able to write equality up to evar instantiation instantiation. Generalises the main function of [eq] constr over the variant of [kind_of_term] it uses. It prevents some optimisation of [Array.equal] where two physically equal arrays are considered (less or) equal. But it does not seem to have appreciable effects on efficiency.
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
| | | | [compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Fix (actually, properly implement :) hashconsing of projections,Gravatar Matthieu Sozeau2014-12-17
| | | | | resulting in huge speedup at Qed/section closing in presence of primitive projections.
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
|
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
| | | | | | | | so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
| | | | function, so plain pointer equality is sufficient.
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
|
* Cleanup in Univ, moving code for UniverseConstraints outside the kernel in ↵Gravatar Matthieu Sozeau2014-06-10
| | | | | | | | Universes. Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes. Remove unused functions from univ as well and refactor a little bit. Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.
* Make kernel reduction code parametric over the handling of universes,Gravatar Matthieu Sozeau2014-06-06
| | | | | | | | | | | allowing fast conversion to be used during unification while respecting the semantics of unification w.r.t universes. - Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv is used for module subtyping. - Outside, infer_conv is wrapped in Reductionops to register the right constraints in an evarmap. - In univ, add a flag to universes to cache the fact that they are >= Set, the most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS).
* Update infer_conv to record trivial Prop <= Type i constraints that are ↵Gravatar Matthieu Sozeau2014-05-26
| | | | | | needed during unification.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:13:37 +0000