diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 17 | ||||
| -rw-r--r-- | pretyping/clenv.mli | 9 | ||||
| -rw-r--r-- | pretyping/unification.ml | 120 | ||||
| -rw-r--r-- | pretyping/unification.mli | 10 |
4 files changed, 84 insertions, 72 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index b9881aaf04..18a22e5c71 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -241,18 +241,19 @@ let clenv_missing ce = clenv_dependent true ce (******************************************************************) -let clenv_unify allow_K cv_pb t1 t2 clenv = - { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd } +let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv = + { clenv with + evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd } -let clenv_unify_meta_types clenv = - { clenv with evd = w_unify_meta_types clenv.env clenv.evd } +let clenv_unify_meta_types ?(flags=default_unify_flags) clenv = + { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } -let clenv_unique_resolver allow_K clenv gl = +let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl = if isMeta (fst (whd_stack clenv.templtyp.rebus)) then - clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) - (clenv_unify_meta_types clenv) + clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl) + (clenv_unify_meta_types ~flags:flags clenv) else - clenv_unify allow_K CUMUL + clenv_unify allow_K CUMUL ~flags:flags (meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv (* [clenv_pose_dependent_evars clenv] diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 8546a44ef3..e6cd960b20 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -18,6 +18,7 @@ open Evd open Evarutil open Mod_subst open Rawterm +open Unification (*i*) (***************************************************************) @@ -69,16 +70,16 @@ val clenv_fchain : (* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *) val clenv_unify : - bool -> conv_pb -> constr -> constr -> clausenv -> clausenv + bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv (* unifies the concl of the goal with the type of the clenv *) val clenv_unique_resolver : - bool -> clausenv -> evar_info sigma -> clausenv + bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv (* same as above ([allow_K=false]) but replaces remaining metas with fresh evars if [evars_flag] is [true] *) val evar_clenv_unique_resolver : - bool -> clausenv -> evar_info sigma -> clausenv + bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv val clenv_pose_dependent_evars : clausenv -> clausenv @@ -98,7 +99,7 @@ val clenv_constrain_last_binding : constr -> clausenv -> clausenv (* defines metas corresponding to the name of the bindings *) val clenv_match_args : arg_bindings -> clausenv -> clausenv -val clenv_unify_meta_types : clausenv -> clausenv +val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (* start with a clenv to refine with a given term with bindings *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b2190c53cf..cac80301f8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -114,12 +114,17 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n = +type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool } + +let default_unify_flags = { modulo_delta = true; use_metas_eagerly = true } + +let unify_0_with_initial_metas metas env sigma cv_pb flags m n = let nb = nb_rel env in let trivial_unify pb (metasubst,_ as substn) m n = - match subst_defined_metas (* too strong: metasubst *) metas m with + let metas = if flags.use_metas_eagerly then metasubst else metas in + match subst_defined_metas metas m with | Some m when - (if mod_delta then is_fconv (conv_pb_of pb) env sigma m n + (if flags.modulo_delta then is_fconv (conv_pb_of pb) env sigma m n else eq_constr m n) -> substn | _ -> error_cannot_unify env sigma (m,n) in let rec unirec_rec curenv pb ((metasubst,evarsubst) as substn) curm curn = @@ -185,7 +190,7 @@ let unify_0_with_initial_metas metas env sigma cv_pb mod_delta m n = | _ -> trivial_unify pb substn cM cN in if (not(occur_meta m)) && - (if mod_delta then is_fconv (conv_pb_of cv_pb) env sigma m n + (if flags.modulo_delta then is_fconv (conv_pb_of cv_pb) env sigma m n else eq_constr m n) then (metas,[]) @@ -200,29 +205,29 @@ let right = false let pop k = if k=0 then 0 else k-1 -let rec unify_with_eta keptside mod_delta env sigma k1 k2 c1 c2 = +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 mod_delta t1 t2 in + let metas,evars = unify_0 env sigma topconv flags t1 t2 in let side,status,(metas',evars') = - unify_with_eta keptside mod_delta env' sigma (pop k1) (pop k2) c1' c2' + 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 mod_delta env' sigma (pop k1) (k2-1) + 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 mod_delta env' sigma (k1-1) (pop k2) + 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 mod_delta c1 c2) + 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 @@ -231,33 +236,33 @@ let rec unify_with_eta keptside mod_delta env sigma k1 k2 c1 c2 = in the case u' <= ?n <= u) *) -let merge_instances env sigma mod_delta st1 st2 c1 c2 = +let merge_instances env sigma flags st1 st2 c1 c2 = match (opp_status st1, st2) with | (UserGiven, ConvUpToEta n2) -> - unify_with_eta left mod_delta env sigma 0 n2 c1 c2 + unify_with_eta left flags env sigma 0 n2 c1 c2 | (ConvUpToEta n1, UserGiven) -> - unify_with_eta right mod_delta env sigma n1 0 c1 c2 + 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 mod_delta env sigma n1 n2 c1 c2 + 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 mod_delta c2 c1 in + 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 mod_delta c1 c2 in + 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 mod_delta c2 c1) - with _ -> (right, IsSubType, unify_0 env sigma Cumul mod_delta c1 c2)) + (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 mod_delta c1 c2) - with _ -> (right, IsSuperType, unify_0 env sigma Cumul mod_delta c2 c1)) + (try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2) + with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1)) (* Unification * @@ -336,13 +341,13 @@ let w_coerce env c ctyp target evd = with e when precatchable_exception e -> evd,c -let unify_to_type env evd mod_delta c u = +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 mod_delta t u + try unify_0 env sigma Cumul flags t u with e when precatchable_exception e -> ([],[]) let coerce_to_type env evd c u = @@ -350,19 +355,19 @@ let coerce_to_type env evd c u = let t = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in w_coerce env c t u evd -let unify_or_coerce_type env evd mod_delta mv c = +let unify_or_coerce_type env evd flags mv c = let mvty = Typing.meta_type evd mv in (* nf_betaiota was before in type_of - useful to reduce types like (x:A)([x]P u) *) if occur_meta mvty then - (evd,c),unify_to_type env evd mod_delta c mvty + (evd,c),unify_to_type env evd flags c mvty else coerce_to_type env evd c mvty,([],[]) -let unify_type env evd mod_delta mv c = +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 mod_delta c mvty + unify_to_type env evd flags c mvty else ([],[]) (* Move metas that may need coercion at the end of the list of instances *) @@ -379,7 +384,7 @@ let order_metas 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 w_merge env with_types flags metas evars evd = let rec w_merge_rec evd metas evars eqns = (* Process evars *) @@ -388,7 +393,7 @@ let w_merge env with_types mod_delta metas evars evd = 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 mod_delta rhs v in + 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 @@ -400,7 +405,7 @@ let w_merge env with_types mod_delta metas evars evd = metas evars' eqns with ex when precatchable_exception ex -> let evd' = - mimick_evar evd mod_delta f (Array.length cl) evn in + mimick_evar evd flags f (Array.length cl) evn in w_merge_rec evd' metas evars eqns) | _ -> (* ensure tail recursion in non-mimickable case! *) @@ -415,7 +420,7 @@ let w_merge env with_types mod_delta metas evars evd = if with_types & to_type <> TypeProcessed then if to_type = CoerceToType then (* Some coercion may have to be inserted *) - (unify_or_coerce_type env evd mod_delta mv c,[]) + (unify_or_coerce_type env evd flags mv c,[]) else (* No coercion needed: delay the unification of types *) ((evd,c),([],[])),(mv,c)::eqns @@ -424,7 +429,7 @@ let w_merge env with_types mod_delta metas evars evd = 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) mod_delta status' status c' c + merge_instances env (evars_of evd) flags status' status c' c in let evd' = if take_left then evd @@ -439,16 +444,16 @@ let w_merge env with_types mod_delta metas evars evd = (* Process type eqns *) match eqns with | (mv,c)::eqns -> - let (metas,evars) = unify_type env evd mod_delta mv c in + let (metas,evars) = unify_type env evd flags mv c in w_merge_rec evd metas evars eqns | [] -> evd - and mimick_evar evd mod_delta hdc nargs sp = + 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 if (evars_of evd') == (evars_of evd'') @@ -458,9 +463,9 @@ let w_merge env with_types mod_delta metas evars evd = (* merge constraints *) w_merge_rec evd (order_metas metas) evars [] -let w_unify_meta_types env evd = +let w_unify_meta_types env ?(flags=default_unify_flags) evd = let metas,evd = retract_coercible_metas evd in - w_merge env true true metas [] evd + w_merge env true flags metas [] evd (* [w_unify env evd M N] performs a unification of M and N, generating a bunch of @@ -472,11 +477,12 @@ let w_unify_meta_types env 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 w_unify_core_0 env with_types cv_pb flags m n evd = let (mc1,evd') = retract_coercible_metas evd in let (mc2,ec) = - unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb mod_delta m n in - w_merge env with_types mod_delta mc2 ec evd' + unify_0_with_initial_metas mc1 env (evars_of evd') cv_pb flags m n + in + w_merge env with_types flags mc2 ec evd' let w_unify_0 env = w_unify_core_0 env false let w_typed_unify env = w_unify_core_0 env true @@ -498,12 +504,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 topconv 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 @@ -555,7 +561,7 @@ let w_unify_to_subterm env ?(mod_delta=true) (op,cl) evd = 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 = +let w_unify_to_subterm_list env flags allow_K oplist t evd = List.fold_right (fun op (evd,l) -> if isMeta op then @@ -565,7 +571,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) @@ -577,29 +583,29 @@ let w_unify_to_subterm_list env mod_delta allow_K oplist t evd = oplist (evd,[]) -let secondOrderAbstraction env mod_delta allow_K typ (p, oplist) evd = +let secondOrderAbstraction env flags allow_K typ (p, oplist) evd = 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 evd' typp typ cllist in - w_unify_0 env topconv mod_delta (mkMeta p) pred evd' + w_unify_0 env topconv flags (mkMeta p) pred 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" @@ -623,7 +629,7 @@ 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 @@ -632,10 +638,10 @@ 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 + w_unify2 env flags 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") @@ -643,14 +649,14 @@ let w_unify allow_K env cv_pb ?(mod_delta=true) ty1 ty2 evd = (* Second order case *) | (Meta _, true, _, _ | _, _, Meta _, true) -> (try - w_unify2 env mod_delta allow_K cv_pb ty1 ty2 evd + w_unify2 env flags 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 + w_typed_unify env cv_pb flags ty1 ty2 evd with ex when precatchable_exception ex -> error "Cannot solve a second-order unification problem") (* General case: try first order *) - | _ -> w_typed_unify env cv_pb mod_delta ty1 ty2 evd + | _ -> w_typed_unify env cv_pb flags ty1 ty2 evd diff --git a/pretyping/unification.mli b/pretyping/unification.mli index d2cb20550b..f0717b2a70 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -14,17 +14,21 @@ open Environ open Evd (*i*) +type unify_flags = { modulo_delta : bool; use_metas_eagerly : bool } + +val default_unify_flags : unify_flags + (* The "unique" unification fonction *) val w_unify : - bool -> env -> conv_pb -> ?mod_delta:bool -> constr -> constr -> evar_defs -> evar_defs + bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_defs -> evar_defs (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) val w_unify_to_subterm : - env -> ?mod_delta:bool -> constr * constr -> evar_defs -> evar_defs * constr + env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr -val w_unify_meta_types : env -> evar_defs -> evar_defs +val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs (*i This should be in another module i*) |