aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/pretyping.ml17
-rw-r--r--pretyping/reductionops.ml86
-rw-r--r--pretyping/reductionops.mli9
-rw-r--r--pretyping/typeclasses.ml6
-rw-r--r--pretyping/typeclasses.mli2
-rw-r--r--pretyping/typing.ml12
-rw-r--r--pretyping/typing.mli5
-rw-r--r--pretyping/unification.ml7
9 files changed, 95 insertions, 57 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index cd7ce89e0..b7fc2de95 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -316,7 +316,7 @@ let exact_ise_stack2 env evd f sk1 sk2 =
if Reductionops.Stack.compare_shape sk1 sk2 then
ise_stack2 evd (List.rev sk1) (List.rev sk2)
else UnifFailure (evd, (* Dummy *) NotSameHead)
-
+
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
let term2 = whd_head_evar evd term2 in
@@ -434,7 +434,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else quick_fail i
and delta i =
switch (evar_eqappr_x ts env i pbty) (apprF,cstsF)
- (whd_betaiota_deltazeta_for_iota_state (fst ts) env i cstsM (vM,skM))
+ (whd_betaiota_deltazeta_for_iota_state
+ (fst ts) env i cstsM (vM,skM))
in
let default i = ise_try i [f1; consume apprF apprM; delta]
in
@@ -451,7 +452,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
try
let termM' = Retyping.expand_projection env evd p c [] in
let apprM', cstsM' =
- whd_betaiota_deltazeta_for_iota_state (fst ts) env evd cstsM (termM',skM)
+ whd_betaiota_deltazeta_for_iota_state
+ (fst ts) env evd cstsM (termM',skM)
in
let delta' i =
switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM')
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 385e100e2..13e5ea97a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -349,21 +349,6 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
(* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
let allow_anonymous_refs = ref false
-(* Utilisé pour inférer le prédicat des Cases *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
-
-let evar_type_fixpoint loc env evdref lna lar vdefj =
- let lt = Array.length vdefj in
- if Int.equal (Array.length lar) lt then
- for i = 0 to lt-1 do
- if not (e_cumul env.ExtraEnv.env evdref (vdefj.(i)).uj_type
- (lift lt lar.(i))) then
- error_ill_typed_rec_body ~loc env.ExtraEnv.env !evdref
- i lna vdefj lar
- done
-
(* coerce to tycon if any *)
let inh_conv_coerce_to_tycon resolve_tc loc env evdref j = function
| None -> j
@@ -653,7 +638,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
- evar_type_fixpoint loc env evdref names ftys vdefj;
+ Typing.check_type_fixpoint loc env.ExtraEnv.env evdref names ftys vdefj;
let ftys = Array.map (nf_evar !evdref) ftys in
let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
let fixj = match fixkind with
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 7ee70d9e0..494d27178 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -26,6 +26,19 @@ exception Elimconst
their parameters in its stack.
*)
+let refolding_in_reduction = ref false
+let _ = Goptions.declare_bool_option {
+ Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optname =
+ "Perform refolding of fixpoints/constants like cbn during reductions";
+ Goptions.optkey = ["Refolding";"Reduction"];
+ Goptions.optread = (fun () -> !refolding_in_reduction);
+ Goptions.optwrite = (fun a -> refolding_in_reduction:=a);
+}
+
+let get_refolding_in_reduction () = !refolding_in_reduction
+let set_refolding_in_reduction = (:=) refolding_in_reduction
+
(** Machinery to custom the behavior of the reduction *)
module ReductionBehaviour = struct
open Globnames
@@ -623,16 +636,17 @@ let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
(* Beta Reduction tools *)
-let apply_subst recfun env cst_l t stack =
+let apply_subst recfun env refold cst_l t stack =
let rec aux env cst_l t stack =
match (Stack.decomp stack,kind_of_term t) with
| Some (h,stacktl), Lambda (_,_,c) ->
- aux (h::env) (Cst_stack.add_param h cst_l) c stacktl
+ let cst_l' = if refold then Cst_stack.add_param h cst_l else cst_l in
+ aux (h::env) cst_l' c stacktl
| _ -> recfun cst_l (substl env t, stack)
in aux env cst_l t stack
let stacklam recfun env t stack =
- apply_subst (fun _ -> recfun) env Cst_stack.empty t stack
+ apply_subst (fun _ -> recfun) env false Cst_stack.empty t stack
let beta_applist (c,l) =
stacklam Stack.zip [] c (Stack.append_app_list l Stack.empty)
@@ -697,11 +711,16 @@ let contract_cofix ?env ?reference (bodynum,(names,types,bodies as typedbodies))
substl closure bodies.(bodynum)
(** Similar to the "fix" case below *)
-let reduce_and_refold_cofix recfun env cst_l cofix sk =
- let raw_answer = contract_cofix ~env ?reference:(Cst_stack.reference cst_l) cofix in
+let reduce_and_refold_cofix recfun env refold cst_l cofix sk =
+ let raw_answer =
+ let env = if refold then Some env else None in
+ contract_cofix ?env ?reference:(Cst_stack.reference cst_l) cofix in
apply_subst
- (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkCoFix cofix) cst_l t,sk'))
- [] Cst_stack.empty raw_answer sk
+ (fun x (t,sk') ->
+ let t' =
+ if refold then Cst_stack.best_replace (mkCoFix cofix) cst_l t else t in
+ recfun x (t',sk'))
+ [] refold Cst_stack.empty raw_answer sk
let reduce_mind_case mia =
match kind_of_term mia.mconstr with
@@ -737,11 +756,18 @@ let contract_fix ?env ?reference ((recindices,bodynum),(names,types,bodies as ty
replace the fixpoint by the best constant from [cst_l]
Other rels are directly substituted by constants "magically found from the
context" in contract_fix *)
-let reduce_and_refold_fix recfun env cst_l fix sk =
- let raw_answer = contract_fix ~env ?reference:(Cst_stack.reference cst_l) fix in
+let reduce_and_refold_fix recfun env refold cst_l fix sk =
+ let raw_answer =
+ let env = if refold then None else Some env in
+ contract_fix ?env ?reference:(Cst_stack.reference cst_l) fix in
apply_subst
- (fun x (t,sk') -> recfun x (Cst_stack.best_replace (mkFix fix) cst_l t,sk'))
- [] Cst_stack.empty raw_answer sk
+ (fun x (t,sk') ->
+ let t' =
+ if refold then
+ Cst_stack.best_replace (mkFix fix) cst_l t
+ else t
+ in recfun x (t',sk'))
+ [] refold Cst_stack.empty raw_answer sk
let fix_recarg ((recindices,bodynum),_) stack =
assert (0 <= bodynum && bodynum < Array.length recindices);
@@ -781,7 +807,7 @@ let equal_stacks (x, l) (y, l') =
| None -> false
| Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2)
-let rec whd_state_gen ?csts tactic_mode flags env sigma =
+let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
let rec whrec cst_l (x, stack as s) =
let () = if !debug_RAKAM then
@@ -804,7 +830,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| _ -> fold ())
| Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
(match lookup_named id env with
- | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
+ | LocalDef (_,body,_) ->
+ whrec (if refold then Cst_stack.add_cst (mkVar id) cst_l else cst_l) (body, stack)
| _ -> fold ())
| Evar ev ->
(match safe_evar_value sigma ev with
@@ -819,7 +846,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
| None -> fold ()
| Some body ->
if not tactic_mode
- then whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
+ then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
+ (body, stack)
else (* Looks for ReductionBehaviour *)
match ReductionBehaviour.get (Globnames.ConstRef c) with
| None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack)
@@ -896,20 +924,20 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
Stack.append_app [|c|] bef,cst_l)::s'))
| LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
- apply_subst whrec [b] cst_l c stack
+ apply_subst whrec [b] refold cst_l c stack
| Cast (c,_,_) -> whrec cst_l (c, stack)
| App (f,cl) ->
whrec
- (Cst_stack.add_args cl cst_l)
+ (if refold then Cst_stack.add_args cl cst_l else cst_l)
(f, Stack.append_app cl stack)
| Lambda (na,t,c) ->
(match Stack.decomp stack with
| Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
- apply_subst whrec [] cst_l x stack
+ apply_subst whrec [] refold cst_l x stack
| None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
let env' = push_rel (LocalAssum (na,t)) env in
- let whrec' = whd_state_gen tactic_mode flags env' sigma in
- (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with
+ let whrec' = whd_state_gen ~refold ~tactic_mode flags env' sigma in
+ (match kind_of_term (Stack.zip ~refold (fst (whrec' (c, Stack.empty)))) with
| App (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
@@ -945,7 +973,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
|args, (Stack.Fix (f,s',cst_l)::s'') when use_fix ->
let x' = Stack.zip(x,args) in
let out_sk = s' @ (Stack.append_app [|x'|] s'') in
- reduce_and_refold_fix whrec env cst_l f out_sk
+ reduce_and_refold_fix whrec env refold cst_l f out_sk
|args, (Stack.Cst (const,curr,remains,s',cst_l) :: s'') ->
let x' = Stack.zip(x,args) in
begin match remains with
@@ -955,7 +983,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
(match constant_opt_value_in env const with
| None -> fold ()
| Some body ->
- whrec (Cst_stack.add_cst (mkConstU const) cst_l)
+ whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l)
(body, s' @ (Stack.append_app [|x'|] s'')))
| Stack.Cst_proj p ->
let pb = lookup_projection p env in
@@ -981,7 +1009,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
match Stack.strip_app stack with
|args, ((Stack.Case _ |Stack.Proj _)::s') ->
- reduce_and_refold_cofix whrec env cst_l cofix stack
+ reduce_and_refold_cofix whrec env refold cst_l cofix stack
|_ -> fold ()
else fold ()
@@ -1073,7 +1101,7 @@ let local_whd_state_gen flags sigma =
whrec
let raw_whd_state_gen flags env =
- let f sigma s = fst (whd_state_gen false flags env sigma s) in
+ let f sigma s = fst (whd_state_gen (get_refolding_in_reduction ()) false flags env sigma s) in
f
let stack_red_of_state_red f =
@@ -1083,7 +1111,7 @@ let stack_red_of_state_red f =
(* Drops the Cst_stack *)
let iterate_whd_gen refold flags env sigma s =
let rec aux t =
- let (hd,sk),_ = whd_state_gen refold flags env sigma (t,Stack.empty) in
+ let (hd,sk),_ = whd_state_gen refold false flags env sigma (t,Stack.empty) in
let whd_sk = Stack.map aux sk in
Stack.zip ~refold (hd,whd_sk)
in aux s
@@ -1468,19 +1496,21 @@ let is_sort env sigma t =
of case/fix (heuristic used by evar_conv) *)
let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
+ let refold = get_refolding_in_reduction () in
+ let tactic_mode = false in
let rec whrec csts s =
- let (t, stack as s),csts' = whd_state_gen ~csts false CClosure.betaiota env sigma s in
+ let (t, stack as s),csts' = whd_state_gen ~csts ~refold ~tactic_mode CClosure.betaiota env sigma s in
match Stack.strip_app stack with
|args, (Stack.Case _ :: _ as stack') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+ let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
|args, (Stack.Fix _ :: _ as stack') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+ let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
|args, (Stack.Proj (n,m,p,_) :: stack'') ->
- let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
+ let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' ~refold ~tactic_mode
(CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
if isConstruct t_o then
whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 874ea6815..4cd7a2a86 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -28,6 +28,11 @@ module ReductionBehaviour : sig
val print : Globnames.global_reference -> Pp.std_ppcmds
end
+(** Option telling if reduction should use the refolding machinery of cbn
+ (off by default) *)
+val get_refolding_in_reduction : unit -> bool
+val set_refolding_in_reduction : bool -> unit
+
(** {6 Machinery about a stack of unfolded constant }
cst applied to params must convertible to term of the state applied to args
@@ -134,8 +139,8 @@ val stack_reduction_of_reduction :
i*)
val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
-val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds ->
- Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
+val whd_state_gen : ?csts:Cst_stack.t -> refold:bool -> tactic_mode:bool ->
+ CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4c33a9c78..4207eccb9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -501,7 +501,7 @@ let is_resolvable evi =
Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- if is_resolvable evi = b then evi
+ if is_resolvable evi == (b : bool) then evi
else
let t = set_resolvable evi.evar_extra b in
{ evi with evar_extra = t }
@@ -548,7 +548,7 @@ let solve_all_instances env evd filter unique split fail =
(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
-let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
- if not (has_typeclasses filter evd) then evd
+ if fast_path && not (has_typeclasses filter evd) then evd
else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 25460ef7d..2530f5dfa 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -101,7 +101,7 @@ val mark_resolvable : evar_info -> evar_info
val is_class_evar : evar_map -> evar_info -> bool
val is_class_type : evar_map -> types -> bool
-val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 696d419af..e79e3d46f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -126,6 +126,16 @@ let e_judge_of_case env evdref ci pj cj lfj =
{ uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj);
uj_type = rslty }
+let check_type_fixpoint loc env evdref lna lar vdefj =
+ let lt = Array.length vdefj in
+ if Int.equal (Array.length lar) lt then
+ for i = 0 to lt-1 do
+ if not (Evarconv.e_cumul env evdref (vdefj.(i)).uj_type
+ (lift lt lar.(i))) then
+ Pretype_errors.error_ill_typed_rec_body ~loc env !evdref
+ i lna vdefj lar
+ done
+
(* FIXME: might depend on the level of actual parameters!*)
let check_allowed_sort env sigma ind c p =
let pj = Retyping.get_judgment_of env sigma p in
@@ -263,7 +273,7 @@ and execute_recdef env evdref (names,lar,vdef) =
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 evdref vdef in
let vdefv = Array.map j_val vdefj in
- let _ = type_fixpoint env1 names lara vdefj in
+ let _ = check_type_fixpoint Loc.ghost env1 evdref names lara vdefj in
(names,lara,vdefv)
and execute_array env evdref = Array.map (execute env evdref)
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index e524edcca..04e5e40bc 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -39,3 +39,8 @@ val e_solve_evars : env -> evar_map ref -> constr -> constr
(** (first constr is term to match, second is return predicate) *)
val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr ->
unit
+
+(** Raise an error message if bodies have types not unifiable with the
+ expected ones *)
+val check_type_fixpoint : Loc.t -> env -> evar_map ref ->
+ Names.Name.t array -> types array -> unsafe_judgment array -> unit
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8feb34e3e..594732a5a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -480,8 +480,8 @@ let unfold_projection env p stk =
let expand_key ts env sigma = function
| Some (IsKey k) -> expand_table_key env k
| Some (IsProj (p, c)) ->
- let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
- Cst_stack.empty (c, unfold_projection env p [])))
+ let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
+ Cst_stack.empty (c, unfold_projection env p [])))
in if Term.eq_constr (mkProj (p, c)) red then None else Some red
| None -> None
@@ -573,7 +573,8 @@ let constr_cmp pb sigma flags t u =
else sigma, b
let do_reduce ts (env, nb) sigma c =
- Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty)))
+ Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state
+ ts env sigma Cst_stack.empty (c, Stack.empty)))
let use_full_betaiota flags =
flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:08:09 +0000