aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml8
-rw-r--r--pretyping/classops.ml35
-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
8 files changed, 82 insertions, 57 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/classops.ml b/pretyping/classops.ml
index 94da51626f..b264e31474 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -111,14 +111,18 @@ end
type cl_index = Bijint.Index.t
+let init_class_tab =
+ let open Bijint in
+ add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
+
let class_tab =
- ref (Bijint.empty : cl_info_typ Bijint.t)
+ Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
let coercion_tab =
- ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
+ Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
let coercions_in_scope =
- ref GlobRef.Set_env.empty
+ Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty
module ClPairOrd =
struct
@@ -131,15 +135,7 @@ end
module ClPairMap = Map.Make(ClPairOrd)
let inheritance_graph =
- ref (ClPairMap.empty : inheritance_path ClPairMap.t)
-
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
-
-let unfreeze (fcl,fco,fig,in_scope) =
- class_tab:=fcl;
- coercion_tab:=fco;
- inheritance_graph:=fig;
- coercions_in_scope:=in_scope
+ Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t)
(* ajout de nouveaux "objets" *)
@@ -153,21 +149,6 @@ let add_new_coercion coe s =
let add_new_path x y =
inheritance_graph := ClPairMap.add x y !inheritance_graph
-let init () =
- class_tab:= Bijint.empty;
- add_new_class CL_FUN { cl_param = 0 };
- add_new_class CL_SORT { cl_param = 0 };
- coercion_tab:= CoeTypMap.empty;
- inheritance_graph:= ClPairMap.empty
-
-let _ =
- Summary.declare_summary "inh_graph"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-let _ = init()
-
(* class_info : cl_typ -> int * cl_info_typ *)
let class_info cl = Bijint.revmap cl !class_tab
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-05-05 22:50:34 +0000