heptagon/compiler/global/clocks.ml

126 lines
3.4 KiB
OCaml
Raw Normal View History

2010-07-23 22:06:06 +02:00
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Names
open Idents
open Types
2010-11-04 18:07:17 +01:00
2010-07-23 22:06:06 +02:00
type ct =
| Ck of ck
| Cprod of ct list
and ck =
| Cbase
| Cvar of link ref
| Con of ck * constructor_name * var_ident
and link =
| Cindex of int
| Clink of ck
exception Unify
2010-11-23 17:10:11 +01:00
let invalid_clock = Cprod []
2010-07-23 22:06:06 +02:00
let index = ref 0
let gen_index () = (incr index; !index)
(** returns a new clock variable *)
let fresh_clock () = Cvar { contents = Cindex (gen_index ()); }
2010-07-23 22:06:06 +02:00
2011-05-09 19:32:12 +02:00
(** returns a new clock type corresponding to the data type [ty] *)
let rec fresh_ct ty = match ty with
| Tprod ty_list ->
(match ty_list with
| [] -> Ck (fresh_clock())
| _ -> Cprod (List.map fresh_ct ty_list))
| Tarray (t, _) -> fresh_ct t
| Tid _ | Tinvalid -> Ck (fresh_clock())
2010-07-23 22:06:06 +02:00
(** returns the canonic (short) representant of a [ck]
and update it to this value. *)
let rec ck_repr ck = match ck with
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar (({ contents = Clink ck } as link)) ->
let ck = ck_repr ck in (link.contents <- Clink ck; ck)
(** verifies that index is fresh in ck. *)
let rec occur_check index ck =
let ck = ck_repr ck in
match ck with
| Cbase -> ()
| Cvar { contents = Cindex n } when index <> n -> ()
| Con (ck, _, _) -> occur_check index ck
| _ -> raise Unify
2010-11-23 17:10:11 +01:00
(** unify ck *)
let rec unify_ck ck1 ck2 =
2010-07-23 22:06:06 +02:00
let ck1 = ck_repr ck1 in
let ck2 = ck_repr ck2 in
if ck1 == ck2
then ()
else
(match (ck1, ck2) with
| (Cbase, Cbase) -> ()
| (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when
n1 = n2 -> ()
| (Cvar (({ contents = Cindex n1 } as v)), _) ->
(occur_check n1 ck2; v.contents <- Clink ck2)
| (_, Cvar (({ contents = Cindex n2 } as v))) ->
(occur_check n2 ck1; v.contents <- Clink ck1)
| (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) ->
unify_ck ck1 ck2
| _ -> raise Unify)
2010-11-23 17:10:11 +01:00
(** unify ct *)
2010-07-23 22:06:06 +02:00
let rec unify t1 t2 =
2010-11-23 17:10:11 +01:00
if t1 == t2 then () else
2010-07-23 22:06:06 +02:00
match (t1, t2) with
| (Ck (Cbase | Cvar { contents = Cindex _; }), Cprod [])
| (Cprod [], Ck (Cbase | Cvar { contents = Cindex _; })) ->
()
2010-07-23 22:06:06 +02:00
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
| _ -> raise Unify
and unify_list t1_list t2_list =
2010-11-23 17:10:11 +01:00
try List.iter2 unify t1_list t2_list
with _ -> raise Unify
2010-07-23 22:06:06 +02:00
2011-05-09 19:32:12 +02:00
let prod ck_l = match ck_l with
| [ck] -> Ck ck
| _ -> Cprod (List.map (fun ck -> Ck ck) ck_l)
(*
let rec tuple ck = function
| Tprod ty_list ->
(match ty_list with
2011-04-14 18:06:54 +02:00
| [] -> Ck ck
2011-05-09 19:32:12 +02:00
| _ -> Cprod (List.map (tuple ck) ty_list))
| Tarray (t, _) -> tuple ck t
2011-04-14 18:06:54 +02:00
| Tid _ | Tinvalid -> Ck ck
2011-05-09 19:32:12 +02:00
*)
(*
let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with
2011-05-12 00:54:02 +02:00
|
2011-05-09 19:32:12 +02:00
let rec optim_base_ck base_ck ct = match ct with
2011-05-12 00:54:02 +02:00
| Ck ck ->
| Cprod c_l ->
2011-05-09 19:32:12 +02:00
*)
2010-07-23 22:06:06 +02:00