Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/delay.ml | ||
---|---|---|
9 | 9 |
(* *) |
10 | 10 |
(********************************************************************) |
11 | 11 |
|
12 |
(** Types definitions and a few utility functions on delay types. |
|
13 |
Delay analysis by type polymorphism instead of constraints *) |
|
14 | 12 |
open Utils |
13 |
(** Types definitions and a few utility functions on delay types. Delay analysis |
|
14 |
by type polymorphism instead of constraints *) |
|
15 | 15 |
|
16 |
type delay_expr = |
|
17 |
{mutable ddesc: delay_desc; |
|
18 |
did: int} |
|
16 |
type delay_expr = { mutable ddesc : delay_desc; did : int } |
|
19 | 17 |
|
20 | 18 |
and delay_desc = |
21 | 19 |
| Dvar (* Monomorphic type variable *) |
22 | 20 |
| Dundef |
23 | 21 |
| Darrow of delay_expr * delay_expr |
24 | 22 |
| Dtuple of delay_expr list |
25 |
| Dlink of delay_expr (* During unification, make links instead of substitutions *) |
|
26 |
| Dunivar (* Polymorphic type variable *) |
|
27 |
type error = |
|
28 |
| Delay_clash of delay_expr * delay_expr |
|
23 |
| Dlink of delay_expr |
|
24 |
(* During unification, make links instead of substitutions *) |
|
25 |
| Dunivar |
|
26 |
(* Polymorphic type variable *) |
|
27 |
|
|
28 |
type error = Delay_clash of delay_expr * delay_expr |
|
29 | 29 |
|
30 | 30 |
exception Unify of delay_expr * delay_expr |
31 |
|
|
31 | 32 |
exception Error of Location.t * error |
32 | 33 |
|
33 | 34 |
let new_id = ref (-1) |
34 | 35 |
|
35 | 36 |
let new_delay desc = |
36 |
incr new_id; {ddesc = desc; did = !new_id } |
|
37 |
incr new_id; |
|
38 |
{ ddesc = desc; did = !new_id } |
|
37 | 39 |
|
38 |
let new_var () = |
|
39 |
new_delay Dvar |
|
40 |
let new_var () = new_delay Dvar |
|
40 | 41 |
|
41 |
let new_univar () = |
|
42 |
new_delay Dunivar |
|
42 |
let new_univar () = new_delay Dunivar |
|
43 | 43 |
|
44 |
let rec repr = |
|
45 |
function |
|
46 |
{ddesc = Dlink i'; _} -> |
|
47 |
repr i' |
|
48 |
| i -> i |
|
44 |
let rec repr = function { ddesc = Dlink i'; _ } -> repr i' | i -> i |
|
49 | 45 |
|
50 | 46 |
(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type |
51 | 47 |
(ensured by language syntax) *) |
52 | 48 |
let split_arrow de = |
53 | 49 |
match (repr de).ddesc with |
54 |
| Darrow (din,dout) -> din,dout |
|
55 |
(* Functions are not first order, I don't think the var case |
|
56 |
needs to be considered here *) |
|
57 |
| _ -> failwith "Internal error: not an arrow type" |
|
50 |
| Darrow (din, dout) -> |
|
51 |
din, dout |
|
52 |
(* Functions are not first order, I don't think the var case needs to be |
|
53 |
considered here *) |
|
54 |
| _ -> |
|
55 |
failwith "Internal error: not an arrow type" |
|
58 | 56 |
|
59 | 57 |
(** Returns the type corresponding to a type list. *) |
60 | 58 |
let delay_of_delay_list de = |
61 |
if (List.length de) > 1 then |
|
62 |
new_delay (Dtuple de) |
|
63 |
else |
|
64 |
List.hd de |
|
59 |
if List.length de > 1 then new_delay (Dtuple de) else List.hd de |
|
65 | 60 |
|
66 | 61 |
(** [is_polymorphic de] returns true if [de] is polymorphic. *) |
67 | 62 |
let rec is_polymorphic de = |
68 | 63 |
match de.ddesc with |
69 |
| Dvar -> false |
|
70 |
| Dundef -> false |
|
71 |
| Darrow (de1,de2) -> (is_polymorphic de1) || (is_polymorphic de2) |
|
72 |
| Dtuple dl -> List.exists is_polymorphic dl |
|
73 |
| Dlink d' -> is_polymorphic d' |
|
74 |
| Dunivar -> true |
|
64 |
| Dvar -> |
|
65 |
false |
|
66 |
| Dundef -> |
|
67 |
false |
|
68 |
| Darrow (de1, de2) -> |
|
69 |
is_polymorphic de1 || is_polymorphic de2 |
|
70 |
| Dtuple dl -> |
|
71 |
List.exists is_polymorphic dl |
|
72 |
| Dlink d' -> |
|
73 |
is_polymorphic d' |
|
74 |
| Dunivar -> |
|
75 |
true |
|
75 | 76 |
|
76 | 77 |
(* Pretty-print*) |
77 | 78 |
open Format |
78 |
|
|
79 |
|
|
79 | 80 |
let rec print_delay fmt de = |
80 | 81 |
match de.ddesc with |
81 | 82 |
| Dvar -> |
82 | 83 |
fprintf fmt "'_%s" (name_of_type de.did) |
83 | 84 |
| Dundef -> |
84 | 85 |
fprintf fmt "1" |
85 |
| Darrow (de1,de2) -> |
|
86 |
| Darrow (de1, de2) ->
|
|
86 | 87 |
fprintf fmt "%a->%a" print_delay de1 print_delay de2 |
87 | 88 |
| Dtuple delist -> |
88 |
fprintf fmt "(%a)" |
|
89 |
(Utils.fprintf_list ~sep:"*" print_delay) delist |
|
89 |
fprintf fmt "(%a)" (Utils.fprintf_list ~sep:"*" print_delay) delist |
|
90 | 90 |
| Dlink de -> |
91 |
print_delay fmt de
|
|
91 |
print_delay fmt de |
|
92 | 92 |
| Dunivar -> |
93 | 93 |
fprintf fmt "'%s" (name_of_delay de.did) |
94 | 94 |
|
95 | 95 |
let pp_error fmt = function |
96 |
| Delay_clash (de1,de2) -> |
|
97 |
Utils.reset_names (); |
|
98 |
fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay de2 |
|
96 |
| Delay_clash (de1, de2) -> |
|
97 |
Utils.reset_names (); |
|
98 |
fprintf fmt "Expected delay %a, got delay %a@." print_delay de1 print_delay |
|
99 |
de2 |
Also available in: Unified diff
reformatting