aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
Commit message (Collapse)AuthorAge
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
| | | | parsing is plugged.
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
| | | | | | of tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 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
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 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
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 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
* 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
* Revise API of understand_ltac to be parameterized by a flag for resolution ↵Gravatar msozeau2012-03-14
| | | | | | | | | of evars. Used when interpreting a constr in Ltac: resolution is now launched if the constr is casted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 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
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
| | | | | | | resolution from Tacinterp to Pretyping (close to resolve_evars) so that final evar resolution can eventually be called from Tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14496 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
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
| | | | | | | | | | | | | | | | | | - Instances found by matching.ml now collect the set of bound variables they possibly depend on in the pattern (see type Pattern.extended_patvar_map); the variables names are canonically ordered so that non-linear matching takes actual names into account. - Removed typing of matching constr instances in advance (in tacinterp.ml) and did it only at use time (in pretyping.ml). Drawback is that we may have to re-type several times the same term but it is necessary for considering terms with locally bound variables of which we do not keep the type (and if even we had kept the type, we would have to adjust the indices to the actual context the term occurs). - A bit of documentation of pattern.mli, matching.mli and pretyping.mli. - Incidentally add env while printing idtac messages. It seems more correct and I hope I did not break some intended existing behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13080 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 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
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
| | | | | | | | | | | | | | | - to type patterns w/o losing the information of what subterm is a hole would need to remember where holes were in "understand", but "understand" needs sometimes to instantiate evars to ensure the type of an evar is not its original type but the type of its instance (what can e.g. lower a universe level); we would need here to update evars type at the same time we define them but this would need in turn to check the convertibility of the actual and expected type since otherwise type-checking constraints may disappear; - typing pattern is apparently expensive in time; is it worth to do it for the benefit of pattern-matching compilation and coercion insertion? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12607 85f007b7-540e-0410-9357-904b9bb8a0f7
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for r12197, the refined evars were not returned in case fail_evarGravatar msozeau2009-06-22
| | | | | | | was true. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12206 85f007b7-540e-0410-9357-904b9bb8a0f7
* - New cleaning phase for the entry points of pretyping.mlGravatar herbelin2009-04-24
| | | | | | | | | | | | | | | | | | | | | | | - Uniformisation of ML names between pretyping.ml and subtac_pretyping_F.ml so as to ease the comparison between these files. Application of a change that cannot do harm: j_nf_evar now called after getting evd from consider_remaining_unif_problems in Subtac_pretyping_F.understand_judgment. Four differences remain (is it the sign of a problem?): 1) understand_type fails in Pretyping if evars remain but does not fail in Subtac_pretyping_F 2) resolve_typeclasses (when called) is called with ~onlyargs:false and ~fail:true in Pretyping.understand, Pretyping.understand_gen and Pretyping.understand_type but with true and false in these same functions in Subtac_pretyping_F 3) understand_ltac does not call typeclasses in Pretyping but it does call it in Subtac_pretyping_F 4) understand_judgment does call typeclasses in Pretyping but not in Subtac_pretyping_F git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
| | | | | | | typeclass code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11047 85f007b7-540e-0410-9357-904b9bb8a0f7
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
| | | | | | | | | | | | | | | | | | | | | | | | all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de l'heuristique d'unification premier ordre flexible/rigideGravatar herbelin2006-09-15
| | | | | | | | | | | | en dernière étape de la procédure d'unification - Nouvelle fonction consider_remaining_unif_problems dédiée à la résolution de l'unification premier ordre flexible/rigide - Déplacement check_evars dans Evarutil Question ouverte: que faire pour l'unif premier ordre flexible/semiflexible ? (cf exemples d'application dans test-suite/success/evars.v) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de check_evars vers command.mlGravatar herbelin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9105 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
| | | | | | | | | | - Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵Gravatar msozeau2006-03-22
| | | | | | | | | | on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made pretyping a functor over a coercion implementation. Pretyping.Default ↵Gravatar msozeau2006-03-22
| | | | | | | | | | | uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.Gravatar msozeau2006-03-13
| | | | | | | | May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des points d'entrée de Pretyping et ConstrinternGravatar herbelin2005-12-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Léger nettoyage et uniformisation + généralisation du point d'entrée ↵Gravatar herbelin2005-09-09
| | | | | | ltac pour qu'il retourne les evar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7361 85f007b7-540e-0410-9357-904b9bb8a0f7
* inclusion de meta_map dans evar_defsGravatar barras2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amelioration message d'erreur pour ltacGravatar herbelin2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression définitive de lmatch et or_metanum dans tacinterpGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
* - modifs de la condition de garde pour mieux tenir compte des raisonnementsGravatar barras2002-04-02
| | | | | | | | | | par l'absurde - un open_constr est maintenant un terme accompagne du sigma dans lequel il est typable (il manquait l'info concernant le contexte de typage des nouvelles evars) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des local_constraints, des ctxtty et du focus.Gravatar clrenard2001-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de dynamiques pour les quotations constr et tacticGravatar delahaye2001-10-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2093 85f007b7-540e-0410-9357-904b9bb8a0f7
* amelioration de la structure des universGravatar barras2001-03-28
| | | | | | | | elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 21:04:51 +0000