01d0cd02c3
We no longer need to store the bounds as the bounds check expression is generated from MiniLS code where the type is directly available.
260 lines
8.4 KiB
OCaml
260 lines
8.4 KiB
OCaml
(**************************************************************************)
|
|
(* *)
|
|
(* MiniLustre *)
|
|
(* *)
|
|
(* Author : Marc Pouzet *)
|
|
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
|
(* *)
|
|
(**************************************************************************)
|
|
(* clock checking *)
|
|
|
|
open Misc
|
|
open Ident
|
|
open Minils
|
|
open Mls_printer
|
|
open Signature
|
|
open Types
|
|
open Location
|
|
open Printf
|
|
|
|
(** Error Kind *)
|
|
type err_kind = | Etypeclash of ct * ct
|
|
|
|
let err_message exp = function
|
|
| Etypeclash (actual_ct, expected_ct) ->
|
|
Printf.eprintf "%aClock Clash: this expression has clock %a, \n\
|
|
but is expected to have clock %a.\n"
|
|
print_exp exp
|
|
print_clock actual_ct
|
|
print_clock expected_ct;
|
|
raise Error
|
|
|
|
exception Unify
|
|
|
|
|
|
|
|
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) ->
|
|
(try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
|
|
| _ -> 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)
|
|
| Tarray _ | Tid _ -> 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)
|
|
| Ecall(_, e_list, r) ->
|
|
let ck_r = match r with
|
|
| None -> new_var()
|
|
| Some(reset) -> typ_of_name h reset
|
|
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
|
|
| Ecall(_, e_list, Some(reset)) ->
|
|
let ck_r = typ_of_name h reset
|
|
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)
|
|
| 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)
|
|
| 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)
|
|
| Earray e_list ->
|
|
let ck = new_var ()
|
|
in (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
|
|
| Earray_op(op) -> typing_array_op h e op
|
|
in (e.e_ck <- ckofct ct; ct)
|
|
|
|
and typing_array_op h e = function
|
|
| 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) ->
|
|
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 (_, _, _, e_list, r) ->
|
|
let ck_r = match r with
|
|
| None -> new_var()
|
|
| Some(reset) -> typ_of_name h reset
|
|
in (List.iter (expect h (Ck ck_r)) e_list; skeleton ck_r e.e_ty)
|
|
|
|
|
|
and expect h expected_ty e =
|
|
let actual_ty = typing h e
|
|
in
|
|
try unify actual_ty expected_ty
|
|
with | Unify -> err_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 = (*TODO FIXME*)
|
|
let typing_eq { eq_lhs = pat; eq_rhs = e } = match e.e_desc with
|
|
| _ -> let ty_pat = typing_pat h pat in
|
|
(try expect h ty_pat e with
|
|
| Error -> (* DEBUG *)
|
|
Printf.eprintf "Complete expression: %a\nClock pattern: %a\n"
|
|
Mls_printer.print_exp e
|
|
Mls_printer.print_clock ty_pat;
|
|
raise Error) in
|
|
List.iter typing_eq eq_list
|
|
|
|
let build h dec =
|
|
List.fold_left (fun h { v_ident = n } -> Env.add n (new_var ()) h) h dec
|
|
|
|
let sbuild h dec base =
|
|
List.fold_left (fun h { v_ident = 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
|
|
(* assumption *)
|
|
(* property *)
|
|
(typing_eqs h' eq_list;
|
|
expect h' (Ck base) e_a;
|
|
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_ident 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; }
|
|
|