diff options
32 files changed, 168 insertions, 130 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 8851ea2b6..14afcc4db 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -1111,6 +1111,8 @@ let create_clos_infos ?(evars=fun _ -> None) flgs env = create (fun _ -> inject) flgs env evars let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env +let env_of_infos infos = infos.i_cache.i_env + let infos_with_reds infos reds = { infos with i_flags = reds } diff --git a/kernel/closure.mli b/kernel/closure.mli index adcf25857..1062d0e61 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -172,6 +172,8 @@ val create_clos_infos : ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle +val env_of_infos : clos_infos -> env + val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 2a4f3a948..aa83864c6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -46,6 +46,8 @@ let empty_env = empty_env let engagement env = env.env_stratification.env_engagement +let type_in_type env = env.env_stratification.env_type_in_type + let is_impredicative_set env = match engagement env with | Some ImpredicativeSet -> true @@ -189,6 +191,10 @@ let set_engagement c env = (* Unsafe *) { env with env_stratification = { env.env_stratification with env_engagement = Some c } } +let set_type_in_type env = + { env with env_stratification = + { env.env_stratification with env_type_in_type = true } } + let push_constraints_to_env (_,univs) env = add_constraints univs env diff --git a/kernel/environ.mli b/kernel/environ.mli index 1523f40d1..7f3fdc536 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -50,6 +50,8 @@ val named_context_val : env -> named_context_val val engagement : env -> engagement option val is_impredicative_set : env -> bool +val type_in_type : env -> bool + (** is the local context empty *) val empty_context : env -> bool @@ -210,6 +212,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env val set_engagement : engagement -> env -> env +val set_type_in_type : env -> env + (** {6 Sets of referred section variables } [global_vars_set env c] returns the list of [id]'s occurring either directly as [Var id] in [c] or indirectly as a section variable diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 5964ed70e..c7701a8b1 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -16,15 +16,15 @@ open Nativecode (** This module implements the conversion test by compiling to OCaml code *) -let rec conv_val pb lvl v1 v2 cu = +let rec conv_val env pb lvl v1 v2 cu = if v1 == v2 then cu else match kind_of_value v1, kind_of_value v2 with | Vaccu k1, Vaccu k2 -> - conv_accu pb lvl k1 k2 cu + conv_accu env pb lvl k1 k2 cu | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in - conv_val CONV (lvl+1) (f1 v) (f2 v) cu + conv_val env CONV (lvl+1) (f1 v) (f2 v) cu | Vconst i1, Vconst i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> @@ -34,29 +34,29 @@ let rec conv_val pb lvl v1 v2 cu = raise NotConvertible; let rec aux lvl max b1 b2 i cu = if Int.equal i max then - conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu + conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu else let cu = - conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu in + conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu | Vfun f1, _ -> - conv_val CONV lvl v1 (fun x -> v2 x) cu + conv_val env CONV lvl v1 (fun x -> v2 x) cu | _, Vfun f2 -> - conv_val CONV lvl (fun x -> v1 x) v2 cu + conv_val env CONV lvl (fun x -> v1 x) v2 cu | _, _ -> raise NotConvertible -and conv_accu pb lvl k1 k2 cu = +and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in let n2 = accu_nargs k2 in if not (Int.equal n1 n2) then raise NotConvertible; if Int.equal n1 0 then - conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu + conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else - let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in - List.fold_right2 (conv_val CONV lvl) (args_of_accu k1) (args_of_accu k2) cu + let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in + List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu -and conv_atom pb lvl a1 a2 cu = +and conv_atom env pb lvl a1 a2 cu = if a1 == a2 then cu else match a1, a2 with @@ -70,18 +70,18 @@ and conv_atom pb lvl a1 a2 cu = if not (eq_constant c1 c2) then raise NotConvertible; cu | Asort s1, Asort s2 -> - check_sort_cmp_universes pb s1 s2 cu; cu + check_sort_cmp_universes env pb s1 s2 cu; cu | Avar id1, Avar id2 -> if not (Id.equal id1 id2) then raise NotConvertible; cu | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; - let cu = conv_accu CONV lvl ac1 ac2 cu in + let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in - if Int.equal len 0 then conv_val CONV lvl p1 p2 cu + if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu else - let cu = conv_val CONV lvl p1 p2 cu in + let cu = conv_val env CONV lvl p1 p2 cu in let max = len - 1 in let rec aux i cu = let tag,arity = tbl.(i) in @@ -89,38 +89,38 @@ and conv_atom pb lvl a1 a2 cu = if Int.equal arity 0 then mk_const tag else mk_block tag (mk_rels_accu lvl arity) in let bi1 = bs1 ci and bi2 = bs2 ci in - if Int.equal i max then conv_val CONV (lvl + arity) bi1 bi2 cu - else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in + if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu + else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in aux 0 cu | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) -> if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible; if f1 == f2 then cu - else conv_fix lvl t1 f1 t2 f2 cu + else conv_fix env lvl t1 f1 t2 f2 cu | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)), (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) -> if not (Int.equal s1 s2) then raise NotConvertible; if f1 == f2 then cu else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible - else conv_fix lvl t1 f1 t2 f2 cu + else conv_fix env lvl t1 f1 t2 f2 cu | Aprod(_,d1,c1), Aprod(_,d2,c2) -> - let cu = conv_val CONV lvl d1 d2 cu in + let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in - conv_val pb (lvl + 1) (d1 v) (d2 v) cu + conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) -and conv_fix lvl t1 f1 t2 f2 cu = +and conv_fix env lvl t1 f1 t2 f2 cu = let len = Array.length f1 in let max = len - 1 in let fargs = mk_rels_accu lvl len in let flvl = lvl + len in let rec aux i cu = - let cu = conv_val CONV lvl t1.(i) t2.(i) cu in + let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in let fi1 = napply f1.(i) fargs in let fi2 = napply f2.(i) fargs in - if Int.equal i max then conv_val CONV flvl fi1 fi2 cu - else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in + if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu + else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in aux 0 cu let native_conv pb sigma env t1 t2 = @@ -144,7 +144,7 @@ let native_conv pb sigma env t1 t2 = let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); (* TODO change 0 when we can have deBruijn *) - ignore(conv_val pb 0 !rt1 !rt2 (Environ.universes env)) + ignore(conv_val env pb 0 !rt1 !rt2 (Environ.universes env)) end | _ -> anomaly (Pp.str "Compilation failure") diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index ba9f30233..a5221c779 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -46,7 +46,8 @@ type globals = { type stratification = { env_universes : universes; - env_engagement : engagement option + env_engagement : engagement option; + env_type_in_type : bool } type val_kind = @@ -92,7 +93,8 @@ let empty_env = { env_nb_rel = 0; env_stratification = { env_universes = initial_universes; - env_engagement = None }; + env_engagement = None; + env_type_in_type = false}; env_conv_oracle = Conv_oracle.empty; retroknowledge = Retroknowledge.initial_retroknowledge } diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 74a5fb1ae..9561333c8 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -33,7 +33,8 @@ type globals = { type stratification = { env_universes : universes; - env_engagement : engagement option + env_engagement : engagement option; + env_type_in_type : bool } type lazy_val diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 31c338dd9..802d2b67b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -177,7 +177,7 @@ let is_cumul = function CUMUL -> true | CONV -> false type 'a universe_compare = { (* Might raise NotConvertible *) - compare : conv_pb -> sorts -> sorts -> 'a -> 'a; + compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -187,8 +187,8 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints -let sort_cmp_universes pb s0 s1 (u, check) = - (check.compare pb s0 s1 u, check) +let sort_cmp_universes env pb s0 s1 (u, check) = + (check.compare env pb s0 s1 u, check) let convert_instances flex u u' (s, check) = (check.compare_instances flex u u' s, check) @@ -310,7 +310,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)"); - sort_cmp_universes cv_pb s1 s2 cuniv + sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -552,7 +552,7 @@ let check_eq univs u u' = let check_leq univs u u' = if not (check_leq univs u u') then raise NotConvertible -let check_sort_cmp_universes pb s0 s1 univs = +let check_sort_cmp_universes env pb s0 s1 univs = match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -566,13 +566,14 @@ let check_sort_cmp_universes pb s0 s1 univs = | CUMUL -> check_leq univs u0 u | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> + | (Type u1, Type u2) -> + if not (type_in_type env) then (match pb with | CUMUL -> check_leq univs u1 u2 | CONV -> check_eq univs u1 u2) -let checked_sort_cmp_universes pb s0 s1 univs = - check_sort_cmp_universes pb s0 s1 univs; univs +let checked_sort_cmp_universes env pb s0 s1 univs = + check_sort_cmp_universes env pb s0 s1 univs; univs let check_convert_instances _flex u u' univs = if Univ.Instance.check_eq univs u u' then univs @@ -593,7 +594,7 @@ let infer_leq (univs, cstrs as cuniv) u u' = let cstrs' = Univ.enforce_leq u u' cstrs in univs, cstrs' -let infer_cmp_universes pb s0 s1 univs = +let infer_cmp_universes env pb s0 s1 univs = match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with @@ -607,10 +608,12 @@ let infer_cmp_universes pb s0 s1 univs = | CUMUL -> infer_leq univs u0 u | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible - | (Type u1, Type u2) -> + | (Type u1, Type u2) -> + if not (type_in_type env) then (match pb with | CUMUL -> infer_leq univs u1 u2 | CONV -> infer_eq univs u1 u2) + else univs let infer_convert_instances flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index cfeafd75c..f0b176104 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -38,7 +38,7 @@ type conv_pb = CONV | CUMUL type 'a universe_compare = { (* Might raise NotConvertible *) - compare : conv_pb -> sorts -> sorts -> 'a -> 'a; + compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: bool (* Instance of a flexible constant? *) -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; } @@ -50,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints val check_sort_cmp_universes : - conv_pb -> sorts -> sorts -> Univ.universes -> unit + env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit (* val sort_cmp : *) (* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 71a6b7a39..f7464013f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -81,7 +81,8 @@ open Declarations These fields could be deduced from [revstruct], but they allow faster name freshness checks. - [univ] and [future_cst] : current and future universe constraints - - [engagement] : are we Set-impredicative ? + - [engagement] : are we Set-impredicative? + - [type_in_type] : does the universe hierarchy collapse? - [imports] : names and digests of Require'd libraries since big-bang. This field will only grow - [loads] : list of libraries Require'd inside the current module. @@ -121,6 +122,7 @@ type safe_environment = univ : Univ.constraints; future_cst : Univ.constraints Future.computation list; engagement : engagement option; + type_in_type : bool; imports : vodigest DPMap.t; loads : (module_path * module_body) list; local_retroknowledge : Retroknowledge.action list} @@ -143,6 +145,7 @@ let empty_environment = future_cst = []; univ = Univ.Constraint.empty; engagement = None; + type_in_type = false; imports = DPMap.empty; loads = []; local_retroknowledge = [] } @@ -179,6 +182,10 @@ let check_engagement env c = Errors.error "Needs option -impredicative-set." | _ -> () +let set_type_in_type senv = + { senv with + env = Environ.set_type_in_type senv.env; + type_in_type = true } (** {6 Stm machinery } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 429597f90..6edea363b 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -97,9 +97,12 @@ val add_constraints : (* (\** Generator of universes *\) *) (* val next_universe : int safe_transformer *) -(** Settin the strongly constructive or classical logical engagement *) +(** Setting the strongly constructive or classical logical engagement *) val set_engagement : Declarations.engagement -> safe_transformer0 +(** Collapsing the type hierarchy *) +val set_type_in_type : safe_transformer0 + (** {6 Interactive module functions } *) val start_module : Label.t -> module_path safe_transformer diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 0e91c7972..976380ede 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -44,25 +44,25 @@ let infos = ref (create_clos_infos betaiotazeta Environ.empty_env) let eq_table_key = Names.eq_table_key eq_constant -let rec conv_val pb k v1 v2 cu = +let rec conv_val env pb k v1 v2 cu = if v1 == v2 then cu - else conv_whd pb k (whd_val v1) (whd_val v2) cu + else conv_whd env pb k (whd_val v1) (whd_val v2) cu -and conv_whd pb k whd1 whd2 cu = +and conv_whd env pb k whd1 whd2 cu = match whd1, whd2 with - | Vsort s1, Vsort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu + | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu | Vprod p1, Vprod p2 -> - let cu = conv_val CONV k (dom p1) (dom p2) cu in - conv_fun pb k (codom p1) (codom p2) cu - | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu - | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu + let cu = conv_val env CONV k (dom p1) (dom p2) cu in + conv_fun env pb k (codom p1) (codom p2) cu + | Vfun f1, Vfun f2 -> conv_fun env CONV k f1 f2 cu + | Vfix (f1,None), Vfix (f2,None) -> conv_fix env k f1 f2 cu | Vfix (f1,Some args1), Vfix(f2,Some args2) -> if nargs args1 <> nargs args2 then raise NotConvertible - else conv_arguments k args1 args2 (conv_fix k f1 f2 cu) - | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu + else conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu) + | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix env k cf1 cf2 cu | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) -> if nargs args1 <> nargs args2 then raise NotConvertible - else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu) + else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu) | Vconstr_const i1, Vconstr_const i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Vconstr_block b1, Vconstr_block b2 -> @@ -70,103 +70,103 @@ and conv_whd pb k whd1 whd2 cu = if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then let rcu = ref cu in for i = 0 to sz - 1 do - rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu + rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu done; !rcu else raise NotConvertible | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> - conv_atom pb k a1 stk1 a2 stk2 cu + conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> - conv_val CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu + conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu | _, Vatom_stk(Aiddef(_,v),stk) -> - conv_whd pb k whd1 (force_whd v stk) cu + conv_whd env pb k whd1 (force_whd v stk) cu | Vatom_stk(Aiddef(_,v),stk), _ -> - conv_whd pb k (force_whd v stk) whd2 cu + conv_whd env pb k (force_whd v stk) whd2 cu | _, _ -> raise NotConvertible -and conv_atom pb k a1 stk1 a2 stk2 cu = +and conv_atom env pb k a1 stk1 a2 stk2 cu = match a1, a2 with | Aind (kn1,i1), Aind(kn2,i2) -> if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 then - conv_stack k stk1 stk2 cu + conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then - conv_stack k stk1 stk2 cu + conv_stack env k stk1 stk2 cu else raise NotConvertible | Aiddef(ik1,v1), Aiddef(ik2,v2) -> begin try if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then - conv_stack k stk1 stk2 cu + conv_stack env k stk1 stk2 cu else raise NotConvertible with NotConvertible -> if oracle_order (oracle_of_infos !infos) false ik1 ik2 then - conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu - else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu + conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu + else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu end | Aiddef(ik1,v1), _ -> - conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu + conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu | _, Aiddef(ik2,v2) -> - conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu + conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu | _, _ -> raise NotConvertible -and conv_stack k stk1 stk2 cu = +and conv_stack env k stk1 stk2 cu = match stk1, stk2 with | [], [] -> cu | Zapp args1 :: stk1, Zapp args2 :: stk2 -> - conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu) + conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu) | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 -> - conv_stack k stk1 stk2 - (conv_arguments k args1 args2 (conv_fix k f1 f2 cu)) + conv_stack env k stk1 stk2 + (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)) | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 -> if check_switch sw1 sw2 then let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in - let rcu = ref (conv_val CONV k vt1 vt2 cu) in + let rcu = ref (conv_val env CONV k vt1 vt2 cu) in let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in for i = 0 to Array.length b1 - 1 do rcu := - conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu + conv_val env CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu done; - conv_stack k stk1 stk2 !rcu + conv_stack env k stk1 stk2 !rcu else raise NotConvertible | _, _ -> raise NotConvertible -and conv_fun pb k f1 f2 cu = +and conv_fun env pb k f1 f2 cu = if f1 == f2 then cu else let arity,b1,b2 = decompose_vfun2 k f1 f2 in - conv_val pb (k+arity) b1 b2 cu + conv_val env pb (k+arity) b1 b2 cu -and conv_fix k f1 f2 cu = +and conv_fix env k f1 f2 cu = if f1 == f2 then cu else if check_fix f1 f2 then let bf1, tf1 = reduce_fix k f1 in let bf2, tf2 = reduce_fix k f2 in - let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in - conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu + let cu = conv_vect (conv_val env CONV k) tf1 tf2 cu in + conv_vect (conv_fun env CONV (k + Array.length tf1)) bf1 bf2 cu else raise NotConvertible -and conv_cofix k cf1 cf2 cu = +and conv_cofix env k cf1 cf2 cu = if cf1 == cf2 then cu else if check_cofix cf1 cf2 then let bcf1, tcf1 = reduce_cofix k cf1 in let bcf2, tcf2 = reduce_cofix k cf2 in - let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in - conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu + let cu = conv_vect (conv_val env CONV k) tcf1 tcf2 cu in + conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu else raise NotConvertible -and conv_arguments k args1 args2 cu = +and conv_arguments env k args1 args2 cu = if args1 == args2 then cu else let n = nargs args1 in if Int.equal n (nargs args2) then let rcu = ref cu in for i = 0 to n - 1 do - rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu + rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu done; !rcu else raise NotConvertible @@ -178,7 +178,7 @@ let rec eq_puniverses f (x,l1) (y,l2) cu = and conv_universes l1 l2 cu = if Univ.Instance.equal l1 l2 then cu else raise NotConvertible -let rec conv_eq pb t1 t2 cu = +let rec conv_eq env pb t1 t2 cu = if t1 == t2 then cu else match kind_of_term t1, kind_of_term t2 with @@ -188,55 +188,55 @@ let rec conv_eq pb t1 t2 cu = if Int.equal m1 m2 then cu else raise NotConvertible | Var id1, Var id2 -> if Id.equal id1 id2 then cu else raise NotConvertible - | Sort s1, Sort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu - | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu - | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu + | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu + | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu + | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu | Prod (_,t1,c1), Prod (_,t2,c2) -> - conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu) - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu + conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu) + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> - conv_eq pb c1 c2 (conv_eq CONV b1 b2 cu) + conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu) | App (c1,l1), App (c2,l2) -> - conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu) + conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu) | Evar (e1,l1), Evar (e2,l2) -> - if Evar.equal e1 e2 then conv_eq_vect l1 l2 cu + if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu else raise NotConvertible | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu | Proj (p1,c1), Proj (p2,c2) -> - if eq_constant p1 p2 then conv_eq pb c1 c2 cu else raise NotConvertible + if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible | Ind c1, Ind c2 -> eq_puniverses eq_ind c1 c2 cu | Construct c1, Construct c2 -> eq_puniverses eq_constructor c1 c2 cu | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - let pcu = conv_eq CONV p1 p2 cu in - let ccu = conv_eq CONV c1 c2 pcu in - conv_eq_vect bl1 bl2 ccu + let pcu = conv_eq env CONV p1 p2 cu in + let ccu = conv_eq env CONV c1 c2 pcu in + conv_eq_vect env bl1 bl2 ccu | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> - if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu) + if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu) else raise NotConvertible | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - if Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu) + if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu) else raise NotConvertible | _ -> raise NotConvertible -and conv_eq_vect vt1 vt2 cu = +and conv_eq_vect env vt1 vt2 cu = let len = Array.length vt1 in if Int.equal len (Array.length vt2) then let rcu = ref cu in for i = 0 to len-1 do - rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu + rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu done; !rcu else raise NotConvertible let vconv pb env t1 t2 = infos := create_clos_infos betaiotazeta env; let _cu = - try conv_eq pb t1 t2 (universes env) + try conv_eq env pb t1 t2 (universes env) with NotConvertible -> let v1 = val_of_constr env t1 in let v2 = val_of_constr env t2 in - let cu = conv_val pb (nb_rel env) v1 v2 (universes env) in + let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in cu in () diff --git a/library/global.ml b/library/global.ml index adfb7cafe..80238d8e2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,6 +77,7 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) +let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) diff --git a/library/global.mli b/library/global.mli index 9e47c16ff..7dcfdbd3a 100644 --- a/library/global.mli +++ b/library/global.mli @@ -27,6 +27,7 @@ val named_context : unit -> Context.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit +val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 567078f85..726e64e81 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1733,7 +1733,7 @@ let build_inversion_problem loc env sigma tms t = (* let sigma, s = Evd.new_sort_variable univ_flexible sigma in *) let s' = Retyping.get_sort_of env sigma t in let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in - let sigma = Evd.set_leq_sort sigma s' s in + let sigma = Evd.set_leq_sort env sigma s' s in let evdref = ref sigma in (* let ty = evd_comb1 (refresh_universes false) evdref ty in *) let pb = diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index a1279c1f2..6a48d84ed 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -403,7 +403,7 @@ let inh_coerce_to_sort loc env evd j = match kind_of_term typ with | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s }) | Evar ev when not (is_defined evd (fst ev)) -> - let (evd',s) = define_evar_as_sort evd ev in + let (evd',s) = define_evar_as_sort env evd ev in (evd',{ utj_val = j.uj_val; utj_type = s }) | _ -> inh_tosort_force loc env evd j diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index d125a799b..47955e8e0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -679,7 +679,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let evd' = if pbty == CONV then Evd.set_eq_sort evd s1 s2 - else Evd.set_leq_sort evd s1 s2 + else Evd.set_leq_sort env evd s1 s2 in Success evd' with Univ.UniverseInconsistency p -> UnifFailure (evd,UnifUnivInconsistency p) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 631438ddf..f32238ee7 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -59,8 +59,8 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in let s' = evd_comb0 (new_sort_variable status) evdref in let evd = - if dir then set_leq_sort !evdref s' s - else set_leq_sort !evdref s s' + if dir then set_leq_sort env !evdref s' s + else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> @@ -1154,7 +1154,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar ~src:evi.evar_source ~filter:evi.evar_filter ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) in - let evd = Evd.set_leq_sort (Evd.set_leq_sort evd k i) k j in + let evd = Evd.set_leq_sort env (Evd.set_leq_sort env evd k i) k j in let evd = solve_evar_evar ~force f g env evd (Some false) (ev3,args1) ev1 in f env evd pbty ev2 (whd_evar evd (mkEvar (ev3,args1))) with Reduction.NotArity -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index ddc1ece96..d9e9ac8f9 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -716,7 +716,7 @@ let define_pure_evar_as_product evd evk = let evd3, (rng, srng) = new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in - let evd3 = Evd.set_leq_sort evd3 (Type prods) s in + let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng in let prod = mkProd (Name id, dom, subst_var id rng) in @@ -780,12 +780,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function (* Refining an evar to a sort *) -let define_evar_as_sort evd (ev,args) = +let define_evar_as_sort env evd (ev,args) = let evd, u = new_univ_variable univ_rigid evd in let evi = Evd.find_undefined evd ev in let s = Type u in let evd' = Evd.define ev (mkSort s) evd in - Evd.set_leq_sort evd' (Type (Univ.super u)) (destSort evi.evar_concl), s + Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s (* We don't try to guess in which sort the type should be defined, since any type has type Type. May cause some trouble, but not so far... *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 081c41560..b90a78434 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -92,7 +92,7 @@ val check_evars : env -> evar_map -> evar_map -> constr -> unit val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types -val define_evar_as_sort : evar_map -> existential -> evar_map * sorts +val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** Instantiate an evar by as many lambda's as needed so that its arguments are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 813a21229..c4bf366ac 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1193,7 +1193,7 @@ let set_eq_instances ?(flex=false) d u1 u2 = add_universe_constraints d (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty) -let set_leq_sort evd s1 s2 = +let set_leq_sort env evd s1 s2 = let s1 = normalize_sort evd s1 and s2 = normalize_sort evd s2 in match is_eq_sort s1 s2 with @@ -1205,7 +1205,9 @@ let set_leq_sort evd s1 s2 = (* else if Univ.is_type0m_univ u2 then *) (* raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *) (* else *) + if not (type_in_type env) then add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2)) + else evd let check_eq evd s s' = Univ.check_eq evd.universes.uctx_universes s s' diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 12a166e66..be8ca7cd5 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -273,8 +273,6 @@ val drop_side_effects : evar_map -> evar_map point. This section defines the relevant manipulation functions. *) val whd_sort_variable : evar_map -> constr -> constr -val set_leq_sort : evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : evar_map -> sorts -> sorts -> evar_map exception UniversesDiffer @@ -462,7 +460,7 @@ val whd_sort_variable : evar_map -> constr -> constr val normalize_universe : evar_map -> Univ.universe -> Univ.universe val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance -val set_leq_sort : evar_map -> sorts -> sorts -> evar_map +val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map val set_eq_sort : evar_map -> sorts -> sorts -> evar_map val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0cbfa7597..9f460d08f 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -517,7 +517,7 @@ let weaken_sort_scheme env evd set sort npars term ty = | Prod (n,t,c) -> if Int.equal np 0 then let osort, t' = change_sort_arity sort t in - evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) !evdref sort osort; + evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort env) !evdref sort osort; mkProd (n, t', c), mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1))) else diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 4b6107c4e..24bf7cbc0 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -557,7 +557,7 @@ let rec instantiate_universes env evdref scl is = function 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 evm s (Sorts.sort_of_univ u) in + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in evdref := evm; s in (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 28ab88526..ad6a79863 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -953,7 +953,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function match kind_of_term (whd_betadeltaiota env sigma t) with | Sort s -> s | Evar ev when is_Type (existential_type sigma ev) -> - evd_comb1 (define_evar_as_sort) evdref ev + evd_comb1 (define_evar_as_sort env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type") in { utj_val = v; diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 025725934..10f2bfd5b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1233,10 +1233,10 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y | Univ.UniverseInconsistency _ -> false | e when is_anomaly e -> error "Conversion test raised an anomaly" -let sigma_compare_sorts pb s0 s1 sigma = +let sigma_compare_sorts env pb s0 s1 sigma = match pb with | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1 - | Reduction.CUMUL -> Evd.set_leq_sort sigma s0 s1 + | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 let sigma_compare_instances flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index aedb41037..6672c7fa7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -250,7 +250,7 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val sort_cmp : conv_pb -> sorts -> sorts -> universes -> unit +val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit val is_conv : env -> evar_map -> constr -> constr -> bool val is_conv_leq : env -> evar_map -> constr -> constr -> bool diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1485b7701..eafc5da9a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -38,7 +38,7 @@ let e_type_judgment env evdref j = match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | Evar ev -> - let (evd,s) = Evarutil.define_evar_as_sort !evdref ev in + let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in evdref := evd; { utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 124faf05b..b07bf4f92 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -588,7 +588,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag (try let sigma' = if pb == CUMUL - then Evd.set_leq_sort sigma s1 s2 + then Evd.set_leq_sort env sigma s1 s2 else Evd.set_eq_sort sigma s1 s2 in (sigma', metasubst, evarsubst) with e when Errors.noncritical e -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 74122d104..95cfd73a0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -434,7 +434,7 @@ let inductive_levels env evdref poly arities inds = (** Indices contribute. *) if Indtypes.is_indices_matter () && List.length ctx > 0 then ( let ilev = sign_level env !evdref ctx in - Evd.set_leq_sort evd (Type ilev) du) + Evd.set_leq_sort env evd (Type ilev) du) else evd in (** Constructors contribute. *) @@ -444,14 +444,14 @@ let inductive_levels env evdref poly arities inds = raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType) else evd else - Evd.set_leq_sort evd (Type cu) du + Evd.set_leq_sort env evd (Type cu) du in let evd = if len >= 2 && Univ.is_type0m_univ cu then (** "Polymorphic" type constraint and more than one constructor, should not land in Prop. Add constraint only if it would land in Prop directly (no informative arguments as well). *) - Evd.set_leq_sort evd (Prop Pos) du + Evd.set_leq_sort env evd (Prop Pos) du else evd in evd) !evdref (Array.to_list levels') destarities sizes diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c310986c6..3eee9658e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -70,6 +70,10 @@ let set_engagement c = engagement := Some c let engage () = match !engagement with Some c -> Global.set_engagement c | None -> () +let type_in_type = ref false +let set_type_in_type () = type_in_type := true +let set_hierarchy () = if !type_in_type then Global.set_type_in_type () + let set_batch_mode () = batch_mode := true let toplevel_default_name = DirPath.make [Id.of_string "Top"] @@ -430,6 +434,7 @@ let parse_args arglist = |"-quiet"|"-silent" -> Flags.make_silent true |"-quick" -> Flags.compilation_mode := BuildVi |"-time" -> Flags.time := true + |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) |"-verbose-compat-notations" -> verb_compat_ntn := true @@ -494,6 +499,7 @@ let init arglist = Mltop.init_known_plugins (); set_vm_opt (); engage (); + set_hierarchy (); (* Be careful to set these variables after the inputstate *) Syntax_def.set_verbose_compat_notations !verb_compat_ntn; Syntax_def.set_compat_notations (not !no_compat_ntn); diff --git a/toplevel/record.ml b/toplevel/record.ml index ebaa6a911..d23338930 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -126,7 +126,7 @@ let typecheck_params_and_fields def id t ps nots fs = if Sorts.is_prop aritysort || (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then evars - else Evd.set_leq_sort evars (Type univ) aritysort + else Evd.set_leq_sort env_ar evars (Type univ) aritysort in let evars, nf = Evarutil.nf_evars_and_universes evars in let newps = map_rel_context nf newps in |