From 2a28c677c3c205ff453b7b5903e4c22f4de2649b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 6 Jul 2015 23:37:42 +0200
Subject: Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its
verbose flag.
---
toplevel/vernac.ml | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index bc8aa2fffa..966b952016 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -215,7 +215,7 @@ let display_cmd_header loc com =
str " [" ++ str cmd ++ str "] ");
Pp.flush_all ()
-let rec vernac_com checknav (loc,com) =
+let rec vernac_com verbose checknav (loc,com) =
let interp = function
| VernacLoad (verbosely, fname) ->
let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in
@@ -241,7 +241,7 @@ let rec vernac_com checknav (loc,com) =
| v when !just_parsing -> ()
- | v -> Stm.interp (Flags.is_verbose()) (loc,v)
+ | v -> Stm.interp verbose (loc,v)
in
try
checknav loc com;
@@ -268,7 +268,7 @@ and read_vernac_file verbosely s =
* raised, which means that we raised the end of the file being loaded *)
while true do
let loc_ast = parse_sentence input in
- vernac_com checknav loc_ast;
+ vernac_com verbosely checknav loc_ast;
pp_flush ()
done
with any -> (* whatever the exception *)
@@ -293,7 +293,7 @@ let checknav loc ast =
if is_deep_navigation_vernac ast then
user_error loc "Navigation commands forbidden in nested commands"
-let eval_expr loc_ast = vernac_com checknav loc_ast
+let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
--
cgit v1.2.3
From 6f2db13c8677fd0148279483359e75b9f128aebc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 16:02:13 +0200
Subject: Univs/minimization: Fix unused variable bug.
---
library/universes.ml | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/library/universes.ml b/library/universes.ml
index a3926bc6f2..1c8a5ad77d 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -723,7 +723,10 @@ let pr_constraints_map cmap =
prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl ()
++ acc)
cmap (mt ())
-
+
+let remove_alg l (ctx, us, algs, insts, cstrs) =
+ (ctx, us, LSet.remove l algs, insts, cstrs)
+
let minimize_univ_variables ctx us algs left right cstrs =
let left, lbounds =
Univ.LMap.fold (fun r lower (left, lbounds as acc) ->
@@ -767,8 +770,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
if not (Level.equal l u) then
(* Should check that u does not
have upper constraints that are not already in right *)
- let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in
- instantiate_with_lbound u lbound false false acc
+ let acc' = remove_alg l acc in
+ instantiate_with_lbound u lbound false false acc'
else acc, (true, false, lbound)
| None ->
try
--
cgit v1.2.3
From 024a7ab20b06d82571c68c3d2ac32cb60fb0053a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 16:02:35 +0200
Subject: test-suite: Fix test-suite Makefile
Using relative path for coqlib, for some reason this fails on Mac OS
X. Took the easiest way to fix it.
---
test-suite/Makefile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 476d850ac9..d2466250ab 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -28,7 +28,7 @@
# Default value when called from a freshly compiled Coq, but can be
# easily overridden
BIN := ../bin/
-LIB := ..
+LIB := $(shell cd ..; pwd)
coqtop := $(BIN)coqtop -boot -q -batch -test-mode -R prerequisite TestSuite
bincoqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
--
cgit v1.2.3
From 7c7726a798caa6b506a727703de24d2bb5bb3956 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:04:45 +0200
Subject: Univs: bug fix.
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
---
kernel/inductive.ml | 10 +++++-----
pretyping/inductiveops.ml | 3 ++-
test-suite/success/polymorphism.v | 12 ++++++++++++
3 files changed, 19 insertions(+), 6 deletions(-)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4c1614bac1..35b29e73a6 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -96,11 +96,11 @@ let full_inductive_instantiate mib u params sign =
let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
Vars.subst_instance_context u ar
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
- let inst_ind = constructor_instantiate mind u mib in
- (fun t ->
- instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
-
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+ let inst_ind = constructor_instantiate mind u mib t in
+ instantiate_params true inst_ind params
+ (Vars.subst_instance_context u mib.mind_params_ctxt)
+
(************************************************************************)
(************************************************************************)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 90aa8000a8..cb091f2d6f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -322,7 +322,8 @@ let instantiate_params t args sign =
let get_constructor ((ind,u as indu),mib,mip,params) j =
assert (j <= Array.length mip.mind_consnames);
let typi = mis_nf_constructor_type (indu,mib,mip) j in
- let typi = instantiate_params typi params mib.mind_params_ctxt in
+ let ctx = Vars.subst_instance_context u mib.mind_params_ctxt in
+ let typi = instantiate_params typi params ctx in
let (args,ccl) = decompose_prod_assum typi in
let (_,allargs) = decompose_app ccl in
let vargs = List.skipn (List.length params) allargs in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index dc22b03f2d..957612ef1d 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -308,3 +308,15 @@ Definition RLRL' : forall x : R, RL x = RL (RL x).
Qed.
End eta.
+
+Module Hurkens'.
+ Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
+Type)) eq_refl.
+
+End Hurkens'.
\ No newline at end of file
--
cgit v1.2.3
From 3264fdaa71b2327a992286a08df0dfbcf78ea4fe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:31:04 +0200
Subject: Checker: Fix bug #4282
Adapt to new [projection] abstract type comprising a constant and
a boolean.
---
checker/cic.mli | 2 +-
checker/closure.ml | 11 ++++++-----
checker/closure.mli | 4 ++--
checker/declarations.ml | 13 +++++++------
checker/environ.ml | 4 ++--
checker/environ.mli | 2 +-
checker/print.ml | 2 +-
checker/reduction.ml | 6 ++++--
checker/term.ml | 2 +-
checker/values.ml | 11 +++++++----
test-suite/coqchk/primproj.v | 2 ++
11 files changed, 34 insertions(+), 25 deletions(-)
create mode 100644 test-suite/coqchk/primproj.v
diff --git a/checker/cic.mli b/checker/cic.mli
index e875e40f0a..d75af76547 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
| Case of case_info * constr * constr * constr array
| Fix of constr pfixpoint
| CoFix of constr pcofixpoint
- | Proj of constant * constr
+ | Proj of projection * constr
type existential = constr pexistential
type rec_declaration = constr prec_declaration
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683fa8..c6cc2185d3 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * constant
+ | Zproj of int * int * projection
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
let (depth, args, s) = strip_update_shift_app m s in
(** Try to drop the params, might fail on partially applied constructors. *)
let argss = try_drop_parameters depth pars args in
- let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
- term = FProj (p, right) }) projs in
+ let hstack =
+ Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+ term = FProj (Projection.make p false, right) }) projs in
argss, [Zapp hstack]
| _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
@@ -738,7 +739,7 @@ let rec knh info m stk =
| FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
- if red_set info.i_flags (fCONST p) then
+ if red_set info.i_flags (fCONST (Projection.constant p)) then
(let pb = lookup_projection p (info.i_env) in
knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
:: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250d6..376e9fef7d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
| FInd of pinductive
| FConstruct of pconstructor
| FApp of fconstr * fconstr array
- | FProj of constant * fconstr
+ | FProj of projection * fconstr
| FFix of fixpoint * fconstr subs
| FCoFix of cofixpoint * fconstr subs
| FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
| Zapp of fconstr array
| Zcase of case_info * fconstr * fconstr array
| ZcaseT of case_info * constr * constr array * fconstr subs
- | Zproj of int * int * constant
+ | Zproj of int * int * projection
| Zfix of fconstr * stack
| Zshift of int
| Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475f9..36e6a7caba 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
let func = map_kn f f' in
match c with
| Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
- | Proj (kn,t) ->
- let kn' =
- try fst (f' kn Univ.Instance.empty)
- with No_subst -> kn
+ | Proj (p,t) ->
+ let p' =
+ Projection.map (fun kn ->
+ try fst (f' kn Univ.Instance.empty)
+ with No_subst -> kn) p
in
let t' = func t in
- if kn' == kn && t' == t then c
- else Proj (kn', t')
+ if p' == p && t' == t then c
+ else Proj (p', t')
| Ind ((kn,i),u) ->
let kn' = f kn in
if kn'==kn then c else Ind ((kn',i),u)
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc7127..c0f366000a 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -147,8 +147,8 @@ let evaluable_constant cst env =
let is_projection cst env =
not (Option.is_empty (lookup_constant cst env).const_proj)
-let lookup_projection cst env =
- match (lookup_constant cst env).const_proj with
+let lookup_projection p env =
+ match (lookup_constant (Projection.constant p) env).const_proj with
| Some pb -> pb
| None -> anomaly ("lookup_projection: constant is not a projection")
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b127f..22fe7d8f17 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -51,7 +51,7 @@ val constant_value : env -> constant puniverses -> constr
val evaluable_constant : constant -> env -> bool
val is_projection : constant -> env -> bool
-val lookup_projection : constant -> env -> projection_body
+val lookup_projection : projection -> env -> projection_body
(* Inductives *)
val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff774..7624fd3257 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
done
in print_string"{"; print_fix (); print_string"}"
| Proj (p, c) ->
- print_string "Proj("; sp_con_display p; print_string ",";
+ print_string "Proj("; sp_con_display (Projection.constant p); print_string ",";
box_display c; print_string ")"
and box_display c = open_hovbox 1; term_display c; close_box()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28fdb130e8..58f0f894ff 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
type lft_constr_stack_elt =
Zlapp of (lift * fconstr) array
- | Zlproj of Names.constant * lift
+ | Zlproj of Names.projection * lift
| Zlfix of (lift * fconstr) * lft_constr_stack
| Zlcase of case_info * lift * fconstr * fconstr array
and lft_constr_stack = lft_constr_stack_elt list
@@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
| (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
f fx1 fx2; cmp_rec a1 a2
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
- if not (Names.eq_con_chk c1 c2) then
+ if not (Names.eq_con_chk
+ (Names.Projection.constant c1)
+ (Names.Projection.constant c2)) then
raise NotConvertible
| (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
if not (fmind ci1.ci_ind ci2.ci_ind) then
diff --git a/checker/term.ml b/checker/term.ml
index 93540276b7..430be49519 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
Array.equal f tl1 tl2 && Array.equal f bl1 bl2
| CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
- | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+ | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
| _ -> false
let rec eq_constr m n =
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d4..46b66adc4a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
*)
@@ -126,6 +126,7 @@ let v_caseinfo =
v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
let rec v_constr =
Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
[|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
[|v_fix|]; (* Fix *)
[|v_cofix|]; (* CoFix *)
- [|v_cst;v_constr|] (* Proj *)
+ [|v_proj;v_constr|] (* Proj *)
|])
and v_prec = Tuple ("prec_declaration",
@@ -205,8 +206,10 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_projbody =
- v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
- v_constr|]
+ v_tuple "projection_body"
+ [|v_cst;Int;Int;v_constr;
+ v_tuple "proj_eta" [|v_constr;v_constr|];
+ v_constr|]
let v_cb = v_tuple "constant_body"
[|v_section_ctxt;
diff --git a/test-suite/coqchk/primproj.v b/test-suite/coqchk/primproj.v
new file mode 100644
index 0000000000..04d0a2b6f7
--- /dev/null
+++ b/test-suite/coqchk/primproj.v
@@ -0,0 +1,2 @@
+Set Primitive Projections.
+Record foo (T : Type) := { bar : T}.
--
cgit v1.2.3
From f29b968c54889dd82fd07d50bc6a52b63ea4edf0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:53:54 +0200
Subject: Document Set/Print Firstorder Solver option.
---
doc/refman/RefMan-tac.tex | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index be82eaa018..8f9ba1ec60 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4164,6 +4164,12 @@ first-order reasoning, written by Pierre Corbineau.
It is not restricted to usual logical connectives but
instead may reason about any first-order class inductive definition.
+The default tactic used by \texttt{firstorder} when no rule applies is {\tt
+ auto with *}, it can be reset locally or globally using the {\nobreak
+ {\tt Set Firstorder Solver {\tac}}} \optindex{Firstorder Solver}
+vernacular command and printed using {\nobreak {\tt Print Firstorder
+ Solver}}.
+
\begin{Variants}
\item {\tt firstorder {\tac}}
\tacindex{firstorder {\tac}}
--
cgit v1.2.3
From 6a0b36f13e9b9ebd693cc2b1688ace9905aa4042 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 8 Jul 2015 07:35:38 +0200
Subject: Use the same optimization level for the VM, whatever the debug level.
---
configure.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/configure.ml b/configure.ml
index 1916e82172..c759782d9d 100644
--- a/configure.ml
+++ b/configure.ml
@@ -396,7 +396,7 @@ let coq_annotate_flag =
then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
else ""
-let cflags = "-Wall -Wno-unused -g " ^ (if !Prefs.debug then "-O1" else "-O2")
+let cflags = "-Wall -Wno-unused -g -O2"
(** * Architecture *)
--
cgit v1.2.3
From c075edff6e7bd7295bcbc859b01dbcf787457e0e Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 8 Jul 2015 11:11:25 +0200
Subject: Fix documentation.
---
doc/refman/CanonicalStructures.tex | 94 +++++++++++++++++++-------------------
1 file changed, 47 insertions(+), 47 deletions(-)
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index b1c278cede..a3372c2965 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -41,25 +41,25 @@ End EQ.
We use Coq modules as name spaces. This allows us to follow the same pattern
and naming convention for the rest of the chapter. The base name space
contains the definitions of the algebraic structure. To keep the example
-small, the algebraic structure $EQ.type$ we are defining is very simplistic,
+small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic,
and characterizes terms on which a binary relation is defined, without
requiring such relation to validate any property.
-The inner $theory$ module contains the overloaded notation $==$ and
+The inner \texttt{theory} module contains the overloaded notation \texttt{==} and
will eventually contain lemmas holding on all the instances of the
algebraic structure (in this case there are no lemmas).
-Note that in practice the user may want to declare $EQ.obj$ as a coercion,
+Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion,
but we will not do that here.
-The following line tests that, when we assume a type $e$ that is in the
-$EQ$ class, then we can relates two of its objects with $==$.
+The following line tests that, when we assume a type \texttt{e} that is in the
+\texttt{EQ} class, then we can relates two of its objects with \texttt{==}.
\begin{coq_example}
Import EQ.theory.
Check forall (e : EQ.type) (a b : EQ.obj e), a == b.
\end{coq_example}
-Still, no concrete type is in the $EQ$ class. We amend that by equipping $nat$
+Still, no concrete type is in the \texttt{EQ} class. We amend that by equipping \texttt{nat}
with a comparison relation.
\begin{coq_example}
@@ -71,23 +71,23 @@ Check 3 == 3.
Eval compute in 3 == 4.
\end{coq_example}
-This last test shows that Coq is now not only able to typecheck $3==3$, but
-also that the infix relation was bound to the $nat\_eq$ relation. This
-relation is selected whenever $==$ is used on terms of type $nat$. This
-can be read in the line declaring the canonical structure $nat\_EQty$,
-where the first argument to $Pack$ is the key and its second argument
+This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but
+also that the infix relation was bound to the \texttt{nat\_eq} relation. This
+relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}. This
+can be read in the line declaring the canonical structure \texttt{nat\_EQty},
+where the first argument to \texttt{Pack} is the key and its second argument
a group of canonical values associated to the key. In this case we associate
-to $nat$ only one canonical value (since its class, $nat\_EQcl$ has just one
-member). The use of the projection $op$ requires its argument to be in
-the class $EQ$, and uses such a member (function) to actually compare
+to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one
+member). The use of the projection \texttt{op} requires its argument to be in
+the class \texttt{EQ}, and uses such a member (function) to actually compare
its arguments.
Similarly, we could equip any other type with a comparison relation, and
-use the $==$ notation on terms of this type.
+use the \texttt{==} notation on terms of this type.
\subsection{Derived Canonical Structures}
-We know how to use $==$ on base types, like $nat$, $bool$, $Z$.
+We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}.
Here we show how to deal with type constructors, i.e. how to make the
following example work:
@@ -109,18 +109,18 @@ Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b).
Check forall n m : nat, (3,4) == (n,m).
\end{coq_example}
-Thanks to the $pair\_EQty$ declaration, Coq is able to build a comparison
+Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison
relation for pairs whenever it is able to build a comparison relation
for each component of the pair. The declaration associates to the key
-$*$ (the type constructor of pairs) the canonical comparison relation
-$pair\_eq$ whenever the type constructor $*$ is applied to two types
-being themselves in the $EQ$ class.
+\texttt{*} (the type constructor of pairs) the canonical comparison relation
+\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types
+being themselves in the \texttt{EQ} class.
\section{Hierarchy of structures}
To get to an interesting example we need another base class to be available.
We choose the class of types that are equipped with an order relation,
-to which we associate the infix $<=$ notation.
+to which we associate the infix \texttt{<=} notation.
\begin{coq_example}
Module LE.
@@ -136,7 +136,7 @@ Module LE.
End LE.
\end{coq_example}
-As before we register a canonical $LE$ class for $nat$.
+As before we register a canonical \texttt{LE} class for \texttt{nat}.
\begin{coq_example}
Import LE.theory.
@@ -145,7 +145,7 @@ Definition nat_LEcl : LE.class nat := LE.Class nat_le.
Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl.
\end{coq_example}
-And we enable Coq to relate pair of terms with $<=$.
+And we enable Coq to relate pair of terms with \texttt{<=}.
\begin{coq_example}
Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) :=
@@ -156,7 +156,7 @@ Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type :=
Check (3,4,5) <= (3,4,5).
\end{coq_example}
-At the current stage we can use $==$ and $<=$ on concrete types,
+At the current stage we can use \texttt{==} and \texttt{<=} on concrete types,
like tuples of natural numbers, but we can't develop an algebraic
theory over the types that are equipped with both relations.
@@ -166,7 +166,7 @@ Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y.
Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y.
\end{coq_example}
-We need to define a new class that inherits from both $EQ$ and $LE$.
+We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}.
\begin{coq_example}
Module LEQ.
@@ -181,8 +181,8 @@ Module LEQ.
Arguments Class {T} _ _ _.
\end{coq_example}
-The $mixin$ component of the $LEQ$ class contains all the extra content
-we are adding to $EQ$ and $LE$. In particular it contains the requirement
+The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content
+we are adding to \texttt{EQ} and \texttt{LE}. In particular it contains the requirement
that the two relations we are combining are compatible.
Unfortunately there is still an obstacle to developing the algebraic theory
@@ -193,12 +193,12 @@ of this new class.
Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m.
\end{coq_example}
-The problem is that the two classes $LE$ and $LEQ$ are not yet related by
+The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by
a subclass relation. In other words Coq does not see that an object
-of the $LEQ$ class is also an object of the $LE$ class.
+of the \texttt{LEQ} class is also an object of the \texttt{LE} class.
The following two constructions tell Coq how to canonically build
-the $LE.type$ and $EQ.type$ structure given an $LEQ.type$ structure
+the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure
on the same type.
\begin{coq_example}
@@ -209,7 +209,7 @@ on the same type.
LE.Pack (obj e) (LE_class _ (class_of e)).
Canonical Structure to_LE.
\end{coq_example}
-We can now formulate out first theorem on the objects of the $LEQ$ structure.
+We can now formulate out first theorem on the objects of the \texttt{LEQ} structure.
\begin{coq_example}
Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y.
now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed.
@@ -231,8 +231,8 @@ Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) :
Fail apply (lele_eq n m). Abort.
\end{coq_example}
-Again one has to tell Coq that the type $nat$ is in the $LEQ$ class, and how
-the type constructor $*$ interacts with the $LEQ$ class. In the following
+Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how
+the type constructor \texttt{*} interacts with the \texttt{LEQ} class. In the following
proofs are omitted for brevity.
\begin{coq_example}
@@ -271,8 +271,8 @@ Qed.
Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2).
\end{coq_example}
-The following script registers an $LEQ$ class for $nat$ and for the
-type constructor $*$. It also tests that they work as expected.
+The following script registers an \texttt{LEQ} class for \texttt{nat} and for the
+type constructor \texttt{*}. It also tests that they work as expected.
Unfortunately, these declarations are very verbose. In the following
subsection we show how to make these declaration more compact.
@@ -294,9 +294,9 @@ Module Add_instance_attempt.
End Add_instance_attempt.
\end{coq_example}
-Note that no direct proof of $n <= m -> m <= n -> n == m$ is provided by the
-user for $n$ and $m$ of type $nat * nat$. What the user provides is a proof of
-this statement for $n$ and $m$ of type $nat$ and a proof that the pair
+Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the
+user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}. What the user provides is a proof of
+this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair
constructor preserves this property. The combination of these two facts is a
simple form of proof search that Coq performs automatically while inferring
canonical structures.
@@ -334,7 +334,7 @@ problem, that will in turn require the inference of some canonical
structures. They are explained in mode details in~\cite{CSwcu}.
We now have all we need to create a compact ``packager'' to declare
-instances of the $LEQ$ class.
+instances of the \texttt{LEQ} class.
\begin{coq_example}
Import infrastructure.
@@ -348,17 +348,17 @@ Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) :=
Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id).
\end{coq_example}
-The object $Pack$ takes a type $T$ (the key) and a mixin $m$. It infers all
-the other pieces of the class $LEQ$ and declares them as canonical values
-associated to the $T$ key. All in all, the only new piece of information
-we add in the $LEQ$ class is the mixin, all the rest is already canonical
-for $T$ and hence can be inferred by Coq.
+The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}. It infers all
+the other pieces of the class \texttt{LEQ} and declares them as canonical values
+associated to the \texttt{T} key. All in all, the only new piece of information
+we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical
+for \texttt{T} and hence can be inferred by Coq.
-$Pack$ is a notation, hence it is not type checked at the time of its
+\texttt{Pack} is a notation, hence it is not type checked at the time of its
declaration. It will be type checked when it is used, an in that case
-$T$ is going to be a concrete type. The odd arguments $\_$ and $id$ we
+\texttt{T} is going to be a concrete type. The odd arguments \texttt{\_} and \texttt{id} we
pass to the
-packager represent respectively the classes to be inferred (like $e$, $o$, etc) and a token ($id$) to force their inference. Again, for all the details the
+packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference. Again, for all the details the
reader can refer to~\cite{CSwcu}.
The declaration of canonical instances can now be way more compact:
--
cgit v1.2.3
From 002606c190a69e02f3d8b722eb64bae02e457f98 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 8 Jul 2015 11:11:50 +0200
Subject: Fix command-line documentation of coq-tex.
---
tools/coq_tex.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index a2cc8384c6..7f2fe741e9 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -249,7 +249,7 @@ let files = ref []
let parse_cl () =
Arg.parse
[ "-o", Arg.String (fun s -> output_specified := true; output := s),
- "output-file Specifiy the resulting LaTeX file";
+ "output-file Specify the resulting LaTeX file";
"-n", Arg.Int (fun n -> linelen := n),
"line-width Set the line width";
"-image", Arg.String (fun s -> image := s),
@@ -265,7 +265,7 @@ let parse_cl () =
"-small", Arg.Set small,
" Coq parts are written in small font";
"-boot", Arg.Set boot,
- " Launch coqtop with the -boot option"
+ " Launch coqtop with the -boot option"
]
(fun s -> files := s :: !files)
"coq-tex [options] file ..."
@@ -290,7 +290,7 @@ let main () =
let _ = Sys.command (!image ^ " -batch") in
exit 1
end else begin
- Printf.printf "Your version of coqtop seems OK\n";
+ (*Printf.printf "Your version of coqtop seems OK\n";*)
flush stdout
end;
List.iter one_file (List.rev !files)
--
cgit v1.2.3
From 8b093fa1828eee800da2bc73de33ea8804175924 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 8 Jul 2015 16:38:34 +0200
Subject: Make sure that scope classes are displayed by Print Scopes. (Fix bug
#4262)
---
interp/notation.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/interp/notation.ml b/interp/notation.ml
index 0b5791d32b..d18b804bfd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -796,8 +796,8 @@ let pr_scope_classes sc =
let l = classes_of_scope sc in
match l with
| [] -> mt ()
- | _ :: l ->
- let opt_s = match l with [] -> mt () | _ -> str "es" in
+ | _ :: ll ->
+ let opt_s = match ll with [] -> mt () | _ -> str "es" in
hov 0 (str "Bound to class" ++ opt_s ++
spc() ++ prlist_with_sep spc pr_scope_class l) ++ fnl()
--
cgit v1.2.3
From 32dc4dc94c5677bc686a16a4a047f1750d0d8582 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 16:57:15 +0200
Subject: Fix documentation of universes.
---
doc/refman/Universes.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 3414311148..018d73908b 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -93,7 +93,7 @@ of monoids).
\begin{coq_example*}
Polymorphic Definition monoid_monoid : Monoid.
- refine (@Build_Monoid Monoid unit_monoid _) ; admit.
+ refine (@Build_Monoid Monoid unit_monoid (fun x y => x)).
Defined.
\end{coq_example*}
\begin{coq_example}
--
cgit v1.2.3
From c71cff0328fa0ee640f35337278f344e0d00698a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 12:44:59 +0200
Subject: Checker: Report bugfixes from kernel/inductive.ml
Wrong handling of mind_params_ctxt...
---
checker/inductive.ml | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645a5..1c8f570df9 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,12 +104,14 @@ let instantiate_params full t u args sign =
let full_inductive_instantiate mib u params sign =
let dummy = Prop Null in
let t = mkArity (sign,dummy) in
- fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+ let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
+ subst_instance_context u ar
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
- let inst_ind = constructor_instantiate mind u mib in
- (fun t ->
- instantiate_params true (inst_ind t) u params mib.mind_params_ctxt)
+
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+ let inst_ind = constructor_instantiate mind u mib t in
+ instantiate_params true inst_ind u params
+ (subst_instance_context u mib.mind_params_ctxt)
(************************************************************************)
(************************************************************************)
--
cgit v1.2.3
From 8ad5f5726283c69a71f7ee0f2d12ce94b707b5a6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 17:39:03 +0200
Subject: Bug 4284: Tentative bugfix for detyping exception.
---
ide/ide_slave.ml | 12 +++++++-----
1 file changed, 7 insertions(+), 5 deletions(-)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index dc52ea9aad..6618dc7ef9 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -185,12 +185,14 @@ let process_goal sigma g =
let ccl =
let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
- let process_hyp d =
+ let process_hyp d (env,l) =
let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
- (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in
- let hyps =
- List.map process_hyp
- (Termops.compact_named_context_reverse (Environ.named_context env)) in
+ let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+ (List.fold_right Environ.push_named d' env,
+ (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+ let (_env, hyps) =
+ Context.fold_named_list_context process_hyp
+ (Termops.compact_named_context_reverse (Environ.named_context env)) ~init:(min_env,[]) in
{ Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
let export_pre_goals pgs =
--
cgit v1.2.3
From a198b3f7402d4b275a7fc67ece827843f00dadf0 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 17:57:54 +0200
Subject: Ide: fix bug #4284 for good
Correct folding order over the named_list_context.
---
ide/ide_slave.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6618dc7ef9..94f9c9a361 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -192,8 +192,8 @@ let process_goal sigma g =
(string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
let (_env, hyps) =
Context.fold_named_list_context process_hyp
- (Termops.compact_named_context_reverse (Environ.named_context env)) ~init:(min_env,[]) in
- { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
+ (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
+ { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
let export_pre_goals pgs =
{
--
cgit v1.2.3
From 7bda7d7070fc55fc38fef4c21557ea61b0c4d17d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 9 Jul 2015 14:50:16 +0900
Subject: Fixing printing of primitive coinductive record status.
They do not have eta-rule indeed, even though it was displayed as such.
---
printing/prettyp.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e50435cda2..b8c5fd4cfc 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -205,16 +205,20 @@ let print_polymorphism ref =
else "not universe polymorphic") ]
else []
-let print_primitive_record mipv = function
+let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
- [pr_id mipv.(0).mind_typename ++ str" is primitive and has eta conversion."]
+ let eta = match recflag with
+ | Decl_kinds.CoFinite -> mt ()
+ | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+ in
+ [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
| _ -> []
let print_primitive ref =
match ref with
| IndRef ind ->
let mib,_ = Global.lookup_inductive ind in
- print_primitive_record mib.mind_packets mib.mind_record
+ print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record
| _ -> []
let print_name_infos ref =
@@ -447,7 +451,7 @@ let gallina_print_inductive sp =
let mipv = mib.mind_packets in
pr_mutual_inductive_body env sp mib ++
with_line_skip
- (print_primitive_record mipv mib.mind_record @
+ (print_primitive_record mib.mind_finite mipv mib.mind_record @
print_inductive_renames sp mipv @
print_inductive_implicit_args sp mipv @
print_inductive_argument_scopes sp mipv)
--
cgit v1.2.3
From 1bf30962d7cd5732393d7722ae6d263d4c812ec8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 10:32:17 +0200
Subject: Make retyping of projections more resilient to wrong environment.
Unfortunately, it seems that retyping can be called in ill-typed terms and/or in
the wrong environment. This was broken for projections by my commit
a51cce369b9c634a93120092d4c7685a242d55b1
---
pretyping/retyping.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 743bc3b19b..fb55265526 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -126,9 +126,11 @@ let retype ?(polyprop=true) sigma =
| App(f,args) ->
strip_outer_cast
(subst_type env sigma (type_of env f) (Array.to_list args))
- | Proj (p,c) ->
+ | Proj (p,c) ->
let ty = type_of env c in
- Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+ (try
+ Inductiveops.type_of_projection_knowing_arg env sigma p c ty
+ with Invalid_argument _ -> retype_error BadRecursiveType)
| Cast (c,_, t) -> t
| Sort _ | Prod _ -> mkSort (sort_of env cstr)
--
cgit v1.2.3
From 3a6b08286ac78c674d6d3e3073b38de26a610fdc Mon Sep 17 00:00:00 2001
From: mlasson
Date: Mon, 22 Jun 2015 21:14:20 +0200
Subject: Template polymorphism: A bug-fix for Bug #4258
Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.
I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
---
checker/inductive.ml | 83 ++++++++++++++++++++++++++++------------------------
kernel/indtypes.ml | 39 +++++++-----------------
kernel/inductive.ml | 76 +++++++++++++++++++++++++++--------------------
3 files changed, 101 insertions(+), 97 deletions(-)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 1c8f570df9..5d31649737 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -144,53 +144,60 @@ let sort_as_univ = function
| Prop Null -> Univ.type0m_univ
| Prop Pos -> Univ.type0_univ
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
let cons_subst u su subst =
- Univ.LMap.add u su subst
-
-let actualize_decl_level env lev t =
- let sign,s = dest_arity env t in
- mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
+ try
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+ try
+ let su = Universe.make u in
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> subst
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env = function
- | (_,Some _,_ as t)::sign, exp, args ->
- let ctx,subst = make_subst env (sign, exp, args) in
- t::ctx, subst
- | d::sign, None::exp, args ->
- let args = match args with _::args -> args | [] -> [] in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, subst
- | d::sign, Some u::exp, a::args ->
- (* We recover the level of the argument, but we don't change the *)
- (* level in the corresponding type in the arity; this level in the *)
- (* arity is a global level which, at typing time, will be enforce *)
- (* to be greater than the level of the argument; this is probably *)
- (* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env a)) in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, cons_subst u s subst
- | (na,None,t as d)::sign, Some u::exp, [] ->
- (* No more argument here: we instantiate the type with a fresh level *)
- (* which is first propagated to the corresponding premise in the arity *)
- (* (actualize_decl_level), then to the conclusion of the arity (via *)
- (* the substitution) *)
- let ctx,subst = make_subst env (sign, exp, []) in
- d::ctx, subst
- | sign, [], _ ->
- (* Uniform parameters are exhausted *)
- sign,Univ.LMap.empty
- | [], _, _ ->
- assert false
-
+let rec make_subst env =
+ let rec make subst = function
+ | (_,Some _,_ as t)::sign, exp, args ->
+ make subst (sign, exp, args)
+ | d::sign, None::exp, args ->
+ let args = match args with _::args -> args | [] -> [] in
+ make subst (sign, exp, args)
+ | d::sign, Some u::exp, a::args ->
+ (* We recover the level of the argument, but we don't change the *)
+ (* level in the corresponding type in the arity; this level in the *)
+ (* arity is a global level which, at typing time, will be enforce *)
+ (* to be greater than the level of the argument; this is probably *)
+ (* a useless extra constraint *)
+ let s = sort_as_univ (snd (dest_arity env a)) in
+ make (cons_subst u s subst) (sign, exp, args)
+ | (na,None,t as d)::sign, Some u::exp, [] ->
+ (* No more argument here: we add the remaining universes to the *)
+ (* substitution (when [u] is distinct from all other universes in the *)
+ (* template, it is identity substitution otherwise (ie. when u is *)
+ (* already in the domain of the substitution) [remember_subst] will *)
+ (* update its image [x] by [sup x u] in order not to forget the *)
+ (* dependency in [u] that remains to be fullfilled. *)
+ make (remember_subst u subst) (sign, exp, [])
+ | sign, [], _ ->
+ (* Uniform parameters are exhausted *)
+ subst
+ | [], _, _ ->
+ assert false
+ in
+ make Univ.LMap.empty
exception SingletonInductiveBecomesProp of Id.t
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+ let subst = make_subst env (ctx,ar.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6b909824ba..e80a3a5a42 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -175,36 +175,19 @@ let cumulate_arity_large_levels env sign =
let is_impredicative env u =
is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+ polymorphism. The elements x_k is None if the k-th parameter (starting
+ from the most recent and ignoring let-definitions) is not contributing
+ or is Some u_k if its level is u_k and is contributing. *)
let param_ccls params =
- let has_some_univ u = function
- | Some v when Univ.Level.equal u v -> true
- | _ -> false
+ let fold acc = function (_, None, p) ->
+ (let c = strip_prod_assum p in
+ match kind_of_term c with
+ | Sort (Type u) -> Univ.Universe.level u
+ | _ -> None) :: acc
+ | _ -> acc
in
- let remove_some_univ u = function
- | Some v when Univ.Level.equal u v -> None
- | x -> x
- in
- let fold l (_, b, p) = match b with
- | None ->
- (* Parameter contributes to polymorphism only if explicit Type *)
- let c = strip_prod_assum p in
- (* Add Type levels to the ordered list of parameters contributing to *)
- (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
- begin match kind_of_term c with
- | Sort (Type u) ->
- (match Univ.Universe.level u with
- | Some u ->
- if List.exists (has_some_univ u) l then
- None :: List.map (remove_some_univ u) l
- else
- Some u :: l
- | None -> None :: l)
- | _ ->
- None :: l
- end
- | _ -> l
- in
- List.fold_left fold [] params
+ List.fold_left fold [] params
(* Type-check an inductive definition. Does not check positivity
conditions. *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 35b29e73a6..84084718f0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -134,46 +134,60 @@ let sort_as_univ = function
(* Template polymorphism *)
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
let cons_subst u su subst =
- Univ.LMap.add u su subst
+ try
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+ try
+ let su = Universe.make u in
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> subst
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env = function
- | (_,Some _,_ as t)::sign, exp, args ->
- let ctx,subst = make_subst env (sign, exp, args) in
- t::ctx, subst
- | d::sign, None::exp, args ->
- let args = match args with _::args -> args | [] -> [] in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, subst
- | d::sign, Some u::exp, a::args ->
- (* We recover the level of the argument, but we don't change the *)
- (* level in the corresponding type in the arity; this level in the *)
- (* arity is a global level which, at typing time, will be enforce *)
- (* to be greater than the level of the argument; this is probably *)
- (* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, cons_subst u s subst
- | (na,None,t as d)::sign, Some u::exp, [] ->
- (* No more argument here: we instantiate the type with a fresh level *)
- (* which is first propagated to the corresponding premise in the arity *)
- (* (actualize_decl_level), then to the conclusion of the arity (via *)
- (* the substitution) *)
- let ctx,subst = make_subst env (sign, exp, []) in
- d::ctx, subst
- | sign, [], _ ->
- (* Uniform parameters are exhausted *)
- sign, Univ.LMap.empty
- | [], _, _ ->
- assert false
+let rec make_subst env =
+ let rec make subst = function
+ | (_,Some _,_ as t)::sign, exp, args ->
+ make subst (sign, exp, args)
+ | d::sign, None::exp, args ->
+ let args = match args with _::args -> args | [] -> [] in
+ make subst (sign, exp, args)
+ | d::sign, Some u::exp, a::args ->
+ (* We recover the level of the argument, but we don't change the *)
+ (* level in the corresponding type in the arity; this level in the *)
+ (* arity is a global level which, at typing time, will be enforce *)
+ (* to be greater than the level of the argument; this is probably *)
+ (* a useless extra constraint *)
+ let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+ make (cons_subst u s subst) (sign, exp, args)
+ | (na,None,t as d)::sign, Some u::exp, [] ->
+ (* No more argument here: we add the remaining universes to the *)
+ (* substitution (when [u] is distinct from all other universes in the *)
+ (* template, it is identity substitution otherwise (ie. when u is *)
+ (* already in the domain of the substitution) [remember_subst] will *)
+ (* update its image [x] by [sup x u] in order not to forget the *)
+ (* dependency in [u] that remains to be fullfilled. *)
+ make (remember_subst u subst) (sign, exp, [])
+ | sign, [], _ ->
+ (* Uniform parameters are exhausted *)
+ subst
+ | [], _, _ ->
+ assert false
+ in
+ make Univ.LMap.empty
exception SingletonInductiveBecomesProp of Id.t
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+ let subst = make_subst env (ctx,ar.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
--
cgit v1.2.3
From 26911bbc0bb3347c922d12b07a1c2bc34bba3c8d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 13:55:36 +0200
Subject: Improve semantics of -native-compiler flag.
Since Guillaume's, launching coqtop without -native-compiler and call
native_compute would mean recompiling silently all dependencies, even if they
had been precompiled (e.g. the stdlib).
The new semantics is that -native-compiler disables separate compilation of the
current library, but still tries to load precompiled dependencies. If loading
fails when the flag is on, coqtop stays silent.
---
kernel/nativelib.ml | 8 +++++---
library/library.ml | 5 +++--
2 files changed, 8 insertions(+), 5 deletions(-)
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 7cb01b6955..70920f1bbe 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -110,9 +110,11 @@ let call_linker ?(fatal=true) prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
if not (Sys.file_exists f) then
- let msg = "Cannot find native compiler file " ^ f in
- if fatal then Errors.error msg
- else Pp.msg_warning (Pp.str msg)
+ begin
+ let msg = "Cannot find native compiler file " ^ f in
+ if fatal then Errors.error msg
+ else if !Flags.native_compiler then Pp.msg_warning (Pp.str msg)
+ end
else
(try
if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
diff --git a/library/library.ml b/library/library.ml
index a8fbe0841c..45fce1c26c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -169,8 +169,9 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- if !Flags.native_compiler then
- Nativelib.link_library ~prefix ~dirname ~basename:f
+ (* This will not produce errors or warnings if the native compiler was
+ not enabled *)
+ Nativelib.link_library ~prefix ~dirname ~basename:f
in
let rec aux = function
| [] -> link m; [libname]
--
cgit v1.2.3
From e1f5a499c43ec0d7b7ebe696941217fb503e2596 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:09:29 +0200
Subject: Kernel: primitive projections handling of let-ins
Fixes bug #4176 (actually two bugs in one)
Correct computation of the type of primitive projections in presence of
let-ins.
---
kernel/indtypes.ml | 57 ++++++++++++++++++++++++++++++-------------
kernel/indtypes.mli | 2 +-
test-suite/bugs/closed/4276.v | 11 +++++++++
3 files changed, 52 insertions(+), 18 deletions(-)
create mode 100644 test-suite/bugs/closed/4276.v
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e80a3a5a42..31c0e83c84 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -646,10 +646,28 @@ exception UndefinableExpansion
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
- mind_consnrealdecls mind_consnrealargs ctx =
+let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+ mind_consnrealdecls mind_consnrealargs paramslet ctx =
let mp, dp, l = repr_mind kn in
- let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+ (** We build a substitution smashing the lets in the record parameters so
+ that typechecking projections requires just a substitution and not
+ matching with a parameter context. *)
+ let indty, paramsletsubst =
+ let subst, inst =
+ List.fold_right
+ (fun (na, b, t) (subst, inst) ->
+ match b with
+ | None -> (mkRel 1 :: List.map (lift 1) subst,
+ mkRel 1 :: List.map (lift 1) inst)
+ | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
+ paramslet ([], [])
+ in
+ let subst = (* For the record parameter: *)
+ mkRel 1 :: List.map (lift 1) subst
+ in
+ let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+ ty, subst
+ in
let ci =
let print_info =
{ ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
@@ -662,34 +680,39 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
let len = List.length ctx in
let x = Name x in
let compat_body ccl i =
- (* [ccl] is defined in context [params;x:rp] *)
- (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+ (* [ccl] is defined in context [params;x:indty] *)
+ (* [ccl'] is defined in context [params;x:indty;x:indty] *)
let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 rp, ccl') in
+ let p = mkLambda (x, lift 1 indty, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
in
- let projections (na, b, t) (i, j, kns, pbs, subst) =
+ let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
match b with
- | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+ | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
+ substl letsubst c :: subst)
| None ->
match na with
| Name id ->
let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+ let projty = substl letsubst (liftn 1 j t) in
let ty = substl subst (liftn 1 j t) in
let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
let compat = compat_body ty (j - 1) in
- let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
- let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+ let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+ let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
let body = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = ty; proj_eta = etab, etat;
+ proj_arg = i; proj_type = projty; proj_eta = etab, etat;
proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+ (i + 1, j + 1, kn :: kns, body :: pbs,
+ fterm :: subst, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+ let (_, _, kns, pbs, subst, letsubst) =
+ List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ in
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
@@ -775,12 +798,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
else Univ.Instance.empty
in
let indsp = ((kn, 0), u) in
- let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+ let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
(try
- let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+ let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
compute_projections indsp pkt.mind_typename rid nparamargs params
- pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+ pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
in Some (Some (rid, kns, projs))
with UndefinableExpansion -> Some None)
| Some _ -> Some None
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7774e52e9c..01acdce5c8 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,5 +43,5 @@ val is_indices_matter : unit -> bool
val compute_projections : pinductive -> Id.t -> Id.t ->
int -> Context.rel_context -> int array -> int array ->
- Context.rel_context ->
+ Context.rel_context -> Context.rel_context ->
(constant array * projection_body array)
diff --git a/test-suite/bugs/closed/4276.v b/test-suite/bugs/closed/4276.v
new file mode 100644
index 0000000000..ba82e6c376
--- /dev/null
+++ b/test-suite/bugs/closed/4276.v
@@ -0,0 +1,11 @@
+Set Primitive Projections.
+
+Record box (T U : Type) (x := T) := wrap { unwrap : T }.
+Definition mybox : box True False := wrap _ _ I.
+Definition unwrap' := @unwrap.
+
+Definition bad' : True := mybox.(unwrap _ _).
+
+Fail Definition bad : False := unwrap _ _ mybox.
+
+(* Closed under the global context *)
\ No newline at end of file
--
cgit v1.2.3
From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:58:06 +0200
Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins.
Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
---
checker/inductive.ml | 7 ++-----
kernel/inductive.ml | 11 +++++------
test-suite/bugs/closed/4283.v | 8 ++++++++
3 files changed, 15 insertions(+), 11 deletions(-)
create mode 100644 test-suite/bugs/closed/4283.v
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5d31649737..e3d8dd2060 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,14 +104,11 @@ let instantiate_params full t u args sign =
let full_inductive_instantiate mib u params sign =
let dummy = Prop Null in
let t = mkArity (sign,dummy) in
- let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
- subst_instance_context u ar
-
+ fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
let inst_ind = constructor_instantiate mind u mib t in
- instantiate_params true inst_ind u params
- (subst_instance_context u mib.mind_params_ctxt)
+ instantiate_params true inst_ind u params mib.mind_params_ctxt
(************************************************************************)
(************************************************************************)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 84084718f0..00d14a25e2 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c =
let s = ind_subst mind mib u in
substl s (subst_instance_constr u c)
-let instantiate_params full t args sign =
+let instantiate_params full t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
@@ -81,7 +81,8 @@ let instantiate_params full t args sign =
(fun (_,copt,_) (largs,subs,ty) ->
match (copt, largs, kind_of_term ty) with
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
- | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t)
+ | (Some b,_,LetIn(_,_,_,t)) ->
+ (largs, (substl subs (subst_instance_constr u b))::subs, t)
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
sign
@@ -93,13 +94,11 @@ let instantiate_params full t args sign =
let full_inductive_instantiate mib u params sign =
let dummy = prop_sort in
let t = mkArity (sign,dummy) in
- let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
- Vars.subst_instance_context u ar
+ fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
let inst_ind = constructor_instantiate mind u mib t in
- instantiate_params true inst_ind params
- (Vars.subst_instance_context u mib.mind_params_ctxt)
+ instantiate_params true inst_ind u params mib.mind_params_ctxt
(************************************************************************)
(************************************************************************)
diff --git a/test-suite/bugs/closed/4283.v b/test-suite/bugs/closed/4283.v
new file mode 100644
index 0000000000..e06998b711
--- /dev/null
+++ b/test-suite/bugs/closed/4283.v
@@ -0,0 +1,8 @@
+Require Import Hurkens.
+
+Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }.
+
+Definition unwrap' := fun (X : Type) (b : box X) => let (unwrap) := b in unwrap.
+
+Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ Type)) eq_refl.
+
--
cgit v1.2.3
From c4486dfda07b872d20746778df5c443b052b92b9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 9 Jul 2015 21:08:44 +0200
Subject: Native compiler: refactor code handling pre-computed values.
Fixes #4139 (Not_found exception with Require in modules).
---
kernel/nativecode.ml | 18 +++++++++++-------
kernel/nativecode.mli | 26 +++++++++++++++-----------
kernel/nativelibrary.ml | 4 ++--
kernel/nativelibrary.mli | 2 +-
kernel/safe_typing.ml | 25 ++++++++++++++++---------
kernel/safe_typing.mli | 4 +++-
library/declaremods.ml | 10 +++-------
library/declaremods.mli | 2 +-
library/global.mli | 2 +-
9 files changed, 53 insertions(+), 40 deletions(-)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index f56b6f83e7..90c437bbfb 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
let symb_tbl = HashtblSymbol.create 211
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
let get_value tbl i =
match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
let symbols_tbl_name = Ginternal "symbols_tbl"
-let get_symbols_tbl () =
+let get_symbols () =
let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
@@ -2058,7 +2062,7 @@ let mk_internal_let s code =
(* ML Code for conversion function *)
let mk_conv_code env sigma prefix t1 t2 =
- clear_symb_tbl ();
+ clear_symbols ();
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
@@ -2080,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
let header = Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_symbols"),
[|MLglobal (Ginternal "()")|])) in
header::gl, (mind_updates, const_updates)
let mk_norm_code env sigma prefix t =
- clear_symb_tbl ();
+ clear_symbols ();
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
@@ -2098,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
let gl = List.rev (setref :: t1 :: gl) in
let header = Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_symbols"),
[|MLglobal (Ginternal "()")|])) in
header::gl, (mind_updates, const_updates)
let mk_library_header dir =
let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
[Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_library_native_symbols"),
[|MLglobal (Ginternal libname)|]))]
let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92dd8..5d4c9e1e2d 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
val mk_open : string -> global
+(* Precomputed values for a compilation unit *)
type symbol
+type symbols
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
type code_location_update
type code_location_updates
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff0b..443cd8c2a0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
- clear_symb_tbl ();
+ clear_symbols ();
let mlcode =
List.fold_left (translate_field prefix mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
let mlcode = add_header_comment (List.rev mlcode) time_info in
- mlcode, get_symbols_tbl ()
+ mlcode, get_symbols ()
| _ -> assert false
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a66fb715d9..29368d1408 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,4 +14,4 @@ open Nativecode
compiler *)
val dump_library : module_path -> dir_path -> env -> module_signature ->
- global list * symbol array
+ global list * symbols
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d9adca0c91..d8473183ab 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -125,7 +125,8 @@ type safe_environment =
type_in_type : bool;
required : vodigest DPMap.t;
loads : (module_path * module_body) list;
- local_retroknowledge : Retroknowledge.action list }
+ local_retroknowledge : Retroknowledge.action list;
+ native_symbols : Nativecode.symbols DPMap.t }
and modvariant =
| NONE
@@ -154,7 +155,8 @@ let empty_environment =
type_in_type = false;
required = DPMap.empty;
loads = [];
- local_retroknowledge = [] }
+ local_retroknowledge = [];
+ native_symbols = DPMap.empty }
let is_initial senv =
match senv.revstruct, senv.modvariant with
@@ -623,7 +625,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
required = senv.required;
loads = senv.loads@oldsenv.loads;
local_retroknowledge =
- senv.local_retroknowledge@oldsenv.local_retroknowledge }
+ senv.local_retroknowledge@oldsenv.local_retroknowledge;
+ native_symbols = senv.native_symbols}
let end_module l restype senv =
let mp = senv.modpath in
@@ -732,11 +735,14 @@ type compiled_library = {
comp_mod : module_body;
comp_deps : library_info array;
comp_enga : engagement option;
- comp_natsymbs : Nativecode.symbol array
+ comp_natsymbs : Nativecode.symbols
}
type native_library = Nativecode.global list
+let get_library_native_symbols senv dir =
+ DPMap.find dir senv.native_symbols
+
(** FIXME: MS: remove?*)
let current_modpath senv = senv.modpath
let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -773,17 +779,17 @@ let export ?except senv dir =
mod_retroknowledge = senv.local_retroknowledge
}
in
- let ast, values =
+ let ast, symbols =
if !Flags.native_compiler then
Nativelibrary.dump_library mp dir senv.env str
- else [], [||]
+ else [], Nativecode.empty_symbols
in
let lib = {
comp_name = dir;
comp_mod = mb;
comp_deps = Array.of_list (DPMap.bindings senv.required);
comp_enga = Environ.engagement senv.env;
- comp_natsymbs = values }
+ comp_natsymbs = symbols }
in
mp, lib, ast
@@ -796,7 +802,7 @@ let import lib cst vodigest senv =
let mb = lib.comp_mod in
let env = Environ.add_constraints mb.mod_constraints senv.env in
let env = Environ.push_context_set cst env in
- (mp, lib.comp_natsymbs),
+ mp,
{ senv with
env =
(let linkinfo =
@@ -805,7 +811,8 @@ let import lib cst vodigest senv =
Modops.add_linked_module mb linkinfo env);
modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
required = DPMap.add lib.comp_name vodigest senv.required;
- loads = (mp,mb)::senv.loads }
+ loads = (mp,mb)::senv.loads;
+ native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols }
(** {6 Safe typing } *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a57fb108c4..1e9cdbda0e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,8 @@ type compiled_library
type native_library = Nativecode.global list
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+
val start_library : DirPath.t -> module_path safe_transformer
val export :
@@ -146,7 +148,7 @@ val export :
(* Constraints are non empty iff the file is a vi2vo *)
val import : compiled_library -> Univ.universe_context_set -> vodigest ->
- (module_path * Nativecode.symbol array) safe_transformer
+ module_path safe_transformer
(** {6 Safe typing judgments } *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index a82f5260ba..f66656d09a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -845,10 +845,6 @@ type library_objects = Lib.lib_objects * Lib.lib_objects
(** For the native compiler, we cache the library values *)
-type library_values = Nativecode.symbol array
-let library_values =
- Summary.ref (Dirmap.empty : library_values Dirmap.t) ~name:"LIBVALUES"
-
let register_library dir cenv (objs:library_objects) digest univ =
let mp = MPfile dir in
let () =
@@ -857,15 +853,15 @@ let register_library dir cenv (objs:library_objects) digest univ =
ignore(Global.lookup_module mp);
with Not_found ->
(* If not, let's do it now ... *)
- let mp', values = Global.import cenv univ digest in
+ let mp' = Global.import cenv univ digest in
if not (ModPath.equal mp mp') then
anomaly (Pp.str "Unexpected disk module name");
- library_values := Dirmap.add dir values !library_values
in
let sobjs,keepobjs = objs in
do_module false Lib.load_objects 1 dir mp ([],Objs sobjs) keepobjs
-let get_library_symbols_tbl dir = Dirmap.find dir !library_values
+let get_library_native_symbols dir =
+ Safe_typing.get_library_native_symbols (Global.safe_env ()) dir
let start_library dir =
let mp = Global.start_library dir in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c3578ec421..319d168d05 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -75,7 +75,7 @@ val register_library :
Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest ->
Univ.universe_context_set -> unit
-val get_library_symbols_tbl : library_name -> Nativecode.symbol array
+val get_library_native_symbols : library_name -> Nativecode.symbols
val start_library : library_name -> unit
diff --git a/library/global.mli b/library/global.mli
index 248e1f86dd..75a1ebee94 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -102,7 +102,7 @@ val export : ?except:Future.UUIDSet.t -> DirPath.t ->
module_path * Safe_typing.compiled_library * Safe_typing.native_library
val import :
Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest ->
- module_path * Nativecode.symbol array
+ module_path
(** {6 Misc } *)
--
cgit v1.2.3
From 8c7fa14c87dff113222469d138fee054b6c1ccb5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 10 Jul 2015 00:00:30 +0200
Subject: Native compiler: make non-fatal linking errors silent except in debug
mode.
---
kernel/nativelib.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 70920f1bbe..b2142b43c7 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -113,7 +113,7 @@ let call_linker ?(fatal=true) prefix f upds =
begin
let msg = "Cannot find native compiler file " ^ f in
if fatal then Errors.error msg
- else if !Flags.native_compiler then Pp.msg_warning (Pp.str msg)
+ else if !Flags.debug then Pp.msg_debug (Pp.str msg)
end
else
(try
@@ -123,7 +123,7 @@ let call_linker ?(fatal=true) prefix f upds =
let exn = Errors.push exn in
let msg = "Dynlink error, " ^ Dynlink.error_message e in
if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
- else Pp.msg_warning (Pp.str msg));
+ else if !Flags.debug then Pp.msg_debug (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
let link_library ~prefix ~dirname ~basename =
--
cgit v1.2.3
From 4ee6f939db643b2636caec18b32762910d419f32 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 10 Jul 2015 10:40:03 +0200
Subject: CHANGES: grammatical correction, suggested by Jason Gross on
Bugzilla.
---
CHANGES | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/CHANGES b/CHANGES
index 050d3e999f..202e27e377 100644
--- a/CHANGES
+++ b/CHANGES
@@ -161,7 +161,7 @@ Specification Language
break user notations using "$(", fixable by inserting a space or
rewriting the notation).
- Constructors in pattern-matching patterns now respect the same rules
- regarding implicit arguments than in applicative position. The old
+ regarding implicit arguments as in applicative position. The old
behavior can be recovered by the command "Set Asymmetric
Patterns". As a side effect, notations for constructors explicitly
mentioning non-implicit parameters can now be used in patterns.
--
cgit v1.2.3
From 591e7e484d544e958595a0fb784336ae050a9c74 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:47 +0200
Subject: Highlighting Universe in CoqIDE.
---
ide/coq.lang | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/ide/coq.lang b/ide/coq.lang
index c65432bdb7..89f93a705e 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -29,7 +29,7 @@
(\%{ident}\.)*\%{ident}
\.(\s|\z)
([-+*]+|{)(\s|\z)|}(\s*})*
- Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion
+ Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe
Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?
((Local|Global)\%{space})?
Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property
--
cgit v1.2.3
From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:59 +0200
Subject: Option -type-in-type: added support in checker and making it
contaminating in vo files (this was not done yet in 24d0027f0 and
090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
---
checker/check_stat.ml | 18 ++++++++++++------
checker/checker.ml | 14 +++++++++-----
checker/cic.mli | 7 +++++--
checker/environ.ml | 25 +++++++++++++++++--------
checker/environ.mli | 4 ++--
checker/indtypes.ml | 4 ++--
checker/reduction.ml | 7 ++++---
checker/safe_typing.ml | 22 +++++++++++++++-------
checker/typeops.ml | 2 +-
checker/values.ml | 6 ++++--
kernel/declarations.mli | 5 ++++-
kernel/environ.ml | 17 ++++++++---------
kernel/environ.mli | 7 ++-----
kernel/fast_typeops.ml | 6 ++----
kernel/indtypes.ml | 2 +-
kernel/pre_env.ml | 6 ++----
kernel/pre_env.mli | 3 +--
kernel/safe_typing.ml | 26 +++++++++++++++-----------
kernel/safe_typing.mli | 5 +----
kernel/typeops.ml | 6 ++----
library/global.ml | 1 -
library/global.mli | 1 -
pretyping/nativenorm.ml | 6 ++----
toplevel/command.ml | 3 +--
toplevel/coqtop.ml | 15 ++++++---------
toplevel/record.ml | 2 +-
26 files changed, 119 insertions(+), 101 deletions(-)
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b992..d041f1b7e1 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
let output_context = ref false
-let pr_engt = function
- Some ImpredicativeSet ->
- str "Theory: Set is impredicative"
- | None ->
- str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+ begin
+ match impr_set with
+ | ImpredicativeSet -> str "Theory: Set is impredicative"
+ | PredicativeSet -> str "Theory: Set is predicative"
+ end ++
+ begin
+ match type_in_type with
+ | StratifiedType -> str "Theory: Stratified type hierarchy"
+ | TypeInType -> str "Theory: Type is of type Type"
+ end
let cst_filter f csts =
Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
ppnl(hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
- str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_ax csts) ++
fnl())); pp_flush()
end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df51..d5d9b9e3b8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
let set_debug () = Flags.debug := true
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
- match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
\n -silent disable trace of constants being checked\
\n\
\n -impredicative-set set sort Set impredicative\
+\n -type-in-type collapse type hierarchy\
\n\
\n -h, --help print this list of options\
\n"
@@ -319,7 +321,9 @@ let parse_args argv =
let rec parse = function
| [] -> ()
| "-impredicative-set" :: rem ->
- set_engagement Cic.ImpredicativeSet; parse rem
+ set_impredicative_set (); parse rem
+ | "-type-in-type" :: rem ->
+ set_type_in_type (); parse rem
| "-coqlib" :: s :: rem ->
if not (exists_dir s) then
diff --git a/checker/cic.mli b/checker/cic.mli
index d75af76547..881d3ca797 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -165,7 +165,10 @@ type action
(** Engagements *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
@@ -407,7 +410,7 @@ type compiled_library = {
comp_name : compilation_unit_name;
comp_mod : module_body;
comp_deps : library_deps;
- comp_enga : engagement option;
+ comp_enga : engagement;
comp_natsymbs : nativecode_symb_array
}
diff --git a/checker/environ.ml b/checker/environ.ml
index c0f366000a..6dbc44d6b8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option
+ env_engagement : engagement
}
type env = {
@@ -33,19 +33,28 @@ let empty_env = {
env_rel_context = [];
env_stratification =
{ env_universes = Univ.initial_universes;
- env_engagement = None};
+ env_engagement = (PredicativeSet,StratifiedType)};
env_imports = MPmap.empty }
let engagement env = env.env_stratification.env_engagement
let universes env = env.env_stratification.env_universes
let rel_context env = env.env_rel_context
-let set_engagement c env =
- match env.env_stratification.env_engagement with
- | Some c' -> if c=c' then env else error "Incompatible engagement"
- | None ->
- { env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+ let expected_impr_set,expected_type_in_type =
+ env.env_stratification.env_engagement in
+ begin
+ match impr_set,expected_impr_set with
+ | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ begin
+ match type_in_type,expected_type_in_type with
+ | StratifiedType, TypeInType -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ { env with env_stratification =
+ { env.env_stratification with env_engagement = c } }
(* Digests *)
diff --git a/checker/environ.mli b/checker/environ.mli
index 22fe7d8f17..f3b2dd839a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option;
+ env_engagement : engagement;
}
type env = {
env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
val empty_env : env
(* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
val set_engagement : Cic.engagement -> env -> env
(* Digests *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e603..e1a6bc7c1d 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
(* Allowed eliminations *)
let check_predicativity env s small level =
- match s, engagement env with
+ match s, fst (engagement env) with
Type u, _ ->
(* let u' = fresh_local_univ () in *)
(* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
- | Prop Pos, Some ImpredicativeSet -> ()
+ | Prop Pos, ImpredicativeSet -> ()
| Prop Pos, _ ->
if not small then failwith "impredicative Set inductive type"
| Prop Null,_ -> ()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58f0f894ff..8ddeea2a20 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,7 +158,7 @@ type conv_pb =
| CONV
| CUMUL
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
| (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
| (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -167,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
CUMUL -> ()
| _ -> raise NotConvertible)
| (Type u1, Type u2) ->
- if not
+ if snd (engagement env) == StratifiedType
+ && not
(match pb with
| CONV -> Univ.check_eq univ u1 u2
| CUMUL -> Univ.check_leq univ u1 u2)
@@ -261,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(match a1, a2 with
| (Sort s1, Sort s2) ->
assert (is_empty_stack v1 && is_empty_stack v2);
- sort_cmp univ cv_pb s1 s2
+ sort_cmp (infos_env infos) univ cv_pb s1 s2
| (Meta n, Meta m) ->
if n=m
then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b65..dd94823135 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
let env = Modops.add_module mb env in
genv := add_digest env dp digest
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
- match engagement env, c with
- | Some ImpredicativeSet, Some ImpredicativeSet -> ()
- | _, None -> ()
- | _, Some ImpredicativeSet ->
- error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(* Libraries = Compiled modules *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b8..21819992a9 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- if engagement env = Some ImpredicativeSet then
+ if fst (engagement env) = ImpredicativeSet then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
else
diff --git a/checker/values.ml b/checker/values.ml
index 46b66adc4a..e82ba10327 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,7 +193,9 @@ let v_lazy_constr =
(** kernel/declarations *)
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -315,7 +317,7 @@ and v_modtype =
let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
- v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+ v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
(** Library objects *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c1c19a757c..561c66b422 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
declarations. This includes global constants/axioms, mutual
inductive definitions, modules and module types *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7e8..30b28177c9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
let engagement env = env.env_stratification.env_engagement
-let type_in_type env = env.env_stratification.env_type_in_type
-
let is_impredicative_set env =
- match engagement env with
- | Some ImpredicativeSet -> true
+ match fst (engagement env) with
+ | ImpredicativeSet -> true
+ | _ -> false
+
+let type_in_type env =
+ match snd (engagement env) with
+ | TypeInType -> true
| _ -> false
let universes env = env.env_stratification.env_universes
@@ -191,11 +194,7 @@ let check_constraints c env =
let set_engagement c env = (* Unsafe *)
{ env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
- { env with env_stratification =
- { env.env_stratification with env_type_in_type = true } }
+ { env.env_stratification with env_engagement = c } }
let push_constraints_to_env (_,univs) env =
add_constraints univs env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e699..4ad0327fc7 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
-val engagement : env -> engagement option
+val engagement : env -> engagement
val is_impredicative_set : env -> bool
-
-val type_in_type : env -> bool
+val type_in_type : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
-val set_type_in_type : env -> env
-
(** {6 Sets of referred section variables }
[global_vars_set env c] returns the list of [id]'s occurring either
directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c6..d22abff10c 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 31c0e83c84..9c79009dba 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign =
sign (Universe.type0m,env))
let is_impredicative env u =
- is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+ is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
(* Returns the list [x_1, ..., x_n] of levels contributing to template
polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7da..5f3f559a2c 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = initial_universes;
- env_engagement = None;
- env_type_in_type = false};
+ env_engagement = (PredicativeSet,StratifiedType) };
env_conv_oracle = Conv_oracle.empty;
retroknowledge = Retroknowledge.initial_retroknowledge;
indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b45e..0ce0bed235 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type lazy_val
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8473183ab..907ad2a1d4 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -184,16 +184,20 @@ let set_engagement c senv =
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
-let check_engagement env c =
- match Environ.engagement env, c with
- | None, Some ImpredicativeSet ->
- Errors.error "Needs option -impredicative-set."
- | _ -> ()
-
-let set_type_in_type senv =
- { senv with
- env = Environ.set_type_in_type senv.env;
- type_in_type = true }
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(** {6 Stm machinery } *)
@@ -734,7 +738,7 @@ type compiled_library = {
comp_name : DirPath.t;
comp_mod : module_body;
comp_deps : library_info array;
- comp_enga : engagement option;
+ comp_enga : engagement;
comp_natsymbs : Nativecode.symbols
}
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1e9cdbda0e..2b4324b96f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -99,12 +99,9 @@ val add_constraints :
(* (\** Generator of universes *\) *)
(* val next_universe : int safe_transformer *)
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
(** {6 Interactive module functions } *)
val start_module : Label.t -> module_path safe_transformer
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a4..fe82d85d5d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28f..0419799b67 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c)
let push_context c = globalize0 (Safe_typing.push_context c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
-let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 75a1ebee94..363bb57890 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
(** Variables, Local definitions, constants, inductive types *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b4b6b8aab8..2432b8d291 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (sup u1 type0_univ)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (sup type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 77339aef44..04238da2bd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -360,8 +360,7 @@ let make_conclusion_flexible evdref ty poly =
else ()
let is_impredicative env u =
- u = Prop Null ||
- (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+ u = Prop Null || (is_impredicative_set env && u = Prop Pos)
let interp_ind_arity env evdref ind =
let c = intern_gen IsType env ind.ind_arity in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5b330cd252..5540dc0ff1 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -112,14 +112,12 @@ let print_memory_stat () =
let _ = at_exit print_memory_stat
-let engagement = ref None
-let set_engagement c = engagement := Some c
+let impredicative_set = ref Declarations.PredicativeSet
+let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
+let type_in_type = ref Declarations.StratifiedType
+let set_type_in_type () = type_in_type := Declarations.TypeInType
let engage () =
- match !engagement with Some c -> Global.set_engagement c | None -> ()
-
-let type_in_type = ref false
-let set_type_in_type () = type_in_type := true
-let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+ Global.set_engagement (!impredicative_set,!type_in_type)
let set_batch_mode () = batch_mode := true
@@ -521,7 +519,7 @@ let parse_args arglist =
|"-filteropts" -> filter_opts := true
|"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
|"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
- |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+ |"-impredicative-set" -> set_impredicative_set ()
|"-indices-matter" -> Indtypes.enforce_indices_matter ()
|"-just-parsing" -> Vernac.just_parsing := true
|"-m"|"--memory" -> memory_stat := true
@@ -605,7 +603,6 @@ let init arglist =
Mltop.init_known_plugins ();
set_vm_opt ();
engage ();
- set_hierarchy ();
(* Be careful to set these variables after the inputstate *)
Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
Syntax_def.set_compat_notations (not !no_compat_ntn);
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb59f..15ad18d9cc 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,7 +135,7 @@ let typecheck_params_and_fields def id t ps nots fs =
let ctx, aritysort = Reduction.dest_arity env0 arity in
assert(List.is_empty ctx); (* Ensured by above analysis *)
if Sorts.is_prop aritysort ||
- (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+ (Sorts.is_set aritysort && is_impredicative_set env0) then
evars
else Evd.set_leq_sort env_ar evars (Type univ) aritysort
in
--
cgit v1.2.3
From 2aaced1d2486deb901ea0a5b134ef28273dda67f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:17:56 +0200
Subject: Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun.
Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a
coercion after resolving instances of type classes.
This fixes MathClasses (while preserving fix of part of from 4944b5e72
and fixes of HoTT_coq_014.v from df6e64fd28).
---
pretyping/classops.mli | 4 ++--
pretyping/coercion.ml | 18 ++++++++++--------
2 files changed, 12 insertions(+), 10 deletions(-)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index c421b4505b..e2bb2d1a00 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer
(** {6 Lookup functions for coercion paths } *)
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
-(** @raise Not_found when no such path exists *)
+(** @raise Not_found in the following functions when no path exists *)
+val lookup_path_between_class : cl_index * cl_index -> inheritance_path
val lookup_path_between : env -> evar_map -> types * types ->
types * types * inheritance_path
val lookup_path_to_fun_from : env -> evar_map -> types ->
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6765ca130b..e61e52c178 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -345,7 +345,7 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:false ~fail:false env evd
-(* appliquer le chemin de coercions p à hj *)
+(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
let j,t,evd =
@@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl =
with NoCoercion as e -> raise e
| e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
-let inh_app_fun env evd j =
+(* Try to coerce to a funclass; raise NoCoercion if not possible *)
+let inh_app_fun_core env evd j =
let t = whd_betadeltaiota env evd j.uj_type in
match kind_of_term t with
| Prod (_,_,_) -> (evd,j)
@@ -387,16 +388,17 @@ let inh_app_fun env evd j =
(!evdref, res)
with NoSubtacCoercion | NoCoercion ->
(evd,j)
- else (evd, j)
+ else raise NoCoercion
+(* Try to coerce to a funclass; returns [j] if no coercion is applicable *)
let inh_app_fun resolve_tc env evd j =
- try inh_app_fun env evd j
+ try inh_app_fun_core env evd j
with
- | Not_found when not resolve_tc
+ | NoCoercion when not resolve_tc
|| not !use_typeclasses_for_conversion -> (evd, j)
- | Not_found ->
- try inh_app_fun env (saturate_evd env evd) j
- with Not_found -> (evd, j)
+ | NoCoercion ->
+ try inh_app_fun_core env (saturate_evd env evd) j
+ with NoCoercion -> (evd, j)
let inh_tosort_force loc env evd j =
try
--
cgit v1.2.3
From 1391955c6635da17b4fb2d7c7b5cec799685e99d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 10:26:57 +0200
Subject: Unused variables reported by OCaml.
---
checker/inductive.ml | 4 ++--
kernel/inductive.ml | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index e3d8dd2060..00d3bc8e14 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -161,7 +161,7 @@ let remember_subst u subst =
(* Propagate the new levels in the signature *)
let rec make_subst env =
let rec make subst = function
- | (_,Some _,_ as t)::sign, exp, args ->
+ | (_,Some _,_)::sign, exp, args ->
make subst (sign, exp, args)
| d::sign, None::exp, args ->
let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +174,7 @@ let rec make_subst env =
(* a useless extra constraint *)
let s = sort_as_univ (snd (dest_arity env a)) in
make (cons_subst u s subst) (sign, exp, args)
- | (na,None,t as d)::sign, Some u::exp, [] ->
+ | (na,None,t)::sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
(* template, it is identity substitution otherwise (ie. when u is *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 00d14a25e2..cf4177c50b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -153,7 +153,7 @@ let remember_subst u subst =
(* Propagate the new levels in the signature *)
let rec make_subst env =
let rec make subst = function
- | (_,Some _,_ as t)::sign, exp, args ->
+ | (_,Some _,_)::sign, exp, args ->
make subst (sign, exp, args)
| d::sign, None::exp, args ->
let args = match args with _::args -> args | [] -> [] in
@@ -166,7 +166,7 @@ let rec make_subst env =
(* a useless extra constraint *)
let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
make (cons_subst u s subst) (sign, exp, args)
- | (na,None,t as d)::sign, Some u::exp, [] ->
+ | (na,None,t)::sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
(* substitution (when [u] is distinct from all other universes in the *)
(* template, it is identity substitution otherwise (ie. when u is *)
--
cgit v1.2.3
From 31ce6ad3ca351b4742f66ed059356191ae96a3ac Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 19:16:05 +0200
Subject: Rewording about how to upgrade on failing calls to constructor.
---
CHANGES | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/CHANGES b/CHANGES
index 202e27e377..733bcc7cf5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -188,10 +188,12 @@ Tactics
during the execution of c, it can backtrack and try b instead of a.
* New tactical (once a) removes all the backtracking points from a
(i.e. it selects the first success of a).
- * Tactic "constructor" is now fully backtracking, thus deprecating
- the need of the undocumented "constructor " syntax which is
- now equivalent to "[> once (constructor; tac) ..]". (potential
- source of rare incompatibilities).
+ * Tactic "constructor" is now fully backtracking. In case of
+ incompatibilities (e.g. combinatoric explosion), the former
+ behavior of "constructor" can be retrieved by using instead
+ "[> once constructor ..]". Thanks to backtracking, undocumented
+ "constructor " syntax is now equivalent to
+ "[> once (constructor; tac) ..]".
* New "multimatch" variant of "match" tactic which backtracks to
new branches in case of a later failure. The "match" tactic is
equivalent to "once multimatch".
--
cgit v1.2.3
From 7351bf1c179c4feebf4d93437625ea358dc59420 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 11 Jul 2015 23:49:31 +0200
Subject: CoqIDE: recenter on backtrack (Close: #4277)
---
ide/coqOps.ml | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2387d65c30..c6d3149475 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -669,7 +669,10 @@ object(self)
push_info "Coq is undoing" in
let conclusion () =
pop_info ();
- if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+ if move_insert then begin
+ buffer#place_cursor ~where:self#get_start_of_input;
+ script#recenter_insert;
+ end;
let start = self#get_start_of_input in
let stop = self#get_end_of_input in
Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
--
cgit v1.2.3
From b3f8288b2243efe59d3358ad4001dd78d62308b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jul 2015 23:59:32 +0200
Subject: Updating checksum in checker (9c732a5cc continued).
Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
---
Makefile.build | 6 +++---
checker/values.ml | 2 +-
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/Makefile.build b/Makefile.build
index 16c5730865..404f176ab4 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -282,11 +282,11 @@ $(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ)))
# For the checker, different flags may be used
-checker/check.cma: | checker/check.mllib.d
+checker/check.cma: | md5chk checker/check.mllib.d
$(SHOW)'OCAMLC -a -o $@'
$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^
-checker/check.cmxa: | checker/check.mllib.d
+checker/check.cmxa: | md5chk checker/check.mllib.d
$(SHOW)'OCAMLOPT -a -o $@'
$(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^
@@ -479,7 +479,7 @@ md5chk:
VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
-validate: $(CHICKEN) md5chk | $(ALLVO)
+validate: $(CHICKEN) | $(ALLVO)
$(SHOW)'COQCHK '
$(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
diff --git a/checker/values.ml b/checker/values.ml
index e82ba10327..45220bd051 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
+MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
*)
--
cgit v1.2.3
From 44f3c1b1071506bcd98dec4e10675624c0142c21 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 14 Jul 2015 11:55:04 +0200
Subject: STM: fix a "exn with no safe id attached" error on a failing query
It showed up at the CoqCS.
---
stm/stm.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/stm/stm.ml b/stm/stm.ml
index 373fd0ba39..8af1aaafdc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2117,7 +2117,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
iraise (State.exn_on report_id e)); `Ok
| VtQuery (false,(report_id,route)), VtNow ->
(try vernac_interp report_id ~route x
- with e when Errors.noncritical e ->
+ with e ->
let e = Errors.push e in
iraise (State.exn_on report_id e)); `Ok
| VtQuery (true,(report_id,_)), w ->
--
cgit v1.2.3
From c57c7edbe517851c7309112f6eb5d8297f03e000 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Jul 2015 17:36:58 +0200
Subject: Univs/Inductive: fix typechecking of cases
I was trying to be a bit too clever with not substituting the universe
instance everywhere: the constructor type/inductive arity has to be
instantiated before instantiate_params runs, which became true only
for constructor types since my last commit.
---
checker/inductive.ml | 2 +-
kernel/inductive.ml | 8 ++++----
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 00d3bc8e14..21b80f323e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -103,7 +103,7 @@ let instantiate_params full t u args sign =
let full_inductive_instantiate mib u params sign =
let dummy = Prop Null in
- let t = mkArity (sign,dummy) in
+ let t = mkArity (subst_instance_context u sign,dummy) in
fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cf4177c50b..87c139f48d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -93,7 +93,7 @@ let instantiate_params full t u args sign =
let full_inductive_instantiate mib u params sign =
let dummy = prop_sort in
- let t = mkArity (sign,dummy) in
+ let t = mkArity (Vars.subst_instance_context u sign,dummy) in
fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
@@ -344,13 +344,13 @@ let is_correct_arity env c pj ind specif params =
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
let env' = push_rel (na1,None,a1) env in
let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
- | Sort s -> family_of_sort s
- | _ -> raise (LocalArity None) in
+ | Sort s -> family_of_sort s
+ | _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
let _ =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
- check_allowed_sort ksort specif
+ check_allowed_sort ksort specif
| _, (_,Some _,_ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar'
| _ ->
--
cgit v1.2.3
From 93579407f5795c117d6c6f1399396b690f80d723 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 09:32:36 +0200
Subject: Fixing anomaly #3743 while printing an error message involving evar
constraints.
Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.
The error message for "Unable to satisfy the following constraints" is
still to be improved though.
---
library/nameops.ml | 5 +++++
library/nameops.mli | 2 +-
pretyping/evarconv.ml | 5 +++--
3 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/library/nameops.ml b/library/nameops.ml
index 02b085a7ac..3a23ab97df 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,6 +136,11 @@ let name_fold_map f e = function
| Name id -> let (e,id) = f e id in (e,Name id)
| Anonymous -> e,Anonymous
+let name_max na1 na2 =
+ match na1 with
+ | Name _ -> na1
+ | Anonymous -> na2
+
let pr_lab l = str (Label.to_string l)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 23432ae2fa..de1f99fe0f 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit
val name_cons : Name.t -> Id.t list -> Id.t list
val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-
+val name_max : Name.t -> Name.t -> Name.t
val pr_lab : Label.t -> Pp.std_ppcmds
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 97b1b16455..64d1345c1f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -726,12 +726,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
UnifFailure (evd,UnifUnivInconsistency p)
| e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
- | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
+ | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
ise_and evd
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
- evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)]
+ let na = Nameops.name_max n1 n2 in
+ evar_conv_x ts (push_rel (na,None,c) env) i pbty c'1 c'2)]
| Rel x1, Rel x2 ->
if Int.equal x1 x2 then
--
cgit v1.2.3
From 3bcc96d5ab6571a7810b68c340af7aa195ef76f4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 09:44:54 +0200
Subject: Continuing 93579407, spotting other potential sources of anomaly
because of the name of a bound variable lost when unifying under a binder in
evarconv.
---
pretyping/evarconv.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 64d1345c1f..bb07bf0563 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -552,13 +552,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
| MaybeFlexible v1, MaybeFlexible v2 -> begin
match kind_of_term term1, kind_of_term term2 with
- | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
+ | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) ->
let f1 i =
ise_and i
[(fun i -> evar_conv_x ts env i CONV b1 b2);
(fun i ->
let b = nf_evar i b1 in
let t = nf_evar i t1 in
+ let na = Nameops.name_max na1 na2 in
evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
@@ -666,13 +667,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
end
| Rigid, Rigid when isLambda term1 && isLambda term2 ->
- let (na,c1,c'1) = destLambda term1 in
- let (_,c2,c'2) = destLambda term2 in
+ let (na1,c1,c'1) = destLambda term1 in
+ let (na2,c2,c'2) = destLambda term2 in
assert app_empty;
ise_and evd
[(fun i -> evar_conv_x ts env i CONV c1 c2);
(fun i ->
let c = nf_evar i c1 in
+ let na = Nameops.name_max na1 na2 in
evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
--
cgit v1.2.3
From ebb53e68cdc935a85c4da10852be4f7f3b492ee2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jul 2015 16:40:25 +0200
Subject: Modules: fix bug #4294
We were throwing away constraints from 'with Definition' in module
type ascriptions.
---
kernel/mod_typing.ml | 4 +++-
kernel/univ.ml | 2 +-
2 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26dd45f5f3..4f20e5f62a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -307,7 +307,9 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
- mod_constraints = cst +++ cst' }
+ (** cst from module body typing, cst' from subtyping,
+ and constraints from module type. *)
+ mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints }
let translate_module env mp inl = function
|MType (params,ty) ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1d82be63b9..336cdb653e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -577,7 +577,7 @@ struct
let is_type0m x = equal type0m x
let is_type0 x = equal type0 x
- (* Returns the formal universe that lies juste above the universe variable u.
+ (* Returns the formal universe that lies just above the universe variable u.
Used to type the sort u. *)
let super l =
if is_small l then type1
--
cgit v1.2.3
From e4aa8f13680a81ec7e2ebe1281b20d5791d13440 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 19:21:35 +0200
Subject: Fix universe instantiation with canonical structures.
Patch by Matthieu Sozeau.
Fixes #3819: "Error: Unsatisfied constraints" due to canonical
structure inference
---
pretyping/recordops.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6dc0d1f3c2..7fde7b7ac4 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -190,7 +190,7 @@ let cs_pattern_of_constr t =
(* Intended to always succeed *)
let compute_canonical_projections (con,ind) =
let env = Global.env () in
- let ctx = Environ.constant_context env con in
+ let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in
let u = Univ.UContext.instance ctx in
let v = (mkConstU (con,u)) in
let ctx = Univ.ContextSet.of_context ctx in
--
cgit v1.2.3
From 6a15394c542e5f16bce9b75fc033397c454f47e9 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 19:24:23 +0200
Subject: Test file for #3819.
---
test-suite/bugs/closed/3819.v | 9 +++++++++
1 file changed, 9 insertions(+)
create mode 100644 test-suite/bugs/closed/3819.v
diff --git a/test-suite/bugs/closed/3819.v b/test-suite/bugs/closed/3819.v
new file mode 100644
index 0000000000..355d23a58b
--- /dev/null
+++ b/test-suite/bugs/closed/3819.v
@@ -0,0 +1,9 @@
+Record Op := { t : Type ; op : t -> t }.
+
+Canonical Structure OpType : Op := Build_Op Type (fun X => X).
+
+Lemma test1 (X:Type) : eq (op OpType X) X.
+Proof eq_refl.
+
+Definition test2 (A:Type) : eq (op _ A) A.
+Proof eq_refl.
\ No newline at end of file
--
cgit v1.2.3
From 8591217a89f0b71e8175752dc55c42a5b89fccec Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 20:21:58 +0200
Subject: Fixing bug #4240 (closure_of_filter was not ensuring refinement of
former filter after 48509b61 and 3cd718c, because filtered let-ins were not
any longer preserved).
---
pretyping/evarsolve.ml | 7 +++++++
test-suite/bugs/closed/4240.v | 12 ++++++++++++
2 files changed, 19 insertions(+)
create mode 100644 test-suite/bugs/closed/4240.v
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index bfd19c6c7d..b2cf21b818 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -157,6 +157,7 @@ let restrict_evar_key evd evk filter candidates =
end
(* Restrict an applied evar and returns its restriction in the same context *)
+(* (the filter is assumed to be at least stronger than the original one) *)
let restrict_applied_evar evd (evk,argsv) filter candidates =
let evd,newevk = restrict_evar_key evd evk filter candidates in
let newargsv = match filter with
@@ -885,6 +886,9 @@ let filter_candidates evd evk filter candidates_update =
else
UpdateWith l'
+(* Given a filter refinement for the evar [evk], restrict it so that
+ dependencies are preserved *)
+
let closure_of_filter evd evk = function
| None -> None
| Some filter ->
@@ -892,8 +896,11 @@ let closure_of_filter evd evk = function
let vars = collect_vars (Evarutil.nf_evar evd (evar_concl evi)) in
let test b (id,c,_) = b || Idset.mem id vars || match c with None -> false | Some c -> not (isRel c || isVar c) in
let newfilter = Filter.map_along test filter (evar_context evi) in
+ (* Now ensure that restriction is at least what is was originally *)
+ let newfilter = Option.cata (Filter.map_along (&&) newfilter) newfilter (Filter.repr (evar_filter evi)) in
if Filter.equal newfilter (evar_filter evi) then None else Some newfilter
+(* The filter is assumed to be at least stronger than the original one *)
let restrict_hyps evd evk filter candidates =
(* What to do with dependencies?
Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
diff --git a/test-suite/bugs/closed/4240.v b/test-suite/bugs/closed/4240.v
new file mode 100644
index 0000000000..083c59fe68
--- /dev/null
+++ b/test-suite/bugs/closed/4240.v
@@ -0,0 +1,12 @@
+(* Check that closure of filter did not restrict the former evar filter *)
+
+Lemma foo (new : nat) : False.
+evar (H1: nat).
+set (H3 := 0).
+assert (H3' := id H3).
+evar (H5: nat).
+clear H3.
+assert (H5 = new).
+unfold H5.
+unfold H1.
+exact (eq_refl new).
--
cgit v1.2.3
From 916a8dc2c6b1dd8400d5c44b5d9c7fc793cc0e97 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 16 Jul 2015 21:40:42 +0200
Subject: Remove old test file for #3819 (now fixed).
---
test-suite/bugs/opened/3819.v | 11 -----------
1 file changed, 11 deletions(-)
delete mode 100644 test-suite/bugs/opened/3819.v
diff --git a/test-suite/bugs/opened/3819.v b/test-suite/bugs/opened/3819.v
deleted file mode 100644
index 7105a65877..0000000000
--- a/test-suite/bugs/opened/3819.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Set Universe Polymorphism.
-
-Record Op := { t : Type ; op : t -> t }.
-
-Canonical Structure OpType : Op := Build_Op Type (fun X => X).
-
-Lemma test1 (X:Type) : eq (op OpType X) X.
-Proof eq_refl.
-
-Lemma test2 (A:Type) : eq (op _ A) A.
-Fail Proof eq_refl.
--
cgit v1.2.3
From 0b3a335219e161dc04f6734e9ee4f7c08cde6cd5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 21:34:08 +0200
Subject: Fixing #4177 (find_projectable was liable to ask to instantiate an
evar twice).
This is a bug in a pretty old code, showing also in 8.3 and 8.4.
---
pretyping/evarsolve.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b2cf21b818..ac1692f451 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -694,7 +694,8 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
(* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
(* projectable on [y] *)
if with_evars then
- let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
+ let f (c,_,id) = isEvar c && is_undefined sigma (fst (destEvar c)) in
+ let idcl' = List.filter f idcl in
match idcl' with
| [c,_,id] ->
begin
--
cgit v1.2.3
From e0d36d4afd7f38eb6816b92d03ecc2d2f7dc8d3f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 22:08:31 +0200
Subject: Slight improvement in naming anonymous variables in error messages:
using closer naming strategies for naming variables in
make_all_name_different and when contracting trivial letins.
Not sure what the best policy is. Maybe the contraction process should
not invent names at al and let make_all_name_different do the job.
Maybe pretyping should name all rels which it pushes to environment
(with cases.ml paying attention to avoid clash).
The problem shows for instance with a PretypeError (... env, ... ,
ActualTypeNotCoercible (NotClean (... env ...)) message with two
copies of env which we don't if they are the same but which have to
share same names for similar rendering of the rels!
This was revealed e.g. by the error message of #4177.
---
pretyping/namegen.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 5aca11ae61..a88c2e20e3 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -278,6 +278,7 @@ let make_all_name_different env =
let avoid = ref (ids_of_named_context (named_context env)) in
process_rel_context
(fun (na,c,t) newenv ->
+ let na = named_hd newenv t na in
let id = next_name_away na !avoid in
avoid := id::!avoid;
push_rel (Name id,c,t) newenv)
--
cgit v1.2.3
From fdd6a17b272995237c9f95fc465bb1ff6871bedc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Jul 2015 22:53:10 +0200
Subject: Refining 71def2f8 on too strong occur-check limiting evar-evar
unification in tactics.
The relaxing of occur-check was ok but was leading trivial problems of
the form ?X[?Meta] = ?X[?Meta] to enter a complex Evar-ization into
?X[?Meta] = ?X[?Y], ?Meta:=?Y which consider_remaining_unif_problems
was not any more able to deal with.
Doing quick: treat the trivial cases ?X[args] = ?X[args] in an ad hoc way,
so that it behaves as if the occur-check had not been restricted.
---
pretyping/unification.ml | 6 +++++-
test-suite/bugs/closed/4205.v | 8 ++++++++
2 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 test-suite/bugs/closed/4205.v
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b5fe5d0b6d..24e06007e9 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -676,7 +676,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| Evar (evk,_ as ev), Evar (evk',_)
when not (Evar.Set.mem evk flags.frozen_evars)
&& Evar.equal evk evk' ->
- sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ let sigma',b = constr_cmp cv_pb sigma flags cM cN in
+ if b then
+ sigma',metasubst,evarsubst
+ else
+ sigma,metasubst,((curenv,ev,cN)::evarsubst)
| Evar (evk,_ as ev), _
when not (Evar.Set.mem evk flags.frozen_evars)
&& not (occur_evar evk cN) ->
diff --git a/test-suite/bugs/closed/4205.v b/test-suite/bugs/closed/4205.v
new file mode 100644
index 0000000000..c40dfcc1f3
--- /dev/null
+++ b/test-suite/bugs/closed/4205.v
@@ -0,0 +1,8 @@
+(* Testing a regression from 8.5beta1 to 8.5beta2 in evar-evar tactic unification problems *)
+
+
+Inductive test : nat -> nat -> nat -> nat -> Prop :=
+ | test1 : forall m n, test m n m n.
+
+Goal test 1 2 3 4.
+erewrite f_equal2 with (f := fun k l => test _ _ k l).
--
cgit v1.2.3