aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--CHANGES3
-rw-r--r--checker/checker.ml2
-rw-r--r--checker/indtypes.ml17
-rw-r--r--checker/reduction.ml17
-rw-r--r--checker/univ.ml34
-rw-r--r--checker/univ.mli15
-rw-r--r--checker/values.ml4
-rw-r--r--dev/ci/ci-common.sh2
-rwxr-xr-xdev/lint-repository.sh2
-rwxr-xr-xdev/tools/backport-pr.sh9
-rw-r--r--doc/refman/RefMan-oth.tex6
-rw-r--r--doc/refman/Universes.tex39
-rw-r--r--engine/logic_monad.ml1
-rw-r--r--engine/logic_monad.mli1
-rw-r--r--engine/universes.ml11
-rw-r--r--engine/universes.mli6
-rw-r--r--interp/constrexpr_ops.ml8
-rw-r--r--interp/constrextern.ml3
-rw-r--r--interp/constrintern.ml24
-rw-r--r--interp/declare.ml7
-rw-r--r--interp/discharge.ml2
-rw-r--r--interp/notation_ops.ml19
-rw-r--r--intf/constrexpr.ml1
-rw-r--r--intf/glob_term.ml1
-rw-r--r--intf/notation_term.ml1
-rw-r--r--intf/pattern.ml2
-rw-r--r--kernel/indtypes.ml22
-rw-r--r--kernel/nativelib.ml5
-rw-r--r--kernel/reduction.ml260
-rw-r--r--kernel/reduction.mli22
-rw-r--r--kernel/term.ml6
-rw-r--r--kernel/term.mli12
-rw-r--r--kernel/univ.ml136
-rw-r--r--kernel/univ.mli58
-rw-r--r--lib/coqProject_file.ml42
-rw-r--r--lib/feedback.mli5
-rw-r--r--library/globnames.ml2
-rw-r--r--plugins/funind/glob_term_to_relation.ml4
-rw-r--r--plugins/funind/glob_termops.ml6
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--pretyping/detyping.ml14
-rw-r--r--pretyping/evarconv.ml14
-rw-r--r--pretyping/glob_ops.ml10
-rw-r--r--pretyping/inductiveops.ml146
-rw-r--r--pretyping/inductiveops.mli9
-rw-r--r--pretyping/inferCumulativity.ml224
-rw-r--r--pretyping/inferCumulativity.mli10
-rw-r--r--pretyping/patternops.ml6
-rw-r--r--pretyping/pretyping.ml5
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/recordops.ml27
-rw-r--r--pretyping/reductionops.ml80
-rw-r--r--pretyping/typing.mli1
-rw-r--r--pretyping/vnorm.ml3
-rw-r--r--printing/ppconstr.ml3
-rw-r--r--printing/prettyp.ml11
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printer.mli3
-rw-r--r--printing/printmod.ml13
-rw-r--r--stm/stm.ml28
-rw-r--r--test-suite/bugs/closed/5726.v34
-rw-r--r--test-suite/output/ErrorInCanonicalStructures.out5
-rw-r--r--test-suite/output/ErrorInCanonicalStructures.v3
-rw-r--r--test-suite/output/ErrorInCanonicalStructures2.out5
-rw-r--r--test-suite/output/ErrorInCanonicalStructures2.v3
-rw-r--r--test-suite/output/Inductive.out4
-rw-r--r--test-suite/output/Inductive.v4
-rw-r--r--test-suite/output/UnivBinders.out2
-rw-r--r--test-suite/success/cumulativity.v26
-rw-r--r--theories/Lists/List.v27
-rw-r--r--tools/CoqMakefile.in3
-rw-r--r--tools/coqdep.ml2
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--vernac/comInductive.ml4
-rw-r--r--vernac/explainErr.ml1
-rw-r--r--vernac/record.ml15
-rw-r--r--vernac/vernacentries.ml4
77 files changed, 926 insertions, 611 deletions
diff --git a/CHANGES b/CHANGES
index cb4b966b0..1084847d5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,9 @@ Universes
module and library boundaries. Global universe names introduced in an
inductive / constant / Let declaration get qualified with the name of
the declaration.
+- Universe cumulativity for inductive types is now specified as a
+ variance for each polymorphic universe. See the reference manual for
+ more information.
Checker
diff --git a/checker/checker.ml b/checker/checker.ml
index b8b4d5dc2..e8eff889c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -18,7 +18,7 @@ let () = at_exit flush_all
let chk_pp = Pp.pp_with Format.std_formatter
let fatal_error info anomaly =
- flush_all (); Feedback.msg_error info; flush_all ();
+ flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all ();
exit (if anomaly then 129 else 1)
let coq_root = Id.of_string "Coq"
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 4de597766..1807ae0ec 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -564,14 +564,23 @@ let check_subtyping cumi paramsctxt env inds =
We must produce the substitution σ : [ Var(i) -> Var (i + n) | 0 <= i < n]
and push the constraints [ Var(n) ... Var(2n - 1) |- cst{σ} ], together
with the cumulativity constraints [ cumul_cst ]. *)
- let len = AUContext.size (ACumulativityInfo.univ_context cumi) in
- let inst = Instance.of_array (Array.init len (fun i -> Level.var (i + len))) in
+ let uctx = ACumulativityInfo.univ_context cumi in
+ let len = AUContext.size uctx in
+ let inst = Instance.of_array @@ Array.init len (fun i -> Level.var (i + len)) in
+
let other_context = ACumulativityInfo.univ_context cumi in
let uctx_other = UContext.make (inst, AUContext.instantiate inst other_context) in
- let cumul_context = AUContext.repr (ACumulativityInfo.subtyp_context cumi) in
- let cumul_cst = UContext.constraints cumul_context in
+ let cumul_cst =
+ Array.fold_left_i (fun i csts var ->
+ match var with
+ | Variance.Irrelevant -> csts
+ | Variance.Covariant -> Constraint.add (Level.var i,Le,Level.var (i+len)) csts
+ | Variance.Invariant -> Constraint.add (Level.var i,Eq,Level.var (i+len)) csts)
+ Constraint.empty (ACumulativityInfo.variance cumi)
+ in
let env = Environ.push_context uctx_other env in
let env = Environ.add_constraints cumul_cst env in
+
(* process individual inductive types: *)
Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
match arity with
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 29bb8901e..2297c90b3 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,24 +158,17 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
let convert_inductive_instances cv_pb cumi u u' univs =
let len_instance =
Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
- let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
if not ((len_instance = Univ.Instance.length u) &&
(len_instance = Univ.Instance.length u')) then
anomaly (Pp.str "Invalid inductive subtyping encountered!")
else
- let comp_cst =
- let comp_subst = (Univ.Instance.append u u') in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
+ let variance = Univ.ACumulativityInfo.variance cumi in
let comp_cst =
match cv_pb with
- CONV ->
- let comp_cst' =
- let comp_subst = (Univ.Instance.append u' u) in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
- Univ.Constraint.union comp_cst comp_cst'
- | CUMUL -> comp_cst
+ | CONV ->
+ Univ.Variance.eq_constraints variance u u' Univ.Constraint.empty
+ | CUMUL ->
+ Univ.Variance.leq_constraints variance u u' Univ.Constraint.empty
in
if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
diff --git a/checker/univ.ml b/checker/univ.ml
index 7d01657df..46b3ce680 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1003,12 +1003,42 @@ end
type abstract_universe_context = AUContext.t
+module Variance =
+struct
+ (** A universe position in the instance given to a cumulative
+ inductive can be the following. Note there is no Contravariant
+ case because [forall x : A, B <= forall x : A', B'] requires [A =
+ A'] as opposed to [A' <= A]. *)
+ type t = Irrelevant | Covariant | Invariant
+
+ let leq_constraint csts variance u u' =
+ match variance with
+ | Irrelevant -> csts
+ | Covariant -> Constraint.add (u, Le, u') csts
+ | Invariant -> Constraint.add (u, Eq, u') csts
+
+ let eq_constraint csts variance u u' =
+ match variance with
+ | Irrelevant -> csts
+ | Covariant | Invariant -> Constraint.add (u, Eq, u') csts
+
+ let leq_constraints variance u u' csts =
+ let len = Array.length u in
+ assert (len = Array.length u' && len = Array.length variance);
+ Array.fold_left3 leq_constraint csts variance u u'
+
+ let eq_constraints variance u u' csts =
+ let len = Array.length u in
+ assert (len = Array.length u' && len = Array.length variance);
+ Array.fold_left3 eq_constraint csts variance u u'
+end
+
module CumulativityInfo =
struct
- type t = universe_context * universe_context
+ type t = universe_context * Variance.t array
let univ_context (univcst, subtypcst) = univcst
- let subtyp_context (univcst, subtypcst) = subtypcst
+ let variance (univs, variance) = variance
end
diff --git a/checker/univ.mli b/checker/univ.mli
index 21c94d952..8c0685e0b 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -218,12 +218,25 @@ end
type abstract_universe_context = AUContext.t
+module Variance :
+sig
+ (** A universe position in the instance given to a cumulative
+ inductive can be the following. Note there is no Contravariant
+ case because [forall x : A, B <= forall x : A', B'] requires [A =
+ A'] as opposed to [A' <= A]. *)
+ type t = Irrelevant | Covariant | Invariant
+
+ val leq_constraints : t array -> Instance.t constraint_function
+ val eq_constraints : t array -> Instance.t constraint_function
+end
+
+
module ACumulativityInfo :
sig
type t
val univ_context : t -> abstract_universe_context
- val subtyp_context : t -> abstract_universe_context
+ val variance : t -> Variance.t array
end
diff --git a/checker/values.ml b/checker/values.ml
index 313067cb6..55e1cdb6f 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -110,10 +110,12 @@ let v_cstrs =
(v_tuple "univ_constraint"
[|v_level;v_enum "order_request" 3;v_level|]))
+let v_variance = v_enum "variance" 3
+
let v_instance = Annot ("instance", Array v_level)
let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
let v_abs_context = v_context (* only for clarity *)
-let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; v_context|]
+let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
(** kernel/term *)
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 05fa33e97..d7a356930 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -19,6 +19,8 @@ else
then
export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
export CI_BRANCH="$CIRCLE_BRANCH"
+ else # assume local
+ export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
fi
export COQBIN="$PWD/bin"
fi
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index e3ec51aeb..ee9c8777a 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -14,7 +14,7 @@ then
# skip PRs from before the linter existed
if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
then
- 2>&1 echo "Linting skipped: pull request older than the linter."
+ 1>&2 echo "Linting skipped: pull request older than the linter."
exit 0
fi
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index d7acf01f1..e4359f703 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -50,6 +50,15 @@ else
fi
+if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+ echo
+ read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
+ echo
+ if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+ exit 1
+ fi
+fi
+
if [[ "${OPTION}" == "--stop-before-merging" ]]; then
exit 0
fi
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 65926c69c..1cd23c929 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -917,9 +917,9 @@ This command displays whether some default timeout has be set or not.
For debugging {\Coq} scripts, sometimes it is desirable to know
whether a command or a tactic fails. If the given command or tactic
fails, the {\tt Fail} statement succeeds, without changing the proof
-state, and {\Coq} prints a message confirming the failure. If the
-command or tactic succeeds, the statement is an error, and {\Coq}
-prints a message indicating that the failure did not occur.
+state, and in interactive mode, {\Coq} prints a message confirming the failure.
+If the command or tactic succeeds, the statement is an error, and
+{\Coq} prints a message indicating that the failure did not occur.
\section{Controlling display}
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index a1a6a4391..6c84a1818 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -68,6 +68,13 @@ is only valid as long as \texttt{Top.4} is strictly smaller than
monomorphic (not universe polymorphic), so the two universes
(in this case \texttt{Top.3} and \texttt{Top.4}) are actually global levels.
+When printing \texttt{pidentity}, we can see the universes it binds in
+the annotation \texttt{@\{Top.2\}}. Additionally, when \texttt{Set
+ Printing Universes} is on we print the ``universe context'' of
+\texttt{pidentity} consisting of the bound universes and the
+constraints they must verify (for \texttt{pidentity} there are no
+constraints).
+
Inductive types can also be declared universes polymorphic on universes
appearing in their parameters or fields. A typical example is given by
monoids:
@@ -138,7 +145,7 @@ producing global universe constraints, one can use the
\optindex{Polymorphic Inductive Cumulativity}
Polymorphic inductive types, coinductive types, variants and records can be
-declared cumulative using the \texttt{Cumulative}. Alternatively,
+declared cumulative using the \texttt{Cumulative} prefix. Alternatively,
there is an option \texttt{Set Polymorphic Inductive Cumulativity} which when set,
makes all subsequent \emph{polymorphic} inductive definitions cumulative. When set,
inductive types and the like can be enforced to be
@@ -151,15 +158,22 @@ Polymorphic Cumulative Inductive list {A : Type} :=
\begin{coq_example}
Print list.
\end{coq_example}
-When printing \texttt{list}, the part of the output of the form
-\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff }
-indicates the universe constraints in order to have the subtyping
-$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$
-(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$.
-In the case of \texttt{list} there is no constraint!
-This also means that any two instances of \texttt{list} are convertible:
-$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and
-furthermore their corresponding (when fully applied to convertible arguments) constructors.
+When printing \texttt{list}, the universe context indicates the
+subtyping constraints by prefixing the level names with symbols.
+
+Because inductive subtypings are only produced by comparing inductives
+to themselves with universes changed, they amount to variance
+information: each universe is either invariant, covariant or
+irrelevant (there are no contravariant subtypings in Coq),
+respectively represented by the symbols \texttt{=}, \texttt{+} and
+\texttt{*}.
+
+Here we see that \texttt{list} binds an irrelevant universe, so any
+two instances of \texttt{list} are convertible:
+$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever
+$\WTEGCONV{A}{B}$ and furthermore their corresponding (when fully
+applied to convertible arguments) constructors.
+
See Chapter~\ref{Cic} for more details on convertibility and subtyping.
The following is an example of a record with non-trivial subtyping relation:
\begin{coq_example*}
@@ -168,8 +182,9 @@ Polymorphic Cumulative Record packType := {pk : Type}.
\begin{coq_example}
Print packType.
\end{coq_example}
-Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are
-convertible if and only if \texttt{i $=$ j}.
+\texttt{packType} binds a covariant universe, i.e.
+$\WTEGCONV{\mathtt{packType@\{i\}}}{\mathtt{packType@\{j\}}}$ whenever
+\texttt{i $\leq$ j}.
Cumulative inductive types, coninductive types, variants and records
only make sense when they are universe polymorphic. Therefore, an
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 9dc5d473b..3674bb943 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -107,7 +107,6 @@ struct
let print_debug s = make (fun _ -> Feedback.msg_info s)
let print_info s = make (fun _ -> Feedback.msg_info s)
let print_warning s = make (fun _ -> Feedback.msg_warning s)
- let print_error s = make (fun _ -> Feedback.msg_error s)
let print_notice s = make (fun _ -> Feedback.msg_notice s)
let run = fun x ->
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 8c8f9fe93..50b4abd8b 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -61,7 +61,6 @@ module NonLogical : sig
val print_warning : Pp.t -> unit t
val print_notice : Pp.t -> unit t
val print_info : Pp.t -> unit t
- val print_error : Pp.t -> unit t
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
diff --git a/engine/universes.ml b/engine/universes.ml
index eaddf98a8..3a00f0fd1 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -1103,14 +1103,3 @@ let solve_constraints_system levels level_bounds level_min =
done;
done;
v
-
-
-(** Operations for universe_info_ind *)
-
-(** Given a universe context representing constraints of an inductive
- this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-let univ_inf_ind_from_universe_context univcst =
- let freshunivs = Instance.of_array
- (Array.map (fun _ -> new_univ_level ())
- (Instance.to_array (UContext.instance univcst)))
- in CumulativityInfo.from_universe_context univcst freshunivs
diff --git a/engine/universes.mli b/engine/universes.mli
index 130dcf8bb..cb6e2ba1b 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -221,9 +221,3 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.t
val solve_constraints_system : Universe.t option array -> Universe.t array -> Universe.t array ->
Universe.t array
-
-(** Operations for universe_info_ind *)
-
-(** Given a universe context representing constraints of an inductive
- this function produces a UInfoInd.t that with the trivial subtyping relation. *)
-val univ_inf_ind_from_universe_context : UContext.t -> CumulativityInfo.t
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7cc8de85d..da04d8786 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -173,10 +173,12 @@ let rec constr_expr_eq e1 e2 =
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
+ | CProj(p1,c1), CProj(p2,c2) ->
+ eq_reference p1 p2 && constr_expr_eq c1 c2
| (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
| CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
| CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
- | CGeneralization _ | CDelimiters _), _ -> false
+ | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
@@ -365,6 +367,8 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+ | CProj (_,c) ->
+ f n acc c
)
let free_vars_of_constr_expr c =
@@ -446,6 +450,8 @@ let map_constr_expr_with_binders g f e = CAst.map (function
let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
+ | CProj (p,c) ->
+ CProj (p, f e c)
)
(* Used in constrintern *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 1330b3741..4f7d537d3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -908,6 +908,9 @@ let rec extern inctx scopes vars r =
| GCast (c, c') ->
CCast (sub_extern true scopes vars c,
Miscops.map_cast_type (extern_typ scopes vars) c')
+ | GProj (p, c) ->
+ let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
+ CProj (pr, sub_extern inctx scopes vars c)
) r'
and extern_typ (_,scopes) =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 61b33aa41..4afe301dd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -836,6 +836,18 @@ let intern_reference ref =
in
Smartlocate.global_of_extended_global r
+let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+ match info with
+ | Misctypes.UAnonymous -> None
+ | Misctypes.UUnknown -> None
+ | Misctypes.UNamed id -> Some (id, 0)
+
+let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+ match level with
+ | Misctypes.GProp -> Misctypes.GProp
+ | Misctypes.GSet -> Misctypes.GSet
+ | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+
(* Is it a global reference or a syntactic definition? *)
let intern_qualid loc qid intern env lvar us args =
match intern_extended_global_of_qualid (loc,qid) with
@@ -867,6 +879,10 @@ let intern_qualid loc qid intern env lvar us args =
DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
| _ -> err ()
end
+ | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+ | Some [_old_level], GSort _new_sort ->
+ (* TODO: add old_level and new_sort to the error message *)
+ user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
| Some _, _ -> err ()
in
c, projapp, args2
@@ -1869,7 +1885,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
- )
+ | CProj (pr, c) ->
+ match intern_reference pr with
+ | ConstRef p ->
+ DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
+ | _ ->
+ raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
+ )
and intern_type env = intern (set_type_scope env)
and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
diff --git a/interp/declare.ml b/interp/declare.ml
index 55f825c25..72cdabfd2 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -364,13 +364,8 @@ let infer_inductive_subtyping (pth, mind_ent) =
| Cumulative_ind_entry cumi ->
begin
let env = Global.env () in
- let env' =
- Environ.push_context
- (Univ.CumulativityInfo.univ_context cumi) env
- in
(* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
- let evd = Evd.from_env env' in
- (pth, Inductiveops.infer_inductive_subtyping env' evd mind_ent)
+ (pth, InferCumulativity.infer_inductive env mind_ent)
end
type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
diff --git a/interp/discharge.ml b/interp/discharge.ml
index 75bfca307..710f88c3f 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -92,7 +92,7 @@ let process_inductive info modlist mib =
let auctx = Univ.ACumulativityInfo.univ_context cumi in
let subst, auctx = Lib.discharge_abstract_universe_context info auctx in
let auctx = Univ.AUContext.repr auctx in
- subst, Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context auctx)
+ subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx)
in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in
let inds =
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 20492e38c..326d05cba 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Miscops.glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
+| NProj (p1, c1), NProj (p2, c2) ->
+ Projection.equal p1 p2 && eq_notation_constr vars c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _), _ -> false
+ | NRec _ | NSort _ | NCast _ | NProj _), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
+ | NProj (p,c) -> GProj (p, f e c)
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a =
if arg != None then has_ltac := true;
NHole (w, naming, arg)
| GRef (r,_) -> NRef r
+ | GProj (p, c) -> NProj (p, aux c)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
@@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw =
let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
+ | NProj (p, c) ->
+ let kn = Projection.constant p in
+ let b = Projection.unfolded p in
+ let kn' = subst_constant subst kn in
+ let c' = subst_notation_constr subst bound c in
+ if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c')
+
+
let subst_interpretation subst (metas,pat) =
let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in
(metas,subst_notation_constr subst bound pat)
@@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_names metas (alp,sigma) (Name id') na in
match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
+ | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 ->
+ match_in u alp metas sigma t1 t2
+
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _), _ -> raise No_match
+ | GCast _ | GProj _ ), _ -> raise No_match
and match_in u = match_ true u
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 8bcdbcc0e..fbf9e248a 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -97,6 +97,7 @@ and constr_expr_r =
| CGeneralization of binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
+ | CProj of reference * constr_expr
and constr_expr = constr_expr_r CAst.t
and case_expr = constr_expr (* expression that is being matched *)
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index f311d33b8..61bbe2c26 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -55,6 +55,7 @@ type 'a glob_constr_r =
| GSort of glob_sort
| GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
| GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
+ | GProj of Projection.t * 'a glob_constr_g
and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
diff --git a/intf/notation_term.ml b/intf/notation_term.ml
index 7823d3feb..cad6f4b82 100644
--- a/intf/notation_term.ml
+++ b/intf/notation_term.ml
@@ -43,6 +43,7 @@ type notation_constr =
notation_constr array * notation_constr array
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
+ | NProj of Projection.t * notation_constr
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
diff --git a/intf/pattern.ml b/intf/pattern.ml
index 20636accf..64873a039 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -26,7 +26,7 @@ type constr_pattern =
| PRel of int
| PApp of constr_pattern * constr_pattern array
| PSoApp of patvar * constr_pattern list
- | PProj of projection * constr_pattern
+ | PProj of Projection.t * constr_pattern
| PLambda of Name.t * constr_pattern * constr_pattern
| PProd of Name.t * constr_pattern * constr_pattern
| PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b117f8714..cfca335d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -234,22 +234,32 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
let check_subtyping cumi paramsctxt env_ar inds =
let numparams = Context.Rel.nhyps paramsctxt in
- let sbsubst = CumulativityInfo.subtyping_susbst cumi in
- let dosubst = subst_univs_level_constr sbsubst in
let uctx = CumulativityInfo.univ_context cumi in
- let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
- let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
+ let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+ let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
+ LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
+ in
+ let dosubst = subst_univs_level_constr lmap in
+ let instance_other = Instance.of_array new_levels in
+ let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
let env = Environ.push_context uctx env_ar in
let env = Environ.push_context uctx_other env in
- let env = push_context (CumulativityInfo.subtyp_context cumi) env in
+ let subtyp_constraints =
+ CumulativityInfo.leq_constraints cumi
+ (UContext.instance uctx) instance_other
+ Constraint.empty
+ in
+ let env = Environ.add_constraints subtyp_constraints env in
(* process individual inductive types: *)
Array.iter (fun (id,cn,lc,(sign,arity)) ->
match arity with
| RegularArity (_, full_arity, _) ->
check_subtyping_arity_constructor env dosubst full_arity numparams true;
Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
- | TemplateArity _ -> ()
+ | TemplateArity _ ->
+ anomaly ~label:"check_subtyping"
+ Pp.(str "template polymorphism and cumulative polymorphism are not compatible")
) inds
(* Type-check an inductive definition. Does not check positivity
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4e7d6b218..1e35f6c03 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -157,9 +157,8 @@ let call_linker ?(fatal=true) prefix f upds =
register_native_file prefix
with Dynlink.Error e as exn ->
let exn = CErrors.push exn in
- let msg = "Dynlink error, " ^ Dynlink.error_message e in
- if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
- else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
+ if fatal then iraise exn
+ else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
match upds with Some upds -> update_locations upds | _ -> ()
let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1724f210d..da7042713 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -200,13 +200,9 @@ let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare =
{ (* Might raise NotConvertible *)
- compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+ compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
- conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
- Univ.Instance.t -> int -> 'a -> 'a;
- conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
- Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
- }
+ compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
type 'a universe_state = 'a * 'a universe_compare
@@ -215,18 +211,68 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
let sort_cmp_universes env pb s0 s1 (u, check) =
- (check.compare env pb s0 s1 u, check)
+ (check.compare_sorts env pb s0 s1 u, check)
(* [flex] should be true for constants, false for inductive types and
constructors. *)
let convert_instances ~flex u u' (s, check) =
(check.compare_instances ~flex u u' s, check)
-
-let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
- (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
-let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
- (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
+let get_cumulativity_constraints cv_pb cumi u u' =
+ match cv_pb with
+ | CONV ->
+ Univ.ACumulativityInfo.eq_constraints cumi u u' Univ.Constraint.empty
+ | CUMUL ->
+ Univ.ACumulativityInfo.leq_constraints cumi u u' Univ.Constraint.empty
+
+let inductive_cumulativity_arguments (mind,ind) =
+ mind.Declarations.mind_nparams +
+ mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+
+let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ ->
+ assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+ s
+ | Declarations.Polymorphic_ind _ ->
+ cmp_instances u1 u2 s
+ | Declarations.Cumulative_ind cumi ->
+ let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
+ if not (Int.equal num_param_arity nargs) then
+ cmp_instances u1 u2 s
+ else
+ let csts = get_cumulativity_constraints cv_pb cumi u1 u2 in
+ cmp_cumul csts s
+
+let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
+ convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+ cv_pb ind nargs u1 u2 s, check
+
+let constructor_cumulativity_arguments (mind, ind, ctor) =
+ let nparamsctxt =
+ mind.Declarations.mind_nparams +
+ mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+ (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+ nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
+
+let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ ->
+ assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
+ s
+ | Declarations.Polymorphic_ind _ ->
+ cmp_instances u1 u2 s
+ | Declarations.Cumulative_ind cumi ->
+ let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
+ if not (Int.equal num_cnstr_args nargs) then
+ cmp_instances u1 u2 s
+ else
+ let csts = get_cumulativity_constraints CONV cumi u1 u2 in
+ cmp_cumul csts s
+
+let convert_constructors ctor nargs u1 u2 (s, check) =
+ convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
+ ctor nargs u1 u2 s, check
let conv_table_key infos k1 k2 cuniv =
if k1 == k2 then cuniv else
@@ -325,9 +371,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in
let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in
- (* compute the lifts that apply to the head of the term (hd1 and hd2) *)
- let el1 = el_stack lft1 v1 in
- let el2 = el_stack lft2 v2 in
+ (** We delay the computation of the lifts that apply to the head of the term
+ with [el_stack] inside the branches where they are actually used. *)
match (fterm_of hd1, fterm_of hd2) with
(* case of leaves *)
| (FAtom a1, FAtom a2) ->
@@ -343,6 +388,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| _ -> raise NotConvertible)
| (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
if Evar.equal ev1 ev2 then
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
convert_vect l2r infos el1 el2
(Array.map (mk_clos env1) args1)
@@ -351,6 +398,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
if Int.equal (reloc_rel n el1) (reloc_rel m el2)
then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -395,6 +444,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
| None ->
if Constant.equal (Projection.constant p1) (Projection.constant p2)
&& compare_stack_shape v1 v2 then
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
convert_stacks l2r infos lft1 lft2 v1 v2 u1
else (* Two projections in WHNF: unfold *)
@@ -434,6 +485,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
@@ -441,6 +494,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
(* Luo's system *)
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
@@ -509,15 +564,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
- let cuniv =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- convert_instances ~flex:false u1 u2 cuniv
- | Declarations.Cumulative_ind cumi ->
- convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
- u2 (CClosure.stack_args_size v2) cuniv
- in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ let nargs = CClosure.stack_args_size v1 in
+ if not (Int.equal nargs (CClosure.stack_args_size v2))
+ then raise NotConvertible
+ else
+ let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
@@ -527,16 +579,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else
let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
- let cuniv =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- convert_instances ~flex:false u1 u2 cuniv
- | Declarations.Cumulative_ind _ ->
- convert_constructors
- (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
- u2 (CClosure.stack_args_size v2) cuniv
- in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ let nargs = CClosure.stack_args_size v1 in
+ if not (Int.equal nargs (CClosure.stack_args_size v2))
+ then raise NotConvertible
+ else
+ let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
+ convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* Eta expansion of records *)
@@ -562,6 +610,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
convert_vect l2r infos
@@ -577,6 +627,8 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
+ let el1 = el_stack lft1 v1 in
+ let el2 = el_stack lft2 v2 in
let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
convert_vect l2r infos
@@ -653,84 +705,14 @@ let check_convert_instances ~flex u u' univs =
else raise NotConvertible
(* general conversion and inference functions *)
-let infer_check_conv_inductives
- infer_check_convert_instances
- infer_check_inductive_instances
- cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- infer_check_convert_instances ~flex:false u1 u2 univs
- | Declarations.Cumulative_ind cumi ->
- let num_param_arity =
- mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- in
- if not (num_param_arity = sv1 && num_param_arity = sv2) then
- infer_check_convert_instances ~flex:false u1 u2 univs
- else
- infer_check_inductive_instances cv_pb cumi u1 u2 univs
-
-let infer_check_conv_constructors
- infer_check_convert_instances
- infer_check_inductive_instances
- (mind, ind, cns) u1 sv1 u2 sv2 univs =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
- infer_check_convert_instances ~flex:false u1 u2 univs
- | Declarations.Cumulative_ind cumi ->
- let num_cnstr_args =
- let nparamsctxt =
- mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
- nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
- in
- if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
- infer_check_convert_instances ~flex:false u1 u2 univs
- else
- infer_check_inductive_instances CONV cumi u1 u2 univs
-
-let check_inductive_instances cv_pb cumi u u' univs =
- let length_ind_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
- in
- let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
- if not ((length_ind_instance = Univ.Instance.length u) &&
- (length_ind_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- let comp_cst =
- let comp_subst = (Univ.Instance.append u u') in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
- let comp_cst =
- match cv_pb with
- CONV ->
- let comp_cst' =
- let comp_subst = (Univ.Instance.append u' u) in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
- Univ.Constraint.union comp_cst comp_cst'
- | CUMUL -> comp_cst
- in
- if (UGraph.check_constraints comp_cst univs) then univs
- else raise NotConvertible
-
-let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
- infer_check_conv_inductives
- check_convert_instances
- check_inductive_instances
- cv_pb ind u1 sv1 u2 sv2 univs
-
-let check_conv_constructors cns u1 sv1 u2 sv2 univs =
- infer_check_conv_constructors
- check_convert_instances
- check_inductive_instances
- cns u1 sv1 u2 sv2 univs
+let check_inductive_instances csts univs =
+ if (UGraph.check_constraints csts univs) then univs
+ else raise NotConvertible
let checked_universes =
- { compare = checked_sort_cmp_universes;
+ { compare_sorts = checked_sort_cmp_universes;
compare_instances = check_convert_instances;
- conv_inductives = check_conv_inductives;
- conv_constructors = check_conv_constructors}
+ compare_cumul_instances = check_inductive_instances; }
let infer_eq (univs, cstrs as cuniv) u u' =
if UGraph.check_eq univs u u' then cuniv
@@ -773,49 +755,13 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
else Univ.enforce_eq_instances u u' cstrs
in (univs, cstrs')
-let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
- let length_ind_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
- in
- let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
- if not ((length_ind_instance = Univ.Instance.length u) &&
- (length_ind_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- let comp_cst =
- let comp_subst = (Univ.Instance.append u u') in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
- let comp_cst =
- match cv_pb with
- CONV ->
- let comp_cst' =
- let comp_subst = (Univ.Instance.append u' u) in
- Univ.AUContext.instantiate comp_subst ind_subtypctx
- in
- Univ.Constraint.union comp_cst comp_cst'
- | CUMUL -> comp_cst
- in
- (univs, Univ.Constraint.union cstrs comp_cst)
-
-
-let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
- infer_check_conv_inductives
- infer_convert_instances
- infer_inductive_instances
- cv_pb ind u1 sv1 u2 sv2 univs
-
-let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
- infer_check_conv_constructors
- infer_convert_instances
- infer_inductive_instances
- cns u1 sv1 u2 sv2 univs
-
-let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
- { compare = infer_cmp_universes;
+let infer_inductive_instances csts (univs,csts') =
+ (univs, Univ.Constraint.union csts csts')
+
+let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
+ { compare_sorts = infer_cmp_universes;
compare_instances = infer_convert_instances;
- conv_inductives = infer_conv_inductives;
- conv_constructors = infer_conv_constructors}
+ compare_cumul_instances = infer_inductive_instances; }
let gen_conv cv_pb l2r reds env evars univs t1 t2 =
let b =
@@ -936,6 +882,18 @@ let hnf_prod_app env t n =
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
+let hnf_prod_applist_assum env n c l =
+ let rec app n subst t l =
+ if Int.equal n 0 then
+ if l == [] then substl subst t
+ else anomaly (Pp.str "Too many arguments.")
+ else match kind (whd_allnolet env t), l with
+ | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+ | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
+ | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+ app n [] c l
+
(* Dealing with arities *)
let dest_prod env =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 573e4c8bd..6f7e3f8f8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -35,15 +35,11 @@ type 'a extended_conversion_function =
type conv_pb = CONV | CUMUL
-type 'a universe_compare =
+type 'a universe_compare =
{ (* Might raise NotConvertible *)
- compare : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
+ compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
- conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
- Univ.Instance.t -> int -> 'a -> 'a;
- conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
- Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
- }
+ compare_cumul_instances : Univ.Constraint.t -> 'a -> 'a }
type 'a universe_state = 'a * 'a universe_compare
@@ -51,6 +47,12 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t
+val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t ->
+ Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t
+
+val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int
+val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int
+
val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t ->
'a * 'a universe_compare -> 'a * 'a universe_compare
@@ -103,6 +105,12 @@ val beta_app : constr -> constr -> constr
(** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
val hnf_prod_applist : env -> types -> constr list -> types
+(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to
+ the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it
+ returns [t] with the assumptions of [Γ] instantiated by [args] and
+ the local definitions of [Γ] expanded. *)
+val hnf_prod_applist_assum : env -> int -> types -> constr list -> types
+
(** Compatibility alias for Term.lambda_appvect_assum *)
val betazeta_appvect : int -> constr -> constr array -> constr
diff --git a/kernel/term.ml b/kernel/term.ml
index fae990d45..a4c92bd33 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -352,10 +352,11 @@ let lambda_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough lambda/let's.") in
app n [] c l
@@ -377,10 +378,11 @@ let prod_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a8cf6e1..b4597676a 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr
val lambda_appvect : constr -> constr array -> constr
(** In [lambda_applist_assum n c args], [c] is supposed to have the
- form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
val lambda_applist_assum : int -> constr -> constr list -> constr
@@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr
(** pseudo-reduction rule *)
(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
-val prod_appvect : constr -> constr array -> constr
-val prod_applist : constr -> constr list -> constr
+val prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
(** In [prod_appvect_assum n c args], [c] is supposed to have the
- form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
-val prod_appvect_assum : int -> constr -> constr array -> constr
-val prod_applist_assum : int -> constr -> constr list -> constr
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
(** {5 Other term destructors. } *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f72f6f26a..080bb7ad4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,7 +712,48 @@ type universe_level_subst = universe_level universe_map
(** A full substitution might involve algebraic universes *)
type universe_subst = universe universe_map
-module Instance : sig
+module Variance =
+struct
+ (** A universe position in the instance given to a cumulative
+ inductive can be the following. Note there is no Contravariant
+ case because [forall x : A, B <= forall x : A', B'] requires [A =
+ A'] as opposed to [A' <= A]. *)
+ type t = Irrelevant | Covariant | Invariant
+
+ let sup x y =
+ match x, y with
+ | Irrelevant, s | s, Irrelevant -> s
+ | Invariant, _ | _, Invariant -> Invariant
+ | Covariant, Covariant -> Covariant
+
+ let pr = function
+ | Irrelevant -> str "*"
+ | Covariant -> str "+"
+ | Invariant -> str "="
+
+ let leq_constraint csts variance u u' =
+ match variance with
+ | Irrelevant -> csts
+ | Covariant -> enforce_leq_level u u' csts
+ | Invariant -> enforce_eq_level u u' csts
+
+ let eq_constraint csts variance u u' =
+ match variance with
+ | Irrelevant -> csts
+ | Covariant | Invariant -> enforce_eq_level u u' csts
+
+ let leq_constraints variance u u' csts =
+ let len = Array.length u in
+ assert (len = Array.length u' && len = Array.length variance);
+ Array.fold_left3 leq_constraint csts variance u u'
+
+ let eq_constraints variance u u' csts =
+ let len = Array.length u in
+ assert (len = Array.length u' && len = Array.length variance);
+ Array.fold_left3 eq_constraint csts variance u u'
+end
+
+module Instance : sig
type t = Level.t array
val empty : t
@@ -732,7 +773,7 @@ module Instance : sig
val subst_fn : universe_level_subst_fn -> t -> t
- val pr : (Level.t -> Pp.t) -> t -> Pp.t
+ val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
val levels : t -> LSet.t
end =
struct
@@ -808,8 +849,12 @@ struct
let levels x = LSet.of_array x
- let pr =
- prvect_with_sep spc
+ let pr prl ?variance =
+ let ppu i u =
+ let v = Option.map (fun v -> v.(i)) variance in
+ pr_opt_no_spc Variance.pr v ++ prl u
+ in
+ prvecti_with_sep spc ppu
let equal t u =
t == u ||
@@ -873,9 +918,9 @@ struct
let empty = (Instance.empty, Constraint.empty)
let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
- let pr prl (univs, cst as ctx) =
+ let pr prl ?variance (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -911,66 +956,42 @@ end
type abstract_universe_context = AUContext.t
let hcons_abstract_universe_context = AUContext.hcons
-(** Universe info for cumulative inductive types:
- A context of universe levels
- with universe constraints, representing local universe variables
- and constraints, together with a context of universe levels with
- universe constraints, representing conditions for subtyping used
- for inductive types.
+(** Universe info for cumulative inductive types: A context of
+ universe levels with universe constraints, representing local
+ universe variables and constraints, together with an array of
+ Variance.t.
- This data structure maintains the invariant that the context for
- subtyping constraints is exactly twice as big as the context for
- universe constraints. *)
+ This data structure maintains the invariant that the variance
+ array has the same length as the universe instance. *)
module CumulativityInfo =
struct
- type t = universe_context * universe_context
+ type t = universe_context * Variance.t array
let make x =
- if (Instance.length (UContext.instance (snd x))) =
- (Instance.length (UContext.instance (fst x))) * 2 then x
+ if (Instance.length (UContext.instance (fst x))) =
+ (Array.length (snd x)) then x
else anomaly (Pp.str "Invalid subtyping information encountered!")
- let empty = (UContext.empty, UContext.empty)
- let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst
+ let empty = (UContext.empty, [||])
+ let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
- let halve_context ctx =
- let len = Array.length (Instance.to_array ctx) in
- let halflen = len / 2 in
- (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
- Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
+ let pr prl (univs, variance) =
+ UContext.pr prl ~variance univs
- let pr prl (univcst, subtypcst) =
- if UContext.is_empty univcst then mt() else
- let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
- (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
- h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
- ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+ let hcons (univs, variance) = (* should variance be hconsed? *)
+ (UContext.hcons univs, variance)
- let hcons (univcst, subtypcst) =
- (UContext.hcons univcst, UContext.hcons subtypcst)
-
- let univ_context (univcst, subtypcst) = univcst
- let subtyp_context (univcst, subtypcst) = subtypcst
-
- let create_trivial_subtyping ctx ctx' =
- CArray.fold_left_i
- (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
- Constraint.empty (Instance.to_array ctx)
+ let univ_context (univs, subtypcst) = univs
+ let variance (univs, variance) = variance
(** This function takes a universe context representing constraints
- of an inductive and a Instance.t of fresh universe names for the
- subtyping (with the same length as the context in the given
- universe context) and produces a UInfoInd.t that with the
- trivial subtyping relation. *)
- let from_universe_context univcst freshunivs =
- let inst = (UContext.instance univcst) in
- assert (Instance.length freshunivs = Instance.length inst);
- (univcst, UContext.make (Instance.append inst freshunivs,
- create_trivial_subtyping inst freshunivs))
-
- let subtyping_susbst (univcst, subtypcst) =
- let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in
- Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
+ of an inductive and produces a CumulativityInfo.t with the
+ trivial subtyping relation. *)
+ let from_universe_context univs =
+ (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
+
+ let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
+ let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
end
@@ -1138,10 +1159,9 @@ let abstract_universes ctx =
let ctx = UContext.make (instance, cstrs) in
instance, ctx
-let abstract_cumulativity_info (univcst, substcst) =
- let instance, univcst = abstract_universes univcst in
- let _, substcst = abstract_universes substcst in
- (instance, (univcst, substcst))
+let abstract_cumulativity_info (univs, variance) =
+ let subst, univs = abstract_universes univs in
+ subst, (univs, variance)
(** Pretty-printing *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 63bef1b81..77ebf5a11 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -238,6 +238,20 @@ type universe_level_subst_fn = Level.t -> Level.t
type universe_subst = Universe.t universe_map
type universe_level_subst = Level.t universe_map
+module Variance :
+sig
+ (** A universe position in the instance given to a cumulative
+ inductive can be the following. Note there is no Contravariant
+ case because [forall x : A, B <= forall x : A', B'] requires [A =
+ A'] as opposed to [A' <= A]. *)
+ type t = Irrelevant | Covariant | Invariant
+
+ val sup : t -> t -> t
+
+ val pr : t -> Pp.t
+
+end
+
(** {6 Universe instances} *)
module Instance :
@@ -273,7 +287,7 @@ sig
val subst_fn : universe_level_subst_fn -> t -> t
(** Substitution by a level-to-level function. *)
- val pr : (Level.t -> Pp.t) -> t -> Pp.t
+ val pr : (Level.t -> Pp.t) -> ?variance:Variance.t array -> t -> Pp.t
(** Pretty-printing, no comments *)
val levels : t -> LSet.t
@@ -347,36 +361,32 @@ end
type abstract_universe_context = AUContext.t
[@@ocaml.deprecated "Use AUContext.t"]
-(** Universe info for inductive types: A context of universe levels
- with universe Constraint.t, representing local universe variables
- and Constraint.t, together with a context of universe levels with
- universe Constraint.t, representing conditions for subtyping used
- for inductive types.
+(** Universe info for cumulative inductive types: A context of
+ universe levels with universe constraints, representing local
+ universe variables and constraints, together with an array of
+ Variance.t.
- This data structure maintains the invariant that the context for
- subtyping Constraint.t is exactly twice as big as the context for
- universe Constraint.t. *)
+ This data structure maintains the invariant that the variance
+ array has the same length as the universe instance. *)
module CumulativityInfo :
sig
type t
- val make : UContext.t * UContext.t -> t
+ val make : UContext.t * Variance.t array -> t
val empty : t
val is_empty : t -> bool
val univ_context : t -> UContext.t
- val subtyp_context : t -> UContext.t
-
- (** This function takes a universe context representing Constraint.t
- of an inductive and a Instance.t of fresh universe names for the
- subtyping (with the same length as the context in the given
- universe context) and produces a UInfoInd.t that with the
- trivial subtyping relation. *)
- val from_universe_context : UContext.t -> Instance.t -> t
+ val variance : t -> Variance.t array
- val subtyping_susbst : t -> universe_level_subst
+ (** This function takes a universe context representing constraints
+ of an inductive and produces a CumulativityInfo.t with the
+ trivial subtyping relation. *)
+ val from_universe_context : UContext.t -> t
+ val leq_constraints : t -> Instance.t constraint_function
+ val eq_constraints : t -> Instance.t constraint_function
end
type cumulativity_info = CumulativityInfo.t
@@ -387,7 +397,9 @@ sig
type t
val univ_context : t -> AUContext.t
- val subtyp_context : t -> AUContext.t
+ val variance : t -> Variance.t array
+ val leq_constraints : t -> Instance.t constraint_function
+ val eq_constraints : t -> Instance.t constraint_function
end
type abstract_cumulativity_info = ACumulativityInfo.t
@@ -481,9 +493,11 @@ val make_abstract_instance : AUContext.t -> Instance.t
val pr_constraint_type : constraint_type -> Pp.t
val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
-val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t
+val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+ UContext.t -> Pp.t
val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
-val pr_abstract_universe_context : (Level.t -> Pp.t) -> AUContext.t -> Pp.t
+val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
+ AUContext.t -> Pp.t
val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
val explain_universe_inconsistency : (Level.t -> Pp.t) ->
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 1e52af0be..e6f1d7e06 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -114,7 +114,7 @@ let process_cmd_line orig_dir proj args =
let parsing_project_file = ref (proj.project_file <> None) in
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
- let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+ let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
let mk_path d =
let p = CUnix.correct_path d orig_dir in
{ path = CUnix.remove_path_dot (post_canonize p);
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 62b909516..37f38c8ff 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -94,8 +94,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit
consequences. *)
val msg_error : ?loc:Loc.t -> Pp.t -> unit
-(** Message indicating that something went really wrong, though still
- recoverable; otherwise an exception would have been raised. *)
+[@@ocaml.deprecated "msg_error is an internal function and should not be \
+ used unless you know what you are doing. Use \
+ [CErrors.user_err] instead."]
val msg_debug : ?loc:Loc.t -> Pp.t -> unit
(** For debugging purposes *)
diff --git a/library/globnames.ml b/library/globnames.ml
index 9d7ab2db8..a6e75fdb6 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -30,7 +30,7 @@ let eq_gr gr1 gr2 =
| IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
| ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
| VarRef v1, VarRef v2 -> Id.equal v1 v2
- | _ -> false
+ | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false
let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0b929b8ca..f7639d22d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -591,6 +591,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
+ | GProj _ -> user_err Pp.(str "Funind does not support primitive projections")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
@@ -697,6 +698,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
+ | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections")
and build_entry_lc_from_case env funname make_discr
(el:tomatch_tuples)
(brl:Glob_term.cases_clauses) avoid :
@@ -1245,7 +1247,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function
discrimination ones *)
| GSort _ -> params
| GHole _ -> params
- | GIf _ | GRec _ | GCast _ ->
+ | GIf _ | GRec _ | GCast _ | GProj _ ->
raise (UserError(Some "compute_cst_params", str "Not handled case"))
) gt
and compute_cst_params_from_app acc (params,rtl) =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index be8abb92e..b4ca1073c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -109,6 +109,7 @@ let change_vars =
| GCast(b,c) ->
GCast(change_vars mapping b,
Miscops.map_cast_type (change_vars mapping) c)
+ | GProj(p,c) -> GProj(p, change_vars mapping c)
) rt
and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
let new_mapping = List.fold_right Id.Map.remove idl mapping in
@@ -293,6 +294,7 @@ let rec alpha_rt excluded rt =
GApp(alpha_rt excluded f,
List.map (alpha_rt excluded) args
)
+ | GProj(p,c) -> GProj(p, alpha_rt excluded c)
in
new_rt
@@ -344,6 +346,7 @@ let is_free_in id =
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
| GCast (b,CastCoerce) -> is_free_in b
+ | GProj (_,c) -> is_free_in c
) x
and is_free_in_br (_,(ids,_,rt)) =
(not (Id.List.mem id ids)) && is_free_in rt
@@ -437,6 +440,8 @@ let replace_var_by_term x_id term =
| GCast(b,c) ->
GCast(replace_var_by_pattern b,
Miscops.map_cast_type replace_var_by_pattern c)
+ | GProj(p,c) ->
+ GProj(p,replace_var_by_pattern c)
) x
and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
if List.exists (fun id -> Id.compare id x_id == 0) idl
@@ -540,6 +545,7 @@ let expand_as =
| GCases(sty,po,el,brl) ->
GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
+ | GProj(p,c) -> GProj(p, expand_as map c)
)
and expand_as_br map (loc,(idl,cpl,rt)) =
(loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 071bab2f3..58154d310 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -215,6 +215,7 @@ let is_rec names =
| GCases(_,_,el,brl) ->
List.exists (fun (e,_) -> lookup names e) el ||
List.exists (lookup_br names) brl
+ | GProj(_,c) -> lookup names c
and lookup_br names (_,(idl,_,rt)) =
let new_names = List.fold_right Id.Set.remove idl names in
lookup new_names rt
@@ -779,6 +780,7 @@ let rec add_args id new_args = CAst.map (function
| CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
| CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization.")
| CDelimiters _ -> anomaly ~label:"add_args " (Pp.str "CDelimiters.")
+ | CProj _ -> user_err Pp.(str "Funind does not support primitive projections")
)
exception Stop of Constrexpr.constr_expr
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 23993243f..754e88139 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t =
| Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
| Proj (p,c) ->
let noparams () =
- let pb = Environ.lookup_projection p (snd env) in
- let pars = pb.Declarations.proj_npars in
- let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
- let args = List.make pars hole in
- GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
- (args @ [detype d flags avoid env sigma c]))
+ GProj (p, detype d flags avoid env sigma c)
in
if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
try noparams ()
@@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function
let r1' = subst_glob_constr subst r1 in
let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
if r1' == r1 && k' == k then raw else GCast (r1',k')
+
+ | GProj (p,c) as raw ->
+ let kn = Projection.constant p in
+ let b = Projection.unfolded p in
+ let kn' = subst_constant subst kn in
+ let c' = subst_glob_constr subst c in
+ if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c')
)
(* Utilities to transform kernel cases to simple pattern-matching problem *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 41c4616f7..dc3acbc3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -353,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
let check_leq_inductives evd cumi u u' =
let u = EConstr.EInstance.kind evd u in
let u' = EConstr.EInstance.kind evd u' in
- let length_ind_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
- in
- let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in
- if not ((length_ind_instance = Univ.Instance.length u) &&
- (length_ind_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- begin
- let comp_subst = (Univ.Instance.append u u') in
- let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in
- Evd.add_constraints evd comp_cst
- end
+ Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u')
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 093f1f0b6..a21137a05 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
Miscops.intro_pattern_naming_eq nam1 nam2
| GCast (c1, t1), GCast (c2, t2) ->
f c1 c2 && cast_type_eq f t1 t2
+ | GProj (p1, t1), GProj (p2, t2) ->
+ Projection.equal p1 p2 && f t1 t2
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ |
- GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false
+ GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false
let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
@@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function
let comp1 = f c in
let comp2 = Miscops.map_cast_type f k in
GCast (comp1,comp2)
+ | GProj (p,c) ->
+ GProj (p, f c)
| (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
)
@@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in
f acc c
+ | GProj(_,c) ->
+ f acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
)
@@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
let acc = match k with
| CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in
f v acc c
+ | GProj(_,c) ->
+ f v acc c
| (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc))
let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 78e6bc6f1..275a079d5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg =
List.exists
(fun ra ->
match dest_recarg ra with
- | Mrec (_,i) -> Int.List.mem i listind
+ | Mrec (_,i) -> Int.List.mem i listind
| _ -> false) rvec
in
Array.exists one_is_rec (dest_subterms rarg)
@@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches =
if (* dependent *) not (Vars.noccurn sigma 1 t) &&
not (has_dependent_elim mib) then
user_err ~hdr:"make_case_or_project"
- Pp.(str"Dependent case analysis not allowed" ++
- str" on inductive type " ++ Names.MutInd.print (fst ind))
+ Pp.(str"Dependent case analysis not allowed" ++
+ str" on inductive type " ++ Names.MutInd.print (fst ind))
in
let branch = branches.(0) in
let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
let n, subst =
List.fold_right
(fun decl (i, subst) ->
- match decl with
- | LocalAssum (na, t) ->
- let t = mkProj (Projection.make ps.(i) true, c) in
- (i + 1, t :: subst)
- | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
- ctx (0, [])
+ match decl with
+ | LocalAssum (na, t) ->
+ let t = mkProj (Projection.make ps.(i) true, c) in
+ (i + 1, t :: subst)
+ | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
+ ctx (0, [])
in Vars.substl subst br
(* substitution in a signature *)
@@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign =
let pv' = whd_all env sigma pval in
match EConstr.kind sigma pv', arsign with
| Lambda (na,t,b), (LocalAssum _)::arsign ->
- srec (push_rel_assum (na, t) env) b arsign
+ srec (push_rel_assum (na, t) env) b arsign
| Lambda (na,_,t), _ ->
(* The following code has an impact on the introduction names
- given by the tactics "case" and "inversion": when the
- elimination is not dependent, "case" uses Anonymous for
- inductive types in Prop and names created by mkProd_name for
- inductive types in Set/Type while "inversion" uses anonymous
- for inductive types both in Prop and Set/Type !!
-
- Previously, whether names were created or not relied on
- whether the predicate created in Indrec.make_case_com had a
- dependent arity or not. To avoid different predicates
- printed the same in v8, all predicates built in indrec.ml
- got a dependent arity (Aug 2004). The new way to decide
- whether names have to be created or not is to use an
- Anonymous or Named variable to enforce the expected
- dependency status (of course, Anonymous implies non
- dependent, but not conversely).
+ given by the tactics "case" and "inversion": when the
+ elimination is not dependent, "case" uses Anonymous for
+ inductive types in Prop and names created by mkProd_name for
+ inductive types in Set/Type while "inversion" uses anonymous
+ for inductive types both in Prop and Set/Type !!
+
+ Previously, whether names were created or not relied on
+ whether the predicate created in Indrec.make_case_com had a
+ dependent arity or not. To avoid different predicates
+ printed the same in v8, all predicates built in indrec.ml
+ got a dependent arity (Aug 2004). The new way to decide
+ whether names have to be created or not is to use an
+ Anonymous or Named variable to enforce the expected
+ dependency status (of course, Anonymous implies non
+ dependent, but not conversely).
From Coq > 8.2, using or not the the effective dependency of
the predicate is parametrable! *)
@@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function
let ctx,_ = Reduction.dest_arity env ty in
let u = Univ.Universe.make l in
let s =
- (* Does the sort of parameter [u] appear in (or equal)
+ (* Does the sort of parameter [u] appear in (or equal)
the sort of inductive [is] ? *)
if univ_level_mem l is then
scl (* constrained sort: replace by scl *)
else
(* unconstrained sort: replace by fresh universe *)
let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
- let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
- evdref := evm; s
+ let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
+ evdref := evm; s
in
(LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp)
| sign, [] -> sign (* Uniform parameters are exhausted *)
@@ -656,93 +656,3 @@ let control_only_guard env c =
iter_constr_with_full_binders push_rel iter env c
in
iter env c
-
-(* inference of subtyping condition for inductive types *)
-
-let infer_inductive_subtyping_arity_constructor
- (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) =
- let numchecked = ref 0 in
- let numparams = Context.Rel.nhyps params in
- let update_contexts (env, evd, csts) csts' =
- (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts')
- in
- let basic_check (env, evd, csts) tp =
- let result =
- if !numchecked >= numparams then
- let csts' =
- Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp)
- in update_contexts (env, evd, csts) csts'
- else
- (env, evd, csts)
- in
- numchecked := !numchecked + 1; result
- in
- let infer_typ typ ctxs =
- match typ with
- | LocalAssum (_, typ') ->
- begin
- try
- let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts)
- with Reduction.NotConvertible ->
- anomaly ~label:"inference of record/inductive subtyping relation failed"
- (Pp.str "Can't infer subtyping for record/inductive type")
- end
- | _ -> anomaly (Pp.str "")
- in
- let arcn' = Term.it_mkProd_or_LetIn arcn params in
- let typs, codom = Reduction.dest_prod env arcn' in
- let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in
- if not is_arity then basic_check last_contexts codom else last_contexts
-
-let infer_inductive_subtyping env evd mind_ent =
- let { Entries.mind_entry_params = params;
- Entries.mind_entry_inds = entries;
- Entries.mind_entry_universes = ground_univs;
- } = mind_ent
- in
- let uinfind =
- match ground_univs with
- | Entries.Monomorphic_ind_entry _
- | Entries.Polymorphic_ind_entry _ -> ground_univs
- | Entries.Cumulative_ind_entry cumi ->
- begin
- let uctx = Univ.CumulativityInfo.univ_context cumi in
- let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
- let dosubst = subst_univs_level_constr sbsubst in
- let instance_other =
- Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx)
- in
- let constraints_other =
- Univ.subst_univs_level_constraints
- sbsubst (Univ.UContext.constraints uctx)
- in
- let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env = Environ.push_context uctx env in
- let env = Environ.push_context uctx_other env in
- let evd =
- Evd.merge_universe_context
- evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other))
- in
- let (_, _, subtyp_constraints) =
- List.fold_left
- (fun ctxs indentry ->
- let _, params = Typeops.infer_local_decls env params in
- let ctxs' = infer_inductive_subtyping_arity_constructor
- ctxs dosubst indentry.Entries.mind_entry_arity true params
- in
- List.fold_left
- (fun ctxs cons ->
- infer_inductive_subtyping_arity_constructor
- ctxs dosubst cons false params
- )
- ctxs' indentry.Entries.mind_entry_lc
- ) (env, evd, Univ.Constraint.empty) entries
- in
- Entries.Cumulative_ind_entry
- (Univ.CumulativityInfo.make
- (Univ.CumulativityInfo.univ_context cumi,
- Univ.UContext.make
- (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi),
- subtyp_constraints)))
- end
- in {mind_ent with Entries.mind_entry_universes = uinfind;}
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 58b1ce6c3..55149552a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -199,12 +199,3 @@ val type_of_inductive_knowing_conclusion :
(********************)
val control_only_guard : env -> types -> unit
-
-(* inference of subtyping condition for inductive types *)
-(* for debugging purposes only to be removed *)
-val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t ->
-(constr -> constr) ->
-types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t
-
-val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry ->
- Entries.mutual_inductive_entry
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
new file mode 100644
index 000000000..a0a8276c5
--- /dev/null
+++ b/pretyping/inferCumulativity.ml
@@ -0,0 +1,224 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Reduction
+open Declarations
+open Constr
+open Univ
+open Util
+
+(** Throughout this module we modify a map [variances] from local
+ universes to [Variance.t]. It starts as a trivial mapping to
+ [Irrelevant] and every time we encounter a local universe we
+ restrict it accordingly. *)
+
+let infer_level_eq u variances =
+ if LMap.mem u variances
+ then LMap.set u Variance.Invariant variances
+ else variances
+
+let infer_level_leq u variances =
+ match LMap.find u variances with
+ | exception Not_found -> variances
+ | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances
+
+let infer_generic_instance_eq variances u =
+ Array.fold_left (fun variances u -> infer_level_eq u variances)
+ variances (Instance.to_array u)
+
+let variance_pb cv_pb var =
+ let open Variance in
+ match cv_pb, var with
+ | _, Irrelevant -> Irrelevant
+ | _, Invariant -> Invariant
+ | CONV, Covariant -> Invariant
+ | CUMUL, Covariant -> Covariant
+
+let infer_cumulative_ind_instance cv_pb cumi variances u =
+ Array.fold_left2 (fun variances varu u ->
+ match LMap.find u variances with
+ | exception Not_found -> variances
+ | varu' ->
+ LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances)
+ variances (ACumulativityInfo.variance cumi) (Instance.to_array u)
+
+let infer_inductive_instance cv_pb env variances ind nargs u =
+ let mind = Environ.lookup_mind (fst ind) env in
+ match mind.mind_universes with
+ | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+ | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+ | Cumulative_ind cumi ->
+ if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs)
+ then infer_generic_instance_eq variances u
+ else infer_cumulative_ind_instance cv_pb cumi variances u
+
+let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u =
+ let mind = Environ.lookup_mind mi env in
+ match mind.mind_universes with
+ | Monomorphic_ind _ -> assert (Instance.is_empty u); variances
+ | Polymorphic_ind _ -> infer_generic_instance_eq variances u
+ | Cumulative_ind cumi ->
+ if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs)
+ then infer_generic_instance_eq variances u
+ else infer_cumulative_ind_instance CONV cumi variances u
+
+let infer_sort cv_pb variances s =
+ match cv_pb with
+ | CONV ->
+ LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances
+ | CUMUL ->
+ LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances
+
+let infer_table_key infos variances c =
+ let open Names in
+ match c with
+ | ConstKey (_, u) ->
+ infer_generic_instance_eq variances u
+ | VarKey _ | RelKey _ -> variances
+
+let rec infer_fterm cv_pb infos variances hd stk =
+ Control.check_for_interrupt ();
+ let open CClosure in
+ let hd,stk = whd_stack infos hd stk in
+ match fterm_of hd with
+ | FAtom a ->
+ begin match kind a with
+ | Sort s -> infer_sort cv_pb variances s
+ | Meta _ -> infer_stack infos variances stk
+ | _ -> assert false
+ end
+ | FEvar ((_,args),e) ->
+ let variances = infer_stack infos variances stk in
+ infer_vect infos variances (Array.map (mk_clos e) args)
+ | FRel _ -> variances
+ | FFlex fl ->
+ let variances = infer_table_key infos variances fl in
+ infer_stack infos variances stk
+ | FProj (_,c) ->
+ let variances = infer_fterm CONV infos variances c [] in
+ infer_stack infos variances stk
+ | FLambda _ ->
+ let (_,ty,bd) = destFLambda mk_clos hd in
+ let variances = infer_fterm CONV infos variances ty [] in
+ infer_fterm CONV infos variances bd []
+ | FProd (_,dom,codom) ->
+ let variances = infer_fterm CONV infos variances dom [] in
+ infer_fterm cv_pb infos variances codom []
+ | FInd (ind, u) ->
+ let variances =
+ if Instance.is_empty u then variances
+ else
+ let nargs = stack_args_size stk in
+ infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+ in
+ infer_stack infos variances stk
+ | FConstruct (ctor,u) ->
+ let variances =
+ if Instance.is_empty u then variances
+ else
+ let nargs = stack_args_size stk in
+ infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+ in
+ infer_stack infos variances stk
+ | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
+ let n = Array.length cl in
+ let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in
+ let le = Esubst.subs_liftn n e in
+ let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in
+ infer_stack infos variances stk
+
+ (* Removed by whnf *)
+ | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false
+
+and infer_stack infos variances (stk:CClosure.stack) =
+ match stk with
+ | [] -> variances
+ | z :: stk ->
+ let open CClosure in
+ let variances = match z with
+ | Zapp v -> infer_vect infos variances v
+ | Zproj _ -> variances
+ | Zfix (fx,a) ->
+ let variances = infer_fterm CONV infos variances fx [] in
+ infer_stack infos variances a
+ | ZcaseT (ci,p,br,e) ->
+ let variances = infer_fterm CONV infos variances (mk_clos e p) [] in
+ infer_vect infos variances (Array.map (mk_clos e) br)
+ | Zshift _ -> variances
+ | Zupdate _ -> variances
+ in
+ infer_stack infos variances stk
+
+and infer_vect infos variances v =
+ Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v
+
+let infer_term cv_pb env variances c =
+ let open CClosure in
+ let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in
+ let infos = create_clos_infos reds env in
+ infer_fterm cv_pb infos variances (CClosure.inject c) []
+
+let infer_arity_constructor env variances arcn is_arity params =
+ let numchecked = ref 0 in
+ let numparams = Context.Rel.nhyps params in
+ let basic_check env variances tp =
+ let variances =
+ if !numchecked >= numparams then
+ infer_term CUMUL env variances tp
+ else
+ variances
+ in
+ numchecked := !numchecked + 1; variances
+ in
+ let infer_typ typ (env,variances) =
+ match typ with
+ | Context.Rel.Declaration.LocalAssum (_, typ') ->
+ (Environ.push_rel typ env, basic_check env variances typ')
+ | Context.Rel.Declaration.LocalDef _ -> assert false
+ in
+ let arcn' = Term.it_mkProd_or_LetIn arcn params in
+ let typs, codom = Reduction.dest_prod env arcn' in
+ let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in
+ (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j}
+ i is irrelevant, j is invariant. *)
+ if not is_arity then basic_check env variances codom else variances
+
+let infer_inductive env mie =
+ let open Entries in
+ let { mind_entry_params = params;
+ mind_entry_inds = entries; } = mie
+ in
+ let univs =
+ match mie.mind_entry_universes with
+ | Monomorphic_ind_entry _
+ | Polymorphic_ind_entry _ as univs -> univs
+ | Cumulative_ind_entry cumi ->
+ let uctx = CumulativityInfo.univ_context cumi in
+ let uarray = Instance.to_array @@ UContext.instance uctx in
+ let env = Environ.push_context uctx env in
+ let variances =
+ Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances)
+ LMap.empty uarray
+ in
+ let variances = List.fold_left (fun variances entry ->
+ let _, params = Typeops.infer_local_decls env params in
+ let variances = infer_arity_constructor
+ env variances entry.mind_entry_arity true params
+ in
+ List.fold_left
+ (fun variances cons ->
+ infer_arity_constructor
+ env variances cons false params)
+ variances entry.mind_entry_lc)
+ variances
+ entries
+ in
+ let variances = Array.map (fun u -> LMap.find u variances) uarray in
+ Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+ in
+ { mie with mind_entry_universes = univs }
diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli
new file mode 100644
index 000000000..a5037ea47
--- /dev/null
+++ b/pretyping/inferCumulativity.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
+ Entries.mutual_inductive_entry
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 41e09004c..1bec4a6f1 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -137,8 +137,7 @@ let rec head_pattern_bound t =
| PCase (_,p,c,br) -> head_pattern_bound c
| PRef r -> r
| PVar id -> VarRef id
- | PProj (p,c) -> ConstRef (Projection.constant p)
- | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _
+ | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _
-> raise BoundPattern
(* Perhaps they were arguments, but we don't beta-reduce *)
| PLambda _ -> raise BoundPattern
@@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
one non-trivial branch. These facts are used in [Constrextern]. *)
PCase (info, pred, pat_of_raw metas vars c, brs)
+ | GProj(p,c) ->
+ PProj(p, pat_of_raw metas vars c)
+
| GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
err ?loc (Pp.str "Non supported pattern."))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92dab24e2..8809558ff 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -737,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = pretype_sort ?loc evdref s in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
+ | GProj (p, c) ->
+ (* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
+ let cj = pretype empty_tycon env evdref lvar c in
+ judge_of_projection env.ExtraEnv.env !evdref p cj
+
| GApp (f,args) ->
let fj = pretype empty_tycon env evdref lvar f in
let floc = loc_of_glob_constr f in
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 1da5b4567..ae4ad0be7 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -4,6 +4,7 @@ Locusops
Pretype_errors
Reductionops
Inductiveops
+InferCumulativity
Vnorm
Arguments_renaming
Nativenorm
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 9ff9a75b3..ab1f3cd32 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
(*s High-level declaration of a canonical structure *)
-let error_not_structure ref =
+let error_not_structure ref description =
user_err ~hdr:"object_declare"
- (Id.print (basename_of_global ref) ++ str" is not a structure object.")
+ (str"Could not declare a canonical structure " ++
+ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++
+ str(description)))
let check_and_decompose_canonical_structure ref =
- let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
+ let sp =
+ match ref with
+ ConstRef sp -> sp
+ | _ -> error_not_structure ref "Expected an instance of a record or structure."
+ in
let env = Global.env () in
let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
- | None -> error_not_structure ref in
+ | None -> error_not_structure ref "Could not find its value in the global environment." in
let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
let body = EConstr.Unsafe.to_constr body in
let f,args = match kind body with
| App (f,args) -> f,args
- | _ -> error_not_structure ref in
+ | _ ->
+ error_not_structure ref "Expected a record or structure constructor applied to arguments." in
let indsp = match kind f with
| Construct ((indsp,1),u) -> indsp
- | _ -> error_not_structure ref in
- let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
+ | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+ let s =
+ try lookup_structure indsp
+ with Not_found ->
+ error_not_structure ref
+ ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
let ntrue_projs = List.count snd s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
- error_not_structure ref;
+ error_not_structure ref "Got too few arguments to the record or structure constructor.";
(sp,indsp)
let declare_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1893018a9..418ea271c 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma =
| Univ.UniverseInconsistency _ ->
raise Reduction.NotConvertible
-let sigma_check_inductive_instances cv_pb uinfind u u' sigma =
- let len_instance =
- Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind)
- in
- let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in
- if not ((len_instance = Univ.Instance.length u) &&
- (len_instance = Univ.Instance.length u')) then
- anomaly (Pp.str "Invalid inductive subtyping encountered!")
- else
- let comp_cst =
- let comp_subst = (Univ.Instance.append u u') in
- Univ.AUContext.instantiate comp_subst ind_sbctx
- in
- let comp_cst =
- match cv_pb with
- Reduction.CONV ->
- let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in
- Univ.Constraint.union comp_cst comp_cst'
- | Reduction.CUMUL -> comp_cst
- in
- try Evd.add_constraints sigma comp_cst
- with Evd.UniversesDiffer
- | Univ.UniverseInconsistency _ ->
- raise Reduction.NotConvertible
-
-let sigma_conv_inductives
- cv_pb (mind, ind) u1 sv1 u2 sv2 sigma =
- try sigma_compare_instances ~flex:false u1 u2 sigma with
- Reduction.NotConvertible ->
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Polymorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Cumulative_ind cumi ->
- let num_param_arity =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- in
- if not (num_param_arity = sv1 && num_param_arity = sv2) then
- raise Reduction.NotConvertible
- else
- sigma_check_inductive_instances cv_pb cumi u1 u2 sigma
-
-let sigma_conv_constructors
- (mind, ind, cns) u1 sv1 u2 sv2 sigma =
- try sigma_compare_instances ~flex:false u1 u2 sigma with
- Reduction.NotConvertible ->
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Polymorphic_ind _ ->
- raise Reduction.NotConvertible
- | Declarations.Cumulative_ind cumi ->
- let num_cnstr_args =
- let nparamsctxt =
- mind.Declarations.mind_nparams +
- mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
- in
- nparamsctxt +
- mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
- in
- if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
- raise Reduction.NotConvertible
- else
- sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma
+let sigma_check_inductive_instances csts sigma =
+ try Evd.add_constraints sigma csts
+ with Evd.UniversesDiffer
+ | Univ.UniverseInconsistency _ ->
+ raise Reduction.NotConvertible
let sigma_univ_state =
- { Reduction.compare = sigma_compare_sorts;
- Reduction.compare_instances = sigma_compare_instances;
- Reduction.conv_inductives = sigma_conv_inductives;
- Reduction.conv_constructors = sigma_conv_constructors}
+ let open Reduction in
+ { compare_sorts = sigma_compare_sorts;
+ compare_instances = sigma_compare_instances;
+ compare_cumul_instances = sigma_check_inductive_instances; }
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 9f084ae8d..153a48a71 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
val judge_of_product : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b21fbf0eb..c93b41786 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
let params,realargs = Util.Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
+ hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
let pT = whd_all env pT in
let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 51735bc9e..1146b42a0 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -732,6 +732,9 @@ let tag_var = tag Tag.variable
return (pr_prim_token p, prec_of_prim_token p)
| CDelimiters (sc,a) ->
return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+ | CProj (p,c) ->
+ let p = pr_proj (pr mt) pr_app c (CAst.make (CRef (p,None))) [] in
+ return (p, lproj)
in
let loc = constr_loc a in
pr_with_comments ?loc
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 2b7886d11..114a071ee 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -78,6 +78,15 @@ let print_ref reduce ref udecl =
in EConstr.it_mkProd_or_LetIn ccl ctx
else typ in
let univs = Global.universes_of_global ref in
+ let variance = match ref with
+ | VarRef _ | ConstRef _ -> None
+ | IndRef (ind,_) | ConstructRef ((ind,_),_) ->
+ let mind = Environ.lookup_mind ind (Global.env ()) in
+ begin match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None
+ | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi)
+ end
+ in
let inst = Univ.AUContext.instance univs in
let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in
let env = Global.env () in
@@ -89,7 +98,7 @@ let print_ref reduce ref udecl =
else mt ()
in
hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++
- Printer.pr_universe_ctx sigma univs)
+ Printer.pr_universe_ctx sigma ?variance univs)
(********************************)
(** Printing implicit arguments *)
diff --git a/printing/printer.ml b/printing/printer.ml
index a63004ceb..d720bc2f8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -263,10 +263,10 @@ let pr_universe_ctx_set sigma c =
else
mt()
-let pr_universe_ctx sigma c =
+let pr_universe_ctx sigma ?variance c =
if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
fnl()++pr_in_comment (fun c -> v 0
- (Univ.pr_universe_context (Termops.pr_evd_level sigma) c)) c
+ (Univ.pr_universe_context (Termops.pr_evd_level sigma) ?variance c)) c
else
mt()
diff --git a/printing/printer.mli b/printing/printer.mli
index 804014745..a3427920a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -120,7 +120,8 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t
val pr_polymorphic : bool -> Pp.t
val pr_cumulative : bool -> bool -> Pp.t
val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
-val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t
+val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array ->
+ Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t
val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
diff --git a/printing/printmod.ml b/printing/printmod.ml
index fb9d45a79..2cdb9be3f 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
let args = Context.Rel.to_extended_list mkRel 0 params in
- let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+ let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
- let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+ let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
@@ -113,13 +114,12 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
let instantiate_cumulativity_info cumi =
let open Univ in
let univs = ACumulativityInfo.univ_context cumi in
- let subtyp = ACumulativityInfo.subtyp_context cumi in
let expose ctx =
let inst = AUContext.instance ctx in
let cst = AUContext.instantiate inst ctx in
UContext.make (inst, cst)
in
- CumulativityInfo.make (expose univs, expose subtyp)
+ CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi)
let print_mutual_inductive env mind mib udecl =
let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
@@ -174,10 +174,11 @@ let print_record env mind mib udecl =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
let args = Context.Rel.to_extended_list mkRel 0 params in
- let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+ let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
- let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+ let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
diff --git a/stm/stm.ml b/stm/stm.ml
index b5848c662..6c956e134 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -85,8 +85,7 @@ let stm_purify f x =
Exninfo.iraise e
let execution_error ?loc state_id msg =
- feedback ~id:state_id
- (Message (Error, loc, msg))
+ feedback ~id:state_id (Message (Error, loc, msg))
module Hooks = struct
@@ -1579,12 +1578,13 @@ end = struct (* {{{ *)
| ReqStates sl -> RespStates (perform_states sl)
let on_marshal_error s = function
- | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^
- "The system state could not be sent to the master process."))
+ | States _ ->
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the master process."))
| BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
- msg_error(Pp.strbrk("Marshalling error: "^s^". "^
- "The system state could not be sent to the worker process. "^
- "Falling back to local, lazy, evaluation."));
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the worker process. "^
+ "Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop));
feedback (InProgress ~-1)
@@ -1672,7 +1672,7 @@ end = struct (* {{{ *)
let (e, info) = CErrors.push e in
(try match Stateid.get info with
| None ->
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1682,17 +1682,17 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (ReplayCommand { loc }, _) } ->
let start, stop = Option.cata Loc.unloc (0,0) loc in
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
- msg_error Pp.(str"unable to print error message: " ++
- str (Printexc.to_string e)));
+ msg_warning Pp.(str"unable to print error message: " ++
+ str (Printexc.to_string e)));
if drop then `ERROR_ADMITTED else `ERROR
let finish_task name (u,cst,_) d p l i =
@@ -2429,7 +2429,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
assert(redefine_qed = true);
if okeep != keep then
- msg_error(strbrk("The command closing the proof changed. "
+ msg_warning(strbrk("The command closing the proof changed. "
^"The kernel cannot take this into account and will "
^(if keep == VtKeep then "not check " else "reject ")
^"the "^(if keep == VtKeep then "new" else "incomplete")
@@ -2702,7 +2702,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
(u,a,true), p
with e ->
let e = CErrors.push e in
- msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
let merge_proof_branch ~valid ?id qast keep brname =
diff --git a/test-suite/bugs/closed/5726.v b/test-suite/bugs/closed/5726.v
new file mode 100644
index 000000000..53ef47357
--- /dev/null
+++ b/test-suite/bugs/closed/5726.v
@@ -0,0 +1,34 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Module GlobalReference.
+
+ Definition type' := Type.
+ Notation type := type'.
+ Check type@{Set}.
+
+End GlobalReference.
+
+Module TypeLiteral.
+
+ Notation type := Type.
+ Check type@{Set}.
+ Check type@{Prop}.
+
+End TypeLiteral.
+
+Module ExplicitSort.
+ Monomorphic Universe u.
+ Notation foo := Type@{u}.
+ Fail Check foo@{Set}.
+ Fail Check foo@{u}.
+
+ Notation bar := Type.
+ Check bar@{u}.
+End ExplicitSort.
+
+Module PropNotationUnsupported.
+ Notation foo := Prop.
+ Fail Check foo@{Set}.
+ Fail Check foo@{Type}.
+End PropNotationUnsupported.
diff --git a/test-suite/output/ErrorInCanonicalStructures.out b/test-suite/output/ErrorInCanonicalStructures.out
new file mode 100644
index 000000000..73da4f44f
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure Foo.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures.v b/test-suite/output/ErrorInCanonicalStructures.v
new file mode 100644
index 000000000..49597df6f
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures.v
@@ -0,0 +1,3 @@
+Record Foo := MkFoo { field1 : nat; field2 : nat -> nat }.
+
+Canonical Structure Foo.
diff --git a/test-suite/output/ErrorInCanonicalStructures2.out b/test-suite/output/ErrorInCanonicalStructures2.out
new file mode 100644
index 000000000..63a2871b8
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.out
@@ -0,0 +1,5 @@
+File "stdin", line 3, characters 0-24:
+Error:
+Could not declare a canonical structure bar.
+Expected an instance of a record or structure.
+
diff --git a/test-suite/output/ErrorInCanonicalStructures2.v b/test-suite/output/ErrorInCanonicalStructures2.v
new file mode 100644
index 000000000..10ee177aa
--- /dev/null
+++ b/test-suite/output/ErrorInCanonicalStructures2.v
@@ -0,0 +1,3 @@
+Definition bar := 99.
+
+Canonical Structure bar.
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e912003f0..af202ea01 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,3 +1,7 @@
The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
"A -> list' A -> list' (A * A)%type".
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
+
+For foo: Argument scopes are [type_scope _]
+For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 8db8956e3..8ff91268a 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -1,3 +1,7 @@
Fail Inductive list' (A:Set) : Set :=
| nil' : list' A
| cons' : A -> list' A -> list' (A*A).
+
+(* Check printing of let-ins *)
+Inductive foo (A : Type) (x : A) (y := x) := Foo.
+Print foo.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index d6d410d1a..668b4e578 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -5,7 +5,7 @@ PWrap has primitive projections with eta conversion.
For PWrap: Argument scope is [type_scope]
For pwrap: Argument scopes are [type_scope _]
punwrap@{u} =
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+fun (A : Type@{u}) (p : PWrap@{u} A) => p.(punwrap)
: forall A : Type@{u}, PWrap@{u} A -> A
(* u |= *)
diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v
index 0ee85712e..1fb3abfe4 100644
--- a/test-suite/success/cumulativity.v
+++ b/test-suite/success/cumulativity.v
@@ -45,6 +45,15 @@ Section TpLift.
End TpLift.
+Record Tp' := { tp' : Tp }.
+
+Definition CTp := Tp.
+(* here we have to reduce a constant to infer the correct subtyping. *)
+Record Tp'' := { tp'' : CTp }.
+
+Definition LiftTp'@{i j|i < j} : Tp'@{i} -> Tp'@{j} := fun x => x.
+Definition LiftTp''@{i j|i < j} : Tp''@{i} -> Tp''@{j} := fun x => x.
+
Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
Proof. reflexivity. Qed.
@@ -98,3 +107,20 @@ Section down.
intros H f g Hfg. exact (H f g Hfg).
Defined.
End down.
+
+Record Arrow@{i j} := { arrow : Type@{i} -> Type@{j} }.
+
+Fail Definition arrow_lift@{i i' j j' | i' < i, j < j'}
+ : Arrow@{i j} -> Arrow@{i' j'}
+ := fun x => x.
+
+Definition arrow_lift@{i i' j j' | i' = i, j < j'}
+ : Arrow@{i j} -> Arrow@{i' j'}
+ := fun x => x.
+
+Inductive Mut1 A :=
+| Base1 : Type -> Mut1 A
+| Node1 : (A -> Mut2 A) -> Mut1 A
+with Mut2 A :=
+ | Base2 : Type -> Mut2 A
+ | Node2 : Mut1 A -> Mut2 A.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index fbf992dbf..eae2c52de 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -2110,13 +2110,13 @@ Section Exists_Forall.
{Exists l} + {~ Exists l}.
Proof.
intro Pdec. induction l as [|a l' Hrec].
- - right. now rewrite Exists_nil.
+ - right. abstract now rewrite Exists_nil.
- destruct Hrec as [Hl'|Hl'].
* left. now apply Exists_cons_tl.
* destruct (Pdec a) as [Ha|Ha].
+ left. now apply Exists_cons_hd.
- + right. now inversion_clear 1.
- Qed.
+ + right. abstract now inversion 1.
+ Defined.
Inductive Forall : list A -> Prop :=
| Forall_nil : Forall nil
@@ -2152,9 +2152,9 @@ Section Exists_Forall.
- destruct Hrec as [Hl'|Hl'].
+ destruct (Pdec a) as [Ha|Ha].
* left. now apply Forall_cons.
- * right. now inversion_clear 1.
- + right. now inversion_clear 1.
- Qed.
+ * right. abstract now inversion 1.
+ + right. abstract now inversion 1.
+ Defined.
End One_predicate.
@@ -2179,6 +2179,16 @@ Section Exists_Forall.
* now apply Exists_cons_hd.
Qed.
+ Lemma neg_Forall_Exists_neg (P:A->Prop) (l:list A) :
+ (forall x:A, {P x} + { ~ P x }) ->
+ ~ Forall P l ->
+ Exists (fun x => ~ P x) l.
+ Proof.
+ intro Dec.
+ apply Exists_Forall_neg; intros.
+ destruct (Dec x); auto.
+ Qed.
+
Lemma Forall_Exists_dec (P:A->Prop) :
(forall x:A, {P x} + { ~ P x }) ->
forall l:list A,
@@ -2186,9 +2196,8 @@ Section Exists_Forall.
Proof.
intros Pdec l.
destruct (Forall_dec P Pdec l); [left|right]; trivial.
- apply Exists_Forall_neg; trivial.
- intro x. destruct (Pdec x); [now left|now right].
- Qed.
+ now apply neg_Forall_Exists_neg.
+ Defined.
Lemma Forall_impl : forall (P Q : A -> Prop), (forall a, P a -> Q a) ->
forall l, Forall P l -> Forall Q l.
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index ca02c983d..173eaae89 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -169,7 +169,8 @@ endif
COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS)
COQCHKFLAGS?=-silent -o $(COQLIBS)
-COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML)
+COQDOCFLAGS?=-interpolate -utf8
+COQDOCLIBS?=$(COQLIBS_NOML)
# The version of Coq being run and the version of coq_makefile that
# generated this makefile
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2433cb1d0..ca14b11bc 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -539,4 +539,4 @@ let _ =
coqdep ()
with CErrors.UserError(s,p) ->
let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
- Feedback.msg_error pp
+ Format.eprintf "%a@\n%!" Pp.pp_with pp
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5c1b27c33..aade101a4 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -312,7 +312,7 @@ let do_vernac ~time doc sid =
top_stderr (fnl ()); raise CErrors.Quit
| CErrors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise CErrors.Drop
- else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid)
+ else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid)
(* Exception printing should be done by the feedback listener,
however this is not yet ready so we rely on the exception for
now. *)
@@ -353,7 +353,7 @@ let rec loop ~time doc =
| CErrors.Drop -> doc
| CErrors.Quit -> exit 0
| any ->
- Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
+ top_stderr (str "Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++
str"Please report" ++
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 1c8677e9c..41474fc63 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -340,7 +340,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
match uctx with
| Polymorphic_const_entry uctx ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
+ Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
else Polymorphic_ind_entry uctx
| Monomorphic_const_entry uctx ->
Monomorphic_ind_entry uctx
@@ -356,7 +356,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
}
in
(if poly && cum then
- Inductiveops.infer_inductive_subtyping env_ar sigma mind_ent
+ InferCumulativity.infer_inductive env_ar mind_ent
else mind_ent), Evd.universe_binders sigma, impls
(* Very syntactical equality *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index d328ad0cf..fc3495796 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -32,6 +32,7 @@ let explain_exn_default = function
| Sys_error msg -> hov 0 (str "System error: " ++ guill msg)
| Out_of_memory -> hov 0 (str "Out of memory.")
| Stack_overflow -> hov 0 (str "Stack overflow.")
+ | Dynlink.Error e -> hov 0 (str "Dynlink error: " ++ str Dynlink.(error_message e))
| Timeout -> hov 0 (str "Timeout!")
| Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
(* Exceptions with pre-evaluated error messages *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1e464eb8b..d9af5378f 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -423,16 +423,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
mind_entry_universes = univs;
}
in
- let mie =
- match ctx with
- | Polymorphic_const_entry ctx ->
- let env = Global.env () in
- let env' = Environ.push_context ctx env in
- let evd = Evd.from_env env' in
- Inductiveops.infer_inductive_subtyping env' evd mie
- | Monomorphic_const_entry _ ->
- mie
- in
+ let mie = InferCumulativity.infer_inductive (Global.env ()) mie in
let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
let rsp = (kn,0) in (* This is ind path of idstruc *)
let cstr = (rsp,1) in
@@ -501,7 +492,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
match univs with
| Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+ Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
else
Polymorphic_ind_entry univs
| Monomorphic_const_entry univs ->
@@ -632,7 +623,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
match univs with
| Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
+ Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
else
Polymorphic_ind_entry univs
| Monomorphic_const_entry univs ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index be09696d1..7223389c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -189,7 +189,7 @@ let print_module r =
Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
| _ -> raise Not_found
with
- Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
+ Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
let print_modtype r =
let (loc,qid) = qualid_of_reference r in
@@ -202,7 +202,7 @@ let print_modtype r =
let mp = Nametab.locate_module qid in
Feedback.msg_notice (Printmod.print_module false mp)
with Not_found ->
- Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
+ user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
let print_namespace ns =
let ns = List.rev (Names.DirPath.repr ns) in