Skip to content
This repository
Newer
Older
100644 405 lines (377 sloc) 18.134 kb
fccc6851 » MLstate
2011-06-21 Initial open-source release
1 (*
2 Copyright © 2011 MLstate
3
4 This file is part of OPA.
5
6 OPA is free software: you can redistribute it and/or modify it under the
7 terms of the GNU Affero General Public License, version 3, as published by
8 the Free Software Foundation.
9 OPA is distributed in the hope that it will be useful, but WITHOUT ANY
10 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
11 FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
12 more details.
13
14 You should have received a copy of the GNU Affero General Public License
15 along with OPA. If not, see <http://www.gnu.org/licenses/>.
16 *)
17 module Q = QmlAst
18 module List = BaseList
19 module Format = BaseFormat
20
21 module IdentAssoc = List.MakeAssoc(Ident)
22
23 exception InvalidRecursion
24
25 let map_intersection merge_value map1 map2 =
26 IdentMap.fold
27 (fun k v1 acc ->
28 try let v2 = IdentMap.find k map2 in
29 IdentMap.add k (merge_value v1 v2) acc
30 with Not_found ->
31 acc
32 ) map1 IdentMap.empty
33
34 (* this function takes a binding (from a recursive set of bindings)
35 * and distinguishes 3 cases:
36 * - the expression is tagged with @recval (coming from rec val or and val in the syntax)
37 * returns Some of a map from the direct dependencies of this expression on the other
38 * identifiers of the bindings of their positions
39 * - the expression is a lambda -> return None
40 * - in other cases, the recursion is invalid, and the InvalidRecursion is raised
41 *)
42 let is_a_val_binding idents (_i, e) =
43 let merge_value = (@) in
44 let find_deps e =
45 QmlAstWalk.Expr.self_traverse_fold
46 (fun self tra deps e ->
47 match e with
48 | Q.Ident (label, i) when IdentSet.mem i idents -> IdentMap.add i [Annot.pos label] deps
49 | Q.Match (_, e, pel) -> (
50 let deps = self deps e in
51 let depss = List.map (fun (_p,e) -> self IdentMap.empty e) pel in
52 match depss with
53 | [] -> assert false
54 | h :: t ->
55 (* we can sure that we depend on an identifier only if all the
56 * branches depend on that identifier
57 * hence we must take the intersection of the dependencies of the branches
58 * and NOT their union *)
59 let intersection = List.fold_left (map_intersection merge_value) h t in
60 IdentMap.merge merge_value intersection deps
61 )
62 | Q.Lambda _ ->
63 deps
64 | _ ->
65 tra deps e
66 ) IdentMap.empty e in
67 let rec is_a_val = function
68 | Q.Lambda _ -> None
69 | Q.Directive (_, `recval, [e], _) ->
70 (* checking that you don't put a val rec on a function *)
71 (try match is_a_val e with
72 | None ->
73 (* FIXME: should be a warning *)
74 let context = QmlError.Context.expr e in
75 QmlError.error context
76 "This expression is a function, it can be recursive without being tagged with 'val'."
77 | Some _ -> () (* could be an assert failure? *)
78 with InvalidRecursion -> ());
79 Some (find_deps e)
80 | Q.Directive (_, `recval, _, _) -> assert false
81 | Q.Coerce (_, e, _)
82 (* BEWARE before editing: keep this set of directive in sync with the one
83 * in remove_toplevel_directives *)
8edc0012 » Valentin Gatien-Baron
2011-07-06 [feature] adding: an @async directive on bindings to perform asynchro…
84 | Q.Directive (_, (#Q.type_directive | #Q.slicer_directive | `async), [e], _) -> is_a_val e
fccc6851 » MLstate
2011-06-21 Initial open-source release
85 | _ -> raise InvalidRecursion in
86 is_a_val e
87
88 let lazy_type gamma var =
89 let typeident = Q.TypeIdent.of_string Opacapi.Types.finite_single_thread_lazy in
90 let (typeident, _) = QmlTypes.Env.TypeIdent.findi ~visibility_applies:true typeident gamma in
91 (* grabbing the typeident from the gamma, or else we might have the infamous
92 * assert failure somewhere in the typer saying "call type_of_type" *)
93 Q.TypeName ([var], typeident)
94 let lazy_force_type gamma var =
95 Q.TypeArrow ([lazy_type gamma var], var)
96 let mutable_make_type gamma ty =
97 let var = QmlAstCons.Type.next_var () in
98 Q.TypeArrow ([var], lazy_type gamma ty)
99 let mutable_set_type gamma ty =
100 Q.TypeArrow ([lazy_type gamma ty; ty], Q.TypeRecord (Q.TyRow ([], None)))
101
102 let force ~val_ gamma annotmap label lazy_i =
103 let lazy_force = val_ Opacapi.FiniteSingleThreadLazy.force in
104 let ty = QmlAnnotMap.find_ty_label label annotmap in
105 let annotmap, force = QmlAstCons.TypedExpr.ident annotmap lazy_force (lazy_force_type gamma ty) in
106 let annotmap, lazy_i_expr = QmlAstCons.TypedExpr.ident annotmap lazy_i (lazy_type gamma ty) in
107 let annotmap, forced_lazy = QmlAstCons.TypedExpr.apply gamma annotmap force [lazy_i_expr] in
108 annotmap, forced_lazy
109
110 let partition_map p l =
111 let rec aux acc1 acc2 = function
112 | [] -> List.rev acc1, List.rev acc2
113 | h :: t ->
114 match p h with
115 | None -> aux acc1 (h :: acc2) t
116 | Some v -> aux ((h, v) :: acc1) acc2 t in
117 aux [] [] l
118
119 let rec drop_until p = function
120 | [] -> None, []
121 | h :: t ->
122 if p h then
123 Some h, t
124 else
125 drop_until p t
126
127 (* simple check to reject at compile time some cases of illegal value recursion
128 * such as [val rec x = x] *)
129 let check_lack_of_cycle val_deps_bindings =
130 let val_deps = List.map (fun ((i,_e),deps) -> (i,deps)) val_deps_bindings in
131 let pos_of_def i =
132 let (_, e), _ = List.find (fun ((j,_),_) -> Ident.equal i j) val_deps_bindings in
133 Q.Pos.expr e in
134 let rec aux occur i posl =
135 if IdentAssoc.mem i occur then (
136 (* the dependencies that cause the immediate loop *)
137 let calls = List.rev ((i,posl) :: occur) in
138 (* the relevant part of the dependencies *)
139 let _, calls = drop_until (fun (j,_) -> Ident.equal i j) calls in
140 OManager.serror "@[<v>%a@]@\n@[<v2>Invalid recursive value binding: @{<bright>%s@} depends on itself@]@\n@[<v2>Hint:@ Here is the chain of immediate dependencies:@ %a@]"
141 FilePos.pp (pos_of_def i)
142 (Ident.original_name i)
143 (Format.pp_list "@\n"
144 (fun f (i,posl) ->
145 (* we have several positions when there are branching,
146 * but perhaps it gives too much information to show all
147 * the positions *)
148 let pos = List.hd posl in
149 Format.fprintf f "@[<v2>%s at %a@]" (Ident.original_name i) FilePos.pp pos
150 )) calls;
151 (* exiting to give only one error message in the recursive group *)
152 raise InvalidRecursion
153 ) else
154 let occur = (i,posl) :: occur in
155 (* only non lambda bindings are in val_deps, so we can get a Not_found here *)
156 let deps = try IdentAssoc.find i val_deps with Not_found -> IdentMap.empty in
157 IdentMap.iter (aux occur) deps in
158 try
159 List.iter
160 (fun (i,_) -> aux [] i [])
161 val_deps
162 with InvalidRecursion -> ()
163
164 let move_ei_tsc_gen label annotmap e =
165 let tsc_gen_opt = QmlAnnotMap.find_tsc_opt_label label annotmap in
166 assert (QmlAnnotMap.find_tsc_opt (Q.QAnnot.expr e) annotmap = None);
167 QmlAnnotMap.add_tsc_opt (Q.QAnnot.expr e) tsc_gen_opt annotmap
168
169 (* now the typing directive are just freaking annoying, because there may be
170 * more slicer directives under them so let's remove them *)
171 let remove_toplevel_directives annotmap e =
172 let rec aux dirs annotmap = function
173 | Q.Coerce (label, e, _)
174 | Q.Directive (label, #Q.type_directive, [e], _) ->
175 let annotmap = move_ei_tsc_gen label annotmap e in
176 aux dirs annotmap e
8edc0012 » Valentin Gatien-Baron
2011-07-06 [feature] adding: an @async directive on bindings to perform asynchro…
177 | Q.Directive (label, (#Q.slicer_directive | `async as v), [e], []) ->
fccc6851 » MLstate
2011-06-21 Initial open-source release
178 let annotmap = move_ei_tsc_gen label annotmap e in
179 aux (v :: dirs) annotmap e
180 | Q.Directive (_, #Q.slicer_directive, _, _) -> assert false
181 | e -> annotmap, dirs, e in
182 aux [] annotmap e
183
184 let rec put_back_toplevel_directives annotmap dirs e =
185 match dirs with
186 | [] -> annotmap, e
187 | dir :: dirs ->
188 let label = Q.Label.expr e in
189 let new_label = Annot.refresh label in
190 let ty = QmlAnnotMap.find_ty_label label annotmap in
191 let tsc_gen_opt = QmlAnnotMap.find_tsc_opt_label label annotmap in
192 let annotmap = QmlAnnotMap.remove_tsc_label label annotmap in
193 let annotmap = QmlAnnotMap.add_ty_label new_label ty annotmap in
194 let annotmap = QmlAnnotMap.add_tsc_opt_label new_label tsc_gen_opt annotmap in
195 let e = Q.Directive (new_label, dir, [e], []) in
196 put_back_toplevel_directives annotmap dirs e
197
198 (*
199 * rewrites [rec val x = e1
200 * and f() = e2]
201 * into
202 * [lazy_x = mutable_make(0)
203 * rec f() = e2[lazy_force(lazy_x) / x ]
204 * _ = mutable_set(lazy_x, ( -> e1[lazy_force(lazy_x) / x ]))
205 * x = lazy_force(lazy_x)
206 * ]
207 * The only expressions in the recursive bindings after this rewriting are lambdas
208 * (modulo coercions, some directives, etc.)
209 *)
210 let process_bindings ~val_ gamma annotmap bindings =
211 let idents = List.fold_left (fun acc (i,_) -> IdentSet.add i acc) IdentSet.empty bindings in
212
213 let invalid_bindings = ref [] in
214 let val_deps_bindings, fun_bindings =
215 partition_map
216 (fun b ->
217 try is_a_val_binding idents b
218 with InvalidRecursion ->
219 invalid_bindings := b :: !invalid_bindings;
220 None
221 ) bindings in
222 if !invalid_bindings <> [] then (
223 (match bindings with
224 | [(i,e)] ->
225 (* a more concise error message in the common case of not mutual recursion *)
226 let context = QmlError.Context.expr e in
227 QmlError.serror context "@[<v2> The recursive definition of @{<bright>%s@} is invalid." (Ident.original_name i)
228 | _ ->
229 OManager.serror "@[<v2>In the recursive group consisting of {@[<h>%a@]}, the following recursive definitions are invalid:@\n%a@]@\n@]"
230 (Format.pp_list ",@ " (fun f i -> Format.pp_print_string f (Ident.original_name i))) (IdentSet.elements idents)
231 (Format.pp_list "@ " (fun f (i,e) -> Format.fprintf f "@{<bright>%s@} at %a" (Ident.original_name i) FilePos.pp (Q.Pos.expr e))) !invalid_bindings
232 );
233 None
234 ) else (
235 check_lack_of_cycle val_deps_bindings;
236 let val_bindings = List.map fst val_deps_bindings in
237 if val_bindings = [] then
238 None
239 else (
240 let mutable_make = val_ Opacapi.Mutable.make in
241 let mutable_set = val_ Opacapi.Mutable.set in
242
243 (* when we write @server rec val x = ..., then we remove the directive
244 * @server from the body of x and we will put it on all the toplevel
245 * bindings generated from x *)
246 let annotmap, val_bindings =
247 List.fold_left_map
248 (fun annotmap (i,e) ->
249 let annotmap, dirs, e = remove_toplevel_directives annotmap e in
250 annotmap, (i, e, dirs)
251 ) annotmap val_bindings in
252 let lazy_idents = List.map (fun (i,_,_) -> Ident.refreshf ~map:"lazy_%s" i) val_bindings in
253 let annotmap, lazy_defs =
254 List.fold_left_map2
255 (fun annotmap i (_,e,dirs) ->
256 let ty = QmlAnnotMap.find_ty (Q.QAnnot.expr e) annotmap in
257 let annotmap, mutable_make = QmlAstCons.TypedExpr.ident annotmap mutable_make (mutable_make_type gamma ty) in
258 (* could put a well typed value if needed (like {evaluating}) *)
259 let annotmap, zero = QmlAstCons.TypedExpr.int annotmap 7 in
260 let annotmap, def = QmlAstCons.TypedExpr.apply gamma annotmap mutable_make [zero] in
261 let annotmap, def = put_back_toplevel_directives annotmap dirs def in
262 annotmap, (i, def)
263 ) annotmap lazy_idents val_bindings in
264 let annotmap, lazy_sets =
265 List.fold_left_map2
266 (fun annotmap i (_, e, dirs) ->
267 let ty = QmlAnnotMap.find_ty (Q.QAnnot.expr e) annotmap in
268 let annotmap, mutable_set = QmlAstCons.TypedExpr.ident annotmap mutable_set (mutable_set_type gamma ty) in
269 let annotmap, lambda = QmlAstCons.TypedExpr.lambda annotmap [] e in
270 let annotmap, lazy_body = QmlAstCons.TypedExpr.sum_element annotmap ["delayed", lambda] in
271 let annotmap, ref_ = QmlAstCons.TypedExpr.ident annotmap i (lazy_type gamma ty) in
272 let annotmap, set = QmlAstCons.TypedExpr.apply gamma annotmap mutable_set [ref_; lazy_body] in
273 let annotmap, set = put_back_toplevel_directives annotmap dirs set in
274 annotmap, (Ident.next "set_lazy", set)
275 ) annotmap lazy_idents val_bindings in
276 let annotmap, original_bindings =
277 List.fold_left_map2
278 (fun annotmap lazy_i (i, e, dirs) ->
279 let annotmap, forced_lazy = force ~val_ gamma annotmap (Q.Label.expr e) lazy_i in
280 let annotmap, forced_lazy = put_back_toplevel_directives annotmap dirs forced_lazy in
281 annotmap, (i, forced_lazy)
282 ) annotmap lazy_idents val_bindings in
283 let assoc_ident = List.map2 (fun lazy_i (i,_,_) -> (i,lazy_i)) lazy_idents val_bindings in
284 let rewrite_binding annotmap (i,e) =
285 let annotmap, e = QmlAstWalk.Expr.traverse_foldmap
286 (fun tra annotmap e ->
287 match e with
288 | Q.Ident (label, i) -> (
289 try
290 let lazy_i = IdentAssoc.find i assoc_ident in
291 force ~val_ gamma annotmap label lazy_i
292 with Not_found ->
293 annotmap, e
294 )
295 | _ -> tra annotmap e
296 ) annotmap e in
297 annotmap, (i, e) in
298 let rewrite_bindings annotmap l =
299 List.fold_left_map rewrite_binding annotmap l in
300 let annotmap, lazy_sets = rewrite_bindings annotmap lazy_sets in
301 let annotmap, fun_bindings = rewrite_bindings annotmap fun_bindings in
302 Some (
303 annotmap,
304 lazy_defs,
305 (if fun_bindings = [] then None else Some fun_bindings),
306 lazy_sets,
307 original_bindings
308 )
309 )
310 )
311
312 let process_bindings_for_toplevel ~val_ gamma annotmap label bindings =
313 match process_bindings ~val_ gamma annotmap bindings with
314 | None ->
315 None
316 | Some (annotmap, lazy_defs, fun_bindings_opt, lazy_sets, original_bindings) ->
317 let code =
318 Q.NewVal (Annot.refresh label, lazy_sets) ::
319 Q.NewVal (Annot.refresh label, original_bindings) ::
320 [] in
321 let code =
322 match fun_bindings_opt with
323 | None -> code
324 | Some fun_bindings -> Q.NewValRec (Annot.refresh label, fun_bindings) :: code in
325 let code = Q.NewVal (Annot.refresh label, lazy_defs) :: code in
326 let add_to_gamma gamma bindings =
327 List.fold_left
328 (fun gamma (i,e) ->
329 let tsc = QmlTypes.Scheme.quantify (QmlAnnotMap.find_ty (Q.QAnnot.expr e) annotmap) in
330 QmlTypes.Env.Ident.add i tsc gamma
331 ) gamma bindings in
332 let gamma = add_to_gamma gamma lazy_defs in
333 let gamma = add_to_gamma gamma lazy_sets in
334 Some (gamma, annotmap, code)
335
336 let process_code ~val_ gamma annotmap code =
337
338 (* rewriting newvalrec *)
339 let (gamma, annotmap), code =
340 List.fold_left_collect
341 (fun (gamma, annotmap) c ->
342 match c with
343 | Q.NewValRec (label, bindings) -> (
344 match process_bindings_for_toplevel ~val_ gamma annotmap label bindings with
345 | None -> (gamma, annotmap), [c]
346 | Some (gamma, annotmap, code) -> (gamma, annotmap), code
347 )
348 | _ -> (gamma, annotmap), [c]
349 ) (gamma, annotmap) code in
350
351 (* rewriting letrec and removing @recval *)
352 let annotmap, code =
353 QmlAstWalk.CodeExpr.fold_map
354 (QmlAstWalk.Expr.self_traverse_foldmap
355 (fun self tra annotmap e ->
356 match e with
357
358 | Q.LetRecIn (label, bindings, e_in) -> (
359 match process_bindings ~val_ gamma annotmap bindings with
360 | None -> tra annotmap e
361 | Some (annotmap, lazy_defs, fun_bindings_opt, lazy_sets, original_bindings) ->
362 let label2 = Annot.refresh label in
363 let label4 = Annot.refresh label in
364 let label5 = Annot.refresh label in
365 (* not copying the information for ei *)
366 let ty = QmlAnnotMap.find_ty_label label annotmap in
367 let annotmap = QmlAnnotMap.add_ty_label label2 ty annotmap in
368 let annotmap = QmlAnnotMap.add_ty_label label4 ty annotmap in
369 let annotmap = QmlAnnotMap.add_ty_label label5 ty annotmap in
370 let e_in =
371 Q.LetIn (label2, lazy_sets,
372 Q.LetIn (label, original_bindings, e_in)) in
373 let e_in =
374 match fun_bindings_opt with
375 | None -> e_in
376 | Some fun_bindings -> Q.LetRecIn (label4, fun_bindings, e_in) in
377 let e_in =
378 Q.LetIn (label5, lazy_defs, e_in) in
379 (* need to go down to rewrite e_in and lazy_sets
380 * (although we could just rewrite them instead of calling ourselves
381 * recursively on the term produced) *)
382 tra annotmap e_in
383 )
384
385 | Q.Directive (label, `recval, [e], []) ->
386 (* it is possible that we have a recval on a let that is not recursive
387 * for instance when we say [rec val x = 1] because the dependency analysis
388 * will transform newvalrec and letrec into newval and letin if possible
389 * also other rewriting (such as the one for let pattern = expr in expr)
390 * may duplicate @recval and put them in not quite legal places, so i prefer
391 * not to give an error and ignore everything *)
392 (* cannot instantiate on a recval, but it has possibly been generalized *)
393 assert (QmlAnnotMap.find_tsc_inst_opt_label label annotmap = None);
394 let annotmap = QmlAnnotMap.add_tsc_opt (Q.QAnnot.expr e) (QmlAnnotMap.find_tsc_opt_label label annotmap) annotmap in
395 self annotmap e
396
397 | Q.Directive (_, `recval, _, _) ->
398 assert false
399
400 | _ -> tra annotmap e
401
402 )
403 ) annotmap code in
404
405 gamma, annotmap, code
Something went wrong with that request. Please try again.