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: pretyping.ml 12053 2009-04-06 16:20:42Z msozeau $ *)
34
type typing_constraint = OfType of types option | IsType
35
type var_map = (identifier * unsafe_judgment) list
36
type unbound_ltac_var_map = (identifier * identifier option) list
38
(************************************************************************)
39
(* This concerns Cases *)
44
(************************************************************************)
46
(* An auxiliary function for searching for fixpoint guard indexes *)
48
exception Found of int array
50
let search_guard loc env possible_indexes fixdefs =
51
(* Standard situation with only one possibility for each fix. *)
52
(* We treat it separately in order to get proper error msg. *)
53
if List.for_all (fun l->1=List.length l) possible_indexes then
54
let indexes = Array.of_list (List.map List.hd possible_indexes) in
55
let fix = ((indexes, 0),fixdefs) in
56
(try check_fix env fix with
57
| e -> if loc = dummy_loc then raise e else Stdpp.raise_with_loc loc e);
60
(* we now search recursively amoungst all combinations *)
64
let indexes = Array.of_list l in
65
let fix = ((indexes, 0),fixdefs) in
66
try check_fix env fix; raise (Found indexes)
67
with TypeError _ -> ())
68
(list_combinations possible_indexes);
69
let errmsg = "Cannot guess decreasing argument of fix." in
70
if loc = dummy_loc then error errmsg else
71
user_err_loc (loc,"search_guard", Pp.str errmsg)
72
with Found indexes -> indexes)
74
(* To embed constr in rawconstr *)
75
let ((constr_in : constr -> Dyn.t),
76
(constr_out : Dyn.t -> constr)) = create "constr"
78
(** Miscellaneous interpretation functions *)
80
let interp_sort = function
82
| RType _ -> new_Type_sort ()
84
let interp_elimination_sort = function
85
| RProp Null -> InProp
92
module Cases : Cases.S
94
(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
95
val allow_anonymous_refs : bool ref
97
(* Generic call to the interpreter from rawconstr to open_constr, leaving
98
unresolved holes as evars and returning the typing contexts of
99
these evars. Work as [understand_gen] for the rest. *)
101
val understand_tcc : ?resolve_classes:bool ->
102
evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
104
val understand_tcc_evars :
105
evar_defs ref -> env -> typing_constraint -> rawconstr -> constr
107
(* More general entry point with evars from ltac *)
109
(* Generic call to the interpreter from rawconstr to constr, failing
110
unresolved holes in the rawterm cannot be instantiated.
112
In [understand_ltac sigma env ltac_env constraint c],
114
sigma : initial set of existential variables (typically dependent subgoals)
115
ltac_env : partial substitution of variables (used for the tactic language)
116
constraint : tell if interpreted as a possibly constrained term or a type
119
val understand_ltac :
120
evar_map -> env -> var_map * unbound_ltac_var_map ->
121
typing_constraint -> rawconstr -> evar_defs * constr
123
(* Standard call to get a constr from a rawconstr, resolving implicit args *)
125
val understand : evar_map -> env -> ?expected_type:Term.types ->
128
(* Idem but the rawconstr is intended to be a type *)
130
val understand_type : evar_map -> env -> rawconstr -> constr
132
(* A generalization of the two previous case *)
134
val understand_gen : typing_constraint -> evar_map -> env ->
137
(* Idem but returns the judgment of the understood term *)
139
val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
141
(* Idem but do not fail on unresolved evars *)
143
val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment
146
(* Internal of Pretyping...
147
* Unused outside, but useful for debugging
150
type_constraint -> env -> evar_defs ref ->
151
var_map * (identifier * identifier option) list ->
152
rawconstr -> unsafe_judgment
155
val_constraint -> env -> evar_defs ref ->
156
var_map * (identifier * identifier option) list ->
157
rawconstr -> unsafe_type_judgment
160
evar_defs ref -> env ->
161
var_map * (identifier * identifier option) list ->
162
typing_constraint -> rawconstr -> constr
167
module Pretyping_F (Coercion : Coercion.S) = struct
169
module Cases = Cases.Cases_F(Coercion)
171
(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
172
let allow_anonymous_refs = ref false
174
let evd_comb0 f evdref =
175
let (evd',x) = f !evdref in
179
let evd_comb1 f evdref x =
180
let (evd',y) = f !evdref x in
184
let evd_comb2 f evdref x y =
185
let (evd',z) = f !evdref x y in
189
let evd_comb3 f evdref x y z =
190
let (evd',t) = f !evdref x y z in
194
let mt_evd = Evd.empty
196
(* Utilis� pour inf�rer le pr�dicat des Cases *)
197
(* Semble exag�rement fort *)
198
(* Faudra pr�f�rer une unification entre les types de toutes les clauses *)
199
(* et autoriser des ? � rester dans le r�sultat de l'unification *)
201
let evar_type_fixpoint loc env evdref lna lar vdefj =
202
let lt = Array.length vdefj in
203
if Array.length lar = lt then
205
if not (e_cumul env evdref (vdefj.(i)).uj_type
206
(lift lt lar.(i))) then
207
error_ill_typed_rec_body_loc loc env (evars_of !evdref)
211
let check_branches_message loc env evdref c (explft,lft) =
212
for i = 0 to Array.length explft - 1 do
213
if not (e_cumul env evdref lft.(i) explft.(i)) then
214
let sigma = evars_of !evdref in
215
error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
218
(* coerce to tycon if any *)
219
let inh_conv_coerce_to_tycon loc env evdref j = function
221
| Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
223
let push_rels vars env = List.fold_right push_rel vars env
225
(* used to enforce a name in Lambda when the type constraints itself
226
is named, hence possibly dependent *)
228
let orelse_name name name' = match name with
232
let pretype_id loc env (lvar,unbndltacvars) id =
234
let (n,typ) = lookup_rel_id id (rel_context env) in
235
{ uj_val = mkRel n; uj_type = lift n typ }
241
let (_,_,typ) = lookup_named id env in
242
{ uj_val = mkVar id; uj_type = typ }
244
try (* To build a nicer ltac error message *)
245
match List.assoc id unbndltacvars with
246
| None -> user_err_loc (loc,"",
247
str "Variable " ++ pr_id id ++ str " should be bound to a term.")
248
| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
250
error_var_not_found_loc loc id
252
(* make a dependent predicate from an undependent one *)
254
let make_dep_of_undep env (IndType (indf,realargs)) pj =
255
let n = List.length realargs in
258
match kind_of_term p with
259
| Lambda (_,_,c) -> decomp (n-1) c
260
| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1]))
262
let sign,s = decompose_prod_n n pj.uj_type in
263
let ind = build_dependent_inductive env indf in
264
let s' = mkProd (Anonymous, ind, s) in
265
let ccl = lift 1 (decomp n pj.uj_val) in
266
let ccl' = mkLambda (Anonymous, ind, ccl) in
267
{uj_val=lam_it ccl' sign; uj_type=prod_it s' sign}
269
let evar_kind_of_term sigma c =
270
kind_of_term (whd_evar (Evd.evars_of sigma) c)
272
(*************************************************************************)
273
(* Main pretyping function *)
275
let pretype_ref evdref env ref =
276
let c = constr_of_global ref in
277
make_judge c (Retyping.get_type_of env Evd.empty c)
279
let pretype_sort = function
280
| RProp c -> judge_of_prop_contents c
281
| RType _ -> judge_of_new_Type ()
283
exception Found of fixpoint
285
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
286
(* in environment [env], with existential variables [evdref] and *)
287
(* the type constraint tycon *)
288
let rec pretype (tycon : type_constraint) env evdref lvar = function
290
inh_conv_coerce_to_tycon loc env evdref
291
(pretype_ref evdref env ref)
295
inh_conv_coerce_to_tycon loc env evdref
296
(pretype_id loc env lvar id)
299
| REvar (loc, evk, instopt) ->
300
(* Ne faudrait-il pas s'assurer que hyps est bien un
301
sous-contexte du contexte courant, et qu'il n'y a pas de Rel "cach�" *)
302
let hyps = evar_filtered_context (Evd.find (evars_of !evdref) evk) in
303
let args = match instopt with
304
| None -> instance_from_named_context hyps
305
| Some inst -> failwith "Evar subtitutions not implemented" in
306
let c = mkEvar (evk, args) in
307
let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in
308
inh_conv_coerce_to_tycon loc env evdref j tycon
310
| RPatVar (loc,(someta,n)) ->
311
anomaly "Found a pattern variable in a rawterm to type"
316
| Some (None, ty) -> ty
318
e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
319
{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
321
| RRec (loc,fixkind,names,bl,lar,vdef) ->
322
let rec type_bl env ctxt = function
324
| (na,bk,None,ty)::bl ->
325
let ty' = pretype_type empty_valcon env evdref lvar ty in
326
let dcl = (na,None,ty'.utj_val) in
327
type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
328
| (na,bk,Some bd,ty)::bl ->
329
let ty' = pretype_type empty_valcon env evdref lvar ty in
330
let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar ty in
331
let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
332
type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
333
let ctxtv = Array.map (type_bl env empty_rel_context) bl in
337
pretype_type empty_valcon (push_rel_context e env) evdref lvar ar)
339
let lara = Array.map (fun a -> a.utj_val) larj in
340
let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
341
let nbfix = Array.length lar in
342
let names = Array.map (fun id -> Name id) names in
343
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
344
let newenv = push_rec_types (names,ftys,[||]) env in
348
(* we lift nbfix times the type in tycon, because of
349
* the nbfix variables pushed to newenv *)
351
decompose_prod_n_assum (rel_context_length ctxt)
352
(lift nbfix ftys.(i)) in
353
let nenv = push_rel_context ctxt newenv in
354
let j = pretype (mk_tycon ty) nenv evdref lvar def in
355
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
356
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
358
evar_type_fixpoint loc env evdref names ftys vdefj;
359
let ftys = Array.map (nf_evar (evars_of !evdref)) ftys in
360
let fdefs = Array.map (fun x -> nf_evar (evars_of !evdref) (j_val x)) vdefj in
361
let fixj = match fixkind with
363
(* First, let's find the guard indexes. *)
364
(* If recursive argument was not given by user, we try all args.
365
An earlier approach was to look only for inductive arguments,
366
but doing it properly involves delta-reduction, and it finally
367
doesn't seem worth the effort (except for huge mutual
369
let possible_indexes = Array.to_list (Array.mapi
370
(fun i (n,_) -> match n with
372
| None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
375
let fixdecls = (names,ftys,fdefs) in
376
let indexes = search_guard loc env possible_indexes fixdecls in
377
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
379
let cofix = (i,(names,ftys,fdefs)) in
380
(try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
381
make_judge (mkCoFix cofix) ftys.(i) in
382
inh_conv_coerce_to_tycon loc env evdref fixj tycon
385
inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
387
| RApp (loc,f,args) ->
388
let fj = pretype empty_tycon env evdref lvar f in
389
let floc = loc_of_rawconstr f in
390
let rec apply_rec env n resj = function
393
let argloc = loc_of_rawconstr c in
394
let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
395
let resty = whd_betadeltaiota env (evars_of !evdref) resj.uj_type in
396
match kind_of_term resty with
398
let hj = pretype (mk_tycon c1) env evdref lvar c in
399
let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
405
let hj = pretype empty_tycon env evdref lvar c in
406
error_cant_apply_not_functional_loc
407
(join_loc floc argloc) env (evars_of !evdref)
410
let resj = apply_rec env 1 fj args in
412
match evar_kind_of_term !evdref resj.uj_val with
414
let f = whd_evar (Evd.evars_of !evdref) f in
415
begin match kind_of_term f with
417
when isInd f or has_polymorphic_type (destConst f)
419
let sigma = evars_of !evdref in
420
let c = mkApp (f,Array.map (whd_evar sigma) args) in
421
let t = Retyping.get_type_of env sigma c in
425
inh_conv_coerce_to_tycon loc env evdref resj tycon
427
| RLambda(loc,name,bk,c1,c2) ->
428
let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
429
let dom_valcon = valcon_of_tycon dom in
430
let j = pretype_type dom_valcon env evdref lvar c1 in
431
let var = (name,None,j.utj_val) in
432
let j' = pretype rng (push_rel var env) evdref lvar c2 in
433
judge_of_abstraction env (orelse_name name name') j j'
435
| RProd(loc,name,bk,c1,c2) ->
436
let j = pretype_type empty_valcon env evdref lvar c1 in
437
let var = (name,j.utj_val) in
438
let env' = push_rel_assum var env in
439
let j' = pretype_type empty_valcon env' evdref lvar c2 in
441
try judge_of_product env name j j'
442
with TypeError _ as e -> Stdpp.raise_with_loc loc e in
443
inh_conv_coerce_to_tycon loc env evdref resj tycon
445
| RLetIn(loc,name,c1,c2) ->
448
| RCast (loc, c, CastConv (DEFAULTcast, t)) ->
449
let tj = pretype_type empty_valcon env evdref lvar t in
450
pretype (mk_tycon tj.utj_val) env evdref lvar c
451
| _ -> pretype empty_tycon env evdref lvar c1
453
let t = refresh_universes j.uj_type in
454
let var = (name,Some j.uj_val,t) in
455
let tycon = lift_tycon 1 tycon in
456
let j' = pretype tycon (push_rel var env) evdref lvar c2 in
457
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
458
uj_type = subst1 j.uj_val j'.uj_type }
460
| RLetTuple (loc,nal,(na,po),c,d) ->
461
let cj = pretype empty_tycon env evdref lvar c in
462
let (IndType (indf,realargs)) =
463
try find_rectype env (evars_of !evdref) cj.uj_type
465
let cloc = loc_of_rawconstr c in
466
error_case_not_inductive_loc cloc env (evars_of !evdref) cj
468
let cstrs = get_constructors env indf in
469
if Array.length cstrs <> 1 then
470
user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor.");
471
let cs = cstrs.(0) in
472
if List.length nal <> cs.cs_nargs then
473
user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables.");
474
let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
475
(List.rev nal) cs.cs_args in
476
let env_f = push_rels fsign env in
477
(* Make dependencies from arity signature impossible *)
479
let arsgn,_ = get_arity env indf in
480
if not !allow_anonymous_refs then
481
List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
484
let psign = (na,None,build_dependent_inductive env indf)::arsgn in
485
let nar = List.length arsgn in
488
let env_p = push_rels psign env in
489
let pj = pretype_type empty_valcon env_p evdref lvar p in
490
let ccl = nf_isevar !evdref pj.utj_val in
491
let psign = make_arity_signature env true indf in (* with names *)
492
let p = it_mkLambda_or_LetIn ccl psign in
494
(Array.to_list cs.cs_concl_realargs)
495
@[build_dependent_constructor cs] in
496
let lp = lift cs.cs_nargs p in
497
let fty = hnf_lam_applist env (evars_of !evdref) lp inst in
498
let fj = pretype (mk_tycon fty) env_f evdref lvar d in
499
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
501
let mis,_ = dest_ind_family indf in
502
let ci = make_case_info env mis LetStyle in
503
mkCase (ci, p, cj.uj_val,[|f|]) in
504
{ uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
507
let tycon = lift_tycon cs.cs_nargs tycon in
508
let fj = pretype tycon env_f evdref lvar d in
509
let f = it_mkLambda_or_LetIn fj.uj_val fsign in
510
let ccl = nf_isevar !evdref fj.uj_type in
512
if noccur_between 1 cs.cs_nargs ccl then
513
lift (- cs.cs_nargs) ccl
515
error_cant_find_case_type_loc loc env (evars_of !evdref)
517
let ccl = refresh_universes ccl in
518
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
520
let mis,_ = dest_ind_family indf in
521
let ci = make_case_info env mis LetStyle in
522
mkCase (ci, p, cj.uj_val,[|f|] )
524
{ uj_val = v; uj_type = ccl })
526
| RIf (loc,c,(na,po),b1,b2) ->
527
let cj = pretype empty_tycon env evdref lvar c in
528
let (IndType (indf,realargs)) =
529
try find_rectype env (evars_of !evdref) cj.uj_type
531
let cloc = loc_of_rawconstr c in
532
error_case_not_inductive_loc cloc env (evars_of !evdref) cj in
533
let cstrs = get_constructors env indf in
534
if Array.length cstrs <> 2 then
535
user_err_loc (loc,"",
536
str "If is only for inductive types with two constructors.");
539
let arsgn,_ = get_arity env indf in
540
if not !allow_anonymous_refs then
541
(* Make dependencies from arity signature impossible *)
542
List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
545
let nar = List.length arsgn in
546
let psign = (na,None,build_dependent_inductive env indf)::arsgn in
547
let pred,p = match po with
549
let env_p = push_rels psign env in
550
let pj = pretype_type empty_valcon env_p evdref lvar p in
551
let ccl = nf_evar (evars_of !evdref) pj.utj_val in
552
let pred = it_mkLambda_or_LetIn ccl psign in
553
let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
554
let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred;
557
jtyp.uj_val, jtyp.uj_type
559
let p = match tycon with
560
| Some (None, ty) -> ty
562
e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
564
it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
565
let pred = nf_evar (evars_of !evdref) pred in
566
let p = nf_evar (evars_of !evdref) p in
567
(* msgnl (str "Pred is: " ++ Termops.print_constr_env env pred);*)
569
let n = rel_context_length cs.cs_args in
570
let pi = lift n pred in (* liftn n 2 pred ? *)
571
let pi = beta_applist (pi, [build_dependent_constructor cs]) in
573
if not !allow_anonymous_refs then
574
List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
580
| Anonymous -> (Name (id_of_string "H"), b, t))
583
let env_c = push_rels csgn env in
584
(* msgnl (str "Pi is: " ++ Termops.print_constr_env env_c pi); *)
585
let bj = pretype (mk_tycon pi) env_c evdref lvar b in
586
it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
587
let b1 = f cstrs.(0) b1 in
588
let b2 = f cstrs.(1) b2 in
590
let mis,_ = dest_ind_family indf in
591
let ci = make_case_info env mis IfStyle in
592
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
594
{ uj_val = v; uj_type = p }
596
| RCases (loc,sty,po,tml,eqns) ->
597
Cases.compile_cases loc sty
598
((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
599
tycon env (* loc *) (po,tml,eqns)
605
let cj = pretype empty_tycon env evdref lvar c in
606
evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
608
let tj = pretype_type empty_valcon env evdref lvar t in
609
let cj = pretype (mk_tycon tj.utj_val) env evdref lvar c in
610
(* User Casts are for helping pretyping, experimentally not to be kept*)
611
(* ... except for Correctness *)
612
let v = mkCast (cj.uj_val, k, tj.utj_val) in
613
{ uj_val = v; uj_type = tj.utj_val }
614
in inh_conv_coerce_to_tycon loc env evdref cj tycon
616
| RDynamic (loc,d) ->
617
if (tag d) = "constr" then
618
let c = constr_out d in
619
let j = (Retyping.get_judgment_of env (evars_of !evdref) c) in
621
(*inh_conv_coerce_to_tycon loc env evdref j tycon*)
623
user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
625
(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
626
and pretype_type valcon env evdref lvar = function
631
let sigma = evars_of !evdref in
632
let t = Retyping.get_type_of env sigma v in
633
match kind_of_term (whd_betadeltaiota env sigma t) with
635
| Evar ev when is_Type (existential_type sigma ev) ->
636
evd_comb1 (define_evar_as_sort) evdref ev
637
| _ -> anomaly "Found a type constraint which is not a type"
642
let s = new_Type_sort () in
643
{ utj_val = e_new_evar evdref env ~src:loc (mkSort s);
646
let j = pretype empty_tycon env evdref lvar c in
647
let loc = loc_of_rawconstr c in
648
let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
652
if e_cumul env evdref v tj.utj_val then tj
654
error_unexpected_type_loc
655
(loc_of_rawconstr c) env (evars_of !evdref) tj.utj_val v
657
let pretype_gen_aux evdref env lvar kind c =
658
let c' = match kind with
660
let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
661
(pretype tycon env evdref lvar c).uj_val
663
(pretype_type empty_valcon env evdref lvar c).utj_val in
664
let evd,_ = consider_remaining_unif_problems env !evdref in
668
let pretype_gen evdref env lvar kind c =
669
let c = pretype_gen_aux evdref env lvar kind c in
670
evdref := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env !evdref;
673
(* TODO: comment faire remonter l'information si le typage a resolu des
674
variables du sigma original. il faudrait que la fonction de typage
675
retourne aussi le nouveau sigma...
678
let understand_judgment sigma env c =
679
let evdref = ref (create_evar_defs sigma) in
680
let j = pretype empty_tycon env evdref ([],[]) c in
681
let evd,_ = consider_remaining_unif_problems env !evdref in
682
let j = j_nf_evar (evars_of evd) j in
683
let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evd in
684
let j = j_nf_evar (evars_of evd) j in
685
check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
688
let understand_judgment_tcc evdref env c =
689
let j = pretype empty_tycon env evdref ([],[]) c in
690
let sigma = evars_of !evdref in
691
let j = j_nf_evar sigma j in
694
(* Raw calls to the unsafe inference machine: boolean says if we must
695
fail on unresolved evars; the unsafe_judgment list allows us to
696
extend env with some bindings *)
698
let ise_pretype_gen fail_evar sigma env lvar kind c =
699
let evdref = ref (Evd.create_evar_defs sigma) in
700
let c = pretype_gen_aux evdref env lvar kind c in
702
let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in
703
let c = Evarutil.nf_isevar evd c in
704
check_evars env Evd.empty evd c;
708
(** Entry points of the high-level type synthesis algorithm *)
710
let understand_gen kind sigma env c =
711
snd (ise_pretype_gen true sigma env ([],[]) kind c)
713
let understand sigma env ?expected_type:exptyp c =
714
snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
716
let understand_type sigma env c =
717
snd (ise_pretype_gen true sigma env ([],[]) IsType c)
719
let understand_ltac sigma env lvar kind c =
720
ise_pretype_gen false sigma env lvar kind c
722
let understand_tcc_evars evdref env kind c =
723
pretype_gen evdref env ([],[]) kind c
725
let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
727
let evdref = ref (Evd.create_evar_defs sigma) in
729
if resolve_classes then
730
pretype_gen evdref env ([],[]) (OfType exptyp) c
732
pretype_gen_aux evdref env ([],[]) (OfType exptyp) c
734
in Evd.evars_of evd, t
737
module Default : S = Pretyping_F(Coercion.Default)
added
removed
pretyping/pretyping.ml
