aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* Closure: fix an issue with r16959 spotted by MatthieuGravatar letouzey2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16966 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_subst.update_delta_resolver : avoid loosing Inline(_,Some _)Gravatar letouzey2013-10-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit should fix the contrib ProjectiveGeometry This update_delta_resolver is in fact a sequential composition (resolver1 then resolver2). The earlier version was strangely favoring the bindings coming from resolver2 over the bindings coming from (resolver1 chained with resolver2). So any inlining information stored in resolver1 could be discarded savagely. Apparently, this situation wasn't occurring in practice until recently, when I started to do lots of Mod_subst.join for improving the size of modular libobjects in the vo's. So, when combining two resolvers now : - Inline(_,None) is the weakest information, it's just a declaration that we intend to inline this kn someday if possible (i.e. when we'll have a transparent implementation for it). This kind of Inline is only relevant inside a module type. - Equiv(_) should only appear in modules (after some Include) so it should be ok if it takes precedence over any Inline(_,None) remaining in the other resolver. - Inline(_,Some _) is there after functor application (cf inline_delta_resolver) : we've done the inlining, so we don't care anymore about other Equiv(_) or Inline(_,None) informations about this kn, since we have anyway a new body for it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16965 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing Kerpair.hash. Since the beginning, it dit not respect the typeGravatar ppedrot2013-10-31
| | | | | | equality, maybe impeding hashconsing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16964 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: better doc + restore ~pure optimizationGravatar gareuselesinge2013-10-31
| | | | | | | | | | | This optimization was undone because the kernel type checking was not a pure functions (it was accessing the conv_oracle state imperatively). Now that the conv_oracle state is part of env, the optimization can be restored. This was the cause of the increase in memory consumption, since it was forcing to keep a copy of the system state for every proof, even the ones that are not delayed/delegated to slaves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16963 85f007b7-540e-0410-9357-904b9bb8a0f7
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
| | | | | | But for vm, the kernel should be functional now git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoiding useless allocations in Closure.Gravatar ppedrot2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16959 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allocation-friendly version of [Pre_env.push_named].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16947 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing universes: tail-rec, allocation friendly [compare_leq].Gravatar ppedrot2013-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16946 85f007b7-540e-0410-9357-904b9bb8a0f7
* Native compiler: library compilation errors are now non fatal.Gravatar mdenes2013-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16944 85f007b7-540e-0410-9357-904b9bb8a0f7
* More sharing in Constr.map_with_binders.Gravatar ppedrot2013-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16938 85f007b7-540e-0410-9357-904b9bb8a0f7
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
| | | | | | | | | | | To reduce the amount of syntactic noise, we now provide a few inner modules Int.List, Id.List, String.List, Sorts.List which contain some monomorphic (or semi-monomorphic) functions such as mem, assoc, ... NB: for Int.List.mem and co we reuse List.memq and so on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16936 85f007b7-540e-0410-9357-904b9bb8a0f7
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
| | | | | | | | | * Using generic fold functions was unecessarily obscure * No more List.mem and hence indirect use of ocaml generic comparison * Rtree.equiv (former Rtree.compare_rtree) has now a less cryptic semantic... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16934 85f007b7-540e-0410-9357-904b9bb8a0f7
* Specializing hash functions for widely used types.Gravatar ppedrot2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16925 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Optimizing Vars.replace_varsGravatar ppedrot2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16916 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing some generic equalities.Gravatar ppedrot2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various optimizations in Constr, such as term sharing and allocationGravatar ppedrot2013-10-22
| | | | | | avoiding. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16911 85f007b7-540e-0410-9357-904b9bb8a0f7
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
| | | | | | | | | | | | | | | | A future always carries a fix_exn with it: a function that enriches an exception with the state in which the error occurs and also a safe state close to it where one could backtrack. A future can be in two states: Ongoing or Finished. The latter state is obtained by Future.join and after that the future can be safely marshalled. An Ongoing future can be marshalled, but its value is lost. This makes it possible to send the environment to a slave process without pre-processing it to drop all unfinished proofs (they are dropped automatically in some sense). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16892 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix comment for new string syntax (OCaml trunk).Gravatar xclerc2013-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16846 85f007b7-540e-0410-9357-904b9bb8a0f7
* A shallow copy of a pre_env does not contain the vm cacheGravatar gareuselesinge2013-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16845 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
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
| | | | | | removing an unneeded indirection. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16781 85f007b7-540e-0410-9357-904b9bb8a0f7
* ind_tables: properly handling side effectsGravatar gareuselesinge2013-08-30
| | | | | | | | | | | | | | If a constant is defined as transparent, not only its side effects (opaque sub proofs as in abstract, and transparent ind schemes) are declared globally, but the ones that are schemes are also declared as such. The only sub optimal thing is that the code handling in a special way the side effects of transparent constants is in declare.ml that does not see ind_tables.ml, hence a forward ref to a function is used. IMO, ind_tables has no reason to stay in toplevel/. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16747 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove Obj.magic from safe typingGravatar gareuselesinge2013-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16741 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
| | | | | | | | | | The extended signature is defined in CMap, and should be compatible with the old one, except that module arguments have to be explicitely named. The implementation itself is quite unsafe, as it relies on the current implementation of OCaml maps, even though that should not be a problem (it has not changed in ages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix computation of discharged hyps for inductive types forgetting the ↵Gravatar msozeau2013-08-23
| | | | | | conclusion of the arity. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
| | | | | | | | | | | | | | | | | | | - Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
* More complete hashcons : lists (dirpath), arrays (constr)Gravatar letouzey2013-08-22
| | | | | | | | | | | | | | | | Earlier, the elements of constr arrays were hash-consed, but not the array itself. This helps a bit when the same (f a1 ... an) is manipulated a lot : -20% in the size of opaque terms in Integral_domain.vo and Nsatz.vo Similarly it's interesting to hash-cons sub-lists for dirpaths, since in Coq.A.B and Coq.A.C we could share Coq.A. With this patch, the hash-consing of constr seems quasi-optimal: Pierre-Marie's marshal compactor is unable to shrink opaque tables by more than 2%, and this difference seems to be due to untyped compaction (for the compactor Rel 1 = Prop Pos). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial revert of r16711Gravatar letouzey2013-08-20
| | | | | | | It seems that it's critical for the native compiler that a fresh (ref NotLinked) is created during substitution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16719 85f007b7-540e-0410-9357-904b9bb8a0f7
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
| | | | | | | | | | | | | | | Simple framework for remote counters. The slaves ask the master for a fresh value. On the master the thread manager answers with a bunch of fresh values (so that further requests can be immediately satisfied). Remote counters are guarded with a mutex on the master, because all slave managers as well as the master thread can access the counter at the same time. I know the name sucks. These counters are remote for the slaves, and local for the master. I'm open to suggestions... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The earlier type [struct_expr_body] was far too broad, leading to code with unclear invariants, many "assert false", etc etc. Its replacement [module_alg_expr] has only three constructors: * MEident * MEapply : note the module_path as 2nd arg, no more constraints here * MEwith : no more constant_body inside, constr is just fine But no more SEBfunctor or SEBstruct constructor here (see below). This way, this datatype corresponds to algebraic expressions, i.e. anything that can appear in non-interactive modules. In fact, it even coincides now with [Entries.module_struct_entry]. - Functor constructors are now necessarily on top of other structures thanks to a generic [functorize] datatype. - Structures are now separated from algebraic expressions by design : the [mod_type] and [typ_expr] fields now only contain structures (or functorized structures), while [mod_type_alg] and [typ_expr_alg] are restricted to algebraic expressions only. - Only the implementation field [mod_expr] could be either algebraic or structural. We handle this via a specialized datatype [module_implementation] with four constructors: * Abstract : no implementation (cf. for instance Declare Module) * Algebraic(_) : for non-interactive modules, e.g. Module M := N. * Struct(_) : for interactive module, e.g. Module M : T. ... End M. * FullStruct : for interactive module with no type restriction. The [FullStruct] is a particular case of [Struct] where the implementation need not be stored at all, since it is exactly equal to its expanded type present in [mod_type]. This is less fragile than hoping as earlier that pointer equality between [mod_type] and [mod_expr] will be preserved... - We clearly emphasize that only [mod_type] and [typ_expr] are relevant for the kernel, while [mod_type_alg] and [typ_expr_alg] are there only for a nicer extraction and shorter module printing. [mod_expr] is also not accessed by the kernel, but it is important for Print Assumptions later. - A few implicit invariants remain, for instance "no MEwith in mod_expr", see the final comment in Declarations - Heavy refactoring of module-related files : modops, mod_typing, safe_typing, declaremods, extraction/extract_env.ml ... - Coqchk has been adapted accordingly. The code concerning MEwith in Mod_checking is now gone, since we cannot have any in mod_expr. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declareops + Modops : more clever substitutionsGravatar letouzey2013-08-20
| | | | | | | | | | | | | | | | | We try harder to preserve pointer equality when substituting. This will probably have little effect (for instance the constr_substituted are anyway _never_ substituted in place), but it cannot harm. Two particular cases: - we try to share (and maintain shared) mind_user_lc and mind_nf_lc - we try to share (and maintain shared) mod_expr and mod_type TODO: check that native compiler is still ok, since we might have less (ref NotLinked) now. Having references in constant_body and co is anyway a Very Bad Idea (TM). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mod_typing : code cleanupGravatar letouzey2013-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16709 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing code refactoringGravatar letouzey2013-08-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - No more modinfo sub-record in the safe_environment record, this was a syntactic pain. senv.modinfo.modpath --> senv.modpath senv.modinfo.variant --> senv.modvariant senv.modinfo.resolver --> senv.modresolver senv.modinfo.resolver_of_param --> senv.paramresolver senv.modinfo.label : removed (can be inferred from modpath) - No more systematic chaining of safe_environment ('old' field). Instead, earlier safe_environment is stored in the modvariant field when necessary (STRUCT and SIG case). - Improved sharing between end_module and end_modtype - More qualified names instead of open, better comments, ... - Some user errors are now checked earlier elsewhere (see for instance vernac_end_segment), so we can turn these errors into asserts. The user error about higher-order include is now algebraic. - Highlight the idea of a state monad in Safe_typing : type 'a safe_transformer = safe_environment -> 'a * safe_environment More systematic code in Global, thanks to 'globalize' function. - Declaremods : less informations stored in openmod_info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16708 85f007b7-540e-0410-9357-904b9bb8a0f7
* Attempt to restore hash-consing of opaque termsGravatar letouzey2013-08-20
| | | | | | Without this, the stdlib vo files are +30% larger git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup code in term_typingGravatar gareuselesinge2013-08-19
| | | | | | | No semantic change, but way less debug printings coming from Paral-ITP git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16703 85f007b7-540e-0410-9357-904b9bb8a0f7
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
| | | | | | | | | | | | | | | Non-opaque-constant's side effects are processed before the constant enters the kernel and global constants are generated for them (as before, but not by side effect in the middle of the proof construction). This makes sense because proofs ending with Defined have to be run immediately, so the list of side effects is immediately available. These side effects are type checked again. To fix that the idea of kernel signatures could be employed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16702 85f007b7-540e-0410-9357-904b9bb8a0f7
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
| | | | | | | | In some cases, an 'a -> 'b field is changed into an ('a -> b') option field so that one can forget the closures and marshal the resulting state git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16683 85f007b7-540e-0410-9357-904b9bb8a0f7
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
| | | | | | | | | It can be: `Yes Full data, in a state that can be marshalled `No Full data, good for Undo only `Shallow Partial data, marshallable, good for slave processes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16682 85f007b7-540e-0410-9357-904b9bb8a0f7
* State Transaction MachineGravatar gareuselesinge2013-08-08
| | | | | | | | | | | | | | | | | | | | | The process_transaction function adds a new edge to the Dag without executing the transaction (when possible). The observe id function runs the transactions necessary to reach to the state id. Transaction being on a merged branch are not executed but stored into a future. The finish function calls observe on the tip of the current branch. Imperative modifications to the environment made by some tactics are now explicitly declared by the tactic and modeled as let-in/beta-redexes at the root of the proof term. An example is the abstract tactic. This is the work described in the Coq Workshop 2012 paper. Coq is compile with thread support from now on. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing #2846: Uncaught exception Reduction.NotArity.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 19:10:42 +0000