summaryrefslogtreecommitdiff
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r--pretyping/unification.ml583
1 files changed, 418 insertions, 165 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 12:17:57 +0000