aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Collapse)Author
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
- 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
2013-05-09Removing Gmap from Notations.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16494 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-08Alert when using ".." outside a Notation command.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16488 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-06States: frozen states can hold closuresgareuselesinge
States.freeze takes ~marshallable:bool, so that (only) when we want to marshal data to disk/network we can ask the freeze functions of the summary to force lazy values. The flag is propagated to Lib and Summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
full usage of notations instead of the previous cheap way to prevent circularity in printing by deactivating all notations. (Since "->" became a notation, printing abbreviations without notations at all had become even more inconvenient). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16470 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-05-05Relaxing the constraint on eta-expanding on the fly while looking forherbelin
notation to use at printing time. We now allow to print "sigT P" as "{x:_ & P x}", generating a "_" for the missing type, when the notation is defined by 'Notation "{ x : A & P }" := (sigT (fun x:A => P))'. Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so that the type is known even when eta-expansion is needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Merging Context and Sign.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
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
2013-04-25Coqide: Globalization feedback (proof of concept)gareuselesinge
A new feedback message for globalization infos can be sent by Coq to Coqide. Coqide stores the information in the proof of concept module wg_Tooltip, that also sets things up so that these infos are displayed as a tooltip when the mouse is over the text they are attached to. These infos are available only on locked text, and on the text just processed in the case of an error (on this piece of text, they vanish as the error tag vanishes as soon as the user edits the text). wg_Tooltip stocks these infos as lazy string. This is not needed in the proof of concept, but is necessary to scale up: Coq may not generate the full piece of info when the message is sent (because of high computational cost or big size) and just send an id; later on, when/if the user asks for the piece of info, the gui requests the info explicitly using the id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16456 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-23minor cleanup in coqtop.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16445 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-22code simplifications concerning Summaryletouzey
- Most of the time, the table registered via Summary.declare_summary is just a single reference. A new function Summary.ref now allows to both declare this ref and register it to summary in one shot. - Clarifications concerning the role of [init_function]. For statically registered tables that don't need a special initializer, just do nothing there (see the new Summary.nop function). Beware: now that Summary exports a function named "ref", any code that do an "open Summary" will probably fail to compile. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16441 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-21Robust display of NotConvertibleTypeField errors (fix #3008, #2995)letouzey
Since the nametab isn't aware of everything needed to print mismatched types (cf the bug test-cases), we create a robust term printer that known how to print a fully-qualified name when [shortest_qualid_of_global] has failed. These Printer.safe_pr_constr and alii are meant to never fail (at worse they display "??", for instance when the env isn't rich enough). Moreover, the environnement may have changed between the raise of NotConvertibleTypeField and its display, so we store the original env in the exception. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16342 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-19Removing the module Libtypes and unifying the Search[Pattern|Rewrite]?ppedrot
mechanism with the SearchAbout one. Searches may be slower, but this is unlikely to be noticed. In addition, according to Hugo, the Libtype summary was imposing a noticeable time penalty without any real advantage. Now Search and SearchPattern are the same. The documentation was not really clear about the difference between both, except that Search was restricted to closed terms. This is an artificial restriction by now. Fixing #2815 btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16320 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-15Extract_env : correct exceptions mentionned in a try ... withletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16306 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
After some investigation, I see no reason to try to hack the nametab in ppvernac, since everything happens there at a lower level (constr_expr). So the offending code that Enrico protected with a State.with_state_protection is now gone. By the way, moved some types from Declaremods to Vernacexpr to avoid some dependencies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16300 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Implicit_quantifiers.is_freevar: cleaner, no more try...with _ ->...letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16279 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 3)letouzey
NB: this "try...with" plus the test at the next line (if !interning_grammar || env.unb then ...) were actually catching too many errors (for instance error_not_enough_arguments). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16278 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12Hipattern : consider jmeq only when Logic.JMeq is loadedletouzey
Otherwise an Anomaly coming from Coqlib.find_reference is raised and catched for the moment, but that will change soon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16275 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-27Coqlib: minor simplificationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16255 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Dir_path --> DirPathletouzey
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18use List.rev_map whenever possibleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Actually adding backtrace handling.ppedrot
I hope I did not forget some [with] clauses. Otherwise, some stack frame will be missing from the debug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-28Uniformization of the "anomaly" command.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
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
2013-01-21Fix bug 2958: Inductive deep in in clause are impossiblepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16133 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-18Unset Asymmetric Patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16129 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-01-07Fixup notation printing in patternspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16117 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Modulification of nameppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16099 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-18Fixing parsing of specific primitive tokens used as notations for patternsherbelin
(e.g. 1 for eq_refl). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16094 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-17Fixed interpretation of "x" as a binding variable for the returnherbelin
predicate in "match x return ... with" when x is a goal variable. Commit 4926 forbade it but too strongly. AFAICS, only notation variables have to be avoided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16083 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of dir_pathppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Modulification of identifierppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
some cleaning of the interface and moving of code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Using library string functions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16065 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-04Backtrack on activating scopes with type casts (was r15978).herbelin
IT happens that there are some other uses of casts, e.g. in nat_int de MathClasses which uses a notation 0 for some class constructor zero, and a cast (0:nat) to force this notation 0 to represent the instance O in nat of the class of types having a zero (eventually, 0, i.e. "zero nat O" and "O" are convertible but the information of being a class instance is lost). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16024 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-28Fix ocamldebug constr printerpboutill
In paterns, we do not try to put _ for params. (nb_params is found using Global table that ocamldebug to not have) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16010 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-26Fixed a monomorphization error.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16004 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25Monomorphization (interp)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15999 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-25More equality functionsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15998 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-23Added a constr_pattern_eqppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15995 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
type in "cast" to activate the temporary interpretation scope. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13More monomorphizationsppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-13Added a CString module.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
the new Int module. Only the most obvious were removed, so there are a lot more in the wild. This may sound heavyweight, but it has two advantages: 1. Monomorphization is explicit, hence we do not miss particular optimizations of equality when doing it carelessly with the generic equality. 2. When we have removed all the generic equalities on integers, we will be able to write something like "let (=) = ()" to retrieve all its other uses (mostly faulty) spread throughout the code, statically. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
to maintain compatibility, the term is then declared as a constant internally. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15948 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 00:38:10 +0000