From 96405852f13a96b185911f93d08f52823796aaa5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= <leonard.gerard@ens.fr>
Date: Thu, 17 Jun 2010 16:09:32 +0200
Subject: [PATCH] Minils printer v1 ( not tested, with ~contracts )

---
 global/signature.ml         |   3 +
 minils/analysis/clocking.ml |  20 +--
 minils/minils_printer.ml    | 297 ++++++++++++++----------------------
 utilities/pp_tools.ml       |  13 +-
 4 files changed, 138 insertions(+), 195 deletions(-)

diff --git a/global/signature.ml b/global/signature.ml
index 4e9a41a..b20bea4 100644
--- a/global/signature.ml
+++ b/global/signature.ml
@@ -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 }
diff --git a/minils/analysis/clocking.ml b/minils/analysis/clocking.ml
index 2724273..6cd3c36 100644
--- a/minils/analysis/clocking.ml
+++ b/minils/analysis/clocking.ml
@@ -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
diff --git a/minils/minils_printer.ml b/minils/minils_printer.ml
index 92ea09a..0a6011e 100644
--- a/minils/minils_printer.ml
+++ b/minils/minils_printer.ml
@@ -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 "@.")
diff --git a/utilities/pp_tools.ml b/utilities/pp_tools.ml
index 6681799..0e7fc19 100644
--- a/utilities/pp_tools.ml
+++ b/utilities/pp_tools.ml
@@ -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 
 (*