-
Notifications
You must be signed in to change notification settings - Fork 1
/
glob_term_to_relation.ml
1582 lines (1521 loc) · 59.3 KB
/
glob_term_to_relation.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
open Printer
open Pp
open Names
open Constr
open Context
open Vars
open Glob_term
open Glob_ops
open Indfun_common
open CErrors
open Util
open Glob_termops
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
let observe strm = if do_observe () then Feedback.msg_debug strm else ()
(*let observennl strm =
if do_observe ()
then Pp.msg strm
else ()*)
type binder_type = Lambda of Name.t | Prod of Name.t | LetIn of Name.t
type glob_context = (binder_type * glob_constr) list
let rec solve_trivial_holes pat_as_term e =
match (DAst.get pat_as_term, DAst.get e) with
| GHole _, _ -> e
| GApp (fp, argsp), GApp (fe, argse) when glob_constr_eq fp fe ->
DAst.make
(GApp
(solve_trivial_holes fp fe, List.map2 solve_trivial_holes argsp argse))
| _, _ -> pat_as_term
(*
compose_glob_context [(bt_1,n_1,t_1);......] rt returns
b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
binders corresponding to the bt_i's
*)
let compose_glob_context =
let compose_binder (bt, t) acc =
match bt with
| Lambda n -> mkGLambda (n, t, acc)
| Prod n -> mkGProd (n, t, acc)
| LetIn n -> mkGLetIn (n, t, None, acc)
in
List.fold_right compose_binder
(*
The main part deals with building a list of globalized constructor expressions
from the rhs of a fixpoint equation.
*)
type 'a build_entry_pre_return =
{ context : glob_context
; (* the binding context of the result *)
value : 'a (* The value *) }
type 'a build_entry_return =
{result : 'a build_entry_pre_return list; to_avoid : Id.t list}
(*
[combine_results combine_fun res1 res2] combine two results [res1] and [res2]
w.r.t. [combine_fun].
Informally, both [res1] and [res2] are lists of "constructors" [res1_1;...]
and [res2_1,....] and we need to produce
[combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
*)
let combine_results
(combine_fun :
'a build_entry_pre_return
-> 'b build_entry_pre_return
-> 'c build_entry_pre_return) (res1 : 'a build_entry_return)
(res2 : 'b build_entry_return) : 'c build_entry_return =
let pre_result =
List.map
(fun res1 ->
(* for each result in arg_res *)
List.map (* we add it in each args_res *)
(fun res2 -> combine_fun res1 res2)
res2.result)
res1.result
in
(* and then we flatten the map *)
{ result = List.concat pre_result
; to_avoid = List.union Id.equal res1.to_avoid res2.to_avoid }
(*
The combination function for an argument with a list of argument
*)
let combine_args arg args =
{ context = arg.context @ args.context
; (* Note that the binding context of [arg] MUST be placed before the one of
[args] in order to preserve possible type dependencies
*)
value = arg.value :: args.value }
let ids_of_binder = function
| LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty
| LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id
let rec change_vars_in_binder mapping = function
| [] -> []
| (bt, t) :: l ->
let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in
(bt, change_vars mapping t)
::
( if Id.Map.is_empty new_mapping then l
else change_vars_in_binder new_mapping l )
let rec replace_var_by_term_in_binder x_id term = function
| [] -> []
| (bt, t) :: l ->
(bt, replace_var_by_term x_id term t)
::
( if Id.Set.mem x_id (ids_of_binder bt) then l
else replace_var_by_term_in_binder x_id term l )
let add_bt_names bt = Id.Set.union (ids_of_binder bt)
let apply_args ctxt body args =
let need_convert_id avoid id =
List.exists (is_free_in id) args || Id.Set.mem id avoid
in
let need_convert avoid bt =
Id.Set.exists (need_convert_id avoid) (ids_of_binder bt)
in
let next_name_away (na : Name.t) (mapping : Id.t Id.Map.t) (avoid : Id.Set.t)
=
match na with
| Name id when Id.Set.mem id avoid ->
let new_id = Namegen.next_ident_away id avoid in
(Name new_id, Id.Map.add id new_id mapping, Id.Set.add new_id avoid)
| _ -> (na, mapping, avoid)
in
let next_bt_away bt (avoid : Id.Set.t) =
match bt with
| LetIn na ->
let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
(LetIn new_na, mapping, new_avoid)
| Prod na ->
let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
(Prod new_na, mapping, new_avoid)
| Lambda na ->
let new_na, mapping, new_avoid = next_name_away na Id.Map.empty avoid in
(Lambda new_na, mapping, new_avoid)
in
let rec do_apply avoid ctxt body args =
match (ctxt, args) with
| _, [] ->
(* No more args *)
(ctxt, body)
| [], _ ->
(* no more fun *)
let f, args' = glob_decompose_app body in
(ctxt, mkGApp (f, args' @ args))
| (Lambda Anonymous, t) :: ctxt', arg :: args' ->
do_apply avoid ctxt' body args'
| (Lambda (Name id), t) :: ctxt', arg :: args' ->
let new_avoid, new_ctxt', new_body, new_id =
if need_convert_id avoid id then
let new_avoid = Id.Set.add id avoid in
let new_id = Namegen.next_ident_away id new_avoid in
let new_avoid' = Id.Set.add new_id new_avoid in
let mapping = Id.Map.add id new_id Id.Map.empty in
let new_ctxt' = change_vars_in_binder mapping ctxt' in
let new_body = change_vars mapping body in
(new_avoid', new_ctxt', new_body, new_id)
else (Id.Set.add id avoid, ctxt', body, id)
in
let new_body = replace_var_by_term new_id arg new_body in
let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
do_apply avoid new_ctxt' new_body args'
| (bt, t) :: ctxt', _ ->
let new_avoid, new_ctxt', new_body, new_bt =
let new_avoid = add_bt_names bt avoid in
if need_convert avoid bt then
let new_bt, mapping, new_avoid = next_bt_away bt new_avoid in
( new_avoid
, change_vars_in_binder mapping ctxt'
, change_vars mapping body
, new_bt )
else (new_avoid, ctxt', body, bt)
in
let new_ctxt', new_body = do_apply new_avoid new_ctxt' new_body args in
((new_bt, t) :: new_ctxt', new_body)
in
do_apply Id.Set.empty ctxt body args
let combine_app f args =
let new_ctxt, new_value = apply_args f.context f.value args.value in
{ (* Note that the binding context of [args] MUST be placed before the one of
the applied value in order to preserve possible type dependencies
*)
context = args.context @ new_ctxt
; value = new_value }
let combine_lam n t b =
{ context = []
; value =
mkGLambda
( n
, compose_glob_context t.context t.value
, compose_glob_context b.context b.value ) }
let combine_prod2 n t b =
{ context = []
; value =
mkGProd
( n
, compose_glob_context t.context t.value
, compose_glob_context b.context b.value ) }
let combine_prod n t b =
{context = t.context @ ((Prod n, t.value) :: b.context); value = b.value}
let combine_letin n t b =
{context = t.context @ ((LetIn n, t.value) :: b.context); value = b.value}
let mk_result ctxt value avoid =
{result = [{context = ctxt; value}]; to_avoid = avoid}
(*************************************************
Some functions to deal with overlapping patterns
**************************************************)
let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type")
let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type")
(*
[make_discr_match_el \[e1,...en\]] builds match e1,...,en with
(the list of expressions on which we will do the matching)
*)
let make_discr_match_el = List.map (fun e -> (e, (Anonymous, None)))
(*
[make_discr_match_brl i \[pat_1,...,pat_n\]] constructs a discrimination pattern matching on the ith expression.
that is.
match ?????? with \\
| pat_1 => False \\
| pat_{i-1} => False \\
| pat_i => True \\
| pat_{i+1} => False \\
\vdots
| pat_n => False
end
*)
let make_discr_match_brl i =
List.map_i
(fun j {CAst.v = idl, patl, _} ->
CAst.make
@@
if Int.equal j i then (idl, patl, mkGRef (Lazy.force coq_True_ref))
else (idl, patl, mkGRef (Lazy.force coq_False_ref)))
0
(*
[make_discr_match brl el i] generates an hypothesis such that it reduce to true iff
brl_{i} is the first branch matched by [el]
Used when we want to simulate the coq pattern matching algorithm
*)
let make_discr_match brl el i =
mkGCases (None, make_discr_match_el el, make_discr_match_brl i brl)
(**********************************************************************)
(* functions used to build case expression from lettuple and if ones *)
(**********************************************************************)
(* [build_constructors_of_type] construct the array of pattern of its inductive argument*)
let build_constructors_of_type ind' argl =
let mib, ind = Inductive.lookup_mind_specif (Global.env ()) ind' in
let npar = mib.Declarations.mind_nparams in
Array.mapi
(fun i _ ->
let construct = (ind', i + 1) in
let constructref = GlobRef.ConstructRef construct in
let _implicit_positions_of_cst =
Impargs.implicits_of_global constructref
in
let cst_narg =
Inductiveops.constructor_nallargs (Global.env ()) construct
in
let argl =
if List.is_empty argl then List.make cst_narg (mkGHole ())
else List.make npar (mkGHole ()) @ argl
in
let pat_as_term =
mkGApp (mkGRef (GlobRef.ConstructRef (ind', i + 1)), argl)
in
cases_pattern_of_glob_constr (Global.env ()) Anonymous pat_as_term)
ind.Declarations.mind_consnames
(******************)
(* Main functions *)
(******************)
let raw_push_named (na, raw_value, raw_typ) env =
match na with
| Anonymous -> env
| Name id -> (
let typ, _ =
Pretyping.understand env (Evd.from_env env)
~expected_type:Pretyping.IsType raw_typ
in
let na = make_annot id Sorts.Relevant in
(* TODO relevance *)
match raw_value with
| None -> EConstr.push_named (NamedDecl.LocalAssum (na, typ)) env
| Some value -> EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env
)
let add_pat_variables sigma pat typ env : Environ.env =
let rec add_pat_variables env pat typ : Environ.env =
observe
(str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
match DAst.get pat with
| PatVar na ->
Environ.push_rel
(RelDecl.LocalAssum (make_annot na Sorts.Relevant, typ))
env
| PatCstr (c, patl, na) ->
let (Inductiveops.IndType (indf, indargs)) =
try
Inductiveops.find_rectype env (Evd.from_env env)
(EConstr.of_constr typ)
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
let constructor : Inductiveops.constructor_summary =
List.find
(fun cs -> Environ.QConstruct.equal env c (fst cs.Inductiveops.cs_cstr))
(Array.to_list constructors)
in
let cs_args_types : types list =
List.map RelDecl.get_type constructor.Inductiveops.cs_args
in
List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
in
let new_env = add_pat_variables env pat typ in
let res =
fst
(Context.Rel.fold_outside
(fun decl (env, ctxt) ->
let open Context.Rel.Declaration in
match decl with
| LocalAssum ({binder_name = Anonymous}, _)
|LocalDef ({binder_name = Anonymous}, _, _) ->
assert false
| LocalAssum (({binder_name = Name id} as na), t) ->
let na = {na with binder_name = id} in
let new_t = substl ctxt t in
observe
( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
++ str "old type := "
++ Printer.pr_lconstr_env env sigma t
++ fnl () ++ str "new type := "
++ Printer.pr_lconstr_env env sigma new_t
++ fnl () );
let open Context.Named.Declaration in
(Environ.push_named (LocalAssum (na, new_t)) env, mkVar id :: ctxt)
| LocalDef (({binder_name = Name id} as na), v, t) ->
let na = {na with binder_name = id} in
let new_t = substl ctxt t in
let new_v = substl ctxt v in
observe
( str "for variable " ++ Ppconstr.pr_id id ++ fnl ()
++ str "old type := "
++ Printer.pr_lconstr_env env sigma t
++ fnl () ++ str "new type := "
++ Printer.pr_lconstr_env env sigma new_t
++ fnl () ++ str "old value := "
++ Printer.pr_lconstr_env env sigma v
++ fnl () ++ str "new value := "
++ Printer.pr_lconstr_env env sigma new_v
++ fnl () );
let open Context.Named.Declaration in
( Environ.push_named (LocalDef (na, new_v, new_t)) env
, mkVar id :: ctxt ))
(Environ.rel_context new_env)
~init:(env, []))
in
observe
(str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env));
res
let rec pattern_to_term_and_type env typ =
DAst.with_val (function
| PatVar Anonymous -> assert false
| PatVar (Name id) -> mkGVar id
| PatCstr (constr, patternl, _) ->
let cst_narg = Inductiveops.constructor_nallargs (Global.env ()) constr in
let (Inductiveops.IndType (indf, indargs)) =
try
Inductiveops.find_rectype env (Evd.from_env env)
(EConstr.of_constr typ)
with Not_found -> assert false
in
let constructors = Inductiveops.get_constructors env indf in
let constructor =
List.find
(fun cs ->
Environ.QConstruct.equal env (fst cs.Inductiveops.cs_cstr) constr)
(Array.to_list constructors)
in
let cs_args_types : types list =
List.map RelDecl.get_type constructor.Inductiveops.cs_args
in
let _, cstl = Inductiveops.dest_ind_family indf in
let csta = Array.of_list cstl in
let implicit_args =
Array.to_list
(Array.init
(cst_narg - List.length patternl)
(fun i ->
Detyping.detype Detyping.Now Id.Set.empty env
(Evd.from_env env)
(EConstr.of_constr csta.(i))))
in
let patl_as_term =
List.map2
(pattern_to_term_and_type env)
(List.rev cs_args_types) patternl
in
mkGApp (mkGRef (GlobRef.ConstructRef constr), implicit_args @ patl_as_term))
(* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return)
of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the
corresponding graphs.
The idea to transform a term [t] into a list of constructors [lc] is the following:
\begin{itemize}
\item if the term is a binder (bind x, body) then first compute [lc'] the list corresponding
to [body] and add (bind x. _) to each elements of [lc]
\item if the term has the form (g t1 ... ... tn) where g does not appears in (fnames)
then compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
then combine those lists and [g] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn],
[g c1 ... cn] is an element of [lc]
\item if the term has the form (f t1 .... tn) where [f] appears in [fnames] then
compute [lc1] ... [lcn] the lists of constructors corresponding to [t1] ... [tn],
then compute those lists and [f] as follows~: for each element [c1,...,cn] of [lc1\times...\times lcn]
create a new variable [res] and [forall res, R_f c1 ... cn res] is in [lc]
\item if the term is a cast just treat its body part
\item
if the term is a match, an if or a lettuple then compute the lists corresponding to each branch of the case
and concatenate them (informally, each branch of a match produces a new constructor)
\end{itemize}
WARNING: The terms constructed here are only USING the glob_constr syntax but are highly bad formed.
We must wait to have complete all the current calculi to set the recursive calls.
At this point, each term [f t1 ... tn] (where f appears in [funnames]) is replaced by
a pseudo term [forall res, res t1 ... tn, res]. A reconstruction phase is done later.
We in fact not create a constructor list since then end of each constructor has not the expected form
but only the value of the function
*)
let pr_glob_constr_env env x = pr_glob_constr_env env (Evd.from_env env) x
let rec build_entry_lc env sigma funnames avoid rt :
glob_constr build_entry_return =
observe (str " Entering : " ++ pr_glob_constr_env env rt);
let open CAst in
match DAst.get rt with
| GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GGenarg _ | GInt _
|GFloat _ ->
(* do nothing (except changing type of course) *)
mk_result [] rt avoid
| GApp (_, _) -> (
let f, args = glob_decompose_app rt in
let args_res : glob_constr list build_entry_return =
List.fold_right
(* create the arguments lists of constructors and combine them *)
(fun arg ctxt_argsl ->
let arg_res =
build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
in
combine_results combine_args arg_res ctxt_argsl)
args (mk_result [] [] avoid)
in
match DAst.get f with
| GLambda _ ->
let rec aux t l =
match l with
| [] -> t
| u :: l -> (
DAst.make
@@
match DAst.get t with
| GLambda (na, _, nat, b) -> GLetIn (na, u, None, aux b l)
| _ -> GApp (t, l) )
in
build_entry_lc env sigma funnames avoid (aux f args)
| GVar id when Id.Set.mem id funnames ->
(* if we have [f t1 ... tn] with [f]$\in$[fnames]
then we create a fresh variable [res],
add [res] and its "value" (i.e. [res v1 ... vn]) to each
pseudo constructor build for the arguments (i.e. a pseudo context [ctxt] and
a pseudo value "v1 ... vn".
The "value" of this branch is then simply [res]
*)
(* XXX here and other [understand] calls drop the ctx *)
let rt_as_constr, ctx = Pretyping.understand env (Evd.from_env env) rt in
let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in
let res_raw_type =
Detyping.detype Detyping.Now Id.Set.empty env (Evd.from_env env)
rt_typ
in
let res = fresh_id args_res.to_avoid "_res" in
let new_avoid = res :: args_res.to_avoid in
let res_rt = mkGVar res in
let new_result =
List.map
(fun arg_res ->
let new_hyps =
[ (Prod (Name res), res_raw_type)
; (Prod Anonymous, mkGApp (res_rt, mkGVar id :: arg_res.value)) ]
in
{context = arg_res.context @ new_hyps; value = res_rt})
args_res.result
in
{result = new_result; to_avoid = new_avoid}
| GVar _ | GEvar _ | GPatVar _ | GHole _ | GGenarg _ | GSort _ | GRef _ ->
(* if have [g t1 ... tn] with [g] not appearing in [funnames]
then
foreach [ctxt,v1 ... vn] in [args_res] we return
[ctxt, g v1 .... vn]
*)
{ args_res with
result =
List.map
(fun args_res -> {args_res with value = mkGApp (f, args_res.value)})
args_res.result }
| GApp _ ->
assert false (* we have collected all the app in [glob_decompose_app] *)
| GLetIn (n, v, t, b) ->
(* if we have [(let x := v in b) t1 ... tn] ,
we discard our work and compute the list of constructor for
[let x = v in (b t1 ... tn)] up to alpha conversion
*)
let new_n, new_b, new_avoid =
match n with
| Name id when List.exists (is_free_in id) args ->
(* need to alpha-convert the name *)
let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in
let new_avoid = id :: avoid in
let new_b = replace_var_by_term id (DAst.make @@ GVar id) b in
(Name new_id, new_b, new_avoid)
| _ -> (n, b, avoid)
in
build_entry_lc env sigma funnames avoid
(mkGLetIn (new_n, v, t, mkGApp (new_b, args)))
| GCases _ | GIf _ | GLetTuple _ | GProj _ ->
(* we have [(match e1, ...., en with ..... end) t1 tn]
we first compute the result from the case and
then combine each of them with each of args one
*)
let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in
combine_results combine_app f_res args_res
| GCast (b, _, _) ->
(* for an applied cast we just trash the cast part
and restart the work.
WARNING: We need to restart since [b] itself should be an application term
*)
build_entry_lc env sigma funnames avoid (mkGApp (b, args))
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GProd _ -> user_err Pp.(str "Cannot apply a type")
| GInt _ -> user_err Pp.(str "Cannot apply an integer")
| GFloat _ -> user_err Pp.(str "Cannot apply a float")
| GArray _ -> user_err Pp.(str "Cannot apply an array")
(* end of the application treatement *) )
| GProj (f, params, c) ->
let args_res : glob_constr list build_entry_return =
List.fold_right
(* create the arguments lists of constructors and combine them *)
(fun arg ctxt_argsl ->
let arg_res =
build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg
in
combine_results combine_args arg_res ctxt_argsl)
(params@[c]) (mk_result [] [] avoid) in
{ args_res with
result =
List.map
(fun args_res ->
let c, params = List.sep_last args_res.value in
{args_res with value = DAst.make (GProj (f, params, c))})
args_res.result }
| GLambda (n, _, t, b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
and combine the two result
*)
let t_res = build_entry_lc env sigma funnames avoid t in
let new_n =
match n with
| Name _ -> n
| Anonymous -> Name (Indfun_common.fresh_id [] "_x")
in
let new_env = raw_push_named (new_n, None, t) env in
let b_res = build_entry_lc new_env sigma funnames avoid b in
combine_results (combine_lam new_n) t_res b_res
| GProd (n, _, t, b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the type
and combine the two result
*)
let t_res = build_entry_lc env sigma funnames avoid t in
let new_env = raw_push_named (n, None, t) env in
let b_res = build_entry_lc new_env sigma funnames avoid b in
if List.length t_res.result = 1 && List.length b_res.result = 1 then
combine_results (combine_prod2 n) t_res b_res
else combine_results (combine_prod n) t_res b_res
| GLetIn (n, v, typ, b) ->
(* we first compute the list of constructor
corresponding to the body of the function,
then the one corresponding to the value [t]
and combine the two result
*)
let v =
match typ with
| None -> v
| Some t -> DAst.make ?loc:rt.loc @@ GCast (v, Some DEFAULTcast, t)
in
let v_res = build_entry_lc env sigma funnames avoid v in
let v_as_constr, ctx = Pretyping.understand env (Evd.from_env env) v in
let v_type = Retyping.get_type_of env (Evd.from_env env) v_as_constr in
let v_r = Sorts.Relevant in
(* TODO relevance *)
let new_env =
match n with
| Anonymous -> env
| Name id ->
EConstr.push_named
(NamedDecl.LocalDef (make_annot id v_r, v_as_constr, v_type))
env
in
let b_res = build_entry_lc new_env sigma funnames avoid b in
combine_results (combine_letin n) v_res b_res
| GCases (_, _, el, brl) ->
(* we create the discrimination function
and treat the case itself
*)
let make_discr = make_discr_match brl in
build_entry_lc_from_case env sigma funnames make_discr el brl avoid
| GIf (b, (na, e_option), lhs, rhs) ->
let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
let ind, _ =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err
( str "Cannot find the inductive associated to "
++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
++ str ". try again with a cast" )
in
let case_pats = build_constructors_of_type (fst ind) [] in
assert (Int.equal (Array.length case_pats) 2);
let brl =
List.map_i (fun i x -> CAst.make ([], [case_pats.(i)], x)) 0 [lhs; rhs]
in
let match_expr = mkGCases (None, [(b, (Anonymous, None))], brl) in
(* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *)
build_entry_lc env sigma funnames avoid match_expr
| GLetTuple (nal, _, b, e) ->
let nal_as_glob_constr =
List.map (function Name id -> mkGVar id | Anonymous -> mkGHole ()) nal
in
let b_as_constr, ctx = Pretyping.understand env (Evd.from_env env) b in
let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in
let ind, _ =
try Inductiveops.find_inductive env (Evd.from_env env) b_typ
with Not_found ->
user_err
( str "Cannot find the inductive associated to "
++ pr_glob_constr_env env b ++ str " in " ++ pr_glob_constr_env env rt
++ str ". try again with a cast" )
in
let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
assert (Int.equal (Array.length case_pats) 1);
let br = CAst.make ([], [case_pats.(0)], e) in
let match_expr = mkGCases (None, [(b, (Anonymous, None))], [br]) in
build_entry_lc env sigma funnames avoid match_expr
| GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast (b, _, _) -> build_entry_lc env sigma funnames avoid b
| GArray _ -> user_err Pp.(str "Not handled GArray")
and build_entry_lc_from_case env sigma funname make_discr (el : tomatch_tuples)
(brl : Glob_term.cases_clauses) avoid : glob_constr build_entry_return =
match el with
| [] -> assert false (* this case correspond to match <nothing> with .... !*)
| el ->
(* this case correspond to
match el with brl end
we first compute the list of lists corresponding to [el] and
combine them .
Then for each element of the combinations,
we compute the result we compute one list per branch in [brl] and
finally we just concatenate those list
*)
let case_resl =
List.fold_right
(fun (case_arg, _) ctxt_argsl ->
let arg_res =
build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg
in
combine_results combine_args arg_res ctxt_argsl)
el (mk_result [] [] avoid)
in
let types =
List.map
(fun (case_arg, _) ->
let case_arg_as_constr, ctx =
Pretyping.understand env (Evd.from_env env) case_arg
in
EConstr.Unsafe.to_constr
(Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr))
el
in
(****** The next works only if the match is not dependent ****)
let results =
List.map
(fun ca ->
let res =
build_entry_lc_from_case_term env sigma types funname make_discr []
brl case_resl.to_avoid ca
in
res)
case_resl.result
in
{ result = List.concat (List.map (fun r -> r.result) results)
; to_avoid =
List.fold_left
(fun acc r -> List.union Id.equal acc r.to_avoid)
[] results }
and build_entry_lc_from_case_term env sigma types funname make_discr
patterns_to_prevent brl avoid matched_expr =
match brl with
| [] -> (* computed_branches *) {result = []; to_avoid = avoid}
| br :: brl' ->
(* alpha conversion to prevent name clashes *)
let {CAst.v = idl, patl, return} = alpha_br avoid br in
let new_avoid = idl @ avoid in
(* for now we can no more use idl as an identifier *)
(* building a list of precondition stating that we are not in this branch
(will be used in the following recursive calls)
*)
let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in
let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
List.map2
(fun pat typ avoid pat'_as_term ->
let renamed_pat, _, _ = alpha_pat avoid pat in
let pat_ids = get_pattern_id renamed_pat in
let env_with_pat_ids = add_pat_variables sigma pat typ new_env in
List.fold_right
(fun id acc ->
let typ_of_id = Typing.type_of_variable env_with_pat_ids id in
let raw_typ_of_id =
Detyping.detype Detyping.Now Id.Set.empty env_with_pat_ids
(Evd.from_env env) typ_of_id
in
mkGProd (Name id, raw_typ_of_id, acc))
pat_ids
(glob_make_neq pat'_as_term (pattern_to_term renamed_pat)))
patl types
in
(* Checking if we can be in this branch
(will be used in the following recursive calls)
*)
let unify_with_those_patterns : (cases_pattern -> bool * bool) list =
List.map
(fun pat pat' -> (are_unifiable env pat pat', eq_cases_pattern env pat pat'))
patl
in
(*
we first compute the other branch result (in ordrer to keep the order of the matching
as much as possible)
*)
let brl'_res =
build_entry_lc_from_case_term env sigma types funname make_discr
((unify_with_those_patterns, not_those_patterns) :: patterns_to_prevent)
brl' avoid matched_expr
in
(* We now create the precondition of this branch i.e.
1- the list of variable appearing in the different patterns of this branch and
the list of equation stating than el = patl (List.flatten ...)
2- If there exists a previous branch which pattern unify with the one of this branch
then a discrimination precond stating that we are not in a previous branch (if List.exists ...)
*)
let those_pattern_preconds =
List.flatten
(List.map3
(fun pat e typ_as_constr ->
let this_pat_ids = ids_of_pat pat in
let typ_as_constr = EConstr.of_constr typ_as_constr in
let typ =
Detyping.detype Detyping.Now Id.Set.empty new_env
(Evd.from_env env) typ_as_constr
in
let pat_as_term = pattern_to_term pat in
(* removing trivial holes *)
let pat_as_term = solve_trivial_holes pat_as_term e in
(* observe (str "those_pattern_preconds" ++ spc () ++ *)
(* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *)
(* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *)
(* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *)
List.fold_right
(fun id acc ->
if Id.Set.mem id this_pat_ids then
( Prod (Name id)
, let typ_of_id = Typing.type_of_variable new_env id in
let raw_typ_of_id =
Detyping.detype Detyping.Now Id.Set.empty new_env
(Evd.from_env env) typ_of_id
in
raw_typ_of_id )
:: acc
else acc)
idl
[(Prod Anonymous, glob_make_eq ~typ pat_as_term e)])
patl matched_expr.value types)
@
if
List.exists
(function
| unifl, _ ->
let unif, _ =
List.split (List.map2 (fun x y -> x y) unifl patl)
in
List.for_all (fun x -> x) unif)
patterns_to_prevent
then
let i = List.length patterns_to_prevent in
let pats_as_constr =
List.map2 (pattern_to_term_and_type new_env) types patl
in
[(Prod Anonymous, make_discr pats_as_constr i)]
else []
in
(* We compute the result of the value returned by the branch*)
let return_res = build_entry_lc new_env sigma funname new_avoid return in
(* and combine it with the preconds computed for this branch *)
let this_branch_res =
List.map
(fun res ->
{ context = matched_expr.context @ those_pattern_preconds @ res.context
; value = res.value })
return_res.result
in
{brl'_res with result = this_branch_res @ brl'_res.result}
let is_res r =
match DAst.get r with
| GVar id -> (
try String.equal (String.sub (Id.to_string id) 0 4) "_res"
with Invalid_argument _ -> false )
| _ -> false
let is_gr env c gr =
match DAst.get c with GRef (r, _) -> Environ.QGlobRef.equal env r gr | _ -> false
let is_gvar c = match DAst.get c with GVar id -> true | _ -> false
let same_raw_term env rt1 rt2 =
match (DAst.get rt1, DAst.get rt2) with
| GRef (r1, _), GRef (r2, _) -> Environ.QGlobRef.equal env r1 r2
| GHole _, GHole _ -> true
| _ -> false
let decompose_raw_eq env lhs rhs =
let rec decompose_raw_eq lhs rhs acc =
observe
( str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " "
++ pr_glob_constr_env env rhs );
let rhd, lrhs = glob_decompose_app rhs in
let lhd, llhs = glob_decompose_app lhs in
observe (str "lhd := " ++ pr_glob_constr_env env lhd);
observe (str "rhd := " ++ pr_glob_constr_env env rhd);
observe (str "llhs := " ++ int (List.length llhs));
observe (str "lrhs := " ++ int (List.length lrhs));
let sllhs = List.length llhs in
let slrhs = List.length lrhs in
if same_raw_term env lhd rhd && Int.equal sllhs slrhs then
(* let _ = assert false in *)
List.fold_right2 decompose_raw_eq llhs lrhs acc
else (lhs, rhs) :: acc
in
decompose_raw_eq lhs rhs []
exception Continue
(*
The second phase which reconstruct the real type of the constructor.
rebuild the globalized constructors expression.
eliminates some meaningless equalities, applies some rewrites......
*)
let rec rebuild_cons env nb_args relname args crossed_types depth rt =
observe (str "rebuilding : " ++ pr_glob_constr_env env rt);
let open Context.Rel.Declaration in
let open CAst in
match DAst.get rt with
| GProd (n, k, t, b) -> (
let not_free_in_t id = not (is_free_in id t) in
let new_crossed_types = t :: crossed_types in
match DAst.get t with
| GApp (res_rt, args') when is_res res_rt -> (
let arg = List.hd args' in
match DAst.get arg with
| GVar this_relname ->
(*i The next call to mk_rel_id is
valid since we are constructing the graph
Ensures by: obvious
i*)
let new_t =
mkGApp (mkGVar (mk_rel_id this_relname), List.tl args' @ [res_rt])
in
let t', ctx = Pretyping.understand env (Evd.from_env env) new_t in
let r = Sorts.Relevant in
(* TODO relevance *)
let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
let new_b, id_to_exclude =
rebuild_cons new_env nb_args relname args new_crossed_types
(depth + 1) b
in
(mkGProd (n, new_t, new_b), Id.Set.filter not_free_in_t id_to_exclude)
| _ ->
(* the first args is the name of the function! *)
assert false )
| GApp (eq_as_ref, [ty; id; rt])
when is_gvar id
&& is_gr env eq_as_ref Coqlib.(lib_ref "core.eq.type")
&& n == Anonymous -> (
let loc1 = rt.CAst.loc in
let loc2 = eq_as_ref.CAst.loc in
let loc3 = id.CAst.loc in
let id = match DAst.get id with GVar id -> id | _ -> assert false in
try
observe (str "computing new type for eq : " ++ pr_glob_constr_env env rt);
let t' =
try fst (Pretyping.understand env (Evd.from_env env) t) (*FIXME*)
with e when CErrors.noncritical e -> raise Continue
in
let is_in_b = is_free_in id b in
let _keep_eq =
(not (List.exists (is_free_in id) args))
|| is_in_b
|| List.exists (is_free_in id) crossed_types
in
let new_args = List.map (replace_var_by_term id rt) args in
let subst_b = if is_in_b then b else replace_var_by_term id rt b in
let r = Sorts.Relevant in
(* TODO relevance *)
let new_env = EConstr.push_rel (LocalAssum (make_annot n r, t')) env in
let new_b, id_to_exclude =
rebuild_cons new_env nb_args relname new_args new_crossed_types
(depth + 1) subst_b
in
(mkGProd (n, t, new_b), id_to_exclude)
with Continue ->
let jmeq = GlobRef.IndRef (fst (EConstr.destInd Evd.empty (jmeq ()))) in
let ty', ctx = Pretyping.understand env (Evd.from_env env) ty in
let ind, args' =
Inductiveops.find_inductive env Evd.(from_env env) ty'
in
let mib, _ = Global.lookup_inductive (fst ind) in
let nparam = mib.Declarations.mind_nparams in
let params, arg' = Util.List.chop nparam args' in
let rt_typ =
DAst.make
@@ GApp
( DAst.make @@ GRef (GlobRef.IndRef (fst ind), None)
, List.map
(fun p ->
Detyping.detype Detyping.Now Id.Set.empty env
(Evd.from_env env) (EConstr.of_constr p))
params
@ Array.to_list
(Array.make (List.length args' - nparam) (mkGHole ())) )
in
let eq' =
DAst.make ?loc:loc1
@@ GApp
( DAst.make ?loc:loc2 @@ GRef (jmeq, None)
, [ty; DAst.make ?loc:loc3 @@ GVar id; rt_typ; rt] )
in
observe
(str "computing new type for jmeq : " ++ pr_glob_constr_env env eq');
let eq'_as_constr, ctx =
Pretyping.understand env (Evd.from_env env) eq'
in
observe (str " computing new type for jmeq : done");
let sigma = Evd.(from_env env) in
let new_args =