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: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
33
let pf_env gls = Global.env_of_context gls.it.evar_hyps
34
let pf_type_of gls c = Typing.type_of (pf_env gls) gls.sigma c
35
let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
36
let pf_concl gl = gl.it.evar_concl
38
(******************************************************************)
39
(* Clausal environments *)
44
templval : constr freelisted;
45
templtyp : constr freelisted }
47
let cl_env ce = ce.env
48
let cl_sigma ce = evars_of ce.evd
50
let subst_clenv sub clenv =
51
{ templval = map_fl (subst_mps sub) clenv.templval;
52
templtyp = map_fl (subst_mps sub) clenv.templtyp;
53
evd = subst_evar_defs_light sub clenv.evd;
56
let clenv_nf_meta clenv c = nf_meta clenv.evd c
57
let clenv_term clenv c = meta_instance clenv.evd c
58
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
59
let clenv_value clenv = meta_instance clenv.evd clenv.templval
60
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp
63
let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
65
let clenv_get_type_of ce c =
66
Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) (metas_of ce.evd) c
68
exception NotExtensibleClause
70
let clenv_push_prod cl =
71
let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
72
let rec clrec typ = match kind_of_term typ with
73
| Cast (t,_,_) -> clrec t
75
let mv = new_meta () in
76
let dep = dependent (mkRel 1) u in
77
let na' = if dep then na else Anonymous in
78
let e' = meta_declare mv t ~name:na' cl.evd in
79
let concl = if dep then subst1 (mkMeta mv) u else u in
80
let def = applist (cl.templval.rebus,[mkMeta mv]) in
81
{ templval = mk_freelisted def;
82
templtyp = mk_freelisted concl;
85
| _ -> raise NotExtensibleClause
88
(* Instantiate the first [bound] products of [t] with metas (all products if
89
[bound] is [None]; unfold local defs *)
91
let clenv_environments evd bound t =
92
let rec clrec (e,metas) n t =
93
match n, kind_of_term t with
94
| (Some 0, _) -> (e, List.rev metas, t)
95
| (n, Cast (t,_,_)) -> clrec (e,metas) n t
96
| (n, Prod (na,t1,t2)) ->
97
let mv = new_meta () in
98
let dep = dependent (mkRel 1) t2 in
99
let na' = if dep then na else Anonymous in
100
let e' = meta_declare mv t1 ~name:na' e in
101
clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
102
(if dep then (subst1 (mkMeta mv) t2) else t2)
103
| (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
104
| (n, _) -> (e, List.rev metas, t)
106
clrec (evd,[]) bound t
108
(* Instantiate the first [bound] products of [t] with evars (all products if
109
[bound] is [None]; unfold local defs *)
111
let clenv_environments_evars env evd bound t =
112
let rec clrec (e,ts) n t =
113
match n, kind_of_term t with
114
| (Some 0, _) -> (e, List.rev ts, t)
115
| (n, Cast (t,_,_)) -> clrec (e,ts) n t
116
| (n, Prod (na,t1,t2)) ->
117
let e',constr = Evarutil.new_evar e env t1 in
118
let dep = dependent (mkRel 1) t2 in
119
clrec (e', constr::ts) (Option.map ((+) (-1)) n)
120
(if dep then (subst1 constr t2) else t2)
121
| (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
122
| (n, _) -> (e, List.rev ts, t)
124
clrec (evd,[]) bound t
126
let clenv_conv_leq env sigma t c bound =
127
let ty = Retyping.get_type_of env sigma c in
128
let evd = Evd.create_goal_evar_defs sigma in
129
let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
130
let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
131
let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
132
let args = List.map (whd_evar (Evd.evars_of evars)) args in
133
check_evars env sigma evars (applist (c,args));
136
let mk_clenv_from_env environ sigma n (c,cty) =
137
let evd = create_goal_evar_defs sigma in
138
let (env,args,concl) = clenv_environments evd n cty in
139
{ templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
140
templtyp = mk_freelisted concl;
144
let mk_clenv_from_n gls n (c,cty) =
145
mk_clenv_from_env (Global.env_of_context gls.it.evar_hyps) gls.sigma n (c, cty)
147
let mk_clenv_from gls = mk_clenv_from_n gls None
149
let mk_clenv_rename_from_n gls n (c,t) =
150
mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
152
let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)
154
(******************************************************************)
156
(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
157
* mv0, or if one of the free vars on mv1's freelist mentions
160
let mentions clenv mv0 =
164
try match meta_opt_fvalue clenv.evd mv1 with
165
| Some (b,_) -> b.freemetas
166
| None -> Metaset.empty
167
with Not_found -> Metaset.empty in
168
meta_exists menrec mlist
171
let clenv_defined clenv mv = meta_defined clenv.evd mv
173
let error_incompatible_inst clenv mv =
174
let na = meta_name clenv.evd mv in
177
errorlabstrm "clenv_assign"
178
(str "An incompatible instantiation has already been found for " ++
181
anomaly "clenv_assign: non dependent metavar already assigned"
183
(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)
184
let clenv_assign mv rhs clenv =
185
let rhs_fls = mk_freelisted rhs in
186
if meta_exists (mentions clenv mv) rhs_fls.freemetas then
187
error "clenv_assign: circularity in unification";
189
if meta_defined clenv.evd mv then
190
if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
191
error_incompatible_inst clenv mv
195
let st = (ConvUpToEta 0,TypeNotProcessed) in
196
{clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
198
error "clenv_assign: undefined meta"
201
let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }
204
(* [clenv_dependent hyps_only clenv]
205
* returns a list of the metavars which appear in the template of clenv,
206
* and which are dependent, This is computed by taking the metavars in cval,
207
* in right-to-left order, and collecting the metavars which appear
208
* in their types, and adding in all the metavars appearing in the
210
* If [hyps_only] then metavariables occurring in the type are _excluded_ *)
212
(* [clenv_metavars clenv mv]
213
* returns a list of the metavars which appear in the type of
214
* the metavar mv. The list is unordered. *)
216
let clenv_metavars evd mv =
217
(mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
219
let dependent_metas clenv mvs conclmetas =
222
Metaset.union deps (clenv_metavars clenv.evd mv))
225
let duplicated_metas c =
226
let rec collrec (one,more as acc) c =
227
match kind_of_term c with
228
| Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more)
229
| _ -> fold_constr collrec acc c
231
snd (collrec ([],[]) c)
233
let clenv_dependent hyps_only clenv =
234
let mvs = undefined_metas clenv.evd in
235
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
236
let deps = dependent_metas clenv mvs ctyp_mvs in
237
let nonlinear = duplicated_metas (clenv_value clenv) in
238
(* Make the assumption that duplicated metas have internal dependencies *)
240
(fun mv -> (Metaset.mem mv deps &&
241
not (hyps_only && Metaset.mem mv ctyp_mvs))
242
or List.mem mv nonlinear)
245
let clenv_missing ce = clenv_dependent true ce
247
(******************************************************************)
249
let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
251
evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
253
let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
254
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
256
let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
257
if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
258
clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
259
(clenv_unify_meta_types ~flags:flags clenv)
261
clenv_unify allow_K CUMUL ~flags:flags
262
(meta_reducible_instance clenv.evd clenv.templtyp) (pf_concl gl) clenv
264
(* [clenv_pose_metas_as_evars clenv dep_mvs]
265
* For each dependent evar in the clause-env which does not have a value,
266
* pose a value for it by constructing a fresh evar. We do this in
267
* left-to-right order, so that every evar's type is always closed w.r.t.
270
* Node added 14/4/08 [HH]: before this date, evars were collected in
271
clenv_dependent by collect_metas in the fold_constr order which is
272
(almost) the left-to-right order of dependencies in term. However,
273
due to K-redexes, collect_metas was sometimes missing some metas.
274
The call to collect_metas has been replaced by a call to
275
undefined_metas, but then the order was the one of definition of
276
the metas (numbers in increasing order) which is _not_ the
277
dependency order when a clenv_fchain occurs (because clenv_fchain
278
plugs a term with a list of consecutive metas in place of a - a priori -
279
arbitrary metavariable belonging to another sequence of consecutive metas:
280
e.g., clenv_fchain may plug (H ?1 ?2) at the position ?6 of
281
(nat_ind ?3 ?4 ?5 ?6), leading to a dependency order 3<4<5<1<2).
282
To ensure the dependency order, we check that the type of each meta
283
to pose is already meta-free, otherwise we postpone the transformation,
284
hoping that no cycle may happen.
286
Another approach could have been to use decimal numbers for metas so that
287
in the example above, (H ?1 ?2) would have been renumbered (H ?6.1 ?6.2)
288
then making the numeric order match the dependency order.
291
let clenv_pose_metas_as_evars clenv dep_mvs =
292
let rec fold clenv = function
295
let ty = clenv_meta_type clenv mv in
296
(* Postpone the evar-ization if dependent on another meta *)
297
(* This assumes no cycle in the dependencies - is it correct ? *)
298
if occur_meta ty then fold clenv (mvs@[mv])
301
new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
302
let clenv = clenv_assign mv evar {clenv with evd=evd} in
306
let evar_clenv_unique_resolver = clenv_unique_resolver
308
(******************************************************************)
310
let connect_clenv gls clenv =
312
evd = evars_reset_evd gls.sigma clenv.evd;
313
env = Global.env_of_context gls.it.evar_hyps }
315
(* [clenv_fchain mv clenv clenv']
317
* Resolves the value of "mv" (which must be undefined) in clenv to be
318
* the template of clenv' be the value "c", applied to "n" fresh
319
* metavars, whose types are chosen by destructing "clf", which should
320
* be a clausale forme generated from the type of "c". The process of
321
* resolution can cause unification of already-existing metavars, and
322
* of the fresh ones which get created. This operation is a composite
323
* of operations which pose new metavars, perform unification on
324
* terms, and make bindings.
328
[clenv] = [env;sigma;metas |- c:T]
329
[clenv'] = [env';sigma';metas' |- d:U]
330
[mv] = [mi] of type [Ti] in [metas]
332
then, if the unification of [Ti] and [U] produces map [rho], the
333
chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
334
[rho'] being [rho;mi:=d].
336
In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
338
let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
339
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
341
{ templval = clenv.templval;
342
templtyp = clenv.templtyp;
344
evar_merge (meta_merge clenv.evd nextclenv.evd) (evars_of clenv.evd);
345
env = nextclenv.env } in
346
(* unify the type of the template of [nextclenv] with the type of [mv] *)
348
clenv_unify allow_K ~flags:flags CUMUL
349
(clenv_term clenv' nextclenv.templtyp)
350
(clenv_meta_type clenv' mv)
352
(* assign the metavar *)
354
clenv_assign mv (clenv_term clenv' nextclenv.templval) clenv''
358
(***************************************************************)
361
type arg_bindings = open_constr explicit_bindings
363
(* [clenv_independent clenv]
364
* returns a list of metavariables which appear in the term cval,
365
* and which are not dependent. That is, they do not appear in
366
* the types of other metavars which are in cval, nor in the type
369
let clenv_independent clenv =
370
let mvs = collect_metas (clenv_value clenv) in
371
let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
372
let deps = dependent_metas clenv mvs ctyp_mvs in
373
List.filter (fun mv -> not (Metaset.mem mv deps)) mvs
375
let check_bindings bl =
376
match list_duplicates (List.map pi2 bl) with
379
(str "The variable " ++ pr_id s ++
380
str " occurs more than once in binding list.");
383
(str "The position " ++ int n ++
384
str " occurs more than once in binding list.")
387
let meta_of_binder clause loc mvs = function
388
| NamedHyp s -> meta_with_name clause.evd s
390
try List.nth mvs (n-1)
391
with (Failure _|Invalid_argument _) ->
392
errorlabstrm "" (str "No such binder.")
394
let error_already_defined b =
398
(str "Binder name \"" ++ pr_id id ++
399
str"\" already defined with incompatible value.")
402
(str "Position " ++ int n ++ str" already defined.")
404
let clenv_unify_binding_type clenv c t u =
405
if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
406
(* Not enough information to know if some subtyping is needed *)
407
CoerceToType, clenv, c
409
(* Enough information so as to try a coercion now *)
411
let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
412
TypeProcessed, { clenv with evd = evd }, c
413
with e when precatchable_exception e ->
414
TypeNotProcessed, clenv, c
416
let clenv_assign_binding clenv k (sigma,c) =
417
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
418
let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
419
let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
420
let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
421
{ clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
423
let clenv_match_args bl clenv =
427
let mvs = clenv_independent clenv in
430
(fun clenv (loc,b,(sigma,c as sc)) ->
431
let k = meta_of_binder clenv loc mvs b in
432
if meta_defined clenv.evd k then
433
if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv
434
else error_already_defined b
436
clenv_assign_binding clenv k sc)
439
let clenv_constrain_last_binding c clenv =
440
let all_mvs = collect_metas clenv.templval.rebus in
442
try list_last all_mvs
443
with Failure _ -> anomaly "clenv_constrain_with_bindings" in
444
clenv_assign_binding clenv k (Evd.empty,c)
446
let clenv_constrain_dep_args hyps_only bl clenv =
450
let occlist = clenv_dependent hyps_only clenv in
451
if List.length occlist = List.length bl then
452
List.fold_left2 clenv_assign_binding clenv occlist bl
455
(strbrk "Not the right number of missing arguments (expected " ++
456
int (List.length occlist) ++ str ").")
458
(****************************************************************)
459
(* Clausal environment for an application *)
461
let make_clenv_binding_gen hyps_only n gls (c,t) = function
462
| ImplicitBindings largs ->
463
let clause = mk_clenv_from_n gls n (c,t) in
464
clenv_constrain_dep_args hyps_only largs clause
465
| ExplicitBindings lbind ->
466
let clause = mk_clenv_rename_from_n gls n (c,t) in
467
clenv_match_args lbind clause
469
mk_clenv_from_n gls n (c,t)
471
let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
472
let make_clenv_binding = make_clenv_binding_gen false None
474
(****************************************************************)
479
(str"TEMPL: " ++ print_constr clenv.templval.rebus ++
480
str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
481
pr_evar_defs clenv.evd)
added
removed
pretyping/clenv.ml
