diff options
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 365 |
1 files changed, 183 insertions, 182 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2764633b..58951302 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarconv.ml 9665 2007-02-21 17:08:10Z herbelin $ *) +(* $Id: evarconv.ml 11157 2008-06-21 10:45:51Z herbelin $ *) open Pp open Util @@ -43,55 +43,28 @@ let eval_flexible_term env c = match kind_of_term c with | Const c -> constant_opt_value env c | Rel n -> - (try let (_,v,_) = lookup_rel n env in option_map (lift n) v + (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v with Not_found -> None) | Var id -> (try let (_,v,_) = lookup_named id env in v with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c | _ -> assert false -(* -let rec apprec_nobeta env sigma s = - let (t,stack as s) = whd_state s in - match kind_of_term (fst s) with - | Case (ci,p,d,lf) -> - let (cr,crargs) = whd_betadeltaiota_stack env sigma d in - let rslt = mkCase (ci, p, applist (cr,crargs), lf) in - if reducible_mind_case cr then - apprec_nobeta env sigma (rslt, stack) - else - s - | Fix fix -> - (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with - | Reduced s -> apprec_nobeta env sigma s - | NotReducible -> s) - | _ -> s - -let evar_apprec_nobeta env isevars stack c = - let rec aux s = - let (t,stack as s') = apprec_nobeta env (evars_of isevars) s in - match kind_of_term t with - | Evar (n,_ as ev) when Evd.is_defined (evars_of isevars) n -> - aux (Evd.existential_value (evars_of isevars) ev, stack) - | _ -> (t, list_of_stack stack) - in aux (c, append_stack (Array.of_list stack) empty_stack) -*) -let evar_apprec env isevars stack c = - let sigma = evars_of isevars in +let evar_apprec env evd stack c = + let sigma = evars_of evd in let rec aux s = - let (t,stack) = Reductionops.apprec env sigma s in + let (t,stack) = whd_betaiota_deltazeta_for_iota_state env sigma s in match kind_of_term t with - | Evar (n,_ as ev) when Evd.is_defined sigma n -> + | Evar (evk,_ as ev) when Evd.is_defined sigma evk -> aux (Evd.existential_value sigma ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack_list stack empty_stack) -let apprec_nohdbeta env isevars c = - let (t,stack as s) = Reductionops.whd_stack c in - match kind_of_term t with - | (Case _ | Fix _) -> evar_apprec env isevars [] c - | _ -> s +let apprec_nohdbeta env evd c = + match kind_of_term (fst (Reductionops.whd_stack c)) with + | (Case _ | Fix _) -> applist (evar_apprec env evd [] c) + | _ -> c (* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem (t1 l1) = (t2 l2) into a problem @@ -116,84 +89,96 @@ let apprec_nohdbeta env isevars c = let check_conv_record (t1,l1) (t2,l2) = try let proji = global_of_constr t1 in - let cstr = global_of_constr t2 in - let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = - lookup_canonical_conversion (proji, cstr) in + let canon_s,l2_effective = + try + match kind_of_term t2 with + Prod (_,a,b) -> (* assert (l2=[]); *) + if dependent (mkRel 1) b then raise Not_found + else lookup_canonical_conversion (proji, Prod_cs),[a;pop b] + | Sort s -> + lookup_canonical_conversion + (proji, Sort_cs (family_of_sort s)),[] + | _ -> + let c2 = try global_of_constr t2 with _ -> raise Not_found in + lookup_canonical_conversion (proji, Const_cs c2),l2 + with Not_found -> + lookup_canonical_conversion (proji,Default_cs),[] + in + let { o_DEF = c; o_INJ=n; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } + = canon_s in let params1, c1, extra_args1 = match list_chop (List.length params) l1 with | params1, c1::extra_args1 -> params1, c1, extra_args1 | _ -> assert false in - let us2,extra_args2 = list_chop (List.length us) l2 in - c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1 + let us2,extra_args2 = list_chop (List.length us) l2_effective in + c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1, + (n,applist(t2,l2)) with _ -> raise Not_found (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) -let rec ise_try isevars = function +let rec ise_try evd = function [] -> assert false - | [f] -> f isevars + | [f] -> f evd | f1::l -> - let (isevars',b) = f1 isevars in - if b then (isevars',b) else ise_try isevars l + let (evd',b) = f1 evd in + if b then (evd',b) else ise_try evd l -let ise_and isevars l = +let ise_and evd l = let rec ise_and i = function [] -> assert false | [f] -> f i | f1::l -> let (i',b) = f1 i in - if b then ise_and i' l else (isevars,false) in - ise_and isevars l + if b then ise_and i' l else (evd,false) in + ise_and evd l -let ise_list2 isevars f l1 l2 = +let ise_list2 evd f l1 l2 = let rec ise_list2 i l1 l2 = match l1,l2 with [], [] -> (i, true) | [x], [y] -> f i x y | x::l1, y::l2 -> let (i',b) = f i x y in - if b then ise_list2 i' l1 l2 else (isevars,false) - | _ -> (isevars, false) in - ise_list2 isevars l1 l2 + if b then ise_list2 i' l1 l2 else (evd,false) + | _ -> (evd, false) in + ise_list2 evd l1 l2 -let ise_array2 isevars f v1 v2 = +let ise_array2 evd f v1 v2 = let rec allrec i = function | -1 -> (i,true) | n -> let (i',b) = f i v1.(n) v2.(n) in - if b then allrec i' (n-1) else (isevars,false) + if b then allrec i' (n-1) else (evd,false) in let lv1 = Array.length v1 in - if lv1 = Array.length v2 then allrec isevars (pred lv1) - else (isevars,false) + if lv1 = Array.length v2 then allrec evd (pred lv1) + else (evd,false) -let rec evar_conv_x env isevars pbty term1 term2 = - let sigma = evars_of isevars in +let rec evar_conv_x env evd pbty term1 term2 = + let sigma = evars_of evd in let term1 = whd_castappevar sigma term1 in let term2 = whd_castappevar sigma term2 in -(* - if eq_constr term1 term2 then - true - else -*) (* Maybe convertible but since reducing can erase evars which [evar_apprec] could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) - if is_ground_term isevars term1 && is_ground_term isevars term2 & - is_fconv pbty env (evars_of isevars) term1 term2 then - (isevars,true) - else if is_undefined_evar isevars term1 then - solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) - else if is_undefined_evar isevars term2 then - solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term2,term1) - else - let (t1,l1) = apprec_nohdbeta env isevars term1 in - let (t2,l2) = apprec_nohdbeta env isevars term2 in - evar_eqappr_x env isevars pbty (t1,l1) (t2,l2) - -and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = + if is_ground_term evd term1 && is_ground_term evd term2 & + is_fconv pbty env (evars_of evd) term1 term2 + then + (evd,true) + else + let term1 = apprec_nohdbeta env evd term1 in + let term2 = apprec_nohdbeta env evd term2 in + if is_undefined_evar evd term1 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2) + else if is_undefined_evar evd term2 then + solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1) + else + evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2) + +and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = (* Evar must be undefined since we have whd_ised *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -215,25 +200,25 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = and f2 i = if sp1 = sp2 then ise_and i - [(fun i -> ise_array2 i - (fun i -> evar_conv_x env i CONV) al1 al2); - (fun i -> ise_list2 i - (fun i -> evar_conv_x env i CONV) l1 l2)] + [(fun i -> ise_list2 i + (fun i -> evar_conv_x env i CONV) l1 l2); + (fun i -> solve_refl evar_conv_x env i sp1 al1 al2, + true)] else (i,false) in - ise_try isevars [f1; f2] + ise_try evd [f1; f2] | Flexible ev1, MaybeFlexible flex2 -> let f1 i = if - is_unification_pattern_evar ev1 l1 & - not (occur_evar (fst ev1) (applist (term2,l2))) + is_unification_pattern_evar env ev1 l1 & + not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in + let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) else if List.length l1 <= List.length l2 then @@ -253,19 +238,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) | None -> (i,false) in - ise_try isevars [f1; f4] + ise_try evd [f1; f4] | MaybeFlexible flex1, Flexible ev2 -> let f1 i = if - is_unification_pattern_evar ev2 l2 & - not (occur_evar (fst ev2) (applist (term1,l1))) + is_unification_pattern_evar env ev2 l2 & + not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in + let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) else if List.length l2 <= List.length l1 then @@ -284,7 +269,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 | None -> (i,false) in - ise_try isevars [f1; f4] + ise_try evd [f1; f4] | MaybeFlexible flex1, MaybeFlexible flex2 -> let f2 i = @@ -313,36 +298,36 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 | None -> (i,false) in - ise_try isevars [f2; f3; f4] + ise_try evd [f2; f3; f4] | Flexible ev1, Rigid _ -> if - is_unification_pattern_evar ev1 l1 & - not (occur_evar (fst ev1) (applist (term2,l2))) + is_unification_pattern_evar env ev1 l1 & + not (occur_evar (fst ev1) (applist appr2)) then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t2 = nf_evar (evars_of isevars) (applist(term2,l2)) in + let t2 = nf_evar (evars_of evd) (applist appr2) in let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn evar_conv_x env isevars (pbty,ev1,t2) + solve_simple_eqn evar_conv_x env evd (pbty,ev1,t2) else (* Postpone the use of an heuristic *) - add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars, + add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true | Rigid _, Flexible ev2 -> if - is_unification_pattern_evar ev2 l2 & - not (occur_evar (fst ev2) (applist (term1,l1))) + is_unification_pattern_evar env ev2 l2 & + not (occur_evar (fst ev2) (applist appr1)) then (* Miller-Pfenning's patterns unification *) (* Preserve generality (except that CCI has no eta-conversion) *) - let t1 = nf_evar (evars_of isevars) (applist(term1,l1)) in + let t1 = nf_evar (evars_of evd) (applist appr1) in let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn evar_conv_x env isevars (pbty,ev2,t1) + solve_simple_eqn evar_conv_x env evd (pbty,ev2,t1) else (* Postpone the use of an heuristic *) - add_conv_pb (pbty,env,applist(term1,l1),applist(term2,l2)) isevars, + add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true | MaybeFlexible flex1, Rigid _ -> @@ -355,7 +340,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_eqappr_x env i pbty (evar_apprec env i l1 v1) appr2 | None -> (i,false) in - ise_try isevars [f3; f4] + ise_try evd [f3; f4] | Rigid _ , MaybeFlexible flex2 -> let f3 i = @@ -367,19 +352,19 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = evar_eqappr_x env i pbty appr1 (evar_apprec env i l2 v2) | None -> (i,false) in - ise_try isevars [f3; f4] + ise_try evd [f3; f4] | Rigid c1, Rigid c2 -> match kind_of_term c1, kind_of_term c2 with - | Cast (c1,_,_), _ -> evar_eqappr_x env isevars pbty (c1,l1) appr2 + | Cast (c1,_,_), _ -> evar_eqappr_x env evd pbty (c1,l1) appr2 - | _, Cast (c2,_,_) -> evar_eqappr_x env isevars pbty appr1 (c2,l2) + | _, Cast (c2,_,_) -> evar_eqappr_x env evd pbty appr1 (c2,l2) | Sort s1, Sort s2 when l1=[] & l2=[] -> - (isevars,base_sort_cmp pbty s1 s2) + (evd,base_sort_cmp pbty s1 s2) | Lambda (na,c1,c'1), Lambda (_,c2,c'2) when l1=[] & l2=[] -> - ise_and isevars + ise_and evd [(fun i -> evar_conv_x env i CONV c1 c2); (fun i -> let c = nf_evar (evars_of i) c1 in @@ -400,18 +385,18 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = and appr2 = evar_apprec env i l2 (subst1 b2 c'2) in evar_eqappr_x env i pbty appr1 appr2 in - ise_try isevars [f1; f2] + ise_try evd [f1; f2] | LetIn (_,b1,_,c'1), _ ->(* On fait commuter les args avec le Let *) - let appr1 = evar_apprec env isevars l1 (subst1 b1 c'1) - in evar_eqappr_x env isevars pbty appr1 appr2 + let appr1 = evar_apprec env evd l1 (subst1 b1 c'1) + in evar_eqappr_x env evd pbty appr1 appr2 | _, LetIn (_,b2,_,c'2) -> - let appr2 = evar_apprec env isevars l2 (subst1 b2 c'2) - in evar_eqappr_x env isevars pbty appr1 appr2 + let appr2 = evar_apprec env evd l2 (subst1 b2 c'2) + in evar_eqappr_x env evd pbty appr1 appr2 | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> - ise_and isevars + ise_and evd [(fun i -> evar_conv_x env i CONV c1 c2); (fun i -> let c = nf_evar (evars_of i) c1 in @@ -419,16 +404,16 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Ind sp1, Ind sp2 -> if sp1=sp2 then - ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2 - else (isevars, false) + ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2 + else (evd, false) | Construct sp1, Construct sp2 -> if sp1=sp2 then - ise_list2 isevars (fun i -> evar_conv_x env i CONV) l1 l2 - else (isevars, false) + ise_list2 evd (fun i -> evar_conv_x env i CONV) l1 l2 + else (evd, false) | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - ise_and isevars + ise_and evd [(fun i -> evar_conv_x env i CONV p1 p2); (fun i -> evar_conv_x env i CONV c1 c2); (fun i -> ise_array2 i @@ -437,7 +422,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) -> if li1=li2 then - ise_and isevars + ise_and evd [(fun i -> ise_array2 i (fun i -> evar_conv_x env i CONV) tys1 tys2); (fun i -> ise_array2 i @@ -445,10 +430,10 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)] - else (isevars,false) + else (evd,false) | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> if i1=i2 then - ise_and isevars + ise_and evd [(fun i -> ise_array2 i (fun i -> evar_conv_x env i CONV) tys1 tys2); (fun i -> ise_array2 i @@ -456,30 +441,31 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = bds1 bds2); (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) l1 l2)] - else (isevars,false) + else (evd,false) - | (Meta _ | Lambda _), _ -> (isevars,false) - | _, (Meta _ | Lambda _) -> (isevars,false) + | (Meta _ | Lambda _), _ -> (evd,false) + | _, (Meta _ | Lambda _) -> (evd,false) - | (Ind _ | Construct _ | Sort _ | Prod _), _ -> (isevars,false) - | _, (Ind _ | Construct _ | Sort _ | Prod _) -> (isevars,false) + | (Ind _ | Construct _ | Sort _ | Prod _), _ -> (evd,false) + | _, (Ind _ | Construct _ | Sort _ | Prod _) -> (evd,false) | (App _ | Case _ | Fix _ | CoFix _), - (App _ | Case _ | Fix _ | CoFix _) -> (isevars,false) + (App _ | Case _ | Fix _ | CoFix _) -> (evd,false) | (Rel _ | Var _ | Const _ | Evar _), _ -> assert false | _, (Rel _ | Var _ | Const _ | Evar _) -> assert false -and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = - let (isevars',ks) = +and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = + let (evd',ks,_) = List.fold_left - (fun (i,ks) b -> + (fun (i,ks,m) b -> + if m=0 then (i,t2::ks, n-1) else let dloc = (dummy_loc,InternalHole) in let (i',ev) = new_evar i env ~src:dloc (substl ks b) in - (i', ev :: ks)) - (isevars,[]) bs + (i', ev :: ks, n - 1)) + (evd,[],n) bs in - ise_and isevars' + ise_and evd' [(fun i -> ise_list2 i (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u)) @@ -491,65 +477,80 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1); (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))] -let first_order_unification env isevars pbty (term1,l1) (term2,l2) = +(* We assume here |l1| <= |l2| *) + +let first_order_unification env evd (ev1,l1) (term2,l2) = + let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in + ise_and evd + (* First compare extra args for better failure message *) + [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1); + (fun i -> + (* Then instantiate evar unless already done by unifying args *) + let t2 = applist(term2,deb2) in + if is_defined_evar i ev1 then + evar_conv_x env i CONV t2 (mkEvar ev1) + else + solve_simple_eqn evar_conv_x env i (CONV,ev1,t2))] + +let choose_less_dependent_instance evk evd term args = + let evi = Evd.find (evars_of evd) evk in + let subst = make_pure_subst evi args in + let subst' = List.filter (fun (id,c) -> c = term) subst in + if subst' = [] then error "Too complex unification problem" else + Evd.evar_define evk (mkVar (fst (List.hd subst'))) evd + +let apply_conversion_problem_heuristic env evd pbty t1 t2 = + let t1 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t1) in + let t2 = apprec_nohdbeta env evd (whd_castappevar (evars_of evd) t2) in + let (term1,l1 as appr1) = decompose_app t1 in + let (term2,l2 as appr2) = decompose_app t2 in match kind_of_term term1, kind_of_term term2 with - | Evar ev1,_ when List.length l1 <= List.length l2 -> - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - ise_and isevars - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest2 l1); - (fun i -> - (* Then instantiate evar unless already done by unifying args *) - let t2 = applist(term2,deb2) in - if is_defined_evar i ev1 then - evar_conv_x env i pbty t2 (mkEvar ev1) - else - solve_simple_eqn evar_conv_x env i (pbty,ev1,t2))] - | _,Evar ev2 when List.length l2 <= List.length l1 -> - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - ise_and isevars - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) rest1 l2); - (fun i -> - (* Then instantiate evar unless already done by unifying args *) - let t1 = applist(term1,deb1) in - if is_defined_evar i ev2 then - evar_conv_x env i pbty t1 (mkEvar ev2) - else - solve_simple_eqn evar_conv_x env i (pbty,ev2,t1))] - | _ -> - (* Some head evar have been instantiated *) - evar_conv_x env isevars pbty (applist(term1,l1)) (applist(term2,l2)) - -let consider_remaining_unif_problems env isevars = - let (isevars,pbs) = get_conv_pbs isevars (fun _ -> true) in + | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] -> + (* The typical kind of constraint coming from patter-matching return + type inference *) + assert (array_for_all (fun a -> a = term2 or isEvar a) args1); + choose_less_dependent_instance evk1 evd term2 args1, true + | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] -> + (* The typical kind of constraint coming from patter-matching return + type inference *) + assert (array_for_all ((=) term1) args2); + choose_less_dependent_instance evk2 evd term1 args2, true + | Evar ev1,_ when List.length l1 <= List.length l2 -> + (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) + first_order_unification env evd (ev1,l1) appr2 + | _,Evar ev2 when List.length l2 <= List.length l1 -> + (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) + first_order_unification env evd (ev2,l2) appr1 + | _ -> + (* Some head evar have been instantiated, or unknown kind of problem *) + evar_conv_x env evd pbty t1 t2 + +let consider_remaining_unif_problems env evd = + let (evd,pbs) = extract_all_conv_pbs evd in List.fold_left - (fun (isevars,b as p) (pbty,env,t1,t2) -> - if b then first_order_unification env isevars pbty - (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t1)) - (apprec_nohdbeta env isevars (whd_castappevar (evars_of isevars) t2)) - else p) - (isevars,true) + (fun (evd,b as p) (pbty,env,t1,t2) -> + if b then apply_conversion_problem_heuristic env evd pbty t1 t2 else p) + (evd,true) pbs (* Main entry points *) -let the_conv_x env t1 t2 isevars = - match evar_conv_x env isevars CONV t1 t2 with +let the_conv_x env t1 t2 evd = + match evar_conv_x env evd CONV t1 t2 with (evd',true) -> evd' | _ -> raise Reduction.NotConvertible -let the_conv_x_leq env t1 t2 isevars = - match evar_conv_x env isevars CUMUL t1 t2 with +let the_conv_x_leq env t1 t2 evd = + match evar_conv_x env evd CUMUL t1 t2 with (evd', true) -> evd' | _ -> raise Reduction.NotConvertible -let e_conv env isevars t1 t2 = - match evar_conv_x env !isevars CONV t1 t2 with - (evd',true) -> isevars := evd'; true +let e_conv env evd t1 t2 = + match evar_conv_x env !evd CONV t1 t2 with + (evd',true) -> evd := evd'; true | _ -> false -let e_cumul env isevars t1 t2 = - match evar_conv_x env !isevars CUMUL t1 t2 with - (evd',true) -> isevars := evd'; true +let e_cumul env evd t1 t2 = + match evar_conv_x env !evd CUMUL t1 t2 with + (evd',true) -> evd := evd'; true | _ -> false |