diff options
| -rw-r--r-- | engine/evd.ml | 42 | ||||
| -rw-r--r-- | engine/evd.mli | 20 | ||||
| -rw-r--r-- | engine/sigma.ml | 32 | ||||
| -rw-r--r-- | engine/sigma.mli | 24 | ||||
| -rw-r--r-- | engine/uState.ml | 49 | ||||
| -rw-r--r-- | engine/uState.mli | 4 |
6 files changed, 98 insertions, 73 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index f751f4d92..b6849f7ff 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -781,25 +781,25 @@ let restrict_universe_context evd vars = let universe_subst evd = UState.subst evd.universes -let merge_context_set ?(sideff=false) rigid evd ctx' = - {evd with universes = UState.merge sideff rigid evd.universes ctx'} +let merge_context_set ?loc ?(sideff=false) rigid evd ctx' = + {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'} let merge_universe_subst evd subst = {evd with universes = UState.merge_subst evd.universes subst } -let with_context_set rigid d (a, ctx) = - (merge_context_set rigid d ctx, a) +let with_context_set ?loc rigid d (a, ctx) = + (merge_context_set ?loc rigid d ctx, a) -let new_univ_level_variable ?name ?(predicative=true) rigid evd = - let uctx', u = UState.new_univ_variable rigid name evd.universes in +let new_univ_level_variable ?loc ?name ?(predicative=true) rigid evd = + let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?name ?(predicative=true) rigid evd = - let uctx', u = UState.new_univ_variable rigid name evd.universes in +let new_univ_variable ?loc ?name ?(predicative=true) rigid evd = + let uctx', u = UState.new_univ_variable ?loc rigid name evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name ?(predicative=true) rigid d = - let (d', u) = new_univ_variable rigid ?name ~predicative d in +let new_sort_variable ?loc ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable ?loc rigid ?name ~predicative d in (d', Type u) let add_global_univ d u = @@ -815,27 +815,27 @@ let make_evar_universe_context e l = | Some us -> List.fold_left (fun uctx (loc,id) -> - fst (UState.new_univ_variable univ_rigid (Some (Id.to_string id)) uctx)) + fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx)) uctx us (****************************************) (* Operations on constants *) (****************************************) -let fresh_sort_in_family ?(rigid=univ_flexible) env evd s = - with_context_set rigid evd (Universes.fresh_sort_in_family env s) +let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = + with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s) -let fresh_constant_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constant_instance env c) +let fresh_constant_instance ?loc env evd c = + with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c) -let fresh_inductive_instance env evd i = - with_context_set univ_flexible evd (Universes.fresh_inductive_instance env i) +let fresh_inductive_instance ?loc env evd i = + with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i) -let fresh_constructor_instance env evd c = - with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c) +let fresh_constructor_instance ?loc env evd c = + with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c) -let fresh_global ?(rigid=univ_flexible) ?names env evd gr = - with_context_set rigid evd (Universes.fresh_global_instance ?names env gr) +let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = + with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr) let whd_sort_variable evd t = t diff --git a/engine/evd.mli b/engine/evd.mli index a9ca9a740..3ae6e586c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -504,9 +504,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -541,10 +541,10 @@ val universes : evar_map -> UGraph.t val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map -val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a +val with_context_set : ?loc:Loc.t -> rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context @@ -559,12 +559,12 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts +val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_map * pconstant +val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive +val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** diff --git a/engine/sigma.ml b/engine/sigma.ml index c25aac0c1..c7b0bb5a5 100644 --- a/engine/sigma.ml +++ b/engine/sigma.ml @@ -36,36 +36,36 @@ let new_evar sigma ?naming info = let define evk c sigma = Sigma ((), Evd.define evk c sigma, ()) -let new_univ_level_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_level_variable ?name ?predicative rigid sigma in +let new_univ_level_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_level_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_univ_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_univ_variable ?name ?predicative rigid sigma in +let new_univ_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_univ_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let new_sort_variable ?name ?predicative rigid sigma = - let (sigma, u) = Evd.new_sort_variable ?name ?predicative rigid sigma in +let new_sort_variable ?loc ?name ?predicative rigid sigma = + let (sigma, u) = Evd.new_sort_variable ?loc ?name ?predicative rigid sigma in Sigma (u, sigma, ()) -let fresh_sort_in_family ?rigid env sigma s = - let (sigma, s) = Evd.fresh_sort_in_family ?rigid env sigma s in +let fresh_sort_in_family ?loc ?rigid env sigma s = + let (sigma, s) = Evd.fresh_sort_in_family ?loc ?rigid env sigma s in Sigma (s, sigma, ()) -let fresh_constant_instance env sigma cst = - let (sigma, cst) = Evd.fresh_constant_instance env sigma cst in +let fresh_constant_instance ?loc env sigma cst = + let (sigma, cst) = Evd.fresh_constant_instance ?loc env sigma cst in Sigma (cst, sigma, ()) -let fresh_inductive_instance env sigma ind = - let (sigma, ind) = Evd.fresh_inductive_instance env sigma ind in +let fresh_inductive_instance ?loc env sigma ind = + let (sigma, ind) = Evd.fresh_inductive_instance ?loc env sigma ind in Sigma (ind, sigma, ()) -let fresh_constructor_instance env sigma pc = - let (sigma, c) = Evd.fresh_constructor_instance env sigma pc in +let fresh_constructor_instance ?loc env sigma pc = + let (sigma, c) = Evd.fresh_constructor_instance ?loc env sigma pc in Sigma (c, sigma, ()) -let fresh_global ?rigid ?names env sigma r = - let (sigma, c) = Evd.fresh_global ?rigid ?names env sigma r in +let fresh_global ?loc ?rigid ?names env sigma r = + let (sigma, c) = Evd.fresh_global ?loc ?rigid ?names env sigma r in Sigma (c, sigma, ()) (** Run *) diff --git a/engine/sigma.mli b/engine/sigma.mli index d7ae2e4ac..643bea403 100644 --- a/engine/sigma.mli +++ b/engine/sigma.mli @@ -66,23 +66,23 @@ val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma (** Polymorphic universes *) -val new_univ_level_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe_level, 'r) sigma -val new_univ_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Univ.universe, 'r) sigma -val new_sort_variable : ?name:string -> ?predicative:bool -> Evd.rigid -> - 'r t -> (Sorts.t, 'r) sigma - -val fresh_sort_in_family : ?rigid:Evd.rigid -> Environ.env -> +val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma +val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma +val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> + Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma + +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env -> 'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma val fresh_constant_instance : - Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma + ?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma val fresh_inductive_instance : - Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma -val fresh_constructor_instance : Environ.env -> 'r t -> constructor -> + ?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma +val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor -> (pconstructor, 'r) sigma -val fresh_global : ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> +val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env -> 'r t -> Globnames.global_reference -> (constr, 'r) sigma (** FILLME *) diff --git a/engine/uState.ml b/engine/uState.ml index 75c03bc89..8aa9a61ab 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -25,9 +25,14 @@ module UNameMap = struct | _, _ -> r) s t end +type uinfo = { + uname : string option; + uloc : Loc.t option; +} + (* 2nd part used to check consistency on the fly. *) type t = - { uctx_names : Univ.Level.t UNameMap.t * string Univ.LMap.t; + { uctx_names : Univ.Level.t UNameMap.t * uinfo Univ.LMap.t; uctx_local : Univ.universe_context_set; (** The local context of variables *) uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) @@ -104,8 +109,13 @@ let constrain_variables diff ctx = with Not_found | Option.IsNone -> cstrs) diff Univ.Constraint.empty -let add_uctx_names s l (names, names_rev) = - (UNameMap.add s l names, Univ.LMap.add l s names_rev) +let add_uctx_names ?loc s l (names, names_rev) = + (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) = + match loc with + | None -> (names, names_rev) + | Some _ -> (names, Univ.LMap.add l { uname = None; uloc = loc } names_rev) let of_binders b = let ctx = empty in @@ -230,8 +240,8 @@ let add_universe_constraints ctx cstrs = let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try str(Univ.LMap.find l map_rev) - with Not_found -> + try str (Option.get (Univ.LMap.find l map_rev).uname) + with Not_found | Option.IsNone -> Universes.pr_with_global_universes l let universe_context ?names ctx = @@ -252,10 +262,14 @@ let universe_context ?names ctx = in if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in - errorlabstrm "universe_context" + let loc = + let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in + try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost + in + user_err_loc (loc, "universe_context", (str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.") + spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) else let inst = Univ.Instance.of_array (Array.of_list newinst) in let ctx = Univ.UContext.make (inst, @@ -274,7 +288,7 @@ let univ_rigid = UnivRigid let univ_flexible = UnivFlexible false let univ_flexible_alg = UnivFlexible true -let merge sideff rigid uctx ctx' = +let merge ?loc sideff rigid uctx ctx' = let open Univ in let levels = ContextSet.levels ctx' in let uctx = if sideff then uctx else @@ -301,10 +315,21 @@ let merge sideff rigid uctx ctx' = with UGraph.AlreadyDeclared when sideff -> g) levels g in + let uctx_names = + let fold u accu = + let modify _ info = match info.uloc with + | None -> { info with uloc = loc } + | Some _ -> info + in + try LMap.modify u modify accu + with Not_found -> LMap.add u { uname = None; uloc = loc } accu + in + (fst uctx.uctx_names, LSet.fold fold levels (snd uctx.uctx_names)) + in let initial = declare uctx.uctx_initial_universes in let univs = declare uctx.uctx_universes in let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_local; uctx_universes; uctx_initial_universes = initial } + { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial } let merge_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } @@ -313,7 +338,7 @@ let emit_side_effects eff u = let uctxs = Safe_typing.universes_of_private eff in List.fold_left (merge true univ_rigid) u uctxs -let new_univ_variable rigid name +let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in let ctx' = Univ.ContextSet.add_universe u ctx in @@ -328,8 +353,8 @@ let new_univ_variable rigid name in let names = match name with - | Some n -> add_uctx_names n u uctx.uctx_names - | None -> uctx.uctx_names + | Some n -> add_uctx_names ?loc n u uctx.uctx_names + | None -> add_uctx_loc u loc uctx.uctx_names in let initial = UGraph.add_universe u false uctx.uctx_initial_universes diff --git a/engine/uState.mli b/engine/uState.mli index 9dc96622e..c5c454020 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -84,11 +84,11 @@ val univ_rigid : rigid val univ_flexible : rigid val univ_flexible_alg : rigid -val merge : bool -> rigid -> t -> Univ.universe_context_set -> t +val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t val merge_subst : t -> Universes.universe_opt_subst -> t val emit_side_effects : Safe_typing.private_constants -> t -> t -val new_univ_variable : rigid -> string option -> t -> t * Univ.Level.t +val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t val add_global_univ : t -> Univ.Level.t -> t val make_flexible_variable : t -> bool -> Univ.Level.t -> t |