From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:23:15 +0200 Subject: Use type Universes.universe_binders. --- engine/uState.ml | 24 ++++++++++-------------- 1 file changed, 10 insertions(+), 14 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index 01a4798217..123b64314c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -11,20 +11,8 @@ open CErrors open Util open Names -module StringOrd = struct type t = string let compare = String.compare end -module UNameMap = struct +module UNameMap = String.Map - include Map.Make(StringOrd) - - let union s t = - if s == t then s - else - merge (fun k l r -> - match l, r with - | Some _, _ -> l - | _, _ -> r) s t -end - type uinfo = { uname : string option; uloc : Loc.t option; @@ -59,12 +47,20 @@ let is_empty ctx = Univ.ContextSet.is_empty ctx.uctx_local && Univ.LMap.is_empty ctx.uctx_univ_variables +let uname_union s t = + if s == t then s + else + UNameMap.merge (fun k l r -> + match l, r with + | Some _, _ -> l + | _, _ -> r) s t + let union ctx ctx' = if ctx == ctx' then ctx else if is_empty ctx' then ctx else let local = Univ.ContextSet.union ctx.uctx_local ctx'.uctx_local in - let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in + let names = uname_union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in -- cgit v1.2.3 From d437078a4ca82f7ca6d19be5ee9452359724f9a0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:46:30 +0200 Subject: Use Maps and ids for universe binders Before sometimes there were lists and strings. --- engine/uState.ml | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index 123b64314c..498d73fd37 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -11,16 +11,16 @@ open CErrors open Util open Names -module UNameMap = String.Map +module UNameMap = Names.Id.Map type uinfo = { - uname : string option; + uname : Id.t option; uloc : Loc.t option; } (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t; + { uctx_names : Universes.universe_binders * uinfo Univ.LMap.t; uctx_local : Univ.ContextSet.t; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -107,10 +107,12 @@ let add_uctx_loc l loc (names, names_rev) = let of_binders b = let ctx = empty in - let names = - List.fold_left (fun acc (id, l) -> add_uctx_names (Id.to_string id) l acc) - ctx.uctx_names b - in { ctx with uctx_names = names } + let rmap = + UNameMap.fold (fun id l rmap -> + Univ.LMap.add l { uname = Some id; uloc = None } rmap) + b Univ.LMap.empty + in + { ctx with uctx_names = b, rmap } let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v @@ -249,20 +251,20 @@ let constrain_variables diff ctx = let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try str (Option.get (Univ.LMap.find l map_rev).uname) + try Id.print (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> Universes.pr_with_global_universes l type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl -let universe_context ~names ~extensible ctx = - let levels = Univ.ContextSet.levels ctx.uctx_local in +let universe_context ~names ~extensible uctx = + let levels = Univ.ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right (fun (loc,id) (newinst, acc) -> let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + try UNameMap.find id (fst uctx.uctx_names) with Not_found -> user_err ?loc ~hdr:"universe_context" (str"Universe " ++ Id.print id ++ str" is not bound anymore.") @@ -274,23 +276,22 @@ let universe_context ~names ~extensible ctx = let loc = try let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in info.uloc with Not_found -> None in user_err ?loc ~hdr:"universe_context" ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ + Univ.LSet.pr (pr_uctx_level uctx) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) else let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in let inst = Univ.Instance.of_array inst in - let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) in - map, ctx + Univ.ContextSet.constraints uctx.uctx_local) in + fst uctx.uctx_names, ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in -- cgit v1.2.3 From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 21:01:57 +0200 Subject: Separate checking univ_decls and obtaining universe binder names. --- engine/uState.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index 498d73fd37..282acb3d6e 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -114,6 +114,8 @@ let of_binders b = in { ctx with uctx_names = b, rmap } +let universe_binders ctx = fst ctx.uctx_names + let instantiate_variable l b v = try v := Univ.LMap.update l (Some b) !v with Not_found -> assert false @@ -291,7 +293,7 @@ let universe_context ~names ~extensible uctx = let inst = Univ.Instance.of_array inst in let ctx = Univ.UContext.make (inst, Univ.ContextSet.constraints uctx.uctx_local) in - fst uctx.uctx_names, ctx + ctx let check_implication uctx cstrs ctx = let gr = initial_graph uctx in @@ -303,14 +305,14 @@ let check_implication uctx cstrs ctx = let check_univ_decl uctx decl = let open Misctypes in - let pl, ctx = universe_context + let ctx = universe_context ~names:decl.univdecl_instance ~extensible:decl.univdecl_extensible_instance uctx in if not decl.univdecl_extensible_constraints then check_implication uctx decl.univdecl_constraints ctx; - pl, ctx + ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in -- cgit v1.2.3 From 02e6d7f39e3dc2aa8859274bc69b2edf8cc91feb Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 16 Sep 2017 14:05:52 +0200 Subject: restrict_universe_context: do not prune named universes. --- engine/uState.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index 282acb3d6e..ff91493ee5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -315,6 +315,9 @@ let check_univ_decl uctx decl = ctx let restrict ctx vars = + let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) + (fst ctx.uctx_names) vars + in let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } -- cgit v1.2.3 From 34d85e1e899f8a045659ccc53bfd6a1f5104130b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 18 Sep 2017 17:22:24 +0200 Subject: Use Entries.constant_universes_entry more. This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean. --- engine/uState.ml | 107 +++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 76 insertions(+), 31 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index ff91493ee5..dadc004c5f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local 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) + 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) + else Monomorphic_ind_entry (context_set uctx) + let of_context_set ctx = { empty with uctx_local = ctx } let subst ctx = ctx.uctx_univ_variables @@ -260,58 +271,92 @@ let pr_uctx_level uctx = type universe_decl = (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl +let error_unbound_universes left uctx = + let open Univ in + let n = LSet.cardinal left in + let loc = + try + let info = + LMap.find (LSet.choose left) (snd uctx.uctx_names) in + info.uloc + with Not_found -> None + in + user_err ?loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ + LSet.pr (pr_uctx_level uctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + let universe_context ~names ~extensible uctx = - let levels = Univ.ContextSet.levels uctx.uctx_local in + let open Univ in + let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right (fun (loc,id) (newinst, acc) -> let l = try UNameMap.find id (fst uctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Id.print id ++ str" is not bound anymore.") - in (l :: newinst, Univ.LSet.remove l acc)) + with Not_found -> assert false + in (l :: newinst, LSet.remove l acc)) names ([], levels) in - if not extensible && not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in - info.uloc - with Not_found -> None - in - user_err ?loc ~hdr:"universe_context" - ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level uctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) + if not extensible && not (LSet.is_empty left) + then error_unbound_universes left uctx else - let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in let inst = Array.append (Array.of_list newinst) left in - let inst = Univ.Instance.of_array inst in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints uctx.uctx_local) in + let inst = Instance.of_array inst in + let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in ctx -let check_implication uctx cstrs ctx = +let check_universe_context_set ~names ~extensible uctx = + if extensible then () + else + let open Univ in + let left = List.fold_left (fun left (loc,id) -> + let l = + try UNameMap.find id (fst uctx.uctx_names) + with Not_found -> assert false + in LSet.remove l left) + (ContextSet.levels uctx.uctx_local) names + in + if not (LSet.is_empty left) + then error_unbound_universes left uctx + +let check_implication uctx cstrs cstrs' = let gr = initial_graph uctx in let grext = UGraph.merge_constraints cstrs gr in - let cstrs' = Univ.UContext.constraints ctx in if UGraph.check_constraints cstrs' grext then () else CErrors.user_err ~hdr:"check_univ_decl" (str "Universe constraints are not implied by the ones declared.") -let check_univ_decl uctx decl = +let check_mono_univ_decl uctx decl = + let open Misctypes in + let () = + let names = decl.univdecl_instance in + let extensible = decl.univdecl_extensible_instance in + check_universe_context_set ~names ~extensible uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); + uctx.uctx_local + +let check_univ_decl ~poly uctx decl = let open Misctypes in - let ctx = universe_context - ~names:decl.univdecl_instance - ~extensible:decl.univdecl_extensible_instance - uctx + 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) + else + let () = check_universe_context_set ~names ~extensible uctx in + Entries.Monomorphic_const_entry uctx.uctx_local in if not decl.univdecl_extensible_constraints then - check_implication uctx decl.univdecl_constraints ctx; + check_implication uctx + decl.univdecl_constraints + (Univ.ContextSet.constraints uctx.uctx_local); ctx let restrict ctx vars = -- cgit v1.2.3 From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 21 Sep 2017 11:14:11 +0200 Subject: Forbid repeated names in universe binders. --- engine/uState.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'engine/uState.ml') diff --git a/engine/uState.ml b/engine/uState.ml index dadc004c5f..4e30640e46 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -109,6 +109,9 @@ let initial_graph ctx = ctx.uctx_initial_universes let algebraics ctx = ctx.uctx_univ_algebraic let add_uctx_names ?loc s l (names, names_rev) = + if UNameMap.mem s names + then user_err ?loc ~hdr:"add_uctx_names" + Pp.(str "Universe " ++ Names.Id.print s ++ str" already bound."); (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) let add_uctx_loc l loc (names, names_rev) = @@ -573,10 +576,6 @@ let normalize uctx = let universe_of_name uctx s = UNameMap.find s (fst uctx.uctx_names) -let add_universe_name uctx s l = - let names' = add_uctx_names s l uctx.uctx_names in - { uctx with uctx_names = names' } - let update_sigma_env uctx env = let univs = Environ.universes env in let eunivs = -- cgit v1.2.3