aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-ltac.tex4
-rw-r--r--doc/refman/RefMan-pre.tex86
-rw-r--r--kernel/nativevalues.ml12
-rw-r--r--plugins/extraction/ocaml.ml10
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/obligations.ml22
-rw-r--r--toplevel/obligations.mli6
9 files changed, 93 insertions, 55 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index b90e682df..de8c26943 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -474,7 +474,7 @@ $v_2$). Branching is left-associative.
The tactic
\begin{quote}
-{\tt if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$}
+{\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$}
\end{quote}
is a generalization of the biased-branching tactics above. The
expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
@@ -482,7 +482,7 @@ to each subgoal independently. For each goal where $v_1$ succeeds at
least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
collectively to the generated subgoals. The $v_2$ tactic can trigger
backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
- if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
+ tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
equivalent to $v_1;v_2$. In each of the goals where $v_1$ does not
succeed at least once, {\tacexpr}$_3$ is evaluated in $v_3$ which is
is then applied to the goal.
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e75ade941..f45072ca4 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -939,9 +939,9 @@ projects:
\begin{itemize}
\item A new asynchronous evaluation and compilation mode by Enrico
Tassi with help from Bruno Barras and Carst Tankink.
-\item The full integration of the new proof engine by Arnaud Spiwack
+\item Full integration of the new proof engine by Arnaud Spiwack
helped by Pierre-Marie Pédrot,
-\item The addition of conversion and reduction based on native compilation
+\item Addition of conversion and reduction based on native compilation
by Maxime Dénès and Benjamin Grégoire.
\item Full universe polymorphism for definitions and inductive types by
Matthieu Sozeau.
@@ -950,28 +950,38 @@ projects:
Matthieu Sozeau.
\end{itemize}
-The full integration of the proof engine brings to primitive tactics and
-the user level Ltac language deep tactic backtracking and multi-goal
-handling.
+The full integration of the proof engine, by Arnaud Spiwack and
+Pierre-Marie Pédrot, brings to primitive tactics and the user level
+Ltac language dependent subgoals, deep backtracking and multiple goal
+handling, along with miscellaneous features and an improved potential
+for future modifications. Dependent subgoals allow statements in a
+goal to mention the proof of another. Proofs of unsolved subgoals
+appear as existential variables. Primitive backtracking make it
+possible to write a tactic with several possible outcomes which are
+tried successively when subsequent tactics fail. Primitives are also
+available to control the backtracking behavior of tactics. Multiple
+goal handling paves the way for smarter automation tactics. It is
+currently used for simple goal manipulation such as goal reordering.
The way Coq processes a document in batch and interactive mode has
been redesigned by Enrico Tassi with help from Bruno Barras. Opaque
proofs, the text between Proof and Qed, can be processed
asynchronously, decoupling the checking of definitions and statements
-from the checking of proofs. In interactive use, this improves the
-reactiveness of the system, since proofs can be processed in the
-background. Similarly the compilation of a file can be split into two
-phases: the first one checking only definitions and statements and
-the second one checking proofs. A file resulting from the first
-phase, .vio extension, can be already Required. All .vio files can be
-turned into complete .vo files in parallel. The same infrastructure
-also allows terminating tactics to be run in parallel on a set of
-goals via the \verb=par:= goal selector.
-
-CoqIDE was modified to cope with asynchronous checking of the document.
-Its source code was also made separate from the one of Coq making it no
-more a special user interface and allowing its release cycle to be
-decoupled with the one of Coq.
+from the checking of proofs. It improves the responsiveness of
+interactive development, since proofs can be processed in the
+background. Similarly compilation of a file can be split into two
+phases: the first one checking only definitions and statements and the
+second one checking proofs. A file resulting from the first
+phase~--~with the .vio extension~--~can be already Required. All .vio
+files can be turned into complete .vo files in parallel. The same
+infrastructure also allows terminating tactics to be run in parallel
+on a set of goals via the \verb=par:= goal selector.
+
+CoqIDE was modified to cope with asynchronous checking of the
+document. Its source code was also made separate from that of Coq, so
+that CoqIDE no longer has a special status among user interfaces,
+paving the way for decoupling its release cycle from that of Coq in
+the future.
Carst Tankink developed a Coq back end for user interfaces built on
Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
@@ -982,13 +992,13 @@ funded by the Paral-ITP French ANR project.
The full universe polymorphism extension was designed by Matthieu
Sozeau. It conservatively extends the universes system and core calculus
with definitions and inductive declarations parameterized by universes
-and constraints. It is based on a change of the kernel architecture to
+and constraints. It is based on a modification of the kernel architecture to
handle constraint checking only, leaving the generation of constraints
to the refinement/type inference engine. Accordingly, tactics are now
fully universe aware, resulting in more localized error messages in case
of inconsistencies and allowing higher-level algorithms like unification
to be entirely type safe. The internal representation of universes has
-been modified but this invisible to the user.
+been modified but this is invisible to the user.
The underlying logic has been extended with $\eta$-conversion for
records defined with primitive projections by Matthieu Sozeau. This
@@ -999,37 +1009,45 @@ with typed equality. Primitive projections, which do not carry the
parameters of the record and are rigid names (not defined as a
pattern-matching construct), make working with nested records more
manageable in terms of time and space consumption. This extension and
-universe polymorphism were carried partly while the author was working
+universe polymorphism were carried out partly while Matthieu Sozeau was working
at the IAS in Princeton.
The guard condition has been made compliant with extensional equality
-principles such as propositional equality and univalence, thanks to
+principles such as propositional extensionality and univalence, thanks to
Maxime Dénès and Bruno Barras. To ensure compatibility with the
univalence axiom, a new flag ``-indices-matter'' has been implemented,
taking into account the universe levels of indices when computing the
levels of inductive types. This supports using Coq as a tool to explore
the relations between homotopy theory and type theory.
+Maxime Dénès and Benjamin Grégoire developed an implementation of
+conversion test and normal form computation using the OCaml native
+compiler. It complements the virtual machine conversion offering much
+faster computation for expensive functions.
+
{\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
and improvements regarding the different components of the system.
-% High-Level Specification Language:
-% - tactics in terms
-% - Universe inconsistency and unification error messages
-% - Named existentials
+Maxime Dénès maintained the bytecode-based reduction machine.
-% Opam Coq Guillaume Claret and Thomas Braibant
+Pierre-Marie Pédrot has extended the syntax of terms to,
+experimentally, allow holes in terms to be solved by a locally
+specified tactic.
-Maxime Dénès and Benjamin Grégoire developed an implementation of the
-conversion test using the OCaml native compiler.
-Bruno Barras and Maxime Dénès fixed a problem in the guard condition
-leading to a refutation of standard axioms like propositional
-extensionality or univalence.
-Maxime Dénès maintained the bytecode-based reduction machine.
+Existential variables are referred to by identifiers rather than mere
+numbers, thanks to Hugo Herbelin.
+
+Error messages for universe inconsistencies have been improved by
+Matthieu Sozeau. Error messages for unification and type inference
+failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and
+Arnaud Spiwack.
Pierre Courtieu contributed new features for using {\Coq} through Proof
General and for better interactive experience (bullets, Search etc).
+A distribution channel for Coq packages using the Opam tool has been
+developed by Thomas Braibant and Guillaume Claret.
+
\begin{flushright}
Paris, January 2015\\
Hugo Herbelin \& Matthieu Sozeau\\
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index d7a219505..e4a779993 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -370,6 +370,11 @@ type coq_pair =
| Paccu of t
| PPair of t * t
+type coq_zn2z =
+ | Zaccu of t
+ | ZW0
+ | ZWW of t * t
+
let mkCarry b i =
if b then (Obj.magic (C1(of_uint i)):t)
else (Obj.magic (C0(of_uint i)):t)
@@ -413,8 +418,13 @@ let subcarryc accu x y =
let of_pair (x, y) =
(Obj.magic (PPair(of_uint x, of_uint y)):t)
+let zn2z_of_pair (x,y) =
+ if Uint31.equal x (Uint31.of_uint 0) &&
+ Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0
+ else (Obj.magic (ZWW(of_uint x, of_uint y)) : t)
+
let no_check_mulc x y =
- of_pair(Uint31.mulc (to_uint x) (to_uint y))
+ zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y))
let mulc accu x y =
if is_int x && is_int y then no_check_mulc x y
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 30ac3d3f8..ce88ea6d2 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,10 @@ and pp_module_type params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (mp, sign) ->
push_visible mp params;
- let l = List.map pp_specif sign in
+ let try_pp_specif x l =
+ try pp_specif x :: l with Failure "empty phrase" -> l
+ in
+ let l = List.fold_right try_pp_specif sign [] in
pop_visible ();
str "sig " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +710,10 @@ and pp_module_expr params = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MEstruct (mp, sel) ->
push_visible mp params;
- let l = List.map pp_structure_elem sel in
+ let try_pp_structure_elem x l =
+ try pp_structure_elem x :: l with Failure "empty phrase" -> l
+ in
+ let l = List.fold_right try_pp_structure_elem sel [] in
pop_visible ();
str "struct " ++ fnl () ++
v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 185888673..1383d7556 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -234,7 +234,7 @@ let reduction_of_red_expr env =
with Not_found ->
error("unknown user-defined reduction \""^s^"\"")))
| CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
- | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
+ | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
in
reduction_of_red_expr
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9cb3bb866..608747d0e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -746,8 +746,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
- let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+ let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
let _ = Obligations.declare_fix_ref := declare_fix
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 894333ad5..1de47d38c 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -167,5 +167,5 @@ val do_cofixpoint :
val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
-val declare_fix : definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa0685861..456a6f9d0 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -21,7 +21,7 @@ open Pp
open Errors
open Util
-let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
+let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
let trace s =
@@ -319,6 +319,7 @@ type program_info = {
prg_kind : definition_kind;
prg_reduce : constr -> constr;
prg_hook : unit Lemmas.declaration_hook;
+ prg_opaque : bool;
}
let assumption_message = Declare.assumption_message
@@ -512,8 +513,9 @@ let declare_definition prg =
let body, typ = subst_body true prg in
let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
(Evd.evar_universe_context_subst prg.prg_ctx) in
+ let opaque = prg.prg_opaque in
let ce =
- definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+ definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
in
progmap_remove prg;
@@ -564,6 +566,7 @@ let declare_mutual_definition l =
let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
let (local,poly,kind) = first.prg_kind in
let fixnames = first.prg_deps in
+ let opaque = first.prg_opaque in
let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
let indexes, fixdecls =
match fixkind with
@@ -584,7 +587,7 @@ let declare_mutual_definition l =
in
(* Declare the recursive definitions *)
let ctx = Evd.evar_context_universe_context first.prg_ctx in
- let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx)
+ let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation first.prg_notations;
@@ -640,7 +643,7 @@ let declare_obligation prg obl body ty uctx =
else
Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
-let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
let obls', b =
match b with
| None ->
@@ -664,7 +667,8 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook
prg_obligations = (obls', Array.length obls');
prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
- prg_hook = hook; }
+ prg_hook = hook;
+ prg_opaque = opaque; }
let get_prog name =
let prg_infos = !from_prg in
@@ -976,9 +980,9 @@ let show_term n =
++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
- ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
+ ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
let info = str (Id.to_string n) ++ str " has type-checked" in
- let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
+ let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose msg_info (info ++ str ".");
@@ -994,11 +998,11 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
| _ -> res)
let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
- ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
+ ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
List.iter
(fun (n, b, t, imps, obls) ->
- let prg = init_prog_info n (Some b) t ctx deps (Some fixkind)
+ let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
notations obls imps kind reduce hook
in progmap_add n prg) l;
let _defined =
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 582b49354..d39e18a48 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,7 +17,7 @@ open Decl_kinds
open Tacexpr
(** Forward declaration. *)
-val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
val declare_definition_ref :
@@ -69,7 +69,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
?kind:Decl_kinds.definition_kind ->
?tactic:unit Proofview.tactic ->
?reduce:(Term.constr -> Term.constr) ->
- ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress
+ ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
type notations =
(Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -85,7 +85,7 @@ val add_mutual_definitions :
?tactic:unit Proofview.tactic ->
?kind:Decl_kinds.definition_kind ->
?reduce:(Term.constr -> Term.constr) ->
- ?hook:unit Lemmas.declaration_hook ->
+ ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
notations ->
fixpoint_kind -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 11:33:11 +0000