diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 38 | ||||
| -rw-r--r-- | library/lib.mli | 11 |
2 files changed, 37 insertions, 12 deletions
diff --git a/library/lib.ml b/library/lib.ml index 499e2ae21..16dd7fdd0 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -417,8 +417,11 @@ let find_opening_node id = type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t - +type abstr_info = { + abstr_ctx : variable_context; + abstr_subst : Univ.universe_level_subst; + abstr_uctx : Univ.AUContext.t; +} type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t type secentry = @@ -483,8 +486,12 @@ let add_section_replacement f g poly hyps = let inst = Univ.UContext.instance ctx in let subst, ctx = Univ.abstract_universes ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (inst,args) exps, - g (sechyps,subst,ctx) abs)::sl + let info = { + abstr_ctx = sechyps; + abstr_subst = subst; + abstr_uctx = ctx; + } in + sectab := (vars,f (inst,args) exps, g info abs) :: sl let add_section_kn poly kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -502,12 +509,21 @@ let section_segment_of_constant con = let section_segment_of_mutual_inductive kn = Names.Mindmap.find kn (snd (pi3 (List.hd !sectab))) -let variable_section_segment_of_reference = function - | ConstRef con -> pi1 (section_segment_of_constant con) - | IndRef (kn,_) | ConstructRef ((kn,_),_) -> - pi1 (section_segment_of_mutual_inductive kn) - | _ -> [] - +let empty_segment = { + abstr_ctx = []; + abstr_subst = Univ.LMap.empty; + abstr_uctx = Univ.AUContext.empty; +} + +let section_segment_of_reference = function +| ConstRef c -> section_segment_of_constant c +| IndRef (kn,_) | ConstructRef ((kn,_),_) -> + section_segment_of_mutual_inductive kn +| VarRef _ -> empty_segment + +let variable_section_segment_of_reference gr = + (section_segment_of_reference gr).abstr_ctx + let section_instance = function | VarRef id -> let eq = function @@ -654,7 +670,7 @@ let discharge_con cst = let discharge_inductive (kn,i) = (discharge_kn kn,i) -let discharge_abstract_universe_context (_, subst, abs_ctx) auctx = +let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx = let open Univ in let len = LMap.cardinal subst in let rec gen_subst i acc = diff --git a/library/lib.mli b/library/lib.mli index 721e2896f..2f4d0d56f 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -153,13 +153,22 @@ val init : unit -> unit (** {6 Section management for discharge } *) type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list -type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext.t +type abstr_info = private { + abstr_ctx : variable_context; + (** Section variables of this prefix *) + abstr_subst : Univ.universe_level_subst; + (** Abstract substitution: named universes are mapped to De Bruijn indices *) + abstr_uctx : Univ.AUContext.t; + (** Universe quantification, same length as the substitution *) +} val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t val section_segment_of_constant : Names.Constant.t -> abstr_info val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info +val section_segment_of_reference : Globnames.global_reference -> abstr_info + val variable_section_segment_of_reference : Globnames.global_reference -> variable_context val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array |