Printer_stuff to be continued mainly on minils and factorisation of mutual printing functions to ident names static and types.
This commit is contained in:
Léonard Gérard
parent
e400ffd9a5
commit
3c22a1a34a
8 changed files with 444 additions and 421 deletions
|
|
@ -79,3 +79,5 @@ module IdentSet = struct
|
|||
Format.fprintf ff "}@]";
|
||||
end
|
||||
|
||||
|
||||
let print_ident ff id = fprintf ff "%s" (name id)
|
||||
|
|
|
|||
|
|
@ -37,3 +37,6 @@ sig
|
|||
include (Set.S with type elt = ident)
|
||||
val fprint_t : Format.formatter -> t -> unit
|
||||
end
|
||||
|
||||
|
||||
val print_ident : Format.formatter -> ident -> unit
|
||||
|
|
|
|||
|
|
@ -41,4 +41,30 @@ let mk_longname s =
|
|||
Modname { qual = String.sub s 0 ind; id = id; }
|
||||
with Not_found -> Name s
|
||||
|
||||
let print_longname ff id = Format.fprintf ff "%s" (fullname id)
|
||||
(** Are infix
|
||||
[or], [quo], [mod], [land], [lor], [lxor], [lsl], [lsr], [asr]
|
||||
and every names not beginning with 'a' .. 'z' | 'A' .. 'Z' | '_' | '`'*)
|
||||
let is_infix s =
|
||||
let module StrSet = Set.Make(String) in
|
||||
let infix_set =
|
||||
List.fold_right StrSet.add
|
||||
["or"; "quo"; "mod"; "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr"]
|
||||
StrSet.empty in
|
||||
if StrSet.mem s infix_set then true
|
||||
else (match String.get s 0 with
|
||||
| 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
|
||||
| _ -> true)
|
||||
|
||||
let print_name ff n =
|
||||
let n = if is_infix n
|
||||
then "( " ^ (n ^ " )") (* do not remove the space around n, since for example "(*" would create bugs *)
|
||||
else n
|
||||
in Format.fprintf ff "%s" n
|
||||
|
||||
let print_longname ff n =
|
||||
match n with
|
||||
| Name m -> print_name ff m
|
||||
| Modname { qual = "Pervasives"; id = m } -> print_name ff m
|
||||
| Modname { qual = m1; id = m2 } -> (Format.fprintf ff "%s." m1; print_name ff m2)
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -130,32 +130,14 @@ let rec print_size_exp ff =
|
|||
| SConst i -> fprintf ff "%d" i
|
||||
| SVar id -> fprintf ff "%s" id
|
||||
| SOp (op, e1, e2) ->
|
||||
(fprintf ff "@[(";
|
||||
print_size_exp ff e1;
|
||||
fprintf ff " %s " (op_to_string op);
|
||||
print_size_exp ff e2;
|
||||
fprintf ff ")@]")
|
||||
fprintf ff "@[(%a %s %a@]"
|
||||
print_size_exp e1 (op_to_string op) print_size_exp e2
|
||||
|
||||
let rec print_list ff print sep l =
|
||||
match l with
|
||||
| [] -> ()
|
||||
| [ x ] -> print ff x
|
||||
| x :: l -> (print ff x; fprintf ff "%s@ " sep; print_list ff print sep l)
|
||||
|
||||
let print_size_constr ff =
|
||||
function
|
||||
let print_size_constr ff = function
|
||||
| Equal (e1, e2) ->
|
||||
(fprintf ff "@[";
|
||||
print_size_exp ff e1;
|
||||
fprintf ff " = ";
|
||||
print_size_exp ff e2;
|
||||
fprintf ff "@]")
|
||||
fprintf ff "@[%a = %a@]" print_size_exp e1 print_size_exp e2
|
||||
| LEqual (e1, e2) ->
|
||||
(fprintf ff "@[";
|
||||
print_size_exp ff e1;
|
||||
fprintf ff " <= ";
|
||||
print_size_exp ff e2;
|
||||
fprintf ff "@]")
|
||||
fprintf ff "@[%a <= %a@]" print_size_exp e1 print_size_exp e2
|
||||
| False -> fprintf ff "False"
|
||||
|
||||
let psize_constr oc c =
|
||||
|
|
|
|||
|
|
@ -15,3 +15,15 @@ type ty =
|
|||
let invalid_type = Tprod []
|
||||
|
||||
let const_array_of ty n = Tarray (ty, SConst n)
|
||||
|
||||
|
||||
|
||||
open Pp_tools
|
||||
open Format
|
||||
|
||||
let rec print_type ff = function
|
||||
| Tprod ty_list ->
|
||||
fprintf ff "@[<hov2>%a@]" (print_list_r print_type "(" " *" ")") ty_list
|
||||
| Tid id -> print_longname ff id
|
||||
| Tarray (ty, n) ->
|
||||
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_size_exp n
|
||||
417
minils/minils.ml
417
minils/minils.ml
|
|
@ -65,7 +65,7 @@ and array_op =
|
|||
| Eupdate of size_exp list * exp * exp (*indices, array, value*)
|
||||
| Eselect_slice of size_exp * size_exp * exp (*lower bound, upper bound, array*)
|
||||
| Econcat of exp * exp
|
||||
| Eiterator of iterator_name * longname * size_exp list * size_exp * exp list * ident option
|
||||
| Eiterator of iterator_type * longname * size_exp list * size_exp * exp list * ident option
|
||||
|
||||
and op_desc = { op_name: longname; op_params: size_exp list; op_kind: op_kind }
|
||||
and op_kind = | Eop | Enode
|
||||
|
|
@ -135,6 +135,8 @@ type program =
|
|||
p_nodes : node_dec list;
|
||||
p_consts : const_dec list; }
|
||||
|
||||
|
||||
|
||||
(*Helper functions to build the AST*)
|
||||
|
||||
|
||||
|
|
@ -151,38 +153,35 @@ let rec size_exp_of_exp e =
|
|||
SOp(sop, size_exp_of_exp e1, size_exp_of_exp e2)
|
||||
| _ -> raise Not_static
|
||||
|
||||
(*Returns the list of bounds of an array type*)
|
||||
(** @return the list of bounds of an array type*)
|
||||
let rec bounds_list ty =
|
||||
match ty with
|
||||
| Tarray(ty, n) -> n::(bounds_list ty)
|
||||
| _ -> []
|
||||
|
||||
(** Returns the var_dec object corresponding to the name n
|
||||
in a list of var_dec. *)
|
||||
(** @return the [var_dec] object corresponding to the name [n]
|
||||
in a list of [var_dec]. *)
|
||||
let rec vd_find n = function
|
||||
| [] -> Format.printf "Not found var %s\n" (name n); raise Not_found
|
||||
| vd::l ->
|
||||
if vd.v_name = n then vd else vd_find n l
|
||||
|
||||
(** Returns whether an object of name n belongs to
|
||||
a list of var_dec. *)
|
||||
(** @return whether an object of name [n] belongs to
|
||||
a list of [var_dec]. *)
|
||||
let rec vd_mem n = function
|
||||
| [] -> false
|
||||
| vd::l -> vd.v_name = n or (vd_mem n l)
|
||||
|
||||
(** [is_record_type ty] returns whether ty corresponds to a record type. *)
|
||||
let is_record_type ty =
|
||||
match ty with
|
||||
| Tid n ->
|
||||
(try
|
||||
ignore (Modules.find_struct n);
|
||||
true
|
||||
with
|
||||
Not_found -> false
|
||||
)
|
||||
| _ -> false
|
||||
|
||||
(** @return whether [ty] corresponds to a record type. *)
|
||||
let is_record_type ty = match ty with
|
||||
| Tid n ->
|
||||
(try
|
||||
ignore (Modules.find_struct n); true
|
||||
with
|
||||
Not_found -> false)
|
||||
| _ -> false
|
||||
|
||||
(*
|
||||
module Vars =
|
||||
struct
|
||||
let rec vars_pat acc = function
|
||||
|
|
@ -316,7 +315,8 @@ struct
|
|||
| Ereset_mem (y, _, _) -> [y]
|
||||
| _ -> []
|
||||
end
|
||||
|
||||
*)
|
||||
(*
|
||||
(* data-flow dependences. pre-dependences are discarded *)
|
||||
module DataFlowDep = Make
|
||||
(struct
|
||||
|
|
@ -338,382 +338,5 @@ module AllDep = Make
|
|||
let def = Vars.def
|
||||
let antidep eq = false
|
||||
end)
|
||||
*)
|
||||
|
||||
module Printer =
|
||||
struct
|
||||
open Format
|
||||
|
||||
let is_infix =
|
||||
let module StrSet = Set.Make(String) in
|
||||
let set_infix = StrSet.singleton "or" in
|
||||
fun s ->
|
||||
if (StrSet.mem s set_infix) then true
|
||||
else begin
|
||||
match (String.get s 0) with
|
||||
| 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false
|
||||
| _ -> true
|
||||
end
|
||||
|
||||
let rec print_list ff print sep l =
|
||||
match l with
|
||||
| [] -> ()
|
||||
| [x] -> print ff x
|
||||
| x :: l ->
|
||||
print ff x;
|
||||
fprintf ff "%s@ " sep;
|
||||
print_list ff print sep l
|
||||
|
||||
let print_name ff n =
|
||||
let n = if is_infix n then
|
||||
match n with
|
||||
| "*" -> "( * )"
|
||||
| _ -> "(" ^ n ^ ")"
|
||||
else n
|
||||
in fprintf ff "%s" n
|
||||
|
||||
let print_longname ff n =
|
||||
match n with
|
||||
| Name(m) -> print_name ff m
|
||||
| Modname({ qual = "Pervasives"; id = m }) ->
|
||||
print_name ff m
|
||||
| Modname({ qual = m1; id = m2 }) ->
|
||||
fprintf ff "%s." m1; print_name ff m2
|
||||
|
||||
let print_ident ff id =
|
||||
fprintf ff "%s" (name id)
|
||||
|
||||
let rec print_pat ff = function
|
||||
| Evarpat(n) -> print_ident ff n
|
||||
| Etuplepat(pat_list) ->
|
||||
fprintf ff "@[(";
|
||||
print_list ff print_pat "," pat_list;
|
||||
fprintf ff ")@]"
|
||||
|
||||
let rec print_type ff = function
|
||||
| Tint -> fprintf ff "int"
|
||||
| Tfloat -> fprintf ff "float"
|
||||
| Tid(id) -> print_longname ff id
|
||||
| Tarray(ty, n) ->
|
||||
print_type ff ty;
|
||||
fprintf ff "^";
|
||||
print_size_exp ff n
|
||||
|
||||
let rec print_type ff = function
|
||||
| Tbase(ty) -> print_type ff ty
|
||||
| Tprod(ty_list) ->
|
||||
fprintf ff "@[(";
|
||||
print_list ff print_type " *" ty_list;
|
||||
fprintf ff ")@]"
|
||||
|
||||
let rec print_ck ff = function
|
||||
| Cbase -> fprintf ff "base"
|
||||
| Con(ck, c, n) ->
|
||||
print_ck ff ck; fprintf ff " on ";
|
||||
print_longname ff c; fprintf ff "(";
|
||||
print_ident ff n; fprintf ff ")"
|
||||
| Cvar { contents = Cindex n } -> fprintf ff "base"
|
||||
| Cvar { contents = Clink ck } -> print_ck ff ck
|
||||
|
||||
let rec print_clock ff = function
|
||||
| Ck(ck) -> print_ck ff ck
|
||||
| Cprod(ct_list) ->
|
||||
fprintf ff "@[(";
|
||||
print_list ff print_clock " *" ct_list;
|
||||
fprintf ff ")@]"
|
||||
|
||||
let print_vd ff { v_name = n; v_type = ty; v_clock = ck } =
|
||||
fprintf ff "@[<v>";
|
||||
print_ident ff n;
|
||||
fprintf ff ":";
|
||||
print_type ff ty;
|
||||
fprintf ff " at ";
|
||||
print_ck ff ck;
|
||||
fprintf ff "@]"
|
||||
|
||||
let rec print_c ff = function
|
||||
| Cint i -> fprintf ff "%d" i
|
||||
| Cfloat f -> fprintf ff "%f" f
|
||||
| Cconstr(tag) -> print_longname ff tag
|
||||
| Carray (n, c) ->
|
||||
print_c ff c;
|
||||
fprintf ff "^";
|
||||
print_size_exp ff n
|
||||
|
||||
let print_call_params ff = function
|
||||
| [] -> ()
|
||||
| l ->
|
||||
fprintf ff "<<";
|
||||
print_list ff print_size_exp "," l;
|
||||
fprintf ff ">>"
|
||||
|
||||
let rec print_exps ff e_list =
|
||||
fprintf ff "@[(";print_list ff print_exp "," e_list; fprintf ff ")@]"
|
||||
|
||||
and print_exp ff e =
|
||||
if !Misc.full_type_info then fprintf ff "(";
|
||||
begin match e.e_desc with
|
||||
| Evar x -> print_ident ff x
|
||||
| Econstvar x -> print_name ff x
|
||||
| Econst c -> print_c ff c
|
||||
| Efby(Some(c), e) ->
|
||||
print_c ff c; fprintf ff " fby "; print_exp ff e
|
||||
| Ereset_mem(y,v,res) ->
|
||||
fprintf ff "@[reset_mem ";
|
||||
print_ident ff y;
|
||||
fprintf ff " = ";
|
||||
print_c ff v;
|
||||
fprintf ff " every ";
|
||||
print_ident ff res;
|
||||
fprintf ff "@]"
|
||||
| Efby(None, e) ->
|
||||
fprintf ff "pre "; print_exp ff e
|
||||
| Eop((Name(m) | Modname { qual = "Pervasives"; id = m }), params, [e1;e2])
|
||||
when is_infix m ->
|
||||
fprintf ff "(%a %s %a %a)"
|
||||
print_exp e1
|
||||
m
|
||||
print_call_params params
|
||||
print_exp e2
|
||||
| Eop(op, params, e_list) ->
|
||||
print_longname ff op;
|
||||
print_call_params ff params;
|
||||
print_exps ff e_list
|
||||
| Eapp({ a_op = f }, params, e_list) ->
|
||||
print_longname ff f;
|
||||
print_call_params ff params;
|
||||
print_exps ff e_list
|
||||
| Eevery({ a_op = f }, params, e_list, x) ->
|
||||
print_longname ff f;
|
||||
print_call_params ff params;
|
||||
print_exps ff e_list;
|
||||
fprintf ff " every "; print_ident ff x
|
||||
| Ewhen(e, c, n) ->
|
||||
fprintf ff "(";
|
||||
print_exp ff e;
|
||||
fprintf ff " when ";
|
||||
print_longname ff c; fprintf ff "(";
|
||||
print_ident ff n; fprintf ff ")";
|
||||
fprintf ff ")"
|
||||
| Eifthenelse(e1, e2, e3) ->
|
||||
fprintf ff "@[if ";print_exp ff e1;
|
||||
fprintf ff "@ then ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@ else ";
|
||||
print_exp ff e3;
|
||||
fprintf ff "@]"
|
||||
| Emerge(x, tag_e_list) ->
|
||||
fprintf ff "@[<hov 2>merge ";print_ident ff x;fprintf ff "@ ";
|
||||
fprintf ff "@[";
|
||||
print_tag_e_list ff tag_e_list;
|
||||
fprintf ff "@]@]"
|
||||
| Etuple(e_list) ->
|
||||
fprintf ff "@[(";
|
||||
print_list ff print_exp "," e_list;
|
||||
fprintf ff ")@]"
|
||||
| Efield(e, field) ->
|
||||
print_exp ff e;
|
||||
fprintf ff ".";
|
||||
print_longname ff field
|
||||
| Estruct(f_e_list) ->
|
||||
fprintf ff "@[<v 1>{";
|
||||
print_list ff
|
||||
(fun ff (field, e) -> print_longname ff field;fprintf ff " = ";
|
||||
print_exp ff e)
|
||||
";" f_e_list;
|
||||
fprintf ff "}@]"
|
||||
(*Array operators*)
|
||||
| Earray e_list ->
|
||||
fprintf ff "@[[";
|
||||
print_list ff print_exp ";" e_list;
|
||||
fprintf ff "]@]"
|
||||
| Erepeat (n,e) ->
|
||||
print_exp ff e;
|
||||
fprintf ff "^";
|
||||
print_size_exp ff n
|
||||
| Eselect (idx,e) ->
|
||||
print_exp ff e;
|
||||
fprintf ff "[";
|
||||
print_list ff print_size_exp "][" idx;
|
||||
fprintf ff "]"
|
||||
| Eselect_dyn (idx, _, e1, e2) ->
|
||||
fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff "[";
|
||||
print_list ff print_exp "][" idx;
|
||||
fprintf ff "] default ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]"
|
||||
| Eupdate (idx, e1, e2) ->
|
||||
fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff " with [";
|
||||
print_list ff print_size_exp "][" idx;
|
||||
fprintf ff "] = ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]"
|
||||
| Eselect_slice (idx1, idx2, e) ->
|
||||
print_exp ff e;
|
||||
fprintf ff "[";
|
||||
print_size_exp ff idx1;
|
||||
fprintf ff "..";
|
||||
print_size_exp ff idx2;
|
||||
fprintf ff "]"
|
||||
| Econcat (e1, e2) ->
|
||||
print_exp ff e1;
|
||||
fprintf ff " @@ ";
|
||||
print_exp ff e2
|
||||
| Eiterator (it, f, params, n, e_list, reset) ->
|
||||
fprintf ff "(";
|
||||
fprintf ff "%s" (iterator_to_string it);
|
||||
fprintf ff " ";
|
||||
(match params with
|
||||
| [] -> print_longname ff f
|
||||
| l ->
|
||||
fprintf ff "(";
|
||||
print_longname ff f;
|
||||
print_call_params ff params;
|
||||
fprintf ff ")"
|
||||
);
|
||||
fprintf ff " <<";
|
||||
print_size_exp ff n;
|
||||
fprintf ff ">>) (@[";
|
||||
print_list ff print_exp "," e_list;
|
||||
fprintf ff ")@]";
|
||||
(match reset with
|
||||
| None -> ()
|
||||
| Some r -> fprintf ff " every %s" (name r)
|
||||
)
|
||||
| Efield_update (f, e1, e2) ->
|
||||
fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff " with .";
|
||||
print_longname ff f;
|
||||
fprintf ff " = ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]"
|
||||
end;
|
||||
if !Misc.full_type_info
|
||||
then begin
|
||||
fprintf ff " : %a)" print_type e.e_ty;
|
||||
if e.e_loc = no_location then fprintf ff " (no loc)"
|
||||
end
|
||||
and print_tag_e_list ff tag_e_list =
|
||||
print_list ff
|
||||
(fun ff (tag, e) ->
|
||||
fprintf ff "@[(";
|
||||
print_longname ff tag;
|
||||
fprintf ff " -> ";
|
||||
print_exp ff e;
|
||||
fprintf ff ")@]@,") ""
|
||||
tag_e_list
|
||||
|
||||
let print_eq ff { eq_lhs = p; eq_rhs = e } =
|
||||
fprintf ff "@[<hov 2>";
|
||||
print_pat ff p;
|
||||
(* (\* DEBUG *\) *)
|
||||
(* fprintf ff " : "; *)
|
||||
(* print_ck ff e.e_ck; *)
|
||||
(* (\* END DEBUG *\) *)
|
||||
fprintf ff " =@ ";
|
||||
print_exp ff e;
|
||||
if !Misc.full_type_info
|
||||
then begin fprintf ff "@ at "; print_ck ff e.e_ck end;
|
||||
fprintf ff ";@]"
|
||||
|
||||
let print_eqs ff l =
|
||||
fprintf ff "@[<v>"; print_list ff print_eq "" l; fprintf ff "@]"
|
||||
|
||||
let print_open_module ff name =
|
||||
fprintf ff "@[open ";
|
||||
print_name ff name;
|
||||
fprintf ff "@.@]"
|
||||
|
||||
let print_type_def ff { t_name = name; t_desc = tdesc } =
|
||||
match tdesc with
|
||||
| Type_abs -> fprintf ff "@[type %s@\n@]" name
|
||||
| Type_enum(tag_name_list) ->
|
||||
fprintf ff "@[type %s = " name;
|
||||
print_list ff print_name "|" tag_name_list;
|
||||
fprintf ff "@\n@]"
|
||||
| Type_struct(f_ty_list) ->
|
||||
fprintf ff "@[type %s = " name;
|
||||
fprintf ff "@[<v 1>{";
|
||||
print_list ff
|
||||
(fun ff (field, ty) -> print_name ff field;
|
||||
fprintf ff ": ";
|
||||
print_type ff ty) ";" f_ty_list;
|
||||
fprintf ff "}@]@\n@]"
|
||||
|
||||
let print_contract ff {c_local = l;
|
||||
c_eq = eqs;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl } =
|
||||
if l <> [] then begin
|
||||
fprintf ff "contract\n";
|
||||
fprintf ff "@[<hov 4>var ";
|
||||
print_list ff print_vd ";" l;
|
||||
fprintf ff ";@]\n"
|
||||
end;
|
||||
if eqs <> [] then begin
|
||||
fprintf ff "@[<v 2>let @,";
|
||||
print_eqs ff eqs;
|
||||
fprintf ff "@]"; fprintf ff "tel\n"
|
||||
end;
|
||||
fprintf ff "assume@ %a@;enforce@ %a with ("
|
||||
print_exp e_a
|
||||
print_exp e_g;
|
||||
print_list ff print_vd ";" cl;
|
||||
fprintf ff ")"
|
||||
|
||||
let print_node_params ff = function
|
||||
| [] -> ()
|
||||
| l ->
|
||||
fprintf ff "<<";
|
||||
print_list ff print_name "," l;
|
||||
fprintf ff ">>"
|
||||
|
||||
let print_node ff
|
||||
{ n_name = n;n_input = ni;n_output = no;
|
||||
n_contract = contract;
|
||||
n_local = nl; n_equs = ne;
|
||||
n_params = params; } =
|
||||
fprintf ff "@[<v 2>node %s" n;
|
||||
print_node_params ff params;
|
||||
fprintf ff "(@[";
|
||||
print_list ff print_vd ";" ni;
|
||||
fprintf ff "@]) returns (@[";
|
||||
print_list ff print_vd ";" no;
|
||||
fprintf ff "@])@,";
|
||||
optunit (print_contract ff) contract;
|
||||
if nl <> [] then begin
|
||||
fprintf ff "@[<hov 2>var ";
|
||||
print_list ff print_vd ";" nl;
|
||||
fprintf ff ";@]@,"
|
||||
end;
|
||||
fprintf ff "@[<v 2>let @,";
|
||||
print_eqs ff ne;
|
||||
fprintf ff "@]@;"; fprintf ff "tel";fprintf ff "@.@]"
|
||||
|
||||
let print_exp oc e =
|
||||
let ff = formatter_of_out_channel oc in
|
||||
print_exp ff e;
|
||||
fprintf ff "@."
|
||||
|
||||
let print_type oc ty =
|
||||
let ff = formatter_of_out_channel oc in
|
||||
print_type ff ty;
|
||||
fprintf ff "@?"
|
||||
|
||||
let print_clock oc ct =
|
||||
let ff = formatter_of_out_channel oc in
|
||||
print_clock ff ct;
|
||||
fprintf ff "@?"
|
||||
|
||||
let print oc { p_opened = pm; p_types = pt; p_nodes = pn } =
|
||||
let ff = formatter_of_out_channel oc in
|
||||
List.iter (print_open_module ff) pm;
|
||||
List.iter (print_type_def ff) pt;
|
||||
List.iter (print_node ff) pn;
|
||||
fprintf ff "@?"
|
||||
end
|
||||
|
|
|
|||
268
minils/minils_printer.ml
Normal file
268
minils/minils_printer.ml
Normal file
|
|
@ -0,0 +1,268 @@
|
|||
open Minils
|
||||
open Names
|
||||
open Ident
|
||||
open Types
|
||||
open Static
|
||||
open Format
|
||||
open Pp_tools
|
||||
|
||||
|
||||
let rec print_pat ff = function
|
||||
| Evarpat n -> print_ident ff n
|
||||
| Etuplepat pat_list ->
|
||||
fprintf ff "@[%a@]" (print_list_r print_pat "("","")") pat_list
|
||||
|
||||
let rec print_ck ff = function
|
||||
| Cbase -> fprintf ff "base"
|
||||
| Con (ck, c, n) ->
|
||||
fprintf ff "%a on %a(%a)" print_ck ck print_longname c print_ident n
|
||||
| Cvar { contents = Cindex n } -> fprintf ff "base"
|
||||
| Cvar { contents = Clink ck } -> print_ck ff ck
|
||||
|
||||
let rec print_clock ff = function
|
||||
| Ck ck -> print_ck ff ck
|
||||
| Cprod ct_list ->
|
||||
fprintf ff "@[%a@]" (print_list_r print_clock "("" *"")") ct_list
|
||||
|
||||
let print_vd ff { v_name = n; v_type = ty; v_clock = ck } =
|
||||
fprintf ff "@[<v>%a : %a at %a@]" print_ident n print_type ty print_ck ck
|
||||
|
||||
let rec print_c ff = function
|
||||
| Cint i -> fprintf ff "%d" i
|
||||
| Cfloat f -> fprintf ff "%f" f
|
||||
| Cconstr tag -> print_longname ff tag
|
||||
| Carray (n, c) -> fprintf ff "@[%a^%a@]" print_c c print_size_exp n
|
||||
|
||||
let print_params ff = function
|
||||
| [] -> ()
|
||||
| l -> print_list_r print_size_exp "<<"","">>" ff l
|
||||
|
||||
let rec print_args ff e_list =
|
||||
fprintf ff "@[%a@]" (print_list_r print_exp "("","")") e_list
|
||||
|
||||
and print_op ff op =
|
||||
fprintf ff "%a %a" print_longname op.op_name print_params op.op_params
|
||||
|
||||
and print_exp ff e =
|
||||
(if !Misc.full_type_info then fprintf ff "(" else ();
|
||||
(match e.e_desc with
|
||||
| Evar x -> print_ident ff x
|
||||
| Econstvar x -> print_name ff x
|
||||
| Econst c -> print_c ff c
|
||||
| Efby ((Some c), e) ->
|
||||
(print_c ff c; fprintf ff " fby "; print_exp ff e)
|
||||
| Efby (None, e) -> (fprintf ff "pre "; print_exp ff e)
|
||||
| Ecall (op, args, reset) ->
|
||||
fprintf ff "%a %a every %a" print_op op print_args args print_ident x
|
||||
| Ewhen (e, c, n) ->
|
||||
fprintf ff "@[(%a when %a(%a))@]"
|
||||
print_exp e print_longname c print_ident n
|
||||
| Eifthenelse (e1, e2, e3) ->
|
||||
fprintf ff "@[if %a@ then %a@ else @]"
|
||||
print_exp e1 print_exp e2 print_exp e3
|
||||
| Emerge (x, tag_e_list) ->
|
||||
fprintf ff "@[<hov2>merge %a@ @[%a@]@]"
|
||||
print_ident x print_tag_e_list tag_e_list
|
||||
| Etuple e_list -> (*TODO*)
|
||||
(fprintf ff "@[(";
|
||||
print_list ff print_exp "," e_list;
|
||||
fprintf ff ")@]")
|
||||
| Efield (e, field) ->
|
||||
(print_exp ff e; fprintf ff "."; print_longname ff field)
|
||||
| Estruct f_e_list ->
|
||||
(fprintf ff "@[<v 1>{";
|
||||
print_list ff
|
||||
(fun ff (field, e) ->
|
||||
(print_longname ff field; fprintf ff " = "; print_exp ff e))
|
||||
";" f_e_list;
|
||||
fprintf ff "}@]")
|
||||
| (*Array operators*) Earray e_list ->
|
||||
(fprintf ff "@[[";
|
||||
print_list ff print_exp ";" e_list;
|
||||
fprintf ff "]@]")
|
||||
| Erepeat (n, e) -> (print_exp ff e; fprintf ff "^"; print_size_exp ff n)
|
||||
| Eselect (idx, e) ->
|
||||
(print_exp ff e;
|
||||
fprintf ff "[";
|
||||
print_list ff print_size_exp "][" idx;
|
||||
fprintf ff "]")
|
||||
| Eselect_dyn (idx, _, e1, e2) ->
|
||||
(fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff "[";
|
||||
print_list ff print_exp "][" idx;
|
||||
fprintf ff "] default ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]")
|
||||
| Eupdate (idx, e1, e2) ->
|
||||
(fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff " with [";
|
||||
print_list ff print_size_exp "][" idx;
|
||||
fprintf ff "] = ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]")
|
||||
| Eselect_slice (idx1, idx2, e) ->
|
||||
(print_exp ff e;
|
||||
fprintf ff "[";
|
||||
print_size_exp ff idx1;
|
||||
fprintf ff "..";
|
||||
print_size_exp ff idx2;
|
||||
fprintf ff "]")
|
||||
| Econcat (e1, e2) ->
|
||||
(print_exp ff e1; fprintf ff " @@ "; print_exp ff e2)
|
||||
| Eiterator (it, f, params, n, e_list, reset) ->
|
||||
(fprintf ff "(";
|
||||
fprintf ff "%s" (iterator_to_string it);
|
||||
fprintf ff " ";
|
||||
(match params with
|
||||
| [] -> print_longname ff f
|
||||
| l ->
|
||||
(fprintf ff "(";
|
||||
print_longname ff f;
|
||||
print_call_params ff params;
|
||||
fprintf ff ")"));
|
||||
fprintf ff " <<";
|
||||
print_size_exp ff n;
|
||||
fprintf ff ">>) (@[";
|
||||
print_list ff print_exp "," e_list;
|
||||
fprintf ff ")@]";
|
||||
(match reset with
|
||||
| None -> ()
|
||||
| Some r -> fprintf ff " every %s" (name r)))
|
||||
| Efield_update (f, e1, e2) ->
|
||||
(fprintf ff "@[";
|
||||
print_exp ff e1;
|
||||
fprintf ff " with .";
|
||||
print_longname ff f;
|
||||
fprintf ff " = ";
|
||||
print_exp ff e2;
|
||||
fprintf ff "@]"));
|
||||
if !Misc.full_type_info
|
||||
then
|
||||
(fprintf ff " : %a)" print_type e.e_ty;
|
||||
if e.e_loc = no_location then fprintf ff " (no loc)" else ())
|
||||
else ())
|
||||
|
||||
and print_tag_e_list ff tag_e_list =
|
||||
print_list ff
|
||||
(fun ff (tag, e) ->
|
||||
(fprintf ff "@[(";
|
||||
print_longname ff tag;
|
||||
fprintf ff " -> ";
|
||||
print_exp ff e;
|
||||
fprintf ff ")@]@,"))
|
||||
"" tag_e_list
|
||||
|
||||
let print_eq ff { eq_lhs = p; eq_rhs = e } = (* (\* DEBUG *\) *)
|
||||
(* fprintf ff " : "; *) (* print_ck ff e.e_ck; *)
|
||||
(* (\* END DEBUG *\) *)
|
||||
(fprintf ff "@[<hov 2>";
|
||||
print_pat ff p;
|
||||
fprintf ff " =@ ";
|
||||
print_exp ff e;
|
||||
if !Misc.full_type_info
|
||||
then (fprintf ff "@ at "; print_ck ff e.e_ck)
|
||||
else ();
|
||||
fprintf ff ";@]")
|
||||
|
||||
let print_eqs ff l =
|
||||
(fprintf ff "@[<v>"; print_list ff print_eq "" l; fprintf ff "@]")
|
||||
|
||||
let print_open_module ff name =
|
||||
(fprintf ff "@[open "; print_name ff name; fprintf ff "@.@]")
|
||||
|
||||
let print_type_def ff { t_name = name; t_desc = tdesc } =
|
||||
match tdesc with
|
||||
| Type_abs -> fprintf ff "@[type %s@\n@]" name
|
||||
| Type_enum tag_name_list ->
|
||||
(fprintf ff "@[type %s = " name;
|
||||
print_list ff print_name "|" tag_name_list;
|
||||
fprintf ff "@\n@]")
|
||||
| Type_struct f_ty_list ->
|
||||
(fprintf ff "@[type %s = " name;
|
||||
fprintf ff "@[<v 1>{";
|
||||
print_list ff
|
||||
(fun ff (field, ty) ->
|
||||
(print_name ff field; fprintf ff ": "; print_type ff ty))
|
||||
";" f_ty_list;
|
||||
fprintf ff "}@]@\n@]")
|
||||
|
||||
let print_contract ff
|
||||
{
|
||||
c_local = l;
|
||||
c_eq = eqs;
|
||||
c_assume = e_a;
|
||||
c_enforce = e_g;
|
||||
c_controllables = cl
|
||||
} =
|
||||
(if l <> []
|
||||
then
|
||||
(fprintf ff "contract\n";
|
||||
fprintf ff "@[<hov 4>var ";
|
||||
print_list ff print_vd ";" l;
|
||||
fprintf ff ";@]\n")
|
||||
else ();
|
||||
if eqs <> []
|
||||
then
|
||||
(fprintf ff "@[<v 2>let @,";
|
||||
print_eqs ff eqs;
|
||||
fprintf ff "@]";
|
||||
fprintf ff "tel\n")
|
||||
else ();
|
||||
fprintf ff "assume@ %a@;enforce@ %a with (" print_exp e_a print_exp e_g;
|
||||
print_list ff print_vd ";" cl;
|
||||
fprintf ff ")")
|
||||
|
||||
let print_node_params ff =
|
||||
function
|
||||
| [] -> ()
|
||||
| l -> (fprintf ff "<<"; print_list ff print_name "," l; fprintf ff ">>")
|
||||
|
||||
let print_node ff
|
||||
{
|
||||
n_name = n;
|
||||
n_input = ni;
|
||||
n_output = no;
|
||||
n_contract = contract;
|
||||
n_local = nl;
|
||||
n_equs = ne;
|
||||
n_params = params
|
||||
} =
|
||||
(fprintf ff "@[<v 2>node %s" n;
|
||||
print_node_params ff params;
|
||||
fprintf ff "(@[";
|
||||
print_list ff print_vd ";" ni;
|
||||
fprintf ff "@]) returns (@[";
|
||||
print_list ff print_vd ";" no;
|
||||
fprintf ff "@])@,";
|
||||
optunit (print_contract ff) contract;
|
||||
if nl <> []
|
||||
then
|
||||
(fprintf ff "@[<hov 2>var ";
|
||||
print_list ff print_vd ";" nl;
|
||||
fprintf ff ";@]@,")
|
||||
else ();
|
||||
fprintf ff "@[<v 2>let @,";
|
||||
print_eqs ff ne;
|
||||
fprintf ff "@]@;";
|
||||
fprintf ff "tel";
|
||||
fprintf ff "@.@]")
|
||||
|
||||
let print_exp oc e =
|
||||
let ff = formatter_of_out_channel oc in (print_exp ff e; fprintf ff "@.")
|
||||
|
||||
let print_type oc ty =
|
||||
let ff = formatter_of_out_channel oc in (print_type ff ty; fprintf ff "@?")
|
||||
|
||||
let print_clock oc ct =
|
||||
let ff = formatter_of_out_channel oc
|
||||
in (print_clock ff ct; fprintf ff "@?")
|
||||
|
||||
let print oc { p_opened = pm; p_types = pt; p_nodes = pn } =
|
||||
let ff = formatter_of_out_channel oc
|
||||
in
|
||||
(List.iter (print_open_module ff) pm;
|
||||
List.iter (print_type_def ff) pt;
|
||||
List.iter (print_node ff) pn;
|
||||
fprintf ff "@?")
|
||||
107
utilities/pp_tools.ml
Normal file
107
utilities/pp_tools.ml
Normal file
|
|
@ -0,0 +1,107 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* Lucid Synchrone V4 *)
|
||||
(* Copyright (C) 2008 Marc Pouzet *)
|
||||
(* Organization : LRI, University of Paris-Sud, Orsay *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
(* useful stuff for printing *)
|
||||
(* $Id: pp_tools.ml,v 1.12.4.1 2009-07-12 09:40:19 gerard Exp $ *)
|
||||
|
||||
open Format
|
||||
|
||||
let rec print_list print ff = function
|
||||
| [] -> ()
|
||||
| x::l ->
|
||||
fprintf ff "@[<hv2>%a@]" print x;
|
||||
List.iter (fprintf ff "@ @[<hv2>%a@]" print) l
|
||||
|
||||
(** print the list x1...xn : \@\[[lp][x1][sep] [x2]...[sep] [xn][rp]\]\@
|
||||
and nothing if the list is empty *)
|
||||
let rec print_list_r print lp sep rp ff = function
|
||||
| [] -> ()
|
||||
| x :: l ->
|
||||
fprintf ff "@[<hv2>%s%a" lp print x;
|
||||
List.iter (fprintf ff "%s@]@ @[<hv2>%a" sep print) l;
|
||||
fprintf ff "%s@]" rp
|
||||
|
||||
(** print the list x1...xn : \@\[[lp][x1] [sep][x2]... [sep][xn][rp]\]\@
|
||||
and nothing if the list is empty *)
|
||||
let rec print_list_l print lp sep rp ff = function
|
||||
| [] -> ()
|
||||
| x :: l ->
|
||||
fprintf ff "@[<hv2>%s%a" lp print x;
|
||||
List.iter (fprintf ff "@]@ @[<hv2>%s%a" sep print) l;
|
||||
fprintf ff "%s@]" rp
|
||||
(*
|
||||
let rec print_list_rb print lp sep rp ff = function
|
||||
| [] -> ()
|
||||
| x :: l ->
|
||||
fprintf ff "@[<2>%s%a" lp print x;
|
||||
List.iter (fprintf ff "%s@]@ @[<2>%a" sep print) l;
|
||||
fprintf ff "%s@]" rp
|
||||
|
||||
let rec print_list_lb print lp sep rp ff = function
|
||||
| [] -> ()
|
||||
| x :: l ->
|
||||
fprintf ff "@[<2>%s%a@]" lp print x;
|
||||
List.iter (fprintf ff "@]@ @[<2>%s%a" sep print) l;
|
||||
fprintf ff "%s@]" rp
|
||||
*)
|
||||
let print_couple print1 print2 lp sep rp ff (c1, c2) =
|
||||
fprintf ff "%s%a%s@ %a%s" lp print1 c1 sep print2 c2 rp
|
||||
|
||||
let print_couple2 print1 print2 lp sep1 sep2 rp ff (c1, c2) =
|
||||
fprintf ff "%s%a%s@ %s%a%s" lp print1 c1 sep1 sep2 print2 c2 rp
|
||||
|
||||
let print_opt print ff = function
|
||||
| None -> ()
|
||||
| Some(s) -> print ff s
|
||||
|
||||
let print_opt_magic print ff = function
|
||||
| None -> pp_print_string ff "Obj.magic ()"
|
||||
| Some(e) -> print ff e
|
||||
|
||||
|
||||
let print_opt2 print sep ff = function
|
||||
| None -> ()
|
||||
| Some(s) -> fprintf ff "%s%a" sep print s
|
||||
|
||||
let print_record print ff r =
|
||||
fprintf ff "@[<hv2>%a@]" (print_list_r print "{ "";"" }") r
|
||||
|
||||
let print_type_params ff pl =
|
||||
print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") " ff pl
|
||||
|
||||
|
||||
(* Map and Set redefinition to allow pretty printing
|
||||
|
||||
module type P = sig
|
||||
type t
|
||||
val fprint : Format.formatter -> t -> unit
|
||||
end
|
||||
|
||||
module type ELT = sig
|
||||
type t
|
||||
val compare : t -> t -> int
|
||||
val fprint : Format.formatter -> t -> unit
|
||||
end
|
||||
|
||||
module SetMake (Elt : ELT) = struct
|
||||
module M = Set.Make(Elt)
|
||||
include M
|
||||
let fprint ff es =
|
||||
Format.fprintf ff "@[<hov>{@ ";
|
||||
iter (fun e -> Format.fprintf ff "%a@ " Elt.fprint e) es;
|
||||
Format.fprintf ff "}@]";
|
||||
end
|
||||
|
||||
module MapMake (Key : ELT) (Elt : P) = struct
|
||||
module M = Map.Make(Key)
|
||||
include M
|
||||
let fprint prp eem =
|
||||
Format.fprintf prp "[@[<hv 2>";
|
||||
iter (fun k m -> Format.fprintf prp "@ | %a -> %a" Key.fprint k Elt.fprint m) eem;
|
||||
Format.fprintf prp "@]@ ]";
|
||||
end
|
||||
*)
|
||||
Loading…
Reference in a new issue