aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Collapse)AuthorAge
* Abstracting evar filter away. The API is not perfect, but better than nothing.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16939 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small optimizations in unification.Gravatar ppedrot2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless array-to-list and converse casts used inGravatar ppedrot2013-10-22
| | | | | | Evar{conv,solve} files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16913 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing evar filters. It seems to cost quite a lot in unification,Gravatar ppedrot2013-10-22
| | | | | | | as witnessed by profiling on time-consuming files. I suspect we can do better by using a smarter representation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16912 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵Gravatar xclerc2013-09-19
| | | | | | with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
| | | | | | | | | | | | casts of ints to evars. - 2 in Evarutil and Goal which are really needed, even though the Goal one could (and should) be removed; - 2 in G_xml and Detyping that are there for completeness sake, but that might be made anomalies altogether; - 1 in Newring which is quite dubious at best, and should be fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16786 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not compute fallback eagerly in EvarconvGravatar pboutill2013-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16546 85f007b7-540e-0410-9357-904b9bb8a0f7
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Clarification of the existence of three algorithms for solving unconstrained evars: - the type-class mechanism - the heuristics for solving pending conversion problems and multi-candidates - Declare Implicit Tactic (when called from tactics) Main function for solving unconstrained evars (when not using understand): Pretyping.solve_remaining_evars - Clarification of the existence of three corresponding kinds of errors when reporting about unsolved evars: Main function for checking resolution of evars independently of the understand functions: Pretyping.check_evars_are_solved - Introduction of inference flags in pretyping for governing which combination of the algorithms to use when calling some understand function; there is also a flag of expanding or not evars and for requiring or not the resolution of all evars - Less hackish way of managing Pretyping.type_constraint: all three different possibilities are now represented by three different constructors - Main semantical changes done: - solving unconstrained evars and reporting is not any longer mixed: one first tries to find unconstrained evars by any way possible; one eventually reports on the existence of unsolved evars using check_evars_are_solved - checking unsolved evars is now done by looking at the evar map, not by looking at the evars occurring in the terms to pretype; the only observed consequence so far is in Cases.v because of subterms (surprisingly) disappering after compilation of pattern-matching - the API changed, see dev/doc/changes.txt Still to do: - Find more uniform naming schemes: - for distinguishing when sigma is passed as a reference or as a value (are used: suffix _evars, prefix e_) - for distinguishing when evars are allowed to remain uninstantiated or not (are used: suffix _evars, again, suffix _tcc, infix _open_) - be more consistent on the use of names evd/sigma/evars or evdref/evars - By the way, shouldn't "understand" be better renamed into "infer" or "preinfer", or "pretype". Grammatically, "understanding a term" looks strange. - Investigate whether the inference flags in tacinterp.ml are really what we want (e.g. do we really want that heuristic remains activated when typeclasses are explicitly deactivated, idem in Tacinterp.interp_open_constr where flags are strange). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7
* Small cleaning of Evd interface.Gravatar ppedrot2013-05-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
| | | | | | | | | | | | | | | | | 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix of r16257 in r16205 for "errors raised by check_evar_instance wereGravatar herbelin2013-04-17
| | | | | | | | | | | | no longer trapped by solve_simple_eqn" was incomplete because "try ... with E as e | e when f e -> ..." means "try ... with (E as e | e) when f e -> ..." and not "try ... with E as e | (e when f e) -> ...". This was the cause for examples 2615.v and 2670.v failing since March 1. The need for "as e" should have warned me. Sorry for the mistake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Like in r16346, do not filter local definitions (here in theGravatar herbelin2013-04-17
| | | | | | | | | | | | | | type-based second-order unification algorithm). In type-based second-order unification algorithm, protect local definitions in instances of evars to wrongly be considered as potentially flexible. Altogether, this fixes the anomaly in #3003 (even if some additional work has to be done to improve the resulting error message, see next commit). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16414 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuation of r16346 on filtering local definitions. RefinedGravatar herbelin2013-03-30
| | | | | | | | | | | | the "choose less dependent" constraint-solving heuristic so that it is not disturbed by local definitions. This is a quick fix. A deeper analysis of the structure of constraints of the form ?x[args] = y, determining if variable y can itself be a local def or not, and whether args can be let-ins aliasing other variables, would allow to know if the fix needs to be refined further. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2989: make unification.ml able to deal with canonical structure in ↵Gravatar pboutill2013-03-25
| | | | | | | | any context + reindenting noise git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16289 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphization.Gravatar ppedrot2013-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16260 85f007b7-540e-0410-9357-904b9bb8a0f7
* compare_stack_shape before ise_stack2 in evar_convGravatar pboutill2013-02-28
| | | | | | + revert r16130 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
| | | | | | trapped by solve_simple_eqn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv: When doing a iota of a fixpoint, use constant name instead of ↵Gravatar pboutill2013-02-25
| | | | | | | | fixpoint definition + Help the use of #trace on evar_conv_appr_x git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16244 85f007b7-540e-0410-9357-904b9bb8a0f7
* A more informative message when the elimination predicate forGravatar herbelin2013-02-17
| | | | | | | | | | | | destruct, rewrite, etc. is not well-typed. Also added support for a more informative message when the elimination predicate is not well-formed while using the smart "second-order" unification algorithm. However the "abstract_list_all" algorithm seems to remain more informative though, so we still use this algorithm for reporting about ill-typed predicates. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7
* Locating errors from consider_remaining_unif_problems if possibleGravatar herbelin2013-02-17
| | | | | | | (useful when consider_remaining_unif_problems not called via pretyping.ml, as e.g. from command.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16206 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
| | | | | | | | error messages. The architecture of unification error handling changed, not helped by ocaml for checking that every exceptions is correctly caught. Report or fix if you find a regression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16205 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envGravatar herbelin2013-01-29
| | | | | | for better uniformity of naming policy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16172 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Fix evarconv so that we have complete eta-conversion:Gravatar msozeau2013-01-22
| | | | | | | | | | | - In the maybeflex/rigid (lambda) case, try eta if the maybeflex doesn't actually unfold (e.g. vars, or the transparent state says it's opaque). - In the flexible/rigid(lambda) case, try eta if miller-pfenning fails (as the stack might not be a purely applicative one). This will zip the flexible term (a case construct most likely) and try eta expansion on it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv: Check stack before term in Canonical Structure approuvalGravatar pboutill2013-01-18
| | | | | | | 3 days of work to swap 2 lines ... but this fixes LemmaOverloading (and hopfully makes Feit-Thomson compilation time back to "normal") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16130 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops reduction machine can refold constantGravatar pboutill2012-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv.Pseudorigid erasureGravatar pboutill2012-12-19
| | | | | | flex_kind is computed from the real term that blocks the reduction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved Intset and Intmap to Int namespace.Gravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evarconv: Fix #2936 + commentsGravatar pboutill2012-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning and small optimization in CList.Gravatar ppedrot2012-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15988 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
| | | | | | | | | List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
| | | | | | | | | | compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
* Unification in Evar_conv uses an abstract machine stateGravatar pboutill2012-08-09
| | | | | | | | | It uses a term in front of a stack instead of a term in front of a list of applied terms. From outside of eq_appr_x nothing should have changed. Nasty evar instantiation bug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops refactoringGravatar pboutill2012-07-20
| | | | | | | | | | | Semantic changes are : - whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack didn't. - Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and cofix. - simpl uses its own whd_ function that do not touch at matched term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
* flex_maybeflex factoringGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15618 85f007b7-540e-0410-9357-904b9bb8a0f7
* miller_pfenning unification code factoringGravatar pboutill2012-07-12
| | | | | | Mind that the behavior of MaybeFlexible, Flexible changes \! (we solve_pattern_eqn using the new list and not the old one) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15617 85f007b7-540e-0410-9357-904b9bb8a0f7
* flex_kind_of_term does not have a copy of termGravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15616 85f007b7-540e-0410-9357-904b9bb8a0f7
* evar reduction is already made by whd_*Gravatar pboutill2012-07-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
| | | | | | | | | | were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2791 by doing a fixpoint computation in consider_remaining_problems:Gravatar msozeau2012-06-21
| | | | | | | take care of checking progress when solving the remaining problems, distinguishing between solved and stuck conversions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing use of an error instead of a boolean result in the unificationGravatar herbelin2012-06-20
| | | | | | | | subroutine choose_less_dependent_instance. This might solve bug #2495 (only "might solve" because the bug does not come with a reproducible example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15461 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reductionops : Better abstract machine stack utilitiesGravatar pboutill2012-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15443 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 15:35:56 +0000