aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/checker.ml5
-rw-r--r--checker/checker.mli9
-rw-r--r--checker/cic.mli12
-rw-r--r--checker/closure.ml46
-rw-r--r--checker/closure.mli14
-rw-r--r--checker/declarations.ml4
-rw-r--r--checker/environ.ml39
-rw-r--r--checker/environ.mli7
-rw-r--r--checker/indtypes.ml34
-rw-r--r--checker/inductive.ml16
-rw-r--r--checker/main.mli10
-rw-r--r--checker/mod_checking.ml11
-rw-r--r--checker/print.mli11
-rw-r--r--checker/reduction.ml60
-rw-r--r--checker/univ.ml42
-rw-r--r--checker/univ.mli17
-rw-r--r--checker/validate.ml2
-rw-r--r--checker/validate.mli9
-rw-r--r--checker/values.ml40
-rw-r--r--checker/values.mli26
-rw-r--r--checker/votour.ml6
-rw-r--r--checker/votour.mli10
22 files changed, 276 insertions, 154 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index fee31b6675..e8eff889c8 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"
@@ -208,8 +208,7 @@ let usage () =
open Type_errors
let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report" ++
- strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
+let report () = strbrk (". Please report at " ^ Coq_config.wwwbugtracker ^ ".")
let guill s = str "\"" ++ str s ++ str "\""
diff --git a/checker/checker.mli b/checker/checker.mli
new file mode 100644
index 0000000000..ceab137747
--- /dev/null
+++ b/checker/checker.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* 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 start : unit -> unit
diff --git a/checker/cic.mli b/checker/cic.mli
index 4a0e706aa1..95dd18f5f3 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -170,6 +170,17 @@ type set_predicativity = ImpredicativeSet | PredicativeSet
type engagement = set_predicativity
+(** {6 Conversion oracle} *)
+
+type level = Expand | Level of int | Opaque
+
+type oracle = {
+ var_opacity : level Id.Map.t;
+ cst_opacity : level Cmap.t;
+ var_trstate : Id.Pred.t;
+ cst_trstate : Cpred.t;
+}
+
(** {6 Representation of constants (Definition/Axiom) } *)
@@ -219,6 +230,7 @@ type typing_flags = {
check_guarded : bool; (** If [false] then fixed points and co-fixed
points are assumed to be total. *)
check_universes : bool; (** If [false] universe constraints are not checked *)
+ conv_oracle : oracle; (** Unfolding strategies for conversion *)
}
type constant_body = {
diff --git a/checker/closure.ml b/checker/closure.ml
index 3a56bba015..14b31e09d6 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -49,13 +49,6 @@ let with_stats c =
end else
Lazy.force c
-type transparent_state = Id.Pred.t * Cpred.t
-let all_opaque = (Id.Pred.empty, Cpred.empty)
-let all_transparent = (Id.Pred.full, Cpred.full)
-
-let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
-let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
-
module type RedFlagsSig = sig
type reds
type red_kind
@@ -63,8 +56,6 @@ module type RedFlagsSig = sig
val fDELTA : red_kind
val fIOTA : red_kind
val fZETA : red_kind
- val fCONST : Constant.t -> red_kind
- val fVAR : Id.t -> red_kind
val no_red : reds
val red_add : reds -> red_kind -> reds
val mkflags : red_kind list -> reds
@@ -80,51 +71,33 @@ module RedFlags = (struct
type reds = {
r_beta : bool;
r_delta : bool;
- r_const : transparent_state;
r_zeta : bool;
r_evar : bool;
r_iota : bool }
type red_kind = BETA | DELTA | IOTA | ZETA
- | CONST of Constant.t | VAR of Id.t
+
let fBETA = BETA
let fDELTA = DELTA
let fIOTA = IOTA
let fZETA = ZETA
- let fCONST kn = CONST kn
- let fVAR id = VAR id
let no_red = {
r_beta = false;
r_delta = false;
- r_const = all_opaque;
r_zeta = false;
r_evar = false;
r_iota = false }
let red_add red = function
| BETA -> { red with r_beta = true }
- | DELTA -> { red with r_delta = true; r_const = all_transparent }
- | CONST kn ->
- let (l1,l2) = red.r_const in
- { red with r_const = l1, Cpred.add kn l2 }
+ | DELTA -> { red with r_delta = true}
| IOTA -> { red with r_iota = true }
| ZETA -> { red with r_zeta = true }
- | VAR id ->
- let (l1,l2) = red.r_const in
- { red with r_const = Id.Pred.add id l1, l2 }
let mkflags = List.fold_left red_add no_red
let red_set red = function
| BETA -> incr_cnt red.r_beta beta
- | CONST kn ->
- let (_,l) = red.r_const in
- let c = Cpred.mem kn l in
- incr_cnt c delta
- | VAR id -> (* En attendant d'avoir des kn pour les Var *)
- let (l,_) = red.r_const in
- let c = Id.Pred.mem id l in
- incr_cnt c delta
| ZETA -> incr_cnt red.r_zeta zeta
| IOTA -> incr_cnt red.r_iota iota
| DELTA -> (* Used for Rel/Var defined in context *)
@@ -700,6 +673,9 @@ let contract_fix_vect fix =
in
(subs_cons(Array.init nfix make_body, env), thisbody)
+let unfold_projection env p =
+ let pb = lookup_projection p env in
+ Zproj (pb.proj_npars, pb.proj_arg, p)
(*********************************************************************)
(* A machine that inspects the head of a term until it finds an
@@ -720,10 +696,9 @@ let rec knh info m stk =
| FCast(t,_,_) -> knh info t stk
| FProj (p,c) ->
- if red_set info.i_flags (fCONST (Projection.constant p)) then
- (let pb = lookup_projection p (info.i_env) in
- knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
- :: zupdate m stk))
+ if red_set info.i_flags fDELTA then
+ let s = unfold_projection info.i_env p in
+ knh info c (s :: zupdate m stk)
else (m,stk)
(* cases where knh stops *)
@@ -755,11 +730,11 @@ let rec knr info m stk =
(match get_args n tys f e stk with
Inl e', s -> knit info e' f s
| Inr lam, s -> (lam,s))
- | FFlex(ConstKey kn) when red_set info.i_flags (fCONST (fst kn)) ->
+ | FFlex(ConstKey kn) when red_set info.i_flags fDELTA ->
(match ref_value_cache info (ConstKey kn) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
- | FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
+ | FFlex(VarKey id) when red_set info.i_flags fDELTA ->
(match ref_value_cache info (VarKey id) with
Some v -> kni info v stk
| None -> (set_norm m; (m,stk)))
@@ -822,6 +797,7 @@ type clos_infos = fconstr infos
let infos_env x = x.i_env
let infos_flags x = x.i_flags
+let oracle_of_infos x = x.i_env.env_conv_oracle
let create_clos_infos flgs env =
create (fun _ -> inject) flgs env
diff --git a/checker/closure.mli b/checker/closure.mli
index 02d8b22fae..7bdc21b605 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -24,14 +24,6 @@ val with_stats: 'a Lazy.t -> 'a
Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
-type transparent_state = Id.Pred.t * Cpred.t
-
-val all_opaque : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> Constant.t -> bool
-
(* Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
@@ -42,8 +34,6 @@ module type RedFlagsSig = sig
val fDELTA : red_kind
val fIOTA : red_kind
val fZETA : red_kind
- val fCONST : Constant.t -> red_kind
- val fVAR : Id.t -> red_kind
(* No reduction at all *)
val no_red : reds
@@ -131,6 +121,8 @@ val eta_expand_stack : stack -> stack
val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
(fconstr * stack) -> stack * stack
+val unfold_projection : env -> Projection.t -> stack_member
+
(* To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
@@ -147,6 +139,8 @@ type clos_infos
val create_clos_infos : reds -> env -> clos_infos
val infos_env : clos_infos -> env
val infos_flags : clos_infos -> reds
+val oracle_of_infos : clos_infos -> oracle
+
(* Reduction function *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 884a1ef18c..15b1f0a0c6 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -484,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
let eq_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> true
- | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
- | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
+ | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2
+ | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2
| _ -> false
let eq_wf_paths = Rtree.equal eq_recarg
diff --git a/checker/environ.ml b/checker/environ.ml
index 9db0d60e89..bbd043c8e9 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -21,7 +21,15 @@ type env = {
env_globals : globals;
env_rel_context : rel_context;
env_stratification : stratification;
- env_imports : Cic.vodigest MPmap.t }
+ env_imports : Cic.vodigest MPmap.t;
+ env_conv_oracle : oracle; }
+
+let empty_oracle = {
+ var_opacity = Id.Map.empty;
+ cst_opacity = Cmap.empty;
+ var_trstate = Id.Pred.empty;
+ cst_trstate = Cpred.empty;
+}
let empty_env = {
env_globals =
@@ -34,7 +42,8 @@ let empty_env = {
env_stratification =
{ env_universes = Univ.initial_universes;
env_engagement = PredicativeSet };
- env_imports = MPmap.empty }
+ env_imports = MPmap.empty;
+ env_conv_oracle = empty_oracle }
let engagement env = env.env_stratification.env_engagement
let universes env = env.env_stratification.env_universes
@@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env =
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
+let set_oracle env oracle = { env with env_conv_oracle = oracle }
+
(* Digests *)
let add_digest env dp digest =
@@ -115,7 +126,7 @@ let add_constant kn cs env =
env_constants = new_constants } in
{ env with env_globals = new_globals }
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
(* Constant types *)
@@ -137,18 +148,16 @@ exception NotEvaluableConst of const_evaluation_result
let constant_value env (kn,u) =
let cb = lookup_constant kn env in
- if cb.const_proj = None then
- match cb.const_body with
- | Def l_body ->
- let b = force_constr l_body in
- begin
- match cb.const_universes with
- | Monomorphic_const _ -> b
- | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
- end
- | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
- | Undef _ -> raise (NotEvaluableConst NoBody)
- else raise (NotEvaluableConst IsProj)
+ match cb.const_body with
+ | Def l_body ->
+ let b = force_constr l_body in
+ begin
+ match cb.const_universes with
+ | Monomorphic_const _ -> b
+ | Polymorphic_const _ -> subst_instance_constr u (force_constr l_body)
+ end
+ | OpaqueDef _ -> raise (NotEvaluableConst Opaque)
+ | Undef _ -> raise (NotEvaluableConst NoBody)
(* A global const is evaluable if it is defined and not opaque *)
let evaluable_constant cst env =
diff --git a/checker/environ.mli b/checker/environ.mli
index 6bda838f8a..36e0ea0274 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -18,6 +18,7 @@ type env = {
env_rel_context : rel_context;
env_stratification : stratification;
env_imports : Cic.vodigest MPmap.t;
+ env_conv_oracle : Cic.oracle;
}
val empty_env : env
@@ -25,6 +26,10 @@ val empty_env : env
val engagement : env -> Cic.engagement
val set_engagement : Cic.engagement -> env -> env
+(** Oracle *)
+
+val set_oracle : env -> Cic.oracle -> env
+
(* Digests *)
val add_digest : env -> DirPath.t -> Cic.vodigest -> env
val lookup_digest : env -> DirPath.t -> Cic.vodigest
@@ -47,7 +52,7 @@ val check_constraints : Univ.constraints -> env -> bool
val lookup_constant : Constant.t -> env -> Cic.constant_body
val add_constant : Constant.t -> Cic.constant_body -> env -> env
val constant_type : env -> Constant.t puniverses -> constr Univ.constrained
-type const_evaluation_result = NoBody | Opaque | IsProj
+type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
val constant_value : env -> Constant.t puniverses -> constr
val evaluable_constant : Constant.t -> env -> bool
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 22c8438126..1807ae0ecd 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -502,10 +502,19 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
indlc
in mk_paths (Mrec ind) irecargs
+let prrecarg = function
+ | Norec -> str "Norec"
+ | Mrec (mind,i) ->
+ str "Mrec[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+ | Imbr (mind,i) ->
+ str "Imbr[" ++ MutInd.debug_print mind ++ pr_comma () ++ int i ++ str "]"
+
let check_subtree t1 t2 =
let cmp_labels l1 l2 = l1 == Norec || eq_recarg l1 l2 in
if not (Rtree.equiv eq_recarg cmp_labels t1 t2)
- then failwith "bad recursive trees"
+ then user_err Pp.(str "Bad recursive tree: found " ++ fnl ()
+ ++ Rtree.pp_tree prrecarg t1 ++ fnl () ++ str " when expected " ++ fnl ()
+ ++ Rtree.pp_tree prrecarg t2)
(* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
let check_positivity env_ar mind params nrecp inds =
@@ -555,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
@@ -586,6 +604,8 @@ let check_inductive env kn mib =
Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
in
let env = Environ.push_context ind_ctx env in
+ (** Locally set the oracle for further typechecking *)
+ let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in
(* check mind_record : TODO ? check #constructor = 1 ? *)
(* check mind_finite : always OK *)
(* check mind_ntypes *)
@@ -593,13 +613,13 @@ let check_inductive env kn mib =
user_err Pp.(str "not the right number of packets");
(* check mind_params_ctxt *)
let params = mib.mind_params_ctxt in
- let _ = check_ctxt env params in
+ let _ = check_ctxt env0 params in
(* check mind_nparams *)
if rel_context_nhyps params <> mib.mind_nparams then
user_err Pp.(str "number the right number of parameters");
(* mind_packets *)
(* - check arities *)
- let env_ar = typecheck_arity env params mib.mind_packets in
+ let env_ar = typecheck_arity env0 params mib.mind_packets in
(* - check constructor types *)
Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
(* check the inferred subtyping relation *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 22353ec168..8d426a3c05 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -381,7 +381,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
let check_case_info env indsp ci =
let (mib,mip) = lookup_mind_specif env indsp in
if
- not (eq_ind indsp ci.ci_ind) ||
+ not (eq_ind_chk indsp ci.ci_ind) ||
(mib.mind_nparams <> ci.ci_npar) ||
(mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
(mip.mind_consnrealargs <> ci.ci_cstr_nargs)
@@ -435,20 +435,14 @@ type subterm_spec =
| Dead_code
| Not_subterm
-let eq_recarg r1 r2 = match r1, r2 with
-| Norec, Norec -> true
-| Mrec i1, Mrec i2 -> Names.eq_ind i1 i2
-| Imbr i1, Imbr i2 -> Names.eq_ind i1 i2
-| _ -> false
-
let eq_wf_paths = Rtree.equal eq_recarg
let inter_recarg r1 r2 = match r1, r2 with
| Norec, Norec -> Some r1
| Mrec i1, Mrec i2
| Imbr i1, Imbr i2
-| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None
-| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None
+| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None
| _ -> None
let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec
@@ -544,7 +538,7 @@ let lookup_subterms env ind =
let match_inductive ind ra =
match ra with
- | (Mrec i | Imbr i) -> eq_ind ind i
+ | (Mrec i | Imbr i) -> eq_ind_chk ind i
| Norec -> false
(* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -645,7 +639,7 @@ let get_recargs_approx env tree ind args =
(* When the inferred tree allows it, we consider that we have a potential
nested inductive type *)
begin match dest_recarg tree with
- | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+ | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' ->
build_recargs_nested ienv tree (ind_kn, largs)
| _ -> mk_norec
end
diff --git a/checker/main.mli b/checker/main.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/checker/main.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 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 4357a690ef..7685863eab 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,6 +26,9 @@ let refresh_arity ar =
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ prcon kn);
+ (** Locally set the oracle for further typechecking *)
+ let oracle = env.env_conv_oracle in
+ let env = Environ.set_oracle env cb.const_typing_flags.conv_oracle in
(** [env'] contains De Bruijn universe variables *)
let env' =
match cb.const_universes with
@@ -53,8 +56,12 @@ let check_constant_declaration env kn cb =
conv_leq envty j ty)
| None -> ()
in
- if constant_is_polymorphic cb then add_constant kn cb env
- else add_constant kn cb env'
+ let env =
+ if constant_is_polymorphic cb then add_constant kn cb env
+ else add_constant kn cb env'
+ in
+ (** Reset the value of the oracle *)
+ Environ.set_oracle env oracle
(** {6 Checking modules } *)
diff --git a/checker/print.mli b/checker/print.mli
new file mode 100644
index 0000000000..3b2715de92
--- /dev/null
+++ b/checker/print.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* 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 Cic
+
+val print_pure_constr : constr -> unit
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 9b8eac04cd..2297c90b3f 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
@@ -276,16 +269,29 @@ let in_whnf (t,stk) =
| (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
| FLOCKED -> assert false
-let oracle_order fl1 fl2 =
- match fl1,fl2 with
- ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
- | _, ConstKey _ -> true
- | _ -> false
-
-let unfold_projection infos p c =
- let pb = lookup_projection p (infos_env infos) in
- let s = Zproj (pb.proj_npars, pb.proj_arg, p) in
- (c, s)
+let default_level = Level 0
+
+let get_strategy { var_opacity; cst_opacity } = function
+ | VarKey id ->
+ (try Names.Id.Map.find id var_opacity
+ with Not_found -> default_level)
+ | ConstKey (c, _) ->
+ (try Names.Cmap.find c cst_opacity
+ with Not_found -> default_level)
+ | RelKey _ -> Expand
+
+let oracle_order infos l2r k1 k2 =
+ let o = Closure.oracle_of_infos infos in
+ match get_strategy o k1, get_strategy o k2 with
+ | Expand, Expand -> l2r
+ | Expand, (Opaque | Level _) -> true
+ | (Opaque | Level _), Expand -> false
+ | Opaque, Opaque -> l2r
+ | Level _, Opaque -> true
+ | Opaque, Level _ -> false
+ | Level n1, Level n2 ->
+ if Int.equal n1 n2 then l2r
+ else n1 < n2
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
@@ -339,7 +345,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
with NotConvertible ->
(* else the oracle tells which constant is to be expanded *)
let (app1,app2) =
- if oracle_order fl1 fl2 then
+ if oracle_order infos false fl1 fl2 then
match unfold_reference infos fl1 with
| Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
| None ->
@@ -356,12 +362,12 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
eqappr univ cv_pb infos app1 app2)
| (FProj (p1,c1), _) ->
- let (def1, s1) = unfold_projection infos p1 c1 in
- eqappr univ cv_pb infos (lft1, whd_stack infos def1 (s1 :: v1)) appr2
+ let s1 = unfold_projection (infos_env infos) p1 in
+ eqappr univ cv_pb infos (lft1, whd_stack infos c1 (s1 :: v1)) appr2
| (_, FProj (p2,c2)) ->
- let (def2, s2) = unfold_projection infos p2 c2 in
- eqappr univ cv_pb infos appr1 (lft2, whd_stack infos def2 (s2 :: v2))
+ let s2 = unfold_projection (infos_env infos) p2 in
+ eqappr univ cv_pb infos appr1 (lft2, whd_stack infos c2 (s2 :: v2))
(* other constructors *)
| (FLambda _, FLambda _) ->
diff --git a/checker/univ.ml b/checker/univ.ml
index 4f31318132..46b3ce6808 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -881,14 +881,6 @@ type universe_level_subst = universe_level universe_map
(** A full substitution might involve algebraic universes *)
type universe_subst = universe universe_map
-let level_subst_of f =
- fun l ->
- try let u = f l in
- match Universe.level u with
- | None -> l
- | Some l -> l
- with Not_found -> l
-
module Instance : sig
type t = Level.t array
@@ -1011,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 0eadc6801f..8c0685e0b2 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level
type universe_subst = universe universe_map
type universe_level_subst = universe_level universe_map
-val level_subst_of : universe_subst_fn -> universe_level_subst_fn
-
(** {6 Universe instances} *)
module Instance :
@@ -220,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/validate.ml b/checker/validate.ml
index 8200405878..2624e6d495 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -49,8 +49,6 @@ let (/) (ctx:error_context) s : error_context = s::ctx
exception ValidObjError of string * error_context * Obj.t
let fail ctx o s = raise (ValidObjError(s,ctx,o))
-type func = error_context -> Obj.t -> unit
-
(* Check that object o is a block with tag t *)
let val_tag t ctx o =
if Obj.is_block o && Obj.tag o = t then ()
diff --git a/checker/validate.mli b/checker/validate.mli
new file mode 100644
index 0000000000..7eed692a0b
--- /dev/null
+++ b/checker/validate.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* 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 validate : bool -> Values.value -> 'a -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 5a371164c6..55e1cdb6f7 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli
+MD5 483493b20fe91cc1bea4350a2db2f82d checker/cic.mli
*)
@@ -70,6 +70,8 @@ let v_map vk vd =
let v_hset v = v_map Int (v_set v)
let v_hmap vk vd = v_map Int (v_map vk vd)
+let v_pred v = v_pair v_bool (v_set v)
+
(* lib/future *)
let v_computation f =
Annot ("Future.computation",
@@ -108,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 *)
@@ -199,6 +203,17 @@ let v_lazy_constr =
let v_impredicative_set = v_enum "impr-set" 2
let v_engagement = v_impredicative_set
+let v_conv_level =
+ v_sum "conv_level" 2 [|[|Int|]|]
+
+let v_oracle =
+ v_tuple "oracle" [|
+ v_map v_id v_conv_level;
+ v_hmap v_cst v_conv_level;
+ v_pred v_id;
+ v_pred v_cst;
+ |]
+
let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -213,7 +228,7 @@ let v_projbody =
v_constr|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
@@ -372,22 +387,3 @@ let v_lib =
let v_opaques = Array (v_computation v_constr)
let v_univopaques =
Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
-
-(** Registering dynamic values *)
-
-module IntOrd =
-struct
- type t = int
- let compare (x : t) (y : t) = compare x y
-end
-
-module IntMap = Map.Make(IntOrd)
-
-let dyn_table : value IntMap.t ref = ref IntMap.empty
-
-let register_dyn name t =
- dyn_table := IntMap.add name t !dyn_table
-
-let find_dyn name =
- try IntMap.find name !dyn_table
- with Not_found -> Any
diff --git a/checker/values.mli b/checker/values.mli
new file mode 100644
index 0000000000..aad8fd5f45
--- /dev/null
+++ b/checker/values.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+type value =
+ | Any
+ | Fail of string
+ | Tuple of string * value array
+ | Sum of string * int * value array array
+ | Array of value
+ | List of value
+ | Opt of value
+ | Int
+ | String
+ | Annot of string * value
+ | Dyn
+
+val v_univopaques : value
+val v_libsum : value
+val v_lib : value
+val v_opaques : value
+val v_stm_seg : value
diff --git a/checker/votour.ml b/checker/votour.ml
index 77c9999c42..8cb97a2b1b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -210,7 +210,6 @@ let access_list v o pos =
let access_block o = match Repr.repr o with
| BLOCK (tag, os) -> (tag, os)
| _ -> raise Exit
-let access_int o = match Repr.repr o with INT i -> i | _ -> raise Exit
(** raises Exit if the object has not the expected structure *)
exception Forbidden
@@ -249,8 +248,7 @@ let rec get_children v o pos = match v with
|Dyn ->
begin match Repr.repr o with
| BLOCK (0, [|id; o|]) ->
- let n = access_int id in
- let tpe = find_dyn n in
+ let tpe = Any in
[|(Int, id, 0 :: pos); (tpe, o, 1 :: pos)|]
| _ -> raise Exit
end
@@ -395,7 +393,7 @@ let visit_vo f =
| None -> ()
done
-let main =
+let () =
if not !Sys.interactive then
Arg.parse [] visit_vo
("votour: guided tour of a Coq .vo or .vi file\n"^
diff --git a/checker/votour.mli b/checker/votour.mli
new file mode 100644
index 0000000000..e1555ba2e2
--- /dev/null
+++ b/checker/votour.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 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 12:37:54 +0000