From 50361dc784c8967e7c4b254102e2cb21cb7e9f9e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 22 Jun 2020 12:55:47 +0200 Subject: Make compute_instance_binders internal to UState --- engine/uState.ml | 17 +++++++++++++++-- engine/univNames.ml | 13 ------------- engine/univNames.mli | 2 -- 3 files changed, 15 insertions(+), 17 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index 25d7638686..ff60a5f9d4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,12 +114,25 @@ let constraints ctx = snd ctx.local let context ctx = ContextSet.to_context ctx.local +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 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 Name (LMap.find lvl revmap) + with Not_found -> Name (name_universe lvl) + in + Array.map map (Instance.to_array inst) + let univ_entry ~poly uctx = let open Entries in if poly then let (binders, _) = uctx.names in let uctx = context uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) binders in Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) @@ -433,7 +446,7 @@ let check_univ_decl ~poly uctx decl = if poly then let (binders, _) = uctx.names in let uctx = universe_context ~names ~extensible uctx in - let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) binders in Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in diff --git a/engine/univNames.ml b/engine/univNames.ml index 6d9095680c..9a66386a21 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -34,19 +34,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -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 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 Name (LMap.find lvl revmap) - with Not_found -> Name (name_universe lvl) - in - Array.map map (Instance.to_array inst) - type univ_name_list = Names.lname list let universe_binders_with_opt_names orig names = diff --git a/engine/univNames.mli b/engine/univNames.mli index 34a18d6b6e..da9ffc3564 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,8 +19,6 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array - type univ_name_list = Names.lname list (** [universe_binders_with_opt_names ref l] -- cgit v1.2.3 From ae1acfefe52937ea7e3a098137df032363051361 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Mar 2020 15:10:32 +0200 Subject: Generate names for anonymous polymorphic universes This should make the univbinders output test less fragile as it depends less on the global counter (still used for universes from section variables). --- engine/uState.ml | 7 +------ engine/univNames.ml | 25 +------------------------ engine/univNames.mli | 9 --------- 3 files changed, 2 insertions(+), 39 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index ff60a5f9d4..d4cb59da26 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,16 +114,11 @@ let constraints ctx = snd ctx.local let context ctx = ContextSet.to_context ctx.local -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 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 Name (LMap.find lvl revmap) - with Not_found -> Name (name_universe lvl) + with Not_found -> Anonymous in Array.map map (Instance.to_array inst) diff --git a/engine/univNames.ml b/engine/univNames.ml index 9a66386a21..2e15558db2 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Names open Univ @@ -30,30 +29,8 @@ let pr_with_global_universes l = (** Local universe names of polymorphic references *) -type universe_binders = Univ.Level.t Names.Id.Map.t +type universe_binders = Level.t Names.Id.Map.t let empty_binders = Id.Map.empty type univ_name_list = Names.lname list - -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 -> - try - List.map2 (fun orig {CAst.v = na} -> - match na with - | Anonymous -> orig - | 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 = 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 da9ffc3564..5f69d199b3 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -20,12 +20,3 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders type univ_name_list = Names.lname list - -(** [universe_binders_with_opt_names ref l] - - If [l] is [Some univs] return the universe binders naming the bound levels - 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 : AUContext.t -> - univ_name_list option -> universe_binders -- cgit v1.2.3