Revision ca7ff3f7
Added by Lélio Brun 8 months 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