aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml35
-rw-r--r--pretyping/cases.mli2
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/classops.ml2
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarconv.ml96
-rw-r--r--pretyping/evardefine.ml2
-rw-r--r--pretyping/evarsolve.ml1
-rw-r--r--pretyping/find_subterm.ml1
-rw-r--r--pretyping/glob_ops.ml16
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/nativenorm.ml7
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/pretype_errors.ml5
-rw-r--r--pretyping/pretype_errors.mli1
-rw-r--r--pretyping/pretyping.ml18
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/recordops.ml4
-rw-r--r--pretyping/reductionops.ml11
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/unification.ml14
23 files changed, 147 insertions, 87 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c3968f8963..b8fb61e35d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1765,12 +1765,12 @@ let build_inversion_problem loc env sigma tms t =
Pushed (true,((tm,tmtyp),deps,na)))
dep_sign decls in
let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
- (* [eqn1] is the first clause of the auxiliary pattern-matching that
+ (* [main_eqn] is the main clause of the auxiliary pattern-matching that
serves as skeleton for the return type: [patl] is the
substructure of constructors extracted from the list of
constraints on the inductive types of the multiple terms matched
in the original pattern-matching problem Xi *)
- let eqn1 =
+ let main_eqn =
{ patterns = patl;
alias_stack = [];
eqn_loc = Loc.ghost;
@@ -1781,19 +1781,24 @@ let build_inversion_problem loc env sigma tms t =
rhs_vars = List.map fst subst;
avoid_ids = avoid;
it = Some (lift n t) } } in
- (* [eqn2] is the default clause of the auxiliary pattern-matching: it will
- catch the clauses of the original pattern-matching problem Xi whose
- type constraints are incompatible with the constraints on the
+ (* [catch_all] is a catch-all default clause of the auxiliary
+ pattern-matching, if needed: it will catch the clauses
+ of the original pattern-matching problem Xi whose type
+ constraints are incompatible with the constraints on the
inductive types of the multiple terms matched in Xi *)
- let eqn2 =
- { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
- alias_stack = [];
- eqn_loc = Loc.ghost;
- used = ref false;
- rhs = { rhs_env = pb_env;
- rhs_vars = [];
- avoid_ids = avoid0;
- it = None } } in
+ let catch_all_eqn =
+ if List.for_all (irrefutable env) patl then
+ (* No need for a catch all clause *)
+ []
+ else
+ [ { patterns = List.map (fun _ -> PatVar (Loc.ghost,Anonymous)) patl;
+ alias_stack = [];
+ eqn_loc = Loc.ghost;
+ used = ref false;
+ rhs = { rhs_env = pb_env;
+ rhs_vars = [];
+ avoid_ids = avoid0;
+ it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
(* let sigma, s = Evd.new_sort_variable sigma in *)
@@ -1810,7 +1815,7 @@ let build_inversion_problem loc env sigma tms t =
pred = (*ty *) mkSort s;
tomatch = sub_tms;
history = start_history n;
- mat = [eqn1;eqn2];
+ mat = main_eqn :: catch_all_eqn;
caseloc = loc;
casestyle = RegularStyle;
typing_function = build_tycon loc env pb_env s subst} in
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 257d1e5787..d7fff8af4b 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -32,6 +32,8 @@ val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> '
val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
+val irrefutable : env -> cases_pattern -> bool
+
(** {6 Compilation primitive. } *)
val compile_cases :
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 43062a0e8d..afd86420e9 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -310,7 +310,7 @@ and cbv_stack_value info env = function
| (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,pi,stk)))
when red_set (info_flags info) fIOTA && Projection.unfolded p ->
let arg = args.(pi.Declarations.proj_npars + pi.Declarations.proj_arg) in
- cbv_stack_value info env (arg, stk)
+ cbv_stack_value info env (strip_appl arg stk)
(* may be reduced later by application *)
| (FIXP(fix,env,[||]), APP(appl,TOP)) -> FIXP(fix,env,appl)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index ece92b66ba..55220f44c0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
if is_ambig && is_verbose () then
- msg_warning (message_ambig !ambig_paths)
+ Feedback.msg_warning (message_ambig !ambig_paths)
type coercion = {
coercion_type : coe_typ;
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 4fb4112022..129725c6d2 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -50,11 +50,11 @@ type bound_ident_map = Id.t Id.Map.t
exception PatternMatchingFailure
let warn_bound_meta name =
- msg_warning (str "Collision between bound variable " ++ pr_id name ++
+ Feedback.msg_warning (str "Collision between bound variable " ++ pr_id name ++
str " and a metavariable of same name.")
let warn_bound_bound name =
- msg_warning (str "Collision between bound variables of name " ++ pr_id name)
+ Feedback.msg_warning (str "Collision between bound variables of name " ++ pr_id name)
let constrain n (ids, m as x) (names, terms as subst) =
try
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c973e1cef3..86921c49b0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -620,7 +620,7 @@ and share_names flags n l avoid env sigma c t =
share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
(* If built with the f/n notation: we renounce to share names *)
| _ ->
- if n>0 then msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
+ if n>0 then Feedback.msg_warning (strbrk "Detyping.detype: cannot factorize fix enough");
let c = detype flags avoid env sigma c in
let t = detype flags avoid env sigma t in
(List.rev l,c,t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 08973a05c4..e5fc5a188d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -103,8 +103,7 @@ let position_problem l2r = function
| CUMUL -> Some l2r
let occur_rigidly ev evd t =
- let (l, app) = decompose_app_vect t in
- let rec aux t =
+ let rec aux t =
match kind_of_term (whd_evar evd t) with
| App (f, c) -> if aux f then Array.exists aux c else false
| Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
@@ -116,7 +115,7 @@ let occur_rigidly ev evd t =
| Prod (_, b, t) -> ignore(aux b || aux t); true
| Rel _ | Var _ -> false
| Case _ -> false
- in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app
+ in try ignore(aux t); false with Occur -> true
(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose
the problem (t1 stack1) = (t2 stack2) into a problem
@@ -368,8 +367,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) =
- let default_fail i = (* costly *)
- UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in
let quick_fail i = (* not costly, loses info *)
UnifFailure (i, NotSameHead)
in
@@ -421,7 +418,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let not_only_app = Stack.not_purely_applicative skM in
let f1 i =
match Stack.list_of_app_stack skF with
- | None -> default_fail evd
+ | None -> quick_fail evd
| Some lF ->
let tM = Stack.zip apprM in
miller_pfenning on_left
@@ -468,10 +465,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) =
let switch f a b = if on_left then f a b else f b a in
let eta evd =
- match kind_of_term termR with
- | Lambda _ -> eta env evd false skR termR skF termF
- | Construct u -> eta_constructor ts env evd skR u skF termF
- | _ -> UnifFailure (evd,NotSameHead)
+ match kind_of_term termR with
+ | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR ->
+ eta env evd false skR termR skF termF
+ | Construct u -> eta_constructor ts env evd skR u skF termF
+ | _ -> UnifFailure (evd,NotSameHead)
in
match Stack.list_of_app_stack skF with
| None ->
@@ -501,15 +499,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(* Evar must be undefined since we have flushed evars *)
let () = if !debug_unification then
let open Pp in
- pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())
+ Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())
++ fnl ()) in
match (flex_kind_of_term (fst ts) env evd term1 sk1,
flex_kind_of_term (fst ts) env evd term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
+ (* sk1[?ev1] =? sk2[?ev2] *)
let f1 i =
+ (* Try first-order unification *)
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
- |None, Success i' ->
- (* Evar can be defined in i' *)
+ | None, Success i' ->
+ (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
+ (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
@@ -517,7 +518,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else
evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
- |Some (r,[]), Success i' ->
+ | Some (r,[]), Success i' ->
+ (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
+ (* we now unify r[?ev1] and ?ev2 *)
let ev2' = whd_evar i' (mkEvar ev2) in
if isEvar ev2' then
solve_simple_eqn (evar_conv_x ts) env i'
@@ -525,16 +528,46 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else
evar_eqappr_x ts env evd pbty
((ev2', sk1), csts1) ((term2, sk2), csts2)
-
- |Some ([],r), Success i' ->
+ | Some ([],r), Success i' ->
+ (* Symmetrically *)
+ (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
+ (* we now unify ?ev1 and r[?ev2] *)
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
(position_problem true pbty,destEvar ev1',Stack.zip(term2,r))
else evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
- |_, (UnifFailure _ as x) -> x
- |Some _, _ -> UnifFailure (i,NotSameArgSize)
+ | None, (UnifFailure _ as x) ->
+ (* sk1 and sk2 have no common outer part *)
+ if Stack.not_purely_applicative sk2 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid true ev1 appr1 appr2
+ else
+ if Stack.not_purely_applicative sk1 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid false ev2 appr2 appr1
+ else
+ (* We could instead try Miller unification, then
+ postpone to see if other equations help, as in:
+ [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *)
+ x
+ | Some _, Success _ ->
+ (* sk1 and sk2 have a common outer part *)
+ if Stack.not_purely_applicative sk2 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid true ev1 appr1 appr2
+ else
+ if Stack.not_purely_applicative sk1 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid false ev2 appr2 appr1
+ else
+ (* We could instead try Miller unification, then
+ postpone to see if other equations help, as in:
+ [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
+ UnifFailure (i,NotSameArgSize)
+ | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
+
and f2 i =
if Evar.equal sp1 sp2 then
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
@@ -712,10 +745,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd [f3; f4]
(* Eta-expansion *)
- | Rigid, _ when isLambda term1 ->
+ | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 ->
eta env evd true sk1 term1 sk2 term2
- | _, Rigid when isLambda term2 ->
+ | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 ->
eta env evd false sk2 term2 sk1 term1
| Rigid, Rigid -> begin
@@ -1071,7 +1104,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
abstract_free_holes evd subst, true
with TypingFailed evd -> evd, false
-let second_order_matching_with_args ts env evd ev l t =
+let second_order_matching_with_args ts env evd pbty ev l t =
(*
let evd,ev = evar_absorb_arguments env evd ev l in
let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
@@ -1079,8 +1112,9 @@ let second_order_matching_with_args ts env evd ev l t =
if b then Success evd
else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
if b then Success evd else
-*)
- UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
+ *)
+ let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
+ UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
@@ -1096,7 +1130,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
type inference *)
(match choose_less_dependent_instance evk1 evd term2 args1 with
| Some evd -> Success evd
- | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
+ | None ->
+ let reason = ProblemBeyondCapabilities in
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
&& List.for_all (fun a -> Term.eq_constr a term1 || isEvar a)
(remove_instance_local_defs evd evk2 args2) ->
@@ -1104,7 +1140,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
type inference *)
(match choose_less_dependent_instance evk2 evd term1 args2 with
| Some evd -> Success evd
- | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
+ | None ->
+ let reason = ProblemBeyondCapabilities in
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
Success (solve_refl ~can_drop:true f env evd
@@ -1119,20 +1157,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
ise_try evd
[(fun evd -> first_order_unification ts env evd (ev1,l1) appr2);
(fun evd ->
- second_order_matching_with_args ts env evd ev1 l1 t2)]
+ second_order_matching_with_args ts env evd pbty ev1 l1 t2)]
| _,Evar ev2 when Array.length l2 <= Array.length l1 ->
(* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
(* and otherwise second-order matching *)
ise_try evd
[(fun evd -> first_order_unification ts env evd (ev2,l2) appr1);
(fun evd ->
- second_order_matching_with_args ts env evd ev2 l2 t1)]
+ second_order_matching_with_args ts env evd pbty ev2 l2 t1)]
| Evar ev1,_ ->
(* Try second-order pattern-matching *)
- second_order_matching_with_args ts env evd ev1 l1 t2
+ second_order_matching_with_args ts env evd pbty ev1 l1 t2
| _,Evar ev2 ->
(* Try second-order pattern-matching *)
- second_order_matching_with_args ts env evd ev2 l2 t1
+ second_order_matching_with_args ts env evd pbty ev2 l2 t1
| _ ->
(* Some head evar have been instantiated, or unknown kind of problem *)
evar_conv_x ts env evd pbty t1 t2
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index ef3a3f5255..d349cf8216 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
open Util
open Pp
open Names
@@ -14,7 +13,6 @@ open Term
open Vars
open Termops
open Namegen
-open Pre_env
open Environ
open Evd
open Evarutil
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 3d1822102a..455a7dbd69 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -20,7 +20,6 @@ open Reductionops
open Evarutil
open Pretype_errors
open Sigma.Notations
-open Context.Rel.Declaration
let normalize_evar evd ev =
match kind_of_term (whd_evar evd (mkEvar ev)) with
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index ae8b91c346..df1fc20f1d 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -108,7 +108,6 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
let rec substrec k t =
if nowhere_except_in && !pos > maxocc then t else
- if not (Vars.closed0 t) then subst_below k t else
try
let subst = test.match_fun test.testing_state t in
if Locusops.is_selected !pos occs then
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index c9860864a9..04100c8a73 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -266,7 +266,7 @@ let add_name_to_ids set na =
| Anonymous -> set
| Name id -> Id.Set.add id set
-let free_glob_vars =
+let free_glob_vars =
let rec vars bounded vs = function
| GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
| GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
@@ -324,10 +324,20 @@ let free_glob_vars =
let vs = vars Id.Set.empty Id.Set.empty rt in
Id.Set.elements vs
+let glob_visible_short_qualid c =
+ let rec aux acc = function
+ | GRef (_,c,_) ->
+ let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
+ let dir,id = Libnames.repr_qualid qualid in
+ if DirPath.is_empty dir then id :: acc else acc
+ | c ->
+ fold_glob_constr aux acc c
+ in aux [] c
+
let add_and_check_ident id set =
if Id.Set.mem id set then
- Pp.(msg_warning
- (str "Collision between bound variables of name " ++ Id.print id));
+ Feedback.msg_warning
+ Pp.(str "Collision between bound variables of name " ++ Id.print id);
Id.Set.add id set
let bound_glob_vars =
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 45444234a3..e0a2de0326 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -40,6 +40,7 @@ val occur_glob_constr : Id.t -> glob_constr -> bool
val free_glob_vars : glob_constr -> Id.t list
val bound_glob_vars : glob_constr -> Id.Set.t
val loc_of_glob_constr : glob_constr -> Loc.t
+val glob_visible_short_qualid : glob_constr -> Id.t list
(** [map_pattern_binders f m c] applies [f] to all the binding names
in a pattern-matching expression ({!Glob_term.GCases}) represented
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 713c99597a..5d36fc78ef 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -184,7 +184,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
(match dest_recarg ra with
| Mrec (_,j) when is_rec -> (depPvect.(j),rest)
| Imbr _ ->
- msg_warning (strbrk "Ignoring recursive call");
+ Feedback.msg_warning (strbrk "Ignoring recursive call");
(None,rest)
| _ -> (None, rest))
in
@@ -592,7 +592,7 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
let lookup_eliminator ind_sp s =
let kn,i = ind_sp in
- let mp,dp,l = repr_mind kn in
+ let mp,dp,l = KerName.repr (MutInd.canonical kn) in
let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
let id = add_suffix ind_id (elimination_suffix s) in
(* Try first to get an eliminator defined in the same section as the *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 8ddfeaf2f0..2a5e999651 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -18,7 +18,6 @@ open Inductive
open Util
open Nativecode
open Nativevalues
-open Nativelambda
open Context.Rel.Declaration
(** This module implements normalization by evaluation to OCaml code *)
@@ -390,16 +389,16 @@ let native_norm env sigma c ty =
let code, upd = mk_norm_code penv sigma prefix c in
match Nativelib.compile ml_filename code with
| true, fn ->
- if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ...");
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Running norm ...");
let t0 = Sys.time () in
Nativelib.call_linker ~fatal:true prefix fn (Some upd);
let t1 = Sys.time () in
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
- if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
let res = nf_val env !Nativelib.rt1 ty in
let t2 = Sys.time () in
let time_info = Format.sprintf "Reification done in %.5f@." (t2 -. t1) in
- if !Flags.debug then Pp.msg_debug (Pp.str time_info);
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
res
| _ -> anomaly (Pp.str "Compilation failure")
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 827071054a..d6305d81a8 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -348,7 +348,7 @@ let rec pat_of_raw metas vars = function
| GHole _ ->
PMeta None
| GCast (_,c,_) ->
- Pp.msg_warning (strbrk "Cast not taken into account in constr pattern");
+ Feedback.msg_warning (strbrk "Cast not taken into account in constr pattern");
pat_of_raw metas vars c
| GIf (_,c,(_,None),b1,b2) ->
PIf (pat_of_raw metas vars c,
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cf5b08c58f..b0715af734 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,15 +14,16 @@ open Type_errors
type unification_error =
| OccurCheck of existential_key * constr
- | NotClean of existential * env * constr
+ | NotClean of existential * env * constr (* Constr is a variable not in scope *)
| NotSameArgSize
| NotSameHead
| NoCanonicalStructure
- | ConversionFailed of env * constr * constr
+ | ConversionFailed of env * constr * constr (* Non convertible closed terms *)
| MetaOccurInBody of existential_key
| InstanceNotSameType of existential_key * env * types * types
| UnifUnivInconsistency of Univ.univ_inconsistency
| CannotSolveConstraint of Evd.evar_constraint * unification_error
+ | ProblemBeyondCapabilities
type position = (Id.t * Locus.hyp_location_flag) option
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index f617df9ee7..880f48e5f9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,6 +24,7 @@ type unification_error =
| InstanceNotSameType of existential_key * env * types * types
| UnifUnivInconsistency of Univ.univ_inconsistency
| CannotSolveConstraint of Evd.evar_constraint * unification_error
+ | ProblemBeyondCapabilities
type position = (Id.t * Locus.hyp_location_flag) option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8baa668c7b..378294c984 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -49,7 +49,7 @@ open Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.Val.t Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
type ltac_var_map = {
ltac_constrs : var_map;
ltac_uconstrs : uconstr_var_map;
@@ -143,7 +143,7 @@ let interp_universe_level_name evd (loc,s) =
with Not_found ->
try
let id = try Id.of_string s with _ -> raise Not_found in
- evd, Idmap.find id names
+ evd, snd (Idmap.find id names)
with Not_found ->
if not (is_strict_universe_declarations ()) then
new_univ_level_variable ~loc ~name:s univ_rigid evd
@@ -184,8 +184,7 @@ type inference_flags = {
}
let frozen_holes (sigma, sigma') =
- let fold evk _ accu = Evar.Set.add evk accu in
- Evd.fold_undefined fold sigma Evar.Set.empty
+ (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma)
let pending_holes (sigma, sigma') =
let fold evk _ accu =
@@ -194,7 +193,7 @@ let pending_holes (sigma, sigma') =
Evd.fold_undefined fold sigma' Evar.Set.empty
let apply_typeclasses env evdref frozen fail_evar =
- let filter_frozen evk = Evar.Set.mem evk frozen in
+ let filter_frozen = frozen in
evdref := Typeclasses.resolve_typeclasses
~filter:(if Flags.is_program_mode ()
then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk))
@@ -389,9 +388,12 @@ let pretype_id pretype k0 loc env evdref lvar id =
with Not_found ->
(* Check if [id] is a ltac variable not bound to a term *)
(* and build a nice error message *)
- if Id.Map.mem id lvar.ltac_genargs then
+ if Id.Map.mem id lvar.ltac_genargs then begin
+ let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
user_err_loc (loc,"",
- str "Variable " ++ pr_id id ++ str " should be bound to a term.");
+ str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+ bound to a " ++ Geninterp.Val.pr typ ++ str ".")
+ end;
(* Check if [id] is a section or goal variable *)
try
{ uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) }
@@ -1126,7 +1128,7 @@ let type_uconstr ?(flags = constr_flags)
ltac_constrs = closure.typed;
ltac_uconstrs = closure.untyped;
ltac_idents = closure.idents;
- ltac_genargs = ist.Geninterp.lfun;
+ ltac_genargs = Id.Map.empty;
} in
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = understand_ltac flags env sigma vars expected_type term in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 91320f20a5..824bb11aa4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -29,7 +29,7 @@ type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = Pattern.constr_under_binders Id.Map.t
type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t
-type unbound_ltac_var_map = Genarg.Val.t Id.Map.t
+type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t
type ltac_var_map = {
ltac_constrs : var_map;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6499ddd537..bbb6a92663 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -216,7 +216,7 @@ let compute_canonical_projections (con,ind) =
if Flags.is_verbose () then
(let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
- msg_warning (strbrk "No global reference exists for projection value"
+ Feedback.msg_warning (strbrk "No global reference exists for projection value"
++ Termops.print_constr t ++ strbrk " in instance "
++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
l
@@ -250,7 +250,7 @@ let open_canonical_structure i (_,o) =
and new_can_s = (Termops.print_constr s.o_DEF) in
let prj = (Nametab.pr_global_env Id.Set.empty proj)
and hd_val = (pr_cs_pattern cs_pat) in
- msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
+ Feedback.msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
++ strbrk " by " ++ prj ++ strbrk " in "
++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)) lo
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7f4249c5b6..79cb7a2f67 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -802,15 +802,16 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
let rec whrec cst_l (x, stack as s) =
let () = if !debug_RAKAM then
let open Pp in
- pp (h 0 (str "<<" ++ Termops.print_constr x ++
+ Feedback.msg_notice
+ (h 0 (str "<<" ++ Termops.print_constr x ++
str "|" ++ cut () ++ Cst_stack.pr cst_l ++
str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
str ">>") ++ fnl ())
in
let fold () =
let () = if !debug_RAKAM then
- let open Pp in pp (str "<><><><><>" ++ fnl ()) in
- if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else (s,cst_l)
+ let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
+ (s,cst_l)
in
match kind_of_term x with
| Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
@@ -1001,7 +1002,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold ()
| Sort _ | Ind _ | Prod _ -> fold ()
in
- whrec (Option.default Cst_stack.empty csts)
+ fun xs ->
+ let (s,cst_l as res) = whrec (Option.default Cst_stack.empty csts) xs in
+ if tactic_mode then (Stack.best_state s cst_l,Cst_stack.empty) else res
(** reduction machine without global env and refold machinery *)
let local_whd_state_gen flags sigma =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3a5796fe1b..3ff96cd72a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -25,7 +25,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
open Goptions
-let set_typeclasses_unique_solutions =
+let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a4a386530d..21cf5548f2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -657,7 +657,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
and cN = Evarutil.whd_head_evar sigma curn in
let () =
if !debug_unification then
- msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN)
+ Feedback.msg_debug (Termops.print_constr_env curenv cM ++ str" ~= " ++ Termops.print_constr_env curenv cN)
in
match (kind_of_term cM,kind_of_term cN) with
| Meta k1, Meta k2 ->
@@ -1054,12 +1054,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- if !debug_unification then msg_debug (str "Starting unification");
+ if !debug_unification then Feedback.msg_debug (str "Starting unification");
let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
try
let res =
- if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
- || subterm_restriction opt flags then None
+ if subterm_restriction opt flags ||
+ occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
+ then
+ None
else
let sigma, b = match flags.modulo_conv_on_closed_terms with
| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
@@ -1075,10 +1077,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
let a = match res with
| Some sigma -> sigma, ms, es
| None -> unirec_rec (env,0) cv_pb opt subst m n in
- if !debug_unification then msg_debug (str "Leaving unification with success");
+ if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
a
with e ->
- if !debug_unification then msg_debug (str "Leaving unification with failure");
+ if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
raise e
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 15:05:15 +0000