clean signature printing.
This commit is contained in:
Léonard Gérard
parent
74cc367a0e
commit
de49540a76
6 changed files with 45 additions and 351 deletions
|
|
@ -24,6 +24,7 @@ let _print_modul ?(full=false) ff m = match m with
|
|||
| Module m -> fprintf ff "%a" print_name m
|
||||
| QualModule { qual = m; name = n } ->
|
||||
fprintf ff "%a%a" (_aux_print_modul ~full:full) m print_name n
|
||||
|
||||
let print_full_modul ff m = _print_modul ~full:true ff m
|
||||
let print_modul ff m = _print_modul ~full:false ff m
|
||||
|
||||
|
|
@ -32,11 +33,30 @@ let _print_qualname ?(full=false) ff { qual = q; name = n} = match q with
|
|||
| LocalModule -> print_name ff n
|
||||
| _ when q = g_env.current_mod && not full -> print_name ff n
|
||||
| _ -> fprintf ff "%a%a" (_aux_print_modul ~full:full) q print_name n
|
||||
|
||||
|
||||
let print_qualname ff qn = _print_qualname ~full:false ff qn
|
||||
let print_full_qualname ff qn = _print_qualname ~full:true ff qn
|
||||
|
||||
let print_shortname ff {name = n} = print_name ff n
|
||||
|
||||
let print_ident ff id = Format.fprintf ff "%s" (name id)
|
||||
|
||||
let rec print_ck ff = function
|
||||
| Cbase -> fprintf ff "."
|
||||
| Con (ck, c, n) -> fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
|
||||
| Cvar { contents = Cindex i } -> fprintf ff "'a%i" i
|
||||
| Cvar { contents = Clink ck } -> print_ck ff ck
|
||||
|
||||
let rec print_ct ff = function
|
||||
| Ck ck -> print_ck ff ck
|
||||
| Cprod ct_list ->
|
||||
fprintf ff "@[<2>(%a)@]" (print_list_r print_ct """ *""") ct_list
|
||||
|
||||
let rec print_sck ff = function
|
||||
| Signature.Cbase -> fprintf ff "."
|
||||
| Signature.Con (ck, c, n) -> fprintf ff "%a on %a(%a)" print_sck ck print_qualname c print_name n
|
||||
|
||||
|
||||
let rec print_static_exp_desc ff sed = match sed with
|
||||
| Sint i -> fprintf ff "%d" i
|
||||
|
|
@ -115,9 +135,14 @@ let print_interface_const ff name c =
|
|||
|
||||
let print_interface_value ff name node =
|
||||
let print_arg ff arg = match arg.a_name with
|
||||
| None -> print_type ff arg.a_type
|
||||
| None ->
|
||||
fprintf ff "@[%a :: %a@]" print_type arg.a_type print_sck arg.a_clock
|
||||
| Some(name) ->
|
||||
fprintf ff "@[%a : %a@]" print_name name print_type arg.a_type in
|
||||
fprintf ff "@[%a : %a :: %a@]"
|
||||
print_name name
|
||||
print_type arg.a_type
|
||||
print_sck arg.a_clock
|
||||
in
|
||||
let print_node_params ff p_list =
|
||||
print_list_r (fun ff p -> print_name ff p.p_name) "<<" "," ">>" ff p_list
|
||||
in
|
||||
|
|
@ -140,17 +165,4 @@ let print_interface ff =
|
|||
(fun key sigtype -> print_interface_value ff key sigtype) m.m_values;
|
||||
Format.fprintf ff "@."
|
||||
|
||||
let print_ident ff id = Format.fprintf ff "%s" (name id)
|
||||
|
||||
let rec print_ck ff = function
|
||||
| Cbase -> fprintf ff "base"
|
||||
| Con (ck, c, n) ->
|
||||
fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
|
||||
| Cvar { contents = Cindex i } -> fprintf ff "'a%i" i
|
||||
| Cvar { contents = Clink ck } -> print_ck ff ck
|
||||
|
||||
let rec print_ct ff = function
|
||||
| Ck ck -> print_ck ff ck
|
||||
| Cprod ct_list ->
|
||||
fprintf ff "@[<2>(%a)@]" (print_list_r print_ct """ *""") ct_list
|
||||
|
||||
|
|
|
|||
|
|
@ -67,17 +67,15 @@ exception SignatureError of error
|
|||
|
||||
let message loc e = begin match e with
|
||||
| Eckvar_unbound_input(var_name,ck_name) ->
|
||||
let a,name = match var_name with None -> "a","" | Some n -> "the"," "^n in
|
||||
Format.eprintf "%aThe variable %s is unbound.@\n
|
||||
Note that %s sampled input%s should come together with its clock.@."
|
||||
let a,name = match var_name with None -> "A","" | Some n -> "The"," "^n in
|
||||
Format.eprintf "%a%s sampled input%s should come together with its sampling variable %s.@."
|
||||
print_location loc
|
||||
ck_name a name
|
||||
a name ck_name
|
||||
| Eckvar_unbound_ouput (var_name,ck_name) ->
|
||||
let a,name = match var_name with None -> "a","" | Some n -> "the"," "^n in
|
||||
Format.eprintf "%aThe variable %s is unbound.@\n
|
||||
Note that %s sampled ouput%s should be returned with its clock.@."
|
||||
let a,name = match var_name with None -> "A","" | Some n -> "The"," "^n in
|
||||
Format.eprintf "%a%s sampled ouput%s should be returned with its sampling value %s.@."
|
||||
print_location loc
|
||||
ck_name a name
|
||||
a name ck_name
|
||||
| Eckvar_unbound(var_name,ck_name) ->
|
||||
Format.eprintf "%aThe variable %s is unbound.@." print_location loc ck_name
|
||||
end;
|
||||
|
|
|
|||
|
|
@ -19,8 +19,6 @@ let compile_program p =
|
|||
let p = silent_pass "Statefulness check" true Stateful.program p in
|
||||
let p = pass "Typing" true Typing.program p pp in
|
||||
|
||||
if !print_types then print_interface Format.std_formatter;
|
||||
|
||||
(* Causality check *)
|
||||
let p = silent_pass "Causality check" !causality Causality.program p in
|
||||
|
||||
|
|
|
|||
|
|
@ -56,7 +56,7 @@ let ck_of_name h x = Env.find x h
|
|||
|
||||
let rec typing_extvalue h w =
|
||||
let ck = match w.w_desc with
|
||||
| Wconst se -> fresh_clock()
|
||||
| Wconst _ -> fresh_clock()
|
||||
| Wvar x -> ck_of_name h x
|
||||
| Wwhen (w1, c, n) ->
|
||||
let ck_n = ck_of_name h n in
|
||||
|
|
@ -196,7 +196,7 @@ let typing_node node =
|
|||
let h = append_env h node.n_local in
|
||||
typing_eqs h node.n_equs;
|
||||
(* synchronize input and output on base : find the free vars and set them to base *)
|
||||
Env.iter (fun id ck -> unify_ck (root_ck_of ck) Cbase) h0;
|
||||
Env.iter (fun _ ck -> unify_ck (root_ck_of ck) Cbase) h0;
|
||||
(*update clock info in variables descriptions *)
|
||||
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
|
||||
let node = { node with n_input = List.map set_clock node.n_input;
|
||||
|
|
|
|||
|
|
@ -1,320 +0,0 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Heptagon *)
|
||||
(* *)
|
||||
(* Author : Marc Pouzet *)
|
||||
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* simple initialization analysis. This is almost trivial since *)
|
||||
(* input/outputs of a node are forced to be initialized *)
|
||||
(* add a special treatment of clock state variables whose initial *)
|
||||
(* values are known. This allows to accept code generated *)
|
||||
(* for automata *)
|
||||
(* if [clock c = C fby ec] then [merge c (C -> e) ...] is initialized *)
|
||||
(* if [e] is initialized only *)
|
||||
|
||||
open Misc
|
||||
open Names
|
||||
open Idents
|
||||
open Minils
|
||||
open Location
|
||||
open Format
|
||||
open Types
|
||||
|
||||
type typ = | Iproduct of typ list | Ileaf of init
|
||||
|
||||
and init = { mutable i_desc : init_desc; mutable i_index : int}
|
||||
|
||||
and init_desc = | Izero | Ione | Ivar | Imax of init * init | Ilink of init
|
||||
|
||||
type typ_env =
|
||||
{ t_init : init; (* its initialisation type *) t_value : longname option }
|
||||
|
||||
(* its initial value *)
|
||||
(* typing errors *)
|
||||
exception Unify
|
||||
|
||||
let index = ref 0
|
||||
|
||||
let gen_index () = (incr index; !index)
|
||||
|
||||
let new_var () = { i_desc = Ivar; i_index = gen_index (); }
|
||||
|
||||
let izero = { i_desc = Izero; i_index = gen_index (); }
|
||||
|
||||
let ione = { i_desc = Ione; i_index = gen_index (); }
|
||||
|
||||
let imax i1 i2 = { i_desc = Imax (i1, i2); i_index = gen_index (); }
|
||||
|
||||
let product l = Iproduct l
|
||||
|
||||
let leaf i = Ileaf i
|
||||
|
||||
(* basic operation on initialization values *)
|
||||
let rec irepr i =
|
||||
match i.i_desc with
|
||||
| Ilink i_son ->
|
||||
let i_son = irepr i_son in (i.i_desc <- Ilink i_son; i_son)
|
||||
| _ -> i
|
||||
|
||||
(** Simplification rules for max. Nothing fancy here *)
|
||||
let max i1 i2 =
|
||||
let i1 = irepr i1 in
|
||||
let i2 = irepr i2
|
||||
in
|
||||
match ((i1.i_desc), (i2.i_desc)) with
|
||||
| (Izero, Izero) -> izero
|
||||
| (Izero, _) -> i2
|
||||
| (_, Izero) -> i1
|
||||
| (_, Ione) | (Ione, _) -> ione
|
||||
| _ -> imax i1 i2
|
||||
|
||||
let rec itype =
|
||||
function | Iproduct ty_list -> itype_list ty_list | Ileaf i -> i
|
||||
|
||||
and itype_list ty_list =
|
||||
List.fold_left (fun acc ty -> max acc (itype ty)) izero ty_list
|
||||
|
||||
(* saturate an initialization type. Every element must be initialized *)
|
||||
let rec initialized i =
|
||||
let i = irepr i
|
||||
in
|
||||
match i.i_desc with
|
||||
| Izero -> ()
|
||||
| Ivar -> i.i_desc <- Ilink izero
|
||||
| Imax (i1, i2) -> (initialized i1; initialized i2)
|
||||
| Ilink i -> initialized i
|
||||
| Ione -> raise Unify
|
||||
|
||||
(* build an initialization type from a type *)
|
||||
let rec skeleton i =
|
||||
function
|
||||
| Tprod ty_list -> product (List.map (skeleton i) ty_list)
|
||||
| Tarray _ | Tid _ -> leaf i
|
||||
|
||||
(* sub-typing *)
|
||||
let rec less left_ty right_ty =
|
||||
if left_ty == right_ty
|
||||
then ()
|
||||
else
|
||||
(match (left_ty, right_ty) with
|
||||
| (Iproduct l1, Iproduct l2) -> List.iter2 less l1 l2
|
||||
| (Ileaf i1, Ileaf i2) -> iless i1 i2
|
||||
| _ -> raise Unify)
|
||||
|
||||
and iless left_i right_i =
|
||||
if left_i == right_i
|
||||
then ()
|
||||
else
|
||||
(let left_i = irepr left_i in
|
||||
let right_i = irepr right_i
|
||||
in
|
||||
if left_i == right_i
|
||||
then ()
|
||||
else
|
||||
(match ((left_i.i_desc), (right_i.i_desc)) with
|
||||
| (Izero, _) | (_, Ione) -> ()
|
||||
| (_, Izero) -> initialized left_i
|
||||
| (Imax (i1, i2), _) -> (iless i1 right_i; iless i2 right_i)
|
||||
| (_, Ivar) ->
|
||||
let left_i = occur_check right_i.i_index left_i
|
||||
in right_i.i_desc <- Ilink left_i
|
||||
| (_, Imax (i1, i2)) ->
|
||||
let i1 = occur_check left_i.i_index i1 in
|
||||
let i2 = occur_check left_i.i_index i2
|
||||
in right_i.i_desc <- Ilink (imax left_i (imax i1 i2))
|
||||
| _ -> raise Unify))
|
||||
|
||||
and (* an inequation [a < t[a]] becomes [a = t[0]] *) occur_check index i =
|
||||
match i.i_desc with
|
||||
| Izero | Ione -> i
|
||||
| Ivar -> if i.i_index = index then izero else i
|
||||
| Imax (i1, i2) -> max (occur_check index i1) (occur_check index i2)
|
||||
| Ilink i -> occur_check index i
|
||||
|
||||
(* computes the initialization type of a merge *)
|
||||
let merge opt_c c_i_list =
|
||||
let rec search c c_i_list =
|
||||
match c_i_list with
|
||||
| [] -> izero
|
||||
| (c0, i) :: c_i_list -> if c = c0 then i else search c c_i_list
|
||||
in
|
||||
match opt_c with
|
||||
| None -> List.fold_left (fun acc (_, i) -> max acc i) izero c_i_list
|
||||
| Some c -> search c c_i_list
|
||||
|
||||
module Printer =
|
||||
struct
|
||||
open Format
|
||||
|
||||
let rec print_list_r print po sep pf ff =
|
||||
function
|
||||
| [] -> ()
|
||||
| x :: l ->
|
||||
(fprintf ff "@[%s%a" po print x;
|
||||
List.iter (fprintf ff "%s@]@ @[%a" sep print) l;
|
||||
fprintf ff "%s@]" pf)
|
||||
|
||||
let rec print_init ff i =
|
||||
match i.i_desc with
|
||||
| Izero -> fprintf ff "0"
|
||||
| Ione -> fprintf ff "1"
|
||||
| Ivar -> fprintf ff "0"
|
||||
| Imax (i1, i2) ->
|
||||
fprintf ff "@[%a\\/%a@]" print_init i1 print_init i2
|
||||
| Ilink i -> print_init ff i
|
||||
|
||||
let rec print_type ff =
|
||||
function
|
||||
| Ileaf i -> print_init ff i
|
||||
| Iproduct ty_list ->
|
||||
fprintf ff "@[%a@]" (print_list_r fprint_type "(" " *" ")") ty_list
|
||||
|
||||
end
|
||||
|
||||
module Error =
|
||||
struct
|
||||
open Location
|
||||
|
||||
type error = | Eclash of typ * typ
|
||||
|
||||
exception Error of location * error
|
||||
|
||||
let error loc kind = raise (Error (loc, kind))
|
||||
|
||||
let message loc kind =
|
||||
((match kind with
|
||||
| Eclash (left_ty, right_ty) ->
|
||||
Format.eprintf
|
||||
"%aInitialization error: this expression has type \
|
||||
%a,@\n\
|
||||
but is expected to have type %a@."
|
||||
print_location loc Printer.output_typ left_ty Printer.
|
||||
output_typ right_ty);
|
||||
raise Errors.Error)
|
||||
|
||||
end
|
||||
|
||||
let less_exp e actual_ty expected_ty =
|
||||
try less actual_ty expected_ty
|
||||
with
|
||||
| Unify -> Error.message e.e_loc (Error.Eclash (actual_ty, expected_ty))
|
||||
|
||||
let rec typing h e =
|
||||
match e.e_desc with
|
||||
| Econst c -> leaf izero
|
||||
| Evar x -> let { t_init = i } = Env.find x h in leaf i
|
||||
| Efby (None, e) -> (expect h e (skeleton izero e.e_ty); leaf ione)
|
||||
| Efby ((Some _), e) -> (expect h e (skeleton izero e.e_ty); leaf izero)
|
||||
| Etuple e_list -> product (List.map (typing h) e_list)
|
||||
|
||||
(*TODO traitement singulier et empêche reset d'un 'op'*)
|
||||
| Ecall (op, e_list, None) when op.op_kind = Efun ->
|
||||
let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list
|
||||
in skeleton i e.e_ty
|
||||
| Ecall (op, e_list, reset) when op.op_kind = Enode ->
|
||||
List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list;
|
||||
let i = match reset with
|
||||
| None -> izero
|
||||
| Some(n) -> let { t_init = i } = Env.find n h in i
|
||||
in skeleton i e.e_ty
|
||||
| Ewhen (e, c, n) ->
|
||||
let { t_init = i1 } = Env.find n h in
|
||||
let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
|
||||
(* result of the encoding of e1 -> e2 ==
|
||||
if true fby false then e1 else e2 *)
|
||||
| Eifthenelse(
|
||||
{ e_desc = Efby(Some (Cconstr tn), { e_desc = Econst (Cconstr fn) }) },
|
||||
e2, e3) when tn = Initial.ptrue & fn = Initial.pfalse ->
|
||||
expect h e3 (skeleton ione e3.e_ty);
|
||||
let i = itype (typing h e2) in skeleton i e.e_ty
|
||||
| Eifthenelse (e1, e2, e3) ->
|
||||
let i1 = itype (typing h e1) in
|
||||
let i2 = itype (typing h e2) in
|
||||
let i3 = itype (typing h e3) in
|
||||
let i = max i1 (max i2 i3) in skeleton i e.e_ty
|
||||
| Emerge (n, c_e_list) ->
|
||||
let { t_init = i; t_value = opt_c } = Env.find n h in
|
||||
let i =
|
||||
merge opt_c
|
||||
(List.map (fun (c, e) -> (c, (itype (typing h e)))) c_e_list)
|
||||
in skeleton i e.e_ty
|
||||
| Efield (e1, n) -> let i = itype (typing h e1) in skeleton i e.e_ty
|
||||
| Estruct l ->
|
||||
let i =
|
||||
List.fold_left (fun acc (_, e) -> max acc (itype (typing h e))) izero
|
||||
l
|
||||
in skeleton i e.e_ty
|
||||
| Efield_update _ | Econstvar _ | Earray _ | Earray_op _ ->
|
||||
leaf izero (* TODO FIXME array_op dans init *)
|
||||
|
||||
and expect h e expected_ty =
|
||||
let actual_ty = typing h e in less_exp e actual_ty expected_ty
|
||||
|
||||
let rec typing_pat h =
|
||||
function
|
||||
| Evarpat x -> let { t_init = i } = Env.find x h in leaf i
|
||||
| Etuplepat pat_list -> product (List.map (typing_pat h) pat_list)
|
||||
|
||||
let typing_eqs h eq_list =
|
||||
List.iter
|
||||
(fun { eq_lhs = pat; eq_rhs = e } ->
|
||||
let ty_pat = typing_pat h pat in expect h e ty_pat)
|
||||
eq_list
|
||||
|
||||
let build h eq_list =
|
||||
let rec build_pat h =
|
||||
function
|
||||
| Evarpat x -> Env.add x { t_init = new_var (); t_value = None; } h
|
||||
| Etuplepat pat_list -> List.fold_left build_pat h pat_list in
|
||||
let build_equation h { eq_lhs = pat; eq_rhs = e } =
|
||||
match (pat, (e.e_desc)) with
|
||||
| (Evarpat x, Efby ((Some (Cconstr c)), _)) ->
|
||||
(* we keep the initial value of state variables *)
|
||||
Env.add x { t_init = new_var (); t_value = Some c; } h
|
||||
| _ -> build_pat h pat
|
||||
in List.fold_left build_equation h eq_list
|
||||
|
||||
let sbuild h dec =
|
||||
List.fold_left
|
||||
(fun h { v_ident = n } -> Env.add n { t_init = izero; t_value = None; } h)
|
||||
h dec
|
||||
|
||||
let typing_contract h contract =
|
||||
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 in
|
||||
let h' = build h eq_list
|
||||
in
|
||||
(* assumption *)
|
||||
(* property *)
|
||||
(typing_eqs h' eq_list;
|
||||
expect h' e_a (skeleton izero e_a.e_ty);
|
||||
expect h' e_g (skeleton izero e_g.e_ty);
|
||||
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
|
||||
} =
|
||||
let h = sbuild Env.empty i_list in
|
||||
let h = sbuild h o_list in
|
||||
let h = typing_contract h contract in
|
||||
let h = build h eq_list in typing_eqs h eq_list
|
||||
|
||||
let program (({ p_nodes = p_node_list } as p)) =
|
||||
(List.iter typing_node p_node_list; p)
|
||||
|
||||
|
|
@ -15,14 +15,20 @@ let pp p = if !verbose then Mls_printer.print stdout p
|
|||
|
||||
let compile_program p =
|
||||
(* Clocking *)
|
||||
let p = pass "Clocking" true Clocking.program p pp in
|
||||
let p =
|
||||
try pass "Clocking" true Clocking.program p pp
|
||||
with Errors.Error ->
|
||||
pp p;
|
||||
comment ~sep:"*** " ("Clocking failed.");
|
||||
if !print_types then Global_printer.print_interface Format.std_formatter;
|
||||
raise Errors.Error
|
||||
in
|
||||
|
||||
if !print_types then Global_printer.print_interface Format.std_formatter;
|
||||
|
||||
(* Level clocks *)
|
||||
let p = pass "Level clock" true Level_clock.program p pp in
|
||||
|
||||
(* Check that the dataflow code is well initialized *)
|
||||
(*let p = silent_pass "Initialization check" !init Init.program p in *)
|
||||
|
||||
(* Automata minimization *)
|
||||
(*
|
||||
let p =
|
||||
|
|
|
|||
Loading…
Reference in a new issue