diff options
Diffstat (limited to 'checker/univ.ml')
-rw-r--r-- | checker/univ.ml | 44 |
1 files changed, 4 insertions, 40 deletions
diff --git a/checker/univ.ml b/checker/univ.ml index 2cd4252b2..e3abc436f 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,7 +1158,9 @@ struct let length = Array.length let append = Array.append - + + let of_array i = i + end (** Substitute instance inst for ctx in csts *) @@ -1231,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 @@ -1315,13 +1286,6 @@ let subst_univs_level_universe subst u = 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 |