jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Minils printer v1 ( not tested, with ~contracts )

Browse source
This commit is contained in:
Léonard Gérard 2010-06-17 16:09:32 +02:00
parent 545a514ba5
commit 96405852f1
4 changed files with 138 additions and 195 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
global/signature.ml
View file

@ -42,6 +42,9 @@ let mk_arg name ty =
let mk_param name =
{ p_name = name }
let print_param ff p = Names.print_name ff p.p_name
let mk_field n ty =
{ f_name = n; f_type = ty }

20
minils/analysis/clocking.ml
View file

@ -14,7 +14,7 @@
open Misc
open Ident
open Minils
open Global
open Signature
open Location
type error = | Etypeclash of ct * ct
@ -26,12 +26,13 @@ let error kind = raise (TypingError(kind))
let message e kind =
begin match kind with
Etypeclash(actual_ct, expected_ct) ->
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
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*)
end;
raise Error
@ -238,11 +239,12 @@ let typing_eqs h eq_list =
try
expect h ty_pat e
with Error ->
(* DEBUG *)
(* TODO remettre en route quand Printer fonctionne
(* DEBUG *)
Printf.eprintf "Complete expression: %a\n"
Printer.print_exp e;
Printf.eprintf "Clock pattern: %a\n"
Printer.print_clock ty_pat;
Printer.print_clock ty_pat; *)
raise Error
)
) eq_list

297
minils/minils_printer.ml
View file

@ -4,9 +4,17 @@ open Ident
open Types
open Static
open Format
open Signature
open Pp_tools
let iterator_to_string i =
match i with
| Imap -> "map"
| Ifold -> "fold"
| Imapfold -> "mapfold"
let rec print_pat ff = function
| Evarpat n -> print_ident ff n
| Etuplepat pat_list ->
@ -25,7 +33,7 @@ let rec print_clock ff = function
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
fprintf ff "@[<v>%a : %a :: %a@]" print_ident n print_type ty print_ck ck
let rec print_c ff = function
| Cint i -> fprintf ff "%d" i
@ -33,174 +41,122 @@ let rec print_c ff = function
| 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 print_params ff l = print_list_l print_size_exp "<<"","">>" ff l
let rec print_args ff e_list =
let print_node_params ff l = print_list_l print_param "<<"","">>" ff l
let print_node_args ff l = print_list_l print_vd "("","")" ff l
let print_index ff idx = print_list print_size_exp "[""][""]" ff idx
let rec print_dyn_index ff idx = print_list print_exp "[""][""]" ff idx
and 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 ())
if !Misc.full_type_info then
fprintf ff "@[<hov2>(%a@ : %a)@]" print_exp_desc e.e_desc print_type e.e_ty
else fprintf ff "%a" print_exp_desc e.e_desc
and print_every ff reset =
print_opt (fun ff id -> fprintf ff " every %a" print_ident id) ff reset
and print_exp_desc ff = function
| 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%a"
print_op op print_args args print_every reset
| 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 "@[<hv>if %a@ then %a@ else %a@]"
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 ->
fprintf ff "@[%a@]" (print_list_r print_exp "("","")") e_list
| Efield (e, field) ->
fprintf ff "%a.%a" print_exp e print_longname field
| Estruct f_e_list ->
print_record (print_couple print_longname print_exp """ =""") ff f_e_list
| Earray e_list ->
fprintf ff "@[%a@]" (print_list_r print_exp "["";""]") e_list
| Earray_op(array_op) ->
print_array_op ff array_op
| Efield_update (f, e1, e2) ->
fprintf ff "@[%a@ with .%a =@ %a@]"
print_exp e1 print_longname f print_exp e2
and print_array_op ff = function
| Erepeat (n, e) -> (print_exp ff e; fprintf ff "^"; print_size_exp ff n)
| Eselect (idx, e) -> fprintf ff "@[%a%a@]" print_exp e print_index idx
| Eselect_dyn (idx, _, e1, e2) ->
fprintf ff "@[%a%a default %a@]"
print_exp e1 print_dyn_index idx print_exp e2
| Eupdate (idx, e1, e2) ->
fprintf ff "@[%a with %a = %a@]" print_exp e1 print_index idx print_exp e2
| Eselect_slice (idx1, idx2, e) ->
fprintf ff "@[%a[%a..%a]@]"
print_exp e print_size_exp idx1 print_size_exp idx2
| Econcat (e1, e2) -> fprintf ff "%a @@ %a" print_exp e1 print_exp e2
| Eiterator (it, f, params, n, e_list, r) ->
fprintf ff "(%s (%a%a) <<%a>>)@ @[%a@]%a"
(iterator_to_string it) print_longname f print_params params
print_size_exp n (print_list_l print_exp "("","")") e_list print_every r
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
fprintf ff "@[%a@]"
(print_list
(print_couple print_longname print_exp "("" ->"")") """""") tag_e_list
let print_eq ff { eq_lhs = p; eq_rhs = e } =
if !Misc.full_type_info
then fprintf ff "@[<hov2>%a :: %a =@ %a;@]"
print_pat p print_ck e.e_ck print_exp e
else fprintf ff "@[<hov2>%a =@ %a;@]" print_pat p print_exp e
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 "@]")
fprintf ff "@\n@[<hv2>let@ %a@]@ tel" (print_list print_eq """""") l
let print_open_module ff name =
(fprintf ff "@[open "; print_name ff name; fprintf ff "@.@]")
let print_open_module ff name = fprintf ff "@[open %a@]@." print_name name
let print_type_def ff { t_name = name; t_desc = tdesc } =
match tdesc with
| Type_abs -> fprintf ff "@[type %s@\n@]" name
let rec print_type_def ff { t_name = name; t_desc = tdesc } =
fprintf ff "@[type %s%a@]@." name print_type_desc tdesc
and print_field ff field =
fprintf ff "%a:@ %a" print_name field.f_name print_type field.f_type
and print_type_desc ff = function
| Type_abs -> ()
| Type_enum tag_name_list ->
(fprintf ff "@[type %s = " name;
print_list ff print_name "|" tag_name_list;
fprintf ff "@\n@]")
fprintf ff " =@ %a" (print_list print_name """|""") tag_name_list
| 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@]")
fprintf ff " =@ %a"
(print_record print_field) f_ty_list
let print_contract ff
{
c_local = l;
c_eq = eqs;
c_assume = e_a;
c_enforce = e_g;
c_controllables = cl
} =
{ c_local = l; c_eq = eqs;
c_assume = e_a; c_enforce = e_g; c_controllables = cl } =
fprintf ff "@\n@[<v2>";
(if l <> []
then
(fprintf ff "contract\n";
fprintf ff "@[<hov 4>var ";
print_list ff print_vd ";" l;
print_list_l print_vd """;""" ff l;
fprintf ff ";@]\n")
else ();
if eqs <> []
@ -211,43 +167,22 @@ let print_contract 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 ")")
print_list_l print_vd """;""" ff 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 "@.@]")
{ n_name = n; n_input = ni; n_output = no;
n_contract = contract; n_local = nl; n_equs = ne; n_params = params } =
fprintf ff "@[<hov2>node %s%a%a@ returns %a%a@\n%a%a@]@."
n
print_node_params params
print_node_args ni
print_node_args no
(print_opt print_contract) contract
(print_list_l print_vd "var "";"";") nl
print_eqs ne
let print_exp oc e =
let ff = formatter_of_out_channel oc in (print_exp ff e; fprintf ff "@.")

13
utilities/pp_tools.ml
View file

@ -10,18 +10,21 @@
open Format
let rec print_list print ff = function
(** print the list x1...xn : \@\[[lp][x1][sep][x2]...[sep][xn][rp]\]\@
and nothing if the list is empty *)
let rec print_list print lp sep rp ff = function
| [] -> ()
| x::l ->
fprintf ff "@[<hv2>%a@]" print x;
List.iter (fprintf ff "@ @[<hv2>%a@]" print) l
fprintf ff "@[<hov2>%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_r print lp sep rp ff = function
| [] -> ()
| x :: l ->
fprintf ff "@[<hv2>%s%a" lp print x;
fprintf ff "@[<hov2>%s%a" lp print x;
List.iter (fprintf ff "%s@]@ @[<hv2>%a" sep print) l;
fprintf ff "%s@]" rp
@ -30,7 +33,7 @@ let rec print_list_r print lp sep rp ff = function
let rec print_list_l print lp sep rp ff = function
| [] -> ()
| x :: l ->
fprintf ff "@[<hv2>%s%a" lp print x;
fprintf ff "@[<hov2>%s%a" lp print x;
List.iter (fprintf ff "@]@ @[<hv2>%s%a" sep print) l;
fprintf ff "%s@]" rp
(*