5
(* Ocaml 3.06 Map.S does not handle is_empty *)
6
let idmap_is_empty m = m = Idmap.empty
9
Some basic functions to rebuild rawconstr
10
In each of them the location is Util.dummy_loc
12
let mkRRef ref = RRef(dummy_loc,ref)
13
let mkRVar id = RVar(dummy_loc,id)
14
let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
15
let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b)
16
let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b)
17
let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
18
let mkRCases(rto,l,brl) = RCases(dummy_loc,Term.RegularStyle,rto,l,brl)
19
let mkRSort s = RSort(dummy_loc,s)
20
let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
21
let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
24
Some basic functions to decompose rawconstrs
25
These are analogous to the ones constrs
27
let raw_decompose_prod =
28
let rec raw_decompose_prod args = function
30
raw_decompose_prod ((n,t)::args) b
35
let raw_decompose_prod_or_letin =
36
let rec raw_decompose_prod args = function
38
raw_decompose_prod ((n,None,Some t)::args) b
40
raw_decompose_prod ((n,Some t,None)::args) b
45
let raw_compose_prod =
46
List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
48
let raw_compose_prod_or_letin =
52
| (n,None,Some t) -> mkRProd(n,t,concl)
53
| (n,Some bdy,None) -> mkRLetIn(n,bdy,concl)
56
let raw_decompose_prod_n n =
57
let rec raw_decompose_prod i args c =
62
raw_decompose_prod (i-1) ((n,t)::args) b
65
raw_decompose_prod n []
68
let raw_decompose_prod_or_letin_n n =
69
let rec raw_decompose_prod i args c =
74
raw_decompose_prod (i-1) ((n,None,Some t)::args) b
76
raw_decompose_prod (i-1) ((n,Some t,None)::args) b
79
raw_decompose_prod n []
82
let raw_decompose_app =
83
let rec decompose_rapp acc rt =
84
(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
87
decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
88
| rt -> rt,List.rev acc
95
(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t2 = t1] *)
96
let raw_make_eq ?(typ= mkRHole ()) t1 t2 =
97
mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1])
99
(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
100
let raw_make_neq t1 t2 =
101
mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2])
103
(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
104
let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
106
(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
107
to [P1 \/ ( .... \/ Pn)]
109
let rec raw_make_or_list = function
110
| [] -> raise (Invalid_argument "mk_or")
112
| e::l -> raw_make_or e (raw_make_or_list l)
115
let remove_name_from_mapping mapping na =
117
| Anonymous -> mapping
118
| Name id -> Idmap.remove id mapping
121
let rec change_vars mapping rt =
127
Idmap.find id mapping
133
| RApp(loc,rt',rtl) ->
135
change_vars mapping rt',
136
List.map (change_vars mapping) rtl
138
| RLambda(loc,name,k,t,b) ->
142
change_vars mapping t,
143
change_vars (remove_name_from_mapping mapping name) b
145
| RProd(loc,name,k,t,b) ->
149
change_vars mapping t,
150
change_vars (remove_name_from_mapping mapping name) b
152
| RLetIn(loc,name,def,b) ->
155
change_vars mapping def,
156
change_vars (remove_name_from_mapping mapping name) b
158
| RLetTuple(loc,nal,(na,rto),b,e) ->
159
let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
162
(na, Option.map (change_vars mapping) rto),
163
change_vars mapping b,
164
change_vars new_mapping e
166
| RCases(loc,sty,infos,el,brl) ->
169
List.map (fun (e,x) -> (change_vars mapping e,x)) el,
170
List.map (change_vars_br mapping) brl
172
| RIf(loc,b,(na,e_option),lhs,rhs) ->
174
change_vars mapping b,
175
(na,Option.map (change_vars mapping) e_option),
176
change_vars mapping lhs,
177
change_vars mapping rhs
179
| RRec _ -> error "Local (co)fixes are not supported"
182
| RCast(loc,b,CastConv (k,t)) ->
183
RCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
184
| RCast(loc,b,CastCoerce) ->
185
RCast(loc,change_vars mapping b,CastCoerce)
186
| RDynamic _ -> error "Not handled RDynamic"
187
and change_vars_br mapping ((loc,idl,patl,res) as br) =
188
let new_mapping = List.fold_right Idmap.remove idl mapping in
189
if idmap_is_empty new_mapping
191
else (loc,idl,patl,change_vars new_mapping res)
197
let rec alpha_pat excluded pat =
199
| PatVar(loc,Anonymous) ->
200
let new_id = Indfun_common.fresh_id excluded "_x" in
201
PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
202
| PatVar(loc,Name id) ->
203
if List.mem id excluded
205
let new_id = Nameops.next_ident_away id excluded in
206
PatVar(loc,Name new_id),(new_id::excluded),
207
(Idmap.add id new_id Idmap.empty)
208
else pat,excluded,Idmap.empty
209
| PatCstr(loc,constr,patl,na) ->
210
let new_na,new_excluded,map =
212
| Name id when List.mem id excluded ->
213
let new_id = Nameops.next_ident_away id excluded in
214
Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
215
| _ -> na,excluded,Idmap.empty
217
let new_patl,new_excluded,new_map =
219
(fun (patl,excluded,map) pat ->
220
let new_pat,new_excluded,new_map = alpha_pat excluded pat in
221
(new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
223
([],new_excluded,map)
226
PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map
228
let alpha_patl excluded patl =
229
let patl,new_excluded,map =
231
(fun (patl,excluded,map) pat ->
232
let new_pat,new_excluded,new_map = alpha_pat excluded pat in
233
new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
235
([],excluded,Idmap.empty)
238
(List.rev patl,new_excluded,map)
243
let raw_get_pattern_id pat acc =
244
let rec get_pattern_id pat =
246
| PatVar(loc,Anonymous) -> assert false
247
| PatVar(loc,Name id) ->
249
| PatCstr(loc,constr,patternl,_) ->
252
let idl' = get_pattern_id pat in
258
(get_pattern_id pat)@acc
260
let get_pattern_id pat = raw_get_pattern_id pat []
262
let rec alpha_rt excluded rt =
265
| RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
266
| RLambda(loc,Anonymous,k,t,b) ->
267
let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
268
let new_excluded = new_id :: excluded in
269
let new_t = alpha_rt new_excluded t in
270
let new_b = alpha_rt new_excluded b in
271
RLambda(loc,Name new_id,k,new_t,new_b)
272
| RProd(loc,Anonymous,k,t,b) ->
273
let new_t = alpha_rt excluded t in
274
let new_b = alpha_rt excluded b in
275
RProd(loc,Anonymous,k,new_t,new_b)
276
| RLetIn(loc,Anonymous,t,b) ->
277
let new_t = alpha_rt excluded t in
278
let new_b = alpha_rt excluded b in
279
RLetIn(loc,Anonymous,new_t,new_b)
280
| RLambda(loc,Name id,k,t,b) ->
281
let new_id = Nameops.next_ident_away id excluded in
286
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
289
let new_excluded = new_id::excluded in
290
let new_t = alpha_rt new_excluded t in
291
let new_b = alpha_rt new_excluded b in
292
RLambda(loc,Name new_id,k,new_t,new_b)
293
| RProd(loc,Name id,k,t,b) ->
294
let new_id = Nameops.next_ident_away id excluded in
295
let new_excluded = new_id::excluded in
300
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
303
let new_t = alpha_rt new_excluded t in
304
let new_b = alpha_rt new_excluded b in
305
RProd(loc,Name new_id,k,new_t,new_b)
306
| RLetIn(loc,Name id,t,b) ->
307
let new_id = Nameops.next_ident_away id excluded in
312
let replace = change_vars (Idmap.add id new_id Idmap.empty) in
315
let new_excluded = new_id::excluded in
316
let new_t = alpha_rt new_excluded t in
317
let new_b = alpha_rt new_excluded b in
318
RLetIn(loc,Name new_id,new_t,new_b)
321
| RLetTuple(loc,nal,(na,rto),t,b) ->
322
let rev_new_nal,new_excluded,mapping =
324
(fun (nal,excluded,mapping) na ->
326
| Anonymous -> (na::nal,excluded,mapping)
328
let new_id = Nameops.next_ident_away id excluded in
331
na::nal,id::excluded,mapping
333
(Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
335
([],excluded,Idmap.empty)
338
let new_nal = List.rev rev_new_nal in
339
let new_rto,new_t,new_b =
340
if idmap_is_empty mapping
342
else let replace = change_vars mapping in
343
(Option.map replace rto, t,replace b)
345
let new_t = alpha_rt new_excluded new_t in
346
let new_b = alpha_rt new_excluded new_b in
347
let new_rto = Option.map (alpha_rt new_excluded) new_rto in
348
RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
349
| RCases(loc,sty,infos,el,brl) ->
351
List.map (function (rt,i) -> alpha_rt excluded rt, i) el
353
RCases(loc,sty,infos,new_el,List.map (alpha_br excluded) brl)
354
| RIf(loc,b,(na,e_o),lhs,rhs) ->
355
RIf(loc,alpha_rt excluded b,
356
(na,Option.map (alpha_rt excluded) e_o),
357
alpha_rt excluded lhs,
358
alpha_rt excluded rhs
360
| RRec _ -> error "Not handled RRec"
363
| RCast (loc,b,CastConv (k,t)) ->
364
RCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
365
| RCast (loc,b,CastCoerce) ->
366
RCast(loc,alpha_rt excluded b,CastCoerce)
367
| RDynamic _ -> error "Not handled RDynamic"
368
| RApp(loc,f,args) ->
371
List.map (alpha_rt excluded) args
376
and alpha_br excluded (loc,ids,patl,res) =
377
let new_patl,new_excluded,mapping = alpha_patl excluded patl in
378
let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
379
let new_excluded = new_ids@excluded in
380
let renamed_res = change_vars mapping res in
381
let new_res = alpha_rt new_excluded renamed_res in
382
(loc,new_ids,new_patl,new_res)
385
[is_free_in id rt] checks if [id] is a free variable in [rt]
388
let rec is_free_in = function
390
| RVar(_,id') -> id_ord id' id == 0
393
| RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
394
| RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) ->
397
| Name id' -> id_ord id' id <> 0
400
is_free_in t || (check_in_b && is_free_in b)
401
| RCases(_,_,_,el,brl) ->
402
(List.exists (fun (e,_) -> is_free_in e) el) ||
403
List.exists is_free_in_br brl
404
| RLetTuple(_,nal,_,b,t) ->
406
not (List.exists (function Name id' -> id'= id | _ -> false) nal)
408
is_free_in t || (check_in_nal && is_free_in b)
410
| RIf(_,cond,_,br1,br2) ->
411
is_free_in cond || is_free_in br1 || is_free_in br2
412
| RRec _ -> raise (UserError("",str "Not handled RRec"))
415
| RCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
416
| RCast (_,b,CastCoerce) -> is_free_in b
417
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
418
and is_free_in_br (_,ids,_,rt) =
419
(not (List.mem id ids)) && is_free_in rt
425
let rec pattern_to_term = function
426
| PatVar(loc,Anonymous) -> assert false
427
| PatVar(loc,Name id) ->
429
| PatCstr(loc,constr,patternl,_) ->
431
Inductiveops.mis_constructor_nargs_env
438
(cst_narg - List.length patternl)
439
(fun _ -> mkRHole ())
443
List.map pattern_to_term patternl
445
mkRApp(mkRRef(Libnames.ConstructRef constr),
446
implicit_args@patl_as_term
451
let replace_var_by_term x_id term =
452
let rec replace_var_by_pattern rt =
455
| RVar(_,id) when id_ord id x_id == 0 -> term
459
| RApp(loc,rt',rtl) ->
461
replace_var_by_pattern rt',
462
List.map replace_var_by_pattern rtl
464
| RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
465
| RLambda(loc,name,k,t,b) ->
469
replace_var_by_pattern t,
470
replace_var_by_pattern b
472
| RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
473
| RProd(loc,name,k,t,b) ->
477
replace_var_by_pattern t,
478
replace_var_by_pattern b
480
| RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
481
| RLetIn(loc,name,def,b) ->
484
replace_var_by_pattern def,
485
replace_var_by_pattern b
487
| RLetTuple(_,nal,_,_,_)
488
when List.exists (function Name id -> id = x_id | _ -> false) nal ->
490
| RLetTuple(loc,nal,(na,rto),def,b) ->
493
(na,Option.map replace_var_by_pattern rto),
494
replace_var_by_pattern def,
495
replace_var_by_pattern b
497
| RCases(loc,sty,infos,el,brl) ->
500
List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
501
List.map replace_var_by_pattern_br brl
503
| RIf(loc,b,(na,e_option),lhs,rhs) ->
504
RIf(loc, replace_var_by_pattern b,
505
(na,Option.map replace_var_by_pattern e_option),
506
replace_var_by_pattern lhs,
507
replace_var_by_pattern rhs
509
| RRec _ -> raise (UserError("",str "Not handled RRec"))
512
| RCast(loc,b,CastConv(k,t)) ->
513
RCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
514
| RCast(loc,b,CastCoerce) ->
515
RCast(loc,replace_var_by_pattern b,CastCoerce)
516
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
517
and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
518
if List.exists (fun id -> id_ord id x_id == 0) idl
520
else (loc,idl,patl,replace_var_by_pattern res)
522
replace_var_by_pattern
527
(* checking unifiability of patterns *)
528
exception NotUnifiable
530
let rec are_unifiable_aux = function
534
| PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs
535
| PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
536
if constructor2 <> constructor1
537
then raise NotUnifiable
540
try ((List.combine cpl1 cpl2)@eqs)
541
with _ -> anomaly "are_unifiable_aux"
543
are_unifiable_aux eqs'
545
let are_unifiable pat1 pat2 =
547
are_unifiable_aux [pat1,pat2];
549
with NotUnifiable -> false
552
let rec eq_cases_pattern_aux = function
556
| PatVar _,PatVar _ -> eq_cases_pattern_aux eqs
557
| PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
558
if constructor2 <> constructor1
559
then raise NotUnifiable
562
try ((List.combine cpl1 cpl2)@eqs)
563
with _ -> anomaly "eq_cases_pattern_aux"
565
eq_cases_pattern_aux eqs'
566
| _ -> raise NotUnifiable
568
let eq_cases_pattern pat1 pat2 =
570
eq_cases_pattern_aux [pat1,pat2];
572
with NotUnifiable -> false
577
let rec ids_of_pat ids = function
578
| PatVar(_,Anonymous) -> ids
579
| PatVar(_,Name id) -> Idset.add id ids
580
| PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
582
ids_of_pat Idset.empty
584
let id_of_name = function
585
| Names.Anonymous -> id_of_string "x"
588
(* TODO: finish Rec caes *)
589
let ids_of_rawterm c =
590
let rec ids_of_rawterm acc c =
591
let idof = id_of_name in
593
| RVar (_,id) -> id::acc
594
| RApp (loc,g,args) ->
595
ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc
596
| RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
597
| RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc
598
| RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
599
| RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc
600
| RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc
601
| RIf (loc,c,(na,po),b1,b2) -> ids_of_rawterm [] c @ ids_of_rawterm [] b1 @ ids_of_rawterm [] b2 @ acc
602
| RLetTuple (_,nal,(na,po),b,c) ->
603
List.map idof nal @ ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc
604
| RCases (loc,sty,rtntypopt,tml,brchl) ->
605
List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_rawterm [] c) brchl)
606
| RRec _ -> failwith "Fix inside a constructor branch"
607
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> []
610
List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_rawterm [] c)
617
let rec zeta_normalize_term rt =
623
| RApp(loc,rt',rtl) ->
625
zeta_normalize_term rt',
626
List.map zeta_normalize_term rtl
628
| RLambda(loc,name,k,t,b) ->
632
zeta_normalize_term t,
633
zeta_normalize_term b
635
| RProd(loc,name,k,t,b) ->
639
zeta_normalize_term t,
640
zeta_normalize_term b
642
| RLetIn(_,Name id,def,b) ->
643
zeta_normalize_term (replace_var_by_term id def b)
644
| RLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b
645
| RLetTuple(loc,nal,(na,rto),def,b) ->
648
(na,Option.map zeta_normalize_term rto),
649
zeta_normalize_term def,
650
zeta_normalize_term b
652
| RCases(loc,sty,infos,el,brl) ->
655
List.map (fun (e,x) -> (zeta_normalize_term e,x)) el,
656
List.map zeta_normalize_br brl
658
| RIf(loc,b,(na,e_option),lhs,rhs) ->
659
RIf(loc, zeta_normalize_term b,
660
(na,Option.map zeta_normalize_term e_option),
661
zeta_normalize_term lhs,
662
zeta_normalize_term rhs
664
| RRec _ -> raise (UserError("",str "Not handled RRec"))
667
| RCast(loc,b,CastConv(k,t)) ->
668
RCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
669
| RCast(loc,b,CastCoerce) ->
670
RCast(loc,zeta_normalize_term b,CastCoerce)
671
| RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
672
and zeta_normalize_br (loc,idl,patl,res) =
673
(loc,idl,patl,zeta_normalize_term res)
682
let rec add_as map pat =
685
| PatCstr(_,_,patl,Name id) ->
686
Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
687
| PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
689
let rec expand_as map rt =
691
| RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ -> rt
698
| RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args)
699
| RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b)
700
| RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b)
701
| RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
702
| RLetTuple(loc,nal,(na,po),v,b) ->
703
RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
704
expand_as map v, expand_as map b)
705
| RIf(loc,e,(na,po),br1,br2) ->
706
RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
707
expand_as map br1, expand_as map br2)
708
| RRec _ -> error "Not handled RRec"
709
| RDynamic _ -> error "Not handled RDynamic"
710
| RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
711
| RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
712
| RCases(loc,sty,po,el,brl) ->
713
RCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
714
List.map (expand_as_br map) brl)
715
and expand_as_br map (loc,idl,cpl,rt) =
716
(loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
718
expand_as Idmap.empty
added
removed
contrib/funind/rawtermops.ml
