diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 2 | ||||
| -rw-r--r-- | engine/evarutil.mli | 12 | ||||
| -rw-r--r-- | engine/evd.ml | 10 | ||||
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | engine/namegen.ml | 3 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 133 |
7 files changed, 83 insertions, 81 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index e85c1f6fd8..6cba6f6075 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -365,7 +365,7 @@ let push_rel_context_to_named_context env sigma typ = * Entry points to define new evars * *------------------------------------*) -let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let default_source = Loc.tag @@ Evar_kinds.InternalHole let restrict_evar evd evk filter candidates = let evd = Sigma.to_evar_map evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ca9591e71b..fcc435a2ec 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -22,13 +22,13 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> (constr, 'r) Sigma.sigma val new_pure_evar : - named_context_val -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + named_context_val -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> (evar, 'r) Sigma.sigma @@ -37,7 +37,7 @@ val new_pure_evar_full : 'r Sigma.t -> evar_info -> (evar, 'r) Sigma.sigma (** the same with side-effects *) val e_new_evar : - env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> constr @@ -45,12 +45,12 @@ val e_new_evar : (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + env -> 'r Sigma.t -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> (constr * sorts, 'r) Sigma.sigma val e_new_type_evar : env -> evar_map ref -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * sorts val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma @@ -72,7 +72,7 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr as a telescope) is [sign] *) val new_evar_instance : named_context_val -> 'r Sigma.t -> types -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> constr list -> (constr, 'r) Sigma.sigma diff --git a/engine/evd.ml b/engine/evd.ml index db048bbd6e..8ade6cb996 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -149,7 +149,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; - evar_source = (Loc.ghost,Evar_kinds.InternalHole); + evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; evar_extra = Store.empty } @@ -704,7 +704,7 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = | _ -> match kind_of_term (fst (decompose_app t2)) with | Evar (evk2,_) -> fst (evar_source evk2 evd) - | _ -> Loc.ghost + | _ -> None (** The following functions return the set of evars immediately contained in the object *) @@ -790,7 +790,7 @@ let make_evar_universe_context e l = | Some us -> List.fold_left (fun uctx (loc,id) -> - fst (UState.new_univ_variable ~loc univ_rigid (Some (Id.to_string id)) uctx)) + fst (UState.new_univ_variable ?loc univ_rigid (Some (Id.to_string id)) uctx)) uctx us (****************************************) @@ -1082,8 +1082,8 @@ let retract_coercible_metas evd = let evar_source_of_meta mv evd = match meta_name evd mv with - | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar) - | Name id -> (Loc.ghost,Evar_kinds.VarInstance id) + | Anonymous -> Loc.tag Evar_kinds.GoalEvar + | Name id -> Loc.tag @@ Evar_kinds.VarInstance id let dependent_evar_ident ev evd = let evi = find evd ev in diff --git a/engine/evd.mli b/engine/evd.mli index 9c40c8b715..0053324706 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -414,7 +414,7 @@ val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> evar_map * evar_constraint list val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list -val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t +val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option (** The following functions return the set of evars immediately contained in the object; need the term to be evar-normal otherwise diff --git a/engine/namegen.ml b/engine/namegen.ml index 3b979f206e..5bd62273c8 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -418,8 +418,7 @@ let use_h_based_elimination_names () = open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of \"H\"-based proposition names in elimination tactics"; optkey = ["Standard";"Proposition";"Elimination";"Names"]; optread = (fun () -> !h_based_elimination_names); diff --git a/engine/proofview.ml b/engine/proofview.ml index 99bd4bc4ff..7f80d40d64 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -66,7 +66,7 @@ let dependent_init = for type classes. *) let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) - let src = (Loc.ghost,Evar_kinds.GoalEvar) in + let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } diff --git a/engine/uState.ml b/engine/uState.ml index c66af02bb9..dc68220575 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -131,84 +131,87 @@ let instantiate_variable l b v = exception UniversesDiffer let process_universe_constraints ctx cstrs = + let open Univ in let univs = ctx.uctx_universes in let vars = ref ctx.uctx_univ_variables in let normalize = Universes.normalize_universe_opt_subst vars in - let rec unify_universes fo l d r local = + let is_local l = Univ.LMap.mem l !vars in + let varinfo x = + match Univ.Universe.level x with + | None -> Inl x + | Some l -> Inr l + in + let equalize_variables fo l l' r r' local = + (** Assumes l = [l',0] and r = [r',0] *) + let () = + if is_local l' then + instantiate_variable l' r vars + else if is_local r' then + instantiate_variable r' l vars + else if not (UGraph.check_eq_level univs l' r') then + (* Two rigid/global levels, none of them being local, + one of them being Prop/Set, disallow *) + if Univ.Level.is_small l' || Univ.Level.is_small r' then + raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + else if fo then + raise UniversesDiffer + in + Univ.enforce_eq_level l' r' local + in + let equalize_universes l r local = match varinfo l, varinfo r with + | Inr l', Inr r' -> equalize_variables false l l' r r' local + | Inr l, Inl r | Inl r, Inr l -> + let alg = Univ.LSet.mem l ctx.uctx_univ_algebraic in + let inst = Univ.univ_level_rem l r r in + if alg then (instantiate_variable l inst vars; local) + else + let lu = Univ.Universe.make l in + if Univ.univ_level_mem l r then + Univ.enforce_leq inst lu local + else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) + | Inl _, Inl _ (* both are algebraic *) -> + if UGraph.check_eq univs l r then local + else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + in + let unify_universes (l, d, r) local = let l = normalize l and r = normalize r in if Univ.Universe.equal l r then local else - let varinfo x = - match Univ.Universe.level x with - | None -> Inl x - | Some l -> Inr (l, Univ.LMap.mem l !vars, Univ.LSet.mem l ctx.uctx_univ_algebraic) - in - if d == Universes.ULe then + match d with + | Universes.ULe -> if UGraph.check_leq univs l r then (** Keep Prop/Set <= var around if var might be instantiated by prop or set later. *) - if Univ.Universe.is_level l then - match Univ.Universe.level r with - | Some r -> - Univ.Constraint.add (Option.get (Univ.Universe.level l),Univ.Le,r) local - | _ -> local - else local + match Univ.Universe.level l, Univ.Universe.level r with + | Some l, Some r -> + Univ.Constraint.add (l, Univ.Le, r) local + | _ -> local else - match Univ.Universe.level r with + begin match Univ.Universe.level r with | None -> error ("Algebraic universe on the right") - | Some rl -> - if Univ.Level.is_small rl then + | Some r' -> + if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in - Univ.LSet.fold (fun l local -> - if Univ.Level.is_small l || Univ.LMap.mem l !vars then - unify_universes fo (Univ.Universe.make l) Universes.UEq r local - else raise (Univ.UniverseInconsistency (Univ.Le, Univ.Universe.make l, r, None))) - levels local + let fold l' local = + let l = Univ.Universe.make l' in + if Univ.Level.is_small l' || is_local l' then + equalize_variables false l l' r r' local + else raise (Univ.UniverseInconsistency (Univ.Le, l, r, None)) + in + Univ.LSet.fold fold levels local else Univ.enforce_leq l r local - else if d == Universes.ULub then - match varinfo l, varinfo r with - | (Inr (l, true, _), Inr (r, _, _)) - | (Inr (r, _, _), Inr (l, true, _)) -> - instantiate_variable l (Univ.Universe.make r) vars; - Univ.enforce_eq_level l r local - | Inr (_, _, _), Inr (_, _, _) -> - unify_universes true l Universes.UEq r local + end + | Universes.ULub -> + begin match Universe.level l, Universe.level r with + | Some l', Some r' -> + equalize_variables true l l' r r' local | _, _ -> assert false - else (* d = Universes.UEq *) - match varinfo l, varinfo r with - | Inr (l', lloc, _), Inr (r', rloc, _) -> - let () = - if lloc then - instantiate_variable l' r vars - else if rloc then - instantiate_variable r' l vars - else if not (UGraph.check_eq univs l r) then - (* Two rigid/global levels, none of them being local, - one of them being Prop/Set, disallow *) - if Univ.Level.is_small l' || Univ.Level.is_small r' then - raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) - else - if fo then - raise UniversesDiffer - in - Univ.enforce_eq_level l' r' local - | Inr (l, loc, alg), Inl r - | Inl r, Inr (l, loc, alg) -> - let inst = Univ.univ_level_rem l r r in - if alg then (instantiate_variable l inst vars; local) - else - let lu = Univ.Universe.make l in - if Univ.univ_level_mem l r then - Univ.enforce_leq inst lu local - else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None)) - | _, _ (* One of the two is algebraic or global *) -> - if UGraph.check_eq univs l r then local - else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None)) + end + | Universes.UEq -> equalize_universes l r local in let local = - Universes.Constraints.fold (fun (l,d,r) local -> unify_universes false l d r local) - cstrs Univ.Constraint.empty + Universes.Constraints.fold unify_universes cstrs Univ.Constraint.empty in !vars, local @@ -255,7 +258,7 @@ let universe_context ?names ctx = let l = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> - user_err ~loc ~hdr:"universe_context" + user_err ?loc ~hdr:"universe_context" (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) pl ([], [], levels) @@ -266,10 +269,10 @@ let universe_context ?names ctx = try let info = Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in - Option.default Loc.ghost info.uloc - with Not_found -> Loc.ghost + info.uloc + with Not_found -> None in - user_err ~loc ~hdr:"universe_context" + user_err ?loc ~hdr:"universe_context" ((str(CString.plural n "Universe") ++ spc () ++ Univ.LSet.pr (pr_uctx_level ctx) left ++ spc () ++ str (CString.conjugate_verb_to_be n) ++ |