From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- pretyping/unification.ml | 471 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 471 insertions(+) create mode 100644 pretyping/unification.ml (limited to 'pretyping/unification.ml') diff --git a/pretyping/unification.ml b/pretyping/unification.ml new file mode 100644 index 00000000..e51f5e0e --- /dev/null +++ b/pretyping/unification.ml @@ -0,0 +1,471 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let na = match kind_of_term a with Var id -> Name id | _ -> na in + 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 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 + try + if is_conv_leq env sigma (Typing.type_of env sigma p) typ then p + else error "abstract_list_all" + with UserError _ -> + raise (PretypeError (env,CannotGeneralize typ)) + + +(*******************************) + +(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n] + renvoie deux listes: + + metasubst:(int*constr)list récolte les instances des (Meta k) + evarsubst:(constr*constr)list récolte les instances des (Const "?k") + + Attention : pas d'unification entre les différences instances d'une + même meta ou evar, il peut rester des doublons *) + +(* Unification order: *) +(* Left to right: unifies first argument and then the other arguments *) +(*let unify_l2r x = List.rev x +(* Right to left: unifies last argument and then the other arguments *) +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 pb ((metasubst,evarsubst) as substn) m n = + let cM = Evarutil.whd_castappevar sigma m + and cN = Evarutil.whd_castappevar sigma n in + match (kind_of_term cM,kind_of_term cN) with + | Meta k1, Meta k2 -> + if k1 < k2 then (k1,cN)::metasubst,evarsubst + else if k1 = k2 then substn + else (k2,cM)::metasubst,evarsubst + | Meta k, _ -> (k,cN)::metasubst,evarsubst + | _, Meta k -> (k,cM)::metasubst,evarsubst + | Evar _, _ -> metasubst,((cM,cN)::evarsubst) + | _, Evar _ -> metasubst,((cN,cM)::evarsubst) + + | Lambda (_,t1,c1), Lambda (_,t2,c2) -> + unirec_rec CONV (unirec_rec CONV substn t1 t2) c1 c2 + | Prod (_,t1,c1), Prod (_,t2,c2) -> + unirec_rec pb (unirec_rec CONV substn t1 t2) c1 c2 + | LetIn (_,b,_,c), _ -> unirec_rec pb substn (subst1 b c) cN + | _, LetIn (_,b,_,c) -> unirec_rec pb substn cM (subst1 b c) + + | 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 CONV) + (unirec_rec 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 CONV) + (unirec_rec CONV (unirec_rec CONV substn p1 p2) c1 c2) cl1 cl2 + + | _ -> trivial_unify pb substn 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) + then + ([],[]) + else + let (mc,ec) = unirec_rec cv_pb ([],[]) m n in + ((*sort_eqns*) mc, (*sort_eqns*) ec) + + +(* Unification + * + * Procedure: + * (1) The function [unify mc wc M N] produces two lists: + * (a) a list of bindings Meta->RHS + * (b) a list of bindings EVAR->RHS + * + * The Meta->RHS bindings cannot themselves contain + * meta-vars, so they get applied eagerly to the other + * bindings. This may or may not close off all RHSs of + * the EVARs. For each EVAR whose RHS is closed off, + * we can just apply it, and go on. For each which + * is not closed off, we need to do a mimick step - + * in general, we have something like: + * + * ?X == (c e1 e2 ... ei[Meta(k)] ... en) + * + * so we need to do a mimick step, converting ?X + * into + * + * ?X -> (c ?z1 ... ?zn) + * + * of the proper types. Then, we can decompose the + * equation into + * + * ?z1 --> e1 + * ... + * ?zi --> ei[Meta(k)] + * ... + * ?zn --> en + * + * and keep on going. Whenever we find that a R.H.S. + * is closed, we can, as before, apply the constraint + * directly. Whenever we find an equation of the form: + * + * ?z -> Meta(n) + * + * we can reverse the equation, put it into our metavar + * substitution, and keep going. + * + * The most efficient mimick possible is, for each + * Meta-var remaining in the term, to declare a + * new EVAR of the same type. This is supposedly + * determinable from the clausale form context - + * we look up the metavar, take its type there, + * and apply the metavar substitution to it, to + * close it off. But this might not always work, + * since other metavars might also need to be resolved. *) + +let applyHead env evd n c = + let rec apprec n c cty evd = + if n = 0 then + (evd, 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 + apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd' + | _ -> error "Apply_Head_Then" + in + apprec n c (Typing.type_of env (evars_of evd) c) evd + +let is_mimick_head f = + match kind_of_term f with + (Const _|Var _|Rel _|Construct _|Ind _) -> true + | _ -> false + +(* [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 ev = Evd.map (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 + (Retyping.get_type_of sp_env (evars_of evd') c) ev.evar_concl 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_unify env evd M N] + performs a unification of M and N, generating a bunch of + unification constraints in the process. These constraints + are processed, one-by-one - they may either generate new + bindings, or, if there is already a binding, new unifications, + which themselves generate new constraints. This continues + until we get failure, or we run out of constraints. + [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 w_unify_0 env = w_unify_core_0 env false +let w_typed_unify env = w_unify_core_0 env true + + +(* takes a substitution s, an open term op and a closed term cl + try to find a subterm of cl which matches op, if op is just a Meta + FAIL because we cannot find a binding *) + +let iter_fail f a = + let n = Array.length a in + let rec ffail i = + if i = n then error "iter_fail" + else + try f a.(i) + with ex when precatchable_exception ex -> ffail (i+1) + in ffail 0 + +(* 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 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 + else error "Bound 1" + with ex when precatchable_exception ex -> + (match kind_of_term cl with + | App (f,args) -> + let n = Array.length args in + assert (n>0); + let c1 = mkApp (f,Array.sub args 0 (n-1)) in + let c2 = args.(n-1) in + (try + matchrec c1 + with ex when precatchable_exception ex -> + matchrec c2) + | Case(_,_,c,lf) -> (* does not search in the predicate *) + (try + matchrec c + with ex when precatchable_exception ex -> + iter_fail matchrec lf) + | LetIn(_,c1,_,c2) -> + (try + matchrec c1 + with ex when precatchable_exception ex -> + matchrec c2) + + | Fix(_,(_,types,terms)) -> + (try + iter_fail matchrec types + with ex when precatchable_exception ex -> + iter_fail matchrec terms) + + | CoFix(_,(_,types,terms)) -> + (try + iter_fail matchrec types + with ex when precatchable_exception ex -> + iter_fail matchrec terms) + + | Prod (_,t,c) -> + (try + matchrec t + with ex when precatchable_exception ex -> + matchrec c) + | Lambda (_,t,c) -> + (try + matchrec t + with ex when precatchable_exception ex -> + matchrec c) + | _ -> error "Match_subterm")) + in + try matchrec cl + with ex when precatchable_exception ex -> + raise (PretypeError (env,NoOccurrenceFound op)) + +let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = + List.fold_right + (fun op (evd,l) -> + if isMeta op then + if allow_K then (evd,op::l) + else error "Match_subterm" + else if occur_meta op then + 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 + with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op) + in + (evd',cl::l) + else if allow_K or dependent op t then + (evd,op::l) + else + (* This is not up to delta ... *) + raise (PretypeError (env,NoOccurrenceFound op))) + oplist + (evd,[]) + +let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd = + let sigma = evars_of evd in + let (evd',cllist) = + w_unify_to_subterm_list env mod_delta 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 w_unify2 env mod_delta 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 + (* Resume first order unification *) + w_unify_0 env cv_pb mod_delta (nf_meta evd' ty1) ty2 evd' + | _, Meta p2 -> + (* Find the predicate *) + let evd' = + secondOrderAbstraction env mod_delta 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' + | _ -> 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. + + If the pattern is not flexible, then we do a first-order + unification, too. + + If the pattern is flexible, and the goal doesn't have a + lambda-abstraction head, then we second-order unification. *) + +(* We decide here if first-order or second-order unif is used for Apply *) +(* We apply a term of type (ai:Ai)C and try to solve a goal C' *) +(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve *) + +(* 3-4-99 [HH] New fo/so choice heuristic : + In case we have to unify (Meta(1) args) with ([x:A]t args') + we first try second-order unification and if it fails first-order. + 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 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 + (* Pattern case *) + | (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 + 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") + + (* 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 + | 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") + + (* General case: try first order *) + | _ -> w_unify_0 env cv_pb mod_delta ty1 ty2 evd + -- cgit v1.2.3