From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/evarconv.ml | 1386 ++++++++++++++++++++++++++++++------------------- 1 file changed, 859 insertions(+), 527 deletions(-) (limited to 'pretyping/evarconv.ml') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8b421ea3..a95af253 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,15 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result let debug_unification = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = - "Print states sended to Evarconv unification"; + "Print states sent to Evarconv unification"; Goptions.optkey = ["Debug";"Unification"]; Goptions.optread = (fun () -> !debug_unification); Goptions.optwrite = (fun a -> debug_unification:=a); } - -type flex_kind_of_term = - | Rigid of constr - | PseudoRigid of constr (* approximated as rigid but not necessarily so *) - | MaybeFlexible of constr (* approx'ed as reducible but not necessarily so *) - | Flexible of existential - -let flex_kind_of_term c l = +let unfold_projection env evd ts p c = + let cst = Projection.constant p in + if is_transparent_constant ts cst then + let c' = Some (mkProj (Projection.make cst true, c)) in + match ReductionBehaviour.get (Globnames.ConstRef cst) with + | None -> c' + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags) then None + else c' + else None + +let eval_flexible_term ts env evd c = match kind_of_term c with - | Rel _ | Const _ | Var _ -> MaybeFlexible c - | Lambda _ when l<>[] -> MaybeFlexible c - | LetIn _ -> MaybeFlexible c - | Evar ev -> Flexible ev - | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid c - | Meta _ | Case _ | Fix _ -> PseudoRigid c - | Cast _ | App _ -> assert false - -let eval_flexible_term ts env c = - match kind_of_term c with - | Const c -> + | Const (c,u as cu) -> if is_transparent_constant ts c - then constant_opt_value env c + then constant_opt_value_in env cu else None | Rel n -> (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v @@ -59,81 +59,126 @@ let eval_flexible_term ts env c = | Var id -> (try if is_transparent_variable ts id then - let (_,v,_) = lookup_named id env in v - else None + let (_,v,_) = lookup_named id env in v + else None with Not_found -> None) | LetIn (_,b,_,c) -> Some (subst1 b c) | Lambda _ -> Some c + | Proj (p, c) -> + if Projection.unfolded p then assert false + else unfold_projection env evd ts p c | _ -> assert false -let evar_apprec ts env evd stack c = - let sigma = evd in - let rec aux s = - let (t,stack) = whd_betaiota_deltazeta_for_iota_state ts env sigma s in - match kind_of_term t with - | 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) +type flex_kind_of_term = + | Rigid + | MaybeFlexible of Constr.t (* reducible but not necessarily reduced *) + | Flexible of existential + +let flex_kind_of_term ts env evd c sk = + match kind_of_term c with + | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> + Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) + | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c + | Evar ev -> Flexible ev + | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid + | Meta _ -> Rigid + | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) + | Cast _ | App _ | Case _ -> assert false let apprec_nohdbeta ts env evd c = - match kind_of_term (fst (Reductionops.whd_stack evd c)) with - | (Case _ | Fix _) -> applist (evar_apprec ts env evd [] c) - | _ -> c + let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in + if Stack.not_purely_applicative sk + then Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + ts env evd Cst_stack.empty appr)) + else c let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -(* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem - (t1 l1) = (t2 l2) into a problem - - l1 = params1@c1::extra_args1 - l2 = us2@extra_args2 - (t1 params1 c1) = (proji params (c xs)) - (t2 us2) = (cstr us) +let occur_rigidly ev evd t = + let (l, app) = decompose_app_vect t in + 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 + | Proj (p, c) -> not (aux c) + | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Cast (p, _, _) -> aux p + | Lambda _ | LetIn _ -> false + | Const _ -> false + | 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 + +(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose + the problem (t1 stack1) = (t2 stack2) into a problem + + stack1 = params1@[c1]@extra_args1 + stack2 = us2@extra_args2 + t1 params1 c1 = proji params (c xs) + t2 us2 = head us extra_args1 = extra_args2 by finding a record R and an object c := [xs:bs](Build_R params v1..vn) - with vi = (cstr us), for which we know that the i-th projection proji + with vi = (head us), for which we know that the i-th projection proji satisfies - (proji params (c xs)) = (cstr us) + proji params (c xs) = head us Rem: such objects, usable for conversion, are defined in the objdef table; practically, it amounts to "canonically" equip t2 into a object c in structure R (since, if c1 were not an evar, the projection would have been reduced) *) -let check_conv_record (t1,l1) (t2,l2) = - try - let proji = global_of_constr t1 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 = global_of_constr t2 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_NPARAMS = nparams; o_TCOMPS = us } = canon_s in - let params1, c1, extra_args1 = - match list_chop nparams l1 with - | params1, c1::extra_args1 -> params1, c1, extra_args1 - | _ -> raise Not_found in - 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 Failure _ | Not_found -> - raise Not_found +let check_conv_record env sigma (t1,sk1) (t2,sk2) = + let (proji, u), arg = Universes.global_app_of_constr t1 in + let canon_s,sk2_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), + (Stack.append_app [|a;pop b|] Stack.empty) + | Sort s -> + lookup_canonical_conversion + (proji, Sort_cs (family_of_sort s)),[] + | _ -> + let c2 = global_of_constr t2 in + lookup_canonical_conversion (proji, Const_cs c2),sk2 + with Not_found -> + let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in + (c,cs),[] + in + let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs; + o_TPARAMS = params; o_NPARAMS = nparams; o_TCOMPS = us } = canon_s in + let params1, c1, extra_args1 = + match arg with + | Some c -> (* A primitive projection applied to c *) + let ty = Retyping.get_type_of ~lax:true env sigma c in + let (i,u), ind_args = + try Inductiveops.find_mrectype env sigma ty + with _ -> raise Not_found + in Stack.append_app_list ind_args Stack.empty, c, sk1 + | None -> + match Stack.strip_n_app nparams sk1 with + | Some (params1, c1, extra_args1) -> params1, c1, extra_args1 + | _ -> raise Not_found in + let us2,extra_args2 = + let l_us = List.length us in + if Int.equal l_us 0 then Stack.empty,sk2_effective + else match (Stack.strip_n_app (l_us-1) sk2_effective) with + | None -> raise Not_found + | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in + let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let c' = subst_univs_level_constr subst c in + let t' = subst_univs_level_constr subst t' in + let bs' = List.map (subst_univs_level_constr subst) bs in + let h, _ = decompose_app_vect t' in + ctx',(h, t2),c',bs',(Stack.append_app_list params Stack.empty,params1), + (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1, + (n,Stack.zip(t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) @@ -142,40 +187,135 @@ let rec ise_try evd = function [] -> assert false | [f] -> f evd | f1::l -> - let (evd',b) = f1 evd in - if b then (evd',b) else ise_try evd l + match f1 evd with + | Success _ as x -> x + | UnifFailure _ -> ise_try evd 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 (evd,false) in + match f1 i with + | Success i' -> ise_and i' l + | UnifFailure _ as x -> x in ise_and evd l -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 (evd,false) - | _ -> (evd, false) in - ise_list2 evd l1 l2 +(* This function requires to get the outermost arguments first. It is + a fold_right for backward compatibility. + + It tries to unify the suffix of 2 lists element by element and if + it reaches the end of a list, it returns the remaining elements in + the other list if there are some. +*) +let ise_exact ise x1 x2 = + match ise x1 x2 with + | None, out -> out + | _, (UnifFailure _ as out) -> out + | Some _, Success i -> UnifFailure (i,NotSameArgSize) let ise_array2 evd f v1 v2 = let rec allrec i = function - | -1 -> (i,true) + | -1 -> Success i | n -> - let (i',b) = f i v1.(n) v2.(n) in - if b then allrec i' (n-1) else (evd,false) - in + match f i v1.(n) v2.(n) with + | Success i' -> allrec i' (n-1) + | UnifFailure _ as x -> x in let lv1 = Array.length v1 in - if lv1 = Array.length v2 then allrec evd (pred lv1) - else (evd,false) - + if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1) + else UnifFailure (evd,NotSameArgSize) + +(* Applicative node of stack are read from the outermost to the innermost + but are unified the other way. *) +let rec ise_app_stack2 env f evd sk1 sk2 = + match sk1,sk2 with + | Stack.App node1 :: q1, Stack.App node2 :: q2 -> + let (t1,l1) = Stack.decomp_node_last node1 q1 in + let (t2,l2) = Stack.decomp_node_last node2 q2 in + begin match ise_app_stack2 env f evd l1 l2 with + |(_,UnifFailure _) as x -> x + |x,Success i' -> x,f env i' CONV t1 t2 + end + | _, _ -> (sk1,sk2), Success evd + +(* This function tries to unify 2 stacks element by element. It works + from the end to the beginning. If it unifies a non empty suffix of + stacks but not the entire stacks, the first part of the answer is + Some(the remaining prefixes to tackle)) *) +let ise_stack2 no_app env evd f sk1 sk2 = + let rec ise_stack2 deep i sk1 sk2 = + let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i + else None, x in + match sk1, sk2 with + | [], [] -> None, Success i + | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> + (match f env i CONV t1 t2 with + | Success i' -> + (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with + | Success i'' -> ise_stack2 true i'' q1 q2 + | UnifFailure _ as x -> fail x) + | UnifFailure _ as x -> fail x) + | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> + if eq_constant (Projection.constant p1) (Projection.constant p2) + then ise_stack2 true i q1 q2 + else fail (UnifFailure (i, NotSameHead)) + | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, + Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> + if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then + match ise_and i [ + (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); + (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); + (fun i -> ise_exact (ise_stack2 false i) a1 a2)] with + | Success i' -> ise_stack2 true i' q1 q2 + | UnifFailure _ as x -> fail x + else fail (UnifFailure (i,NotSameHead)) + | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ + | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false + | Stack.App _ :: _, Stack.App _ :: _ -> + if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else + begin match ise_app_stack2 env f i sk1 sk2 with + |_,(UnifFailure _ as x) -> fail x + |(l1, l2), Success i' -> ise_stack2 true i' l1 l2 + end + |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) + in ise_stack2 false evd (List.rev sk1) (List.rev sk2) + +(* Make sure that the matching suffix is the all stack *) +let exact_ise_stack2 env evd f sk1 sk2 = + let rec ise_stack2 i sk1 sk2 = + match sk1, sk2 with + | [], [] -> Success i + | Stack.Case (_,t1,c1,_)::q1, Stack.Case (_,t2,c2,_)::q2 -> + ise_and i [ + (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_array2 i (fun ii -> f env ii CONV) c1 c2); + (fun i -> f env i CONV t1 t2)] + | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, + Stack.Fix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 -> + if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then + ise_and i [ + (fun i -> ise_stack2 i q1 q2); + (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); + (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); + (fun i -> ise_stack2 i a1 a2)] + else UnifFailure (i,NotSameHead) + | Stack.Proj (n1,a1,p1,_)::q1, Stack.Proj (n2,a2,p2,_)::q2 -> + if eq_constant (Projection.constant p1) (Projection.constant p2) + then ise_stack2 i q1 q2 + else (UnifFailure (i, NotSameHead)) + | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ + | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false + | Stack.App _ :: _, Stack.App _ :: _ -> + begin match ise_app_stack2 env f i sk1 sk2 with + |_,(UnifFailure _ as x) -> x + |(l1, l2), Success i' -> ise_stack2 i' l1 l2 + end + |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead) + in + 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 @@ -183,426 +323,578 @@ let rec evar_conv_x ts env evd pbty term1 term2 = could have found, we do it only if the terms are free of evar. Note: incomplete heuristic... *) let ground_test = - if is_ground_term evd term1 && is_ground_term evd term2 then - if is_trans_fconv pbty ts env evd term1 term2 then - Some true - else if is_ground_env evd env then Some false - else None - else None in + if is_ground_term evd term1 && is_ground_term evd term2 then ( + let evd, b = + try infer_conv ~pb:pbty ~ts:(fst ts) env evd term1 term2 + with Univ.UniverseInconsistency _ -> evd, false + in + if b then Some (evd, true) + else if is_ground_env evd env then Some (evd, false) + else None) + else None + in match ground_test with - Some b -> (evd,b) + | Some (evd, true) -> Success evd + | Some (evd, false) -> UnifFailure (evd,ConversionFailed (env,term1,term2)) | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) - let term1 = apprec_nohdbeta ts env evd term1 in - let term2 = apprec_nohdbeta ts env evd term2 in - if is_undefined_evar evd term1 then - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,destEvar term1,term2) - else if is_undefined_evar evd term2 then - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,destEvar term2,term1) - else + let term1 = apprec_nohdbeta (fst ts) env evd term1 in + let term2 = apprec_nohdbeta (fst ts) env evd term2 in + let default () = evar_eqappr_x ts env evd pbty - (decompose_app term1) (decompose_app term2) - -and evar_eqappr_x ?(rhs_is_already_stuck = false) - ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = - - let eta env evd onleft term l term' l' = - assert (l = []); - let (na,c,body) = destLambda term in - let c = nf_evar evd c in + (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) + (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) + in + begin match kind_of_term term1, kind_of_term term2 with + | Evar ev, _ when Evd.is_undefined evd (fst ev) -> + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem true pbty,ev,term2) with + | UnifFailure (_,OccurCheck _) -> + (* Eta-expansion might apply *) default () + | x -> x) + | _, Evar ev when Evd.is_undefined evd (fst ev) -> + (match solve_simple_eqn (evar_conv_x ts) env evd + (position_problem false pbty,ev,term1) with + | UnifFailure (_, OccurCheck _) -> + (* Eta-expansion might apply *) default () + | x -> x) + | _ -> default () + end + +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 + let miller_pfenning on_left fallback ev lF tM evd = + match is_unification_pattern_evar env evd ev lF tM with + | None -> fallback () + | Some l1' -> (* Miller-Pfenning's patterns unification *) + let t2 = nf_evar evd tM in + let t2 = solve_pattern_eqn env l1' t2 in + solve_simple_eqn (evar_conv_x ts) env evd + (position_problem on_left pbty,ev,t2) + in + let consume_stack on_left (termF,skF) (termO,skO) evd = + let switch f a b = if on_left then f a b else f b a in + let not_only_app = Stack.not_purely_applicative skO in + match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with + |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> + switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r)) + |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO + |_, (UnifFailure _ as x) -> x + |Some _, _ -> UnifFailure (evd,NotSameArgSize) in + let eta env evd onleft sk term sk' term' = + assert (match sk with [] -> true | _ -> false); + let (na,c1,c'1) = destLambda term in + let c = nf_evar evd c1 in let env' = push_rel (na,None,c) env in - let appr1 = evar_apprec ts env' evd [] body in - let appr2 = (lift 1 term', List.map (lift 1) l' @ [mkRel 1]) in - if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2 - else evar_eqappr_x ts env' evd CONV appr2 appr1 + let out1 = whd_betaiota_deltazeta_for_iota_state + (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in + let out2 = whd_nored_state evd + (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), + Cst_stack.empty in + if onleft then evar_eqappr_x ts env' evd CONV out1 out2 + else evar_eqappr_x ts env' evd CONV out2 out1 in - + let rigids env evd sk term sk' term' = + let b,univs = Universes.eq_constr_universes term term' in + if b then + ise_and evd [(fun i -> + let cstrs = Universes.to_constraints (Evd.universes i) univs in + try Success (Evd.add_constraints i cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] + else UnifFailure (evd,NotSameHead) + in + let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = + let switch f a b = if on_left then f a b else f b a in + 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 + | Some lF -> + let tM = Stack.zip apprM in + miller_pfenning on_left + (fun () -> if not_only_app then (* Postpone the use of an heuristic *) + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM + else quick_fail i) + ev lF tM i + and consume (termF,skF as apprF) (termM,skM as apprM) i = + if not (Stack.is_empty skF && Stack.is_empty skM) then + consume_stack on_left apprF apprM i + 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)) + in + let default i = ise_try i [f1; consume apprF apprM; delta] + in + match kind_of_term termM with + | Proj (p, c) when not (Stack.is_empty skF) -> + (* Might be ?X args = p.c args', and we have to eta-expand the + primitive projection if |args| >= |args'|+1. *) + let nargsF = Stack.args_size skF and nargsM = Stack.args_size skM in + begin + (* ?X argsF' ~= (p.c ..) argsM' -> ?X ~= (p.c ..), no need to expand *) + if nargsF <= nargsM then default evd + else + let f = + 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) + in + let delta' i = + switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') + in + fun i -> ise_try i [f1; consume apprF apprM'; delta'] + with Retyping.RetypeError _ -> + (* Happens thanks to w_unify building ill-typed terms *) + default + in f evd + end + | _ -> default evd + in + 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) + in + match Stack.list_of_app_stack skF with + | None -> + ise_try evd [consume_stack on_left apprF apprR; eta] + | Some lF -> + let tR = Stack.zip apprR in + miller_pfenning on_left + (fun () -> + ise_try evd + [eta;(* Postpone the use of an heuristic *) + (fun i -> + if not (occur_rigidly (fst ev) i tR) then + let i,tF = + if isRel tR || isVar tR then + (* Optimization so as to generate candidates *) + let i,ev = evar_absorb_arguments env i ev lF in + i,mkEvar ev + else + i,Stack.zip apprF in + switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) + tF tR + else + UnifFailure (evd,OccurCheck (fst ev,tR)))]) + ev lF tR evd + in + let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - let pr_state (tm,l) = - h 0 (Termops.print_constr tm ++ str "|" ++ cut () - ++ prlist_with_sep pr_semicolon - (fun x -> hov 1 (Termops.print_constr x)) l) in - pp (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ()) ++ fnl ()) in - match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with + pp (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) -> let f1 i = - if List.length l1 > List.length l2 then - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - ise_and i - [(fun i -> solve_simple_eqn (evar_conv_x ts) env i - (position_problem false pbty,ev2,applist(term1,deb1))); - (fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) rest1 l2)] - else - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in - ise_and i - [(fun i -> solve_simple_eqn (evar_conv_x ts) env i - (position_problem true pbty,ev1,applist(term2,deb2))); - (fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) l1 rest2)] + match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with + |None, Success i' -> + (* Evar can be defined in i' *) + 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',term2) + else + evar_eqappr_x ts env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) + |Some (r,[]), Success i' -> + let ev2' = whd_evar i' (mkEvar ev2) in + if isEvar ev2' then + solve_simple_eqn (evar_conv_x ts) env i' + (position_problem false pbty,destEvar ev2',Stack.zip(term1,r)) + else + evar_eqappr_x ts env evd pbty + ((ev2', sk1), csts1) ((term2, sk2), csts2) + + |Some ([],r), Success i' -> + 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) and f2 i = - if sp1 = sp2 then - ise_and i - [(fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) l1 l2); - (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2, - true)] - else (i,false) + if Evar.equal sp1 sp2 then + match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with + |None, Success i' -> + Success (solve_refl (fun env i pbty a1 a2 -> + is_success (evar_conv_x ts env i pbty a1 a2)) + env i' (position_problem true pbty) sp1 al1 al2) + |_, (UnifFailure _ as x) -> x + |Some _, _ -> UnifFailure (i,NotSameArgSize) + else UnifFailure (i,NotSameHead) in ise_try evd [f1; f2] - | Flexible ev1, MaybeFlexible flex2 -> - let f1 i = - match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with - | Some l1' -> - (* Miller-Pfenning's patterns unification *) - (* Preserve generality (except that CCI has no eta-conversion) *) - let t2 = nf_evar evd (applist appr2) in - let t2 = solve_pattern_eqn env l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev1,t2) - | None -> (i,false) - and f2 i = - if - List.length l1 <= List.length l2 - then - (* Try first-order unification *) - (* (heuristic that gives acceptable results in practice) *) - let (deb2,rest2) = - list_chop (List.length l2-List.length l1) l2 in - ise_and i - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) l1 rest2); - (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))] - else (i,false) - and f3 i = - match eval_flexible_term ts env flex2 with - | Some v2 -> - evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> (i,false) - in - ise_try evd [f1; f2; f3] + | Flexible ev1, MaybeFlexible v2 -> + flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 - | MaybeFlexible flex1, Flexible ev2 -> - let f1 i = - match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with - | Some l1' -> - (* Miller-Pfenning's patterns unification *) - (* Preserve generality (except that CCI has no eta-conversion) *) - let t1 = nf_evar evd (applist appr1) in - let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev2,t1) - | None -> (i,false) - and f2 i = - if - List.length l2 <= List.length l1 - then - (* Try first-order unification *) - (* (heuristic that gives acceptable results in practice) *) - let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in - ise_and i - (* First compare extra args for better failure message *) - [(fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) rest1 l2); - (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)] - else (i,false) - and f3 i = - match eval_flexible_term ts env flex1 with - | Some v1 -> - evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> (i,false) - in - ise_try evd [f1; f2; f3] + | MaybeFlexible v1, Flexible ev2 -> + flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1 - | MaybeFlexible flex1, MaybeFlexible flex2 -> begin - match kind_of_term flex1, kind_of_term flex2 with - | LetIn (na,b1,t1,c'1), LetIn (_,b2,_,c'2) -> + | MaybeFlexible v1, MaybeFlexible v2 -> begin + match kind_of_term term1, kind_of_term term2 with + | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) -> let f1 i = ise_and i - [(fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> evar_conv_x ts env i CONV t1 t2); + (fun i -> evar_conv_x ts env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in evar_conv_x ts (push_rel (na,Some b,t) env) i pbty c'1 c'2); - (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)] + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = - let appr1 = evar_apprec ts env i l1 (subst1 b1 c'1) - and appr2 = evar_apprec ts env i l2 (subst1 b2 c'2) - in evar_eqappr_x ts env i pbty appr1 appr2 + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) + in evar_eqappr_x ts env i pbty out1 out2 in ise_try evd [f1; f2] + | Proj (p, c), Proj (p', c') + when Constant.equal (Projection.constant p) (Projection.constant p') -> + let f1 i = + ise_and i + [(fun i -> evar_conv_x ts env i CONV c c'); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + and f2 i = + let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) + in evar_eqappr_x ts env i pbty out1 out2 + in + ise_try evd [f1; f2] + + (* Catch the p.c ~= p c' cases *) + | Proj (p,c), Const (p',u) when eq_constant (Projection.constant p) p' -> + let res = + try Some (destApp (Retyping.expand_projection env evd p c [])) + with Retyping.RetypeError _ -> None + in + (match res with + | Some (f1,args1) -> + evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) + (appr2,csts2) + | None -> UnifFailure (evd,NotSameHead)) + + | Const (p,u), Proj (p',c') when eq_constant p (Projection.constant p') -> + let res = + try Some (destApp (Retyping.expand_projection env evd p' c' [])) + with Retyping.RetypeError _ -> None + in + (match res with + | Some (f2,args2) -> + evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) + | None -> UnifFailure (evd,NotSameHead)) + | _, _ -> - let f1 i = - if eq_constr flex1 flex2 then - ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2 - else - (i,false) + let f1 i = + (* Gather the universe constraints that would make term1 and term2 equal. + If these only involve unifications of flexible universes to other universes, + allow this identification (first-order unification of universes). Otherwise + fallback to unfolding. + *) + let b,univs = Universes.eq_constr_universes term1 term2 in + if b then + ise_and i [(fun i -> + try Success (Evd.add_universe_constraints i univs) + with UniversesDiffer -> UnifFailure (i,NotSameHead) + | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + else UnifFailure (i,NotSameHead) and f2 i = - (try conv_record ts env i - (try check_conv_record appr1 appr2 - with Not_found -> check_conv_record appr2 appr1) - with Not_found -> (i,false)) + (try + if not (snd ts) then raise Not_found + else conv_record ts env i + (try check_conv_record env i appr1 appr2 + with Not_found -> check_conv_record env i appr2 appr1) + with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f3 i = (* heuristic: unfold second argument first, exception made if the first argument is a beta-redex (expand a constant only if necessary) or the second argument is potentially usable as a canonical projection or canonical value *) let rec is_unnamed (hd, args) = match kind_of_term hd with - | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> false - | (Case _|Fix _|CoFix _|Meta _|Rel _)-> true - | Evar _ -> false (* immediate solution without Canon Struct *) - | Lambda _ -> assert(args = []); true - | LetIn (_,b,_,c) -> - is_unnamed (evar_apprec ts env i args (subst1 b c)) - | App _| Cast _ -> assert false in + | (Var _|Construct _|Ind _|Const _|Prod _|Sort _) -> + Stack.not_purely_applicative args + | (CoFix _|Meta _|Rel _)-> true + | Evar _ -> Stack.not_purely_applicative args + (* false (* immediate solution without Canon Struct *)*) + | Lambda _ -> assert (match args with [] -> true | _ -> false); true + | LetIn (_,b,_,c) -> is_unnamed + (fst (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i Cst_stack.empty (subst1 b c, args))) + | Fix _ -> true (* Partially applied fix can be the result of a whd call *) + | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args + | Case _ | App _| Cast _ -> assert false in let rhs_is_stuck_and_unnamed () = - match eval_flexible_term ts env flex2 with - | None -> false - | Some v2 -> is_unnamed (evar_apprec ts env i l2 v2) in + let applicative_stack = fst (Stack.strip_app sk2) in + is_unnamed + (fst (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in - if isLambda flex1 || rhs_is_already_stuck then - match eval_flexible_term ts env flex1 with - | Some v1 -> - evar_eqappr_x ~rhs_is_already_stuck - ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> - match eval_flexible_term ts env flex2 with - | Some v2 -> - evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> (i,false) + + if (isLambda term1 || rhs_is_already_stuck) + && (not (Stack.not_purely_applicative sk1)) then + evar_eqappr_x ~rhs_is_already_stuck ts env i pbty + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + (appr2,csts2) else - match eval_flexible_term ts env flex2 with - | Some v2 -> - evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> - match eval_flexible_term ts env flex1 with - | Some v1 -> - evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> (i,false) + evar_eqappr_x ts env i pbty (appr1,csts1) + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f1; f2; f3] - end + end - | Rigid c1, Rigid c2 when isLambda c1 & isLambda c2 -> - let (na,c1,c'1) = destLambda c1 in - let (_,c2,c'2) = destLambda c2 in - assert (l1=[] & l2=[]); + | Rigid, Rigid when isLambda term1 && isLambda term2 -> + let (na,c1,c'1) = destLambda term1 in + let (_,c2,c'2) = destLambda term2 in + assert app_empty; ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)] - | Flexible ev1, (Rigid _ | PseudoRigid _) -> - (match is_unification_pattern_evar env evd ev1 l1 (applist appr2) with - | Some l1 -> - (* Miller-Pfenning's pattern unification *) - (* Preserve generality thanks to eta-conversion) *) - let t2 = nf_evar evd (applist appr2) in - let t2 = solve_pattern_eqn env l1 t2 in - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev1,t2) - | None -> - if isLambda term2 then - eta env evd false term2 l2 term1 l1 - else - (* Postpone the use of an heuristic *) - add_conv_pb (pbty,env,applist appr1,applist appr2) evd, - true) - - | (Rigid _ | PseudoRigid _), Flexible ev2 -> - (match is_unification_pattern_evar env evd ev2 l2 (applist appr1) with - | Some l2 -> - (* Miller-Pfenning's pattern unification *) - (* Preserve generality thanks to eta-conversion) *) - let t1 = nf_evar evd (applist appr1) in - let t1 = solve_pattern_eqn env l2 t1 in - solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev2,t1) - | None -> - if isLambda term1 then - eta env evd true term1 l1 term2 l2 - else - (* Postpone the use of an heuristic *) - add_conv_pb (pbty,env,applist appr1,applist appr2) evd, - true) - - | MaybeFlexible flex1, (Rigid _ | PseudoRigid _) -> + | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 + | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 + + | MaybeFlexible v1, Rigid -> let f3 i = - (try conv_record ts env i (check_conv_record appr1 appr2) - with Not_found -> (i,false)) + (try + if not (snd ts) then raise Not_found + else conv_record ts env i (check_conv_record env i appr1 appr2) + with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - match eval_flexible_term ts env flex1 with - | Some v1 -> - evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> - if isLambda term2 then - eta env i false term2 l2 term1 l1 - else - (i,false) + evar_eqappr_x ts env i pbty + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + (appr2,csts2) in - ise_try evd [f3; f4] + ise_try evd [f3; f4] - | (Rigid _ | PseudoRigid _), MaybeFlexible flex2 -> + | Rigid, MaybeFlexible v2 -> let f3 i = - (try conv_record ts env i (check_conv_record appr2 appr1) - with Not_found -> (i,false)) + (try + if not (snd ts) then raise Not_found + else conv_record ts env i (check_conv_record env i appr2 appr1) + with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - match eval_flexible_term ts env flex2 with - | Some v2 -> - evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> - if isLambda term1 then - eta env i true term1 l1 term2 l2 - else - (i,false) + evar_eqappr_x ts env i pbty (appr1,csts1) + (whd_betaiota_deltazeta_for_iota_state + (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in - ise_try evd [f3; f4] + ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid c1, _ when isLambda c1 -> - eta env evd true term1 l1 term2 l2 - - | _, Rigid c2 when isLambda c2 -> - eta env evd false term2 l2 term1 l1 - - | Rigid c1, Rigid c2 -> begin - match kind_of_term c1, kind_of_term c2 with - - | Sort s1, Sort s2 when l1=[] & l2=[] -> - (try - let evd' = - if pbty = CONV - then Evd.set_eq_sort evd s1 s2 - else Evd.set_leq_sort evd s1 s2 - in (evd', true) - with Univ.UniverseInconsistency _ -> (evd, false) - | e when Errors.noncritical e -> (evd, false)) - - | Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] -> + | Rigid, _ when isLambda term1 -> + eta env evd true sk1 term1 sk2 term2 + + | _, Rigid when isLambda term2 -> + eta env evd false sk2 term2 sk1 term1 + + | Rigid, Rigid -> begin + match kind_of_term term1, kind_of_term term2 with + + | Sort s1, Sort s2 when app_empty -> + (try + let evd' = + if pbty == CONV + then Evd.set_eq_sort env evd s1 s2 + else Evd.set_leq_sort env evd s1 s2 + in Success evd' + with Univ.UniverseInconsistency p -> + UnifFailure (evd,UnifUnivInconsistency p) + | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead)) + + | Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty -> ise_and evd [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in evar_conv_x ts (push_rel (n,None,c) env) i pbty c'1 c'2)] - | Ind sp1, Ind sp2 -> - if eq_ind sp1 sp2 then - ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2 - else (evd, false) - - | Construct sp1, Construct sp2 -> - if eq_constructor sp1 sp2 then - ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2 - else (evd, false) + | Rel x1, Rel x2 -> + if Int.equal x1 x2 then + exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + else UnifFailure (evd,NotSameHead) + + | Var var1, Var var2 -> + if Id.equal var1 var2 then + exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + else UnifFailure (evd,NotSameHead) + + | Const _, Const _ + | Ind _, Ind _ + | Construct _, Construct _ -> + rigids env evd sk1 term1 sk2 term2 + + | Construct u, _ -> + eta_constructor ts env evd sk1 u sk2 term2 + + | _, Construct u -> + eta_constructor ts env evd sk2 u sk1 term1 + + | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) + if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then + ise_and evd [ + (fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2); + (fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + else UnifFailure (evd, NotSameHead) | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> - if i1=i2 then + if Int.equal i1 i2 then ise_and evd [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) tys1 tys2); (fun i -> ise_array2 i (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV) bds1 bds2); - (fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) l1 l2)] - else (evd,false) - - | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> (evd,false) - | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> (evd,false) - - | (App _ | Meta _ | Cast _ | Case _ | Fix _), _ -> assert false - | (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false + (fun i -> exact_ise_stack2 env i + (evar_conv_x ts) sk1 sk2)] + else UnifFailure (evd,NotSameHead) + + | (Meta _, _) | (_, Meta _) -> + begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with + |_, (UnifFailure _ as x) -> x + |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 + |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip (term1,sk1')) (Stack.zip (term2,sk2')) + end + + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _), _ -> + UnifFailure (evd,NotSameHead) + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _) -> + UnifFailure (evd,NotSameHead) + + | (App _ | Cast _ | Case _ | Proj _), _ -> assert false + | (LetIn _| Evar _), _ -> assert false | (Lambda _), _ -> assert false end - | PseudoRigid c1, PseudoRigid c2 -> begin - match kind_of_term c1, kind_of_term c2 with +and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = + (* Tries to unify the states - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - ise_and evd - [(fun i -> evar_conv_x ts env i CONV p1 p2); - (fun i -> evar_conv_x ts env i CONV c1 c2); - (fun i -> ise_array2 i - (fun i -> evar_conv_x ts env i CONV) cl1 cl2); - (fun i -> ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2)] - - | Fix (li1,(_,tys1,bds1 as recdef1)), Fix (li2,(_,tys2,bds2)) -> - if li1=li2 then - ise_and evd - [(fun i -> ise_array2 i - (fun i -> evar_conv_x ts env i CONV) tys1 tys2); - (fun i -> ise_array2 i - (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV) - bds1 bds2); - (fun i -> ise_list2 i - (fun i -> evar_conv_x ts env i CONV) l1 l2)] - else (evd,false) + (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) - | (Meta _ | Case _ | Fix _ | CoFix _), - (Meta _ | Case _ | Fix _ | CoFix _) -> (evd,false) + and the terms - | (App _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> assert false - | _, (App _ | Ind _ | Construct _ | Sort _ | Prod _) -> assert false + h us = h2 us2 - | (LetIn _ | Cast _), _ -> assert false - | _, (LetIn _ | Cast _) -> assert false + where - | (Lambda _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false - | _, (Lambda _ | Rel _ | Var _ | Const _ | Evar _) -> assert false - end + c = the constant for the canonical structure (i.e. some term of the form + fun (xs:bs) => Build_R params v1 .. vi-1 (h us) vi+1 .. vn) + bs = the types of the parameters of the canonical structure + c1 = the main argument of the canonical projection + sk1, sk2 = the surrounding stacks of the conversion problem + params1, params2 = the params of the projection (empty if a primitive proj) - | PseudoRigid _, Rigid _ -> (evd,false) + knowing that - | Rigid _, PseudoRigid _ -> (evd,false) + (proji params1 c1 | sk1) = (h2 us2 | sk2) -and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = - let (evd',ks,_) = - List.fold_left - (fun (i,ks,m) b -> - if m=n then (i,t2::ks, m-1) else - let dloc = (dummy_loc,InternalHole) in - let (i',ev) = new_evar i env ~src:dloc (substl ks b) in - (i', ev :: ks, m - 1)) - (evd,[],List.length bs - 1) bs - in - ise_and evd' - [(fun i -> - ise_list2 i - (fun i x1 x -> evar_conv_x trs env i CONV x1 (substl ks x)) - params1 params); - (fun i -> - ise_list2 i - (fun i u1 u -> evar_conv_x trs env i CONV u1 (substl ks u)) - us2 us); - (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks)))); - (fun i -> ise_list2 i (fun i -> evar_conv_x trs env i CONV) ts ts1)] + had to be initially resolved + *) + let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in + if Reductionops.Stack.compare_shape sk1 sk2 then + let (evd',ks,_,test) = + List.fold_left + (fun (i,ks,m,test) b -> + if match n with Some n -> Int.equal m n | None -> false then + let ty = Retyping.get_type_of env i t2 in + let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in + (i,t2::ks, m-1, test) + else + let dloc = (Loc.ghost,Evar_kinds.InternalHole) in + let (i',ev) = new_evar env i ~src:dloc (substl ks b) in + (i', ev :: ks, m - 1,test)) + (evd,[],List.length bs,fun i -> Success i) bs + in + let app = mkApp (c, Array.rev_of_list ks) in + ise_and evd' + [(fun i -> + exact_ise_stack2 env i + (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x)) + params1 params); + (fun i -> + exact_ise_stack2 env i + (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u)) + us2 us); + (fun i -> evar_conv_x trs env i CONV c1 app); + (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); + test; + (fun i -> evar_conv_x trs env i CONV h2 + (fst (decompose_app_vect (substl ks h))))] + else UnifFailure(evd,(*dummy*)NotSameHead) + +and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = + let mib = lookup_mind (fst ind) env in + match mib.Declarations.mind_record with + | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> + let pars = mib.Declarations.mind_nparams in + (try + let l1' = Stack.tail pars sk1 in + let l2' = + let term = Stack.zip (term2,sk2) in + List.map (fun p -> mkProj (Projection.make p false, term)) (Array.to_list projs) + in + exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' + (Stack.append_app_list l2' Stack.empty) + with + | Invalid_argument _ -> + (* Stack.tail: partially applied constructor *) + UnifFailure(evd,NotSameHead)) + | _ -> UnifFailure (evd,NotSameHead) + +let evar_conv_x ts = evar_conv_x (ts, true) + +(* Profiling *) +let evar_conv_x = + if Flags.profile then + let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in + Profile.profile6 evar_conv_xkey evar_conv_x + else evar_conv_x + +let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () + +let evar_conv_x ts = Hook.get evar_conv_hook_get ts + +let set_evar_conv f = Hook.set evar_conv_hook_set f -(* getting rid of the optional argument rhs_is_already_stuck *) -let evar_eqappr_x ts env evd pbty appr1 appr2 = - evar_eqappr_x ts env evd pbty appr1 appr2 (* We assume here |l1| <= |l2| *) let first_order_unification ts env evd (ev1,l1) (term2,l2) = - let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in + let (deb2,rest2) = Array.chop (Array.length l2-Array.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 ts env i CONV) rest2 l1); + [(fun i -> ise_array2 i (fun i -> evar_conv_x ts 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 + let t2 = mkApp(term2,deb2) in + if is_defined i (fst ev1) then evar_conv_x ts env i CONV t2 (mkEvar ev1) else solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] @@ -610,46 +902,50 @@ let first_order_unification ts env evd (ev1,l1) (term2,l2) = let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in let subst = make_pure_subst evi args in - let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in - if subst' = [] then evd, false else - Evd.define evk (mkVar (fst (List.hd subst'))) evd, true + let subst' = List.filter (fun (id,c) -> Term.eq_constr c term) subst in + match subst' with + | [] -> None + | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) -let apply_on_subterm evdref f c t = - let rec applyrec (k,c as kc) t = +let apply_on_subterm env evdref f c t = + let rec applyrec (env,(k,c) as acc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) - if eq_constr c t then f k + if e_eq_constr_univs evdref c t then f k else match kind_of_term t with | Evar (evk,args) when Evd.is_undefined !evdref evk -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g (_,b,_) a = if b = None then applyrec kc a else a in + let g (_,b,_) a = if Option.is_empty b then applyrec acc a else a in mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) | _ -> - map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) - applyrec kc t + map_constr_with_binders_left_to_right + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) + applyrec acc t in - applyrec (0,c) t + applyrec (env,(0,c)) t let filter_possible_projections c ty ctxt args = - let fv1 = free_rels c in - let fv2 = collect_vars c in + (* Since args in the types will be replaced by holes, we count the + fv of args to have a well-typed filter; don't know how necessary + it is however to have a well-typed filter here *) + let fv1 = free_rels (mkApp (c,args)) (* Hack: locally untyped *) in + let fv2 = collect_vars (mkApp (c,args)) in + let len = Array.length args in let tyvars = collect_vars ty in - List.map2 (fun (id,b,_) a -> - b <> None || + List.map_i (fun i (id,b,_) -> + let () = assert (i < len) in + let a = Array.unsafe_get args i in + (match b with None -> false | Some c -> not (isRel c || isVar c)) || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) (* in u *) - isRel a && Intset.mem (destRel a) fv1 || - isVar a && Idset.mem (destVar a) fv2 || - Idset.mem id tyvars) - ctxt args - -let initial_evar_data evi = - let ids = List.map pi1 (evar_context evi) in - (evar_filter evi, List.map mkVar ids) + isRel a && Int.Set.mem (destRel a) fv1 || + isVar a && Id.Set.mem (destVar a) fv2 || + Id.Set.mem id tyvars) + 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") let set_solve_evars f = solve_evars := f @@ -671,48 +967,49 @@ let set_solve_evars f = solve_evars := f * proposition from Dan Grayson] *) +exception TypingFailed of evar_map + let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try - let args = Array.to_list args in let evi = Evd.find_undefined evd evk in - let env_evar = evar_env evi in + let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let filter = evar_filter evi in let instance = List.map mkVar (List.map pi1 ctxt) in let rec make_subst = function | (id,_,t)::ctxt', c::l, occs::occsl when isVarId id c -> - if occs<>None then + begin match occs with + | Some _ -> error "Cannot force abstraction on identity instance." - else + | None -> make_subst (ctxt',l,occsl) + end | (id,_,t)::ctxt', c::l, occs::occsl -> let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections c ty ctxt args in - let filter = List.map2 (&&) filter filter' in - (id,t,c,ty,evs,filter,occs) :: make_subst (ctxt',l,occsl) - | [], [], [] -> [] - | _ -> anomaly "Signature, instance and occurrences list do not match" in + (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) + | _, _, [] -> [] + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list") in let rec set_holes evdref rhs = function | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with - | Some (false,[]) -> mkVar id + | Some Locus.AllOccurrences -> mkVar id | Some _ -> error "Selection of specific occurrences not supported" | None -> let evty = set_holes evdref cty subst in - let instance = snd (list_filter2 (fun b c -> b) (filter,instance)) in + let instance = Filter.filter_list filter instance in let evd,ev = new_evar_instance sign !evdref evty ~filter instance in evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in - set_holes evdref (apply_on_subterm evdref set_var c rhs) subst + set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst | [] -> rhs in - let subst = make_subst (ctxt,args,argoccs) in + let subst = make_subst (ctxt,Array.to_list args,argoccs) in let evdref = ref evd in let rhs = set_holes evdref rhs subst in @@ -720,10 +1017,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* We instantiate the evars of which the value is forced by typing *) let evd,rhs = - try !solve_evars env_evar evd rhs + let evdref = ref evd in + try let c = !solve_evars env_evar evdref rhs in !evdref,c with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise Exit in + raise (TypingFailed !evdref) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> @@ -735,10 +1033,12 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) let evd = Evd.define evk (mkVar id) evd in - let evd,b = evar_conv_x ts env_evar evd CUMUL idty evty in - if not b then error "Cannot find an instance"; - let evd,b = reconsider_conv_pbs (evar_conv_x ts) evd in - if not b then error "Cannot find an instance"; + match evar_conv_x ts env_evar evd CUMUL idty evty with + | UnifFailure _ -> error "Cannot find an instance" + | Success evd -> + match reconsider_conv_pbs (evar_conv_x ts) evd with + | UnifFailure _ -> error "Cannot find an instance" + | Success evd -> evd else evd @@ -749,63 +1049,78 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = in force_instantiation evd !evsref | [] -> - Evd.define evk rhs evd in - + let evd = + try Evarsolve.check_evar_instance evd evk rhs + (evar_conv_x full_transparent_state) + with IllTypedInstance _ -> raise (TypingFailed evd) + in + Evd.define evk rhs evd + in abstract_free_holes evd subst, true - with Exit -> evd, false + with TypingFailed evd -> evd, false let second_order_matching_with_args ts env evd 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 - second_order_matching ts env evd ev argoccs t + let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in + let evd, b = second_order_matching ts env evd ev argoccs t in + if b then Success evd + else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + if b then Success evd else *) - (evd,false) + UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in - let (term1,l1 as appr1) = decompose_app t1 in - let (term2,l2 as appr2) = decompose_app t2 in + let (term1,l1 as appr1) = try destApp t1 with DestKO -> (t1, [||]) in + let (term2,l2 as appr2) = try destApp t2 with DestKO -> (t2, [||]) in + let app_empty = Array.is_empty l1 && Array.is_empty l2 in match kind_of_term term1, kind_of_term term2 with - | Evar (evk1,args1), (Rel _|Var _) when l1 = [] & l2 = [] - & List.for_all (fun a -> eq_constr a term2 or isEvar a) - (remove_instance_local_defs evd evk1 (Array.to_list args1)) -> + | Evar (evk1,args1), (Rel _|Var _) when app_empty + && List.for_all (fun a -> Term.eq_constr a term2 || isEvar a) + (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return type inference *) - choose_less_dependent_instance evk1 evd term2 args1 - | (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = [] - & List.for_all (fun a -> eq_constr a term1 or isEvar a) - (remove_instance_local_defs evd evk2 (Array.to_list args2)) -> + (match choose_less_dependent_instance evk1 evd term2 args1 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | (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) -> (* The typical kind of constraint coming from pattern-matching return type inference *) - choose_less_dependent_instance evk2 evd term1 args2 - | Evar (evk1,args1), Evar (evk2,args2) when evk1 = evk2 -> - let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in - solve_refl ~can_drop:true f env evd evk1 args1 args2, true + (match choose_less_dependent_instance evk2 evd term1 args2 with + | Some evd -> Success evd + | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> + let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in + Success (solve_refl ~can_drop:true f env evd + (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 -> - solve_evar_evar ~force:true - (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2, true - | Evar ev1,_ when List.length l1 <= List.length l2 -> + Success (solve_evar_evar ~force:true + (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd + (position_problem true pbty) ev1 ev2) + | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) 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 (applist appr2))] - | _,Evar ev2 when List.length l2 <= List.length l1 -> + second_order_matching_with_args ts env evd 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 (applist appr1))] + second_order_matching_with_args ts env evd ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 (applist appr2) + second_order_matching_with_args ts env evd ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 (applist appr1) + second_order_matching_with_args ts env evd ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 @@ -828,9 +1143,9 @@ let max_undefined_with_candidates evd = | Some l -> (evk,ev_info,l)::evars) evd [] in match l with | [] -> None - | a::l -> Some (list_last (a::l)) + | a::l -> Some (List.last (a::l)) -let rec solve_unconstrained_evars_with_canditates evd = +let rec solve_unconstrained_evars_with_candidates ts evd = (* max_undefined is supposed to return the most recent, hence possibly most dependent evar *) match max_undefined_with_candidates evd with @@ -840,70 +1155,87 @@ let rec solve_unconstrained_evars_with_canditates evd = | [] -> error "Unsolvable existential variables." | a::l -> try - let conv_algo = evar_conv_x full_transparent_state in + let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in - let evd,b = reconsider_conv_pbs conv_algo evd in - if b then solve_unconstrained_evars_with_canditates evd - else aux l - with e when Pretype_errors.precatchable_exception e -> - aux l in + match reconsider_conv_pbs conv_algo evd with + | Success evd -> solve_unconstrained_evars_with_candidates ts evd + | UnifFailure _ -> aux l + with + | IllTypedInstance _ -> aux l + | e when Pretype_errors.precatchable_exception e -> aux l in (* List.rev is there to favor most dependent solutions *) (* and favor progress when used with the refine tactics *) let evd = aux (List.rev l) in - solve_unconstrained_evars_with_canditates evd + solve_unconstrained_evars_with_candidates ts evd -let solve_unconstrained_impossible_cases evd = +let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with - | _,ImpossibleCase -> Evd.define evk (j_type (coq_unit_judge ())) evd' + | _,Evar_kinds.ImpossibleCase -> + let j, ctx = coq_unit_judge () in + let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd' ctx in + let ty = j_type j in + let conv_algo = evar_conv_x full_transparent_state in + let evd' = check_evar_instance evd' evk ty conv_algo in + Evd.define evk ty evd' | _ -> evd') evd evd - -let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd = - let evd = solve_unconstrained_evars_with_canditates evd in +let consider_remaining_unif_problems env + ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = + let evd = solve_unconstrained_evars_with_candidates ts evd in let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in - if b then - let (evd', rest) = extract_all_conv_pbs evd' in - if rest = [] then aux evd' pbs true stuck - else (* Unification got actually stuck, postpone *) + (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with + | Success evd' -> + let (evd', rest) = extract_all_conv_pbs evd' in + begin match rest with + | [] -> aux evd' pbs true stuck + | _ -> (* Unification got actually stuck, postpone *) aux evd pbs progress (pb :: stuck) - else Pretype_errors.error_cannot_unify env evd (t1, t2) + end + | UnifFailure (evd,reason) -> + Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) + env evd ~reason (t1, t2)) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd - | (pbty,env,t1,t2) :: _ -> + | (pbty,env,t1,t2 as pb) :: _ -> (* There remains stuck problems *) - Pretype_errors.error_cannot_unify env evd (t1, t2) + Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) + env evd (t1, t2) in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in check_problems_are_solved env heuristic_solved_evd; - solve_unconstrained_impossible_cases heuristic_solved_evd + solve_unconstrained_impossible_cases env heuristic_solved_evd (* Main entry points *) -let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd = +exception UnableToUnify of evar_map * unification_error + +let default_transparent_state env = full_transparent_state +(* Conv_oracle.get_transp_state (Environ.oracle env) *) + +let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x ts env evd CONV t1 t2 with - (evd',true) -> evd' - | _ -> raise Reduction.NotConvertible + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd = +let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x ts env evd CUMUL t1 t2 with - (evd', true) -> evd' - | _ -> raise Reduction.NotConvertible + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let e_conv ?(ts=full_transparent_state) env evdref t1 t2 = +let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with - (evd',true) -> evdref := evd'; true - | _ -> false + | Success evd' -> evdref := evd'; true + | _ -> false -let e_cumul ?(ts=full_transparent_state) env evdref t1 t2 = +let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CUMUL t1 t2 with - (evd',true) -> evdref := evd'; true - | _ -> false + | Success evd' -> evdref := evd'; true + | _ -> false -- cgit v1.2.3