lustrec / src / delay.ml @ b38ffff3
History | View | Annotate | Download (2.97 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
(** Types definitions and a few utility functions on delay types. *) |
13 |
(** Delay analysis by type polymorphism instead of constraints *) |
14 |
open Utils |
15 |
|
16 |
type delay_expr = |
17 |
{mutable ddesc: delay_desc; |
18 |
did: int} |
19 |
|
20 |
and delay_desc = |
21 |
| Dvar (* Monomorphic type variable *) |
22 |
| Dundef |
23 |
| Darrow of delay_expr * delay_expr |
24 |
| 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 |
29 |
|
30 |
exception Unify of delay_expr * delay_expr |
31 |
exception Error of Location.t * error |
32 |
|
33 |
let new_id = ref (-1) |
34 |
|
35 |
let new_delay desc = |
36 |
incr new_id; {ddesc = desc; did = !new_id } |
37 |
|
38 |
let new_var () = |
39 |
new_delay Dvar |
40 |
|
41 |
let new_univar () = |
42 |
new_delay Dunivar |
43 |
|
44 |
let rec repr = |
45 |
function |
46 |
{ddesc = Dlink i'} -> |
47 |
repr i' |
48 |
| i -> i |
49 |
|
50 |
(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type |
51 |
(ensured by language syntax) *) |
52 |
let split_arrow de = |
53 |
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" |
58 |
|
59 |
(** Returns the type corresponding to a type list. *) |
60 |
let delay_of_delay_list de = |
61 |
if (List.length de) > 1 then |
62 |
new_delay (Dtuple de) |
63 |
else |
64 |
List.hd de |
65 |
|
66 |
(** [is_polymorphic de] returns true if [de] is polymorphic. *) |
67 |
let rec is_polymorphic de = |
68 |
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 |
75 |
|
76 |
(* Pretty-print*) |
77 |
open Format |
78 |
|
79 |
let rec print_delay fmt de = |
80 |
match de.ddesc with |
81 |
| Dvar -> |
82 |
fprintf fmt "'_%s" (name_of_type de.did) |
83 |
| Dundef -> |
84 |
fprintf fmt "1" |
85 |
| Darrow (de1,de2) -> |
86 |
fprintf fmt "%a->%a" print_delay de1 print_delay de2 |
87 |
| Dtuple delist -> |
88 |
fprintf fmt "(%a)" |
89 |
(Utils.fprintf_list ~sep:"*" print_delay) delist |
90 |
| Dlink de -> |
91 |
print_delay fmt de |
92 |
| Dunivar -> |
93 |
fprintf fmt "'%s" (name_of_delay de.did) |
94 |
|
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 |