diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 10:42:41 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:19:03 +0100 |
commit | c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c (patch) | |
tree | 995ef76564fb951d0dd84a5834d05bbe27b5d239 /library/lib.ml | |
parent | 2d6e395dead61a49ede6208bc40e16b4b8e68ce4 (diff) |
Using a dedicated type for Lib.abstr_info.
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 38 |
1 files changed, 27 insertions, 11 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 = |