aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
| | | | | | | | | | | | | | We now accept the following code: Definition E := 0. Module E. End E. Techically, we simply allow the same label to occur at most twice in a structure_body, which is a (label * structure_field_body) list). These two label occurences should not be at the same level of fields (e.g. a SFBmodule and a SFBmind are ok, but not two SFBmodule's or a SFBmodule and a SFBmodtype). Gain : a minimal amount of code change. Drawback : no more simple List.assoc or equivalent should be performed on a structure_body ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
| | | | | | Same for check_leq instead of check_geq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15081 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
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
| | | | | | From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)Gravatar letouzey2011-10-26
| | | | | | | | | | | | | | | | | | | When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1] in the environment. But since the stricter checks of commit r14150, this is an error if the environment already knows [mtb1] (for instance when doing (F M) and checking that M is compatible with the type of the arg of F. [check_subtypes] now expect [mtb1] to be already in env, and we move the add_module to the unique call site of this function that requires it. Moreover, we solve a second issue : when subtyping a functor, we update the environment once inside the functor, and this is also refused by the checks of commits r14150. So we first remove the module name from the env before doing the update. Since the module added earlier was a functor, there is no inner defs to chase in env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7
* More descriptive error messages in checkerGravatar glondu2011-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14576 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
* bug 2423: consider "" as the empty prefixGravatar barras2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14265 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed coqchk usage and man page + added option -coqlibGravatar barras2011-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14264 85f007b7-540e-0410-9357-904b9bb8a0f7
* ported r14149 from v8.3 branch: bug in checker (redefined global)Gravatar barras2011-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
| | | | | | | The env was used for a particular case of Cbytegen.compile_constant_body, but we can actually guess that it will answer a particular BCallias con. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14134 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
| | | | | | | | This is to allow users to install plugins when coq is installed system-wide. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14001 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder search path order, so the standard library is search last.Gravatar herbelin2011-04-14
| | | | | | | | | This allows the construction of an extended library that shadows the standard library. Signed-off-by: Tom Prince <tom.prince@ualberta.net> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | After discussion with Bruno and Hugo, coqtop now accepts that an opaque constant in a module type could be implemented by anything of the right type, even if bodies differ. Said otherwise, with respect to subtyping, an opaque constant behaves just as a parameter. This was already the case in coqchk, and a footnote in documentation is advertising for quite some time that: "Opaque definitions are processed as assumptions." Truly, it might seem awkward that "Definition x:=3" can implement "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing can go wrong afterwards, since Coq is forced to ignore that the x in signature has body "2". Similarly, "T with Definition x := c" is now legal when T contains an opaque x, even when this x isn't convertible with c. By avoiding accesses to opaque bodies, we also achieve some speedup (less delayed load of .vo final sections containing opaque terms). Nota: the extraction will have to be adapted, since for the moment it might access the body of opaque constants: the warning emitted when doing that should become an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The recent experiment with -dont-load-proofs in the stdlib showed that this options isn't fully safe: some axioms were generated (Include ? functor application ? This is still to be fully understood). Instead, I've implemented an idea of Yann: only load opaque proofs when we need them. This is almost as fast as -dont-load-proofs (on the stdlib, we're now 15% faster than before instead of 20% faster with -dont-load-proofs), but fully compatible with Coq standard behavior. Technically, the const_body field of Declarations.constant_body now regroup const_body + const_opaque + const_inline in a ternary type. It is now either: - Undef : an axiom or parameter, with an inline info - Def : a transparent definition, with a constr_substituted - OpaqueDef : an opaque definition, with a lazy constr_substitued Accessing the lazy constr of an OpaqueDef might trigger the read on disk of the final section of a .vo, where opaque proofs are located. Some functions (body_of_constant, is_opaque, constant_has_body) emulate the behavior of the old fields. The rest of Coq (including the checker) has been adapted accordingly, either via direct access to the new const_body or via these new functions. Many places look nicer now (ok, subjective notion). There are now three options: -lazy-load-proofs (default), -force-load-proofs (earlier semantics), -dont-load-proofs. Note that -outputstate now implies -force-load-proofs (otherwise the marshaling fails on some delayed lazy). On the way, I fixed what looked like a bug : a module type (T with Definition x := c) was accepted even when x in T was opaque. I also tried to clarify Subtyping.check_constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13952 85f007b7-540e-0410-9357-904b9bb8a0f7
* checker: cleanupGravatar glondu2011-03-04
| | | | | | Backport of changes introduced in r13443. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13867 85f007b7-540e-0410-9357-904b9bb8a0f7
* checker: add eta-expansionGravatar glondu2011-03-04
| | | | | | Backport of changes introduced in r13443 and r13494. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Propagate recent kernel changes to the checkerGravatar letouzey2011-03-03
| | | | | | | | | | | | | Cf in particular commits 13807 (about inlining) and 13835-13836 (changing the internal structure of delta_resolver and substitution). A pity we should duplicate so much code in the Checker... I tried to fix the corresponding val_* functions that check the integrity of the .vo, it seems to work, but I'm not familiar with this code. After this commit, apparently "make validate" accepts all the stdlib again, apart the new file setoid_ring/Ring2.v recently added by Loic, where it says "type error" on ring_syntax1. To be investigated... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13865 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
| | | | | | | | | | conversion. - Fix trans_fconv* to use evars correctly. - Normalize the goal with respect to evars before rewriting in [rewrite], allowing to see instanciations from other subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As said in CHANGES: << The inlining done during application of functors can now be controlled more precisely. In addition to the "!F G" syntax preventing any inlining, we can now use a priority level to select parameters to inline : "<30>F G" means "only inline in F the parameters whose levels are <= 30". The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. >> Nota : the syntax "Parameter Inline(30) foo" is equivalent to "Set Inline Level 30. Parameter Inline foo.", and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G." For instance, in ZBinary, eq is @Logic.eq and should rather be inlined, while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined. We could achieve this behavior by setting a level such as 30 to the parameter eq, and then tweaking the current level when applying functors. This idea of levels might be too restrictive, we'll see, but at least the implementation of this change was quite simple. There might be situation where parameters cannot be linearly ordered according to their "inlinablility". For these cases, we would need to mention names to inline or not at a functor application, and this is a bit more tricky (and might be a pain to use if there are many names). No documentation for the moment, since this feature is experimental and might still evolve. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
| | | | | | | | | No need to tell the world about the fact that constraints are implemented via caml's Set. Other modules just need to know about the empty and union functions (and addition functions "enforce_geq" and "enforce_eq" that were already there). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Checker: remove some dead codeGravatar letouzey2010-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
| | | | | | | | | | In particular, the unused lib/tlm.ml and lib/gset.ml are removed In addition, to simplify code, Libobject.record_object returning only the ('a->obj) function, which is enough almost all the time. Use Libobject.record_object_full if you really need also the (obj->'a). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
| | | | | | | This commit fixes a bug that made the system inconsistent with proof irrelevance (the main idea being that Set = Prop by reflexivity). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13450 85f007b7-540e-0410-9357-904b9bb8a0f7
* Explicit Mod_checking signatureGravatar glondu2010-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
| | | | | | | +commit r13412 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13418 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix likely semantic typosGravatar glondu2010-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13417 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
| | | | | | See http://caml.inria.fr/mantis/view.php?id=4940 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13413 85f007b7-540e-0410-9357-904b9bb8a0f7
* * checker/Safe_typing.LightenLibrary:Gravatar regisgia2010-08-27
| | | | | | Remove the function "save" as the checker only needs to read vo files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13387 85f007b7-540e-0410-9357-904b9bb8a0f7
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
| | | | | | | Rename "lighten_*" into "traverse_*" inside the [traverse_library] function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13385 85f007b7-540e-0410-9357-904b9bb8a0f7
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
| | | | | | | Fix a bug in traverse_library. The extraction was not satisfied with [mod_expr] set to [None]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13384 85f007b7-540e-0410-9357-904b9bb8a0f7
* * checker/SafeTyping kernel/SafeTyping:Gravatar regisgia2010-08-27
| | | | | | Fix typos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13380 85f007b7-540e-0410-9357-904b9bb8a0f7
* * lib/Flags: Replace dont_load_proofs by load_proofs since not loadingGravatar regisgia2010-08-27
| | | | | | | | | | | proofs is now the default behavior of coqtop. * lib/Coqtop: Update accordingly. * checker/Check library/Library: Pass the right "load_proofs" flag to LightenLibrary.load. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13378 85f007b7-540e-0410-9357-904b9bb8a0f7
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
| | | | | | | | | This module introduces an indirection behind opaque const_body to enable the optional demarshalling of them. * library/Library checker/Check: Use LightenLibrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13377 85f007b7-540e-0410-9357-904b9bb8a0f7
* adpated the checker to handle coomutative cuts and lazynessGravatar barras2010-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 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
* ported bug fix r13290 to checkerGravatar barras2010-07-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13304 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix typosGravatar glondu2010-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13053 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove code specific for ocaml 3.06Gravatar letouzey2010-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
| | | | | | | | | | | | | | | | | | | | | | | The choice between camlp4/5 is done during configure with flags -usecamlp5 (default for the moment) vs. -usecamlp4. Currently, to have a full camlp4 compatibility, you need to change all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI" into "`EOI" in grammar entries. I've a sed script that does that (actually the converse), but I prefer to re-think it and check a few things before branching this sed into the build mechanism. lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5 and try to propose a common interface (cf LexerSig / GrammarSig). A few incompatible quotations have been turned into underlying code manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END parsable by both camlp4 and 5. See in particular the fate of <:str_item< declare ... end >> Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc). This forces to use camlp5 > 5.01. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
| | | | | | | | | | | | | | | In checker: - delta_resolver inferred by the module system is checked through regular delta reduction steps - the old mind_equiv field of mutual_inductive is simulated through a special table in environ - small optimization, if the signature and the implementation of a module are physically equal (always happen for the toplevel module of a vo) then the checker checks only the signature. In kernel - in names i have added two special equality functions over constant and inductive names for the checker, so that the checker does not take in account the cannonical name inferred by the module system. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12977 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
* kills a warning about vo in checker/safe_typingGravatar letouzey2010-03-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12872 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed confusion between number of cstr arguments and number of pattern ↵Gravatar barras2010-03-12
| | | | | | variables (which include let-ins in cstr type) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12864 85f007b7-540e-0410-9357-904b9bb8a0f7
* added validation of delta_resolver (which seem to have an impact on typing)Gravatar barras2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12800 85f007b7-540e-0410-9357-904b9bb8a0f7
* [checker] fixed vo validation problems, module incompatibilities remainGravatar barras2010-02-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Segmenttree: New. A very simple implementation of segment trees.Gravatar regisgia2010-01-08
| | | | | | | | | | * Unicodetable: Update with the standard table for lower case conversion. * Util: Rewrite "lowercase_unicode" to take the entire unicode character set into account. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Rewrite [classify_unicode] using standard unicode tables.Gravatar regisgia2009-12-20
| | | | | | | | (This should be a conservative extension of the old version.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:18:56 +0000