aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
Commit message (Collapse)AuthorAge
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
| | | | | Make this module deal only with opaque proofs. Make discharging/substitution invariant more explicit via a third constructor.
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | To obtain a.vo one can now: 1) coqtop -quick -compile a 2) coqtop -vi2vo a.vi To make that possible the .vo structure has been complicated. It is now made of 5 segments. | vo | vi | vi2vo | contents --------------+------+-----+-------+------------------------------------ lib | Yes | Yes | Yes | libstack (modules, notations,...) opauqe_univs | No | Yes | Yes | constraints coming from opaque proofs discharge | No | Yes | No | data needed to close sections tasks | No | Yes | No | STM tasks to produce proof terms opaque_proofs | Yes | Yes | Yes | proof terms --------------+------+-----+-------+------------------------------------ This means one can load only the strictly necessay parts. Usually one does not load the tasks segment of a .vi nor the opaque_proof segment of a .vo, unless one is turning a .vi into a .vo, in which case he load all the segments. Optional segments are marshalled as None. But for lib, all segments are Array.t of: | type --------------+--------------------------------------------------------- lib | a list of Libobject.obj (n'importe quoi) opauqe_univs | Univ.consraints Future.computation discharge | what Cooking.cook_constr needs tasks | Stm.tasks (a task is system_state * vernacexpr list) opaque_proofs | Term.constr Future.computation --------------+------+-----+-------+------------------------------------ Invariant: all Future.computation in a vo file (obtained by a vi2vo compilation or not) have been terminated with Future.join (or Future.sink). This means they are values (inside a box). This invariant does not hold for vi files. E.g. opauqe_proofs can be dangling Future.computation (i.e. NotHere exception). The vi2vo compilation step will replace them by true values. Rationale for opaque_univs: in the vi2vo transformation we want to reuse the lib segment. Hence the missing pieces have to be put on the side, not inside. Opaque proof terms are already in a separte segment. Universe constraints are not, hence the new opauqe_univs segment. Such segment, if present in a .vo file, is always loaded, and Declare.open_constant will add to the environment the constraints stored there. For regular constants this is not necessay since the constraints are already in their enclosing module (and also in the constant_body). With vi2vo the constraints coming from the proof are not in the constant_body (hence not in the enclosing module) but there and are added to the environment explicitly by Declare.open_constant. Rationale for discharge: vi2vo produces a proof term in its original context (in the middle of a section). Then it has to discharge the object. This segment contains the data that is needed in order to do so. It is morally the input that Lib.close_section passes to Cooking (via the insane rewinding of libstack, GlobalRecipe, etc chain). Checksums: the checksum of .vi and a .vo obtain from it is the same. This means that if if b.vo has been compiled using a.vi, and then a.vi is compiled into a.vo, Require Import b works (and recursively loads a.vo).
* Tacinterp: fewer Proofview.Goal.enterl.Gravatar Arnaud Spiwack2014-02-25
| | | | | | | | | | | I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their context. Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API). Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way). Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
* cbn understands ArgumentsGravatar Pierre Boutillier2014-02-24
| | | | (excepts list of args that must be constructors
* Stack operations of Reductionops in Reductionops.StackGravatar Pierre Boutillier2014-02-24
|
* More sharing in Logic, together with some code cleaning.Gravatar Pierre-Marie Pédrot2014-02-21
|
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
| | | | | | The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes.
* STM: fix valid_id coming from Qed errorsGravatar Enrico Tassi2014-02-10
|
* Tracking memory misallocation by trying to improve sharing.Gravatar Pierre-Marie Pédrot2014-02-03
|
* Fixing backtrace reporting.Gravatar Pierre-Marie Pédrot2014-02-02
|
* Typos in comment.Gravatar Arnaud Spiwack2014-01-31
|
* Fixing backtrace handling here and there.Gravatar Pierre-Marie Pédrot2014-01-30
|
* Useless Array.of_listGravatar Pierre-Marie Pédrot2014-01-10
|
* Exporting the full pretyper options in Goal.constr_of_raw.Gravatar Pierre-Marie Pédrot2014-01-10
|
* Algebraized "No such hypothesis" errorsGravatar Pierre-Marie Pédrot2014-01-06
|
* Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, ↵Gravatar Arnaud Spiwack2014-01-06
| | | | | | | | | | | | | without" This reverts commit bfe1141026da70d8f59cf47b5fe61ffc20a29f3c. Conflicts: proofs/proofview_monad.ml This is potentially a temporary commit until a final decision is taken on hand-written versus extracted ocaml for the tactic monad. The hand-written implementation has a bug where the + tactical would not behave properly (I tried to find why, but couldn't: the hand-written implementation looks fine, but it isn't. Beats me). There is a conflict with Pierre-Marie's commit 4832692: Fixing backtrace registering of various tactic-related try-with blocks.
* Proof_using: new syntax + suggestionGravatar Enrico Tassi2014-01-05
| | | | | | | | | | | | | | | | | | | | | | | | Proof using can be followed by: - All : all variables - Type : all variables occurring in the type - expr: - (a b .. c) : set - expr + expr : set union - expr - expr : set difference - -expr : set complement (All - expr) Exceptions: - a singleton set can be written without parentheses. This also allows the implementation of named sets sharing the same name space of section hyps ans write - bla - x : where bla is defined as (a b .. x y) elsewhere. - if expr is just a set, then parentheses can be omitted This module also implements some AI to tell the user how he could decorate "Proof" with a "using BLA" clause. Finally, one can Set Default Proof Using "str" to any string that is used whenever the "using ..." part is missing. The coding of this sucks a little since it is the parser that applies the default.
* Proof_global: Simpler API for proof_terminatorGravatar Enrico Tassi2014-01-04
|
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
| | | | | | | | | | | | | | | | Experimental. Turned out to be much harder to implement than I thought. The main issue is that the reification in the native compiler and the VM is not quite untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence, when reifying an application u = t a1 ... an, the type of t has to be known or reconstructed. It is always possible to do so in plain CIC, when u is in normal form and its type is known. However, with partial terms this may no longer be the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of evars and metas. This still has to be tested more extensively, but the correction of the kernel native conversion (on terms without evars or metas) should not be impacted. Much of this could be reused for the VM.
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
| | | | | | To make this possible the state id has to reach the kernel. Hence definition_entry has an extra field, and many files had to be fixed.
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
| | | | | | Actually, this was wrong, as evars should not appear until interpretation. Evarmaps were only passed around uselessly, and often fed with dummy or irrelevant values.
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
|
* Fix Admitted.Gravatar Arnaud Spiwack2013-12-04
| | | | Commit "The commands that initiate proofs…" was a bit hasty in its treatment of Admitted (in an attempt of making things simple, I actually required the proof to be completed for Admitted to go through…).
* Proof_global: fix start_proof comment after the preceding commits.Gravatar Arnaud Spiwack2013-12-04
|
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
| | | | This commit removes the hook.
* Refactoring: storing more information in the terminator closure.Gravatar Arnaud Spiwack2013-12-04
| | | | | | We used to keep a lot of information in the global proof environment, for the end-of-proof commands to use. Now that the end commands are dumb, they are better stored in the proof-termination closure allocated by the starting command. In this commit, we remove the compute_guard parameter.
* The commands that initiate proofs are now in charge of what happens when ↵Gravatar Arnaud Spiwack2013-12-04
| | | | | | | | | | proofs end. The proof ending commands like Qed and Defined had all the control on what happened to the proof when they are closed. In constrast, proof starting commands were dumb: start a proof, give it a name, that's it. In such a situation if we want to come up with new reasons to open proofs, we would need new proof-closing commands. In this commit we decide at proof-starting time how to dispatch the various Qed/Defined, etc… By registering a function in the interactive proof environment. This way, proofs are always closed the same but we can invent new ways to start them.
* Allow proofs to start with dependent goals.Gravatar Arnaud Spiwack2013-12-04
| | | I use a telescope to represent to goals, and let proofview.ml generate the appropriate existential variables.
* Fixing ltac constr variable handling in refine.Gravatar Pierre-Marie Pédrot2013-11-30
|
* Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute notGravatar Hugo Herbelin2013-11-29
| | | | | | | | supporting metas/evars). Fix of #3169 is by calling pretyping retyper rather than the non evar-aware kernel type-checker (since argument of vm_compute is supposed to be already typable). Support of metas/evars in vm is still to be done...
* Useless computation in Goal handle augmentation.Gravatar ppedrot2013-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do not print tactic notation names at each interpretation step.Gravatar ppedrot2013-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17082 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial applications in Goal.Gravatar ppedrot2013-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17074 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewriting the proof monad mechanism. Now it uses pure OCaml code, withoutGravatar ppedrot2013-11-07
| | | | | | | | | | | | | going through a Coq extraction phase. We use second order quantification through OCaml records, which allows for a very precise use of low-level application. This results in quite a remarkable speedup but there is still room for improvement. This code was written by translating straightforwardly the Coq generated code in a human-readable dialect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17068 85f007b7-540e-0410-9357-904b9bb8a0f7
* Less partial applications in Vars, as well as better memory allocation.Gravatar ppedrot2013-11-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17065 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reducing allocation in tclDISPATCHGEN, by doing a List.map at the same timeGravatar ppedrot2013-11-05
| | | | | | the argument list is consumed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17062 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was ↵Gravatar aspiwack2013-11-04
| | | | | | | | | | solved. This made "autorewrite using tac" fail. Spotted in CoLoR and Demos. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the tactical ; [ … ] : the "incorrect number of goal" error was not ↵Gravatar aspiwack2013-11-04
| | | | | | | | | | caught by ltac tacticals. The errors were not translated into ltac errors (and at some occurence errors were raised in OCaml rather than inside the tactic monad). Spotted in ProjectiveGeometry and Goedel. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allowing proofs starting with a non-empty evarmap.Gravatar ppedrot2013-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17055 85f007b7-540e-0410-9357-904b9bb8a0f7
* A try/with was catching every exception.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update comments.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Doc: solve the bad interaction between Declare Implicit Tactic and refine.Gravatar aspiwack2013-11-02
| | | | | | An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix destruct: nf_evar prior to tactic interpretation.Gravatar aspiwack2013-11-02
| | | | | | Noticed in CoRN git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17028 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add primitives in Goal.V82 to access the goal in nf_evar'd form.Gravatar aspiwack2013-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17025 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
| | | | | | Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
| | | | | | | | | | | | | Puts on the shelf every goals under focus on which other goals under focus depend. Useful when we want to solve these goals by unification (as in a first order proof search procedure, for instance). Also meant to be able to recover approximately the semantics of the old refine with the new implementation (use refine t; shelve_unifiable). TODO: bug dans l'example de shelve_unifiable git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrects a bug on Proofview.Goal.enter whereby sigmas were captured and used ↵Gravatar aspiwack2013-11-02
| | | | | | | | | | at the wrong time. The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t)) had the correct semantics! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17014 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
| | | | | | The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
* bootstrap/Monad.v: implements the writer monad in continuation passing style.Gravatar aspiwack2013-11-02
| | | | | | | Benefits: fewer pair constructed/destructed especially in split. Potential costs: plus and zero now have closures with 11 arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17012 85f007b7-540e-0410-9357-904b9bb8a0f7
* bootstrap/Monad.v: implements the environment monad in continuation passing ↵Gravatar aspiwack2013-11-02
| | | | | | | | | style. Benefits: the underlying monads are not referenced in the "current" primitive. Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17011 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 02:37:25 +0000