aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Collapse)AuthorAge
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
| | | | For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
| | | | | For better error messages. The API change is backwards compatible, using a new optional argument.
* Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
| | | | | | | We unify types of let-ins in FO heuristic before their bodies, using cumulativity in either direction. This maintains the invariant that we are comparing terms in related types throughout unification. Also adapt test-suite file for bug #3929.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\
| * evar_conv: Refine occur_rigidlyGravatar Matthieu Sozeau2016-06-13
| | | | | | | | | | | | | | This avoids postponing constraints which will surely produce an occur-check and allow to backtrack on first-order unifications producing those constraints directly (e.g. to apply eta). (fixes HoTT/HoTT with 8.5).
| * Minor simplification in evarconv.Gravatar Hugo Herbelin2016-06-12
| | | | | | | | | | | | Function default_fail was always part of an ise_try. Its associated error message was anyway thrown away. It is then irrelevant and could be made simpler.
| * Protecting eta-expansion in evarconv.ml against ill-typed problems.Gravatar Hugo Herbelin2016-06-12
| | | | | | | | | | | | This can happen with the "with" clause (see e.g. #4782), but also with recursive calls in first-order unification (e.g. "?n a a b = f a" when a matching between "b" and "a" is tried before expanding f).
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\|
| * Fixing #4644 (regression of unification on evar-evar problems with a match).Gravatar Hugo Herbelin2016-06-09
| | | | | | | | | | Typically, a problem of the form "?x args = match ?y with ... end" was a failure even if miller-unification was applicable.
| * Minor simplification in evarconv.ml.Gravatar Hugo Herbelin2016-06-09
| |
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
* | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
| | | | | | | | | | Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \
| | * Fix incorrect behavior of CS resolutionGravatar Matthieu Sozeau2016-03-16
| |/ | | | | | | | | | | | | | | | | | | Due to a change in pretyping, using cast annotations as typing constraints, the canonical structure problems given to the unification could contain non-evar-normalized terms, hence we force evar normalization where necessary to ensure the same CS solutions can be found. Here the dependency test is fooled by an erasable dependency, and the following resolution needs a independent codomain for pop b to be well-scoped.
| * Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
| | | | | | | | | | | | | | | | | | E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive records with eta for which conversion is incomplete. - Eta-conversion only applies to BiFinite inductives - Finiteness information is now checked by the kernel (the constructor types must be strictly non recursive for BiFinite declarations).
* | Slightly contracting code of evarconv.ml.Gravatar Hugo Herbelin2016-02-28
| |
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| | | | | | | | | | | | | | | Some functions were left in the old paradigm because they are only used by the unification algorithms, so they are not worthwhile to change for now.
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
| |
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
| |
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| | | | | | | | | | | | The evar counter has been moved from Evarutil to Evd, and all functions in Evarutil now go through a dedicated primitive to create a fresh evar from an evarmap.
| * 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.
| * Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
| | | | | | | | of arguments of eta_constructor.
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| | | | | | | | naming of arguments of eta.
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| |
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| |
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
|/
* Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
| | | | | because of the name of a bound variable lost when unifying under a binder in evarconv.
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
| | | | | | | | Indeed, the name of a bound variable was lost when unifying under a Prod in evarconv. The error message for "Unable to satisfy the following constraints" is still to be improved though.
* Some dead code.Gravatar Hugo Herbelin2015-04-21
|
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
| | | | unification fails due to that, during a conversion step.
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
| | | | | | | | | | | | | | | | | Unifying two let-in's expresions syntactically is a heuristic (compared to performing the zeta-reduction). This heuristic was requiring unification of types which is too strong for the heuristic to work uniformly since the types might only be related modulo subtyping. The patch is to remove the unification of types, which allows then to have the heuristic work uniformly on the bodies. On the other side, I hope it does not loose (still heuristical) unifications compared to before (presumably, since instantiating the evars in the body will induce constraints for solving potential evars in the types of the let-in bodies, but this would need a proof). Anyway, it is not about correction, it is about a heuristic, which maybe done too early actually.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
| | | | | | typed-based matching: it provokes a stack overflow in contrib ClassicalRealisability. To be investigated later on. (See 893a02f643858ba0b0172648e77af9ccb65f03df.)
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06
| | | | 3cd718c, to the case of second_order_matching.
* Fixing old filter bug in second_order_matching.Gravatar Hugo Herbelin2015-01-06
|
* Tentatively trying to restore the use of second-order typed-basedGravatar Hugo Herbelin2015-01-03
| | | | | | unification algorithm in consider_remaining_unif_problems. If it happens to be problematic, one can backtrack to the "optimization" from 3bd9cb26b which has a restriction on rels/vars.
* An optimization in the use of unification candidates so as to get theGravatar Hugo Herbelin2015-01-01
| | | | | | following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
* Simplifying second_order_matching: no need to invert the linearGravatar Hugo Herbelin2014-12-30
| | | | initial segment of the context of the evar.
* Documenting check_record + changing a possibly undefined int into int option.Gravatar Hugo Herbelin2014-12-15
|
* Two fixes in unification (bugs #3782 and #3709)Gravatar Matthieu Sozeau2014-12-12
| | | | | | | | - In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
* Fine-tuning unification error (using OccurCheck in evarconv).Gravatar Hugo Herbelin2014-12-11
|
* Setup hook to change the unification algorithm used by evarconv,Gravatar Matthieu Sozeau2014-12-09
| | | | e.g. for MTac.
* Being consistent in making arbitrary choices in recursive calls toGravatar Hugo Herbelin2014-12-02
| | | | | | | | | evar_define. Interestingly, the added choose in evarconv.ml allows solve_evar_evar to be observationally commutative, in the sense of not either fail or succeed in compiling the stdlib whether problems are given in the left-to-right or right-to-left order.
* Option -type-in-type continued (deactivate test for inferred sort ofGravatar Hugo Herbelin2014-11-19
| | | | | inductive types + deactivate test for equality of sort + deactivate the check that the constraints Prop/Set <= Type are declared).
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 23:57:25 +0000