(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result let debug_unification = ref (false) let _ = Goptions.declare_bool_option { Goptions.optdepr = false; Goptions.optname = "Print states sent to Evarconv unification"; Goptions.optkey = ["Debug";"Unification"]; Goptions.optread = (fun () -> !debug_unification); Goptions.optwrite = (fun a -> debug_unification:=a); } (*******************************************) (* Functions to deal with impossible cases *) (*******************************************) (* XXX: we would like to search for this with late binding "data.id.type" etc... *) let impossible_default_case () = let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in let (_, u) = Term.destConst c in Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx) let coq_unit_judge = let open Environ in let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in let na1 = Name (Id.of_string "A") in let na2 = Name (Id.of_string "H") in fun () -> match impossible_default_case () with | Some (id, type_of_id, ctx) -> make_judge id type_of_id, ctx | None -> (* In case the constants id/ID are not defined *) Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))), Univ.ContextSet.empty let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = match EConstr.kind evd c with | Const (c, u) -> if is_transparent_constant ts c then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) else None | Rel n -> (try match lookup_rel n env with | RelDecl.LocalAssum _ -> None | RelDecl.LocalDef (_,v,_) -> Some (lift n v) with Not_found -> None) | Var id -> (try if is_transparent_variable ts id then env |> lookup_named id |> NamedDecl.get_value 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 type flex_kind_of_term = | Rigid | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) | Flexible of EConstr.existential let flex_kind_of_term ts env evd c sk = match EConstr.kind evd 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 add_conv_pb (pb, env, x, y) sigma = Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma let apprec_nohdbeta ts env evd c = let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in if Stack.not_purely_applicative sk then Stack.zip evd (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 let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match EConstr.kind 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 (evk',_) -> if Evar.equal evk evk' 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 (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem 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 = (head us), for which we know that the i-th projection proji satisfies 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 env sigma (t1,sk1) (t2,sk2) = let (proji, u), arg = Termops.global_app_of_constr sigma t1 in let canon_s,sk2_effective = try match EConstr.kind sigma t2 with Prod (_,a,b) -> (* assert (l2=[]); *) let _, a, b = destProd sigma t2 in if noccurn sigma 1 b then lookup_canonical_conversion (proji, Prod_cs), (Stack.append_app [|a;pop b|] Stack.empty) else raise Not_found | Sort s -> let s = ESorts.kind sigma s in lookup_canonical_conversion (proji, Sort_cs (family_of_sort s)),[] | _ -> let (c2, _) = Termops.global_of_constr sigma 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 us = List.map EConstr.of_constr us in let params = List.map EConstr.of_constr params 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 = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in let t' = subst_univs_level_constr subst t' in let bs' = List.map (EConstr.of_constr %> subst_univs_level_constr subst) bs in let h, _ = decompose_app_vect sigma 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 sigma (t2,sk2)) (* Precondition: one of the terms of the pb is an uninstantiated evar, * possibly applied to arguments. *) let rec ise_try evd = function [] -> assert false | [f] -> f evd | f1::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 -> match f1 i with | Success i' -> ise_and i' l | UnifFailure _ as x -> x in ise_and evd l 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 -> Success i | n -> 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 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 let push_rec_types pfix env = let (i, c, t) = pfix in let inj c = EConstr.Unsafe.to_constr c in push_rec_types (i, Array.map inj c, Array.map inj t) env (* 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 check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in let length_ind_instance = Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in if not ((length_ind_instance = Univ.Instance.length u) && (length_ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else begin let comp_subst = (Univ.Instance.append u u') in let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in Evd.add_constraints evd comp_cst end 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 (* 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... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 in if b then Success evd else UnifFailure (evd, ConversionFailed (env,term1,term2)) with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with | UnifFailure (evd, e) when not (is_ground_env evd env) -> None | _ -> Some e) else None in match ground_test with | Some result -> result | 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 (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 (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) in begin match EConstr.kind evd term1, EConstr.kind evd 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 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 = tM in let t2 = solve_pattern_eqn env evd 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 evd (termF,l)) (Stack.zip evd (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 evd (termF,l)) (Stack.zip evd (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 evd term in let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in 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 evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.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 check_strict () = let univs = EConstr.eq_constr_universes evd term term' in match univs with | Some univs -> begin let cstrs = Universes.to_constraints (Evd.universes evd) univs in try Success (Evd.add_constraints evd cstrs) with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) end | None -> UnifFailure (evd, NotSameHead) in let first_try_strict_check cond u u' try_subtyping_constraints = if cond then let univs = EConstr.eq_constr_universes evd term term' in match univs with | Some univs -> begin let cstrs = Universes.to_constraints (Evd.universes evd) univs in try Success (Evd.add_constraints evd cstrs) with Univ.UniverseInconsistency p -> try_subtyping_constraints () end | None -> UnifFailure (evd, NotSameHead) else UnifFailure (evd, NotSameHead) in let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with | Const (c, u), Const (c', u') -> check_strict () | Ind (ind, u), Ind (ind', u') -> let check_subtyping_constraints () = let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in begin let mind = Environ.lookup_mind (fst ind) env in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> UnifFailure (evd, NotSameHead) | Declarations.Cumulative_ind cumi -> begin let num_param_arity = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then UnifFailure (evd, NotSameHead) else begin let evd' = check_leq_inductives evd cumi u u' in Success (check_leq_inductives evd' cumi u' u) end end end in first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints | Construct (cons, u), Construct (cons', u') -> let check_subtyping_constraints () = let ind, ind' = fst cons, fst cons' in let j, j' = snd cons, snd cons' in let nparamsaplied = Stack.args_size sk in let nparamsaplied' = Stack.args_size sk' in let mind = Environ.lookup_mind (fst ind) env in match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> UnifFailure (evd, NotSameHead) | Declarations.Cumulative_ind cumi -> begin let num_cnstr_args = let nparamsctxt = mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in nparamsctxt + mind.Declarations.mind_packets.(snd ind). Declarations.mind_consnrealargs.(j - 1) in if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then UnifFailure (evd, NotSameHead) else begin let evd' = check_leq_inductives evd cumi u u' in Success (check_leq_inductives evd' cumi u' u) end end in first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints | _, _ -> anomaly (Pp.str "") in ise_and evd [(fun i -> try compare_heads i with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] 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 -> quick_fail evd | Some lF -> let tM = Stack.zip evd 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 evd 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 EConstr.kind evd 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 EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> eta env evd false skR termR skF termF | Construct u -> eta_constructor ts env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in miller_pfenning on_left (fun () -> ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> if not (occur_rigidly ev i tR) then let i,tF = if isRel i tR || isVar i 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 evd 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 Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> (* sk1[?ev1] =? sk2[?ev2] *) let f1 i = (* Try first-order unification *) match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with | None, Success i' -> (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1', term2) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) | Some (r,[]), Success i' -> (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' (mkEvar ev2) in if isEvar i' ev2' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) else evar_eqappr_x ts env evd pbty ((ev2', sk1), csts1) ((term2, sk2), csts2) | Some ([],r), Success i' -> (* Symmetrically *) (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) (* we now unify ?ev1 and r[?ev2] *) let ev1' = whd_evar i' (mkEvar ev1) in if isEvar i' ev1' then solve_simple_eqn (evar_conv_x ts) env i' (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) else evar_eqappr_x ts env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) | None, (UnifFailure _ as x) -> (* sk1 and sk2 have no common outer part *) if Stack.not_purely_applicative sk2 then (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) flex_rigid true ev1 appr1 appr2 else if Stack.not_purely_applicative sk1 then (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) flex_rigid false ev2 appr2 appr1 else (* We could instead try Miller unification, then postpone to see if other equations help, as in: [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) x | Some _, Success _ -> (* sk1 and sk2 have a common outer part *) if Stack.not_purely_applicative sk2 then (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) flex_rigid true ev1 appr1 appr2 else if Stack.not_purely_applicative sk1 then (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) flex_rigid false ev2 appr2 appr1 else (* We could instead try Miller unification, then postpone to see if other equations help, as in: [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) UnifFailure (i,NotSameArgSize) | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") and f2 i = if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with |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 v2 -> flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 | MaybeFlexible v1, Flexible ev2 -> flex_maybeflex false ev2 (appr2,csts2) (appr1,csts1) v1 | MaybeFlexible v1, MaybeFlexible v2 -> begin match EConstr.kind evd term1, EConstr.kind evd term2 with | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> let f1 i = (* FO *) ise_and i [(fun i -> ise_try i [(fun i -> evar_conv_x ts env i CUMUL t1 t2); (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); (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 let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (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] | 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 evd (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 evd (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 = (* 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 univs = EConstr.eq_constr_universes evd term1 term2 in match univs with | Some univs -> 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)] | None -> UnifFailure (i,NotSameHead) and f2 i = (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 EConstr.kind i hd with | (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 () = 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 (EConstr.isLambda i 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 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 | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> let (na1,c1,c'1) = EConstr.destLambda evd term1 in let (na2,c2,c'2) = EConstr.destLambda evd 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 let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | 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 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 = 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] | Rigid, MaybeFlexible v2 -> let f3 i = (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 = 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] (* Eta-expansion *) | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Sort s1, Sort s2 when app_empty -> (try let s1 = ESorts.kind evd s1 in let s2 = ESorts.kind evd s2 in 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 CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) | Prod (n1,c1,c'1), Prod (n2,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 let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | 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 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 -> 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 i' (term1,sk1')) (Stack.zip i' (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 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 (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) and the terms h us = h2 us2 where 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) knowing that (proji params1 c1 | sk1) = (h2 us2 | sk2) 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.tag Evar_kinds.InternalHole in let (i', ev) = Evarutil.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 i (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.BiFinite -> let pars = mib.Declarations.mind_nparams in (try let l1' = Stack.tail pars sk1 in let l2' = let term = Stack.zip evd (term2,sk2) in List.map (fun p -> EConstr.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 (* We assume here |l1| <= |l2| *) let first_order_unification ts env evd (ev1,l1) (term2,l2) = 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_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 = 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))] 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) -> EConstr.eq_constr evd c term) subst in match subst' with | [] -> None | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd) 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 *) let eq_constr c1 c2 = match EConstr.eq_constr_universes !evdref c1 c2 with | None -> false | Some cstr -> try ignore (Evd.add_universe_constraints !evdref cstr); true with UniversesDiffer -> false in if eq_constr c t then f k else match EConstr.kind !evdref t with | Evar (evk,args) -> let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in let g decl a = if is_local_assum decl 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 !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t in applyrec (env,(0,c)) t let filter_possible_projections evd c ty ctxt args = (* 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 evd (mkApp (c,args)) (* Hack: locally untyped *) in let fv2 = collect_vars evd (mkApp (c,args)) in let len = Array.length args in let tyvars = collect_vars evd ty in List.map_i (fun i decl -> let () = assert (i < len) in let a = Array.unsafe_get args i in (match decl with | NamedDecl.LocalAssum _ -> false | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr 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 evd a && Int.Set.mem (destRel evd a) fv1 || isVar evd a && Id.Set.mem (destVar evd a) fv2 || Id.Set.mem (NamedDecl.get_id decl) tyvars) 0 ctxt let solve_evars = ref (fun _ -> failwith "solve_evars not installed") let set_solve_evars f = solve_evars := f (* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing * x1:T1 .. xn:Tn |- ev : ty * by looking for a maximal well-typed abtraction over u1..un in rhs * * We first build C[e11..e1p1,..,en1..enpn] obtained from rhs by replacing * all occurrences of u1..un by evars eij of type Ti' where itself Ti' has * been obtained from the type of ui by also replacing all occurrences of * u1..ui-1 by evars. * * Then, we use typing to infer the relations between the different * occurrences. If some occurrence is still unconstrained after typing, * we instantiate successively the unresolved occurrences of un by xn, * of un-1 by xn-1, etc [the idea comes from Chung-Kil Hur, that he * used for his Heq plugin; extensions to several arguments based on a * proposition from Dan Grayson] *) exception TypingFailed of evar_map let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try let evi = Evd.find_undefined evd evk 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 instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in let rec make_subst = function | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with | Some _ -> user_err Pp.(str "Cannot force abstraction on identity instance.") | None -> make_subst (ctxt',l,occsl) end | decl'::ctxt', c::l, occs::occsl -> let id = NamedDecl.get_id decl' in let t = EConstr.of_constr (NamedDecl.get_type decl') in let evs = ref [] in let ty = Retyping.get_type_of env_rhs evd c in let filter' = filter_possible_projections evd c ty ctxt args 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 Locus.AllOccurrences -> mkVar id | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in let instance = Filter.filter_list filter instance in let evd = !evdref in let (evd, ev) = new_evar_instance sign evd evty ~filter instance in evdref := evd; evsref := (fst (destEvar !evdref ev),evty)::!evsref; ev in set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst | [] -> rhs 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 let evd = !evdref in (* We instantiate the evars of which the value is forced by typing *) let 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 (TypingFailed !evdref) in let rec abstract_free_holes evd = function | (id,idty,c,_,evsref,_,_)::l -> let rec force_instantiation evd = function | (evk,evty)::evs -> let evd = if is_undefined evd evk then (* We force abstraction over this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) (* This is an arbitrary choice *) let evd = Evd.define evk (Constr.mkVar id) evd in match evar_conv_x ts env_evar evd CUMUL idty evty with | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> match reconsider_unif_constraints (evar_conv_x ts) evd with | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") | Success evd -> evd else evd in force_instantiation evd evs | [] -> abstract_free_holes evd l in force_instantiation evd !evsref | [] -> 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 (EConstr.Unsafe.to_constr rhs) evd in abstract_free_holes evd subst, true with TypingFailed evd -> evd, false let to_pb (pb, env, t1, t2) = (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2) let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in 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 *) let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then let open Pp in Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 ++ cut () ++ print_constr t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> 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 pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 let error_cannot_unify env evd pb ?reason t1 t2 = Pretype_errors.error_cannot_unify ?loc:(loc_of_conv_pb evd pb) env evd ?reason (t1, t2) let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2) | _ -> () exception MaxUndefined of (Evar.t * evar_info * Constr.t list) let max_undefined_with_candidates evd = let fold evk evi () = match evi.evar_candidates with | None -> () | Some l -> raise (MaxUndefined (evk, evi, l)) in (** [fold_right] traverses the undefined map in decreasing order of indices. The evar with candidates of maximum index is thus the first evar with candidates found by a [fold_right] traversal. This has a significant impact on performance. *) try let () = Evar.Map.fold_right fold (Evd.undefined_map evd) () in None with MaxUndefined ans -> Some ans 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 | None -> evd | Some (evk,ev_info,l) -> let rec aux = function | [] -> user_err Pp.(str "Unsolvable existential variables.") | a::l -> try let conv_algo = evar_conv_x ts in let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in let evd = Evd.define evk a evd in match reconsider_unif_constraints 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_candidates ts evd let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> match ev_info.evar_source with | loc,Evar_kinds.ImpossibleCase -> let j, ctx = coq_unit_judge () in let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc 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 (EConstr.Unsafe.to_constr ty) evd' | _ -> evd') evd evd let solve_unif_constraints_with_heuristics 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 t1 = EConstr.of_constr t1 in let t2 = EConstr.of_constr t2 in (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) end | UnifFailure (evd,reason) -> error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> let t1 = EConstr.of_constr t1 in let t2 = EConstr.of_constr t2 in (* There remains stuck problems *) error_cannot_unify env evd pb 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 env heuristic_solved_evd let consider_remaining_unif_problems = solve_unif_constraints_with_heuristics (* Main entry points *) 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 | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) 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 | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CONV t1 t2 with | Success evd' -> evdref := evd'; true | _ -> false let e_cumul env ?(ts=default_transparent_state env) evdref t1 t2 = match evar_conv_x ts env !evdref CUMUL t1 t2 with | Success evd' -> evdref := evd'; true | _ -> false