aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evd.ml18
-rw-r--r--pretyping/evd.mli4
-rw-r--r--pretyping/pretyping.ml37
-rw-r--r--printing/ppconstr.ml2
-rw-r--r--printing/printer.ml2
7 files changed, 42 insertions, 25 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 18012f8a1..0c1c20ec6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -295,7 +295,7 @@ GEXTEND Gram
[ [ id = ident; ":="; c = lconstr -> (id,c) ] ]
;
evar_instance:
- [ [ "@{"; l = LIST1 inst SEP ","; "}" -> l
+ [ [ "@{"; l = LIST1 inst SEP ";"; "}" -> l
| -> [] ] ]
;
instance:
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b59f67bc3..1ff1b903f 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -439,7 +439,7 @@ let rec detype isgoal avoid env sigma t =
| Evar (evk,cl) ->
let id,l =
try Evd.evar_ident evk sigma,
- Evd.evar_instance_array isVarId (Evd.find sigma evk) cl
+ Evd.evar_instance_array (fun id c -> try let n = List.index Name.equal (Name id) env in isRelN n c with Not_found -> isVarId id c) (Evd.find sigma evk) cl
with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), [] in
GEvar (dl,id,
List.map (on_snd (detype isgoal avoid env sigma)) l)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 4dc3672a4..813a21229 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -279,22 +279,6 @@ let instantiate_evar_array info c args =
| [] -> c
| _ -> replace_vars inst c
-let complete_instance hyps update =
- let oldinst = List.map (fun (id,_,_) -> mkVar id) hyps in
- let rec aux seen newinst = function
- | [] -> newinst
- | (id,c) :: l ->
- if List.mem id seen then
- user_err_loc (Loc.ghost,"",pr_id id ++ str "appears more than once.")
- else
- let l1,l2 = List.split_when (fun c -> isVarId id c) newinst in
- match l2 with
- | [] ->
- user_err_loc (Loc.ghost,"",str "No such variable in the signature of the existential variable: " ++ pr_id id)
- | _::tl ->
- aux (id::seen) (l1 @ c :: tl) l in
- Array.of_list (aux [] oldinst update)
-
module StringOrd = struct type t = string let compare = String.compare end
module UNameMap = struct
@@ -1554,6 +1538,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
(**********************************************************)
(* Pretty-printing *)
+let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+
let pr_instance_status (sc,typ) =
begin match sc with
| IsSubType -> str " [or a subtype of it]"
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 2cea0eaa2..12a166e66 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -229,8 +229,6 @@ val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
val instantiate_evar_array : evar_info -> constr -> constr array -> constr
-val complete_instance : named_context -> (Id.t * constr) list -> constr array
-
val subst_evar_defs_light : substitution -> evar_map -> evar_map
(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
@@ -526,6 +524,8 @@ type open_constr = evar_map * constr
type unsolvability_explanation = SeveralInstancesFound of int
(** Failure explanation. *)
+val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
+
(** {5 Debug pretty-printers} *)
val pr_evar_info : evar_info -> Pp.std_ppcmds
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0115f67d5..28ab88526 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -231,6 +231,14 @@ let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
| Some t ->
evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t
+let check_instance loc subst = function
+ | [] -> ()
+ | (id,_) :: _ ->
+ if List.mem_assoc id subst then
+ user_err_loc (loc,"",pr_id id ++ str "appears more than once.")
+ else
+ user_err_loc (loc,"",str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+
(* used to enforce a name in Lambda when the type constraints itself
is named, hence possibly dependent *)
@@ -415,9 +423,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
with Not_found ->
user_err_loc (loc,"",str "Unknown existential variable.") in
let hyps = evar_filtered_context (Evd.find !evdref evk) in
- let f c = (pretype empty_tycon env evdref lvar c).uj_val in
- let inst = List.map (on_snd f) inst in
- let args = complete_instance hyps inst in
+ let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = (Retyping.get_judgment_of env !evdref c) in
inh_conv_coerce_to_tycon loc env evdref j tycon
@@ -911,6 +917,31 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
{ uj_val = v; uj_type = tval }
in inh_conv_coerce_to_tycon loc env evdref cj tycon
+and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
+ let f (id,_,t) (subst,update) =
+ let t = replace_vars subst t in
+ let c, update =
+ try
+ let c = List.assoc id update in
+ let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in
+ c.uj_val, List.remove_assoc id update
+ with Not_found ->
+ try
+ let (n,_,t') = lookup_rel_id id (rel_context env) in
+ if is_conv env !evdref t t' then raise Not_found else mkRel n, update
+ with Not_found ->
+ try
+ let (_,_,t') = lookup_named id env in
+ if is_conv env !evdref t t' then raise Not_found else mkVar id, update
+ with Not_found ->
+ user_err_loc (loc,"",str "Cannot interpret " ++
+ pr_existential_key !evdref evk ++
+ str " in current context: no binding for " ++ pr_id id ++ str ".") in
+ ((id,c)::subst, update) in
+ let subst,inst = List.fold_right f hyps ([],update) in
+ check_instance loc subst inst;
+ Array.map_of_list snd subst
+
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
and pretype_type resolve_tc valcon env evdref lvar = function
| GHole (loc, knd, None) ->
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index baafbc04f..058dc2447 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -180,7 +180,7 @@ let pr_evar pr id l =
| [] -> mt()
| l ->
let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
- str"@{" ++ hov 0 (prlist_with_sep pr_comma f l) ++ str"}"))
+ str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f l) ++ str"}"))
let las = lapp
let lpator = 100
diff --git a/printing/printer.ml b/printing/printer.ml
index 2aa9850a8..c19d0fea4 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -225,7 +225,7 @@ let pr_puniverses f env (c,u) =
else mt ())
let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+let pr_existential_key = Evd.pr_existential_key
let pr_existential env sigma ev = pr_lconstr_env env sigma (mkEvar ev)
let pr_inductive env ind = pr_lconstr_env env Evd.empty (mkInd ind)
let pr_constructor env cstr = pr_lconstr_env env Evd.empty (mkConstruct cstr)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 08:18:54 +0000