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: detyping.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
31
(****************************************************************************)
32
(* Tools for printing of Cases *)
34
let encode_inductive r =
35
let indsp = inductive_of_reference r in
36
let constr_lengths = mis_constr_nargs indsp in
37
(indsp,constr_lengths)
39
(* Parameterization of the translation from constr to ast *)
41
(* Tables for Cases printing under a "if" form, a "let" form, *)
43
let has_two_constructors lc =
44
Array.length lc = 2 (* & lc.(0) = 0 & lc.(1) = 0 *)
46
let isomorphic_to_tuple lc = (Array.length lc = 1)
49
let (_,lc as x) = encode_inductive r in
50
if not (has_two_constructors lc) then
51
user_err_loc (loc_of_reference r,"encode_if",
52
str "This type has not exactly two constructors.");
56
let (_,lc as x) = encode_inductive r in
57
if not (isomorphic_to_tuple lc) then
58
user_err_loc (loc_of_reference r,"encode_tuple",
59
str "This type cannot be seen as a tuple type.");
62
module PrintingCasesMake =
64
val encode : reference -> inductive * int array
65
val member_message : std_ppcmds -> bool -> std_ppcmds
70
type t = inductive * int array
71
let encode = Test.encode
72
let subst subst ((kn,i), ints as obj) =
73
let kn' = subst_kn subst kn in
74
if kn' == kn then obj else
76
let printer (ind,_) = pr_global_env Idset.empty (IndRef ind)
77
let key = Goptions.SecondaryTable ("Printing",Test.field)
78
let title = Test.title
79
let member_message x = Test.member_message (printer x)
80
let synchronous = true
83
module PrintingCasesIf =
84
PrintingCasesMake (struct
85
let encode = encode_bool
87
let title = "Types leading to pretty-printing of Cases using a `if' form: "
88
let member_message s b =
89
str "Cases on elements of " ++ s ++
91
(if b then " are printed using a `if' form"
92
else " are not printed using a `if' form")
95
module PrintingCasesLet =
96
PrintingCasesMake (struct
97
let encode = encode_tuple
100
"Types leading to a pretty-printing of Cases using a `let' form:"
101
let member_message s b =
102
str "Cases on elements of " ++ s ++
104
(if b then " are printed using a `let' form"
105
else " are not printed using a `let' form")
108
module PrintingIf = Goptions.MakeRefTable(PrintingCasesIf)
109
module PrintingLet = Goptions.MakeRefTable(PrintingCasesLet)
111
(* Flags.for printing or not wildcard and synthetisable types *)
115
let wildcard_value = ref true
116
let force_wildcard () = !wildcard_value
118
let _ = declare_bool_option
120
optname = "forced wildcard";
121
optkey = SecondaryTable ("Printing","Wildcard");
122
optread = force_wildcard;
123
optwrite = (:=) wildcard_value }
125
let synth_type_value = ref true
126
let synthetize_type () = !synth_type_value
128
let _ = declare_bool_option
130
optname = "pattern matching return type synthesizability";
131
optkey = SecondaryTable ("Printing","Synth");
132
optread = synthetize_type;
133
optwrite = (:=) synth_type_value }
135
let reverse_matching_value = ref true
136
let reverse_matching () = !reverse_matching_value
138
let _ = declare_bool_option
140
optname = "pattern-matching reversibility";
141
optkey = SecondaryTable ("Printing","Matching");
142
optread = reverse_matching;
143
optwrite = (:=) reverse_matching_value }
145
(* Auxiliary function for MutCase printing *)
146
(* [computable] tries to tell if the predicate typing the result is inferable*)
149
(* We first remove as many lambda as the arity, then we look
150
if it remains a lambda for a dependent elimination. This function
151
works for normal eta-expanded term. For non eta-expanded or
152
non-normal terms, it may affirm the pred is synthetisable
153
because of an undetected ultimate dependent variable in the second
154
clause, or else, it may affirms the pred non synthetisable
155
because of a non normal term in the fourth clause.
156
A solution could be to store, in the MutCase, the eta-expanded
157
normal form of pred to decide if it depends on its variables
159
Lorsque le pr�dicat est d�pendant de mani�re certaine, on
160
ne d�clare pas le pr�dicat synth�tisable (m�me si la
161
variable d�pendante ne l'est pas effectivement) parce que
162
sinon on perd la r�ciprocit� de la synth�se (qui, lui,
163
engendrera un pr�dicat non d�pendant) *)
167
let _,ccl = decompose_lam p in
168
noccur_between 1 (k+1) ccl
170
let avoid_flag isgoal = if isgoal then Some true else None
172
let lookup_name_as_renamed env t s =
173
let rec lookup avoid env_names n c = match kind_of_term c with
174
| Prod (name,_,c') ->
175
(match concrete_name (Some true) avoid env_names name c' with
176
| (Name id,avoid') ->
177
if id=s then (Some n)
178
else lookup avoid' (add_name (Name id) env_names) (n+1) c'
179
| (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
180
| LetIn (name,_,_,c') ->
181
(match concrete_name (Some true) avoid env_names name c' with
182
| (Name id,avoid') ->
183
if id=s then (Some n)
184
else lookup avoid' (add_name (Name id) env_names) (n+1) c'
185
| (Anonymous,avoid') -> lookup avoid' env_names (n+1) (pop c'))
186
| Cast (c,_,_) -> lookup avoid env_names n c
188
in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
190
let lookup_index_as_renamed env t n =
191
let rec lookup n d c = match kind_of_term c with
192
| Prod (name,_,c') ->
193
(match concrete_name (Some true) [] empty_names_context name c' with
194
(Name _,_) -> lookup n (d+1) c'
201
lookup (n-1) (d+1) c')
202
| LetIn (name,_,_,c') ->
203
(match concrete_name (Some true) [] empty_names_context name c' with
204
| (Name _,_) -> lookup n (d+1) c'
211
lookup (n-1) (d+1) c'
213
| Cast (c,_,_) -> lookup n d c
214
| _ -> if n=0 then Some (d-1) else None
217
(**********************************************************************)
218
(* Fragile algorithm to reverse pattern-matching compilation *)
220
let update_name na ((_,e),c) =
222
| Name _ when force_wildcard () & noccurn (list_index na e) c ->
227
let rec decomp_branch n nal b (avoid,env as e) c =
228
if n=0 then (List.rev nal,(e,c))
231
match kind_of_term (strip_outer_cast c) with
232
| Lambda (na,_,c) -> na,c,concrete_let_name
233
| LetIn (na,_,_,c) -> na,c,concrete_name
235
Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
237
let na',avoid' = f (Some b) avoid env na c in
238
decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
240
let rec build_tree na isgoal e ci cl =
241
let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
242
let cnl = ci.ci_cstr_nargs in
244
(list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
247
and align_tree nal isgoal (e,c as rhs) = match nal with
250
match kind_of_term c with
251
| Case (ci,p,c,cl) when c = mkRel (list_index na (snd e))
252
& (* don't contract if p dependent *)
253
computable p (ci.ci_pp_info.ind_nargs) ->
254
let clauses = build_tree na isgoal e ci cl in
256
(List.map (fun (pat,rhs) ->
257
let lines = align_tree nal isgoal rhs in
258
List.map (fun (hd,rest) -> pat::hd,rest) lines)
261
let pat = PatVar(dl,update_name na rhs) in
262
let mat = align_tree nal isgoal rhs in
263
List.map (fun (hd,rest) -> pat::hd,rest) mat
265
and contract_branch isgoal e (cn,mkpat,b) =
266
let nal,rhs = decomp_branch cn [] isgoal e b in
267
let mat = align_tree nal isgoal rhs in
268
List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
270
(**********************************************************************)
271
(* Transform internal representation of pattern-matching into list of *)
274
let is_nondep_branch c n =
276
let sign,ccl = decompose_lam_n_assum n c in
277
noccur_between 1 (rel_context_length sign) ccl
278
with _ -> (* Not eta-expanded or not reduced *)
281
let extract_nondep_branches test c b n =
282
let rec strip n r = if n=0 then r else
284
| RLambda (_,_,_,_,t) -> strip (n-1) t
285
| RLetIn (_,_,_,t) -> strip (n-1) t
286
| _ -> assert false in
287
if test c n then Some (strip n b) else None
289
let it_destRLambda_or_LetIn_names n c =
290
let rec aux n nal c =
291
if n=0 then (List.rev nal,c) else match c with
292
| RLambda (_,na,_,_,c) -> aux (n-1) (na::nal) c
293
| RLetIn (_,na,_,c) -> aux (n-1) (na::nal) c
297
let x = Nameops.next_ident_away (id_of_string "x") l in
298
(* Not efficient but unusual and no function to get free rawvars *)
299
(* if occur_rawconstr x c then next (x::l) else x in *)
302
let x = next (free_rawvars c) in
303
let a = RVar (dl,x) in
304
aux (n-1) (Name x :: nal)
306
| RApp (loc,p,l) -> RApp (loc,c,l@[a])
307
| _ -> (RApp (dl,c,[a])))
310
let detype_case computable detype detype_eqns testdep avoid data p c bl =
311
let (indsp,st,nparams,consnargsl,k) = data in
312
let synth_type = synthetize_type () in
313
let tomatch = detype c in
314
let alias, aliastyp, pred=
315
if (not !Flags.raw_print) & synth_type & computable & Array.length bl<>0
317
Anonymous, None, None
319
match Option.map detype p with
320
| None -> Anonymous, None, None
322
let nl,typ = it_destRLambda_or_LetIn_names k p in
323
let n,typ = match typ with
324
| RLambda (_,x,_,t,c) -> x, c
325
| _ -> Anonymous, typ in
327
if List.for_all ((=) Anonymous) nl then None
328
else Some (dl,indsp,nparams,nl) in
329
n, aliastyp, Some typ
331
let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
332
let eqnl = detype_eqns constructs consnargsl bl in
335
if !Flags.raw_print then
337
else if st = LetPatternStyle then
339
else if PrintingLet.active (indsp,consnargsl) then
341
else if PrintingIf.active (indsp,consnargsl) then
348
| LetStyle when aliastyp = None ->
349
let bl' = Array.map detype bl in
350
let (nal,d) = it_destRLambda_or_LetIn_names consnargsl.(0) bl'.(0) in
351
RLetTuple (dl,nal,(alias,pred),tomatch,d)
352
| IfStyle when aliastyp = None ->
353
let bl' = Array.map detype bl in
355
array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
356
if array_for_all ((<>) None) nondepbrs then
357
RIf (dl,tomatch,(alias,pred),
358
Option.get nondepbrs.(0),Option.get nondepbrs.(1))
360
RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
362
RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
364
let detype_sort = function
366
| Type u -> RType (Some u)
368
(**********************************************************************)
369
(* Main detyping function *)
371
let detype_anonymous = ref (fun loc n -> anomaly "detype: index to an anonymous variable")
372
let set_detype_anonymous f = detype_anonymous := f
374
let rec detype (isgoal:bool) avoid env t =
375
match kind_of_term (collapse_appl t) with
377
(try match lookup_name_of_rel n env with
378
| Name id -> RVar (dl, id)
379
| Anonymous -> !detype_anonymous dl n
381
let s = "_UNBOUND_REL_"^(string_of_int n)
382
in RVar (dl, id_of_string s))
384
(* Meta in constr are not user-parsable and are mapped to Evar *)
388
let _ = Global.lookup_named id in RRef (dl, VarRef id)
391
| Sort s -> RSort (dl,detype_sort s)
393
RCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
394
| Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
395
| Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
396
| LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
398
RApp (dl,detype isgoal avoid env f,
399
array_map_to_list (detype isgoal avoid env) args)
400
| Const sp -> RRef (dl, ConstRef sp)
403
Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
405
RRef (dl, IndRef ind_sp)
406
| Construct cstr_sp ->
407
RRef (dl, ConstructRef cstr_sp)
408
| Case (ci,p,c,bl) ->
409
let comp = computable p (ci.ci_pp_info.ind_nargs) in
410
detype_case comp (detype isgoal avoid env)
411
(detype_eqns isgoal avoid env ci comp)
412
is_nondep_branch avoid
413
(ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar,
414
ci.ci_cstr_nargs,ci.ci_pp_info.ind_nargs)
416
| Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef
417
| CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef
419
and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
420
let def_avoid, def_env, lfi =
422
(fun (avoid, env, l) na ->
423
let id = next_name_away na avoid in
424
(id::avoid, add_name (Name id) env, id::l))
425
(avoid, env, []) names in
426
let n = Array.length tys in
428
(fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
430
RRec(dl,RFix (Array.map (fun i -> Some i, RStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
431
Array.map (fun (bl,_,_) -> bl) v,
432
Array.map (fun (_,_,ty) -> ty) v,
433
Array.map (fun (_,bd,_) -> bd) v)
435
and detype_cofix isgoal avoid env n (names,tys,bodies) =
436
let def_avoid, def_env, lfi =
438
(fun (avoid, env, l) na ->
439
let id = next_name_away na avoid in
440
(id::avoid, add_name (Name id) env, id::l))
441
(avoid, env, []) names in
442
let ntys = Array.length tys in
444
(fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
446
RRec(dl,RCoFix n,Array.of_list (List.rev lfi),
447
Array.map (fun (bl,_,_) -> bl) v,
448
Array.map (fun (_,_,ty) -> ty) v,
449
Array.map (fun (_,bd,_) -> bd) v)
451
and share_names isgoal n l avoid env c t =
452
match kind_of_term c, kind_of_term t with
453
(* factorize even when not necessary to have better presentation *)
454
| Lambda (na,t,c), Prod (na',t',c') ->
455
let na = match (na,na') with
459
let t = detype isgoal avoid env t in
460
let id = next_name_away na avoid in
461
let avoid = id::avoid and env = add_name (Name id) env in
462
share_names isgoal (n-1) ((Name id,Explicit,None,t)::l) avoid env c c'
463
(* May occur for fix built interactively *)
464
| LetIn (na,b,t',c), _ when n > 0 ->
465
let t' = detype isgoal avoid env t' in
466
let b = detype isgoal avoid env b in
467
let id = next_name_away na avoid in
468
let avoid = id::avoid and env = add_name (Name id) env in
469
share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t
470
(* Only if built with the f/n notation or w/o let-expansion in types *)
471
| _, LetIn (_,b,_,t) when n > 0 ->
472
share_names isgoal n l avoid env c (subst1 b t)
473
(* If it is an open proof: we cheat and eta-expand *)
474
| _, Prod (na',t',c') when n > 0 ->
475
let t' = detype isgoal avoid env t' in
476
let id = next_name_away na' avoid in
477
let avoid = id::avoid and env = add_name (Name id) env in
478
let appc = mkApp (lift 1 c,[|mkRel 1|]) in
479
share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c'
480
(* If built with the f/n notation: we renounce to share names *)
482
if n>0 then warning "Detyping.detype: cannot factorize fix enough";
483
let c = detype isgoal avoid env c in
484
let t = detype isgoal avoid env t in
487
and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
489
if !Flags.raw_print or not (reverse_matching ()) then raise Exit;
490
let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
491
List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
495
(array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
497
and detype_eqn isgoal avoid env constr construct_nargs branch =
498
let make_pat x avoid env b ids =
499
if force_wildcard () & noccurn 1 b then
500
PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
502
let id = next_name_away_in_cases_pattern x avoid in
503
PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
505
let rec buildrec ids patlist avoid env n b =
508
[PatCstr(dl, constr, List.rev patlist,Anonymous)],
509
detype isgoal avoid env b)
511
match kind_of_term b with
513
let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
514
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
517
let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
518
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) b
520
| Cast (c,_,_) -> (* Oui, il y a parfois des cast *)
521
buildrec ids patlist avoid env n c
523
| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
524
termes seront construits � partir de la syntaxe Cases *)
525
(* nommage de la nouvelle variable *)
526
let new_b = applist (lift 1 b, [mkRel 1]) in
527
let pat,new_avoid,new_env,new_ids =
528
make_pat Anonymous avoid env new_b ids in
529
buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
532
buildrec [] [] avoid env construct_nargs branch
534
and detype_binder isgoal bk avoid env na ty c =
537
concrete_let_name (avoid_flag isgoal) avoid env na c
539
concrete_name (avoid_flag isgoal) avoid env na c in
540
let r = detype isgoal avoid' (add_name na' env) c in
542
| BProd -> RProd (dl, na',Explicit,detype isgoal avoid env ty, r)
543
| BLambda -> RLambda (dl, na',Explicit,detype isgoal avoid env ty, r)
544
| BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
546
let rec detype_rel_context where avoid env sign =
547
let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
548
let rec aux avoid env = function
555
if b<>None then concrete_let_name None avoid env na c
556
else concrete_name None avoid env na c in
557
let b = Option.map (detype false avoid env) b in
558
let t = detype false avoid env t in
559
(na',Explicit,b,t) :: aux avoid' (add_name na' env) rest
560
in aux avoid env (List.rev sign)
562
(**********************************************************************)
563
(* Module substitution: relies on detyping *)
565
let rec subst_cases_pattern subst pat =
568
| PatCstr (loc,((kn,i),j),cpl,n) ->
569
let kn' = subst_kn subst kn
570
and cpl' = list_smartmap (subst_cases_pattern subst) cpl in
571
if kn' == kn && cpl' == cpl then pat else
572
PatCstr (loc,((kn',i),j),cpl',n)
574
let rec subst_rawconstr subst raw =
577
let ref',t = subst_global subst ref in
578
if ref' == ref then raw else
586
let r' = subst_rawconstr subst r
587
and rl' = list_smartmap (subst_rawconstr subst) rl in
588
if r' == r && rl' == rl then raw else
591
| RLambda (loc,n,bk,r1,r2) ->
592
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
593
if r1' == r1 && r2' == r2 then raw else
594
RLambda (loc,n,bk,r1',r2')
596
| RProd (loc,n,bk,r1,r2) ->
597
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
598
if r1' == r1 && r2' == r2 then raw else
599
RProd (loc,n,bk,r1',r2')
601
| RLetIn (loc,n,r1,r2) ->
602
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
603
if r1' == r1 && r2' == r2 then raw else
604
RLetIn (loc,n,r1',r2')
606
| RCases (loc,sty,rtno,rl,branches) ->
607
let rtno' = Option.smartmap (subst_rawconstr subst) rtno
608
and rl' = list_smartmap (fun (a,x as y) ->
609
let a' = subst_rawconstr subst a in
611
let topt' = Option.smartmap
612
(fun (loc,(sp,i),x,y as t) ->
613
let sp' = subst_kn subst sp in
614
if sp == sp' then t else (loc,(sp',i),x,y)) topt in
615
if a == a' && topt == topt' then y else (a',(n,topt'))) rl
616
and branches' = list_smartmap
617
(fun (loc,idl,cpl,r as branch) ->
619
list_smartmap (subst_cases_pattern subst) cpl
620
and r' = subst_rawconstr subst r in
621
if cpl' == cpl && r' == r then branch else
625
if rtno' == rtno && rl' == rl && branches' == branches then raw else
626
RCases (loc,sty,rtno',rl',branches')
628
| RLetTuple (loc,nal,(na,po),b,c) ->
629
let po' = Option.smartmap (subst_rawconstr subst) po
630
and b' = subst_rawconstr subst b
631
and c' = subst_rawconstr subst c in
632
if po' == po && b' == b && c' == c then raw else
633
RLetTuple (loc,nal,(na,po'),b',c')
635
| RIf (loc,c,(na,po),b1,b2) ->
636
let po' = Option.smartmap (subst_rawconstr subst) po
637
and b1' = subst_rawconstr subst b1
638
and b2' = subst_rawconstr subst b2
639
and c' = subst_rawconstr subst c in
640
if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
641
RIf (loc,c',(na,po'),b1',b2')
643
| RRec (loc,fix,ida,bl,ra1,ra2) ->
644
let ra1' = array_smartmap (subst_rawconstr subst) ra1
645
and ra2' = array_smartmap (subst_rawconstr subst) ra2 in
646
let bl' = array_smartmap
647
(list_smartmap (fun (na,k,obd,ty as dcl) ->
648
let ty' = subst_rawconstr subst ty in
649
let obd' = Option.smartmap (subst_rawconstr subst) obd in
650
if ty'==ty & obd'==obd then dcl else (na,k,obd',ty')))
652
if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
653
RRec (loc,fix,ida,bl',ra1',ra2')
657
| RHole (loc,ImplicitArg (ref,i)) ->
658
let ref',_ = subst_global subst ref in
659
if ref' == ref then raw else
660
RHole (loc,InternalHole)
661
| RHole (loc, (BinderType _ | QuestionMark _ | CasesType | InternalHole |
662
TomatchTypeParameter _ | GoalEvar | ImpossibleCase)) -> raw
664
| RCast (loc,r1,k) ->
667
let r1' = subst_rawconstr subst r1 and r2' = subst_rawconstr subst r2 in
668
if r1' == r1 && r2' == r2 then raw else
669
RCast (loc,r1', CastConv (k,r2'))
671
let r1' = subst_rawconstr subst r1 in
672
if r1' == r1 then raw else RCast (loc,r1',k))
675
(* Utilities to transform kernel cases to simple pattern-matching problem *)
677
let simple_cases_matrix_of_branches ind brns brs =
678
list_map2_i (fun i n b ->
679
let nal,c = it_destRLambda_or_LetIn_names n b in
680
let mkPatVar na = PatVar (dummy_loc,na) in
681
let p = PatCstr (dummy_loc,(ind,i+1),List.map mkPatVar nal,Anonymous) in
682
let ids = map_succeed Nameops.out_name nal in
683
(dummy_loc,ids,[p],c))
686
let return_type_of_predicate ind nparams n pred =
687
let nal,p = it_destRLambda_or_LetIn_names (n+1) pred in
688
(List.hd nal, Some (dummy_loc, ind, nparams, List.tl nal)), Some p
added
removed
pretyping/detyping.ml
