From c73fa639eb0a8eaf4e5121aa600f88f2d4349a0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 10:42:41 +0100 Subject: Using a dedicated type for Lib.abstr_info. --- library/lib.ml | 38 +++++++++++++++++++++++++++----------- library/lib.mli | 11 ++++++++++- 2 files changed, 37 insertions(+), 12 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 499e2ae21f..16dd7fdd01 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 721e2896f7..2f4d0d56ff 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 -- cgit v1.2.3 From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 13 Dec 2017 13:57:10 +0100 Subject: Returning instance instead of substitution in universe context abstraction. This datatype enforces stronger invariants, e.g. that we only have in the substitution codomain a connex interval of variables from 0 to n - 1. --- library/lib.ml | 15 +++++---------- library/lib.mli | 4 ++-- 2 files changed, 7 insertions(+), 12 deletions(-) (limited to 'library') diff --git a/library/lib.ml b/library/lib.ml index 16dd7fdd01..971089c171 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -419,7 +419,7 @@ type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = { abstr_ctx : variable_context; - abstr_subst : Univ.universe_level_subst; + abstr_subst : Univ.Instance.t; abstr_uctx : Univ.AUContext.t; } type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t @@ -511,7 +511,7 @@ let section_segment_of_mutual_inductive kn = let empty_segment = { abstr_ctx = []; - abstr_subst = Univ.LMap.empty; + abstr_subst = Univ.Instance.empty; abstr_uctx = Univ.AUContext.empty; } @@ -672,13 +672,8 @@ let discharge_inductive (kn,i) = 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 = - if i < 0 then acc - else - let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in - gen_subst (pred i) acc - in - let subst = gen_subst (AUContext.size auctx - 1) subst in + let ainst = make_abstract_instance auctx in + let subst = Instance.append subst ainst in + let subst = make_instance_subst subst in let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in subst, AUContext.union abs_ctx auctx diff --git a/library/lib.mli b/library/lib.mli index 2f4d0d56ff..cf75d5f8cf 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -156,8 +156,8 @@ type variable_context = variable_info list 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_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) abstr_uctx : Univ.AUContext.t; (** Universe quantification, same length as the substitution *) } -- cgit v1.2.3