1
(* -*- compile-command: "make -C ../.. bin/coqtop.byte" -*- *)
2
(************************************************************************)
3
(* v * The Coq Proof Assistant / The Coq Development Team *)
4
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
5
(* \VV/ **************************************************************)
6
(* // * This file is distributed under the terms of the *)
7
(* * GNU Lesser General Public License Version 2.1 *)
8
(************************************************************************)
10
(* $Id: subtac_cases.ml 12194 2009-06-17 16:38:09Z msozeau $ *)
34
(************************************************************************)
35
(* Pattern-matching compilation (Cases) *)
36
(************************************************************************)
38
(************************************************************************)
39
(* Configuration, errors and warnings *)
43
let mssg_may_need_inversion () =
44
str "Found a matching with no clauses on a term unknown to have an empty inductive type"
47
let make_anonymous_patvars =
48
list_tabulate (fun _ -> PatVar (dummy_loc,Anonymous))
50
(* Environment management *)
51
let push_rels vars env = List.fold_right push_rel vars env
54
List.fold_right (fun (x,d,t) e -> push_rel (x,Some d,t) e)
56
(* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
57
over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
59
let regeneralize_rel i k j = if j = i+k then k else if j < i+k then j else j
61
let rec regeneralize_index i k t = match kind_of_term t with
62
| Rel j when j = i+k -> mkRel (k+1)
63
| Rel j when j < i+k -> t
64
| Rel j when j > i+k -> t
65
| _ -> map_constr_with_binders succ (regeneralize_index i) k t
71
let mkSpecialLetInJudge j (na,(deppat,nondeppat,d,t)) =
74
| DepAlias -> mkLetIn (na,deppat,t,j.uj_val)
76
if (not (dependent (mkRel 1) j.uj_type))
77
or (* A leaf: *) isRel deppat
79
(* The body of pat is not needed to type j - see *)
80
(* insert_aliases - and both deppat and nondeppat have the *)
81
(* same type, then one can freely substitute one by the other *)
82
subst1 nondeppat j.uj_val
84
(* The body of pat is not needed to type j but its value *)
85
(* is dependent in the type of j; our choice is to *)
86
(* enforce this dependency *)
87
mkLetIn (na,deppat,t,j.uj_val));
88
uj_type = subst1 deppat j.uj_type }
90
(**********************************************************************)
91
(* Structures used in compiling pattern-matching *)
95
avoid_ids : identifier list;
100
{ patterns : cases_pattern list;
102
alias_stack : name list;
106
type matrix = equation list
108
(* 1st argument of IsInd is the original ind before extracting the summary *)
110
| IsInd of types * inductive_type
111
| NotInd of constr option * types
113
type tomatch_status =
114
| Pushed of ((constr * tomatch_type) * int list)
115
| Alias of (constr * constr * alias_constr * constr)
116
| Abstract of rel_declaration
118
type tomatch_stack = tomatch_status list
120
(* The type [predicate_signature] types the terms to match and the rhs:
122
- [PrLetIn (names,dep,pred)] types a pushed term ([Pushed]),
123
if dep<>Anonymous, the term is dependent, let n=|names|, if
124
n<>0 then the type of the pushed term is necessarily an
125
inductive with n real arguments. Otherwise, it may be
126
non inductive, or inductive without real arguments, or inductive
127
originating from a subterm in which case real args are not dependent;
128
it accounts for n+1 binders if dep or n binders if not dep
129
- [PrProd] types abstracted term ([Abstract]); it accounts for one binder
130
- [PrCcl] types the right-hand-side
131
- Aliases [Alias] have no trace in [predicate_signature]
134
type predicate_signature =
135
| PrLetIn of (name list * name) * predicate_signature
136
| PrProd of predicate_signature
139
(* We keep a constr for aliases and a cases_pattern for error message *)
143
| AliasConstructor of constructor
145
type pattern_history =
147
| MakeAlias of alias_builder * pattern_continuation
149
and pattern_continuation =
150
| Continuation of int * cases_pattern list * pattern_history
151
| Result of cases_pattern list
153
let start_history n = Continuation (n, [], Top)
155
let initial_history = function Continuation (_,[],Top) -> true | _ -> false
157
let feed_history arg = function
158
| Continuation (n, l, h) when n>=1 ->
159
Continuation (n-1, arg :: l, h)
160
| Continuation (n, _, _) ->
161
anomaly ("Bad number of expected remaining patterns: "^(string_of_int n))
163
anomaly "Exhausted pattern history"
165
(* This is for non exhaustive error message *)
167
let rec rawpattern_of_partial_history args2 = function
168
| Continuation (n, args1, h) ->
169
let args3 = make_anonymous_patvars (n - (List.length args2)) in
170
build_rawpattern (List.rev_append args1 (args2@args3)) h
173
and build_rawpattern args = function
175
| MakeAlias (AliasLeaf, rh) ->
177
rawpattern_of_partial_history [PatVar (dummy_loc, Anonymous)] rh
178
| MakeAlias (AliasConstructor pci, rh) ->
179
rawpattern_of_partial_history
180
[PatCstr (dummy_loc, pci, args, Anonymous)] rh
182
let complete_history = rawpattern_of_partial_history []
184
(* This is to build glued pattern-matching history and alias bodies *)
186
let rec simplify_history = function
187
| Continuation (0, l, Top) -> Result (List.rev l)
188
| Continuation (0, l, MakeAlias (f, rh)) ->
189
let pargs = List.rev l in
190
let pat = match f with
191
| AliasConstructor pci ->
192
PatCstr (dummy_loc,pci,pargs,Anonymous)
195
PatVar (dummy_loc, Anonymous) in
199
(* Builds a continuation expecting [n] arguments and building [ci] applied
200
to this [n] arguments *)
202
let push_history_pattern n current cont =
203
Continuation (n, [], MakeAlias (current, cont))
205
(* A pattern-matching problem has the following form:
207
env, isevars |- <pred> Cases tomatch of mat end
209
where tomatch is some sequence of "instructions" (t1 ... tn)
211
and mat is some matrix
212
(p11 ... p1n -> rhs1)
214
(pm1 ... pmn -> rhsm)
216
Terms to match: there are 3 kinds of instructions
218
- "Pushed" terms to match are typed in [env]; these are usually just
219
Rel(n) except for the initial terms given by user and typed in [env]
220
- "Abstract" instructions means an abstraction has to be inserted in the
221
current branch to build (this means a pattern has been detected dependent
222
in another one and generalisation is necessary to ensure well-typing)
223
- "Alias" instructions means an alias has to be inserted (this alias
224
is usually removed at the end, except when its type is not the
225
same as the type of the matched term from which it comes -
226
typically because the inductive types are "real" parameters)
230
They consist of a raw term to type in an environment specific to the
231
clause they belong to: the names of declarations are those of the
232
variables present in the patterns. Therefore, they come with their
233
own [rhs_env] (actually it is the same as [env] except for the names
237
type pattern_matching_problem =
239
isevars : Evd.evar_defs ref;
240
pred : predicate_signature option;
241
tomatch : tomatch_stack;
242
history : pattern_continuation;
245
casestyle: case_style;
246
typing_function: type_constraint -> env -> rawconstr -> unsafe_judgment }
248
(*--------------------------------------------------------------------------*
249
* A few functions to infer the inductive type from the patterns instead of *
250
* checking that the patterns correspond to the ind. type of the *
251
* destructurated object. Allows type inference of examples like *
252
* match n with O => true | _ => false end *
253
* match x in I with C => true | _ => false end *
254
*--------------------------------------------------------------------------*)
256
(* Computing the inductive type from the matrix of patterns *)
258
(* We use the "in I" clause to coerce the terms to match and otherwise
259
use the constructor to know in which type is the matching problem
261
Note that insertion of coercions inside nested patterns is done
262
each time the matrix is expanded *)
264
let rec find_row_ind = function
266
| PatVar _ :: l -> find_row_ind l
267
| PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
269
let inductive_template isevars env tmloc ind =
270
let arsign = get_full_arity_sign env ind in
271
let hole_source = match tmloc with
272
| Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
273
| None -> fun _ -> (dummy_loc, Evd.InternalHole) in
276
(fun (na,b,ty) (subst,evarl,n) ->
279
let ty' = substl subst ty in
280
let e = e_new_evar isevars env ~src:(hole_source n) ty' in
281
(e::subst,e::evarl,n+1)
283
(b::subst,evarl,n+1))
285
applist (mkInd ind,List.rev evarl)
288
(************************************************************************)
291
let mkExistential env ?(src=(dummy_loc,Evd.InternalHole)) isevars =
292
e_new_evar isevars env ~src:src (new_Type ())
294
let evd_comb2 f isevars x y =
295
let (evd',y) = f !isevars x y in
300
module Cases_F(Coercion : Coercion.S) : S = struct
302
let inh_coerce_to_ind isevars env ty tyi =
303
let expected_typ = inductive_template isevars env None tyi in
304
(* devrait être indifférent d'exiger leq ou pas puisque pour
305
un inductif cela doit être égal *)
306
let _ = e_cumul env isevars expected_typ ty in ()
308
let unify_tomatch_with_patterns isevars env loc typ pats =
309
match find_row_ind pats with
310
| None -> NotInd (None,typ)
311
| Some (_,(ind,_)) ->
312
inh_coerce_to_ind isevars env typ ind;
313
try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
314
with Not_found -> NotInd (None,typ)
316
let find_tomatch_tycon isevars env loc = function
317
(* Try if some 'in I ...' is present and can be used as a constraint *)
318
| Some (_,ind,_,_) -> mk_tycon (inductive_template isevars env loc ind)
319
| None -> empty_tycon
321
let coerce_row typing_fun isevars env pats (tomatch,(_,indopt)) =
322
let loc = Some (loc_of_rawconstr tomatch) in
323
let tycon = find_tomatch_tycon isevars env loc indopt in
324
let j = typing_fun tycon env tomatch in
325
let evd, j = Coercion.inh_coerce_to_base (loc_of_rawconstr tomatch) env !isevars j in
327
let typ = nf_evar (Evd.evars_of !isevars) j.uj_type in
329
try IsInd (typ,find_rectype env (Evd.evars_of !isevars) typ)
331
unify_tomatch_with_patterns isevars env loc typ pats in
334
let coerce_to_indtype typing_fun isevars env matx tomatchl =
335
let pats = List.map (fun r -> r.patterns) matx in
336
let matx' = match matrix_transpose pats with
337
| [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
339
List.map2 (coerce_row typing_fun isevars env) matx' tomatchl
343
let adjust_tomatch_to_pattern pb ((current,typ),deps) =
344
(* Ideally, we could find a common inductive type to which both the
345
term to match and the patterns coerce *)
346
(* In practice, we coerce the term to match if it is not already an
347
inductive type and it is not dependent; moreover, we use only
348
the first pattern type and forget about the others *)
349
let typ = match typ with IsInd (t,_) -> t | NotInd (_,t) -> t in
351
try IsInd (typ,find_rectype pb.env (Evd.evars_of !(pb.isevars)) typ)
352
with Not_found -> NotInd (None,typ) in
353
let tomatch = ((current,typ),deps) in
355
| NotInd (None,typ) ->
356
let tm1 = List.map (fun eqn -> List.hd eqn.patterns) pb.mat in
357
(match find_row_ind tm1 with
359
| Some (_,(ind,_)) ->
360
let indt = inductive_template pb.isevars pb.env None ind in
362
if deps = [] & isEvar typ then
363
(* Don't insert coercions if dependent; only solve evars *)
364
let _ = e_cumul pb.env pb.isevars indt typ in
367
(evd_comb2 (Coercion.inh_conv_coerce_to dummy_loc pb.env)
368
pb.isevars (make_judge current typ) (mk_tycon_type indt)).uj_val in
369
let sigma = Evd.evars_of !(pb.isevars) in
370
let typ = IsInd (indt,find_rectype pb.env sigma indt) in
371
((current,typ),deps))
374
(* extract some ind from [t], possibly coercing from constructors in [tm] *)
375
let to_mutind env isevars tm c t =
377
| Some body -> *) NotInd (c,t)
378
(* | None -> unify_tomatch_with_patterns isevars env t tm*)
380
let type_of_tomatch = function
384
let mkDeclTomatch na = function
385
| IsInd (t,_) -> (na,None,t)
386
| NotInd (c,t) -> (na,c,t)
388
let map_tomatch_type f = function
389
| IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
390
| NotInd (c,t) -> NotInd (Option.map f c, f t)
392
let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
393
let lift_tomatch_type n = liftn_tomatch_type n 1
395
let lift_tomatch n ((current,typ),info) =
396
((lift n current,lift_tomatch_type n typ),info)
398
(**********************************************************************)
399
(* Utilities on patterns *)
401
let current_pattern eqn =
402
match eqn.patterns with
404
| [] -> anomaly "Empty list of patterns"
406
let alias_of_pat = function
407
| PatVar (_,name) -> name
408
| PatCstr(_,_,_,name) -> name
410
let unalias_pat = function
411
| PatVar (c,name) as p ->
412
if name = Anonymous then p else PatVar (c,Anonymous)
413
| PatCstr(a,b,c,name) as p ->
414
if name = Anonymous then p else PatCstr (a,b,c,Anonymous)
416
let remove_current_pattern eqn =
417
match eqn.patterns with
421
alias_stack = alias_of_pat pat :: eqn.alias_stack }
422
| [] -> anomaly "Empty list of patterns"
424
let prepend_pattern tms eqn = {eqn with patterns = tms@eqn.patterns }
426
(**********************************************************************)
427
(* Well-formedness tests *)
428
(* Partial check on patterns *)
430
exception NotAdjustable
432
let rec adjust_local_defs loc = function
433
| (pat :: pats, (_,None,_) :: decls) ->
434
pat :: adjust_local_defs loc (pats,decls)
435
| (pats, (_,Some _,_) :: decls) ->
436
PatVar (loc, Anonymous) :: adjust_local_defs loc (pats,decls)
438
| _ -> raise NotAdjustable
440
let check_and_adjust_constructor env ind cstrs = function
441
| PatVar _ as pat -> pat
442
| PatCstr (loc,((_,i) as cstr),args,alias) as pat ->
443
(* Check it is constructor of the right type *)
444
let ind' = inductive_of_constructor cstr in
445
if Closure.mind_equiv env ind' ind then
446
(* Check the constructor has the right number of args *)
447
let ci = cstrs.(i-1) in
448
let nb_args_constr = ci.cs_nargs in
449
if List.length args = nb_args_constr then pat
452
let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
453
in PatCstr (loc, cstr, args', alias)
454
with NotAdjustable ->
455
error_wrong_numarg_constructor_loc loc (Global.env())
458
(* Try to insert a coercion *)
460
Coercion.inh_pattern_coerce_to loc pat ind' ind
462
error_bad_constructor_loc loc cstr ind
464
let check_all_variables typ mat =
466
(fun eqn -> match current_pattern eqn with
467
| PatVar (_,id) -> ()
468
| PatCstr (loc,cstr_sp,_,_) ->
469
error_bad_pattern_loc loc cstr_sp typ)
472
let check_unused_pattern env eqn =
473
if not !(eqn.used) then
474
raise_pattern_matching_error
475
(eqn.eqn_loc, env, UnusedClause eqn.patterns)
477
let set_used_pattern eqn = eqn.used := true
481
| [] -> errorlabstrm "build_leaf" (mssg_may_need_inversion())
483
set_used_pattern eqn;
486
(**********************************************************************)
487
(* Functions to deal with matrix factorization *)
489
let occur_in_rhs na rhs =
492
| Name id -> occur_rawconstr id rhs.it
494
let is_dep_patt eqn = function
495
| PatVar (_,name) -> occur_in_rhs name eqn.rhs
498
let dependencies_in_rhs nargs eqns =
499
if eqns = [] then list_tabulate (fun _ -> false) nargs (* Only "_" patts *)
501
let deps = List.map (fun (tms,eqn) -> List.map (is_dep_patt eqn) tms) eqns in
502
let columns = matrix_transpose deps in
503
List.map (List.exists ((=) true)) columns
505
let dependent_decl a = function
506
| (na,None,t) -> dependent a t
507
| (na,Some c,t) -> dependent a t || dependent a c
509
(* Computing the matrix of dependencies *)
511
(* We are in context d1...dn |- and [find_dependencies k 1 nextlist]
512
computes for declaration [k+1] in which of declarations in
513
[nextlist] (which corresponds to d(k+2)...dn) it depends;
514
declarations are expressed by index, e.g. in dependency list
515
[n-2;1], [1] points to [dn] and [n-2] to [d3] *)
517
let rec find_dependency_list k n = function
519
| (used,tdeps,d)::rest ->
520
let deps = find_dependency_list k (n+1) rest in
521
if used && dependent_decl (mkRel n) d
522
then list_add_set (List.length rest + 1) (list_union deps tdeps)
525
let find_dependencies is_dep_or_cstr_in_rhs d (k,nextlist) =
526
let deps = find_dependency_list k 1 nextlist in
527
if is_dep_or_cstr_in_rhs || deps <> []
528
then (k-1,(true ,deps,d)::nextlist)
529
else (k-1,(false,[] ,d)::nextlist)
531
let find_dependencies_signature deps_in_rhs typs =
532
let k = List.length deps_in_rhs in
533
let _,l = List.fold_right2 find_dependencies deps_in_rhs typs (k,[]) in
534
List.map (fun (_,deps,_) -> deps) l
538
(* A Pushed term to match has just been substituted by some
539
constructor t = (ci x1...xn) and the terms x1 ... xn have been added to
542
- all terms to match and to push (dependent on t by definition)
543
must have (Rel depth) substituted by t and Rel's>depth lifted by n
544
- all pushed terms to match (non dependent on t by definition) must
547
We start with depth=1
550
let regeneralize_index_tomatch n =
551
let rec genrec depth = function
553
| Pushed ((c,tm),l)::rest ->
554
let c = regeneralize_index n depth c in
555
let tm = map_tomatch_type (regeneralize_index n depth) tm in
556
let l = List.map (regeneralize_rel n depth) l in
557
Pushed ((c,tm),l)::(genrec depth rest)
558
| Alias (c1,c2,d,t)::rest ->
559
Alias (regeneralize_index n depth c1,c2,d,t)::(genrec depth rest)
560
| Abstract d::rest ->
561
Abstract (map_rel_declaration (regeneralize_index n depth) d)
562
::(genrec (depth+1) rest) in
565
let rec replace_term n c k t =
566
if t = mkRel (n+k) then lift k c
567
else map_constr_with_binders succ (replace_term n c) k t
569
let replace_tomatch n c =
570
let rec replrec depth = function
572
| Pushed ((b,tm),l)::rest ->
573
let b = replace_term n c depth b in
574
let tm = map_tomatch_type (replace_term n c depth) tm in
575
List.iter (fun i -> if i=n+depth then anomaly "replace_tomatch") l;
576
Pushed ((b,tm),l)::(replrec depth rest)
577
| Alias (c1,c2,d,t)::rest ->
578
Alias (replace_term n c depth c1,c2,d,t)::(replrec depth rest)
579
| Abstract d::rest ->
580
Abstract (map_rel_declaration (replace_term n c depth) d)
581
::(replrec (depth+1) rest) in
584
let liftn_rel_declaration n k = map_rel_declaration (liftn n k)
585
let substnl_rel_declaration sigma k = map_rel_declaration (substnl sigma k)
587
let rec liftn_tomatch_stack n depth = function
589
| Pushed ((c,tm),l)::rest ->
590
let c = liftn n depth c in
591
let tm = liftn_tomatch_type n depth tm in
592
let l = List.map (fun i -> if i<depth then i else i+n) l in
593
Pushed ((c,tm),l)::(liftn_tomatch_stack n depth rest)
594
| Alias (c1,c2,d,t)::rest ->
595
Alias (liftn n depth c1,liftn n depth c2,d,liftn n depth t)
596
::(liftn_tomatch_stack n depth rest)
597
| Abstract d::rest ->
598
Abstract (map_rel_declaration (liftn n depth) d)
599
::(liftn_tomatch_stack n (depth+1) rest)
602
let lift_tomatch_stack n = liftn_tomatch_stack n 1
604
(* if [current] has type [I(p1...pn u1...um)] and we consider the case
605
of constructor [ci] of type [I(p1...pn u'1...u'm)], then the
606
default variable [name] is expected to have which type?
607
Rem: [current] is [(Rel i)] except perhaps for initial terms to match *)
609
(************************************************************************)
610
(* Some heuristics to get names for variables pushed in pb environment *)
611
(* Typical requirement:
613
[match y with (S (S x)) => x | x => x end] should be compiled into
614
[match y with O => y | (S n) => match n with O => y | (S x) => x end end]
616
and [match y with (S (S n)) => n | n => n end] into
617
[match y with O => y | (S n0) => match n0 with O => y | (S n) => n end end]
619
i.e. user names should be preserved and created names should not
620
interfere with user names *)
622
let merge_name get_name obj = function
623
| Anonymous -> get_name obj
626
let merge_names get_name = List.map2 (merge_name get_name)
628
let get_names env sign eqns =
629
let names1 = list_tabulate (fun _ -> Anonymous) (List.length sign) in
630
(* If any, we prefer names used in pats, from top to bottom *)
633
(fun (pats,eqn) names -> merge_names alias_of_pat pats names)
635
(* Otherwise, we take names from the parameters of the constructor but
636
avoiding conflicts with user ids *)
638
List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
641
(fun (l,avoid) d na ->
644
(fun (na,_,t) -> Name (next_name_away (named_hd env t na) avoid))
647
(na::l,(out_name na)::avoid))
648
([],allvars) (List.rev sign) names2 in
651
(************************************************************************)
652
(* Recovering names for variables pushed to the rhs' environment *)
654
let recover_alias_names get_name = List.map2 (fun x (_,c,t) ->(get_name x,c,t))
656
let all_name sign = List.map (fun (n, b, t) -> let n = match n with Name _ -> n | Anonymous -> Name (id_of_string "Anonymous") in
659
let push_rels_eqn sign eqn =
660
let sign = all_name sign in
661
{eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env; } }
663
let push_rels_eqn_with_names sign eqn =
664
let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
665
let sign = recover_alias_names alias_of_pat pats sign in
666
push_rels_eqn sign eqn
668
let build_aliases_context env sigma names allpats pats =
669
(* pats is the list of bodies to push as an alias *)
670
(* They all are defined in env and we turn them into a sign *)
671
(* cuts in sign need to be done in allpats *)
672
let rec insert env sign1 sign2 n newallpats oldallpats = function
673
| (deppat,_,_,_)::pats, Anonymous::names when not (isRel deppat) ->
674
(* Anonymous leaves must be considered named and treated in the *)
675
(* next clause because they may occur in implicit arguments *)
676
insert env sign1 sign2
677
n newallpats (List.map List.tl oldallpats) (pats,names)
678
| (deppat,nondeppat,d,t)::pats, na::names ->
679
let nondeppat = lift n nondeppat in
680
let deppat = lift n deppat in
682
List.map2 (fun l1 l2 -> List.hd l2::l1) newallpats oldallpats in
683
let oldallpats = List.map List.tl oldallpats in
684
let decl = (na,Some deppat,t) in
685
let a = (deppat,nondeppat,d,t) in
686
insert (push_rel decl env) (decl::sign1) ((na,a)::sign2) (n+1)
687
newallpats oldallpats (pats,names)
688
| [], [] -> newallpats, sign1, sign2, env
689
| _ -> anomaly "Inconsistent alias and name lists" in
690
let allpats = List.map (fun x -> [x]) allpats
691
in insert env [] [] 0 (List.map (fun _ -> []) allpats) allpats (pats, names)
693
let insert_aliases_eqn sign eqnnames alias_rest eqn =
694
let thissign = List.map2 (fun na (_,c,t) -> (na,c,t)) eqnnames sign in
695
push_rels_eqn thissign { eqn with alias_stack = alias_rest; }
698
let insert_aliases env sigma alias eqns =
699
(* Là, y a une faiblesse, si un alias est utilisé dans un cas par *)
700
(* défaut présent mais inutile, ce qui est le cas général, l'alias *)
701
(* est introduit même s'il n'est pas utilisé dans les cas réguliers *)
702
let eqnsnames = List.map (fun eqn -> List.hd eqn.alias_stack) eqns in
703
let alias_rests = List.map (fun eqn -> List.tl eqn.alias_stack) eqns in
704
(* names2 takes the meet of all needed aliases *)
706
List.fold_right (merge_name (fun x -> x)) eqnsnames Anonymous in
707
(* Only needed aliases are kept by build_aliases_context *)
708
let eqnsnames, sign1, sign2, env =
709
build_aliases_context env sigma [names2] eqnsnames [alias] in
710
let eqns = list_map3 (insert_aliases_eqn sign1) eqnsnames alias_rests eqns in
713
(**********************************************************************)
714
(* Functions to deal with elimination predicate *)
717
let noccur_between_without_evar n m term =
718
let rec occur_rec n c = match kind_of_term c with
719
| Rel p -> if n<=p && p<n+m then raise Occur
721
| _ -> iter_constr_with_binders succ occur_rec n c
723
try occur_rec n term; true with Occur -> false
725
(* Inferring the predicate *)
726
let prepare_unif_pb typ cs =
727
let n = List.length (assums_of_rel_context cs.cs_args) in
729
(* We may need to invert ci if its parameters occur in typ *)
731
if noccur_between_without_evar 1 n typ then lift (-n) typ
733
error "Unable to infer return clause of this pattern-matching problem" in
734
let args = extended_rel_list (-n) cs.cs_args in
735
let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
737
(* This is the problem: finding P s.t. cs_args |- (P realargs ci) = typ' *)
738
(Array.map (lift (-n)) cs.cs_concl_realargs, ci, typ')
741
(* Infering the predicate *)
743
The problem to solve is the following:
745
We match Gamma |- t : I(u01..u0q) against the following constructors:
747
Gamma, x11...x1p1 |- C1(x11..x1p1) : I(u11..u1q)
749
Gamma, xn1...xnpn |- Cn(xn1..xnp1) : I(un1..unq)
751
Assume the types in the branches are the following
753
Gamma, x11...x1p1 |- branch1 : T1
755
Gamma, xn1...xnpn |- branchn : Tn
757
Assume the type of the global case expression is Gamma |- T
759
The predicate has the form phi = [y1..yq][z:I(y1..yq)]? and must satisfy
760
the following n+1 equations:
762
Gamma, x11...x1p1 |- (phi u11..u1q (C1 x11..x1p1)) = T1
764
Gamma, xn1...xnpn |- (phi un1..unq (Cn xn1..xnpn)) = Tn
765
Gamma |- (phi u01..u0q t) = T
769
- Clearly, if xij occurs in Ti, then, a "match z with (Ci xi1..xipi) => ..."
770
should be inserted somewhere in Ti.
772
- If T is undefined, an easy solution is to insert a "match z with (Ci
773
xi1..xipi) => ..." in front of each Ti
775
- Otherwise, T1..Tn and T must be step by step unified, if some of them
776
diverge, then try to replace the diverging subterm by one of y1..yq or z.
778
- The main problem is what to do when an existential variables is encountered
780
let prepare_unif_pb typ cs =
781
let n = cs.cs_nargs in
782
let _,p = decompose_prod_n n typ in
783
let ci = build_dependent_constructor cs in
784
(* This is the problem: finding P s.t. cs_args |- (P realargs ci) = p *)
785
(n, cs.cs_concl_realargs, ci, p)
787
let eq_operator_lift k (n,n') = function
788
| OpRel p, OpRel p' when p > k & p' > k ->
789
if p < k+n or p' < k+n' then false else p - n = p' - n'
790
| op, op' -> op = op'
792
let rec transpose_args n =
795
(Array.map (fun l -> List.hd l) lv)::
796
(transpose_args (m-1) (Array.init (fun l -> List.tl l)))
798
let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k
800
let reloc_operator (k,n) = function OpRel p when p > k ->
801
let rec unify_clauses k pv =
802
let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (Evd.evars_of isevars)) p) pv in
803
let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in
804
if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv'
806
let argvl = transpose_args (List.length args1) pv' in
807
let k' = shift_operator k op1 in
808
let argl = List.map (unify_clauses k') argvl in
809
gather_constr (reloc_operator (k,n1) op1) argl
812
let abstract_conclusion typ cs =
813
let n = List.length (assums_of_rel_context cs.cs_args) in
814
let (sign,p) = decompose_prod_n n typ in
817
let infer_predicate loc env isevars typs cstrs indf =
818
(* Il faudra substituer les isevars a un certain moment *)
819
if Array.length cstrs = 0 then (* "TODO4-3" *)
820
error "Inference of annotation for empty inductive types not implemented"
822
(* Empiric normalization: p may depend in a irrelevant way on args of the*)
823
(* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
825
Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
827
let eqns = array_map2 prepare_unif_pb typs cstrs in
828
(* First strategy: no dependencies at all *)
830
let (mis,_) = dest_ind_family indf in
831
let (cclargs,_,typn) = eqns.(mis_nconstr mis -1) in
833
let (sign,_) = get_arity env indf in
835
if array_exists is_Type typs then
836
(* Heuristic to avoid comparison between non-variables algebric univs*)
839
mkExistential env ~src:(loc, Evd.CasesType) isevars
841
if array_for_all (fun (_,_,typ) -> e_cumul env isevars typ mtyp) eqns
843
(* Non dependent case -> turn it into a (dummy) dependent one *)
844
let sign = (Anonymous,None,build_dependent_inductive env indf)::sign in
845
let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
846
(true,pred) (* true = dependent -- par défaut *)
849
let s = get_sort_of env (evars_of isevars) typs.(0) in
850
let predpred = it_mkLambda_or_LetIn (mkSort s) sign in
851
let caseinfo = make_default_case_info mis in
852
let brs = array_map2 abstract_conclusion typs cstrs in
853
let predbody = mkCase (caseinfo, (nf_betaiota predpred), mkRel 1, brs) in
854
let pred = it_mkLambda_or_LetIn (lift (List.length sign) mtyp) sign in
857
(* We skip parameters *)
861
applist (mkConstruct cs.cs_cstr, extended_rel_list 0 cs.cs_args))
863
let ct = array_map2 (fun ci (_,_,t) -> (ci,t)) cis eqns in
864
raise_pattern_matching_error (loc,env, CannotInferPredicate ct)
869
(* Propagation of user-provided predicate through compilation steps *)
871
let rec map_predicate f k = function
872
| PrCcl ccl -> PrCcl (f k ccl)
874
PrProd (map_predicate f (k+1) pred)
875
| PrLetIn ((names,dep as tm),pred) ->
876
let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
877
PrLetIn (tm, map_predicate f (k+k') pred)
879
let rec noccurn_predicate k = function
880
| PrCcl ccl -> noccurn k ccl
881
| PrProd pred -> noccurn_predicate (k+1) pred
882
| PrLetIn ((names,dep),pred) ->
883
let k' = List.length names + (if dep<>Anonymous then 1 else 0) in
884
noccurn_predicate (k+k') pred
886
let liftn_predicate n = map_predicate (liftn n)
888
let lift_predicate n = liftn_predicate n 1
890
let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0
892
let substnl_predicate sigma = map_predicate (substnl sigma)
894
(* This is parallel bindings *)
895
let subst_predicate (args,copt) pred =
896
let sigma = match copt with
897
| None -> List.rev args
898
| Some c -> c::(List.rev args) in
899
substnl_predicate sigma 0 pred
901
let specialize_predicate_var (cur,typ) = function
902
| PrProd _ | PrCcl _ ->
903
anomaly "specialize_predicate_var: a pattern-variable must be pushed"
904
| PrLetIn (([],dep),pred) ->
905
subst_predicate ([],if dep<>Anonymous then Some cur else None) pred
906
| PrLetIn ((_,dep),pred) ->
908
| IsInd (_,IndType (_,realargs)) ->
909
subst_predicate (realargs,if dep<>Anonymous then Some cur else None) pred
910
| _ -> anomaly "specialize_predicate_var")
912
let ungeneralize_predicate = function
913
| PrLetIn _ | PrCcl _ -> anomaly "ungeneralize_predicate: expects a product"
914
| PrProd pred -> pred
916
(*****************************************************************************)
917
(* We have pred = [X:=realargs;x:=c]P typed in Gamma1, x:I(realargs), Gamma2 *)
918
(* and we want to abstract P over y:t(x) typed in the same context to get *)
920
(* pred' = [X:=realargs;x':=c](y':t(x'))P[y:=y'] *)
922
(* We first need to lift t(x) s.t. it is typed in Gamma, X:=rargs, x' *)
923
(* then we have to replace x by x' in t(x) and y by y' in P *)
924
(*****************************************************************************)
925
let generalize_predicate ny d = function
926
| PrLetIn ((names,dep as tm),pred) ->
927
if dep=Anonymous then anomaly "Undetected dependency";
928
let p = List.length names + 1 in
929
let pred = lift_predicate 1 pred in
930
let pred = regeneralize_index_predicate (ny+p+1) pred in
931
PrLetIn (tm, PrProd pred)
932
| PrProd _ | PrCcl _ ->
933
anomaly "generalize_predicate: expects a non trivial pattern"
935
let rec extract_predicate l = function
936
| pred, Alias (deppat,nondeppat,_,_)::tms ->
937
let tms' = match kind_of_term nondeppat with
938
| Rel i -> replace_tomatch i deppat tms
939
| _ -> (* initial terms are not dependent *) tms in
940
extract_predicate l (pred,tms')
941
| PrProd pred, Abstract d'::tms ->
942
let d' = map_rel_declaration (lift (List.length l)) d' in
943
substl l (mkProd_or_LetIn d' (extract_predicate [] (pred,tms)))
944
| PrLetIn (([],dep),pred), Pushed ((cur,_),_)::tms ->
945
extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
946
| PrLetIn ((_,dep),pred), Pushed ((cur,IsInd (_,(IndType(_,realargs)))),_)::tms ->
947
let l = List.rev realargs@l in
948
extract_predicate (if dep<>Anonymous then cur::l else l) (pred,tms)
951
| _ -> anomaly"extract_predicate: predicate inconsistent with terms to match"
953
let abstract_predicate env sigma indf cur tms = function
954
| (PrProd _ | PrCcl _) -> anomaly "abstract_predicate: must be some LetIn"
955
| PrLetIn ((names,dep),pred) ->
956
let sign = make_arity_signature env true indf in
957
(* n is the number of real args + 1 *)
958
let n = List.length sign in
959
let tms = lift_tomatch_stack n tms in
961
match kind_of_term cur with
962
| Rel i -> regeneralize_index_tomatch (i+n) tms
963
| _ -> (* Initial case *) tms in
964
(* Depending on whether the predicate is dependent or not, and has real
965
args or not, we lift it to make room for [sign] *)
966
(* Even if not intrinsically dep, we move the predicate into a dep one *)
968
if names = [] & n <> 1 then
969
(* Real args were not considered *)
970
(if dep<>Anonymous then
971
((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1)
975
(* Real args are OK *)
976
(List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,
977
if dep<>Anonymous then 0 else 1) in
978
let pred = lift_predicate k pred in
979
let pred = extract_predicate [] (pred,tms) in
980
(true, it_mkLambda_or_LetIn_name env pred sign)
982
let rec known_dependent = function
984
| Some (PrLetIn ((_,dep),_)) -> dep<>Anonymous
985
| Some (PrCcl _) -> false
987
anomaly "known_dependent: can only be used when patterns remain"
989
(* [expand_arg] is used by [specialize_predicate]
990
it replaces gamma, x1...xn, x1...xk |- pred
991
by gamma, x1...xn, x1...xk-1 |- [X=realargs,xk=xk]pred (if dep) or
992
by gamma, x1...xn, x1...xk-1 |- [X=realargs]pred (if not dep) *)
994
let expand_arg n alreadydep (na,t) deps (k,pred) =
995
(* current can occur in pred even if the original problem is not dependent *)
997
if alreadydep<>Anonymous then alreadydep
998
else if deps = [] && noccurn_predicate 1 pred then Anonymous
999
else Name (id_of_string "x") in
1000
let pred = if dep<>Anonymous then pred else lift_predicate (-1) pred in
1001
(* There is no dependency in realargs for subpattern *)
1002
(k-1, PrLetIn (([],dep), pred))
1005
(*****************************************************************************)
1006
(* pred = [X:=realargs;x:=c]P types the following problem: *)
1008
(* Gamma |- match Pushed(c:I(realargs)) rest with...end: pred *)
1010
(* where the branch with constructor Ci:(x1:T1)...(xn:Tn)->I(realargsi) *)
1011
(* is considered. Assume each Ti is some Ii(argsi). *)
1012
(* We let e=Ci(x1,...,xn) and replace pred by *)
1014
(* pred' = [X1:=rargs1,x1:=x1']...[Xn:=rargsn,xn:=xn'](P[X:=realargsi;x:=e]) *)
1016
(* s.t Gamma,x1'..xn' |- match Pushed(x1')..Pushed(xn') rest with..end :pred'*)
1018
(*****************************************************************************)
1019
let specialize_predicate tomatchs deps cs = function
1020
| (PrProd _ | PrCcl _) ->
1021
anomaly "specialize_predicate: a matched pattern must be pushed"
1022
| PrLetIn ((names,isdep),pred) ->
1023
(* Assume some gamma st: gamma, (X,x:=realargs,copt) |- pred *)
1024
let nrealargs = List.length names in
1025
let k = nrealargs + (if isdep<>Anonymous then 1 else 0) in
1026
(* We adjust pred st: gamma, x1..xn, (X,x:=realargs,copt) |- pred' *)
1027
let n = cs.cs_nargs in
1028
let pred' = liftn_predicate n (k+1) pred in
1029
let argsi = if nrealargs <> 0 then Array.to_list cs.cs_concl_realargs else [] in
1030
let copti = if isdep<>Anonymous then Some (build_dependent_constructor cs) else None in
1031
(* The substituends argsi, copti are all defined in gamma, x1...xn *)
1032
(* We need _parallel_ bindings to get gamma, x1...xn |- pred'' *)
1033
let pred'' = subst_predicate (argsi, copti) pred' in
1034
(* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *)
1035
let pred''' = liftn_predicate n (n+1) pred'' in
1036
(* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
1037
snd (List.fold_right2 (expand_arg n isdep) tomatchs deps (n,pred'''))
1039
let find_predicate loc env isevars p typs cstrs current
1040
(IndType (indf,realargs)) tms =
1043
| Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
1044
| None -> infer_predicate loc env isevars typs cstrs indf in
1045
let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
1047
(pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
1050
(pred, typ, new_Type ())
1052
(************************************************************************)
1053
(* Sorting equations by constructor *)
1055
type inversion_problem =
1056
(* the discriminating arg in some Ind and its order in Ind *)
1057
| Incompatible of int * (int * int)
1058
| Constraints of (int * constr) list
1060
let solve_constraints constr_info indt =
1064
let rec irrefutable env = function
1065
| PatVar (_,name) -> true
1066
| PatCstr (_,cstr,args,_) ->
1067
let ind = inductive_of_constructor cstr in
1068
let (_,mip) = Inductive.lookup_mind_specif env ind in
1069
let one_constr = Array.length mip.mind_user_lc = 1 in
1070
one_constr & List.for_all (irrefutable env) args
1072
let first_clause_irrefutable env = function
1073
| eqn::mat -> List.for_all (irrefutable env) eqn.patterns
1076
let group_equations pb ind current cstrs mat =
1078
if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
1079
let brs = Array.create (Array.length cstrs) [] in
1080
let only_default = ref true in
1082
List.fold_right (* To be sure it's from bottom to top *)
1084
let rest = remove_current_pattern eqn in
1085
let pat = current_pattern eqn in
1086
match check_and_adjust_constructor pb.env ind cstrs pat with
1087
| PatVar (_,name) ->
1088
(* This is a default clause that we expand *)
1089
for i=1 to Array.length cstrs do
1090
let n = cstrs.(i-1).cs_nargs in
1091
let args = make_anonymous_patvars n in
1092
brs.(i-1) <- (args, rest) :: brs.(i-1)
1094
| PatCstr (loc,((_,i)),args,_) ->
1095
(* This is a regular clause *)
1096
only_default := false;
1097
brs.(i-1) <- (args,rest) :: brs.(i-1)) mat () in
1100
(************************************************************************)
1101
(* Here starts the pattern-matching compilation algorithm *)
1103
(* Abstracting over dependent subterms to match *)
1104
let rec generalize_problem pb = function
1107
let d = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
1108
let pb' = generalize_problem pb l in
1109
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
1110
let tomatch = regeneralize_index_tomatch (i+1) tomatch in
1112
tomatch = Abstract d :: tomatch;
1113
pred = Option.map (generalize_predicate i d) pb'.pred }
1115
(* No more patterns: typing the right-hand-side of equations *)
1117
let rhs = extract_rhs pb in
1118
let tycon = match pb.pred with
1119
| None -> anomaly "Predicate not found"
1120
| Some (PrCcl typ) -> mk_tycon typ
1121
| Some _ -> anomaly "not all parameters of pred have been consumed" in
1122
pb.typing_function tycon rhs.rhs_env rhs.it
1124
(* Building the sub-problem when all patterns are variables *)
1125
let shift_problem (current,t) pb =
1127
tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
1128
pred = Option.map (specialize_predicate_var (current,t)) pb.pred;
1129
history = push_history_pattern 0 AliasLeaf pb.history;
1130
mat = List.map remove_current_pattern pb.mat }
1132
(* Building the sub-pattern-matching problem for a given branch *)
1133
let build_branch current deps pb eqns const_info =
1134
(* We remember that we descend through a constructor *)
1136
if Array.length const_info.cs_concl_realargs = 0
1137
& not (known_dependent pb.pred) & deps = []
1144
push_history_pattern const_info.cs_nargs
1145
(AliasConstructor const_info.cs_cstr)
1148
(* We find matching clauses *)
1149
let cs_args = (*assums_of_rel_context*) const_info.cs_args in
1150
let names = get_names pb.env cs_args eqns in
1151
let submat = List.map (fun (tms,eqn) -> prepend_pattern tms eqn) eqns in
1153
raise_pattern_matching_error
1154
(dummy_loc, pb.env, NonExhaustive (complete_history history));
1155
let typs = List.map2 (fun (_,c,t) na -> (na,c,t)) cs_args names in
1158
(fun (na,c,t as d) (env,typs,tms) ->
1159
let tm1 = List.map List.hd tms in
1160
let tms = List.map List.tl tms in
1161
(push_rel d env, (na,to_mutind env pb.isevars tm1 c t)::typs,tms))
1162
typs (pb.env,[],List.map fst eqns) in
1165
find_dependencies_signature
1166
(dependencies_in_rhs const_info.cs_nargs eqns) (List.rev typs) in
1168
(* The dependent term to subst in the types of the remaining UnPushed
1169
terms is relative to the current context enriched by topushs *)
1170
let ci = build_dependent_constructor const_info in
1172
(* We replace [(mkRel 1)] by its expansion [ci] *)
1173
(* and context "Gamma = Gamma1, current, Gamma2" by "Gamma;typs;curalias" *)
1174
(* This is done in two steps : first from "Gamma |- tms" *)
1175
(* into "Gamma; typs; curalias |- tms" *)
1176
let tomatch = lift_tomatch_stack const_info.cs_nargs pb.tomatch in
1180
(fun i (na,t) deps -> Pushed ((mkRel i, lift_tomatch_type i t), deps))
1181
1 typs' (List.rev dep_sign) in
1183
let sign = List.map (fun (na,t) -> mkDeclTomatch na t) typs' in
1186
applist (mkInd (inductive_of_constructor const_info.cs_cstr),
1187
List.map (lift const_info.cs_nargs) const_info.cs_params),
1188
const_info.cs_concl_realargs) in
1190
let cur_alias = lift (List.length sign) current in
1191
let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in
1192
let env' = push_rels sign pb.env in
1193
let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in
1197
tomatch = List.rev_append currents tomatch;
1200
mat = List.map (push_rels_eqn_with_names sign) submat }
1202
(**********************************************************************
1205
pb = { env, subst, tomatch, mat, ...}
1206
tomatch = list of Pushed (c:T) or Abstract (na:T) or Alias (c:T)
1208
"Pushed" terms and types are relative to env
1209
"Abstract" types are relative to env enriched by the previous terms to match
1213
(**********************************************************************)
1214
(* Main compiling descent *)
1215
let rec compile pb =
1216
match pb.tomatch with
1217
| (Pushed cur)::rest -> match_current { pb with tomatch = rest } cur
1218
| (Alias x)::rest -> compile_alias pb x rest
1219
| (Abstract d)::rest -> compile_generalization pb d rest
1220
| [] -> build_leaf pb
1222
and match_current pb tomatch =
1223
let ((current,typ as ct),deps) = adjust_tomatch_to_pattern pb tomatch in
1226
check_all_variables typ pb.mat;
1227
compile (shift_problem ct pb)
1228
| IsInd (_,(IndType(indf,realargs) as indt)) ->
1229
let mind,_ = dest_ind_family indf in
1230
let cstrs = get_constructors pb.env indf in
1231
let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
1232
if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt then
1233
compile (shift_problem ct pb)
1235
let _constraints = Array.map (solve_constraints indt) cstrs in
1237
(* We generalize over terms depending on current term to match *)
1238
let pb = generalize_problem pb deps in
1240
(* We compile branches *)
1241
let brs = array_map2 (compile_branch current deps pb) eqns cstrs in
1243
(* We build the (elementary) case analysis *)
1244
let brvals = Array.map (fun (v,_) -> v) brs in
1245
let brtyps = Array.map (fun (_,t) -> t) brs in
1247
find_predicate pb.caseloc pb.env pb.isevars
1248
pb.pred brtyps cstrs current indt pb.tomatch in
1249
let ci = make_case_info pb.env mind pb.casestyle in
1250
let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
1251
let inst = List.map mkRel deps in
1252
{ uj_val = applist (case, inst);
1253
uj_type = substl inst typ }
1255
and compile_branch current deps pb eqn cstr =
1256
let sign, pb = build_branch current deps pb eqn cstr in
1257
let j = compile pb in
1258
(it_mkLambda_or_LetIn j.uj_val sign, j.uj_type)
1260
and compile_generalization pb d rest =
1263
env = push_rel d pb.env;
1265
pred = Option.map ungeneralize_predicate pb.pred;
1266
mat = List.map (push_rels_eqn [d]) pb.mat } in
1267
let j = compile pb in
1268
{ uj_val = mkLambda_or_LetIn d j.uj_val;
1269
uj_type = mkProd_or_LetIn d j.uj_type }
1271
and compile_alias pb (deppat,nondeppat,d,t) rest =
1272
let history = simplify_history pb.history in
1273
let sign, newenv, mat =
1274
insert_aliases pb.env (Evd.evars_of !(pb.isevars)) (deppat,nondeppat,d,t) pb.mat in
1275
let n = List.length sign in
1277
(* We had Gamma1; x:current; Gamma2 |- tomatch(x) and we rebind x to get *)
1278
(* Gamma1; x:current; Gamma2; typs; x':=curalias |- tomatch(x') *)
1279
let tomatch = lift_tomatch_stack n rest in
1280
let tomatch = match kind_of_term nondeppat with
1282
if n = 1 then regeneralize_index_tomatch (i+n) tomatch
1283
else replace_tomatch i deppat tomatch
1284
| _ -> (* initial terms are not dependent *) tomatch in
1290
pred = Option.map (lift_predicate n) pb.pred;
1293
let j = compile pb in
1294
List.fold_left mkSpecialLetInJudge j sign
1296
(* pour les alias des initiaux, enrichir les env de ce qu'il faut et
1297
substituer après par les initiaux *)
1299
(**************************************************************************)
1300
(* Preparation of the pattern-matching problem *)
1302
(* builds the matrix of equations testing that each eqn has n patterns
1303
* and linearizing the _ patterns.
1304
* Syntactic correctness has already been done in astterm *)
1305
let matx_of_eqns env eqns =
1306
let build_eqn (loc,ids,lpat,rhs) =
1309
avoid_ids = ids@(ids_of_named_context (named_context env));
1317
in List.map build_eqn eqns
1319
(************************************************************************)
1320
(* preparing the elimination predicate if any *)
1322
let oldprepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
1323
let cook (n, l, env, signs) = function
1324
| c,IsInd (_,IndType(indf,realargs)) ->
1325
let indf' = lift_inductive_family n indf in
1326
let sign = make_arity_signature env dep indf' in
1327
let p = List.length realargs in
1329
(n + p + 1, c::(List.rev realargs)@l, push_rels sign env,sign::signs)
1331
(n + p, (List.rev realargs)@l, push_rels sign env,sign::signs)
1333
(n, l, env, []::signs) in
1334
let n, allargs, env, signs = List.fold_left cook (0, [], env, []) tomatchs in
1335
let names = List.rev (List.map (List.map pi1) signs) in
1337
List.map (fun c -> lift n (nf_betadeltaiota env (Evd.evars_of !isevars) c)) allargs in
1338
let rec build_skeleton env c =
1339
(* Don't put into normal form, it has effects on the synthesis of evars *)
1340
(* let c = whd_betadeltaiota env (evars_of isevars) c in *)
1341
(* We turn all subterms possibly dependent into an evar with maximum ctxt*)
1342
if isEvar c or List.exists (eq_constr c) allargs then
1343
e_new_evar isevars env ~src:(loc, Evd.CasesType)
1344
(Retyping.get_type_of env (Evd.evars_of !isevars) c)
1346
map_constr_with_full_binders push_rel build_skeleton env c
1348
names, build_skeleton env (lift n c)
1350
(* Here, [pred] is assumed to be in the context built from all *)
1351
(* realargs and terms to match *)
1352
let build_initial_predicate isdep allnames pred =
1353
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
1354
let rec buildrec n pred = function
1357
let names' = if isdep then List.tl names else names in
1358
let n' = n + List.length names' in
1359
let pred, p, user_p =
1361
if dependent (mkRel (nar-n')) pred then pred, 1, 1
1362
else liftn (-1) (nar-n') pred, 0, 1
1366
let na = List.hd names in
1367
if na = Anonymous then
1368
(* peut arriver en raison des evars *)
1369
Name (id_of_string "x") (*Hum*)
1372
PrLetIn ((names',na), buildrec (n'+user_p) pred lnames)
1373
in buildrec 0 pred allnames
1375
let extract_arity_signature env0 tomatchl tmsign =
1376
let get_one_sign n tm (na,t) =
1378
| NotInd (bo,typ) ->
1380
| None -> [na,Option.map (lift n) bo,lift n typ]
1381
| Some (loc,_,_,_) ->
1382
user_err_loc (loc,"",
1383
str "Unexpected type annotation for a term of non inductive type"))
1384
| IsInd (_,IndType(indf,realargs)) ->
1385
let indf' = lift_inductive_family n indf in
1386
let (ind,params) = dest_ind_family indf' in
1387
let nrealargs = List.length realargs in
1390
| Some (loc,ind',nparams,realnal) ->
1392
user_err_loc (loc,"",str "Wrong inductive type");
1393
if List.length params <> nparams
1394
or nrealargs <> List.length realnal then
1395
anomaly "Ill-formed 'in' clause in cases";
1397
| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
1398
let arsign = fst (get_arity env0 indf') in
1399
(na,None,build_dependent_inductive env0 indf')
1400
::(List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign) in
1401
let rec buildrec n = function
1403
| (_,tm)::ltm, x::tmsign ->
1404
let l = get_one_sign n tm x in
1405
l :: buildrec (n + List.length l) (ltm,tmsign)
1407
in List.rev (buildrec 0 (tomatchl,tmsign))
1409
let extract_arity_signatures env0 tomatchl tmsign =
1410
let get_one_sign tm (na,t) =
1412
| NotInd (bo,typ) ->
1414
| None -> [na,bo,typ]
1415
| Some (loc,_,_,_) ->
1416
user_err_loc (loc,"",
1417
str "Unexpected type annotation for a term of non inductive type"))
1418
| IsInd (_,IndType(indf,realargs)) ->
1419
let (ind,params) = dest_ind_family indf in
1420
let nrealargs = List.length realargs in
1423
| Some (loc,ind',nparams,realnal) ->
1425
user_err_loc (loc,"",str "Wrong inductive type");
1426
if List.length params <> nparams
1427
or nrealargs <> List.length realnal then
1428
anomaly "Ill-formed 'in' clause in cases";
1430
| None -> list_tabulate (fun _ -> Anonymous) nrealargs in
1431
let arsign = fst (get_arity env0 indf) in
1432
(na,None,build_dependent_inductive env0 indf)
1433
::(try List.map2 (fun x (_,c,t) ->(x,c,t)) realnal arsign with _ -> assert false) in
1434
let rec buildrec = function
1436
| (_,tm)::ltm, x::tmsign ->
1437
let l = get_one_sign tm x in
1438
l :: buildrec (ltm,tmsign)
1440
in List.rev (buildrec (tomatchl,tmsign))
1442
let inh_conv_coerce_to_tycon loc env isevars j tycon =
1445
let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
1450
let out_ind = function IsInd (_, IndType(x, y)) -> (x, y) | _ -> assert(false)
1452
let string_of_name name =
1454
| Anonymous -> "anonymous"
1455
| Name n -> string_of_id n
1457
let id_of_name n = id_of_string (string_of_name n)
1459
let make_prime_id name =
1460
let str = string_of_name name in
1461
id_of_string str, id_of_string (str ^ "'")
1463
let prime avoid name =
1464
let previd, id = make_prime_id name in
1465
previd, next_ident_away_from id avoid
1467
let make_prime avoid prevname =
1468
let previd, id = prime !avoid prevname in
1469
avoid := id :: !avoid;
1472
let eq_id avoid id =
1473
let hid = id_of_string ("Heq_" ^ string_of_id id) in
1474
let hid' = next_ident_away_from hid avoid in
1477
let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
1478
let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
1480
let hole = RHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
1482
let context_of_arsign l =
1483
let (x, _) = List.fold_right
1485
(lift_rel_context n c @ x, List.length c + n))
1489
let constr_of_pat env isevars arsign pat avoid =
1490
let rec typ env (ty, realargs) pat avoid =
1492
| PatVar (l,name) ->
1493
let name, avoid = match name with
1494
Name n -> name, avoid
1496
let previd, id = prime avoid (Name (id_of_string "wildcard")) in
1497
Name id, id :: avoid
1499
PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
1500
| PatCstr (l,((_, i) as cstr),args,alias) ->
1501
let cind = inductive_of_constructor cstr in
1502
let IndType (indf, _) = find_rectype env (Evd.evars_of !isevars) (lift (-(List.length realargs)) ty) in
1503
let ind, params = dest_ind_family indf in
1504
if ind <> cind then error_bad_constructor_loc l cstr ind;
1505
let cstrs = get_constructors env indf in
1506
let ci = cstrs.(i-1) in
1507
let nb_args_constr = ci.cs_nargs in
1508
assert(nb_args_constr = List.length args);
1509
let patargs, args, sign, env, n, m, avoid =
1511
(fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid) ->
1512
let pat', sign', arg', typ', argtypargs, n', avoid =
1513
typ env (lift (n - m) t, []) ua avoid
1515
let args' = arg' :: List.map (lift n') args in
1516
let env' = push_rels sign' env in
1517
(pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
1518
ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
1520
let args = List.rev args in
1521
let patargs = List.rev patargs in
1522
let pat' = PatCstr (l, cstr, patargs, alias) in
1523
let cstr = mkConstruct ci.cs_cstr in
1524
let app = applistc cstr (List.map (lift (List.length sign)) params) in
1525
let app = applistc app args in
1526
let apptype = Retyping.get_type_of env (Evd.evars_of !isevars) app in
1527
let IndType (indf, realargs) = find_rectype env (Evd.evars_of !isevars) apptype in
1530
pat', sign, app, apptype, realargs, n, avoid
1532
let sign = (alias, None, lift m ty) :: sign in
1533
let avoid = id :: avoid in
1534
let sign, i, avoid =
1536
let env = push_rels sign env in
1537
isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars;
1538
let eq_t = mk_eq (lift (succ m) ty)
1539
(mkRel 1) (* alias *)
1540
(lift 1 app) (* aliased term *)
1542
let neq = eq_id avoid id in
1543
(Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
1544
with Reduction.NotConvertible -> sign, 1, avoid
1546
(* Mark the equality as a hole *)
1547
pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
1549
let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in
1550
pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid
1553
(* shadows functional version *)
1554
let eq_id avoid id =
1555
let hid = id_of_string ("Heq_" ^ string_of_id id) in
1556
let hid' = next_ident_away_from hid !avoid in
1557
avoid := hid' :: !avoid;
1560
let rels_of_patsign =
1561
List.map (fun ((na, b, t) as x) ->
1563
| Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
1566
let vars_of_ctx ctx =
1568
List.fold_right (fun (na, b, t) (prev, vars) ->
1570
| Some t' when kind_of_term t' = Rel 0 ->
1573
(RRef (dummy_loc, Lazy.force refl_ref)), [hole; RVar (dummy_loc, prev)])) :: vars
1576
Anonymous -> raise (Invalid_argument "vars_of_ctx")
1577
| Name n -> n, RVar (dummy_loc, n) :: vars)
1578
ctx (id_of_string "vars_of_ctx_error", [])
1581
let rec is_included x y =
1583
| PatVar _, _ -> true
1584
| _, PatVar _ -> true
1585
| PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias') ->
1586
if i = i' then List.for_all2 is_included args args'
1589
(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its
1590
full signature. However prevpatterns are in the original one signature per pattern form.
1592
let build_ineqs prevpatterns pats liftsign =
1593
let _tomatchs = List.length pats in
1597
let acc = List.fold_left2
1598
(* ppat is the pattern we are discriminating against, curpat is the current one. *)
1599
(fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat)
1600
(curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
1603
| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
1604
if is_included curpat ppat then
1605
(* Length of previous pattern's signature *)
1606
let lens = List.length ppat_sign in
1607
(* Accumulated length of previous pattern's signatures *)
1608
let len' = lens + len in
1610
((* Jump over previous prevpat signs *)
1611
lift_rel_context len ppat_sign @ sign,
1613
succ n, (* nth pattern *)
1614
mkApp (Lazy.force eq_ind,
1615
[| lift (len' + liftsign) curpat_ty;
1616
liftn (len + liftsign) (succ lens) ppat_c ;
1617
lift len' curpat_c |]) ::
1618
List.map (lift lens (* Jump over this prevpat signature *)) c)
1621
(Some ([], 0, 0, [])) eqnpats pats
1624
| Some (sign, len, _, c') ->
1625
let conj = it_mkProd_or_LetIn (mk_not (mk_conj c'))
1626
(lift_rel_context liftsign sign)
1630
in match diffs with [] -> None
1631
| _ -> Some (mk_conj diffs)
1633
let subst_rel_context k ctx subst =
1636
(fun (n, b, t) (k, acc) ->
1637
(succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
1641
let lift_rel_contextn n k sign =
1642
let rec liftrec k = function
1644
(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
1647
liftrec (rel_context_length sign + k) sign
1649
let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
1653
(fun (branches, eqns, prevpatterns) eqn ->
1654
let _, newpatterns, pats =
1656
(fun (idents, newpatterns, pats) pat arsign ->
1657
let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
1658
(idents, pat' :: newpatterns, cpat :: pats))
1659
([], [], []) eqn.patterns sign
1661
let newpatterns = List.rev newpatterns and opats = List.rev pats in
1662
let rhs_rels, pats, signlen =
1664
(fun (renv, pats, n) (sign,c, (s, args), p) ->
1665
(* Recombine signatures and terms of all of the row's patterns *)
1666
let sign' = lift_rel_context n sign in
1667
let len = List.length sign' in
1669
(* lift to get outside of previous pattern's signatures. *)
1670
(sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
1672
([], [], 0) opats in
1673
let pats, _ = List.fold_left
1674
(* lift to get outside of past patterns to get terms in the combined environment. *)
1675
(fun (pats, n) (sign, c, (s, args), p) ->
1676
let len = List.length sign in
1677
((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
1680
let ineqs = build_ineqs prevpatterns pats signlen in
1681
let rhs_rels' = rels_of_patsign rhs_rels in
1682
let _signenv = push_rel_context rhs_rels' env in
1685
List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
1686
(args @ c :: allargs, List.length args + succ n))
1689
let args = List.rev args in
1690
substl args (liftn signlen (succ nargs) arity)
1692
let rhs_rels', tycon =
1693
let neqs_rels, arity =
1697
[Anonymous, None, ineqs], lift 1 arity
1699
let eqs_rels, arity = decompose_prod_n_assum neqs arity in
1700
eqs_rels @ neqs_rels @ rhs_rels', arity
1702
let rhs_env = push_rels rhs_rels' env in
1703
let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
1704
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
1705
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
1706
let branch_name = id_of_string ("branch_" ^ (string_of_int !i)) in
1707
let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
1709
let bref = RVar (dummy_loc, branch_name) in
1710
match vars_of_ctx rhs_rels with
1712
| l -> RApp (dummy_loc, bref, l)
1714
let branch = match ineqs with
1715
Some _ -> RApp (dummy_loc, branch, [ hole ])
1719
let rhs = { eqn.rhs with it = branch } in
1720
(branch_decl :: branches,
1721
{ eqn with patterns = newpatterns; rhs = rhs } :: eqns,
1722
opats :: prevpatterns))
1726
(* Builds the predicate. If the predicate is dependent, its context is
1727
* made of 1+nrealargs assumptions for each matched term in an inductive
1728
* type and 1 assumption for each term not _syntactically_ in an
1731
* Each matched terms are independently considered dependent or not.
1733
* A type constraint but no annotation case: it is assumed non dependent.
1736
let lift_ctx n ctx =
1738
List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
1741
(* Turn matched terms into variables. *)
1742
let abstract_tomatch env tomatchs =
1743
let prev, ctx, names =
1745
(fun (prev, ctx, names) (c, t) ->
1746
let lenctx = List.length ctx in
1747
match kind_of_term c with
1748
Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names
1750
let name = next_ident_away_from (id_of_string "filtered_var") names in
1751
(mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
1752
(Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
1754
([], [], []) tomatchs
1755
in List.rev prev, ctx
1757
let is_dependent_ind = function
1758
IsInd (_, IndType (indf, args)) when List.length args > 0 -> true
1761
let build_dependent_signature env evars avoid tomatchs arsign =
1762
let avoid = ref avoid in
1763
let arsign = List.rev arsign in
1764
let allnames = List.rev (List.map (List.map pi1) arsign) in
1765
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
1766
let eqs, neqs, refls, slift, arsign' =
1768
(fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign ->
1771
number of previous eqs,
1772
lift to get outside eqs and in the introduced variables ('as' and 'in'),
1773
new arity signatures
1776
IsInd (ty, IndType (indf, args)) when List.length args > 0 ->
1777
(* Build the arity signature following the names in matched terms as much as possible *)
1778
let argsign = List.tl arsign in (* arguments in inverse application order *)
1779
let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
1780
let argsign = List.rev argsign in (* arguments in application order *)
1781
let env', nargeqs, argeqs, refl_args, slift, argsign' =
1783
(fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
1784
let argt = Retyping.get_type_of env evars arg in
1786
if Reductionops.is_conv env evars argt t then
1787
(mk_eq (lift (nargeqs + slift) argt)
1788
(mkRel (nargeqs + slift))
1789
(lift (nargeqs + nar) arg),
1790
mk_eq_refl argt arg)
1792
(mk_JMeq (lift (nargeqs + slift) t)
1793
(mkRel (nargeqs + slift))
1794
(lift (nargeqs + nar) argt)
1795
(lift (nargeqs + nar) arg),
1796
mk_JMeq_refl argt arg)
1800
match kind_of_term arg with
1801
Rel n -> pi1 (Environ.lookup_rel n env)
1804
make_prime avoid name
1807
(Name (eq_id avoid previd), None, eq) :: argeqs,
1808
refl_arg :: refl_args,
1810
(Name id, b, t) :: argsign'))
1811
(env, 0, [], [], slift, []) args argsign
1814
(lift (nargeqs + slift) appt)
1815
(mkRel (nargeqs + slift))
1816
(lift (nargeqs + nar) ty)
1817
(lift (nargeqs + nar) tm)
1819
let refl_eq = mk_JMeq_refl ty tm in
1820
let previd, id = make_prime avoid appn in
1821
(((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
1823
refl_eq :: refl_args,
1825
(((Name id, appb, appt) :: argsign') :: arsigns))
1828
(* Non dependent inductive or not inductive, just use a regular equality *)
1829
let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
1830
let previd, id = make_prime avoid name in
1831
let arsign' = (Name id, b, typ) in
1832
let tomatch_ty = type_of_tomatch ty in
1834
mk_eq (lift nar tomatch_ty)
1835
(mkRel slift) (lift nar tm)
1837
([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
1838
(mk_eq_refl tomatch_ty tm) :: refl_args,
1839
pred slift, (arsign' :: []) :: arsigns))
1840
([], 0, [], nar, []) tomatchs arsign
1842
let arsign'' = List.rev arsign' in
1843
assert(slift = 0); (* we must have folded over all elements of the arity signature *)
1844
arsign'', allnames, nar, eqs, neqs, refls
1846
(**************************************************************************)
1847
(* Main entry of the matching compilation *)
1849
let liftn_rel_context n k sign =
1850
let rec liftrec k = function
1852
(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
1855
liftrec (k + rel_context_length sign) sign
1857
let nf_evars_env evar_defs (env : env) : env =
1858
let nf t = nf_isevar evar_defs t in
1859
let env0 : env = reset_context env in
1860
let f e (na, b, t) e' : env =
1861
Environ.push_named (na, Option.map nf b, nf t) e'
1863
let env' = Environ.fold_named_context f ~init:env0 env in
1864
Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e')
1867
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
1869
let prepare_predicate_from_arsign_tycon loc env evm tomatchs arsign c =
1870
let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
1872
List.fold_left2 (fun (subst, len) (tm, tmtype) sign ->
1873
let signlen = List.length sign in
1874
match kind_of_term tm with
1875
| Rel n when dependent tm c
1876
&& signlen = 1 (* The term to match is not of a dependent type itself *) ->
1877
((n, len) :: subst, len - signlen)
1878
| Rel _ when not (dependent tm c)
1879
&& signlen > 1 (* The term is of a dependent type but does not appear in
1880
the tycon, maybe some variable in its type does. *) ->
1882
NotInd _ -> (* len - signlen, subst*) assert false (* signlen > 1 *)
1883
| IsInd (_, IndType(indf,realargs)) ->
1885
(fun (subst, len) arg ->
1886
match kind_of_term arg with
1887
| Rel n when dependent arg c ->
1888
((n, len) :: subst, pred len)
1889
| _ -> (subst, pred len))
1890
(subst, len) realargs)
1891
| _ -> (subst, len - signlen))
1892
([], nar) tomatchs arsign
1894
let rec predicate lift c =
1895
match kind_of_term c with
1896
| Rel n when n > lift ->
1898
(* Make the predicate dependent on the matched variable *)
1899
let idx = List.assoc (n - lift) subst in
1902
(* A variable that is not matched, lift over the arsign. *)
1905
map_constr_with_binders succ predicate lift c
1908
(* The tycon may be ill-typed after abstraction. *)
1909
let pred = predicate 0 c in
1910
let env' = push_rel_context (context_of_arsign arsign) env in
1911
ignore(Typing.sort_of env' evm pred); pred
1912
with _ -> lift nar c
1915
let prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs sign tycon rtntyp =
1916
(* We extract the signature of the arity *)
1917
let arsign = extract_arity_signature env tomatchs sign in
1918
let newenv = List.fold_right push_rels arsign env in
1919
let allnames = List.rev (List.map (List.map pi1) arsign) in
1922
let predcclj = typing_fun (mk_tycon (new_Type ())) newenv rtntyp in
1923
let predccl = (j_nf_isevar !isevars predcclj).uj_val in
1924
Some (build_initial_predicate true allnames predccl)
1926
match valcon_of_tycon tycon with
1929
prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars) tomatchs arsign ty
1930
in Some (build_initial_predicate true allnames pred)
1933
let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) =
1935
let typing_fun tycon env = typing_fun tycon env isevars in
1937
(* We build the matrix of patterns and right-hand-side *)
1938
let matx = matx_of_eqns env eqns in
1940
(* We build the vector of terms to match consistently with the *)
1941
(* constructors found in patterns *)
1942
let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
1943
let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in
1944
if predopt = None then
1945
let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in
1946
let tomatchs_len = List.length tomatchs_lets in
1947
let env = push_rel_context tomatchs_lets env in
1948
let len = List.length eqns in
1949
let sign, allnames, signlen, eqs, neqs, args =
1950
(* The arity signature *)
1951
let arsign = extract_arity_signatures env tomatchs (List.map snd tomatchl) in
1952
(* Build the dependent arity signature, the equalities which makes
1953
the first part of the predicate and their instantiations. *)
1955
build_dependent_signature env (Evd.evars_of !isevars) avoid tomatchs arsign
1959
match valcon_of_tycon tycon with
1960
| None -> let ev = mkExistential env isevars in ev, ev
1962
t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
1963
tomatchs sign (lift tomatchs_len t)
1966
let ctx = context_of_arsign eqs in
1967
let neqs = List.length ctx in
1968
neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
1971
(* Type the rhs under the assumption of equations *)
1972
constrs_of_pats typing_fun env isevars matx tomatchs sign neqs arity
1974
let matx = List.rev matx in
1975
let _ = assert(len = List.length lets) in
1976
let env = push_rels lets env in
1977
let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
1978
let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
1979
let args = List.rev_map (lift len) args in
1980
let pred = liftn len (succ signlen) arity in
1981
let pred = build_initial_predicate true allnames pred in
1983
(* We push the initial terms to match and push their alias to rhs' envs *)
1984
(* names of aliases will be recovered from patterns (hence Anonymous here) *)
1985
let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
1991
tomatch = initial_pushed;
1992
history = start_history (List.length initial_pushed);
1996
typing_function = typing_fun } in
1998
let j = compile pb in
1999
(* We check for unused patterns *)
2000
List.iter (check_unused_pattern env) matx;
2001
let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
2003
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
2004
uj_type = nf_isevar !isevars tycon; }
2007
(* We build the elimination predicate if any and check its consistency *)
2008
(* with the type of arguments to match *)
2009
let tmsign = List.map snd tomatchl in
2010
let pred = prepare_predicate_from_rettyp loc typing_fun isevars env tomatchs tmsign tycon predopt in
2012
(* We push the initial terms to match and push their alias to rhs' envs *)
2013
(* names of aliases will be recovered from patterns (hence Anonymous here) *)
2014
let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
2019
tomatch = initial_pushed;
2020
history = start_history (List.length initial_pushed);
2024
typing_function = typing_fun } in
2026
let j = compile pb in
2027
(* We check for unused patterns *)
2028
List.iter (check_unused_pattern env) matx;
2029
inh_conv_coerce_to_tycon loc env isevars j tycon
added
removed
contrib/subtac/subtac_cases.ml
