aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/term.ml
Commit message (Collapse)AuthorAge
...
* 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
* 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
* * Kernel/Terms:Gravatar regisgia2013-01-06
| | | | | | | Fix an inconsistency in the hashing function of [constr]s. (Thanks to Thomas Braibant for having pointed this out.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16116 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
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing a comment.Gravatar herbelin2012-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphizationsGravatar ppedrot2012-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
| | | | | | | | | | | | | | | | | 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
* 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
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
| | | | | | not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 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
* kernel/Term:Gravatar regisgia2012-09-14
| | | | | | | Backtrack on a type definition that was moved by error by the previous patch. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15798 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
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
| | | | | | known instances in unification.ml). This refines the fix to bug #1918. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15459 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
| | | | | | change of semantics). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15060 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
* Term: properly ignore Casts between Apps in constr_ordGravatar puech2011-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14739 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: useless conversion to list in constr_ord deletedGravatar puech2011-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14738 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: Fix hash_constr behavior for Cast lnterleaved in application spines.Gravatar puech2011-11-28
| | | | | | | | hash_constr should give the same hash to two terms differing only by the presence of Casts. It should now make the same quotients on terms than constr_ord or equals_constr. This handles the case of App(Cast(App(f, l1), _, a), l2). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14735 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2011-11-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14698 85f007b7-540e-0410-9357-904b9bb8a0f7
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14546 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-cons the statically allocated Rels (1 to 16) to themselvesGravatar letouzey2011-10-10
| | | | | | | | | | | | | This is just a minor detail, but if we take care to use in mkRel always the same physical Rels for n <= 16, then let's ensure that these Rels are preserved by hash-consing. This way, we avoid killing some sharing during hash-consing of most of constr but not all (for instance those in mind). In fact, this is probably superfluous since earlier commit about "| Rel n as t -> t", but let's be sure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-cons of constr : avoid some useless allocationsGravatar letouzey2011-10-10
| | | | | | | Since we hash-cons arrays in place, no need to re-allocate a few structures around them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14540 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing of constr could share moreGravatar letouzey2011-10-02
| | | | | | | | | | | | | | | | | - An inductive is hidden inside case_info. (btw, maybe we could get rid of this ci_ind altogether, since the information is already in the predicate of the match) - Typical situation where user kn and canonical kn are initially (==) was not preserved by hconsing of constant / mutual_inductive - inductive = (mutual_inductive * int) and constructor = inductive * int were not properly shared This should fix the strange situation of Udine/PiCalc taking *more* vo space after the last round of hcons tweaks. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Polishing commits r14492, r14448 and r14407 (tactics propagateGravatar herbelin2011-09-25
| | | | | | | | conversion hints to kernel). Whether REVERTcast must be known from coqchk is unclear. In the meantime, warn about the unstability of the situation (see also bug #2599). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove specific hash-consing of Term.types (was unused anyway)Gravatar letouzey2011-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14488 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hash-consing: attempt to stop hash-consing separately constr in declare.mlGravatar letouzey2011-09-22
| | | | | | | | | | | | Now that Yann has provided a better hashing mechanism for constr, it might be interesting to (re-?)activate a global hash-consing of constr. Earlier, specific hash-cons tables were created at each call to hcons_constant_declaration. According to Hugo, this was meant to avoid blow-up in at least contrib Pocklington. This contrib seems to behave nicely now with global hashconsing (thanks Yann ;-). We'll see tomorrow what impact this has on other contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14487 85f007b7-540e-0410-9357-904b9bb8a0f7
* More twicks on hash-consingGravatar letouzey2011-09-08
| | | | | | | | | | | | | | | | | | | | | | - When hash-consing, seeing ident as having string as sub-structure induces a penalty: two searchs are done in two tables (one for string, one for id). We simply say now that the hcons function for ident is the one for string - use more == during hash-consing of Names.uniq_ident and Names.module_path - clarification concerning hash-cons of Names.constant and Names.mutual_inductive: we only hash-cons the canonical part, but == could be used nonetheless on the obtained pair. Simply note that canonical_con of hash-consed constants will produce kernel_names that may be (=) but not (==). - Code cleanup : no direct use of string hash-consing apart in Names, we hence simplify hcons_names git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14464 85f007b7-540e-0410-9357-904b9bb8a0f7
* Having added a special Cast for remembering the use of conversionGravatar herbelin2011-09-04
| | | | | | | | | | | | | | | | | tactic steps (r14407) increased the size of proof-terms, leading in some cases (e.g. in Nijmegen/Algebra) to calls to simpl becoming extremely costly on such terms built with tactics. We try as a workaround to remove the newly introduced Cast after it has been used by the type-checking algorithm. We incidentally fixed eq_constr which was not fully transparent wrt casts. We also removed useless code in judge_of_apply (has_revert). Note: checker still to be updated to reflect a possible use of this new kind of cast. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagated information from the reduction tactics to the kernel soGravatar herbelin2011-08-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | that the kernel conversion solves the delta/delta critical pair the same way the tactics did. This allows to improve Qed time when slow down is due to conversion having (arbitrarily) made the wrong choice. Propagation is done thanks to a new kind of cast called REVERTcast. Notes: - Vm conversion not modified - size of vo generally grows because of additional casts - this remains a heuristic... for the record, when a reduction tactic is applied on the goal t leading to new goal t', this is translated in the kernel in a conversion t' <= t where, hence, reducing in t' must be preferred; what the propagation of reduction cast to the kernel does not do is whether it is preferable to first unfold c or to first compare u' and u in "c u' = c u"; in particular, intermediate casts are sometimes useful to solve this kind of issues (this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the combination "simpl;red" needs the intermediate cast to ensure Qed answers quickly); henceforth the merge of nested casts in mkCast is deactivated - for tactic "change", REVERTcast should be used when conversion is in the hypotheses, but convert_hyp does not (yet) support this (would require e.g. that convert_hyp overwrite some given hyp id with a body-cleared let-binding new_id := Cast(old_id,REVERTCast,t)) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: fix hash_constr to hash modulo casts & names (like compare_constr)Gravatar puech2011-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14387 85f007b7-540e-0410-9357-904b9bb8a0f7
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
| | | | | | | Allows to be sure that we apply the smart constructors. Propagate the change to Closure, Reduction, Term, Cbv and Newring git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14386 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: simplify compare_constr by removing calls to decompose_appGravatar puech2011-08-01
| | | | | | I think the additional check was here for historical reasons (before the invariant on Apps was enforced) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: replace generic = on mutual_inductive_body by mib_equalGravatar puech2011-07-29
| | | | | | Term: add function eq_rel_declaration git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14366 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: moved function constr_ord (a.k.a compare_constr) from Sequent to TermGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by ↵Gravatar puech2011-07-29
| | | | | | | | Constrhash and Termhash We need a function hash_constr (added in Term) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14345 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hahtbl_alt: separate generic combine functionsGravatar puech2011-07-29
| | | | | | ... and report changes on Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14344 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: added function eq_named_declarationGravatar puech2011-07-29
| | | | | | We need to move eq_constr upwards git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14319 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: slight reorganization of the fileGravatar puech2011-07-29
| | | | | | | - removed duplicate constructors - moved code around for more clarity git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14314 85f007b7-540e-0410-9357-904b9bb8a0f7
* Term: Refactoring of hashconsingGravatar puech2011-07-29
| | | | | | | - moved the alterate Hashtable module to a separate file - moved all hashconsing-related function to a separate section in Term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14312 85f007b7-540e-0410-9357-904b9bb8a0f7
* argument renaming in liftn (match with usual terminology)Gravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14311 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few extra combinators about rel_declaration/named_declaration + a bit of docGravatar herbelin2011-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/Term:Gravatar regisgia2010-12-01
| | | | | | | | | - Fix a bug in [comp_term] (casts were ignored). - Improve the efficiency of hash table lookup. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13662 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Remove an unsound optimization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Kernel/TermGravatar regisgia2010-12-01
| | | | | | | | Fix an efficiency bug when hash-consing deep [constr]s. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13660 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 14:03:21 +0000