-
Notifications
You must be signed in to change notification settings - Fork 125
/
pass_LambdaLifting.ml
1309 lines (1180 loc) · 48 KB
/
pass_LambdaLifting.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
(*
Copyright © 2011 MLstate
This file is part of OPA.
OPA is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
OPA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with OPA. If not, see <http://www.gnu.org/licenses/>.
*)
(*
@author Sebastien Briais
*)
(* references:
Lambda lifting in quadratic time
Olivier Danvy, Ulrik Schultz
ML-Style Typing, Lambda Lifting and Partial Evaluation
Peter Thiemann
*)
(* Lambda lifting is composed of three passes:
1-name every anonymous lambda
2-compute the extra parameters to add to the functions and lift them
3-hoist the (now) closed functions to toplevel
1-The first pass is trivial.
The job is done by name_anonymous_lambda_* functions.
2-The second pass is the difficult one.
The job is done by parameterLift* functions.
It is done as explained in Danvy and Schultz article.
At each "let rec ... and ...", the call graph of the currently defined
functions is built.
The solution for these functions (ie the extra parameters to add) is
then computed by walking through the strongly connected components of
this call graph in reverse order.
Once the solution is found, the code is rewritten. Some care must be
taken in order to guarantee that identifiers are defined only once.
3-The third pass is less easy than it might appear at first glance,
especially if type information must be maintained.
Some reorder is needed here.
The job is done by hoist* functions and split_and_reorder.
Some non trivial examples:
1-Parameter lifting, code reordering
val f u v w =
let rec g x = x + v
and h y = g y + i y
and i z =
let j () = h z + w in j ()
in i u
This shows the difficulty to compute the extra parameters.
Despite h is closed, some extra parameters need to be added
to it, since it calls i (which is non closed).
The call graph for the big "let rec ... and ..." which
define g, h and i will be
g ->
h -> g, i
i -> h
The free variables (not functions) are
fv(g) = v
fv(h) = 0
fv(i) = w
The scc are
{h, i} -> {g}
The solution is computed by walking throught the scc in reverse order.
We get:
{g} -> {v}
{h, i} -> {v, w}
Hence, after the parameter lifting pass, we get:
val f u v w =
let rec g v x = x + v
and h v w y = g v y + i v w y
and i v w z =
let j v w z () = h v w z + w in j v w z ()
in i v w u
After code hoisting, we get:
val f u v w = i v w u
val g v x = x + v
val h v w y = g v y + i v w y
val i v w z = j v w z ()
val j v w z () = h v w z + w
Obviously, some reordering is needed. We finally get:
val g v x = x + v
val rec h v w y = g v y + i v w y
and i v w z = j v w z ()
and j v w z () = h v w z + w
val f u v w = i v w u
2-Typing issues - parameter lifting
val id x = x
val h v =
let y = (id,v) in
let g z = y.fst y.fst y.snd
in g v
Here, y has type ('a->'a,'b)
Since y is free in g, it needs to be given as an extra parameter to g.
But, the following code will not type in ML.
val id x = x
val h v =
let y = (id,v) in
let g y z = y.fst y.fst y.snd
in g y v
This is because the type scheme of y is instantiated with two
different types in g.
One solution is to lift y several times, one for each instantiation
of y.
If rank-2 polymorphism is possible, then things become easier. We
just need to annotate the type of y, when added as an extra
parameter to g.
val id x = x
val h v =
let y = (id,v) in
let g (y:forall 'a.('a->'a,'b)) z = y.fst y.fst y.snd
in g y v
3-Typing issues - code hoisting
Assume
null: 'a list -> bool
tl : 'a list -> 'a
The following code shows that code hoisting is not that easy, if
one do no want to break typability.
val rec f y z =
let rec g x =
if (null x) then f [] z else g (tl x)
in
if null y then 0
else (g [0]) + (g [true])
Basically, we will get:
val rec g x = if (null x) then f [] z else g (tl x)
and f y z = if null y then 0 else (g [0]) + (g [true])
Unfortunately, this does not type anymore.
One solution is to implement what is explained in Thiemann's article.
Another solution is to have rank-2 polymorphism and polymorphic recursion.
In this latter case, we will simply annotate g with the
type forall 'a.('a list->int).
*)
(* depends *)
module List = Base.List
(* shorthands *)
module Q = QmlAst
(* refactoring in progress *)
(* -- *)
type options = {
mode : [ `typed | `untyped | `fun_action of (IdentSet.t ref * IdentSet.t ref) ];
}
#<Debugvar:LAMBDA_DEBUG>
let debug_coerce annotmap body _ty =
#<If:LAMBDA_COERCE>
QmlAstCons.TypedExpr.coerce annotmap body _ty
#<Else>
annotmap,body
#<End>
let pp_ident_set f set =
IdentSet.iter (fun x -> Format.fprintf f "%s@ " (Ident.to_string x)) set
type 'a ignored_directive =[
| Q.type_directive
| Q.lambda_lifting_directive
| Q.slicer_directive
| Q.closure_instrumentation_directive
| `async
]
(* some utility functions to get types and type schemes *)
let get_ty annotmap ann =
QmlAnnotMap.find_ty ann annotmap
let get_tsc gamma x =
match QmlTypes.Env.Ident.find_opt x gamma with
| None -> failwith (Format.sprintf "get_tsc: cannot find %s in gamma" (Ident.to_string x))
| Some(tsc) -> tsc
let get_explicit_tsc gamma x =
QmlTypes.Scheme.explicit_forall (get_tsc gamma x)
let get_tsc_annotmap annotmap ann =
match QmlAnnotMap.find_tsc_opt ann annotmap with
| None -> QmlTypes.Scheme.id (get_ty annotmap ann)
| Some(tsc) -> tsc
(* compute the free names of an expression
input:
e: Q.expr
the expression to analyse
output:
the set of free names of e
*)
let fn_of_expr e =
QmlAstWalk.Expr.fold_with_env
(* collect the binders *)
(fun bn x _ ->
IdentSet.add x bn)
(* no binder initially *)
IdentSet.empty
(* collect the free variables *)
(fun bn fn e ->
match e with
| Q.Ident (_, x) ->
if IdentSet.mem x bn then fn
else IdentSet.add x fn
| _ -> fn)
(* no free variables initially *)
IdentSet.empty
(* the expression to analyse *)
e
(* depending on e,
build the node
let bnds in body, or
let rec bnds in body
*)
let mk_let_rec e bnds body =
match e with
| Q.LetIn (label, _, _) ->
(* QmlAstCons.UntypedExpr.letin bnds body *)
Q.LetIn (label, bnds, body)
| Q.LetRecIn (label, _, _) ->
(* QmlAstCons.UntypedExpr.letrecin bnds body *)
Q.LetRecIn (label, bnds, body)
| _ -> assert false
(* give a name to anonymous lambda *)
let name_anonymous_lambda_expr ~options annotmap (toplevel_name,e) =
let mk_let annotmap x e =
(* build the node "let x = e in x" *)
if options.mode = `typed then
let ty = get_ty annotmap (Q.QAnnot.expr e) in
let annotmap,id_x = QmlAstCons.TypedExpr.ident annotmap x ty in
let annotmap,let_in = QmlAstCons.TypedExpr.letin annotmap [x,e] id_x in
annotmap,let_in
else (
let pos_let = Q.Pos.expr e in
let label_let = Annot.next_label pos_let in
let label_ident = Annot.next_label pos_let in
(annotmap,
(QmlAstCons.UntypedExprWithLabel.letin
~label: label_let [x,e]
(QmlAstCons.UntypedExprWithLabel.ident ~label: label_ident x)))
) in
(* is_anonymous is a flag which indicates
whether the given expression is the rhs of a let *)
let aux =
match options.mode with
| `typed
| `untyped ->
let rec aux tra is_anonymous annotmap e =
match e with
| Q.Lambda _ when is_anonymous ->
let fun_ident = Ident.refreshf ~map:"anon_fun_%s" toplevel_name in
let annotmap, e = aux tra false annotmap e in
mk_let annotmap fun_ident e
| Q.LetIn (_, bnds, body)
| Q.LetRecIn (_, bnds, body) ->
let annotmap,bnds' =
List.fold_left_map_stable
(fun annotmap ((x,e) as p) ->
let annotmap,e' = aux tra false annotmap e in
if e == e' then annotmap, p else
annotmap,(x,e'))
annotmap bnds in
let annotmap,body' = aux tra true annotmap body in
if body' == body && bnds == bnds' then annotmap, e else
annotmap,mk_let_rec e bnds' body'
| Q.Coerce _
| Q.Directive(_, #ignored_directive,_,_) ->
tra is_anonymous annotmap e
| _ ->
tra true annotmap e in
aux
| `fun_action (public_set,client_set) ->
let rec aux tra _ annotmap e =
match e with
| Q.Directive (_, `fun_action v, [e], _) ->
assert (v = None);
(* here we don't check that we actually have a lambda inside the fun_action
* it is on purpose: we want to lift anything, not just lambdas *)
(* we remove the directive `fun_action, but we will put it back later *)
let fun_ident = Ident.refreshf ~map:"fun_action_%s" toplevel_name in
let fun_ident' = Ident.refreshf ~map:"fun_action_eta_%s" toplevel_name in
public_set := IdentSet.add fun_ident !public_set;
client_set := IdentSet.add fun_ident' !client_set;
let annotmap, e = aux tra false annotmap e in
let pos = Q.Pos.expr e in
let label () = Annot.next_label pos in
annotmap,
QmlAstCons.UntypedExprWithLabel.letin ~label:(label()) [fun_ident, e]
(QmlAstCons.UntypedExprWithLabel.letin ~label:(label())
[fun_ident', QmlAstUtils.Lambda.eta_expand_ast 1 (QmlAstCons.UntypedExprWithLabel.ident ~label:(label()) fun_ident)]
(QmlAstCons.UntypedExprWithLabel.ident ~label:(label()) fun_ident'))
| Q.Directive (_, `fun_action _, _, _) -> assert false
| _ -> tra false annotmap e in
aux in
let acc, e = QmlAstWalk.Expr.traverse_foldmap_context_down aux false annotmap e in
acc, (toplevel_name, e)
(* returns whether e is a function or not *)
let get_arity_of_lambda e =
QmlAstWalk.Expr.traverse_findmap
(fun tra e ->
match e with
| Q.Lambda (_, args, _) -> Some (List.length args)
| Q.Coerce _
| Q.Directive(_, #ignored_directive,_,_) -> tra e
| _ -> None
) e
let is_lambda e = get_arity_of_lambda e <> None
type env = {
funcs: (Ident.t list * int) IdentMap.t; (* maps lifted ident to their environment * original arity *)
(* maps from identifiers that will be lifted to their free variables *)
gamma: QmlTypes.gamma (* the gamma this is given back by the pass
* starts empty and grows with each definition toplevel def
* it contains all toplevel types and is used to determine if
* a name is defined at toplevel or not *);
hoisted : (Ident.t * Q.expr) list list;
hierarchy : Ident.t list; (* see the description of @lifted_lambda *)
}
(* In the functions that take an env and a gamma, the gamma
* is the environment only for the current declaration (but it
* contains everything, not only toplevel identifiers)
* this gamma never goes 'up', its value from recursive calls
* is always ignored
* It is used only to propagate types
*)
type binding = Ident.t * Q.expr
(* compute a map which give for each function identifiers
of the funcs declarations
its set of free functions symbols and its set of free variables
ie
function ident -> (free functions, free variables)
*)
let get_vars env (funcs : binding list) =
let fun_names =
List.fold_left
(fun s (x,_e) -> IdentSet.add x s)
IdentSet.empty funcs in
List.fold_left
(fun map (x,e) ->
let fn = fn_of_expr e in
let ff_x,fv_x =
IdentSet.fold
(fun n (ff_x,fv_x) ->
try
let (env,_) = IdentMap.find n env.funcs in
(ff_x,(* when you call a local function, then you need its environment
* because you will replace 'f' in your body by f(env1,...,envn) *)
List.fold_left
(fun env fv -> IdentSet.add fv env)
fv_x
env)
with Not_found ->
if IdentSet.mem n fun_names then
(IdentSet.add n ff_x,fv_x)
else (ff_x,IdentSet.add n fv_x))
fn
(IdentSet.empty,IdentSet.empty)
in
let fv_x = (* removing the names from the computed gamma
* (because they are at the toplevel) *)
IdentSet.filter
(fun x -> not (QmlTypes.Env.Ident.mem x env.gamma)) fv_x
in
IdentMap.add x (ff_x,fv_x) map)
IdentMap.empty
funcs
module M1 =
struct
type t = {ident : Ident.t; mutable set : IdentSet.t}
let compare {ident=ident1} {ident=ident2} = Ident.compare ident1 ident2
let hash {ident=ident} = Ident.hash ident
let equal {ident=ident1} {ident=ident2} = Ident.equal ident1 ident2
end
module G1 = Graph.Imperative.Digraph.Concrete(M1)
module SCC1 = GraphUtils.Components.Make(G1)
(* compute the mapping that gives for each function its environment
for a nest of mutually recursive functions
the result is a list of list
each sublist gives for each function identifiers its extra environment
each sublist will be turned in a definition of mutually recursive
functions
*)
let compute_solution env funcs =
match funcs with
| [] -> [] (* no function in the let bindings *)
| [(i,_)] ->
(* no mutual recursion -> no need to compute sccs *)
let (_,fv_i) = IdentMap.find i (get_vars env funcs) in
[([i],IdentSet.elements fv_i)]
| _ ->
let size = 2 in
let names = get_vars env funcs in
(* create the call graph *)
let g = G1.create ~size () in
(* first the vertices
one vertex per function identifier *)
let vertices =
IdentMap.mapi
(fun x (_,fv_x) ->
let v_x = G1.V.create {M1.ident=x; M1.set=fv_x} in
G1.add_vertex g v_x;
v_x)
names in
(* then the edges
if f calls g then add an edge from f to g
*)
IdentMap.iter
(fun x (ff_x,_) ->
let v_x = IdentMap.find x vertices in
IdentSet.iter
(fun y ->
let v_y = IdentMap.find y vertices in
G1.add_edge g v_x v_y)
ff_x) names;
(* compute the strongly connected components *)
let scc = SCC1.scc ~size g in
(* compute the vf sets
walk through the scc in reverse topological order *)
List.map
(fun p ->
let v =
List.fold_left
(fun v ({M1.set=vf_x_ref} as v_x) ->
let env_x = G1.fold_succ
(fun {M1.set=vf_y_ref} vf ->
IdentSet.union vf vf_y_ref)
g v_x vf_x_ref in
IdentSet.union v env_x)
IdentSet.empty
p in
List.iter (fun v_x -> v_x.M1.set <- v) p;
(* order the elements *)
let elt_v = IdentSet.elements v in
let f_idents = List.map (fun v_x -> v_x.M1.ident) p in
f_idents,elt_v)
scc
(* get fresh identifiers for abstracting the functions *)
let get_fresh_identifiers env gamma =
List.map
(fun x ->
let fresh_x =
Ident.refresh ~map:(Printf.sprintf "extra_%s") x in
let ty = get_explicit_tsc gamma x in
(fresh_x,ty))
env
let get_fresh_identifiers_untyped env =
List.map (Ident.refresh ~map:(Printf.sprintf "extra_%s")) env
(* add lambda on top of an expression *)
let absify ~toplevel env gamma_with_lambda_bindings annotmap e xs =
match xs with
| [] when toplevel -> annotmap, e
| _ ->
QmlAstWalk.Expr.traverse_foldmap
(fun tra annotmap -> function
| Q.Lambda (_, il, e) ->
let orig_xs =
List.map (fun i ->
let tsc = QmlTypes.Env.Ident.find i gamma_with_lambda_bindings in
let ty = QmlTypes.Scheme.explicit_forall tsc in
(i, ty)) il in
let annotmap, e = QmlAstCons.TypedExpr.lambda annotmap (xs @ orig_xs) e in
QmlAstCons.TypedExpr.directive_id annotmap (`lifted_lambda (List.length xs, List.tl env.hierarchy)) e
| Q.Coerce _
| Q.Directive (_, #ignored_directive, _, _) as e ->
tra annotmap e
| _ ->
(* you don't add parameters to something that is not a function *)
assert false) annotmap e
let absify_untyped ~toplevel e xs =
match xs with
| [] when toplevel -> e
| _ ->
QmlAstWalk.Expr.traverse_map
(fun tra expr ->
match expr with
| Q.Lambda (_, orig_xs, e) ->
let pos = Q.Pos.expr expr in
let label = Annot.next_label pos in
QmlAstCons.UntypedExprWithLabel.lambda ~label (xs @ orig_xs) e
| Q.Coerce _
| Q.Directive (_, #ignored_directive, _, _) as e -> tra e
| _ -> assert false)
e
let absify_fun_action e xs =
(* could use 0-ary functions, but since it's completely untested,
* seems risky for now *)
let xs = if xs = [] then [Ident.next "_"] else xs in
let pos = Q.Pos.expr e in
let label = Annot.next_label pos in
QmlAstCons.UntypedExprWithLabel.lambda ~label xs e
(* substitution on expressions *)
let subst e sigma =
QmlAstWalk.Expr.map_up
(fun e ->
match e with
| Q.Ident (label, x) ->
begin
try
let y = IdentMap.find x sigma in
Q.Ident (label, y)
with Not_found -> e
end
| _ -> e
) e
let mk_let_rec_tree ~options (gamma,annotmap,env) e funcs vals body =
let aux env f =
List.fold_left_map
(fun (env,annotmap) ((f,body) as bnd) ->
match options.mode with
| `fun_action (public_set, client_set) ->
let label = Annot.refresh (Q.Label.expr body) in
ignore (label, public_set, client_set);
let body =
if IdentSet.mem f !public_set then
Q.Directive (label, `visibility_annotation (`public `funaction), [body], [])
else (
assert (IdentSet.mem f !client_set);
Q.Directive (label, `side_annotation `client, [body], [])
) in
(env, annotmap), (f, body)
| `untyped ->
(env, annotmap), bnd
| `typed ->
let annot = Q.QAnnot.expr body in
let tsc = QmlTypes.Env.Ident.find f env.gamma in
let annotmap =
if QmlGenericScheme.is_empty tsc then
annotmap
else
(* tsc_gen for ei, only when non trivial *)
QmlAnnotMap.add_tsc annot tsc annotmap in
(*let ty = QmlTypes.Scheme.explicit_forall tsc in
let annotmap,body = debug_coerce annotmap body ty in*)
(env, annotmap), bnd
) env f in
let annotmap, body =
match vals with
| [] ->
(* beware of not dumping the annot for ei that was (maybe) on the original LetIn *)
let annot_e = Q.QAnnot.expr e in
let annot_body = Q.QAnnot.expr body in
assert (QmlAnnotMap.find_tsc_opt annot_body annotmap = None);
let annotmap =
QmlAnnotMap.add_tsc_opt annot_body
(QmlAnnotMap.find_tsc_opt annot_e annotmap) annotmap in
annotmap, body
| _ ->
annotmap, mk_let_rec e vals body in
let (env, annotmap), funcs = List.fold_left_map aux (env,annotmap) funcs in
let env = {env with hoisted = List.rev_append funcs env.hoisted} in
(gamma,annotmap,env), body
let mk_apply gamma annotmap e args old_args =
let annotmap, args =
List.fold_left_map (fun annotmap (x,ty) -> QmlAstCons.TypedExpr.ident annotmap x ty) annotmap args in
QmlAstCons.TypedExpr.apply gamma annotmap e (args @ old_args)
type context = (* this datatype represents an apply node
* its use is described in Apply case below *) {
applied : Q.expr;
args : Q.expr list;
mutable used : bool;
tsc_gen_opt : (Q.ty,unit) QmlGenericScheme.tsc option;
}
module IdentAssoc = BaseList.MakeAssoc(Ident)
let rec get_arrow_ty annotmap = function
| Q.Lambda (label,_,_) -> (
match QmlAnnotMap.find_ty_label label annotmap with
| Q.TypeArrow (a,b) -> (a,b)
| _ -> assert false
)
| Q.Coerce (_, e, _) ->
get_arrow_ty annotmap e
| Q.Directive (_, #ignored_directive, l, _) -> (
match l with
| [e] -> get_arrow_ty annotmap e
| _ -> assert false
)
| _ -> assert false
let get_params_and_return_of_arrow_type gamma ty =
match QmlTypesUtils.Inspect.follow_alias_noopt gamma ty with
| Q.TypeArrow (params,ty) -> params,ty
| _ -> assert false
let wrap_partial_apply ~partial annotmap e =
let info = QmlAnnotMap.find (Q.QAnnot.expr e) annotmap in
let annot = Annot.next () in
let annotmap = QmlAnnotMap.add annot info annotmap in
let label = Annot.make_label annot (Q.Pos.expr e) in
annotmap, Q.Directive (label, partial, [e], [])
let wrap_partial_apply_untyped ~partial e =
let label = Annot.next_label (Q.Pos.expr e) in
Q.Directive (label, partial, [e], [])
(* solution: map function names to list of variables
e: the expression to lift *)
(* gamma = typing environment of the currently analysed expression *)
let rec parameterLiftExp ~options ?outer_apply ((gamma,annotmap,env) as full_env) e =
match e with
| Q.Coerce _
| Q.Directive (_, #ignored_directive, _, _) ->
(* propagating outer_apply *)
QmlAstWalk.Expr.foldmap_nonrec (fun acc e -> parameterLiftExp ~options ?outer_apply acc e) full_env e
| Q.Apply (label, e1, es) ->
(* we may need to regroup this apply in the case f(args) to create
* f(env,args) and not f(env)(args)
* so we remember it in [outer_apply] and we use it in the ident case
* we can't match Apply (Ident _, _) because we may have directives or
* coercions in the middle *)
let acc, es' = List.fold_left_map (fun acc e -> parameterLiftExp ~options acc e) full_env es in
let tsc_gen_opt = QmlAnnotMap.find_tsc_opt_label label annotmap in
let outer_apply = {applied = e1; args = es'; used = false; tsc_gen_opt} in
let acc, e1' = parameterLiftExp ~options ~outer_apply acc e1 in
acc, if e1 == e1' && es == es' then e else
if outer_apply.used then e1' else Q.Apply (label, e1', es')
| (Q.Ident (label, x)) as whole_expr ->
begin
try
(* if ident is a function symbol *)
(* the args have not yet been refreshed
(need to be substituted afterwards) *)
let (args,original_arity) = IdentMap.find x env.funcs in
match args, options.mode with
| [], `typed ->
let tsc = QmlTypes.Env.Ident.find x env.gamma in
let annotmap =
if QmlGenericScheme.is_empty tsc then annotmap
else QmlAnnotMap.add_tsc_inst_label label tsc annotmap in
(gamma,annotmap,env), e
| [], `untyped ->
(* we need to reinsert the @fun_action directive even if the lambda had no
* environment *)
full_env, e
| _ ->
let e, old_args, partial, orig_tsc_gen_opt =
match outer_apply with
| None ->
assert (original_arity <> -1);
let tsc_gen_opt = QmlAnnotMap.find_tsc_opt_label label annotmap in
e, [], `partial_apply (Some original_arity,false), tsc_gen_opt
(* ident with an env -> partial application *)
| Some ({applied = e; args = el; used; tsc_gen_opt} as context) ->
(* full apply (if the user code didn't contain
* any partial apply) *)
assert (used = false);
(* we say that we already used the outer apply
* or else we would end up with [f(env,args)(args)]
* instead of [f(env,args)] *)
context.used <- true;
e, el, `full_apply (List.length args), tsc_gen_opt in
(match options.mode with
| `typed ->
let args =
List.map
(fun x ->
let ty = get_explicit_tsc gamma x in x,ty)
args in
let ty =
let ty = get_ty annotmap (Q.QAnnot.expr e) in
match partial with
| `partial_apply _ ->
(* if we create [f(env)], we say that
* that [f] has type [env -> args -> return] *)
Q.TypeArrow (List.map snd args, ty)
| `full_apply _ ->
(* if we create [f(env,args)], we say that
* [f] has type [env, args -> return] *)
let params, ty = get_params_and_return_of_arrow_type env.gamma ty in
Q.TypeArrow (List.map snd args @ params, ty) in
let annotmap,e = QmlAstCons.TypedExpr.ident annotmap x ty in
let annotmap =
let tsc = QmlTypes.Env.Ident.find x env.gamma in
if QmlGenericScheme.is_empty tsc then annotmap
else QmlAnnotMap.add_tsc_inst (Q.QAnnot.expr e) tsc annotmap in
let annotmap,e =
let annotmap, e = mk_apply gamma annotmap e args old_args in
wrap_partial_apply ~partial annotmap e in
(* propagating the tsc_gen that was (maybe) on the ident or apply *)
let annotmap = QmlAnnotMap.add_tsc_opt (Q.QAnnot.expr e) orig_tsc_gen_opt annotmap in
(gamma,annotmap,env),e
| `untyped ->
let e =
let args =
List.map
(fun arg_expr ->
(* Use location of the whole initial expression we
are processing. *)
let pos = Q.Pos.expr whole_expr in
let label = Annot.next_label pos in
QmlAstCons.UntypedExprWithLabel.ident
~label arg_expr)
args in
(* Like above, let's use location of the whole initial
expression we are processing. *)
let pos_for_e = Q.Pos.expr whole_expr in
let label_for_e = Annot.next_label pos_for_e in
let e =
QmlAstCons.UntypedExprWithLabel.apply
~label: label_for_e e (args @ old_args) in
wrap_partial_apply_untyped ~partial e in
(full_env, e)
| `fun_action (public_set,_) ->
let pos = Annot.pos label in
let args =
(* could use a 0-ary function in the case args=[] *)
if args = [] then [QmlAstCons.UntypedExprWithLabel.int ~label:(Annot.next_label pos) 0]
else List.map (fun i -> QmlAstCons.UntypedExprWithLabel.ident ~label:(Annot.next_label pos) i) args in
let e = QmlAstCons.UntypedExprWithLabel.may_apply ~label:(Annot.next_label pos) (QmlAstCons.UntypedExprWithLabel.may_apply ~label:(Annot.next_label pos) e args) old_args in
if IdentSet.mem x !public_set then
full_env, e
else
let label = Annot.next_label (Q.Pos.expr e) in
let e = Q.Directive (label, `fun_action None, [e], []) in
full_env, e
)
with Not_found -> full_env,e
end
| Q.LetIn (_, bnds, body)
| Q.LetRecIn (_, bnds, body) ->
let full_env,(funcs,vals) =
parameterLiftBnds ~options ~toplevel:false full_env bnds in
let (_,annotmap,env),body =
parameterLiftExp ~options full_env body in
mk_let_rec_tree ~options (gamma,annotmap,env) e funcs vals body
| Q.Match (label, expr, guards) ->
let (_,annotmap,env),expr = parameterLiftExp ~options full_env expr in
let (_,annotmap,env),guards =
parameterLiftGuards ~options (gamma,annotmap,env) guards in
(gamma,annotmap,env), Q.Match (label, expr, guards)
| _ -> QmlAstWalk.Expr.foldmap_nonrec (fun acc e -> parameterLiftExp ~options acc e) full_env e
and parameterLiftGuards ~options (gamma,annotmap,env) guards =
let update_gamma gamma annotmap pat =
QmlAstWalk.Pattern.fold_down
(fun gamma p ->
match p with
| Q.PatVar (_, x) ->
let ty = get_ty annotmap (Q.QAnnot.pat p) in
QmlTypes.Env.Ident.add x (QmlTypes.Scheme.id ty) gamma
| Q.PatAs (_, _, x) ->
(* Instead of:
let ty = get_ty annotmap (Q.QAnnot.pat p) in
let tsc = QmlTypes.Scheme.generalize env.gamma ty in
we get the scheme specially stored for the alias in which
column variables have been refreshed to make them generalizable.
This way, we get the scheme whose body represent the type of
only the aliased part of the pattern and not the global type
of all the patterns unified. *)
let tsc = get_tsc_annotmap annotmap (Q.QAnnot.pat p) in
QmlTypes.Env.Ident.add x tsc gamma
| _ -> gamma)
gamma
pat in
let (annotmap,env),guards =
List.fold_left_map
(fun (annotmap,env) (pat,expr) ->
let gamma = if options.mode = `typed then update_gamma gamma annotmap pat else gamma in
let (_,annotmap,env),expr =
parameterLiftExp ~options (gamma,annotmap,env) expr
in
(annotmap,env),(pat,expr))
(annotmap,env) guards in
(gamma,annotmap,env),guards
and parameterLiftBnds ~options ~toplevel (gamma,annotmap,env) bnds =
let (funcs,vals) =
match options.mode with
| `fun_action (public_set,client_set) ->
(match bnds with
| [(name,_)] when IdentSet.mem name !public_set || IdentSet.mem name !client_set ->
(* we name every fun_action, so we know these are always singleton *)
bnds, []
| _ -> [], bnds (* no lifting otherwise *)
)
| `typed | `untyped ->
List.partition (fun (_x,e) -> is_lambda e) bnds in
let gamma =
if options.mode = `typed then
List.fold_left
(fun gamma (x,e) ->
QmlTypes.Env.Ident.add x (get_tsc_annotmap annotmap (Q.QAnnot.expr e)) gamma)
gamma
vals
else
gamma
in
let funcs_sols = compute_solution env funcs in
let env =
let solution =
(* update the solution *)
List.fold_left
(fun solution (f_idents,env) ->
List.fold_left
(fun solution f_ident ->
let body = IdentAssoc.find f_ident funcs in
let original_arity =
match get_arity_of_lambda body with
| Some i -> i
| None ->
assert (match options.mode with `fun_action _ -> true | _ -> false);
-1 in
IdentMap.safe_add f_ident (env,original_arity) solution)
solution
f_idents)
env.funcs
funcs_sols
in
{ env with funcs = solution }
in
let env =
match options.mode with
| `typed ->
let env_gamma =
List.fold_left
(fun env_gamma (f_idents,extra) ->
let tys = List.map (get_explicit_tsc gamma) extra in
List.fold_left
(fun env_gamma f_ident ->
let body = IdentAssoc.find f_ident funcs in
let ty_params,ty_ret = get_arrow_ty annotmap body in
let ty = Q.TypeArrow (tys @ ty_params,ty_ret) in
let tsc = QmlTypes.Scheme.quantify ty in
QmlTypes.Env.Ident.add f_ident tsc env_gamma
) env_gamma f_idents
) env.gamma funcs_sols in
{env with gamma = env_gamma}
| `fun_action _ | `untyped -> env in
let hierarchy = env.hierarchy in
let (annotmap,env),funcs =
(* rewrite the body of each function *)
List.fold_left_map
(fun (annotmap,env) (f_idents,extra) ->
List.fold_left_map
(fun (annotmap,env) f_ident ->
let body =
(* get the original body of f_ident *)
snd (List.find
(fun (x,_) -> Ident.equal x f_ident)
funcs) in
(* lift the body *)
let env = {env with hierarchy = f_ident :: hierarchy} in
let (gamma_with_lambda_bindings,annotmap,env),body =
parameterLiftLambda ~options (gamma,annotmap,env) body in
let annotmap,body,sigma =
match options.mode with
| `typed ->
(* get fresh identifiers (that will be abstracted) *)
let fresh_extra = get_fresh_identifiers extra gamma in
(* abstract the new variables *)
let annotmap,body = absify ~toplevel env gamma_with_lambda_bindings annotmap body fresh_extra in
(* compute the substitution
free variable -> fresh identifier *)
let sigma =
List.fold_left
(fun sigma (x,(y,_)) ->
IdentMap.add x y sigma)
IdentMap.empty
(List.combine extra fresh_extra) in
annotmap,body,sigma
| `fun_action _ | `untyped as mode ->
(* Warning: the types are not the same as the code above *)
let fresh_extra = get_fresh_identifiers_untyped extra in
let body =
match mode with
| `fun_action _ -> absify_fun_action body fresh_extra
| `untyped -> absify_untyped ~toplevel body fresh_extra in
let sigma = IdentMap.from_list (List.combine extra fresh_extra) in
annotmap,body,sigma in
(* replace each free variables by the corresponding
fresh identifier *)
let body = subst body sigma in
(annotmap,env),(f_ident,body))
(annotmap,env)
f_idents)
(annotmap,env)
funcs_sols in
let (annotmap,env),vals =
List.fold_left_map
(fun (annotmap,env) (x,e) ->
let (_,annotmap,env),e = parameterLiftExp ~options (gamma,annotmap,env) e in
(annotmap,env),(x,e))
(annotmap,env)
vals in
let env = {env with hierarchy} in
(gamma,annotmap,env),(funcs,vals)
(* the gamma returned by this function contains the identifiers bound by the lambda
* this is actually needed by parameterLiftBinding to avoid recomputing the types
* of the parameters (and since the code is globally renamed, having too much names
* in the gamma isn't a problem) *)
and parameterLiftLambda ~options ((gamma,annotmap,env) as full_env) e =
match e with
| Q.Lambda (_, params,_) when options.mode = `typed ->
begin
let ty = get_ty annotmap (Q.QAnnot.expr e) in
match ty with
| Q.TypeArrow (ty_params,_) ->
let gamma =
List.fold_left2
(fun gamma x ty -> QmlTypes.Env.Ident.add x (QmlTypes.Scheme.id ty) gamma)
gamma params ty_params in
QmlAstWalk.Expr.foldmap_nonrec (parameterLiftLambda ~options) (gamma,annotmap,env) e
| _ -> (* could happen with overloads, the clean way to solve this
* would be to have annotations on lambda and let bound bindings *)
let context = QmlError.Context.annoted_expr annotmap e in
QmlError.i_error None context (
"unexpected type @{<bright>%a@}"
)
QmlPrint.pp#ty ty
end