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: evarutil.ml 12107 2009-04-25 19:58:24Z herbelin $ *)
26
(* Expanding existential variables (pretyping.ml) *)
27
(* 1- whd_ise fails if an existential is undefined *)
29
exception Uninstantiated_evar of existential_key
31
let rec whd_ise sigma c =
32
match kind_of_term c with
33
| Evar (evk,args as ev) when Evd.mem sigma evk ->
34
if Evd.is_defined sigma evk then
35
whd_ise sigma (existential_value sigma ev)
36
else raise (Uninstantiated_evar evk)
40
(* Expand evars, possibly in the head of an application *)
41
let whd_castappevar_stack sigma c =
42
let rec whrec (c, l as s) =
43
match kind_of_term c with
44
| Evar (evk,args as ev) when Evd.mem sigma evk & Evd.is_defined sigma evk
45
-> whrec (existential_value sigma ev, l)
46
| Cast (c,_,_) -> whrec (c, l)
47
| App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
52
let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c)
54
let nf_evar = Pretype_errors.nf_evar
55
let j_nf_evar = Pretype_errors.j_nf_evar
56
let jl_nf_evar = Pretype_errors.jl_nf_evar
57
let jv_nf_evar = Pretype_errors.jv_nf_evar
58
let tj_nf_evar = Pretype_errors.tj_nf_evar
60
let nf_named_context_evar sigma ctx =
61
Sign.map_named_context (Reductionops.nf_evar sigma) ctx
63
let nf_rel_context_evar sigma ctx =
64
Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
66
let nf_env_evar sigma env =
67
let nc' = nf_named_context_evar sigma (Environ.named_context env) in
68
let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
69
push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
71
let nf_evar_info evc info =
73
evar_concl = Reductionops.nf_evar evc info.evar_concl;
74
evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps}
76
let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
79
let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars (Evd.evars_of evd)) evd
81
let nf_isevar evd = nf_evar (Evd.evars_of evd)
82
let j_nf_isevar evd = j_nf_evar (Evd.evars_of evd)
83
let jl_nf_isevar evd = jl_nf_evar (Evd.evars_of evd)
84
let jv_nf_isevar evd = jv_nf_evar (Evd.evars_of evd)
85
let tj_nf_isevar evd = tj_nf_evar (Evd.evars_of evd)
87
(**********************)
88
(* Creating new metas *)
89
(**********************)
91
(* Generator of metavariables *)
93
let meta_ctr = ref 0 in
94
fun () -> incr meta_ctr; !meta_ctr
96
let mk_new_meta () = mkMeta(new_meta())
98
let collect_evars emap c =
99
let rec collrec acc c =
100
match kind_of_term c with
102
if Evd.mem emap evk & not (Evd.is_defined emap evk) then evk::acc
103
else (* No recursion on the evar instantiation *) acc
105
fold_constr collrec acc c in
106
list_uniquize (collrec [] c)
108
let push_dependent_evars sigma emap =
109
Evd.fold (fun ev {evar_concl = ccl} (sigma',emap') ->
111
(fun (sigma',emap') ev ->
112
(Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
113
(sigma',emap') (collect_evars emap' ccl))
116
(* replaces a mapping of existentials into a mapping of metas.
117
Problem if an evar appears in the type of another one (pops anomaly) *)
118
let evars_to_metas sigma (emap, c) =
119
let emap = nf_evars emap in
120
let sigma',emap' = push_dependent_evars sigma emap in
121
let change_exist evar =
122
let ty = nf_betaiota emap (existential_type emap evar) in
123
let n = new_meta() in
124
mkCast (mkMeta n, DEFAULTcast, ty) in
126
match kind_of_term c with
127
| Evar (evk,_ as ev) when Evd.mem emap' evk -> change_exist ev
128
| _ -> map_constr replace c in
131
(* The list of non-instantiated existential declarations *)
133
let non_instantiated sigma =
134
let listev = to_list sigma in
137
if evi.evar_body = Evar_empty then
138
((ev,nf_evar_info sigma evi)::l) else l)
141
(**********************)
142
(* Creating new evars *)
143
(**********************)
145
(* Generator of existential names *)
146
let new_untyped_evar =
147
let evar_ctr = ref 0 in
148
fun () -> incr evar_ctr; existential_of_int !evar_ctr
150
(*------------------------------------*
151
* functional operations on evar sets *
152
*------------------------------------*)
154
let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) ?filter instance =
158
| Some filter -> snd (list_filter2 (fun b c -> b) (filter,instance)) in
160
(let ctxt = named_context_of_val sign in
161
list_distinct (ids_of_named_context ctxt));
162
let newevk = new_untyped_evar() in
163
let evd = evar_declare sign newevk typ ~src:src ?filter evd in
164
(evd,mkEvar (newevk,Array.of_list instance))
166
(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
167
* [make_projectable_subst ev args] builds the substitution [Gamma:=args].
168
* If a variable and an alias of it are bound to the same instance, we skip
169
* the alias (we just use eq_constr -- instead of conv --, since anyway,
170
* only instances that are variables -- or evars -- are later considered;
171
* morever, we can bet that similar instances came at some time from
172
* the very same substitution. The removal of aliased duplicates is
173
* useful to ensure the uniqueness of a projection.
176
let make_projectable_subst sigma evi args =
177
let sign = evar_filtered_context evi in
178
let rec alias_of_var id =
179
match pi2 (Sign.lookup_named id sign) with
180
| Some t when isVar t -> alias_of_var (destVar t)
183
(fun (id,b,c) (args,l) ->
185
| Some c, a::rest when
186
isVar c & (try eq_constr a (snd (List.assoc (destVar c) l)) with Not_found -> false) -> (rest,l)
187
| _, a::rest -> (rest, (id, (alias_of_var id,whd_evar sigma a))::l)
188
| _ -> anomaly "Instance does not match its signature")
189
sign (List.rev (Array.to_list args),[]))
191
let make_pure_subst evi args =
193
(fun (id,b,c) (args,l) ->
195
| a::rest -> (rest, (id,a)::l)
196
| _ -> anomaly "Instance does not match its signature")
197
(evar_filtered_context evi) (List.rev (Array.to_list args),[]))
199
(* [push_rel_context_to_named_context] builds the defining context and the
200
* initial instance of an evar. If the evar is to be used in context
202
* Gamma = a1 ... an xp ... x1
203
* \- named part -/ \- de Bruijn part -/
205
* then the x1...xp are turned into variables so that the evar is declared in
208
* a1 ... an xp ... x1
209
* \----------- named part ------------/
211
* but used applied to the initial instance "a1 ... an Rel(p) ... Rel(1)"
212
* so that ev[a1:=a1 ... an:=an xp:=Rel(p) ... x1:=Rel(1)] is correctly typed
215
* Remark 1: The instance is reverted in practice (i.e. Rel(1) comes first)
216
* Remark 2: If some of the ai or xj are definitions, we keep them in the
217
* instance. This is necessary so that no unfolding of local definitions
218
* happens when inferring implicit arguments (consider e.g. the problem
219
* "x:nat; x':=x; f:forall x, x=x -> Prop |- f _ (refl_equal x')"
220
* we want the hole to be instantiated by x', not by x (which would have the
221
* case in [invert_instance] if x' had disappear of the instance).
222
* Note that at any time, if, in some context env, the instance of
223
* declaration x:A is t and the instance of definition x':=phi(x) is u, then
224
* we have the property that u and phi(t) are convertible in env.
227
let push_rel_context_to_named_context env typ =
228
(* compute the instances relative to the named context and rel_context *)
229
let ids = List.map pi1 (named_context env) in
230
let inst_vars = List.map mkVar ids in
231
let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
232
(* move the rel context to a named context and extend the named instance *)
233
(* with vars of the rel context *)
234
(* We do keep the instances corresponding to local definition (see above) *)
235
let (subst, _, env) =
236
Sign.fold_rel_context
237
(fun (na,c,t) (subst, avoid, env) ->
238
let id = next_name_away na avoid in
239
let d = (id,Option.map (substl subst) c,substl subst t) in
240
(mkVar id :: subst, id::avoid, push_named d env))
241
(rel_context env) ~init:([], ids, env) in
242
(named_context_val env, substl subst typ, inst_rels@inst_vars)
244
(* [new_evar] declares a new existential in an env env with type typ *)
245
(* Converting the env into the sign of the evar to define *)
247
let new_evar evd env ?(src=(dummy_loc,InternalHole)) ?filter typ =
248
let sign,typ',instance = push_rel_context_to_named_context env typ in
249
new_evar_instance sign evd typ' ~src:src ?filter instance
251
(* The same using side-effect *)
252
let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ty =
253
let (evd',ev) = new_evar !evdref env ~src:src ?filter ty in
257
(*------------------------------------*
258
* operations on the evar constraints *
259
*------------------------------------*)
261
let is_pattern inst =
262
array_for_all (fun a -> isRel a || isVar a) inst &&
265
(* Pb: defined Rels and Vars should not be considered as a pattern... *)
267
let is_pattern inst =
268
let rec is_hopat l = function
271
(isRel t or isVar t) && not (List.mem t l) && is_hopat (t::l) tl in
272
is_hopat [] (Array.to_list inst)
275
let evar_well_typed_body evd ev evi body =
277
let env = evar_unfiltered_env evi in
278
let ty = evi.evar_concl in
279
Typing.check env (evars_of evd) body ty;
283
(str "Ill-typed evar instantiation: " ++ fnl() ++
284
pr_evar_defs evd ++ fnl() ++
285
str "----> " ++ int ev ++ str " := " ++
289
(* We have x1..xq |- ?e1 and had to solve something like
290
* Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
291
* ?e2[v1..vn], hence flexible. We had to go through k binders and now
292
* virtually have x1..xq, y1..yk | ?e1' and the equation
293
* Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
294
* What we do is to formally introduce ?e1' in context x1..xq, Γ, y1..yk,
295
* but forbidding it to use the variables of Γ (otherwise said,
296
* Γ is here only for ensuring the correct typing of ?e1').
298
* In fact, we optimize a little and try to compute a maximum
299
* common subpart of x1..xq and Γ. This is done by detecting the
300
* longest subcontext x1..xp such that Γ = x1'..xp' z1..zm and
303
* At the end, we return ?e1'[x1..xn z1..zm y1..yk] so that ?e1 can be
304
* instantiated by (...\y1 ... \yk ... ?e1[x1..xn z1..zm y1..yk]) and the
305
* new problem is Σ; Γ, y1..yk |- ?e1'[u1..un z1..zm y1..yk] = c,
306
* making the z1..zm unavailable.
308
* This is what [extend_evar Γ evd k (?e1[u1..uq]) c] does.
311
let shrink_context env subst ty =
312
let rev_named_sign = List.rev (named_context env) in
313
let rel_sign = rel_context env in
314
(* We merge the contexts (optimization) *)
315
let rec shrink_rel i subst rel_subst rev_rel_sign =
316
match subst,rev_rel_sign with
317
| (id,c)::subst,_::rev_rel_sign when c = mkRel i ->
318
shrink_rel (i-1) subst (mkVar id::rel_subst) rev_rel_sign
320
substl_rel_context rel_subst (List.rev rev_rel_sign),
323
let rec shrink_named subst named_subst rev_named_sign =
324
match subst,rev_named_sign with
325
| (id,c)::subst,(id',b',t')::rev_named_sign when c = mkVar id' ->
326
shrink_named subst ((id',mkVar id)::named_subst) rev_named_sign
328
let nrel = List.length rel_sign in
329
let rel_sign, ty = shrink_rel nrel subst [] (List.rev rel_sign) in
330
[], map_rel_context (replace_vars named_subst) rel_sign,
331
replace_vars named_subst ty
333
map_named_context (replace_vars named_subst) (List.rev rev_named_sign),
336
shrink_named subst [] rev_named_sign
338
let extend_evar env evdref k (evk1,args1) c =
339
let ty = get_type_of env (evars_of !evdref) c in
340
let overwrite_first v1 v2 =
341
let v = Array.copy v1 in
342
let n = Array.length v - Array.length v2 in
343
for i = 0 to Array.length v2 - 1 do v.(n+i) <- v2.(i) done;
345
let evi1 = Evd.find (evars_of !evdref) evk1 in
346
let named_sign',rel_sign',ty =
347
if k = 0 then [], [], ty
348
else shrink_context env (List.rev (make_pure_subst evi1 args1)) ty in
350
List.fold_right push_rel rel_sign'
351
(List.fold_right push_named named_sign' (evar_unfiltered_env evi1)) in
352
let nb_to_hide = rel_context_length rel_sign' - k in
353
let rel_filter = list_map_i (fun i _ -> i > nb_to_hide) 1 rel_sign' in
354
let named_filter1 = List.map (fun _ -> true) (evar_context evi1) in
355
let named_filter2 = List.map (fun _ -> false) named_sign' in
356
let filter = rel_filter@named_filter2@named_filter1 in
357
let evar1' = e_new_evar evdref extenv ~filter:filter ty in
358
let evk1',args1'_in_env = destEvar evar1' in
359
let args1'_in_extenv = Array.map (lift k) (overwrite_first args1'_in_env args1) in
360
(evar1',(evk1',args1'_in_extenv))
362
let subfilter p filter l =
364
List.fold_left (fun (filter,l,newl) b ->
366
let a,l' = match l with a::args -> a,args | _ -> assert false in
367
if p a then (true::filter,l',a::newl) else (false::filter,l',newl)
368
else (false::filter,l,newl))
370
(List.rev filter,List.rev l)
372
let restrict_upon_filter evd evi evk p args =
373
let filter = evar_filter evi in
374
let newfilter,newargs = subfilter p filter args in
375
if newfilter <> filter then
376
let (evd,newev) = new_evar evd (evar_unfiltered_env evi) ~src:(evar_source evk evd)
377
~filter:newfilter evi.evar_concl in
378
let evd = Evd.evar_define evk newev evd in
379
evd,fst (destEvar newev),newargs
384
let rec collrec acc c =
385
match kind_of_term c with
386
| Var id -> list_add_set id acc
387
| _ -> fold_constr collrec acc c
391
type clear_dependency_error =
392
| OccurHypInSimpleClause of identifier option
393
| EvarTypingBreak of existential
395
exception ClearDependencyError of identifier * clear_dependency_error
397
let rec check_and_clear_in_constr evdref err ids c =
398
(* returns a new constr where all the evars have been 'cleaned'
399
(ie the hypotheses ids have been removed from the contexts of
402
if List.mem id' ids then
403
raise (ClearDependencyError (id',err))
405
match kind_of_term c with
409
| ( Const _ | Ind _ | Construct _ ) ->
410
let vars = Environ.vars_of_global (Global.env()) c in
411
List.iter check vars; c
413
| Evar (evk,l as ev) ->
414
if Evd.is_defined_evar !evdref ev then
415
(* If evk is already defined we replace it by its definition *)
416
let nc = whd_evar (evars_of !evdref) c in
417
(check_and_clear_in_constr evdref err ids nc)
419
(* We check for dependencies to elements of ids in the
420
evar_info corresponding to e and in the instance of
421
arguments. Concurrently, we build a new evar
422
corresponding to e where hypotheses of ids have been
424
let evi = Evd.find (evars_of !evdref) evk in
425
let ctxt = Evd.evar_filtered_context evi in
426
let (nhyps,nargs,rids) =
428
(fun (rid,ob,c as h) a (hy,ar,ri) ->
429
(* Check if some id to clear occurs in the instance
430
a of rid in ev and remember the dependency *)
432
List.filter (fun id -> List.mem id ids) (collect_vars a)
434
| id :: _ -> (hy,ar,(rid,id)::ri)
436
(* Check if some rid to clear in the context of ev
437
has dependencies in another hyp of the context of ev
438
and transitively remember the dependency *)
439
match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
440
| (_,id') :: _ -> (hy,ar,(rid,id')::ri)
442
(* No dependency at all, we can keep this ev's context hyp *)
444
ctxt (Array.to_list l) ([],[],[]) in
445
(* Check if some rid to clear in the context of ev has dependencies
446
in the type of ev and adjust the source of the dependency *)
448
try check_and_clear_in_constr evdref (EvarTypingBreak ev)
449
(List.map fst rids) (evar_concl evi)
450
with ClearDependencyError (rid,err) ->
451
raise (ClearDependencyError (List.assoc rid rids,err)) in
453
let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
454
let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
455
evdref := Evd.evar_define evk ev' !evdref;
456
let (evk',_) = destEvar ev' in
457
mkEvar(evk', Array.of_list nargs)
459
| _ -> map_constr (check_and_clear_in_constr evdref err ids) c
461
let clear_hyps_in_evi evdref hyps concl ids =
462
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
463
hypothesis does not depend on a element of ids, and erases ids in
464
the contexts of the evars occuring in evi *)
466
check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
468
let check_context (id,ob,c) =
469
let err = OccurHypInSimpleClause (Some id) in
470
(id, Option.map (check_and_clear_in_constr evdref err ids) ob,
471
check_and_clear_in_constr evdref err ids c)
477
if (List.for_all (fun e -> not (Idset.mem e d)) ids) then
478
(* v does depend on any of ids, it's ok *)
481
(* v depends on one of the cleared hyps: we forget the computed value *)
484
remove_hyps ids check_context check_value hyps
489
(* Expand rels and vars that are bound to other rels or vars so that
490
dependencies in variables are canonically associated to the most ancient
491
variable in its family of aliased variables *)
493
let expand_var_once env x = match kind_of_term x with
495
begin match pi2 (lookup_rel n env) with
496
| Some t when isRel t or isVar t -> lift n t
497
| _ -> raise Not_found
500
begin match pi2 (lookup_named id env) with
501
| Some t when isVar t -> t
502
| _ -> raise Not_found
507
let rec expand_var_at_least_once env x =
508
let t = expand_var_once env x in
509
try expand_var_at_least_once env t
512
let expand_var env x =
513
try expand_var_at_least_once env x with Not_found -> x
515
let expand_var_opt env x =
516
try Some (expand_var_at_least_once env x) with Not_found -> None
518
let rec expand_vars_in_term env t = match kind_of_term t with
519
| Rel _ | Var _ -> expand_var env t
520
| _ -> map_constr_with_full_binders push_rel expand_vars_in_term env t
522
let rec expansions_of_var env x =
524
let t = expand_var_once env x in
525
t :: expansions_of_var env t
529
(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
530
* that project on [y]. It is able to find solutions to the following
531
* two kinds of problems:
533
* - ?n[...;x:=y;...] = y
534
* - ?n[...;x:=?m[args];...] = y with ?m[args] = y recursively solvable
536
* (see test-suite/success/Fixpoint.v for an example of application of
537
* the second kind of problem).
539
* The seek for [y] is up to variable aliasing. In case of solutions that
540
* differ only up to aliasing, the binding that requires the less
541
* steps of alias reduction is kept. At the end, only one solution up
542
* to aliasing is kept.
544
* [find_projectable_vars] also unifies against evars that themselves mention
545
* [y] and recursively.
547
* In short, the following situations give the following solutions:
549
* problem evar ctxt soluce remark
550
* z1; z2:=z1 |- ?ev[z1;z2] = z1 y1:A; y2:=y1 y1 \ thanks to defs kept in
551
* z1; z2:=z1 |- ?ev[z1;z2] = z2 y1:A; y2:=y1 y2 / subst and preferring =
552
* z1; z2:=z1 |- ?ev[z1] = z2 y1:A y1 thanks to expand_var
553
* z1; z2:=z1 |- ?ev[z2] = z1 y1:A y1 thanks to expand_var
554
* z3 |- ?ev[z3;z3] = z3 y1:A; y2:=y1 y2 see make_projectable_subst
556
* Remark: [find_projectable_vars] assumes that identical instances of
557
* variables in the same set of aliased variables are already removed (see
558
* [make_projectable_subst])
563
type evar_projection =
565
| ProjectEvar of existential * evar_info * identifier * evar_projection
567
let rec find_projectable_vars with_evars env sigma y subst =
568
let is_projectable (id,(idc,y')) =
569
let y' = whd_evar sigma y' in
570
if y = y' or expand_var env y = expand_var env y'
571
then (idc,(y'=y,(id,ProjectVar)))
572
else if with_evars & isEvar y' then
573
let (evk,argsv as t) = destEvar y' in
574
let evi = Evd.find sigma evk in
575
let subst = make_projectable_subst sigma evi argsv in
576
let l = find_projectable_vars with_evars env sigma y subst in
578
| [id',p] -> (idc,(true,(id,ProjectEvar (t,evi,id',p))))
581
let l = map_succeed is_projectable subst in
582
let l = list_partition_by (fun (idc,_) (idc',_) -> idc = idc') l in
583
let l = List.map (List.map snd) l in
584
List.map (fun l -> try List.assoc true l with Not_found -> snd (List.hd l)) l
586
(* [filter_solution] checks if one and only one possible projection exists
587
* among a set of solutions to a projection problem *)
589
let filter_solution = function
590
| [] -> raise Not_found
591
| (id,p)::_::_ -> raise NotUnique
592
| [id,p] -> (mkVar id, p)
594
let project_with_effects env sigma effects t subst =
595
let c, p = filter_solution (find_projectable_vars false env sigma t subst) in
596
effects := p :: !effects;
599
(* In case the solution to a projection problem requires the instantiation of
600
* subsidiary evars, [do_projection_effects] performs them; it
601
* also try to instantiate the type of those subsidiary evars if their
602
* type is an evar too.
604
* Note: typing creates new evar problems, which induces a recursive dependency
605
* with [evar_define]. To avoid a too large set of recursive functions, we
606
* pass [evar_define] to [do_projection_effects] as a parameter.
609
let rec do_projection_effects define_fun env ty evd = function
611
| ProjectEvar ((evk,argsv),evi,id,p) ->
612
let evd = Evd.evar_define evk (mkVar id) evd in
613
(* TODO: simplify constraints involving evk *)
614
let evd = do_projection_effects define_fun env ty evd p in
615
let ty = whd_betadeltaiota env (evars_of evd) (Lazy.force ty) in
616
if not (isSort ty) then
617
(* Don't try to instantiate if a sort because if evar_concl is an
618
evar it may commit to a univ level which is not the right
619
one (however, regarding coercions, because t is obtained by
620
unif, we know that no coercion can be inserted) *)
621
let subst = make_pure_subst evi argsv in
622
let ty' = replace_vars subst evi.evar_concl in
623
let ty' = whd_evar (evars_of evd) ty' in
624
if isEvar ty' then define_fun env (destEvar ty') ty evd else evd
628
(* Assuming Σ; Γ, y1..yk |- c, [invert_subst Γ k Σ [x1:=u1;...;xn:=un] c]
629
* tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
630
* The strategy is to imitate the structure of c and then to invert
631
* the variables of c (i.e. rels or vars of Γ) using the algorithm
632
* implemented by project_with_effects/find_projectable_vars.
633
* It returns either a unique solution or says whether 0 or more than
634
* 1 solutions is found.
636
* Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
637
* Postcondition: if φ(x1..xn) is returned then
638
* Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
640
* The effects correspond to evars instantiated while trying to project.
642
* [invert_subst] is used on instances of evars. Since the evars are flexible,
643
* these instances are potentially erasable. This is why we don't investigate
644
* whether evars in the instances of evars are unifiable, to the contrary of
645
* [invert_definition].
648
type projectibility_kind =
650
| UniqueProjection of constr * evar_projection list
652
type projectibility_status =
654
| Invertible of projectibility_kind
656
let invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders =
657
let effects = ref [] in
659
let t = whd_evar sigma t in
660
match kind_of_term t with
662
project_with_effects env sigma effects (mkRel (i-k)) subst_in_env
664
project_with_effects env sigma effects t subst_in_env
666
map_constr_with_binders succ aux k t in
668
let c = aux k c_in_env_extended_with_k_binders in
669
Invertible (UniqueProjection (c,!effects))
671
| Not_found -> CannotInvert
672
| NotUnique -> Invertible NoUniqueProjection
674
let invert_arg env k sigma (evk,args_in_env) c_in_env_extended_with_k_binders =
675
let subst_in_env = make_projectable_subst sigma (Evd.find sigma evk) args_in_env in
676
let res = invert_arg_from_subst env k sigma subst_in_env c_in_env_extended_with_k_binders in
678
| Invertible (UniqueProjection (c,_)) when occur_evar evk c -> CannotInvert
682
let effective_projections =
683
map_succeed (function Invertible c -> c | _ -> failwith"")
685
let instance_of_projection f env t evd projs =
686
let ty = lazy (Retyping.get_type_of env (evars_of evd) t) in
688
| NoUniqueProjection -> raise NotUnique
689
| UniqueProjection (c,effects) ->
690
(List.fold_left (do_projection_effects f env ty) evd effects, c)
692
let filter_of_projection = function CannotInvert -> false | _ -> true
694
let filter_along f projs v =
695
let l = Array.to_list v in
696
let _,l = list_filter2 (fun b c -> f b) (projs,l) in
699
(* Redefines an evar with a smaller context (i.e. it may depend on less
700
* variables) such that c becomes closed.
701
* Example: in "fun (x:?1) (y:list ?2[x]) => x = y :> ?3[x,y] /\ x = nil bool"
702
* ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
703
* ?1 <-- list ?2 pb: ?2 may depend on x, but not ?1.
704
* What we do is that ?2 is defined by a new evar ?4 whose context will be
705
* a prefix of ?2's env, included in ?1's env.
707
* If "hyps |- ?e : T" and "filter" selects a subset hyps' of hyps then
708
* [do_restrict_hyps evd ?e filter] sets ?e:=?e'[hyps'] and returns ?e'
709
* such that "hyps' |- ?e : T"
712
let do_restrict_hyps_virtual evd evk filter =
713
(* What to do with dependencies?
714
Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
715
- If y is in a non-erasable position in C(x,y) (i.e. it is not below an
716
occurrence of x in the hnf of C), then z should be removed too.
717
- If y is in a non-erasable position in T(x,y,z) then the problem is
719
Computing whether y is erasable or not may be costly and the
720
interest for this early detection in practice is not obvious. We let
721
it for future work. In any case, thanks to the use of filters, the whole
722
(unrestricted) context remains consistent. *)
723
let evi = Evd.find (evars_of evd) evk in
724
let env = evar_unfiltered_env evi in
725
let oldfilter = evar_filter evi in
726
let filter,_ = List.fold_right (fun oldb (l,filter) ->
727
if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
728
oldfilter ([],List.rev filter) in
729
new_evar evd env ~src:(evar_source evk evd)
730
~filter:filter evi.evar_concl
732
let do_restrict_hyps evd evk projs =
733
let filter = List.map filter_of_projection projs in
734
if List.for_all (fun x -> x) filter then
737
let evd,nc = do_restrict_hyps_virtual evd evk filter in
738
let evd = Evd.evar_define evk nc evd in
739
let evk',_ = destEvar nc in
742
(* [postpone_evar_term] postpones an equation of the form ?e[σ] = c *)
744
let postpone_evar_term env evd (evk,argsv) rhs =
745
let rhs = expand_vars_in_term env rhs in
746
let evi = Evd.find (evars_of evd) evk in
748
restrict_upon_filter evd evi evk
749
(* Keep only variables that depends in rhs *)
750
(* This is not safe: is the variable is a local def, its body *)
751
(* may contain references to variables that are removed, leading to *)
752
(* a ill-formed context. We would actually need a notion of filter *)
753
(* that says that the body is hidden. Note that expand_vars_in_term *)
754
(* expands only rels and vars aliases, not rels or vars bound to an *)
755
(* arbitrary complex term *)
756
(fun a -> not (isRel a || isVar a) || dependent a rhs)
757
(Array.to_list argsv) in
758
let args = Array.of_list args in
759
let pb = (Reduction.CONV,env,mkEvar(evk,args),rhs) in
760
Evd.add_conv_pb pb evd
762
(* [postpone_evar_evar] postpones an equation of the form ?e1[σ1] = ?e2[σ2] *)
764
let postpone_evar_evar env evd projs1 (evk1,args1) projs2 (evk2,args2) =
765
(* Leave an equation between (restrictions of) ev1 andv ev2 *)
766
let args1' = filter_along filter_of_projection projs1 args1 in
767
let evd,evk1' = do_restrict_hyps evd evk1 projs1 in
768
let args2' = filter_along filter_of_projection projs2 args2 in
769
let evd,evk2' = do_restrict_hyps evd evk2 projs2 in
770
let pb = (Reduction.CONV,env,mkEvar(evk1',args1'),mkEvar (evk2',args2')) in
773
(* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
774
* to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
775
* - if there are at most one φj for each vj s.t. vj = φj(u1..un),
776
* we first restrict ?2 to the subset v_k1..v_kq of the vj that are
777
* inversible and we set ?1[x1..xn] := ?2[φk1(x1..xn)..φkp(x1..xn)]
778
* - symmetrically if there are at most one ψj for each uj s.t.
780
* - otherwise, each position i s.t. ui does not occur in v1..vp has to
781
* be restricted and similarly for the vi, and we leave the equation
782
* as an open equation (performed by [postpone_evar])
784
* Warning: the notion of unique φj is relative to some given class
785
* of unification problems
787
* Note: argument f is the function used to instantiate evars.
790
exception CannotProject of projectibility_status list
792
let solve_evar_evar_l2r f env evd (evk1,args1) (evk2,_ as ev2) =
793
let proj1 = array_map_to_list (invert_arg env 0 (evars_of evd) ev2) args1 in
795
(* Instantiate ev2 with (a restriction of) ev1 if uniquely projectable *)
796
let proj1' = effective_projections proj1 in
798
list_fold_map (instance_of_projection f env (mkEvar ev2)) evd proj1' in
799
let evd,evk1' = do_restrict_hyps evd evk1 proj1 in
800
Evd.evar_define evk2 (mkEvar(evk1',Array.of_list args1')) evd
802
raise (CannotProject proj1)
804
let solve_evar_evar f env evd ev1 ev2 =
805
try solve_evar_evar_l2r f env evd ev1 ev2
806
with CannotProject projs1 ->
807
try solve_evar_evar_l2r f env evd ev2 ev1
808
with CannotProject projs2 ->
809
postpone_evar_evar env evd projs1 ev1 projs2 ev2
811
let expand_rhs env sigma subst rhs =
812
let d = (named_hd env rhs Anonymous,Some rhs,get_type_of env sigma rhs) in
813
let rhs' = lift 1 rhs in
814
let f (id,(idc,t)) = (id,(idc,replace_term rhs' (mkRel 1) (lift 1 t))) in
815
push_rel d env, List.map f subst, mkRel 1
817
(* We try to instantiate the evar assuming the body won't depend
818
* on arguments that are not Rels or Vars, or appearing several times
819
* (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
821
* 1) Let "env |- ?ev[hyps:=args] = rhs" be the unification problem
822
* 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
823
* where only Rel's and Var's are relevant in subst
824
* 3) We recur on rhs, "imitating" the term, and failing if some Rel/Var is
825
* not in the scope of ?ev. For instance, the problem
826
* "y:nat |- ?x[] = y" where "|- ?1:nat" is not satisfiable because
827
* ?1 would be instantiated by y which is not in the scope of ?1.
828
* 4) We try to "project" the term if the process of imitation fails
829
* and that only one projection is possible
831
* Note: we don't assume rhs in normal form, it may fail while it would
832
* have succeeded after some reductions.
834
* This is the work of [invert_definition Γ Σ ?ev[hyps:=args]
835
* Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
836
* Postcondition: if φ(x1..xn) is returned then
837
* Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
840
exception NotInvertibleUsingOurAlgorithm of constr
841
exception NotEnoughInformationToProgress
843
let rec invert_definition choose env evd (evk,argsv as ev) rhs =
844
let evdref = ref evd in
845
let progress = ref false in
846
let evi = Evd.find (evars_of evd) evk in
847
let subst = make_projectable_subst (evars_of evd) evi argsv in
850
let project_variable t =
851
(* Evar/Var problem: unifiable iff variable projectable from ev subst *)
853
let sols = find_projectable_vars true env (evars_of !evdref) t subst in
854
let c, p = match sols with
855
| [] -> raise Not_found
856
| [id,p] -> (mkVar id, p)
857
| (id,p)::_::_ -> if choose then (mkVar id, p) else raise NotUnique
859
let ty = lazy (Retyping.get_type_of env (evars_of !evdref) t) in
860
let evd = do_projection_effects evar_define env ty !evdref p in
864
| Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
866
if not !progress then raise NotEnoughInformationToProgress;
867
(* No unique projection but still restrict to where it is possible *)
868
let ts = expansions_of_var env t in
869
let test c = isEvar c or List.mem c ts in
870
let filter = array_map_to_list test argsv in
871
let args' = filter_along (fun x -> x) filter argsv in
872
let evd,evar = do_restrict_hyps_virtual !evdref evk filter in
873
let evk',_ = destEvar evar in
874
let pb = (Reduction.CONV,env,mkEvar(evk',args'),t) in
875
evdref := Evd.add_conv_pb pb evd;
878
let rec imitate (env',k as envk) t =
879
let t = whd_evar (evars_of !evdref) t in
880
match kind_of_term t with
881
| Rel i when i>k -> project_variable (mkRel (i-k))
882
| Var id -> project_variable t
883
| Evar (evk',args' as ev') ->
884
if evk = evk' then error_occur_check env (evars_of evd) evk rhs;
885
(* Evar/Evar problem (but left evar is virtual) *)
888
(invert_arg_from_subst env k (evars_of !evdref) subst) args'
891
(* Try to project (a restriction of) the right evar *)
892
let eprojs' = effective_projections projs' in
894
list_fold_map (instance_of_projection evar_define env' t)
896
let evd,evk' = do_restrict_hyps evd evk' projs' in
898
mkEvar (evk',Array.of_list args')
901
(* Make the virtual left evar real *)
902
let (evar'',ev'') = extend_evar env' evdref k ev t in
904
(* Try to project (a restriction of) the left evar ... *)
905
try solve_evar_evar_l2r evar_define env' !evdref ev'' ev'
906
with CannotProject projs'' ->
907
(* ... or postpone the problem *)
908
postpone_evar_evar env' !evdref projs'' ev'' projs' ev' in
913
(* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
914
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
917
let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in
918
let body = imitate (env,0) rhs in
921
(* [evar_define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
922
* an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
923
* [evar_define] tries to find an instance lhs such that
924
* "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
925
* context "hyps" and not referring to itself.
928
and occur_existential evm c =
929
let rec occrec c = match kind_of_term c with
930
| Evar (e, _) -> if not (is_defined evm e) then raise Occur
931
| _ -> iter_constr occrec c
932
in try occrec c; false with Occur -> true
934
and evar_define ?(choose=false) env (evk,_ as ev) rhs evd =
936
let (evd',body) = invert_definition choose env evd ev rhs in
937
if occur_meta body then error "Meta cannot occur in evar body.";
938
(* invert_definition may have instantiate some evars of rhs with evk *)
939
(* so we recheck acyclicity *)
940
if occur_evar evk body then error_occur_check env (evars_of evd) evk body;
941
(* needed only if an inferred type *)
942
let body = refresh_universes body in
943
(* Cannot strictly type instantiations since the unification algorithm
944
* does not unify applications from left to right.
945
* e.g problem f x == g y yields x==y and f==g (in that order)
946
* Another problem is that type variables are evars of type Type
949
let env = evar_env evi in
950
let ty = evi.evar_concl in
951
Typing.check env (evars_of evd') body ty
954
(str "Ill-typed evar instantiation: " ++ fnl() ++
955
pr_evar_defs evd' ++ fnl() ++
956
str "----> " ++ int ev ++ str " := " ++
959
Evd.evar_define evk body evd'
961
| NotEnoughInformationToProgress ->
962
postpone_evar_term env evd ev rhs
963
| NotInvertibleUsingOurAlgorithm t ->
964
error_not_clean env (evars_of evd) evk t (evar_source evk evd)
966
(*-------------------*)
967
(* Auxiliary functions for the conversion algorithms modulo evars
970
let has_undefined_evars evd t =
971
let evm = evars_of evd in
973
match kind_of_term t with
975
(match evar_body (Evd.find evm ev) with
977
has_ev c; Array.iter has_ev args
979
raise NotInstantiatedEvar)
980
| _ -> iter_constr has_ev t in
981
try let _ = has_ev t in false
982
with (Not_found | NotInstantiatedEvar) -> true
984
let is_ground_term evd t =
985
not (has_undefined_evars evd t)
987
let is_ground_env evd env =
988
let is_ground_decl = function
989
(_,Some b,_) -> is_ground_term evd b
991
List.for_all is_ground_decl (rel_context env) &&
992
List.for_all is_ground_decl (named_context env)
993
(* Memoization is safe since evar_map and environ are applicative
995
let is_ground_env = memo1_2 is_ground_env
998
let rec hrec c = match kind_of_term c with
999
| Evar (evk,_) -> evk
1000
| Case (_,_,c,_) -> hrec c
1001
| App (c,_) -> hrec c
1002
| Cast (c,_,_) -> hrec c
1003
| _ -> failwith "headconstant"
1007
(* Check if an applied evar "?X[args] l" is a Miller's pattern; note
1008
that we don't care whether args itself contains Rel's or even Rel's
1009
distinct from the ones in l *)
1011
let rec expand_and_check_vars env = function
1014
if isRel a or isVar a then
1015
let l = expand_and_check_vars env l in
1016
match expand_var_opt env a with
1018
| Some a' when isRel a' or isVar a' -> list_add_set a' l
1023
let is_unification_pattern_evar env (_,args) l t =
1024
List.for_all (fun x -> isRel x || isVar x) l (* common failure case *)
1026
let l' = Array.to_list args @ l in
1027
let l'' = try Some (expand_and_check_vars env l') with Exit -> None in
1031
if occur_meta_or_existential t then
1032
(* Probably no restrictions on allowed vars in presence of evars *)
1035
(* Probably strong restrictions coming from t being evar-closed *)
1036
let t = expand_vars_in_term env t in
1037
let fv_rels = free_rels t in
1038
let fv_ids = global_vars env t in
1039
List.filter (fun c ->
1040
match kind_of_term c with
1041
| Var id -> List.mem id fv_ids
1042
| Rel n -> Intset.mem n fv_rels
1043
| _ -> assert false) l in
1047
let is_unification_pattern (env,nb) f l t =
1048
match kind_of_term f with
1050
array_for_all (fun c -> isRel c && destRel c <= nb) l
1053
is_unification_pattern_evar env ev (Array.to_list l) t
1057
(* From a unification problem "?X l1 = term1 l2" such that l1 is made
1058
of distinct rel's, build "\x1...xn.(term1 l2)" (patterns unification) *)
1060
let solve_pattern_eqn env l1 c =
1061
let l1 = List.map (expand_var env) l1 in
1062
let c' = List.fold_right (fun a c ->
1063
let c' = subst_term (lift 1 a) (lift 1 c) in
1064
match kind_of_term a with
1065
(* Rem: if [a] links to a let-in, do as if it were an assumption *)
1066
| Rel n -> let (na,_,t) = lookup_rel n env in mkLambda (na,lift n t,c')
1067
| Var id -> let (id,_,t) = lookup_named id env in mkNamedLambda id t c'
1068
| _ -> assert false)
1070
(* Warning: we may miss some opportunity to eta-reduce more since c'
1071
is not in normal form *)
1074
(* This code (i.e. solve_pb, etc.) takes a unification
1075
* problem, and tries to solve it. If it solves it, then it removes
1076
* all the conversion problems, and re-runs conversion on each one, in
1077
* the hopes that the new solution will aid in solving them.
1079
* The kinds of problems it knows how to solve are those in which
1080
* the usable arguments of an existential var are all themselves
1081
* universal variables.
1082
* The solution to this problem is to do renaming for the Var's,
1083
* to make them match up with the Var's which are found in the
1084
* hyps of the existential, to do a "pop" for each Rel which is
1085
* not an argument of the existential, and a subst1 for each which
1086
* is, again, with the corresponding variable. This is done by
1089
* Thus, we take the arguments of the existential which we are about
1090
* to assign, and zip them with the identifiers in the hypotheses.
1091
* Then, we process all the Var's in the arguments, and sort the
1092
* Rel's into ascending order. Then, we just march up, doing
1093
* subst1's and pop's.
1095
* NOTE: We can do this more efficiently for the relative arguments,
1096
* by building a long substituend by hand, but this is a pain in the
1100
let status_changed lev (pbty,_,t1,t2) =
1102
List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
1104
try List.mem (head_evar t2) lev with Failure _ -> false
1106
(* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
1107
* definitions. We try to unify the xi with the yi pairwise. The pairs
1108
* that don't unify are discarded (i.e. ?i is redefined so that it does not
1109
* depend on these args). *)
1111
let solve_refl conv_algo env evd evk argsv1 argsv2 =
1112
if argsv1 = argsv2 then evd else
1113
let evi = Evd.find (evars_of evd) evk in
1114
(* Filter and restrict if needed *)
1116
restrict_upon_filter evd evi evk
1117
(fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
1118
(List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
1119
(* Leave a unification problem *)
1120
let args1,args2 = List.split args in
1121
let argsv1 = Array.of_list args1 and argsv2 = Array.of_list args2 in
1122
let pb = (Reduction.CONV,env,mkEvar(evk,argsv1),mkEvar(evk,argsv2)) in
1123
Evd.add_conv_pb pb evd
1125
(* Tries to solve problem t1 = t2.
1126
* Precondition: t1 is an uninstantiated evar
1127
* Returns an optional list of evars that were instantiated, or None
1128
* if the problem couldn't be solved. *)
1130
(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
1131
let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
1133
let t2 = whd_evar (evars_of evd) t2 in
1134
let evd = match kind_of_term t2 with
1135
| Evar (evk2,args2 as ev2) ->
1137
solve_refl conv_algo env evd evk1 args1 args2
1139
if pbty = Reduction.CONV
1140
then solve_evar_evar evar_define env evd ev1 ev2
1141
else add_conv_pb (pbty,env,mkEvar ev1,t2) evd
1143
let evd = evar_define ~choose env ev1 t2 evd in
1144
let evm = evars_of evd in
1145
let evi = Evd.find evm evk1 in
1146
if occur_existential evm evi.evar_concl then
1147
let evenv = evar_env evi in
1148
let evc = nf_isevar evd evi.evar_concl in
1149
match evi.evar_body with
1150
| Evar_defined body ->
1151
let ty = nf_isevar evd (Retyping.get_type_of_with_meta evenv evm (metas_of evd) body) in
1152
add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
1153
| Evar_empty -> (* Resulted in a constraint *)
1157
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
1159
(fun (evd,b as p) (pbty,env,t1,t2) ->
1160
if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
1162
with e when precatchable_exception e ->
1165
let evars_of_term c =
1166
let rec evrec acc c =
1167
match kind_of_term c with
1168
| Evar (n, _) -> Intset.add n acc
1169
| _ -> fold_constr evrec acc c
1171
evrec Intset.empty c
1173
let evars_of_named_context nc =
1174
List.fold_right (fun (_, b, t) s ->
1175
Option.fold_left (fun s t ->
1176
Intset.union s (evars_of_term t))
1177
s b) nc Intset.empty
1179
let evars_of_evar_info evi =
1180
Intset.union (evars_of_term evi.evar_concl)
1182
(match evi.evar_body with
1183
| Evar_empty -> Intset.empty
1184
| Evar_defined b -> evars_of_term b)
1185
(evars_of_named_context (named_context_of_val evi.evar_hyps)))
1187
(* [check_evars] fails if some unresolved evar remains *)
1188
(* it assumes that the defined existentials have already been substituted *)
1190
let check_evars env initial_sigma evd c =
1191
let sigma = evars_of evd in
1192
let c = nf_evar sigma c in
1193
let rec proc_rec c =
1194
match kind_of_term c with
1195
| Evar (evk,args) ->
1196
assert (Evd.mem sigma evk);
1197
if not (Evd.mem initial_sigma evk) then
1198
let (loc,k) = evar_source evk evd in
1199
let evi = nf_evar_info sigma (Evd.find sigma evk) in
1200
error_unsolvable_implicit loc env sigma evi k None
1201
| _ -> iter_constr proc_rec c
1204
(* Operations on value/type constraints *)
1206
type type_constraint_type = (int * int) option * constr
1207
type type_constraint = type_constraint_type option
1209
type val_constraint = constr option
1212
* Basically, we have the following kind of constraints (in increasing
1214
* (false,(None,None)) -> no constraint at all
1215
* (true,(None,None)) -> we must build a judgement which _TYPE is a kind
1216
* (_,(None,Some ty)) -> we must build a judgement which _TYPE is ty
1217
* (_,(Some v,_)) -> we must build a judgement which _VAL is v
1218
* Maybe a concrete datatype would be easier to understand.
1219
* We differentiate (true,(None,None)) from (_,(None,Some Type))
1220
* because otherwise Case(s) would be misled, as in
1221
* (n:nat) Case n of bool [_]nat end would infer the predicate Type instead
1225
(* The empty type constraint *)
1226
let empty_tycon = None
1228
let mk_tycon_type c = (None, c)
1229
let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
1230
is current abstraction *)
1232
(* Builds a type constraint *)
1233
let mk_tycon ty = Some (mk_tycon_type ty)
1235
let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
1237
(* Constrains the value of a type *)
1238
let empty_valcon = None
1240
(* Builds a value constraint *)
1241
let mk_valcon c = Some c
1243
(* Refining an evar to a product or a sort *)
1245
(* Declaring any type to be in the sort Type shouldn't be harmful since
1246
cumulativity now includes Prop and Set in Type...
1247
It is, but that's not too bad *)
1248
let define_evar_as_abstraction abs evd (ev,args) =
1249
let evi = Evd.find (evars_of evd) ev in
1250
let evenv = evar_unfiltered_env evi in
1251
let (evd1,dom) = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
1253
next_ident_away (id_of_string "x")
1254
(ids_of_named_context (evar_context evi)) in
1255
let newenv = push_named (nvar, None, dom) evenv in
1257
new_evar evd1 newenv ~src:(evar_source ev evd1) (new_Type())
1258
~filter:(true::evar_filter evi) in
1259
let prod = abs (Name nvar, dom, subst_var nvar rng) in
1260
let evd3 = Evd.evar_define ev prod evd2 in
1261
let evdom = fst (destEvar dom), args in
1263
fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
1264
let prod' = abs (Name nvar, mkEvar evdom, mkEvar evrng) in
1267
let define_evar_as_product evd (ev,args) =
1268
define_evar_as_abstraction (fun t -> mkProd t) evd (ev,args)
1270
let define_evar_as_lambda evd (ev,args) =
1271
define_evar_as_abstraction (fun t -> mkLambda t) evd (ev,args)
1273
let define_evar_as_sort evd (ev,args) =
1274
let s = new_Type () in
1275
Evd.evar_define ev s evd, destSort s
1277
(* We don't try to guess in which sort the type should be defined, since
1278
any type has type Type. May cause some trouble, but not so far... *)
1280
let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
1282
(* Propagation of constraints through application and abstraction:
1283
Given a type constraint on a functional term, returns the type
1284
constraint on its domain and codomain. If the input constraint is
1285
an evar instantiate it with the product of 2 new evars. *)
1287
let split_tycon loc env evd tycon =
1288
let rec real_split evd c =
1289
let t = whd_betadeltaiota env (Evd.evars_of evd) c in
1290
match kind_of_term t with
1291
| Prod (na,dom,rng) -> evd, (na, dom, rng)
1292
| Evar ev when not (Evd.is_defined_evar evd ev) ->
1293
let (evd',prod) = define_evar_as_product evd ev in
1294
let (_,dom,rng) = destProd prod in
1295
evd',(Anonymous, dom, rng)
1296
| _ -> error_not_product_loc loc env (Evd.evars_of evd) c
1299
| None -> evd,(Anonymous,None,None)
1303
let evd', (n, dom, rng) = real_split evd c in
1304
evd', (n, mk_tycon dom, mk_tycon rng)
1305
| Some (init, cur) ->
1307
let evd', (x, dom, rng) = real_split evd c in
1312
evd, (Anonymous, None,
1313
Some (if cur = 1 then None,c else Some (init, pred cur), c)))
1315
let valcon_of_tycon x =
1317
| Some (None, t) -> Some t
1320
let lift_abstr_tycon_type n (abs, t) =
1322
None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
1323
| Some (init, abs) ->
1324
let abs' = abs + n in
1325
if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
1326
else (Some (init, abs'), t)
1328
let lift_tycon_type n (abs, t) = (abs, lift n t)
1329
let lift_tycon n = Option.map (lift_tycon_type n)
1331
let pr_tycon_type env (abs, t) =
1333
None -> Termops.print_constr_env env t
1334
| Some (init, cur) -> str "Abstract (" ++ int init ++ str "," ++ int cur ++ str ") " ++ Termops.print_constr_env env t
1336
let pr_tycon env = function
1338
| Some t -> pr_tycon_type env t
added
removed
pretyping/evarutil.ml
