Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 543 lines (506 sloc) 19.478 kB
fccc685 Initial open-source release
MLstate authored
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
10 OPA is distributed in the hope that it will be useful, but WITHOUT ANY
11 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
12 FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
13 more details.
14
15 You should have received a copy of the GNU Affero General Public License
16 along with OPA. If not, see <http://www.gnu.org/licenses/>.
17 *)
18
19 (* depends *)
20 module List = BaseList
21
22 (* shorthands *)
23 module Q = QmlAst
24
25 let next =
26 let r = ref 0 in
27 fun () -> incr r; !r
28
29 module type S =
30 sig
31 type effect
32 val join_effect : effect -> effect -> effect
33 val effect_of : [`bypass of BslKey.t] -> effect
34 val no_effect : effect
35 val all_effects : effect
36 val to_string : effect -> string
37 end
38
39 module type E =
40 sig
41 type effect
42 type effects
43 type typ
44 val string_of_typ : typ -> string
45 val flatten_effect : effects -> effect
46
47 type env = (effects IdentMap.t * typ IdentMap.t)
48 val infer_code : ?initial_env:env -> (BslKey.t -> Q.ty) -> Q.code -> env
49 end
50
51 module EffectAnalysis(S:S) : E with type effect = S.effect =
52 struct
53 type level = int
54 type effect = S.effect
55 type var =
56 | Fresh of level ref * int
57 | Unified of typ
58 and typ =
59 | Var of var ref
60 | Dontcare
61 | Arrow of typ list * effects * typ
62 and effects = effect * effect_var ref
63 and effect_var =
64 | EFresh of level ref * int
65 | EUnified of effects
66
67 let join_effects = S.join_effect
68
69 let rec flatten_effect_aux (eff, v) =
70 match !v with
71 | EFresh (_,v) -> eff, v
72 | EUnified (eff2, v2) -> flatten_effect_aux (join_effects eff eff2, v2)
73 let flatten_effect e = fst (flatten_effect_aux e)
74
75 let rec string_of_typ = function
76 | Var v ->
77 (match !v with
78 | Fresh (lev,_) -> "_" ^ string_of_int !lev
79 | Unified ty -> string_of_typ ty)
80 | Dontcare ->
81 "dontcare"
82 | Arrow (tyl,e,ty) ->
83 let sl = String.concat " -> " (List.map string_of_typ tyl) in
84 let s = string_of_typ ty in
85 let eff, var = flatten_effect_aux e in
86 "(" ^ sl ^ " " ^ string_of_int var ^ (S.to_string eff) ^ "->" ^ " " ^ s ^ ")"
87
88 let rec traverse_normalize tra = function
89 | Dontcare
90 | Var {contents = Fresh _ } as ty -> ty
91 | Var {contents = Unified ty} -> traverse_normalize tra ty
92 | Arrow (typs,effects,typ) -> Arrow (List.map tra typs,traverse_normalize_eff effects,tra typ)
93 and traverse_normalize_eff ((l,v) as p) =
94 match !v with
95 | EFresh _ -> p
96 | EUnified (l2,v2) -> traverse_normalize_eff (join_effects l l2, v2)
97 let shallow_normalize ty = traverse_normalize (fun x -> x) ty
98 let rec normalize ty = traverse_normalize normalize ty
99
100 let rec occur_check v = function
101 | Dontcare -> ()
102 | Var v' ->
103 if v == v' then failwith "Cyclic unification"
104 else
105 (match !v' with
106 | Fresh _ -> ()
107 | Unified ty -> occur_check v ty)
108 | Arrow (tyl,_,ty) ->
109 List.iter (occur_check v) tyl;
110 occur_check v ty
111
112 let generic_level = -1
113
114 let rec set_max_level max_level = function
115 | Dontcare -> ()
116 | Arrow (tyl,_,ty) ->
117 List.iter (set_max_level max_level) tyl;
118 set_max_level max_level ty
119 | Var v ->
120 match !v with
121 | Fresh (lev,_) ->
122 if !lev <> generic_level then
123 if !lev > max_level then
124 lev := max_level
125 | Unified ty -> set_max_level max_level ty
126
127 let rec unify ty1 ty2 =
128 if ty1 == ty2 then () else (
129 let ty1 = shallow_normalize ty1 in
130 let ty2 = shallow_normalize ty2 in
131 if ty1 == ty2 then () else (
132 match ty1, ty2 with
133 | Var v1, Var v2 ->
134 let lev1 = (match !v1 with Fresh (lev1, _) -> lev1 | _ -> assert false) in
135 let lev2 = (match !v2 with Fresh (lev2, _) -> lev2 | _ -> assert false) in
136 v2 := Unified ty1;
137 lev1 := min !lev1 !lev2
138 | Var v, ty
139 | ty, Var v ->
140 occur_check v ty;
141 set_max_level (match !v with Fresh (lev, _) -> !lev | _ -> assert false) ty;
142 v := Unified ty
143 | Arrow (tyl1,(l1, r1),ret1), Arrow (tyl2,(l2, r2),ret2) ->
144 let lev1 = (match !r1 with EFresh (r,_) -> !r | _ -> assert false) in
145 let lev2 = (match !r2 with EFresh (r,_) -> !r | _ -> assert false) in
146 let r3 = ref (EFresh (ref (min lev1 lev2), next())) in
147 r1 := EUnified (l2, r3);
148 r2 := EUnified (l1, r3);
149 List.iter2 unify tyl1 tyl2;
150 unify ret1 ret2
151 | Dontcare, Dontcare ->
152 ()
153 | Dontcare, Arrow (tyl,(_,r),ty)
154 | Arrow (tyl,(_,r),ty), Dontcare ->
155 (*Printf.printf "Loss of precision: unifying %s and %s\n%!"
156 (string_of_typ ty1) (string_of_typ ty2);*)
157 (match !r with
158 | EFresh (lev,_) ->
159 let r2 = ref (EFresh (lev, next())) in
160 r := EUnified (S.all_effects, r2);
161 List.iter (unify Dontcare) tyl;
162 unify Dontcare ty
163 | _ -> assert false)
164 )
165 )
166
167 let rec instantiate level ((varmap,effmap) as map) = function
168 | Dontcare -> map, Dontcare
169 | Var {contents = Fresh (this_level,i)} as ty ->
170 (try map, IntMap.find i varmap
171 with Not_found ->
172 if !this_level = generic_level then
173 let v = Var (ref (Fresh (ref level, next ()))) in
174 (IntMap.add i v varmap,effmap), v
175 else
176 map, ty)
177 | Var {contents = Unified ty} ->
178 instantiate level map ty
179 | Arrow (tyl,effects,ty) ->
180 let map, tyl = List.fold_left_map (instantiate level) map tyl in
181 let (varmap, effmap), ty = instantiate level map ty in
182 let effmap, effects = instantiate_eff level effmap effects in
183 (varmap, effmap), Arrow (tyl, effects, ty)
184 and instantiate_eff level effmap (l,v) =
185 match !v with
186 | EFresh (this_level,i) ->
187 (try effmap, (l, IntMap.find i effmap)
188 with Not_found ->
189 if !this_level = generic_level then
190 let v = ref (EFresh (ref level, next())) in
191 IntMap.add i v effmap, (l, v)
192 else
193 effmap, (l, v))
194 | EUnified (l2,v2) -> instantiate_eff level effmap (join_effects l l2, v2)
195 let instantiate level ty =
196 snd (instantiate level (IntMap.empty,IntMap.empty) ty)
197
198 let rec generalize level = function
199 | Var v ->
200 (match !v with
201 | Fresh (this_level,_) ->
202 if !this_level <> generic_level && !this_level > level then
203 this_level := generic_level
204 | Unified ty -> generalize level ty)
205 | Dontcare -> ()
206 | Arrow (tyl,effects,ty) ->
207 List.iter (generalize level) tyl;
208 generalize level ty;
209 generalize_eff level effects
210 and generalize_eff level (_,v) =
211 match !v with
212 | EFresh (this_level,_) ->
213 if !this_level <> generic_level && !this_level > level then
214 this_level := generic_level
215 | EUnified eff -> generalize_eff level eff
216
217 let next_var level = Var (ref (Fresh (ref level, next())))
218 let next_eff_var level = ref (EFresh (ref level, next()))
219
220 let infer_pattern env p level =
221 QmlAstWalk.Pattern.fold_down
222 (fun env -> function
223 | Q.PatVar (_, i) | Q.PatAs (_, _, i) ->
224 IdentMap.add i (next_var level) env
225 | _ -> env) env p
226
227 let rec convert_type varmap level = function
228 | Q.TypeArrow (tyl,ty) ->
229 Arrow (List.map (convert_type varmap level) tyl, (S.no_effect, next_eff_var level), convert_type varmap level ty)
230 | Q.TypeVar v ->
231 (try QmlTypeVars.TypeVarMap.find v !varmap
232 with Not_found ->
233 let v2 = next_var level in
234 varmap := QmlTypeVars.TypeVarMap.add v v2 !varmap;
235 v2)
236 | _ ->
237 Dontcare
238
239 (* need to know whether we are in covariant or contravariant positions
240 * but since no bypass ever returns a function, well ... *)
241 let rewrite_arrow level effect ty =
242 let varmap = ref QmlTypeVars.TypeVarMap.empty in
243 match ty with
244 | Q.TypeArrow (tyl,ty) ->
245 Arrow (List.map (convert_type varmap level) tyl, (effect, next_eff_var level), convert_type varmap level ty)
246 | ty -> convert_type varmap level ty
247
248 let rec infer bp env effect level e =
249 try
250 let ty =
251 match e with
252 | Q.Const _ -> Dontcare
253 | Q.Ident (_, i) ->
254 (try instantiate level (IdentMap.find i env)
255 with Not_found -> Printf.printf "Not found %s\n%!"
256 (Ident.to_string i);
257 assert false)
258 | Q.LetIn (_, iel,e) ->
259 let env =
260 List.fold_left
261 (fun new_env (i,e) ->
262 let ty = infer bp env effect (level+1) e in
263 generalize level ty;
264 IdentMap.add i ty new_env) env iel in
265 infer bp env effect (level+1) e
266 | Q.LetRecIn (_, iel, e) ->
267 let itys = List.map (fun (i,_) -> (i,next_var (level+1))) iel in
268 let env = List.fold_left (fun env (i,ty) -> IdentMap.add i ty env) env itys in
269 let tys' = List.map (fun (_,e) -> infer bp env effect (level+1) e) iel in
270 List.iter2 (fun (_,ty) ty' -> unify ty ty') itys tys';
271 List.iter (generalize level) tys';
272 infer bp env effect (level+1) e
273 | Q.Lambda (_, sl, e) ->
274 let styl = List.map (fun s -> (s, next_var level)) sl in
275 let env =
276 List.fold_left
277 (fun env (s,ty) -> IdentMap.add s ty env) env styl in
278 let effect = next_eff_var level in
279 let ty = infer bp env effect (level+1) e in
280 Arrow (List.map snd styl, (S.no_effect,effect), ty)
281 | Q.Directive (_, `partial_apply missing, [e], _) -> (
282 let missing = Option.get missing in
283 match e with
284 | Q.Apply (_, e, el) ->
285 (* no change on the current effect, since it is a partial
286 * application *)
287 let arrow_ty = infer bp env effect level e in
288 let tyl = List.map (infer bp env effect level) el in
289 let missing_types = List.init missing (fun _ -> next_var level) in
290 let ret_ty = next_var level in
291 let new_effect = (S.no_effect,next_eff_var level) in
292 unify (Arrow (tyl @ missing_types,new_effect,ret_ty)) arrow_ty;
293 Arrow (missing_types,new_effect,ret_ty)
294 | _ -> assert false
295 )
296 | Q.Apply (_, e, el) ->
297 let arrow_ty = infer bp env effect (level+1) e in
298 let tyl = List.map (infer bp env effect (level+1)) el in
299 let ret_ty = next_var level in
300 unify (Arrow (tyl,(S.no_effect,effect),ret_ty)) arrow_ty;
301 ret_ty
302 | Q.Match (_, e, pel) ->
303 (* not sure about that node *)
304 let ___TY = infer bp env effect (level+1) e in
305 let infer_rule env (p,e) =
306 let env = infer_pattern env p level in
307 infer bp env effect (level+1) e in
308 (match pel with
309 | [] -> assert false
310 | rule_ :: pel ->
311 let ty = infer_rule env rule_ in
312 List.iter
313 (fun rule_ ->
314 let ty' = infer_rule env rule_ in
315 unify ty ty')
316 pel;
317 ty)
318 | Q.Record (_, sel) ->
319 List.iter (fun (_s,e) -> ignore (infer bp env effect (level+1) e)) sel;
320 Dontcare
321 | Q.Dot (_, e, _s) ->
322 ignore (infer bp env effect (level+1) e);
323 Dontcare (* not quite good, will have troubles with higher order *)
324 | Q.ExtendRecord (_, _s, e1, e2) ->
325 ignore (infer bp env effect (level+1) e1);
326 ignore (infer bp env effect (level+1) e2);
327 Dontcare
328 | Q.Bypass (_, b) ->
329 (* call a bypass typer, and add side effect to the arrow *)
330 let qty = bp b in
331 let its_effect = S.effect_of (`bypass b) in
332 (*Format.printf "%s has type %a and effect %s@."
333 (BslKey.to_string b) QmlPrint.pp#ty qty (S.to_string its_effect);*)
334 rewrite_arrow level its_effect qty
335 | Q.Coerce (_, e, _) ->
336 infer bp env effect (level+1) e
337 | Q.Path (_, el, _) ->
338 List.iter (function
339 | Q.ExprKey e -> ignore (infer bp env effect (level+1) e)
340 | _ -> ()) el;
341 Dontcare
342 | Q.Directive (_, `fail, el, _) ->
343 List.iter (fun e -> ignore (infer bp env effect level e)) el;
344 next_var level
345 | Q.Directive (_, ( `restricted_bypass _
346 | `expanded_bypass
347 | #Q.type_directive
348 | `recval
349 | #Q.slicer_directive
350 | `partial_apply _
351 | `lifted_lambda _
352 | `full_apply _
353 | `assert_), l, _) -> (
354 match l with
355 | [e] -> infer bp env effect (level+1) e
356 | _ -> assert false
357 )
358 | Q.Directive (_, _, el, _) ->
359 (* there should be different categories here, we care about some directives
360 * and most of the time, the type is 'a -> 'a so we don't want to lose it! *)
361 List.iter (fun e -> ignore (infer bp env effect (level+1) e)) el;
362 Dontcare in
363 (*Format.printf "%a -> %s@." QmlPrint.pp#expr e (string_of_typ ty);*)
364 ty
365 with exn ->
366 let context = QmlError.Context.expr e in
367 QmlError.serror context "QmlEffect error@.";
368 raise exn
369
370 type env = (effects IdentMap.t * typ IdentMap.t)
371 let infer_code ?(initial_env=(IdentMap.empty, IdentMap.empty)) bp code =
372 List.fold_left
373 (fun ((_,env) as full_env) ->
374 function
375 | Q.NewVal (_,iel) ->
376 let level = 0 in
377 List.fold_left
378 (fun (env_effect,last_env) (i,e) ->
379 let effect = next_eff_var generic_level in
380 let ty = infer bp env effect (level+1) e in
381 generalize level ty;
382 let last_env = IdentMap.add i ty last_env in
383 let env_effect = IdentMap.add i (S.no_effect,effect) env_effect in
384 #<If:EFFECTS_SHOW> Printf.printf "%s has type %s with effect %s\n%!" (Ident.to_string i) (string_of_typ ty) (S.to_string (flatten_effect (S.no_effect,effect)))#<End>;
385 env_effect, last_env
386 ) full_env iel
387 | Q.NewValRec (_,iel) ->
388 let level = 0 in
389 let itys = List.map (fun (i,_) -> (i,next_var (level+1))) iel in
390 let full_env = List.fold_left (fun (env_effect,env) (i,ty) -> (env_effect,IdentMap.add i ty env)) full_env itys in
391 let full_env, tys' = List.fold_left_map
392 (fun (env_effect,env) (i,e) ->
393 let effect = next_eff_var generic_level in
394 let ty = infer bp env effect (level+1) e in
395 let env = IdentMap.add i ty env in
396 let env_effect = IdentMap.add i (S.no_effect,effect) env_effect in
397 (env_effect, env), ty
398 ) full_env iel in
399 List.iter2 (fun (_i,ty) ty' -> unify ty ty') itys tys';
400 List.iter (generalize level) tys';
401 #<If:EFFECTS_SHOW> List.iter (fun (i,ty) -> Printf.printf "%s has type %s\n%!" (Ident.to_string i) (string_of_typ ty)) itys#<End>;
402 full_env
403 | _ -> assert false
404 )
405 initial_env
406 code
407 end
408
409 let effect_of' = function
410 | `bypass s ->
411 (* FIXME: this reminds me the dark days when we have no bsl
412 and huge list of bypass floating around
413 it should be replaced by a bypass property
414 it affects the way bypass interacts slicer
415 two bypass with the exactly the same definition have different behaviour
416 which is totally misleading *)
417 match BslKey.to_string s with
418 | "bslpervasives_int_neg"
419 | "bslpervasives_int_add"
420 | "bslpervasives_int_sub"
421 | "bslpervasives_int_mul"
422 | "bslpervasives_int_div"
423 | "bslpervasives_float_neg"
424 | "bslpervasives_float_add"
425 | "bslpervasives_float_sub"
426 | "bslpervasives_float_mul"
427 | "bslpervasives_float_div"
428 | "bslstring_concat"
429 | "bslstring_of_int"
430 | "bsltime_local_format"
431 | "bslpervasives_compare_int"
432 | "bslpervasives_compare_string"
433 | "bslpervasives_compare_char"
434 | "bslpervasives_compare_float"
435 | "bslpervasives_int_cmp_eq"
436 | "bslpervasives_int_cmp_neq"
437 | "bslpervasives_int_cmp_leq"
438 | "bslpervasives_int_cmp_lneq"
439 | "bslpervasives_int_cmp_gneq"
440 | "bslpervasives_int_cmp_geq"
441 | "bslvalue_tsc_get"
442 | "bslpervasives_magic_id"
443 | "bslvalue_record_name_of_field"
444 | "bslvalue_record_field_of_name"
445 | "bslnumber_int_of_float"
446 | "bslnumber_int_of_string"
447 | "bslnumber_float_of_int"
448 | "bslpervasives_string_of_char"
449 | "bslnumber_float_to_string"
450 | "bslpervasives_dump"
451 | "bslvalue_record_fold_record"
452 | "bslvalue_record_fold_2_record"
453 | "bslvalue_record_empty_constructor"
454 | "bslvalue_record_add_field"
455 | "bslvalue_record_make_record"
456 | "bslvalue_record_make_simple_record"
457 | "bslnumber_math_abs_f"
458 | "bslnumber_math_abs_i"
459 | "bslnumber_math_acos"
460 | "bslnumber_math_asin"
461 | "bslnumber_math_atan"
462 | "bslnumber_math_ceil"
463 | "bslnumber_math_cos"
464 | "bslnumber_math_exp"
465 | "bslnumber_math_floor"
466 | "bslnumber_math_isnan"
467 | "bslnumber_math_is_infinite"
468 | "bslnumber_math_is_normal"
469 | "bslnumber_math_log"
470 | "bslnumber_math_sin"
471 | "bslnumber_math_sqrt_f"
472 | "bslnumber_math_sqrt_i"
473 | "bslnumber_math_tan"
474 | "bslnumber_int_ordering"
475 | "bslpervasives_webutils_server_side"
476 | "bslpervasives_aresameobject"
477 | "bslstring_check_match_literal"
478 | "bslstring_get"
479 | "bslpervasives_int_of_first_char"
480 | "bslnumber_int_op_asr"
481 | "bslnumber_int_op_lsr"
482 | "bslnumber_int_op_lsl"
483 | "bslnumber_int_op_lnot"
484 | "bslnumber_int_op_lxor"
485 | "bslnumber_int_op_lor"
486 | "bslnumber_int_op_land"
487 | "bslnumber_int_to_char"
488 | "bslpervasives_int_mod"
489 | "bslstring_sub"
490 | "bslstring_init" (* THIS ONE IS FALSE, no side effect if the given function
491 * has no side effect either *)
492 | "bslcactutf_cactutf_length"
493 | "bslstring_length"
494 | "sys_argv"
495 | "sys_argc"
496 ->
497 `pure
498
499 | "bsltime_now" ->
500 `read
501
502 | "bslpervasives_print_endline"
503 | "bslpervasives_print_string"
504 | "bslpervasives_prerr_string"
505 | "bslpervasives_print_int"
506 | "bslpervasives_jlog" ->
507 `write
508
509 | "bslreference_create" ->
510 `alloc
511
512 | "bslpervasives_error" -> (* accepting to clean errors *)
513 `error
514
515 | _ -> `impure
516
517 module SideEffectS =
518 struct
519 type effect = bool
520 let join_effect = (||)
521 let no_effect = false
522 let all_effects = true
523 let effect_of x =
524 match effect_of' x with
525 | `pure | `alloc | `read | `error -> false
526 | `impure | `write -> true
527 let to_string = function
528 | true -> "+"
529 | false -> ""
530 end
531
532 module SlicerEffectS =
533 struct
534 include SideEffectS
535 let effect_of x =
536 match effect_of' x with
537 | `pure | `write | `error -> false
538 | `impure | `alloc | `read -> true
539 end
540
541 module SideEffect = EffectAnalysis(SideEffectS)
542 module SlicerEffect = EffectAnalysis(SlicerEffectS)
Something went wrong with that request. Please try again.