diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 3 | ||||
| -rw-r--r-- | engine/evd.mli | 3 | ||||
| -rw-r--r-- | engine/uState.ml | 42 | ||||
| -rw-r--r-- | engine/uState.mli | 8 | ||||
| -rw-r--r-- | engine/univNames.ml | 66 | ||||
| -rw-r--r-- | engine/univNames.mli | 4 |
6 files changed, 64 insertions, 62 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index b3848e1b5b..6345046431 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -891,6 +891,9 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } +let make_nonalgebraic_variable evd u = + { evd with universes = UState.make_nonalgebraic_variable evd.universes u } + (****************************************) (* Operations on constants *) (****************************************) diff --git a/engine/evd.mli b/engine/evd.mli index be54bebcd7..0a8d1f3287 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -561,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map (** See [UState.make_flexible_variable] *) +val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map +(** See [UState.make_nonalgebraic_variable]. *) + val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/uState.ml b/engine/uState.ml index aa7ec63a6f..5747ae2ad4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local let const_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_const_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_const_entry (nas, uctx) else Monomorphic_const_entry (context_set uctx) (* does not support cumulativity since you need more info *) let ind_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_ind_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_ind_entry (nas, uctx) else Monomorphic_ind_entry (context_set uctx) let of_context_set ctx = { empty with uctx_local = ctx } @@ -140,7 +148,25 @@ let of_binders b = in { ctx with uctx_names = b, rmap } -let universe_binders ctx = fst ctx.uctx_names +let invent_name (named,cnt) u = + let rec aux i = + let na = Id.of_string ("u"^(string_of_int i)) in + if Id.Map.mem na named then aux (i+1) + else Id.Map.add na u named, i+1 + in + aux cnt + +let universe_binders ctx = + let open Univ in + let named, rev = ctx.uctx_names in + let named, _ = LSet.fold (fun u named -> + match LMap.find u rev with + | exception Not_found -> (* not sure if possible *) invent_name named u + | { uname = None } -> invent_name named u + | { uname = Some _ } -> named) + (ContextSet.levels ctx.uctx_local) (named, 0) + in + named let instantiate_variable l b v = try v := Univ.LMap.set l (Some b) !v @@ -394,8 +420,11 @@ let check_univ_decl ~poly uctx decl = let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in - if poly - then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = universe_context ~names ~extensible uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Entries.Polymorphic_const_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in Entries.Monomorphic_const_entry uctx.uctx_local @@ -566,6 +595,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_nonalgebraic_variable ctx u = + { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } + let make_flexible_nonalgebraic ctx = {ctx with uctx_univ_algebraic = Univ.LSet.empty} diff --git a/engine/uState.mli b/engine/uState.mli index 8053a7bf83..ad0cd5c1bb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t Turn the variable [l] flexible, and algebraic if [algebraic] is true and [l] can be. That is if there are no strict upper constraints on [l] and and it does not appear in the instance of any non-algebraic - universe. Otherwise the variable is just made flexible. *) + universe. Otherwise the variable is just made flexible. + + If [l] is already algebraic it will remain so even with [algebraic:false]. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +val make_nonalgebraic_variable : t -> Univ.Level.t -> t +(** Make the level non algebraic. Undefined behaviour on + already-defined algebraics. *) + (** Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations). *) diff --git a/engine/univNames.ml b/engine/univNames.ml index a71f9c5736..1019f8f0c2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,69 +36,24 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" - -let universe_binders_of_global ref : Id.t list = - try - let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> [] - -let cache_ubinder (_,(ref,l)) = - universe_binders_table := GlobRef.Map.add ref l !universe_binders_table - -let subst_ubinder (subst,(ref,l as orig)) = - let ref' = fst (Globnames.subst_global subst ref) in - if ref == ref' then orig else ref', l - let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) Id.of_string_soft (Level.to_string lvl) -let discharge_ubinder (_,(ref,l)) = - (** Expand polymorphic binders with the section context *) - let info = Lib.section_segment_of_reference ref in - let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in - let map lvl = match Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - snd (Libnames.repr_qualid qid) - with Not_found -> name_universe lvl - in - let l = List.map map sec_inst @ l in - Some (ref, l) - -let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj = - let open Libobject in - declare_object { (default_object "universe binder") with - cache_function = cache_ubinder; - load_function = (fun _ x -> cache_ubinder x); - classify_function = (fun x -> Substitute x); - subst_function = subst_ubinder; - discharge_function = discharge_ubinder; - rebuild_function = (fun x -> x); } - -let register_universe_binders ref ubinders = - (** TODO: change the API to register a [Name.t list] instead. This is the last - part of the code that depends on the internal representation of names in - abstract contexts, but removing it requires quite a rework of the - callers. *) - let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in +let compute_instance_binders inst ubinders = let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in let map lvl = - try LMap.find lvl revmap - with Not_found -> name_universe lvl + try Name (LMap.find lvl revmap) + with Not_found -> Name (name_universe lvl) in - let ubinders = Array.map_to_list map (Instance.to_array univs) in - if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) + Array.map map (Instance.to_array inst) type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref names = - let orig = universe_binders_of_global ref in +let universe_binders_with_opt_names orig names = + let orig = AUContext.names orig in + let orig = Array.to_list orig in let udecl = match names with | None -> orig | Some udecl -> @@ -106,11 +61,14 @@ let universe_binders_with_opt_names ref names = List.map2 (fun orig {CAst.v = na} -> match na with | Anonymous -> orig - | Name id -> id) orig udecl + | Name id -> Name id) orig udecl with Invalid_argument _ -> let len = List.length orig in CErrors.user_err ~hdr:"universe_binders_with_opt_names" Pp.(str "Universe instance should have length " ++ int len) in - let fold i acc na = Names.Id.Map.add na (Level.var i) acc in + let fold i acc na = match na with + | Name id -> Names.Id.Map.add id (Level.var i) acc + | Anonymous -> acc + in List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index bd4062ade4..6e68153ac2 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit +val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array type univ_name_list = Names.lname list @@ -29,5 +29,5 @@ type univ_name_list = Names.lname list of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. Otherwise return the bound universe names registered for [ref]. *) -val universe_binders_with_opt_names : Names.GlobRef.t -> +val universe_binders_with_opt_names : AUContext.t -> univ_name_list option -> universe_binders |