aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml161
1 files changed, 92 insertions, 69 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 7544ba37a..64d837f0c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -416,8 +416,15 @@ let expand_key ts env sigma = function
with RetypeError _ -> None)
| None -> None
-let subterm_restriction is_subterm flags =
- not is_subterm && flags.restrict_conv_on_strict_subterms
+
+type unirec_flags = {
+ at_top: bool;
+ with_types: bool;
+ with_cs : bool;
+}
+
+let subterm_restriction opt flags =
+ not opt.at_top && flags.restrict_conv_on_strict_subterms
let key_of env b flags f =
if subterm_restriction b flags then None else
@@ -542,8 +549,18 @@ let eta_constructor_app env f l1 term =
| _ -> assert false)
| _ -> assert false
+let debug_unification = ref (false)
+let _ = Goptions.declare_bool_option {
+ Goptions.optsync = true; Goptions.optdepr = false;
+ Goptions.optname =
+ "Print states sent to w_unify unification";
+ Goptions.optkey = ["Debug";"Tactic";"Unification"];
+ Goptions.optread = (fun () -> !debug_unification);
+ Goptions.optwrite = (fun a -> debug_unification:=a);
+}
+
let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n =
- let rec unirec_rec (curenv,nb as curenvnb) pb b wt ((sigma,metasubst,evarsubst) as substn) curm curn =
+ let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn =
let cM = Evarutil.whd_head_evar sigma curm
and cN = Evarutil.whd_head_evar sigma curn in
let () =
@@ -555,7 +572,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
if Int.equal k1 k2 then substn else
let stM,stN = extract_instance_status pb in
let sigma =
- if wt && flags.check_applied_meta_types then
+ if opt.with_types && flags.check_applied_meta_types then
let tyM = Typing.meta_type sigma k1 in
let tyN = Typing.meta_type sigma k2 in
let l, r = if k2 < k1 then tyN, tyM else tyM, tyN in
@@ -567,7 +584,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| Meta k, _
when not (dependent cM cN) (* helps early trying alternatives *) ->
let sigma =
- if wt && flags.check_applied_meta_types then
+ if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = Typing.meta_type sigma k in
let tyN = get_type_of curenv ~lax:true sigma cN in
@@ -587,7 +604,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| _, Meta k
when not (dependent cN cM) (* helps early trying alternatives *) ->
let sigma =
- if wt && flags.check_applied_meta_types then
+ if opt.with_types && flags.check_applied_meta_types then
(try
let tyM = get_type_of curenv ~lax:true sigma cM in
let tyN = Typing.meta_type sigma k in
@@ -629,20 +646,21 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
error_cannot_unify curenv sigma (m,n))
| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
- unirec_rec (push (na,t1) curenvnb) CONV true wt
- (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
+ unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true}
+ (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
| Prod (na,t1,c1), Prod (_,t2,c2) ->
- unirec_rec (push (na,t1) curenvnb) pb true false
- (unirec_rec curenvnb CONV true false substn t1 t2) c1 c2
- | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b wt substn (subst1 a c) cN
- | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b wt substn cM (subst1 a c)
+ unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true}
+ (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2
+ | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN
+ | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c)
(** Fast path for projections. *)
| Proj (p1,c1), Proj (p2,c2) when eq_constant
(Projection.constant p1) (Projection.constant p2) ->
- (try unify_same_proj curenvnb cv_pb true wt substn c1 c2
+ (try unify_same_proj curenvnb cv_pb {opt with at_top = true}
+ substn c1 c2
with ex when precatchable_exception ex ->
- unify_not_same_head curenvnb pb b wt substn cM cN)
+ unify_not_same_head curenvnb pb opt substn cM cN)
| Proj (p1,c1), _ when not (Projection.unfolded p1) ->
let cM' =
@@ -652,7 +670,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
to FO and eta in particular, fail gracefully in that case *)
error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- unirec_rec curenvnb CONV true false substn cM' cN
+ unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM' cN
| _, Proj (p2,c2) when not (Projection.unfolded p2) ->
let cN' =
@@ -662,43 +680,44 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
to FO and eta in particular, fail gracefully in that case *)
error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- unirec_rec curenvnb CONV true false substn cM cN'
+ unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn cM cN'
(* eta-expansion *)
| Lambda (na,t1,c1), _ when flags.modulo_eta ->
- unirec_rec (push (na,t1) curenvnb) CONV true wt substn
+ unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn
c1 (mkApp (lift 1 cN,[|mkRel 1|]))
| _, Lambda (na,t2,c2) when flags.modulo_eta ->
- unirec_rec (push (na,t2) curenvnb) CONV true wt substn
+ unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn
(mkApp (lift 1 cM,[|mkRel 1|])) c2
(* For records *)
| App (f1, l1), _ when flags.modulo_eta && is_eta_constructor_app curenv f1 l1 ->
(try let l1', l2' = eta_constructor_app curenv f1 l1 cN in
Array.fold_left2
- (unirec_rec curenvnb CONV true wt) substn l1' l2'
+ (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2'
with ex when precatchable_exception ex ->
(match kind_of_term cN with
- | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
- | _ -> unify_not_same_head curenvnb pb b wt substn cM cN))
+ | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+ | _ -> unify_not_same_head curenvnb pb opt substn cM cN))
| _, App (f2, l2) when flags.modulo_eta && is_eta_constructor_app curenv f2 l2 ->
(try let l2', l1' = eta_constructor_app curenv f2 l2 cM in
Array.fold_left2
- (unirec_rec curenvnb CONV true wt) substn l1' l2'
+ (unirec_rec curenvnb CONV {opt with at_top = true; with_cs = false}) substn l1' l2'
with ex when precatchable_exception ex ->
(match kind_of_term cM with
- | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
- | _ -> unify_not_same_head curenvnb pb b wt substn cM cN))
+ | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+ | _ -> unify_not_same_head curenvnb pb opt substn cM cN))
| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
(try
- Array.fold_left2 (unirec_rec curenvnb CONV true wt)
- (unirec_rec curenvnb CONV true false
- (unirec_rec curenvnb CONV true false substn p1 p2) c1 c2)
+ let opt' = {opt with at_top = true; with_types = false} in
+ Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true})
+ (unirec_rec curenvnb CONV opt'
+ (unirec_rec curenvnb CONV opt' substn p1 p2) c1 c2)
cl1 cl2
with ex when precatchable_exception ex ->
- reduce curenvnb pb b wt substn cM cN)
+ reduce curenvnb pb opt substn cM cN)
| App (f1,l1), _ when
(isMeta f1 && use_metas_pattern_unification flags nb l1
@@ -708,8 +727,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
with
| None ->
(match kind_of_term cN with
- | App (f2,l2) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
- | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)
+ | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+ | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
| Some l ->
solve_pattern_eqn_array curenvnb f1 l cN substn)
@@ -721,18 +740,18 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
with
| None ->
(match kind_of_term cM with
- | App (f1,l1) -> unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
- | _ -> unify_not_same_head curenvnb pb b wt substn cM cN)
+ | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
+ | _ -> unify_not_same_head curenvnb pb opt substn cM cN)
| Some l ->
solve_pattern_eqn_array curenvnb f2 l cM substn)
| App (f1,l1), App (f2,l2) ->
- unify_app curenvnb pb b substn cM f1 l1 cN f2 l2
+ unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2
| _ ->
- unify_not_same_head curenvnb pb b wt substn cM cN
+ unify_not_same_head curenvnb pb opt substn cM cN
- and unify_app (curenv, nb as curenvnb) pb b (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
+ and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
try
let expand_proj c l =
match kind_of_term c with
@@ -745,18 +764,20 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
in
let f1, l1 = expand_proj f1 l1 in
let f2, l2 = expand_proj f2 l2 in
+ let opta = {opt with at_top = true; with_types = false} in
+ let optf = {opt with at_top = true; with_types = true} in
let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
- Array.fold_left2 (unirec_rec curenvnb CONV true false)
- (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
+ Array.fold_left2 (unirec_rec curenvnb CONV opta)
+ (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2
with ex when precatchable_exception ex ->
- try reduce curenvnb pb b false substn cM cN
+ try reduce curenvnb pb {opt with with_types = false} substn cM cN
with ex when precatchable_exception ex ->
- try canonical_projections curenvnb pb b cM cN substn
+ try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
- expand curenvnb pb b false substn cM f1 l1 cN f2 l2
+ expand curenvnb pb {opt with with_types = false} substn cM f1 l1 cN f2 l2
- and unify_same_proj (curenv, nb as curenvnb) cv_pb b wt substn c1 c2 =
- let substn = unirec_rec curenvnb CONV b wt substn c1 c2 in
+ and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 =
+ let substn = unirec_rec curenvnb CONV opt substn c1 c2 in
try (* Force unification of the types to fill in parameters *)
let ty1 = get_type_of curenv ~lax:true sigma c1 in
let ty2 = get_type_of curenv ~lax:true sigma c2 in
@@ -768,33 +789,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
ty1 ty2
with RetypeError _ -> substn
- and unify_not_same_head curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
- try canonical_projections curenvnb pb b cM cN substn
+ and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn) cM cN =
+ try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
let sigma', b = constr_cmp cv_pb sigma flags cM cN in
if b then (sigma', metas, evars)
else
- try reduce curenvnb pb b wt substn cM cN
+ try reduce curenvnb pb opt substn cM cN
with ex when precatchable_exception ex ->
let (f1,l1) =
match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
let (f2,l2) =
match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
- expand curenvnb pb b wt substn cM f1 l1 cN f2 l2
+ expand curenvnb pb opt substn cM f1 l1 cN f2 l2
- and reduce curenvnb pb b wt (sigma, metas, evars as substn) cM cN =
- if use_full_betaiota flags && not (subterm_restriction b flags) then
+ and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN =
+ if use_full_betaiota flags && not (subterm_restriction opt flags) then
let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
if not (Term.eq_constr cM cM') then
- unirec_rec curenvnb pb b wt substn cM' cN
+ unirec_rec curenvnb pb opt substn cM' cN
else
let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in
if not (Term.eq_constr cN cN') then
- unirec_rec curenvnb pb b wt substn cM cN'
+ unirec_rec curenvnb pb opt substn cM cN'
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
- and expand (curenv,_ as curenvnb) pb b wt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 =
+ and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 =
let res =
(* Try full conversion on meta-free terms. *)
(* Back to 1995 (later on called trivial_unify in 2002), the
@@ -808,7 +829,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
(it is used by apply and rewrite); it might now be redundant
with the support for delta-expansion (which is used
essentially for apply)... *)
- if subterm_restriction b flags then None else
+ if subterm_restriction opt flags then None else
match flags.modulo_conv_on_closed_terms with
| None -> None
| Some convflags ->
@@ -830,48 +851,48 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
match res with
| Some substn -> substn
| None ->
- let cf1 = key_of curenv b flags f1 and cf2 = key_of curenv b flags f2 in
+ let cf1 = key_of curenv opt flags f1 and cf2 = key_of curenv opt flags f2 in
match oracle_order curenv cf1 cf2 with
| None -> error_cannot_unify curenv sigma (cM,cN)
| Some true ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
- unirec_rec curenvnb pb b wt substn
+ unirec_rec curenvnb pb opt substn
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
- unirec_rec curenvnb pb b wt substn cM
+ unirec_rec curenvnb pb opt substn cM
(whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key flags.modulo_delta curenv sigma cf2 with
| Some c ->
- unirec_rec curenvnb pb b wt substn cM
+ unirec_rec curenvnb pb opt substn cM
(whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
(match expand_key flags.modulo_delta curenv sigma cf1 with
| Some c ->
- unirec_rec curenvnb pb b wt substn
+ unirec_rec curenvnb pb opt substn
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
- and canonical_projections (curenv, _ as curenvnb) pb b cM cN (sigma,_,_ as substn) =
+ and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp cM then
let f1l1 = whd_nored_state sigma (cM,Stack.empty) in
if is_open_canonical_projection curenv sigma f1l1 then
let f2l2 = whd_nored_state sigma (cN,Stack.empty) in
- solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
+ solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- if
+ if not opt.with_cs ||
begin match flags.modulo_conv_on_closed_terms with
| None -> true
- | Some _ -> subterm_restriction b flags
+ | Some _ -> subterm_restriction opt flags
end then
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else
@@ -880,11 +901,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
let f2l2 = whd_nored_state sigma (cN, Stack.empty) in
if is_open_canonical_projection curenv sigma f2l2 then
let f1l1 = whd_nored_state sigma (cM, Stack.empty) in
- solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
+ solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
- and solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 (sigma,ms,es) =
+ and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
try Evarconv.check_conv_record f1l1 f2l2
with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
@@ -901,24 +922,26 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
(sigma,[],List.length bs - 1) bs
in
try
+ let opt' = {opt with with_types = false} in
let (substn,_,_) = Reductionops.Stack.fold2
- (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+ (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
(evd,ms,es) us2 us in
let (substn,_,_) = Reductionops.Stack.fold2
- (fun s u1 u -> unirec_rec curenvnb pb b false s u1 (substl ks u))
+ (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
substn params1 params in
- let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb b false) substn ts ts1 in
+ let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt') substn ts ts1 in
let app = mkApp (c, Array.rev_of_list ks) in
(* let substn = unirec_rec curenvnb pb b false substn t cN in *)
- unirec_rec curenvnb pb b false substn c1 app
+ unirec_rec curenvnb pb opt' substn c1 app
with Invalid_argument "Reductionops.Stack.fold2" ->
error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
+ let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
let res =
if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n
- || subterm_restriction conv_at_top flags then None
+ || subterm_restriction opt flags 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
@@ -933,7 +956,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
in
match res with
| Some sigma -> sigma, ms, es
- | None -> unirec_rec (env,0) cv_pb conv_at_top false subst m n
+ | None -> unirec_rec (env,0) cv_pb opt subst m n
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-26 22:47:01 +0000