aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Collapse)AuthorAge
* 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
* Minimal implementation of `Shallow marshalling of LibGravatar gareuselesinge2013-09-12
| | | | | | Just sufficient to make abstract work in such an (empty) lib. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16772 85f007b7-540e-0410-9357-904b9bb8a0f7
* summary for ML modules made correctGravatar gareuselesinge2013-08-30
| | | | | | | | | This summary entry is special because its unfreeze may load ML code that in turns adds summary entries. Hence it is the first summary piece to be unfreezed, otherwise some summaries may get lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16752 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
* recdef: restore old semantics (pre STM)Gravatar gareuselesinge2013-08-30
| | | | | | | | The Stm commit switched from an home made handling of failures to a with_state_protection. This was wrong, since in case of success the global state has to be left altered. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16746 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
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
| | | | | | | | | | | Since digests are strings (of size 16), we just dump them now in vo files (cf. Digest.output) instead of using Marshal on them : this is cleaner and saves a few bytes. Increased VOMAGIC to clearly identify this change in the format. Please rerun ./configure after this commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16722 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
* 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
* 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
* 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
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16679 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
* 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
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | | | | When refering to a module / module type, or when doing an include, we do not duplicate and substitution original libobjects immediatly. Instead, we store the module path, plus a substitution. The libobjects are retrieved later from this module path and substituted, typically during a Require. This allows to vastly decrease vo size (up to 50% on some files in the stdlib). More work is done during load (some substitutions), but the extra time overhead appears to be negligible. Beware: all subst_function operations should now be environment-insensitive, since they may be arbitrarily delayed. Apparently only subst_arguments_scope had to be adapted. A few more remarks: - Increased code factorisation between modules and modtypes - Many errors and anomaly are now assert - One hack : brutal access of inner parts of module types (cf handle_missing_substobjs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops.destr_functor without useless envGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16627 85f007b7-540e-0410-9357-904b9bb8a0f7
* More dynamic argument scopesGravatar letouzey2013-07-17
| | | | | | | | | | | | | | | | | | | | When arguments scopes are set manually, nothing new, they stay as they are (until maybe another Arguments invocation). But when argument scopes are computed out of the argument type and the Bind Scope information, this kind of scope is now dynamic: a later Bind Scope will be able to impact the scopes of an earlier constant. For Instance: Definition f (n:nat) := n. About f. (* Argument scope is [nat_scope] *) Bind Scope other_scope with nat. About f. (* Argument scope is [other_scope] *) This allows to get rid of hacks for modifying scopes during functor applications. Moreover, the subst_arguments_scope is now environment-insensitive (needed for forthcoming changes in declaremods). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Register Inline command for the native compiler. Will be ported to ↵Gravatar mdenes2013-07-10
| | | | | | | | | | the VM too. Almost only a new grammar entry since the inlining machinery was already implemented. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cosmetic changeGravatar gareuselesinge2013-05-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
| | | | | | it into the standard logger instead. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
| | | | | | | | 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
* Summary: support selective freezeGravatar gareuselesinge2013-05-06
| | | | | | One can freeze/unfreeze a portion of the summary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16477 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
* 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
* Fix issues with "Reset Initial" in scripts given to coqtop -lGravatar letouzey2013-04-23
| | | | | | | | | | | | | | Doing coqtop -l on a file starting with Reset Initial used to fail. To avoid that, we now always place an initial DOT in the libstack. Backtrack.reset_initial has been adapted accordingly: during an interactive session following a Load via coqtop -l (or .coqrc), a Reset Initial will bring back at the start of the interactive session, *not* undoing the initial Load. Note : Reset Initial might hence not be equivalent anymore to BackTo 1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16449 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqtop -compile: avoid with_heavy_rollback when non-interactiveGravatar letouzey2013-04-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7
* code simplifications concerning SummaryGravatar letouzey2013-04-22
| | | | | | | | | | | | | | | - 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
* Declaremods: some more minor cleanupGravatar letouzey2013-04-22
| | | | | | Some code cleaning and factorisation , comments, indentations, ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
| | | | | | | | - get_module_substobjs (resp. modtype) without useless mp_from arg - no need for the whole Safe_typing.pack_module - ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Declaremods: drop some useless stuff (slight gain in vo size)Gravatar letouzey2013-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16406 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Get rid of the LightenLibrary hack : no more last-minute collect of opaque terms and Obj.magic tricks. Instead, we make coqc accumulate the opaque terms as soon as constant_bodies are created outside sections. In these cases, the opaque terms are placed in a special table, and some (DirPath.t * int) are used as indexes in constant_body. In an interactive session, the local opaque terms stay directly stored in the constant_body. The structure of .vo file stays similar : magic number, regular library structure, digest of the first part, array of opaque terms. In addition, we now have a final checksum for checking the integrity of the whole .vo file. The other difference is that lazy_constr aren't changed into int indexes in .vo files, but are now coded as (substitution list * DirPath.t * int). In particular this approach allows to refer to opaque terms from another library. This (and accumulating substitutions in lazy_constr) seems to greatly help decreasing the size of opaque tables : -20% of vo size on the standard library :-). The compilation times are slightly better, but that can be statistic noise. The -force-load-proofs isn't active anymore : it behaves now just like -lazy-load-proofs. The -dont-load-proofs mode has slightly changed : opaque terms aren't seen as axioms anymore, but accessing their bodies will raise an error. Btw, API change : Declareops.body_of_constant now produces directly a constr option instead of a constr_substituted option git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16382 85f007b7-540e-0410-9357-904b9bb8a0f7
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
| | | | | | Very little space saved this way, but it would hurt either... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16375 85f007b7-540e-0410-9357-904b9bb8a0f7
* Synchronizing loadpath with the backtrack mechanism.Gravatar ppedrot2013-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
| | | | | | the interface. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 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
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16332 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
| | | | | | | | | | | | 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
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16281 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
| | | | | | | | | | | | | | | | | | | | | | | | | | Why? : avoid catching (and probably ignoring) exceptions such as Sys.Break, anomalies, assertions, leading to undetected bugs and ignored Ctrl-C. How? : when the precise exception(s) concerned by the try is known, use them explicitely in the "with". Otherwise, let's use the pattern "with e when Errors.noncritical e -> " Particular case : when an exception is catched and reraised immediately after some adjustments, we leave it untouched. Simply, for easily identifying these situations later, the name of the exception variable is changed to "reraise". Please also adopt this coding style. Automatic checks based on the "mascot" tool of X. Clerc will be runned regularly. If you want to avoid to check a particular try...with, use the variable name "any" after the "with". All these changes have been tested using the standard library and the test-suite, but unfortunately this is far from ensuring that coqtop behaves as before. We'll see after the nightly bench... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16276 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
| | | | | | | has to be refered through its qualified name even when the module containing it is imported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16263 85f007b7-540e-0410-9357-904b9bb8a0f7
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
| | | | | | | | - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml - the functions that were in declarations.ml (mostly substitution utilities and hashcons) are now in kernel/declareops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 07:51:09 +0000