aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/environ.ml3
-rw-r--r--checker/indtypes.ml44
-rw-r--r--checker/inductive.ml14
-rw-r--r--checker/inductive.mli4
-rw-r--r--checker/mod_checking.ml12
-rw-r--r--checker/reduction.ml14
-rw-r--r--checker/subtyping.ml52
-rw-r--r--checker/term.ml34
-rw-r--r--checker/term.mli1
-rw-r--r--checker/univ.ml125
-rw-r--r--checker/univ.mli40
11 files changed, 124 insertions, 219 deletions
diff --git a/checker/environ.ml b/checker/environ.ml
index 11b8ea67cc..d3f393c651 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -122,8 +122,7 @@ type const_evaluation_result = NoBody | Opaque | IsProj
let constraints_of cb u =
match cb.const_universes with
| Monomorphic_const _ -> Univ.Constraint.empty
- | Polymorphic_const ctx ->
- Univ.UContext.constraints (Univ.subst_instance_context u ctx)
+ | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx
let map_regular_arity f = function
| RegularArity a as ar ->
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 92e94c1ab0..22c8438126 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -525,10 +525,10 @@ let check_positivity env_ar mind params nrecp inds =
Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
(* Check arities and constructors *)
-let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity =
+let check_subtyping_arity_constructor env (subst : Univ.Instance.t) (arcn : constr) numparams is_arity =
let numchecked = ref 0 in
let basic_check ev tp =
- if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+ if !numchecked < numparams then () else conv_leq ev tp (Term.subst_instance_constr subst tp);
numchecked := !numchecked + 1
in
let check_typ typ typ_env =
@@ -548,26 +548,27 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
(* Check that the subtyping information inferred for inductive types in the block is correct. *)
(* 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 check_subtyping cumi paramsctxt env inds =
+ let open Univ in
let numparams = rel_context_nhyps paramsctxt in
- let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in
- let other_instnace = Univ.CumulativityInfo.subtyping_other_instance cumi in
- let dosubst = subst_univs_level_constr sbsubst in
- let uctx = Univ.CumulativityInfo.univ_context cumi in
- let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
- let env = Environ.push_context uctx env_ar
- in
- let env = Environ.push_context uctx_other env
- in
- let env = Environ.push_context
- (Univ.CumulativityInfo.subtyp_context cumi) env
- in
+ (** In [env] we already have [ Var(0) ... Var(n-1) |- cst ] available.
+ 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 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 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
| RegularArity { mind_user_arity = 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
+ check_subtyping_arity_constructor env inst full_arity numparams true;
+ Array.iter (fun cnt -> check_subtyping_arity_constructor env inst cnt numparams false) lc
| TemplateArity _ -> ()
) inds
@@ -579,10 +580,10 @@ let check_inductive env kn mib =
(* check mind_constraints: should be consistent with env *)
let ind_ctx =
match mib.mind_universes with
- | Monomorphic_ind ctx -> ctx
- | Polymorphic_ind auctx -> Univ.instantiate_univ_context auctx
+ | Monomorphic_ind _ -> Univ.UContext.empty (** Already in the global environment *)
+ | Polymorphic_ind auctx -> Univ.AUContext.repr auctx
| Cumulative_ind cumi ->
- Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+ Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
in
let env = Environ.push_context ind_ctx env in
(* check mind_record : TODO ? check #constructor = 1 ? *)
@@ -606,8 +607,7 @@ let check_inductive env kn mib =
match mib.mind_universes with
| Monomorphic_ind _ | Polymorphic_ind _ -> ()
| Cumulative_ind acumi ->
- check_subtyping
- (Univ.instantiate_cumulativity_info acumi) params env_ar mib.mind_packets
+ check_subtyping acumi params env_ar mib.mind_packets
in
(* check mind_nparams_rec: positivity condition *)
check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 93ffa329a6..1271a02b0e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -66,20 +66,6 @@ let inductive_is_cumulative mib =
| Polymorphic_ind ctx -> false
| Cumulative_ind cumi -> true
-let inductive_polymorphic_instance mib =
- match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.Instance.empty
- | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
- | Cumulative_ind cumi ->
- Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
-
-let inductive_polymorphic_context mib =
- match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.UContext.empty
- | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
- | Cumulative_ind cumi ->
- Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
-
(************************************************************************)
(* Build the substitution that replaces Rels by the appropriate *)
diff --git a/checker/inductive.mli b/checker/inductive.mli
index 698b8b77c2..8f605935db 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -26,10 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool
val inductive_is_cumulative : mutual_inductive_body -> bool
-val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance
-
-val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context
-
val type_of_inductive : env -> mind_specif puniverses -> constr
(* Return type as quoted by the user *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 15e9ae2951..4948f6008f 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,22 +26,21 @@ let refresh_arity ar =
let check_constant_declaration env kn cb =
Feedback.msg_notice (str " checking cst:" ++ prcon kn);
- let env', u =
+ (** [env'] contains De Bruijn universe variables *)
+ let env' =
match cb.const_universes with
- | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty
+ | Monomorphic_const ctx -> push_context ~strict:true ctx env
| Polymorphic_const auctx ->
- let ctx = Univ.instantiate_univ_context auctx in
- push_context ~strict:false ctx env, Univ.UContext.instance ctx
+ let ctx = Univ.AUContext.repr auctx in
+ push_context ~strict:false ctx env
in
let envty, ty =
match cb.const_type with
RegularArity ty ->
- let ty = subst_instance_constr u ty in
let ty', cu = refresh_arity ty in
let envty = push_context_set cu env' in
let _ = infer_type envty ty' in envty, ty
| TemplateArity(ctxt,par) ->
- assert(Univ.Instance.is_empty u);
let _ = check_ctxt env' ctxt in
check_polymorphic_arity env' ctxt par;
env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt
@@ -49,7 +48,6 @@ let check_constant_declaration env kn cb =
let () =
match body_of_constant cb with
| Some bd ->
- let bd = subst_instance_constr u bd in
(match cb.const_proj with
| None -> let j = infer envty bd in
conv_leq envty j ty
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 93b8b907ca..6d8783d7e5 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -157,25 +157,23 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
else raise NotConvertible
let convert_inductive_instances cv_pb cumi u u' univs =
- let ind_instance =
- Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in
+ let len_instance =
+ Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in
let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
- if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
- (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+ 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.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ 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.UContext.constraints
- (Univ.subst_instance_context comp_subst ind_subtypctx)
+ Univ.AUContext.instantiate comp_subst ind_subtypctx
in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 5fd5510a7f..3097c3a0b9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -81,6 +81,14 @@ let check_conv_error error f env a1 a2 =
with
NotConvertible -> error ()
+let check_polymorphic_instance error env auctx1 auctx2 =
+ if not (Univ.AUContext.size auctx1 == Univ.AUContext.size auctx2) then
+ error ()
+ else if not (Univ.check_subtype (Environ.universes env) auctx2 auctx1) then
+ error ()
+ else
+ Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+
(* for now we do not allow reorderings *)
let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
let kn = MutInd.make2 mp1 l in
@@ -93,19 +101,17 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let mib2 = subst_mind subst2 mib2 in
let check eq f = if not (eq (f mib1) (f mib2)) then error () in
- let u =
- let process inst inst' =
- if Univ.Instance.equal inst inst' then inst else error ()
- in
+ let env, u =
match mib1.mind_universes, mib2.mind_universes with
- | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+ | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
| Polymorphic_ind auctx, Polymorphic_ind auctx' ->
- process
- (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+ let env = check_polymorphic_instance error env auctx auctx' in
+ env, Univ.make_abstract_instance auctx'
| Cumulative_ind cumi, Cumulative_ind cumi' ->
- process
- (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
- (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+ let auctx = Univ.ACumulativityInfo.univ_context cumi in
+ let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
+ let env = check_polymorphic_instance error env auctx auctx' in
+ env, Univ.make_abstract_instance auctx'
| _ -> error ()
in
let eq_projection_body p1 p2 =
@@ -118,7 +124,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
check (eq_constr) (fun x -> snd x.proj_eta);
check (eq_constr) (fun x -> x.proj_body); true
in
- let check_inductive_type env t1 t2 =
+ let check_inductive_type t1 t2 =
(* Due to template polymorphism, the conclusions of
t1 and t2, if in Type, are generated as the least upper bounds
@@ -170,8 +176,8 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* nparams done *)
(* params_ctxt done because part of the inductive types *)
(* Don't check the sort of the type if polymorphic *)
- check_inductive_type env
- (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
+ check_inductive_type
+ (type_of_inductive env ((mib1,p1), u)) (type_of_inductive env ((mib2,p2),u))
in
let check_cons_types i p1 p2 =
Array.iter2 (check_conv conv env)
@@ -309,27 +315,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let c2 = force_constr lc2 in
check_conv conv env c1 c2))
| IndType ((kn,i),mind1) ->
- ignore (CErrors.user_err (Pp.str (
+ CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by an inductive type. Hint: you can rename the " ^
"inductive type and give a definition to map the old name to the new " ^
- "name.")));
- if constant_has_body cb2 then error () ;
- let u = inductive_polymorphic_instance mind1 in
- let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
- let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- check_conv conv_leq env arity1 typ2
- | IndConstr (((kn,i),j) as cstr,mind1) ->
- ignore (CErrors.user_err (Pp.str (
+ "name."))
+ | IndConstr (((kn,i),j),mind1) ->
+ CErrors.user_err (Pp.str (
"The kernel does not recognize yet that a parameter can be " ^
"instantiated by a constructor. Hint: you can rename the " ^
"constructor and give a definition to map the old name to the new " ^
- "name.")));
- if constant_has_body cb2 then error () ;
- let u1 = inductive_polymorphic_instance mind1 in
- let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
- let ty2 = Typeops.type_of_constant_type env cb2.const_type in
- check_conv conv env ty1 ty2
+ "name."))
let rec check_modules env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module None msb1 in
diff --git a/checker/term.ml b/checker/term.ml
index 9bcb15bc72..5995dfcc61 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -447,37 +447,3 @@ let subst_instance_constr subst c =
let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else map_rel_context (fun x -> subst_instance_constr s x) ctx
-
-let subst_univs_level_constr subst c =
- if Univ.is_empty_level_subst subst then c
- else
- let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
- let changed = ref false in
- let rec aux t =
- match t with
- | Const (c, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; Const (c, u'))
- | Ind (i, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; Ind (i, u'))
- | Construct (c, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; Construct (c, u'))
- | Sort (Type u) ->
- let u' = Univ.subst_univs_level_universe subst u in
- if u' == u then t else
- (changed := true; Sort (sort_of_univ u'))
- | _ -> map_constr aux t
- in
- let c' = aux c in
- if !changed then c' else c
diff --git a/checker/term.mli b/checker/term.mli
index ccf5b59e0c..679a56ee45 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -57,4 +57,3 @@ val eq_constr : constr -> constr -> bool
(** Instance substitution for polymorphism. *)
val subst_instance_constr : Univ.universe_instance -> constr -> constr
val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
-val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
diff --git a/checker/univ.ml b/checker/univ.ml
index b434db129e..e3abc436f0 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1075,6 +1075,7 @@ module Instance : sig
val check_eq : t check_function
val length : t -> int
val append : t -> t -> t
+ val of_array : Level.t array -> t
end =
struct
type t = Level.t array
@@ -1157,9 +1158,38 @@ struct
let length = Array.length
let append = Array.append
-
+
+ let of_array i = i
+
end
+(** Substitute instance inst for ctx in csts *)
+
+let subst_instance_level s l =
+ match l.Level.data with
+ | Level.Var n -> s.(n)
+ | _ -> l
+
+let subst_instance_instance s i =
+ Array.smartmap (fun l -> subst_instance_level s l) i
+
+let subst_instance_universe s u =
+ let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
+ let u' = Universe.smartmap f u in
+ if u == u' then u
+ else Universe.sort u'
+
+let subst_instance_constraint s (u,d,v as c) =
+ let u' = subst_instance_level s u in
+ let v' = subst_instance_level s v in
+ if u' == u && v' == v then c
+ else (u',d,v')
+
+let subst_instance_constraints s csts =
+ Constraint.fold
+ (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
+ csts Constraint.empty
+
type universe_instance = Instance.t
type 'a puniverses = 'a * Instance.t
@@ -1175,6 +1205,7 @@ struct
let make x = x
let instance (univs, cst) = univs
let constraints (univs, cst) = cst
+ let size (univs, _) = Instance.length univs
let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
let pr prl (univs, cst as ctx) =
@@ -1184,7 +1215,18 @@ end
type universe_context = UContext.t
-module AUContext = UContext
+module AUContext =
+struct
+ include UContext
+
+ let repr (inst, cst) =
+ (Array.mapi (fun i l -> Level.var i) inst, cst)
+
+ let instantiate inst (u, cst) =
+ assert (Array.length u = Array.length inst);
+ subst_instance_constraints inst cst
+
+end
type abstract_universe_context = AUContext.t
@@ -1192,43 +1234,11 @@ module CumulativityInfo =
struct
type t = universe_context * universe_context
- let make x =
- if (Array.length (UContext.instance (snd x))) =
- (Array.length (UContext.instance (fst x))) * 2 then x
- else anomaly (Pp.str "Invalid subtyping information encountered!")
-
- let empty = (UContext.empty, UContext.empty)
-
- let halve_context ctx =
- let len = Array.length ctx in
- let halflen = len / 2 in
- ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen))
-
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 ctx
-
- let from_universe_context univcst freshunivs =
- let inst = (UContext.instance univcst) in
- assert (Array.length freshunivs = Array.length inst);
- (univcst, UContext.make (Array.append inst freshunivs,
- create_trivial_subtyping inst freshunivs))
-
- let subtyping_other_instance (univcst, subtypcst) =
- let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
-
- 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'
-
end
-type cumulativity_info = CumulativityInfo.t
-
module ACumulativityInfo = CumulativityInfo
type abstract_cumulativity_info = ACumulativityInfo.t
@@ -1242,7 +1252,17 @@ struct
end
type universe_context_set = ContextSet.t
+(** Instance subtyping *)
+let check_subtype univs ctxT ctx =
+ if AUContext.size ctx == AUContext.size ctx then
+ let (inst, cst) = AUContext.repr ctx in
+ let cstT = UContext.constraints (AUContext.repr ctxT) in
+ let push accu v = add_universe v false accu in
+ let univs = Array.fold_left push univs inst in
+ let univs = merge_constraints cstT univs in
+ check_constraints cst univs
+ else false
(** Substitutions. *)
@@ -1263,46 +1283,9 @@ let subst_univs_level_universe subst u =
if u == u' then u
else Universe.sort u'
-(** Substitute instance inst for ctx in csts *)
-
-let subst_instance_level s l =
- match l.Level.data with
- | Level.Var n -> s.(n)
- | _ -> l
-
-let subst_instance_instance s i =
- Array.smartmap (fun l -> subst_instance_level s l) i
-
-let subst_instance_universe s u =
- let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in
- let u' = Universe.smartmap f u in
- if u == u' then u
- else Universe.sort u'
-
-let subst_instance_constraint s (u,d,v as c) =
- let u' = subst_instance_level s u in
- let v' = subst_instance_level s v in
- if u' == u && v' == v then c
- else (u',d,v')
-
-let subst_instance_constraints s csts =
- Constraint.fold
- (fun c csts -> Constraint.add (subst_instance_constraint s c) csts)
- csts Constraint.empty
-
-let subst_instance_context inst (inner_inst, inner_constr) =
- (inner_inst, subst_instance_constraints inst inner_constr)
-
let make_abstract_instance (ctx, _) =
Array.mapi (fun i l -> Level.var i) ctx
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) =
- (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_cumulativity_info (ctx, ctx') =
- (instantiate_univ_context ctx, instantiate_univ_context ctx')
-
(** With level to universe substitutions. *)
type universe_subst_fn = universe_level -> universe
diff --git a/checker/univ.mli b/checker/univ.mli
index 457ccbdfff..7f5aa76260 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,8 @@ sig
(** Create a new universe level from a unique identifier and an associated
module path. *)
+ val var : int -> t
+
val pr : t -> Pp.std_ppcmds
(** Pretty-printing *)
@@ -179,6 +181,8 @@ sig
val length : t -> int
(** Compute the length of the instance *)
+ val of_array : Level.t array -> t
+
val append : t -> t -> t
(** Append two universe instances *)
end
@@ -208,32 +212,14 @@ module AUContext :
sig
type t
- val instance : t -> Instance.t
-
-end
-
-type abstract_universe_context = AUContext.t
-
-module CumulativityInfo :
-sig
- type t
-
- val make : universe_context * universe_context -> t
-
- val empty : t
-
- val univ_context : t -> universe_context
- val subtyp_context : t -> universe_context
-
- val from_universe_context : universe_context -> universe_instance -> t
+ val size : t -> int
- val subtyping_other_instance : t -> universe_instance
-
- val subtyping_susbst : t -> universe_level_subst
+ val instantiate : Instance.t -> t -> Constraint.t
+ val repr : t -> UContext.t
end
-type cumulativity_info = CumulativityInfo.t
+type abstract_universe_context = AUContext.t
module ACumulativityInfo :
sig
@@ -276,18 +262,16 @@ val subst_univs_universe : universe_subst_fn -> universe -> universe
(** Substitution of instances *)
val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
(* val make_instance_subst : universe_instance -> universe_level_subst *)
(* val make_inverse_instance_subst : universe_instance -> universe_level_subst *)
-(** Get the instantiated graph. *)
-val instantiate_univ_context : abstract_universe_context -> universe_context
-val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
-
(** Build the relative instance corresponding to the context *)
val make_abstract_instance : abstract_universe_context -> universe_instance
-
+
+(** Check instance subtyping *)
+val check_subtype : universes -> AUContext.t -> AUContext.t -> bool
+
(** {6 Pretty-printing of universes. } *)
val pr_constraint_type : constraint_type -> Pp.std_ppcmds
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:49:30 +0000