aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml3
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml6
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml21
-rw-r--r--engine/evd.mli2
-rw-r--r--engine/proofview.ml6
-rw-r--r--engine/termops.ml27
-rw-r--r--engine/universes.ml2
9 files changed, 40 insertions, 31 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 1f4ff5092f..33d7acc319 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -784,6 +784,9 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
Sigma.Sigma (of_constr t,sigma,p)
+let is_global sigma gr c =
+ Globnames.is_global gr (to_constr sigma c)
+
module Unsafe =
struct
let to_sorts = ESorts.unsafe_to_sorts
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 06020c5738..94b7ca96ae 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -261,6 +261,8 @@ val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
'r Sigma.t -> Globnames.global_reference -> (t, 'r) Sigma.sigma
+val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+
(** {5 Extra} *)
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6cba6f6075..59ad4ef472 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -220,7 +220,7 @@ let make_pure_subst evi args =
(fun decl (args,l) ->
match args with
| a::rest -> (rest, (NamedDecl.get_id decl, a)::l)
- | _ -> anomaly (Pp.str "Instance does not match its signature"))
+ | _ -> anomaly (Pp.str "Instance does not match its signature."))
(evar_filtered_context evi) (Array.rev_to_list args,[]))
(*------------------------------------*
@@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
let evd = Sigma.to_evar_map evd in
let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
- let evd, evk' = Evd.restrict evk filter ?candidates evd in
+ let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
let new_pure_evar_full evd evi =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index fcc435a2ec..496ec5bc43 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
- constr list option -> (existential_key, 'r) Sigma.sigma
+ ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
(** Polymorphic constants *)
diff --git a/engine/evd.ml b/engine/evd.ml
index b677705bc9..08d26f40d4 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -155,7 +155,7 @@ let make_evar hyps ccl = {
}
let instance_mismatch () =
- anomaly (Pp.str "Signature and its instance do not match")
+ anomaly (Pp.str "Signature and its instance do not match.")
let evar_concl evi = evi.evar_concl
@@ -400,7 +400,7 @@ let rename evk id (evtoid, idtoev) =
match id' with
| None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
| Some id' ->
- if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+ if Idmap.mem id idtoev then anomaly (str "Evar name already in use.");
(EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
let reassign_name_defined evk evk' (evtoid, idtoev as names) =
@@ -553,7 +553,7 @@ let existential_type d (n, args) =
let info =
try find d n
with Not_found ->
- anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared") in
+ anomaly (str "Evar " ++ str (string_of_existential n) ++ str " was not declared.") in
instantiate_evar_array info info.evar_concl args
let add_constraints d c =
@@ -635,9 +635,9 @@ let define_aux def undef evk body =
try EvMap.find evk undef
with Not_found ->
if EvMap.mem evk def then
- anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice")
+ anomaly ~label:"Evd.define" (Pp.str "cannot define an evar twice.")
else
- anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar")
+ anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
in
let () = assert (oldinfo.evar_body == Evar_empty) in
let newinfo = { oldinfo with evar_body = Evar_defined body } in
@@ -653,12 +653,13 @@ let define evk body evd =
let evar_names = EvNames.remove_name_defined evk evd.evar_names in
{ evd with defn_evars; undf_evars; last_mods; evar_names }
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
let evar_info' =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
evar_extra = Store.empty } in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
@@ -1021,7 +1022,7 @@ let try_meta_fvalue evd mv =
let meta_fvalue evd mv =
try try_meta_fvalue evd mv
- with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value")
+ with Not_found -> anomaly ~label:"meta_fvalue" (Pp.str "meta has no value.")
let meta_value evd mv =
(fst (try_meta_fvalue evd mv)).rebus
@@ -1040,7 +1041,7 @@ let meta_declare mv v ?(name=Anonymous) evd =
let meta_assign mv (v, pb) evd =
let modify _ = function
| Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
- | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined")
+ | _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.")
in
let metas = Metamap.modify mv modify evd.metas in
set_metas evd metas
@@ -1048,7 +1049,7 @@ let meta_assign mv (v, pb) evd =
let meta_reassign mv (v, pb) evd =
let modify _ = function
| Clval(na, _, ty) -> Clval (na, (mk_freelisted v, pb), ty)
- | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined")
+ | _ -> anomaly ~label:"meta_reassign" (Pp.str "not yet defined.")
in
let metas = Metamap.modify mv modify evd.metas in
set_metas evd metas
@@ -1089,7 +1090,7 @@ let dependent_evar_ident ev evd =
let evi = find evd ev in
match evi.evar_source with
| (_,Evar_kinds.VarInstance id) -> id
- | _ -> anomaly (str "Not an evar resulting of a dependent binding")
+ | _ -> anomaly (str "Not an evar resulting of a dependent binding.")
(**********************************************************)
(* Extra data *)
diff --git a/engine/evd.mli b/engine/evd.mli
index 0053324706..86755c360b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool ->
(** {6 Misc} *)
val restrict : evar -> Filter.t -> ?candidates:constr list ->
- evar_map -> evar_map * evar
+ ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
(** Restrict an undefined evar into a new evar by filtering context and
possibly limiting the instances to a set of candidates *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ddfc0e39dd..29bb1ef397 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
let info =
if goal then
{ info with Evd.evar_source = match info.Evd.evar_source with
+ (* Two kinds for goal evars:
+ - GoalEvar (morally not dependent)
+ - VarInstance (morally dependent of some name).
+ This is a heuristic for naming these evars. *)
+ | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+ Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
| _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
| loc,_ -> loc,Evar_kinds.GoalEvar }
else info
diff --git a/engine/termops.ml b/engine/termops.ml
index ca32c06a75..92016d4af4 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -31,10 +31,6 @@ let pr_sort_family = function
| InProp -> (str "Prop")
| InType -> (str "Type")
-let pr_name = function
- | Name id -> pr_id id
- | Anonymous -> str "_"
-
let pr_con sp = str(string_of_con sp)
let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
@@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
hov 1
(str"fix " ++ int i ++ spc() ++ str"{" ++
v 0 (prlist_with_sep spc (fun (na,i,ty,bd) ->
- pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
+ Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
@@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with
(str"(" ++ pr_constr t ++ str " ->" ++ spc() ++
pr_constr c ++ str")")
| Lambda (na,t,c) -> hov 1
- (str"fun " ++ pr_name na ++ str":" ++
+ (str"fun " ++ Name.print na ++ str":" ++
pr_constr t ++ str" =>" ++ spc() ++ pr_constr c)
| LetIn (na,b,t,c) -> hov 0
- (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++
+ (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++
str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++
pr_constr c)
| App (c,l) -> hov 1
@@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with
hov 1
(str"cofix " ++ int i ++ spc() ++ str"{" ++
v 0 (prlist_with_sep spc (fun (na,ty,bd) ->
- pr_name na ++ str":" ++ pr_constr ty ++
+ Name.print na ++ str":" ++ pr_constr ty ++
cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
str"}")
@@ -112,6 +108,7 @@ let pr_evar_suggested_name evk sigma =
| None -> match evi.evar_source with
| _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
| _,Evar_kinds.VarInstance id -> id
+ | _,Evar_kinds.QuestionMark (_,Name id) -> id
| _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
| _ ->
let env = reset_with_named_context evi.evar_hyps (Global.env()) in
@@ -308,8 +305,8 @@ let pr_evar_universe_context ctx =
let print_env_short env =
let print_constr = print_kconstr in
let pr_rel_decl = function
- | RelDecl.LocalAssum (n,_) -> pr_name n
- | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")"
+ | RelDecl.LocalAssum (n,_) -> Name.print n
+ | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
in
let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
let nc = List.rev (named_context env) in
@@ -506,7 +503,7 @@ let push_named_rec_types (lna,typarray,_) env =
(fun i na t ->
match na with
| Name id -> LocalAssum (id, lift i t)
- | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
+ | Anonymous -> anomaly (Pp.str "Fix declarations must be named."))
lna typarray in
Array.fold_left
(fun e assum -> push_named assum e) env ctxt
@@ -582,7 +579,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with
(* Get the last arg of an application *)
let last_arg sigma c = match EConstr.kind sigma c with
| App (f,cl) -> Array.last cl
- | _ -> anomaly (Pp.str "last_arg")
+ | _ -> anomaly (Pp.str "last_arg.")
(* Get the last arg of an application *)
let decompose_app_vect sigma c =
@@ -1289,7 +1286,7 @@ let rec eta_reduce_head sigma c =
(match EConstr.kind sigma (eta_reduce_head sigma c') with
| App (f,cl) ->
let lastn = (Array.length cl) - 1 in
- if lastn < 0 then anomaly (Pp.str "application without arguments")
+ if lastn < 0 then anomaly (Pp.str "application without arguments.")
else
(match EConstr.kind sigma cl.(lastn) with
| Rel 1 ->
@@ -1442,7 +1439,7 @@ let prod_applist sigma c l =
match EConstr.kind sigma c, l with
| Prod(_,_,c), arg::l -> app (arg::subst) c l
| _, [] -> Vars.substl subst c
- | _ -> anomaly (Pp.str "Not enough prod's") in
+ | _ -> anomaly (Pp.str "Not enough prod's.") in
app [] c l
(* Combinators on judgments *)
@@ -1458,7 +1455,7 @@ let context_chop k ctx =
| (0, l2) -> (List.rev acc, l2)
| (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t)
| (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
- | (_, []) -> anomaly (Pp.str "context_chop")
+ | (_, []) -> anomaly (Pp.str "context_chop.")
in chop_aux [] (k,ctx)
(* Do not skip let-in's *)
diff --git a/engine/universes.ml b/engine/universes.ml
index 1900112dde..f201081862 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -101,7 +101,7 @@ let enforce_eq_instances_univs strict x y c =
let ax = Instance.to_array x and ay = Instance.to_array y in
if Array.length ax != Array.length ay then
CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
- Pp.str " instances of different lengths");
+ Pp.str " instances of different lengths.");
CArray.fold_right2
(fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
ax ay c
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 06:03:15 +0000