From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- pretyping/unification.ml | 583 +++++++++++++++++++++++++++++++++-------------- 1 file changed, 418 insertions(+), 165 deletions(-) (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5fb8054f..fc812594 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: unification.ml 9517 2007-01-22 17:37:58Z herbelin $ *) +(* $Id: unification.ml 11157 2008-06-21 10:45:51Z herbelin $ *) open Pp open Util @@ -23,6 +23,8 @@ open Rawterm open Pattern open Evarutil open Pretype_errors +open Retyping +open Coercion.Default (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms, gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *) @@ -31,31 +33,69 @@ let abstract_scheme env c l lname_typ = List.fold_left2 (fun t (locc,a) (na,_,ta) -> let na = match kind_of_term a with Var id -> Name id | _ -> na in +(* [occur_meta ta] test removed for support of eelim/ecase but consequences + are unclear... if occur_meta ta then error "cannot find a type for the generalisation" - else if occur_meta a then lambda_name env (na,ta,t) + else *) if occur_meta a then lambda_name env (na,ta,t) else lambda_name env (na,ta,subst_term_occ locc a t)) c (List.rev l) lname_typ -let abstract_list_all env sigma typ c l = - let ctxt,_ = decomp_n_prod env sigma (List.length l) typ in - let p = abstract_scheme env c (List.map (function a -> [],a) l) ctxt in +let abstract_list_all env evd typ c l = + let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in + let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in + let p = abstract_scheme env c l_with_all_occs ctxt in try - if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p else error "abstract_list_all" - with UserError _ -> - raise (PretypeError (env,CannotGeneralize typ)) + with UserError _ | Type_errors.TypeError _ -> + error_cannot_find_well_typed_abstraction env (evars_of evd) p l (**) +(* A refinement of [conv_pb]: the integers tells how many arguments + were applied in the context of the conversion problem; if the number + is non zero, steps of eta-expansion will be allowed +*) + +type conv_pb_up_to_eta = Cumul | ConvUnderApp of int * int + +let topconv = ConvUnderApp (0,0) +let of_conv_pb = function CONV -> topconv | CUMUL -> Cumul +let conv_pb_of = function ConvUnderApp _ -> CONV | Cumul -> CUMUL +let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb + +let opp_status = function + | IsSuperType -> IsSubType + | IsSubType -> IsSuperType + | ConvUpToEta _ | UserGiven as x -> x + +let add_type_status (x,y) = ((x,TypeNotProcessed),(y,TypeNotProcessed)) + +let extract_instance_status = function + | Cumul -> add_type_status (IsSubType, IsSuperType) + | ConvUnderApp (n1,n2) -> add_type_status (ConvUpToEta n1, ConvUpToEta n2) + +let rec assoc_pair x = function + [] -> raise Not_found + | (a,b,_)::l -> if compare a x = 0 then b else assoc_pair x l + +let rec subst_meta_instances bl c = + match kind_of_term c with + | Meta i -> (try assoc_pair i bl with Not_found -> c) + | _ -> map_constr (subst_meta_instances bl) c + let solve_pattern_eqn_array env f l c (metasubst,evarsubst) = match kind_of_term f with | Meta k -> - (k,solve_pattern_eqn env (Array.to_list l) c)::metasubst,evarsubst + let c = solve_pattern_eqn env (Array.to_list l) c in + let n = Array.length l - List.length (fst (decompose_lam c)) in + let pb = (ConvUpToEta n,TypeNotProcessed) in + (k,c,pb)::metasubst,evarsubst | Evar ev -> (* Currently unused: incompatible with eauto/eassumption backtracking *) - metasubst,(f,solve_pattern_eqn env (Array.to_list l) c)::evarsubst + metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst | _ -> assert false (*******************************) @@ -78,79 +118,207 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let unify_0 env sigma cv_pb mod_delta m n = - let trivial_unify pb substn m n = - if (not(occur_meta m)) && - (if mod_delta then is_fconv pb env sigma m n else eq_constr m n) - then substn - else error_cannot_unify env sigma (m,n) in - let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn = +type unify_flags = { + modulo_conv_on_closed_terms : Names.transparent_state option; + use_metas_eagerly : bool; + modulo_delta : Names.transparent_state; +} + +let default_unify_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; + use_metas_eagerly = true; + modulo_delta = full_transparent_state; +} + +let default_no_delta_unify_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; + use_metas_eagerly = true; + modulo_delta = empty_transparent_state; +} + +let expand_constant env flags c = + match kind_of_term c with + | Const cst when is_transparent (ConstKey cst) && + Cpred.mem cst (snd flags.modulo_delta) -> + constant_opt_value env cst + | Var id when is_transparent (VarKey id) && + Idpred.mem id (fst flags.modulo_delta) -> + named_body id env + | _ -> None + +let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = + let nb = nb_rel env in + let trivial_unify pb (metasubst,_) m n = + let subst = if flags.use_metas_eagerly then metasubst else fst subst in + match subst_defined_metas subst m with + | Some m -> + (match flags.modulo_conv_on_closed_terms with + Some flags -> + is_trans_fconv (conv_pb_of pb) flags env sigma m n + | None -> constr_cmp (conv_pb_of cv_pb) m n) + | _ -> constr_cmp (conv_pb_of cv_pb) m n in + let rec unirec_rec curenv pb b ((metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_castappevar sigma curm and cN = Evarutil.whd_castappevar sigma curn in match (kind_of_term cM,kind_of_term cN) with | Meta k1, Meta k2 -> + let stM,stN = extract_instance_status pb in if k1 < k2 - then (k1,cN)::metasubst,evarsubst - else if k1 = k2 then substn else (k2,cM)::metasubst,evarsubst + then (k1,cN,stN)::metasubst,evarsubst + else if k1 = k2 then substn + else (k2,cM,stM)::metasubst,evarsubst | Meta k, _ -> (* Here we check that [cN] does not contain any local variables *) - if (closedn (nb_rel env) cN) - then (k,cN)::metasubst,evarsubst - else error_cannot_unify_local curenv sigma (curenv,m,n,cN) + if (closedn nb cN) + then (k,cN,snd (extract_instance_status pb))::metasubst,evarsubst + else error_cannot_unify_local curenv sigma (m,n,cN) | _, Meta k -> (* Here we check that [cM] does not contain any local variables *) - if (closedn (nb_rel env) cM) - then (k,cM)::metasubst,evarsubst - else error_cannot_unify_local curenv sigma (curenv,m,n,cM) - | Evar _, _ -> metasubst,((cM,cN)::evarsubst) - | _, Evar _ -> metasubst,((cN,cM)::evarsubst) + if (closedn nb cM) + then (k,cM,fst (extract_instance_status pb))::metasubst,evarsubst + else error_cannot_unify_local curenv sigma (m,n,cM) + | Evar ev, _ -> metasubst,((ev,cN)::evarsubst) + | _, Evar ev -> metasubst,((ev,cM)::evarsubst) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push_rel_assum (na,t1) curenv) CONV - (unirec_rec curenv CONV substn t1 t2) c1 c2 + unirec_rec (push_rel_assum (na,t1) curenv) topconv true + (unirec_rec curenv topconv true substn t1 t2) c1 c2 | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push_rel_assum (na,t1) curenv) pb - (unirec_rec curenv CONV substn t1 t2) c1 c2 - | LetIn (_,b,_,c), _ -> unirec_rec curenv pb substn (subst1 b c) cN - | _, LetIn (_,b,_,c) -> unirec_rec curenv pb substn cM (subst1 b c) + unirec_rec (push_rel_assum (na,t1) curenv) (prod_pb pb) true + (unirec_rec curenv topconv true substn t1 t2) c1 c2 + | LetIn (_,a,_,c), _ -> unirec_rec curenv pb b substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenv pb b substn cM (subst1 a c) + | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> + array_fold_left2 (unirec_rec curenv topconv true) + (unirec_rec curenv topconv true + (unirec_rec curenv topconv true substn p1 p2) c1 c2) cl1 cl2 + | App (f1,l1), _ when - isMeta f1 & is_unification_pattern f1 l1 & not (dependent f1 cN) -> + isMeta f1 & is_unification_pattern curenv f1 l1 & + not (dependent f1 cN) -> solve_pattern_eqn_array curenv f1 l1 cN substn | _, App (f2,l2) when - isMeta f2 & is_unification_pattern f2 l2 & not (dependent f2 cM) -> + isMeta f2 & is_unification_pattern curenv f2 l2 & + not (dependent f2 cM) -> solve_pattern_eqn_array curenv f2 l2 cM substn | App (f1,l1), App (f2,l2) -> let len1 = Array.length l1 and len2 = Array.length l2 in - let (f1,l1,f2,l2) = - if len1 = len2 then (f1,l1,f2,l2) - else if len1 < len2 then - let extras,restl2 = array_chop (len2-len1) l2 in - (f1, l1, appvect (f2,extras), restl2) - else - let extras,restl1 = array_chop (len1-len2) l1 in - (appvect (f1,extras), restl1, f2, l2) in - (try - array_fold_left2 (unirec_rec curenv CONV) - (unirec_rec curenv CONV substn f1 f2) l1 l2 - with ex when precatchable_exception ex -> - trivial_unify pb substn cM cN) - | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> - array_fold_left2 (unirec_rec curenv CONV) - (unirec_rec curenv CONV - (unirec_rec curenv CONV substn p1 p2) c1 c2) cl1 cl2 - | _ -> trivial_unify pb substn cM cN + (try + let (f1,l1,f2,l2) = + if len1 = len2 then (f1,l1,f2,l2) + else if len1 < len2 then + let extras,restl2 = array_chop (len2-len1) l2 in + (f1, l1, appvect (f2,extras), restl2) + else + let extras,restl1 = array_chop (len1-len2) l1 in + (appvect (f1,extras), restl1, f2, l2) in + let pb = ConvUnderApp (len1,len2) in + array_fold_left2 (unirec_rec curenv topconv true) + (unirec_rec curenv pb true substn f1 f2) l1 l2 + with ex when precatchable_exception ex -> + expand curenv pb b substn cM f1 l1 cN f2 l2) + + | _ -> + let (f1,l1) = + match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in + let (f2,l2) = + match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in + expand curenv pb b substn cM f1 l1 cN f2 l2 + + and expand curenv pb b substn cM f1 l1 cN f2 l2 = + if trivial_unify pb substn cM cN then substn + else if b then + match expand_constant curenv flags f1 with + | Some c -> + unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN + | None -> + match expand_constant curenv flags f2 with + | Some c -> + unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2))) + | None -> + error_cannot_unify env sigma (cM,cN) + else + error_cannot_unify env sigma (cM,cN) + in if (not(occur_meta m)) && - (if mod_delta then is_fconv cv_pb env sigma m n else eq_constr m n) + (match flags.modulo_conv_on_closed_terms with + Some flags -> + is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n + | None -> constr_cmp (conv_pb_of cv_pb) m n) then - ([],[]) + subst else - let (mc,ec) = unirec_rec env cv_pb ([],[]) m n in - ((*sort_eqns*) mc, (*sort_eqns*) ec) + unirec_rec env cv_pb conv_at_top subst m n + +let unify_0 = unify_0_with_initial_metas ([],[]) true +let left = true +let right = false + +let pop k = if k=0 then 0 else k-1 + +let rec unify_with_eta keptside flags env sigma k1 k2 c1 c2 = + (* Reason up to limited eta-expansion: ci is allowed to start with ki lam *) + (* Question: try whd_betadeltaiota on ci if ki>0 ? *) + match kind_of_term c1, kind_of_term c2 with + | (Lambda (na,t1,c1'), Lambda (_,t2,c2')) -> + let env' = push_rel_assum (na,t1) env in + let metas,evars = unify_0 env sigma topconv flags t1 t2 in + let side,status,(metas',evars') = + unify_with_eta keptside flags env' sigma (pop k1) (pop k2) c1' c2' + in (side,status,(metas@metas',evars@evars')) + | (Lambda (na,t,c1'),_) when k2 > 0 -> + let env' = push_rel_assum (na,t) env in + let side = left in (* expansion on the right: we keep the left side *) + unify_with_eta side flags env' sigma (pop k1) (k2-1) + c1' (mkApp (lift 1 c2,[|mkRel 1|])) + | (_,Lambda (na,t,c2')) when k1 > 0 -> + let env' = push_rel_assum (na,t) env in + let side = right in (* expansion on the left: we keep the right side *) + unify_with_eta side flags env' sigma (k1-1) (pop k2) + (mkApp (lift 1 c1,[|mkRel 1|])) c2' + | _ -> + (keptside,ConvUpToEta(min k1 k2), + unify_0 env sigma topconv flags c1 c2) + +(* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'], + we now compute the problem on [u =? u'] and decide which of u or u' is kept + + Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically + in the case u' <= ?n <= u) + *) + +let merge_instances env sigma flags st1 st2 c1 c2 = + match (opp_status st1, st2) with + | (UserGiven, ConvUpToEta n2) -> + unify_with_eta left flags env sigma 0 n2 c1 c2 + | (ConvUpToEta n1, UserGiven) -> + unify_with_eta right flags env sigma n1 0 c1 c2 + | (ConvUpToEta n1, ConvUpToEta n2) -> + let side = left (* arbitrary choice, but agrees with compatibility *) in + unify_with_eta side flags env sigma n1 n2 c1 c2 + | ((IsSubType | ConvUpToEta _ | UserGiven as oppst1), + (IsSubType | ConvUpToEta _ | UserGiven)) -> + let res = unify_0 env sigma Cumul flags c2 c1 in + if oppst1=st2 then (* arbitrary choice *) (left, st1, res) + else if st2=IsSubType or st1=UserGiven then (left, st1, res) + else (right, st2, res) + | ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1), + (IsSuperType | ConvUpToEta _ | UserGiven)) -> + let res = unify_0 env sigma Cumul flags c1 c2 in + if oppst1=st2 then (* arbitrary choice *) (left, st1, res) + else if st2=IsSuperType or st1=UserGiven then (left, st1, res) + else (right, st2, res) + | (IsSuperType,IsSubType) -> + (try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1) + with _ -> (right, IsSubType, unify_0 env sigma Cumul flags c1 c2)) + | (IsSubType,IsSuperType) -> + (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2) + with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1)) (* Unification * @@ -208,7 +376,8 @@ let applyHead env evd n c = else match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with | Prod (_,c1,c2) -> - let (evd',evar) = Evarutil.new_evar evd env c1 in + let (evd',evar) = + Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' | _ -> error "Apply_Head_Then" in @@ -218,94 +387,167 @@ let is_mimick_head f = match kind_of_term f with (Const _|Var _|Rel _|Construct _|Ind _) -> true | _ -> false - + +let pose_all_metas_as_evars env evd t = + let evdref = ref evd in + let rec aux t = match kind_of_term t with + | Meta mv -> + (match Evd.meta_opt_fvalue !evdref mv with + | Some ({rebus=c},_) -> c + | None -> + let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in + let ty = if mvs = Evd.Metaset.empty then ty else aux ty in + let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in + evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref; + ev) + | _ -> + map_constr aux t in + let c = aux t in + (* side-effect *) + (!evdref, c) + +let try_to_coerce env evd c cty tycon = + let j = make_judge c cty in + let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in + let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in + if b then + let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in + (evd',j'.uj_val) + else + error "Cannot solve unification constraints" + +let w_coerce_to_type env evd c cty mvty = + let evd,mvty = pose_all_metas_as_evars env evd mvty in + let tycon = mk_tycon_type mvty in + try try_to_coerce env evd c cty tycon + with e when precatchable_exception e -> + (* inh_conv_coerce_rigid_to should have reasoned modulo reduction + but there are cases where it though it was not rigid (like in + fst (nat,nat)) and stops while it could have seen that it is rigid *) + let cty = Tacred.hnf_constr env (evars_of evd) cty in + try_to_coerce env evd c cty tycon + +let w_coerce env evd mv c = + let cty = get_type_of env (evars_of evd) c in + let mvty = Typing.meta_type evd mv in + w_coerce_to_type env evd c cty mvty + +let unify_to_type env evd flags c u = + let sigma = evars_of evd in + let c = refresh_universes c in + let t = get_type_of_with_meta env sigma (metas_of evd) c in + let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in + let u = Tacred.hnf_constr env sigma u in + try unify_0 env sigma Cumul flags t u + with e when precatchable_exception e -> ([],[]) + +let unify_type env evd flags mv c = + let mvty = Typing.meta_type evd mv in + if occur_meta mvty then + unify_to_type env evd flags c mvty + else ([],[]) + +(* Move metas that may need coercion at the end of the list of instances *) + +let order_metas metas = + let rec order latemetas = function + | [] -> List.rev latemetas + | (_,_,(status,to_type) as meta)::metas -> + if to_type = CoerceToType then order (meta::latemetas) metas + else meta :: order latemetas metas + in order [] metas + +(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) + +let solve_simple_evar_eqn env evd ev rhs = + let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in + if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs); + let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in + if not b then error "Cannot solve unification constraints"; + evd + (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] is true, unification of types of metas is required *) -let w_merge env with_types mod_delta metas evars evd = - let ty_metas = ref [] in - let ty_evars = ref [] in - let rec w_merge_rec evd metas evars = - match (evars,metas) with - | ([], []) -> evd - - | ((lhs,rhs)::t, metas) -> - (match kind_of_term rhs with - - | Meta k -> w_merge_rec evd ((k,lhs)::metas) t - - | krhs -> - (match kind_of_term lhs with - - | Evar (evn,_ as ev) -> - if is_defined_evar evd ev then - let (metas',evars') = - unify_0 env (evars_of evd) CONV mod_delta rhs lhs in - w_merge_rec evd (metas'@metas) (evars'@t) - else begin - let rhs' = - if occur_meta rhs then subst_meta metas rhs else rhs - in - if occur_evar evn rhs' then - error "w_merge: recursive equation"; - match krhs with - | App (f,cl) when is_mimick_head f -> - (try - w_merge_rec (fst (evar_define env ev rhs' evd)) metas t - with ex when precatchable_exception ex -> - let evd' = - mimick_evar evd mod_delta f (Array.length cl) evn in - w_merge_rec evd' metas evars) - | _ -> - (* ensure tail recursion in non-mimickable case! *) - w_merge_rec (fst (evar_define env ev rhs' evd)) metas t - end - - | _ -> anomaly "w_merge_rec")) - - | ([], (mv,n)::t) -> - if meta_defined evd mv then - let (metas',evars') = - unify_0 env (evars_of evd) CONV mod_delta - (meta_fvalue evd mv).rebus n in - w_merge_rec evd (metas'@t) evars' - else - begin - if with_types (* or occur_meta mvty *) then - (let mvty = Typing.meta_type evd mv in - try - let sigma = evars_of evd in - (* why not typing with the metamap ? *) - let nty = Typing.type_of env sigma (nf_meta evd n) in - let (mc,ec) = unify_0 env sigma CUMUL mod_delta nty mvty in - ty_metas := mc @ !ty_metas; - ty_evars := ec @ !ty_evars - with e when precatchable_exception e -> ()); - let evd' = meta_assign mv n evd in - w_merge_rec evd' t [] - end - - and mimick_evar evd mod_delta hdc nargs sp = +let w_merge env with_types flags (metas,evars) evd = + let rec w_merge_rec evd metas evars eqns = + + (* Process evars *) + match evars with + | ((evn,_ as ev),rhs)::evars' -> + if is_defined_evar evd ev then + let v = Evd.existential_value (evars_of evd) ev in + let (metas',evars'') = + unify_0 env (evars_of evd) topconv flags rhs v in + w_merge_rec evd (metas'@metas) (evars''@evars') eqns + else begin + let rhs' = subst_meta_instances metas rhs in + match kind_of_term rhs with + | App (f,cl) when is_mimick_head f & occur_meta rhs' -> + if occur_evar evn rhs' then + error_occur_check env (evars_of evd) evn rhs'; + let evd' = mimick_evar evd flags f (Array.length cl) evn in + w_merge_rec evd' metas evars eqns + | _ -> + w_merge_rec (solve_simple_evar_eqn env evd ev rhs') + metas evars' eqns + end + | [] -> + + (* Process metas *) + match metas with + | (mv,c,(status,to_type))::metas -> + let ((evd,c),(metas'',evars'')),eqns = + if with_types & to_type <> TypeProcessed then + if to_type = CoerceToType then + (* Some coercion may have to be inserted *) + (w_coerce env evd mv c,([],[])),[] + else + (* No coercion needed: delay the unification of types *) + ((evd,c),([],[])),(mv,c)::eqns + else + ((evd,c),([],[])),eqns in + if meta_defined evd mv then + let {rebus=c'},(status',_) = meta_fvalue evd mv in + let (take_left,st,(metas',evars')) = + merge_instances env (evars_of evd) flags status' status c' c + in + let evd' = + if take_left then evd + else meta_reassign mv (c,(st,TypeProcessed)) evd + in + w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns + else + let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in + w_merge_rec evd' (metas@metas'') evars'' eqns + | [] -> + + (* Process type eqns *) + match eqns with + | (mv,c)::eqns -> + let (metas,evars) = unify_type env evd flags mv c in + w_merge_rec evd metas evars eqns + | [] -> evd + + and mimick_evar evd flags hdc nargs sp = let ev = Evd.find (evars_of evd) sp in let sp_env = Global.env_of_context ev.evar_hyps in let (evd', c) = applyHead sp_env evd nargs hdc in let (mc,ec) = - unify_0 sp_env (evars_of evd') CUMUL mod_delta + unify_0 sp_env (evars_of evd') Cumul flags (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl in - let evd'' = w_merge_rec evd' mc ec in + let evd'' = w_merge_rec evd' mc ec [] in if (evars_of evd') == (evars_of evd'') then Evd.evar_define sp c evd'' else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in (* merge constraints *) - let evd' = w_merge_rec evd metas evars in - if with_types then - (* merge constraints about types: if they fail, don't worry *) - try w_merge_rec evd' !ty_metas !ty_evars - with e when precatchable_exception e -> evd' - else - evd' + w_merge_rec evd (order_metas metas) evars [] + +let w_unify_meta_types env ?(flags=default_unify_flags) evd = + let metas,evd = retract_coercible_metas evd in + w_merge env true flags (metas,[]) evd (* [w_unify env evd M N] performs a unification of M and N, generating a bunch of @@ -317,9 +559,22 @@ let w_merge env with_types mod_delta metas evars evd = [clenv_typed_unify M N clenv] expects in addition that expected types of metavars are unifiable with the types of their instances *) -let w_unify_core_0 env with_types cv_pb mod_delta m n evd = - let (mc,ec) = unify_0 env (evars_of evd) cv_pb mod_delta m n in - w_merge env with_types mod_delta mc ec evd +let check_types env evd subst m n = + if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then + unify_0_with_initial_metas subst true env (evars_of evd) topconv + default_unify_flags + (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m) + (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n) + else + subst + +let w_unify_core_0 env with_types cv_pb flags m n evd = + let (mc1,evd') = retract_coercible_metas evd in + let subst1 = check_types env evd (mc1,[]) m n in + let subst2 = + unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n + in + w_merge env with_types flags subst2 evd' let w_unify_0 env = w_unify_core_0 env false let w_typed_unify env = w_unify_core_0 env true @@ -341,12 +596,12 @@ let iter_fail f a = (* Tries to find an instance of term [cl] in term [op]. Unifies [cl] to every subterm of [op] until it finds a match. Fails if no match is found *) -let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd = +let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd = let rec matchrec cl = let cl = strip_outer_cast cl in (try if closed0 cl - then w_unify_0 env CONV mod_delta op cl evd,cl + then w_unify_0 env topconv flags op cl evd,cl else error "Bound 1" with ex when precatchable_exception ex -> (match kind_of_term cl with @@ -396,9 +651,9 @@ let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd = in try matchrec cl with ex when precatchable_exception ex -> - raise (PretypeError (env,NoOccurrenceFound op)) + raise (PretypeError (env,NoOccurrenceFound (op, None))) -let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = +let w_unify_to_subterm_list env flags allow_K oplist t evd = List.fold_right (fun op (evd,l) -> if isMeta op then @@ -408,7 +663,7 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = let (evd',cl) = try (* This is up to delta for subterms w/o metas ... *) - w_unify_to_subterm env ~mod_delta (strip_outer_cast op,t) evd + w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) in (evd',cl::l) @@ -416,37 +671,37 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = (evd,op::l) else (* This is not up to delta ... *) - raise (PretypeError (env,NoOccurrenceFound op))) + raise (PretypeError (env,NoOccurrenceFound (op, None)))) oplist (evd,[]) -let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd = - let sigma = evars_of evd in +let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = + (* Remove delta when looking for a subterm *) + let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in let (evd',cllist) = - w_unify_to_subterm_list env mod_delta allow_K oplist typ evd in + w_unify_to_subterm_list env flags allow_K oplist typ evd in let typp = Typing.meta_type evd' p in - let pred = abstract_list_all env sigma typp typ cllist in - w_unify_0 env CONV mod_delta (mkMeta p) pred evd' + let pred = abstract_list_all env evd' typp typ cllist in + w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd' -let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd = +let w_unify2 env flags allow_K cv_pb ty1 ty2 evd = let c1, oplist1 = whd_stack ty1 in let c2, oplist2 = whd_stack ty2 in match kind_of_term c1, kind_of_term c2 with | Meta p1, _ -> (* Find the predicate *) let evd' = - secondOrderAbstraction env mod_delta allow_K ty2 (p1,oplist1) evd in + secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in (* Resume first order unification *) - w_unify_0 env cv_pb mod_delta (nf_meta evd' ty1) ty2 evd' + w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd' | _, Meta p2 -> (* Find the predicate *) let evd' = - secondOrderAbstraction env mod_delta allow_K ty1 (p2, oplist2) evd in + secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in (* Resume first order unification *) - w_unify_0 env cv_pb mod_delta ty1 (nf_meta evd' ty2) evd' + w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd' | _ -> error "w_unify2" - (* The unique unification algorithm works like this: If the pattern is flexible, and the goal has a lambda-abstraction at the head, then we do a first-order unification. @@ -467,7 +722,8 @@ let w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd = Before, second-order was used if the type of Meta(1) and [x:A]t was convertible and first-order otherwise. But if failed if e.g. the type of Meta(1) had meta-variables in it. *) -let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd = +let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd = + let cv_pb = of_conv_pb cv_pb in let hd1,l1 = whd_stack ty1 in let hd2,l2 = whd_stack ty2 in match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with @@ -475,25 +731,22 @@ let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd = | (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true) when List.length l1 = List.length l2 -> (try - w_typed_unify env cv_pb mod_delta ty1 ty2 evd + w_typed_unify env cv_pb flags ty1 ty2 evd with ex when precatchable_exception ex -> try - w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound c) as e -> raise e - | ex when precatchable_exception ex -> - error "Cannot solve a second-order unification problem") + w_unify2 env flags allow_K cv_pb ty1 ty2 evd + with PretypeError (env,NoOccurrenceFound _) as e -> raise e) (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try - w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd - with PretypeError (env,NoOccurrenceFound c) as e -> raise e + w_unify2 env flags allow_K cv_pb ty1 ty2 evd + with PretypeError (env,NoOccurrenceFound _) as e -> raise e | ex when precatchable_exception ex -> try - w_typed_unify env cv_pb mod_delta ty1 ty2 evd - with ex when precatchable_exception ex -> - error "Cannot solve a second-order unification problem") + w_typed_unify env cv_pb flags ty1 ty2 evd + with ex' when precatchable_exception ex' -> + raise ex) (* General case: try first order *) - | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd - + | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd -- cgit v1.2.3