aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml8
-rw-r--r--pretyping/globEnv.ml22
-rw-r--r--pretyping/globEnv.mli5
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/pretyping.ml44
-rw-r--r--pretyping/recordops.ml14
-rw-r--r--pretyping/reductionops.ml9
7 files changed, 74 insertions, 30 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index fc24e9b3a9..265909980b 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> debug_cbv:=a);
}
-let pr_key = function
+let debug_pr_key = function
| ConstKey (sp,_) -> Names.Constant.print sp
| VarKey id -> Names.Id.print id
| RelKey n -> Pp.(str "REL_" ++ int n)
@@ -320,14 +320,14 @@ and norm_head_ref k info env stack normt =
if red_set_ref (info_flags info.infos) normt then
match ref_value_cache info.infos info.tab normt with
| Some body ->
- if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
+ if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
strip_appl (shift_value k body) stack
| None ->
- if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+ if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
(VAL(0,make_constr_ref k normt),stack)
else
begin
- if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt);
+ if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
(VAL(0,make_constr_ref k normt),stack)
end
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 12788e5ec5..25510826cc 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -55,16 +55,16 @@ let env env = env.static_env
let vars_of_env env =
Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
-let ltac_interp_name { ltac_idents ; ltac_genargs } = function
- | Anonymous -> Anonymous
- | Name id as na ->
- try Name (Id.Map.find id ltac_idents)
- with Not_found ->
- if Id.Map.mem id ltac_genargs then
- user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
- spc () ++ str "is not bound to an identifier." ++
- spc () ++str "It cannot be used in a binder.")
- else na
+let ltac_interp_id { ltac_idents ; ltac_genargs } id =
+ try Id.Map.find id ltac_idents
+ with Not_found ->
+ if Id.Map.mem id ltac_genargs then
+ user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
+ spc () ++ str "is not bound to an identifier." ++
+ spc () ++str "It cannot be used in a binder.")
+ else id
+
+let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
let push_rel sigma d env =
let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
@@ -182,6 +182,8 @@ let interp_ltac_variable ?loc typing_fun env sigma id =
end;
raise Not_found
+let interp_ltac_id env id = ltac_interp_id env.lvar id
+
module ConstrInterpObj =
struct
type ('r, 'g, 't) obj =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 4038523211..70a7ee6e2f 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -76,6 +76,11 @@ val hide_variable : t -> Name.t -> Id.t -> t
val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) ->
t -> evar_map -> Id.t -> unsafe_judgment
+(** Interp an identifier as an ltac variable bound to an identifier,
+ or as the identifier itself if not bound to an ltac variable *)
+
+val interp_ltac_id : t -> Id.t -> Id.t
+
(** Interpreting a generic argument, typically a "ltac:(...)", taking
into account the possible renaming *)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ec0ff73062..b040e63cd2 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches =
not (has_dependent_elim mib) then
user_err ~hdr:"make_case_or_project"
Pp.(str"Dependent case analysis not allowed" ++
- str" on inductive type " ++ Names.MutInd.print (fst ind))
+ str" on inductive type " ++ print_constr_env env sigma (mkInd ind))
in
let branch = branches.(0) in
let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d10c00fa6e..a4c2cb2352 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -480,6 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
| GEvar (id, inst) ->
(* Ne faudrait-il pas s'assurer que hyps est bien un
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+ let id = interp_ltac_id env id in
let evk =
try Evd.evar_key id !evdref
with Not_found ->
@@ -499,6 +500,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (k, naming, None) ->
+ let open Namegen in
+ let naming = match naming with
+ | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id)
+ | IntroAnonymous -> IntroAnonymous
+ | IntroFresh id -> IntroFresh (interp_ltac_id env id) in
let ty =
match tycon with
| Some ty -> ty
@@ -960,20 +966,50 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
let f decl (subst,update) =
let id = NamedDecl.get_id decl in
+ let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
let t = replace_vars subst (NamedDecl.get_type decl) in
+ let check_body id c =
+ match b, c with
+ | Some b, Some c ->
+ if not (is_conv !!env !evdref b c) then
+ user_err ?loc (str "Cannot interpret " ++
+ pr_existential_key !evdref evk ++
+ strbrk " in current context: binding for " ++ Id.print id ++
+ strbrk " is not convertible to its expected definition (cannot unify " ++
+ quote (print_constr_env !!env !evdref b) ++
+ strbrk " and " ++
+ quote (print_constr_env !!env !evdref c) ++
+ str ").")
+ | Some b, None ->
+ user_err ?loc (str "Cannot interpret " ++
+ pr_existential_key !evdref evk ++
+ strbrk " in current context: " ++ Id.print id ++
+ strbrk " should be bound to a local definition.")
+ | None, _ -> () in
+ let check_type id t' =
+ if not (is_conv !!env !evdref t t') then
+ user_err ?loc (str "Cannot interpret " ++
+ pr_existential_key !evdref evk ++
+ strbrk " in current context: binding for " ++ Id.print id ++
+ strbrk " is not well-typed.") in
let c, update =
try
let c = List.assoc id update in
let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in
+ check_body id (Some c.uj_val);
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 (lift n t') then mkRel n, update else raise Not_found
+ let (n,b',t') = lookup_rel_id id (rel_context !!env) in
+ check_type id (lift n t');
+ check_body id (Option.map (lift n) b');
+ mkRel n, update
with Not_found ->
try
- let t' = !!env |> lookup_named id |> NamedDecl.get_type in
- if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found
+ let decl = lookup_named id !!env in
+ check_type id (NamedDecl.get_type decl);
+ check_body id (NamedDecl.get_value decl);
+ mkVar id, update
with Not_found ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !evdref evk ++
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index bd41e61b34..77ad96d2cf 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -334,19 +334,19 @@ let error_not_structure ref description =
user_err ~hdr:"object_declare"
(str"Could not declare a canonical structure " ++
(Id.print (basename_of_global ref) ++ str"." ++ spc() ++
- str(description)))
+ description))
let check_and_decompose_canonical_structure ref =
let sp =
match ref with
ConstRef sp -> sp
- | _ -> error_not_structure ref "Expected an instance of a record or structure."
+ | _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
in
let env = Global.env () in
let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
let vc = match Environ.constant_opt_value_in env (sp, u) with
| Some vc -> vc
- | None -> error_not_structure ref "Could not find its value in the global environment." in
+ | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
let env = Global.env () in
let evd = Evd.from_env env in
let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
@@ -354,18 +354,18 @@ let check_and_decompose_canonical_structure ref =
let f,args = match kind body with
| App (f,args) -> f,args
| _ ->
- error_not_structure ref "Expected a record or structure constructor applied to arguments." in
+ error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in
let indsp = match kind f with
| Construct ((indsp,1),u) -> indsp
- | _ -> error_not_structure ref "Expected an instance of a record or structure." in
+ | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in
let s =
try lookup_structure indsp
with Not_found ->
error_not_structure ref
- ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in
+ (str "Could not find the record or structure " ++ Termops.print_constr (EConstr.mkInd indsp)) in
let ntrue_projs = List.count snd s.s_PROJKIND in
if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
- error_not_structure ref "Got too few arguments to the record or structure constructor.";
+ error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
(sp,indsp)
let declare_canonical_structure ref =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index f4c8a6cd66..a0d20b7ce4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -341,6 +341,7 @@ struct
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
and 'a t = 'a member list
+ (* Debugging printer *)
let rec pr_member pr_c member =
let open Pp in
let pr_c x = hov 1 (pr_c x) in
@@ -351,7 +352,7 @@ struct
prvect_with_sep (pr_bar) pr_c br
++ str ")"
| Proj (p,cst) ->
- str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")"
+ str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")"
| Fix (f,args,cst) ->
str "ZFix(" ++ Termops.pr_fix pr_c f
++ pr_comma () ++ pr pr_c args ++ str ")"
@@ -368,11 +369,11 @@ struct
let open Pp in
match c with
| Cst_const (c, u) ->
- if Univ.Instance.is_empty u then Constant.print c
- else str"(" ++ Constant.print c ++ str ", " ++
+ if Univ.Instance.is_empty u then Constant.debug_print c
+ else str"(" ++ Constant.debug_print c ++ str ", " ++
Univ.Instance.pr Univ.Level.pr u ++ str")"
| Cst_proj p ->
- str".(" ++ Constant.print (Projection.constant p) ++ str")"
+ str".(" ++ Constant.debug_print (Projection.constant p) ++ str")"
let empty = []
let is_empty = CList.is_empty
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:09:32 +0000