heptagon/compiler/global/clocks.ml

182 lines
6 KiB
OCaml
Raw Normal View History

(***********************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Gwenael Delaval, LIG/INRIA, UJF *)
(* Leonard Gerard, Parkas, ENS *)
(* Adrien Guatto, Parkas, ENS *)
(* Cedric Pasteur, Parkas, ENS *)
2012-06-29 01:43:15 +02:00
(* Marc Pouzet, Parkas, ENS *)
(* *)
(* Copyright 2012 ENS, INRIA, UJF *)
(* *)
(* This file is part of the Heptagon compiler. *)
(* *)
(* Heptagon is free software: you can redistribute it and/or modify it *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* Heptagon is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
2010-07-23 22:06:06 +02:00
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
2011-05-23 09:24:57 +02:00
| Cbase | Con _
| Cvar { contents = Cindex _ } -> ck
2010-07-23 22:06:06 +02:00
| Cvar (({ contents = Clink ck } as link)) ->
2011-05-23 09:24:57 +02:00
let ck = ck_repr ck in
link.contents <- Clink ck;
ck
2010-07-23 22:06:06 +02:00
(** 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
2011-05-23 09:24:57 +02:00
2010-11-23 17:10:11 +01:00
(** unify ck *)
2011-05-23 09:24:57 +02:00
and unify_ck ck1 ck2 =
2010-07-23 22:06:06 +02:00
let ck1 = ck_repr ck1 in
let ck2 = ck_repr ck2 in
2011-05-23 09:24:57 +02:00
if ck1 == ck2 then ()
2010-07-23 22:06:06 +02:00
else
2011-05-23 09:24:57 +02:00
match (ck1, ck2) with
| Cbase, Cbase -> ()
| Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 } when n1 = n2 -> ()
| Con (ck1, c1, n1), Con (ck2, c2, n2) when (c1 = c2) & (n1 = n2) ->
unify_ck ck1 ck2
| Cvar ({ contents = Cindex n } as v), ck
| ck, Cvar ({ contents = Cindex n } as v) ->
occur_check n ck;
v.contents <- Clink ck
| _ -> raise Unify
2010-07-23 22:06:06 +02:00
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 [])
2011-05-23 09:24:57 +02:00
| (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
2011-05-23 09:24:57 +02:00
let rec skeleton ck = function
| Tprod ty_list ->
(match ty_list with
2011-06-09 14:12:32 +02:00
| [_] -> Ck ck
| l -> Cprod (List.map (skeleton ck) l))
| Tarray _ | Tid _ | Tinvalid -> Ck ck
let unprod ct =
let rec f acc ct = match ct with
| Ck ck -> ck::acc
| Cprod ct_l -> List.fold_left f acc ct_l
in
f [] ct
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)
2011-05-12 17:40:23 +02:00
let rec root_ck_of ck = match ck_repr ck with
2011-05-23 09:24:57 +02:00
| Cbase
| Cvar { contents = Cindex _ } -> ck
2011-05-12 17:40:23 +02:00
| Con(ck,_,_) -> root_ck_of ck
2011-05-23 09:24:57 +02:00
| Cvar { contents = Clink _ } -> Misc.internal_error "Clocks, wrong repr"
2011-05-12 17:40:23 +02:00
let rec last_clock ct = match ct with
| Ck ck -> ck
| Cprod l -> last_clock (Misc.last_element l)
(** returns whether [ck1] and [ck2] are leafs of the same clock node :
E.g. .... on C1(x) and .... on C2(x) are. *)
let same_control ck1 ck2 = match ck_repr ck1, ck_repr ck2 with
| Cbase, Cbase -> true
| Con(_,_,x1), Con(_,_,x2) -> x1 = x2
| Cvar {contents = Cindex i1}, Cvar {contents = Cindex i2} -> i1 = i2
| _ -> false
2010-07-23 22:06:06 +02:00
(** returns the first clock of a ct. *)
let rec first_ck ct = match ct with
| Ck ck -> ck
| Cprod [] -> assert false
| Cprod (ct::_) -> first_ck ct
2012-06-20 17:09:17 +02:00
let are_disjoint ck1 ck2 =
let rec list_of_samplers acc ck = match ck with
| Cbase | Cvar _ -> acc
| Con(ck, c, x) -> list_of_samplers ((c, x)::acc) ck
in
let rec disjoint_samplers s_ck1 s_ck2 = match s_ck1, s_ck2 with
| [], _ -> false
| _ , [] -> false
| (c1, x1)::s_ck1, (c2, x2)::s_ck2 ->
if Idents.ident_compare x1 x2 <> 0 then
false
else
c1 <> c2 || disjoint_samplers s_ck1 s_ck2
in
disjoint_samplers (list_of_samplers [] ck1) (list_of_samplers [] ck2)