1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: unification.ml 12163 2009-06-06 17:36:47Z herbelin $ *)
29
(* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
30
gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
32
let abstract_scheme env c l lname_typ =
34
(fun t (locc,a) (na,_,ta) ->
35
let na = match kind_of_term a with Var id -> Name id | _ -> na in
36
(* [occur_meta ta] test removed for support of eelim/ecase but consequences
38
if occur_meta ta then error "cannot find a type for the generalisation"
39
else *) if occur_meta a then lambda_name env (na,ta,t)
40
else lambda_name env (na,ta,subst_term_occ locc a t))
45
let abstract_list_all env evd typ c l =
46
let ctxt,_ = decomp_n_prod env (evars_of evd) (List.length l) typ in
47
let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
48
let p = abstract_scheme env c l_with_all_occs ctxt in
50
if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
51
else error "abstract_list_all"
52
with UserError _ | Type_errors.TypeError _ ->
53
error_cannot_find_well_typed_abstraction env (evars_of evd) p l
57
(* A refinement of [conv_pb]: the integers tells how many arguments
58
were applied in the context of the conversion problem; if the number
59
is non zero, steps of eta-expansion will be allowed
62
type conv_pb_up_to_eta = Cumul | ConvUnderApp of int * int
64
let topconv = ConvUnderApp (0,0)
65
let of_conv_pb = function CONV -> topconv | CUMUL -> Cumul
66
let conv_pb_of = function ConvUnderApp _ -> CONV | Cumul -> CUMUL
67
let prod_pb = function ConvUnderApp _ -> topconv | pb -> pb
69
let opp_status = function
70
| IsSuperType -> IsSubType
71
| IsSubType -> IsSuperType
72
| ConvUpToEta _ | UserGiven as x -> x
74
let add_type_status (x,y) = ((x,TypeNotProcessed),(y,TypeNotProcessed))
76
let extract_instance_status = function
77
| Cumul -> add_type_status (IsSubType, IsSuperType)
78
| ConvUnderApp (n1,n2) -> add_type_status (ConvUpToEta n1, ConvUpToEta n2)
80
let rec assoc_pair x = function
82
| (a,b,_)::l -> if compare a x = 0 then b else assoc_pair x l
84
let rec subst_meta_instances bl c =
85
match kind_of_term c with
86
| Meta i -> (try assoc_pair i bl with Not_found -> c)
87
| _ -> map_constr (subst_meta_instances bl) c
89
let solve_pattern_eqn_array (env,nb) sigma f l c (metasubst,evarsubst) =
90
match kind_of_term f with
92
let c = solve_pattern_eqn env (Array.to_list l) c in
93
let n = Array.length l - List.length (fst (decompose_lam c)) in
94
let pb = (ConvUpToEta n,TypeNotProcessed) in
95
if noccur_between 1 nb c then
96
(k,lift (-nb) c,pb)::metasubst,evarsubst
97
else error_cannot_unify_local env sigma (mkApp (f, l),c,c)
99
(* Currently unused: incompatible with eauto/eassumption backtracking *)
100
metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
103
let push d (env,n) = (push_rel_assum d env,n+1)
105
(*******************************)
107
(* Unification � l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
110
metasubst:(int*constr)list r�colte les instances des (Meta k)
111
evarsubst:(constr*constr)list r�colte les instances des (Const "?k")
113
Attention : pas d'unification entre les diff�rences instances d'une
114
m�me meta ou evar, il peut rester des doublons *)
116
(* Unification order: *)
117
(* Left to right: unifies first argument and then the other arguments *)
118
(*let unify_l2r x = List.rev x
119
(* Right to left: unifies last argument and then the other arguments *)
122
let sort_eqns = unify_r2l
126
modulo_conv_on_closed_terms : Names.transparent_state option;
127
use_metas_eagerly : bool;
128
modulo_delta : Names.transparent_state;
131
let default_unify_flags = {
132
modulo_conv_on_closed_terms = Some full_transparent_state;
133
use_metas_eagerly = true;
134
modulo_delta = full_transparent_state;
137
let default_no_delta_unify_flags = {
138
modulo_conv_on_closed_terms = Some full_transparent_state;
139
use_metas_eagerly = true;
140
modulo_delta = empty_transparent_state;
143
let expand_key env = function
144
| Some (ConstKey cst) -> constant_opt_value env cst
145
| Some (VarKey id) -> named_body id env
146
| Some (RelKey _) -> None
150
match kind_of_term f with
151
| Const cst when is_transparent (ConstKey cst) &&
152
Cpred.mem cst (snd flags.modulo_delta) ->
154
| Var id when is_transparent (VarKey id) &&
155
Idpred.mem id (fst flags.modulo_delta) ->
159
let oracle_order env cf1 cf2 =
164
| Some k2 -> Some false)
168
| Some k2 -> Some (Conv_oracle.oracle_order k1 k2)
170
let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
171
let trivial_unify curenv pb (metasubst,_) m n =
172
let subst = if flags.use_metas_eagerly then metasubst else fst subst in
173
match subst_defined_metas subst m with
175
if (match flags.modulo_conv_on_closed_terms with
177
is_trans_fconv (conv_pb_of pb) flags env sigma m1 n
178
| None -> false) then true else
179
if (not (is_ground_term (create_evar_defs sigma) m1))
180
|| occur_meta_or_existential n then false else
181
error_cannot_unify curenv sigma (m, n)
183
let rec unirec_rec (curenv,nb as curenvnb) pb b ((metasubst,evarsubst) as substn) curm curn =
184
let cM = Evarutil.whd_castappevar sigma curm
185
and cN = Evarutil.whd_castappevar sigma curn in
186
match (kind_of_term cM,kind_of_term cN) with
187
| Meta k1, Meta k2 ->
188
let stM,stN = extract_instance_status pb in
190
then (k1,cN,stN)::metasubst,evarsubst
191
else if k1 = k2 then substn
192
else (k2,cM,stM)::metasubst,evarsubst
193
| Meta k, _ when not (dependent cM cN) ->
194
(* Here we check that [cN] does not contain any local variables *)
196
(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
197
else if noccur_between 1 nb cN then
198
(k,lift (-nb) cN,snd (extract_instance_status pb))::metasubst,
200
else error_cannot_unify_local curenv sigma (m,n,cN)
201
| _, Meta k when not (dependent cN cM) ->
202
(* Here we check that [cM] does not contain any local variables *)
204
(k,cM,snd (extract_instance_status pb))::metasubst,evarsubst
205
else if noccur_between 1 nb cM
207
(k,lift (-nb) cM,fst (extract_instance_status pb))::metasubst,
209
else error_cannot_unify_local curenv sigma (m,n,cM)
210
| Evar ev, _ -> metasubst,((ev,cN)::evarsubst)
211
| _, Evar ev -> metasubst,((ev,cM)::evarsubst)
212
| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
213
unirec_rec (push (na,t1) curenvnb) topconv true
214
(unirec_rec curenvnb topconv true substn t1 t2) c1 c2
215
| Prod (na,t1,c1), Prod (_,t2,c2) ->
216
unirec_rec (push (na,t1) curenvnb) (prod_pb pb) true
217
(unirec_rec curenvnb topconv true substn t1 t2) c1 c2
218
| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b substn (subst1 a c) cN
219
| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b substn cM (subst1 a c)
221
| Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) ->
222
array_fold_left2 (unirec_rec curenvnb topconv true)
223
(unirec_rec curenvnb topconv true
224
(unirec_rec curenvnb topconv true substn p1 p2) c1 c2) cl1 cl2
226
| App (f1,l1), _ when
227
isMeta f1 & is_unification_pattern curenvnb f1 l1 cN &
228
not (dependent f1 cN) ->
229
solve_pattern_eqn_array curenvnb sigma f1 l1 cN substn
231
| _, App (f2,l2) when
232
isMeta f2 & is_unification_pattern curenvnb f2 l2 cM &
233
not (dependent f2 cM) ->
234
solve_pattern_eqn_array curenvnb sigma f2 l2 cM substn
236
| App (f1,l1), App (f2,l2) ->
237
let len1 = Array.length l1
238
and len2 = Array.length l2 in
241
if len1 = len2 then (f1,l1,f2,l2)
242
else if len1 < len2 then
243
let extras,restl2 = array_chop (len2-len1) l2 in
244
(f1, l1, appvect (f2,extras), restl2)
246
let extras,restl1 = array_chop (len1-len2) l1 in
247
(appvect (f1,extras), restl1, f2, l2) in
248
let pb = ConvUnderApp (len1,len2) in
249
array_fold_left2 (unirec_rec curenvnb topconv true)
250
(unirec_rec curenvnb pb true substn f1 f2) l1 l2
251
with ex when precatchable_exception ex ->
252
expand curenvnb pb b substn cM f1 l1 cN f2 l2)
255
if constr_cmp (conv_pb_of cv_pb) cM cN then substn else
257
match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in
259
match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in
260
expand curenvnb pb b substn cM f1 l1 cN f2 l2
262
and expand (curenv,_ as curenvnb) pb b substn cM f1 l1 cN f2 l2 =
263
if trivial_unify curenv pb substn cM cN then substn
265
let cf1 = key_of flags f1 and cf2 = key_of flags f2 in
266
match oracle_order curenv cf1 cf2 with
267
| None -> error_cannot_unify curenv sigma (cM,cN)
269
(match expand_key curenv cf1 with
271
unirec_rec curenvnb pb b substn
272
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
274
(match expand_key curenv cf2 with
276
unirec_rec curenvnb pb b substn cM
277
(whd_betaiotazeta sigma (mkApp(c,l2)))
279
error_cannot_unify curenv sigma (cM,cN)))
281
(match expand_key curenv cf2 with
283
unirec_rec curenvnb pb b substn cM
284
(whd_betaiotazeta sigma (mkApp(c,l2)))
286
(match expand_key curenv cf1 with
288
unirec_rec curenvnb pb b substn
289
(whd_betaiotazeta sigma (mkApp(c,l1))) cN
291
error_cannot_unify curenv sigma (cM,cN)))
293
error_cannot_unify curenv sigma (cM,cN)
296
if (if occur_meta m then false else
297
if (match flags.modulo_conv_on_closed_terms with
299
is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
300
| None -> constr_cmp (conv_pb_of cv_pb) m n) then true else
301
if (not (is_ground_term (create_evar_defs sigma) m))
302
|| occur_meta_or_existential n then false else
303
if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
304
| Some (cv_id, cv_k), (dl_id, dl_k) ->
305
Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
306
| None,(dl_id, dl_k) ->
307
Idpred.is_empty dl_id && Cpred.is_empty dl_k)
308
then error_cannot_unify env sigma (m, n) else false)
312
unirec_rec (env,0) cv_pb conv_at_top subst m n
314
let unify_0 = unify_0_with_initial_metas ([],[]) true
319
let pop k = if k=0 then 0 else k-1
321
let rec unify_with_eta keptside flags env sigma k1 k2 c1 c2 =
322
(* Reason up to limited eta-expansion: ci is allowed to start with ki lam *)
323
(* Question: try whd_betadeltaiota on ci if ki>0 ? *)
324
match kind_of_term c1, kind_of_term c2 with
325
| (Lambda (na,t1,c1'), Lambda (_,t2,c2')) ->
326
let env' = push_rel_assum (na,t1) env in
327
let metas,evars = unify_0 env sigma topconv flags t1 t2 in
328
let side,status,(metas',evars') =
329
unify_with_eta keptside flags env' sigma (pop k1) (pop k2) c1' c2'
330
in (side,status,(metas@metas',evars@evars'))
331
| (Lambda (na,t,c1'),_) when k2 > 0 ->
332
let env' = push_rel_assum (na,t) env in
333
let side = left in (* expansion on the right: we keep the left side *)
334
unify_with_eta side flags env' sigma (pop k1) (k2-1)
335
c1' (mkApp (lift 1 c2,[|mkRel 1|]))
336
| (_,Lambda (na,t,c2')) when k1 > 0 ->
337
let env' = push_rel_assum (na,t) env in
338
let side = right in (* expansion on the left: we keep the right side *)
339
unify_with_eta side flags env' sigma (k1-1) (pop k2)
340
(mkApp (lift 1 c1,[|mkRel 1|])) c2'
342
(keptside,ConvUpToEta(min k1 k2),
343
unify_0 env sigma topconv flags c1 c2)
345
(* We solved problems [?n =_pb u] (i.e. [u =_(opp pb) ?n]) and [?n =_pb' u'],
346
we now compute the problem on [u =? u'] and decide which of u or u' is kept
348
Rem: the upper constraint is lost in case u <= ?n <= u' (and symmetrically
349
in the case u' <= ?n <= u)
352
let merge_instances env sigma flags st1 st2 c1 c2 =
353
match (opp_status st1, st2) with
354
| (UserGiven, ConvUpToEta n2) ->
355
unify_with_eta left flags env sigma 0 n2 c1 c2
356
| (ConvUpToEta n1, UserGiven) ->
357
unify_with_eta right flags env sigma n1 0 c1 c2
358
| (ConvUpToEta n1, ConvUpToEta n2) ->
359
let side = left (* arbitrary choice, but agrees with compatibility *) in
360
unify_with_eta side flags env sigma n1 n2 c1 c2
361
| ((IsSubType | ConvUpToEta _ | UserGiven as oppst1),
362
(IsSubType | ConvUpToEta _ | UserGiven)) ->
363
let res = unify_0 env sigma Cumul flags c2 c1 in
364
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
365
else if st2=IsSubType or st1=UserGiven then (left, st1, res)
366
else (right, st2, res)
367
| ((IsSuperType | ConvUpToEta _ | UserGiven as oppst1),
368
(IsSuperType | ConvUpToEta _ | UserGiven)) ->
369
let res = unify_0 env sigma Cumul flags c1 c2 in
370
if oppst1=st2 then (* arbitrary choice *) (left, st1, res)
371
else if st2=IsSuperType or st1=UserGiven then (left, st1, res)
372
else (right, st2, res)
373
| (IsSuperType,IsSubType) ->
374
(try (left, IsSubType, unify_0 env sigma Cumul flags c2 c1)
375
with _ -> (right, IsSubType, unify_0 env sigma Cumul flags c1 c2))
376
| (IsSubType,IsSuperType) ->
377
(try (left, IsSuperType, unify_0 env sigma Cumul flags c1 c2)
378
with _ -> (right, IsSuperType, unify_0 env sigma Cumul flags c2 c1))
383
* (1) The function [unify mc wc M N] produces two lists:
384
* (a) a list of bindings Meta->RHS
385
* (b) a list of bindings EVAR->RHS
387
* The Meta->RHS bindings cannot themselves contain
388
* meta-vars, so they get applied eagerly to the other
389
* bindings. This may or may not close off all RHSs of
390
* the EVARs. For each EVAR whose RHS is closed off,
391
* we can just apply it, and go on. For each which
392
* is not closed off, we need to do a mimick step -
393
* in general, we have something like:
395
* ?X == (c e1 e2 ... ei[Meta(k)] ... en)
397
* so we need to do a mimick step, converting ?X
400
* ?X -> (c ?z1 ... ?zn)
402
* of the proper types. Then, we can decompose the
407
* ?zi --> ei[Meta(k)]
411
* and keep on going. Whenever we find that a R.H.S.
412
* is closed, we can, as before, apply the constraint
413
* directly. Whenever we find an equation of the form:
417
* we can reverse the equation, put it into our metavar
418
* substitution, and keep going.
420
* The most efficient mimick possible is, for each
421
* Meta-var remaining in the term, to declare a
422
* new EVAR of the same type. This is supposedly
423
* determinable from the clausale form context -
424
* we look up the metavar, take its type there,
425
* and apply the metavar substitution to it, to
426
* close it off. But this might not always work,
427
* since other metavars might also need to be resolved. *)
429
let applyHead env evd n c =
430
let rec apprec n c cty evd =
434
match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
437
Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
438
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
439
| _ -> error "Apply_Head_Then"
441
apprec n c (Typing.type_of env (evars_of evd) c) evd
443
let is_mimick_head f =
444
match kind_of_term f with
445
(Const _|Var _|Rel _|Construct _|Ind _) -> true
448
let pose_all_metas_as_evars env evd t =
449
let evdref = ref evd in
450
let rec aux t = match kind_of_term t with
452
(match Evd.meta_opt_fvalue !evdref mv with
453
| Some ({rebus=c},_) -> c
455
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
456
let ty = if mvs = Evd.Metaset.empty then ty else aux ty in
457
let ev = Evarutil.e_new_evar evdref env ~src:(dummy_loc,GoalEvar) ty in
458
evdref := meta_assign mv (ev,(ConvUpToEta 0,TypeNotProcessed)) !evdref;
466
let try_to_coerce env evd c cty tycon =
467
let j = make_judge c cty in
468
let (evd',j') = inh_conv_coerce_rigid_to dummy_loc env evd j tycon in
469
let (evd',b) = Evarconv.consider_remaining_unif_problems env evd' in
471
let evd' = Evd.map_metas_fvalue (nf_evar (evars_of evd')) evd' in
474
error "Cannot solve unification constraints"
476
let w_coerce_to_type env evd c cty mvty =
477
let evd,mvty = pose_all_metas_as_evars env evd mvty in
478
let tycon = mk_tycon_type mvty in
479
try try_to_coerce env evd c cty tycon
480
with e when precatchable_exception e ->
481
(* inh_conv_coerce_rigid_to should have reasoned modulo reduction
482
but there are cases where it though it was not rigid (like in
483
fst (nat,nat)) and stops while it could have seen that it is rigid *)
484
let cty = Tacred.hnf_constr env (evars_of evd) cty in
485
try_to_coerce env evd c cty tycon
487
let w_coerce env evd mv c =
488
let cty = get_type_of_with_meta env (evars_of evd) (metas_of evd) c in
489
let mvty = Typing.meta_type evd mv in
490
w_coerce_to_type env evd c cty mvty
492
let unify_to_type env evd flags c u =
493
let sigma = evars_of evd in
494
let c = refresh_universes c in
495
let t = get_type_of_with_meta env sigma (List.map (on_snd (nf_meta evd)) (metas_of evd)) (nf_meta evd c) in
496
let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
497
let u = Tacred.hnf_constr env sigma u in
498
try unify_0 env sigma Cumul flags t u
499
with e when precatchable_exception e -> ([],[])
501
let unify_type env evd flags mv c =
502
let mvty = Typing.meta_type evd mv in
503
if occur_meta_or_existential mvty or is_arity env (evars_of evd) mvty then
504
unify_to_type env evd flags c mvty
507
(* Move metas that may need coercion at the end of the list of instances *)
509
let order_metas metas =
510
let rec order latemetas = function
511
| [] -> List.rev latemetas
512
| (_,_,(status,to_type) as meta)::metas ->
513
if to_type = CoerceToType then order (meta::latemetas) metas
514
else meta :: order latemetas metas
517
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
519
let solve_simple_evar_eqn env evd ev rhs =
520
let evd,b = solve_simple_eqn Evarconv.evar_conv_x env evd (CONV,ev,rhs) in
521
if not b then error_cannot_unify env (evars_of evd) (mkEvar ev,rhs);
522
let (evd,b) = Evarconv.consider_remaining_unif_problems env evd in
523
if not b then error "Cannot solve unification constraints";
526
(* [w_merge env sigma b metas evars] merges common instances in metas
527
or in evars, possibly generating new unification problems; if [b]
528
is true, unification of types of metas is required *)
530
let w_merge env with_types flags (metas,evars) evd =
531
let rec w_merge_rec evd metas evars eqns =
535
| ((evn,_ as ev),rhs)::evars' ->
536
if is_defined_evar evd ev then
537
let v = Evd.existential_value (evars_of evd) ev in
538
let (metas',evars'') =
539
unify_0 env (evars_of evd) topconv flags rhs v in
540
w_merge_rec evd (metas'@metas) (evars''@evars') eqns
542
let rhs' = subst_meta_instances metas rhs in
543
match kind_of_term rhs with
544
| App (f,cl) when is_mimick_head f & occur_meta rhs' ->
545
if occur_evar evn rhs' then
546
error_occur_check env (evars_of evd) evn rhs';
547
let evd' = mimick_evar evd flags f (Array.length cl) evn in
548
w_merge_rec evd' metas evars eqns
550
w_merge_rec (solve_simple_evar_eqn env evd ev rhs')
557
| (mv,c,(status,to_type))::metas ->
558
let ((evd,c),(metas'',evars'')),eqns =
559
if with_types & to_type <> TypeProcessed then
560
if to_type = CoerceToType then
561
(* Some coercion may have to be inserted *)
562
(w_coerce env evd mv c,([],[])),[]
564
(* No coercion needed: delay the unification of types *)
565
((evd,c),([],[])),(mv,c)::eqns
567
((evd,c),([],[])),eqns in
568
if meta_defined evd mv then
569
let {rebus=c'},(status',_) = meta_fvalue evd mv in
570
let (take_left,st,(metas',evars')) =
571
merge_instances env (evars_of evd) flags status' status c' c
574
if take_left then evd
575
else meta_reassign mv (c,(st,TypeProcessed)) evd
577
w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
579
let evd' = meta_assign mv (c,(status,TypeProcessed)) evd in
580
w_merge_rec evd' (metas@metas'') evars'' eqns
583
(* Process type eqns *)
586
let (metas,evars) = unify_type env evd flags mv c in
587
w_merge_rec evd metas evars eqns
590
and mimick_evar evd flags hdc nargs sp =
591
let ev = Evd.find (evars_of evd) sp in
592
let sp_env = Global.env_of_context ev.evar_hyps in
593
let (evd', c) = applyHead sp_env evd nargs hdc in
595
unify_0 sp_env (evars_of evd') Cumul flags
596
(Retyping.get_type_of_with_meta sp_env (evars_of evd') (metas_of evd') c) ev.evar_concl in
597
let evd'' = w_merge_rec evd' mc ec [] in
598
if (evars_of evd') == (evars_of evd'')
599
then Evd.evar_define sp c evd''
600
else Evd.evar_define sp (Evarutil.nf_evar (evars_of evd'') c) evd'' in
602
(* merge constraints *)
603
w_merge_rec evd (order_metas metas) evars []
605
let w_unify_meta_types env ?(flags=default_unify_flags) evd =
606
let metas,evd = retract_coercible_metas evd in
607
w_merge env true flags (metas,[]) evd
609
(* [w_unify env evd M N]
610
performs a unification of M and N, generating a bunch of
611
unification constraints in the process. These constraints
612
are processed, one-by-one - they may either generate new
613
bindings, or, if there is already a binding, new unifications,
614
which themselves generate new constraints. This continues
615
until we get failure, or we run out of constraints.
616
[clenv_typed_unify M N clenv] expects in addition that expected
617
types of metavars are unifiable with the types of their instances *)
619
let check_types env evd flags subst m n =
620
let sigma = evars_of evd in
621
if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
622
unify_0_with_initial_metas subst true env (evars_of evd) topconv
624
(Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
625
(Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
629
let w_unify_core_0 env with_types cv_pb flags m n evd =
630
let (mc1,evd') = retract_coercible_metas evd in
631
let subst1 = check_types env evd flags (mc1,[]) m n in
633
unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
635
w_merge env with_types flags subst2 evd'
637
let w_unify_0 env = w_unify_core_0 env false
638
let w_typed_unify env = w_unify_core_0 env true
641
(* takes a substitution s, an open term op and a closed term cl
642
try to find a subterm of cl which matches op, if op is just a Meta
643
FAIL because we cannot find a binding *)
646
let n = Array.length a in
648
if i = n then error "iter_fail"
651
with ex when precatchable_exception ex -> ffail (i+1)
654
(* Tries to find an instance of term [cl] in term [op].
655
Unifies [cl] to every subterm of [op] until it finds a match.
656
Fails if no match is found *)
657
let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
658
let rec matchrec cl =
659
let cl = strip_outer_cast cl in
662
then w_unify_0 env topconv flags op cl evd,cl
664
with ex when precatchable_exception ex ->
665
(match kind_of_term cl with
667
let n = Array.length args in
669
let c1 = mkApp (f,Array.sub args 0 (n-1)) in
670
let c2 = args.(n-1) in
673
with ex when precatchable_exception ex ->
675
| Case(_,_,c,lf) -> (* does not search in the predicate *)
678
with ex when precatchable_exception ex ->
679
iter_fail matchrec lf)
680
| LetIn(_,c1,_,c2) ->
683
with ex when precatchable_exception ex ->
686
| Fix(_,(_,types,terms)) ->
688
iter_fail matchrec types
689
with ex when precatchable_exception ex ->
690
iter_fail matchrec terms)
692
| CoFix(_,(_,types,terms)) ->
694
iter_fail matchrec types
695
with ex when precatchable_exception ex ->
696
iter_fail matchrec terms)
701
with ex when precatchable_exception ex ->
706
with ex when precatchable_exception ex ->
708
| _ -> error "Match_subterm"))
711
with ex when precatchable_exception ex ->
712
raise (PretypeError (env,NoOccurrenceFound (op, None)))
714
let w_unify_to_subterm_list env flags allow_K oplist t evd =
718
if allow_K then (evd,op::l)
719
else error "Match_subterm"
720
else if occur_meta_or_existential op then
723
(* This is up to delta for subterms w/o metas ... *)
724
w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
725
with PretypeError (env,NoOccurrenceFound _) when allow_K -> (evd,op)
728
else if allow_K or dependent op t then
731
(* This is not up to delta ... *)
732
raise (PretypeError (env,NoOccurrenceFound (op, None))))
736
let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
737
(* Remove delta when looking for a subterm *)
738
let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
740
w_unify_to_subterm_list env flags allow_K oplist typ evd in
741
let typp = Typing.meta_type evd' p in
742
let pred = abstract_list_all env evd' typp typ cllist in
743
w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
745
let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
746
let c1, oplist1 = whd_stack (evars_of evd) ty1 in
747
let c2, oplist2 = whd_stack (evars_of evd) ty2 in
748
match kind_of_term c1, kind_of_term c2 with
750
(* Find the predicate *)
752
secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in
753
(* Resume first order unification *)
754
w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
756
(* Find the predicate *)
758
secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in
759
(* Resume first order unification *)
760
w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
761
| _ -> error "w_unify2"
763
(* The unique unification algorithm works like this: If the pattern is
764
flexible, and the goal has a lambda-abstraction at the head, then
765
we do a first-order unification.
767
If the pattern is not flexible, then we do a first-order
770
If the pattern is flexible, and the goal doesn't have a
771
lambda-abstraction head, then we second-order unification. *)
773
(* We decide here if first-order or second-order unif is used for Apply *)
774
(* We apply a term of type (ai:Ai)C and try to solve a goal C' *)
775
(* The type C is in clenv.templtyp.rebus with a lot of Meta to solve *)
777
(* 3-4-99 [HH] New fo/so choice heuristic :
778
In case we have to unify (Meta(1) args) with ([x:A]t args')
779
we first try second-order unification and if it fails first-order.
780
Before, second-order was used if the type of Meta(1) and [x:A]t was
781
convertible and first-order otherwise. But if failed if e.g. the type of
782
Meta(1) had meta-variables in it. *)
783
let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
784
let cv_pb = of_conv_pb cv_pb in
785
let hd1,l1 = whd_stack (evars_of evd) ty1 in
786
let hd2,l2 = whd_stack (evars_of evd) ty2 in
787
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
789
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
790
when List.length l1 = List.length l2 ->
792
w_typed_unify env cv_pb flags ty1 ty2 evd
793
with ex when precatchable_exception ex ->
795
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
796
with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
798
(* Second order case *)
799
| (Meta _, true, _, _ | _, _, Meta _, true) ->
801
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
802
with PretypeError (env,NoOccurrenceFound _) as e -> raise e
803
| ex when precatchable_exception ex ->
805
w_typed_unify env cv_pb flags ty1 ty2 evd
806
with ex' when precatchable_exception ex' ->
809
(* General case: try first order *)
810
| _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
added
removed
pretyping/unification.ml
