aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
Commit message (Collapse)AuthorAge
...
* Fixing bad comparison in Detyping.Gravatar Pierre-Marie Pédrot2014-03-01
|
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Typo resulting in bad eta-expansion of destructing let's body.Gravatar Hugo Herbelin2013-11-25
| | | | Revealed by message on coq-club on 24/11/2013.
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16921 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
* 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
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16351 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16283 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
* Improving formatting of output of "Test table".Gravatar herbelin2013-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16159 85f007b7-540e-0410-9357-904b9bb8a0f7
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
| | | | | | | | | | | | | native OCaml code. Warning: the "retroknowledge" mechanism has not been ported to the native compiler, because integers and persistent arrays will ultimately be defined as primitive constructions. Until then, computation on numbers may be faster using the VM, since it takes advantage of machine integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of nameGravatar ppedrot2012-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not display REVERTcast inserted by reduction tactics (unless printing all).Gravatar herbelin2012-12-17
| | | | | | Question of printing DEFAULTcast inserted by reduction tactics still open. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16081 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
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15994 85f007b7-540e-0410-9357-904b9bb8a0f7
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
| | | | | | peculiarly messy, I hope I did not introduce too many bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 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
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 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
* Avoid Pp.std_ppcmds in Misctypes.sort_infoGravatar letouzey2012-08-07
| | | | | | | | Otherwise, after a Set Printing Universes we may end on a comparison of Pp.std_ppcmds, which may fail on functional values (cf. Constrextern.check_same_type), as notice by Pierre-Marie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15697 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
* Replacing some str with strbrkGravatar ppedrot2012-06-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15422 85f007b7-540e-0410-9357-904b9bb8a0f7
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
* No more Univ in grammar.cmaGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
* global_reference migrated from Libnames to new Globnames, less deps in ↵Gravatar letouzey2012-05-29
| | | | | | grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
| | | | | | Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
| | | | | | | | | Corresponding operations in locusops.ml and miscops.ml The type of occurrences is now a clear algebraic one instead of a bool*list hard to understand. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | The optimisation done of Namegen.visibly_occur_id did not preserve the previous behavior when pr_constr/constr_extern/detype were called on a term with free rel variables. We backtrack on it to go back to the 8.2 behavior. Seized this opportunity to clarify the meaning of the at_top flag in constrextern.ml and printer.ml and to rename it into goal_concl_style. The badly-named at_top flag was introduced in Coq 6.3 in 1999 to mean that when printing variables bound in the goal, names had to avoid the names of the variables of the goal context, so as to keep naming stable when using "intro"; in r4458, printing improved by not avoiding names that were short names of global definitions, e.g. "S", or "O" (except when the at_top flag was on for compatibility reasons). Other printing strategies could be possible in the non-goal-concl-style mode. For instance, all bound variables could be made distinct in a given expression, even if no clash occur, therefore following so-called Barendregt's convention. This could be done by setting "avoid" to "ids_of_rel_context (rel_context env)" in extern_constr and extern_type (and then, Namegen.visibly_occur_id could be re-simplified again!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
| | | | | | | | | Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a DEPRECATED flag in declaration of options. For now only two options ↵Gravatar ppedrot2011-11-24
| | | | | | are declared as such, but I suspect Coq to contain some more. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | For instance, consider this inductive type: Inductive Ind := A | B | C | D. For detecting "match" on this type, one was forced earlier to write code in Ltac using "match goal" and/or "context [...]" and long patterns such as: match _ with A => _ | B => _ | C => _ | D => _ end After this patch, this pattern can be shortened in many alternative ways: match _ with A => _ | _ => _ end match _ with B => _ | _ => _ end match _ in Ind with _ => _ end Indeed, if we want to detect a "match" of a given type, we can either leave at least one branch where a constructor is explicit, or use a "in" annotation. Now, we can also detect any "match" regardless of its type: match _ with _ => _ end Note : this will even detect "match" over empty inductive types. Compatibility should be preserved, since "match _ with end" will continue to correspond only to empty inductive types. Internally, the constr_pattern PCase has changed quite a lot, a few elements are now grouped into a case_info_pattern record, while branches are now lists of given sub-patterns. NB: writing "match" with missing last branches in a constr pattern was actually tolerated by Pattern.pattern_of_glob_constr earlier, since the number of constructor per inductive is unknown there. And this was triggering an uncaught exception in a array_fold_left_2 in Matching later. Oups. At least this patch fixes this issue... Btw: the code in Pattern.pattern_of_glob_constr was quadratic in the number of branch in a match pattern. I doubt this was really a problem, but having now linear code instead cannot harm ;-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14644 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14621 85f007b7-540e-0410-9357-904b9bb8a0f7
* This is exactly the structure needed to handle controlling printingGravatar herbelin2011-07-16
| | | | | | | | of terms of record type with record or constructor syntax. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14285 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug in printing let-in binders in fix/cofixGravatar herbelin2011-04-24
| | | | | | (backport from branch v8.3) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14055 85f007b7-540e-0410-9357-904b9bb8a0f7
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
| | | | | | | | | perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\ W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s /glob_terms?/glob_constr/g' **/*.ml* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | There was a discrepancy of the notions "raw" and "globalized" between constrs and tactics, and some confusion of the notions in e.g. genarg.mli (see all globwit_* there). This commit is a first step towards unification of terminology between constrs and tactics. Changes in module names will be done separately. In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even affected by this change, has not been touched and highlights another confusion in "ARGUMENT EXTEND" in general that will be addressed later. The funind plugin doesn't respect the same naming conventions as the rest, so leave some "raw" there for now... they will be addressed later. This big commit has been generated with the following command (wrapped here, but should be on a *single* line): perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder| _context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G \2/g' `git ls-files|grep -v dev/doc/changes.txt` git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
| | | | | | | | | | | | | - Added support for recursive notations with binders - Added support for arbitrary large iterators in recursive notations - More checks on the use of variables and improved error messages - Do side-effects in metasyntax only when sure that everything is ok - Documentation Note: it seems there were a small bug in match_alist (instances obtained from matching the first copy of iterator were not propagated). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2279 (printing nested let-in was in exponential time)Gravatar herbelin2010-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12887 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed confusion between number of cstr arguments and number of pattern ↵Gravatar barras2010-03-12
| | | | | | variables (which include let-ins in cstr type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12608 85f007b7-540e-0410-9357-904b9bb8a0f7
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
| | | | | | | | | | | | | | | | | | | | | | - backtrack on incompatibility introduced in intro while trying to simplify the condition about when to restart the subscript of a name (the legacy says: find a new name from x0 if the name xN exists in the context but find a new name from xN+1 if the name xN does not exists in the context but is a global to avoid). - made the names chosen by "intro" compliant with the ones printed in the goal and used for "intros until" (possible source of rare incompatibilities) [replaced the use of visibly_occur_id for printing the goal into a call to next_name_away_in_goal] - also made the names internal to T in "T -> U" printed the same in the goal as they are while printing T after it is introducted in the hypotheses [non contravariant propagation of boolean isgoal in detype_binder] - simplified a bit visibly_occur_id (the Rel and Var cases were useless as soon as the avoid list contained the current env); still this function is costly with polynomial time in the depth of binders - see file output/Naming.v for examples git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12549 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 23:49:55 +0000