heptagon/minils/analysis/clocking.ml

298 lines
7.9 KiB
OCaml
Raw Normal View History

2010-06-15 10:49:03 +02:00
(**************************************************************************)
(* *)
(* MiniLustre *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* clock checking *)
(* $Id$ *)
open Misc
open Ident
open Minils
open Signature
2010-06-15 10:49:03 +02:00
open Location
type error = | Etypeclash of ct * ct
exception TypingError of error
exception Unify
let error kind = raise (TypingError(kind))
let message e kind =
begin match kind with
Etypeclash(actual_ct, expected_ct) -> ()
(*TODO remettre en route quand Printer fonctionne
Printf.eprintf "%aClock Clash: this expression has clock %a, \n\
but is expected to have clock %a.\n"
Printer.print_exp e
Printer.print_clock actual_ct
Printer.print_clock expected_ct*)
2010-06-15 10:49:03 +02:00
end;
raise Error
let index = ref 0
let gen_index () = incr index; !index
let new_var () = Cvar { contents = Cindex (gen_index ()) }
let rec repr ck =
match ck with
Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar ({ contents = Clink(ck) } as link) ->
let ck = repr ck in
link.contents <- Clink(ck);
ck
let rec occur_check index ck =
let ck = repr ck in
match ck with
Cbase -> ()
| Cvar { contents = Cindex n } when index <> n -> ()
| Con(ck, _, _) -> occur_check index ck
| _ -> raise Unify
let rec ck_value ck =
match ck with
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cvar { contents = Clink(ck) } ->
ck_value ck
let rec unify t1 t2 =
if t1 == t2 then ()
else match t1, t2 with
Ck(ck1), Ck(ck2) -> unify_ck ck1 ck2
| Cprod(ct_list1), Cprod(ct_list2) ->
begin try
List.iter2 unify ct_list1 ct_list2
with
_ -> raise Unify
end
| _ -> raise Unify
and unify_ck ck1 ck2 =
let ck1 = repr ck1 in
let ck2 = 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
let rec eq ck1 ck2 =
match repr ck1, repr ck2 with
| Cbase, Cbase -> true
| Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 } -> true
| Con(ck1, _, n1), Con(ck2, _, n2) when (n1 = n2) -> eq ck1 ck2
| _ -> false
let rec unify t1 t2 =
match t1, t2 with
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 =
try
List.iter2 unify t1_list t2_list
with
_ -> raise Unify
let rec skeleton ck = function
| Tprod(ty_list) -> Cprod(List.map (skeleton ck) ty_list)
| Tbase _ -> Ck(ck)
let ckofct = function
| Ck(ck) -> repr ck
| Cprod(ct_list) -> Cbase
let prod = function
| [] -> assert false
| [ty] -> ty
| ty_list -> Tprod(ty_list)
let typ_of_name h x = Env.find x h
let rec typing h e =
let ct = match e.e_desc with
| Econst _ | Econstvar _ -> Ck(new_var ())
| Evar(x) -> Ck(typ_of_name h x)
| Efby(c, e) -> typing h e
| Etuple(e_list) ->
Cprod(List.map (typing h) e_list)
| Eop(_,_, e_list) ->
let ck = new_var () in
List.iter (expect h (Ck(ck))) e_list;
skeleton ck e.e_ty
| Eapp(_,_, e_list) ->
let ck_r = new_var () in
List.iter (expect h (Ck(ck_r))) e_list;
skeleton ck_r e.e_ty
| Eevery(_,_, e_list, n) ->
let ck_r = typ_of_name h n in
List.iter (expect h (Ck(ck_r))) e_list;
skeleton ck_r e.e_ty
| Ewhen(e, c, n) ->
let ck_n = typ_of_name h n in
expect h (skeleton ck_n e.e_ty) e;
skeleton (Con(ck_n, c, n)) e.e_ty
| Eifthenelse(e1, e2, e3) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty in
expect h (Ck(ck)) e1;
expect h ct e2;
expect h ct e3; ct
| Emerge(n, c_e_list) ->
let ck_c = typ_of_name h n in
typing_c_e_list h ck_c n c_e_list;
skeleton ck_c e.e_ty
| Efield(e1,n) ->
let ck = new_var () in
let ct = skeleton ck e1.e_ty in
expect h (Ck(ck)) e1;
ct
| Estruct(l) ->
let ck = new_var () in
List.iter
(fun (n,e) ->
let ct = skeleton ck e.e_ty in
expect h ct e)
l;
Ck(ck)
(*Array operators*)
| Earray e_list ->
let ck = new_var () in
List.iter (expect h (Ck(ck))) e_list;
skeleton ck e.e_ty
| Erepeat (_,e) ->
typing h e
| Eselect (_,e) ->
typing h e
| Eselect_dyn (e_list, _, e, defe) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty in
expect h ct e;
List.iter (expect h ct) e_list;
ct
| Eupdate (_, e1, e2) | Efield_update (_, e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty in
expect h (Ck(ck)) e1;
expect h ct e2;
ct
| Eselect_slice (_ , _, e) ->
typing h e
| Econcat (e1, e2) ->
let ck = new_var () in
let ct = skeleton ck e.e_ty in
expect h (Ck(ck)) e1;
expect h ct e2;
ct
| Eiterator (_, f, _, _, e_list, _) ->
let ck_r = new_var () in
List.iter (expect h (Ck(ck_r))) e_list;
skeleton ck_r e.e_ty
| Ereset_mem (_, _, x) -> assert false
in
e.e_ck <- ckofct ct;
ct
and expect h expected_ty e =
let actual_ty = typing h e in
try unify actual_ty expected_ty
with Unify -> message e (Etypeclash(actual_ty, expected_ty))
and typing_c_e_list h ck_c n c_e_list =
let rec typrec = function
| [] -> ()
| (c, e) :: c_e_list ->
expect h (skeleton (Con(ck_c, c, n)) e.e_ty) e;
typrec c_e_list in
typrec c_e_list
let rec typing_pat h = function
| Evarpat(x) -> Ck(typ_of_name h x)
| Etuplepat(pat_list) -> Cprod(List.map (typing_pat h) pat_list)
let typing_eqs h eq_list =
List.iter
2010-06-15 15:08:14 +02:00
(fun { eq_lhs = pat; eq_rhs = e } ->
2010-06-15 10:49:03 +02:00
(match e.e_desc with
| Ereset_mem (_, _, x) ->
let ck = typ_of_name h x in
e.e_ck <- ck;
| _ ->
let ty_pat = typing_pat h pat in
try
expect h ty_pat e
with Error ->
(* TODO remettre en route quand Printer fonctionne
(* DEBUG *)
2010-06-15 10:49:03 +02:00
Printf.eprintf "Complete expression: %a\n"
Printer.print_exp e;
Printf.eprintf "Clock pattern: %a\n"
Printer.print_clock ty_pat; *)
2010-06-15 10:49:03 +02:00
raise Error
)
) eq_list
let build h dec =
List.fold_left (fun h { v_name = n } -> Env.add n (new_var ()) h) h dec
let sbuild h dec base =
List.fold_left (fun h { v_name = n } -> Env.add n base h) h dec
let typing_contract h contract base =
match contract with
| None -> h
| Some { c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list } ->
let h = sbuild h c_list base in
let h' = build h l_list in
typing_eqs h' eq_list;
(* assumption *)
expect h' (Ck base) e_a;
(* property *)
expect h' (Ck base) e_g;
h
let typing_node ({ n_name = f; n_input = i_list; n_output = o_list;
n_contract = contract;
n_local = l_list; n_equs = eq_list } as node) =
let base = Cbase in
let h = sbuild Env.empty i_list base in
let h = sbuild h o_list base in
let h = typing_contract h contract base in
let h = build h l_list in
typing_eqs h eq_list;
(*update clock info in variables descriptions *)
let set_clock vd =
{ vd with v_clock = ck_value (Env.find vd.v_name h) } in
{ node with n_input = List.map set_clock i_list;
n_output = List.map set_clock o_list;
n_local = List.map set_clock l_list; }
let program ({ p_nodes = p_node_list } as p) =
{ p with p_nodes = List.map typing_node p_node_list }