Working prototype for an interpret ! But very messy.

1 files changed, 28 insertions, 10 deletions

diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 611e802..857e01d 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -57,7 +57,7 @@ let arrow_precedence = 20
 let if_precedence = 10
 
 let expr_precedence = function
-  | AST_unary (_, _) | AST_pre(_) | AST_not(_) -> 99
+  | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> 99
   | AST_binary(op, _, _) -> binary_op_precedence op
   | AST_binary_rel(r, _, _) -> binary_rel_precedence r
   | AST_binary_bool(r, _, _) -> binary_bool_precedence r
@@ -84,11 +84,6 @@ let rec string_of_typ = function
   | AST_TINT -> "int"
   | AST_TBOOL -> "bool"
   | AST_TREAL -> "real"
-  | AST_TGROUP its ->
-    List.fold_left (fun s t ->
-      (if s = "" then "" else s ^ ", ") ^ (string_of_typ t))
-      ""
-      its
 
 (* expressions *)
 
@@ -108,7 +103,7 @@ let rec print_expr fmt e =
       if expr_precedence e1 <= expr_precedence e
       then Format.fprintf fmt "(%a)" print_expr e1
       else Format.fprintf fmt "%a" print_expr e1
-  | AST_pre (e1,_) ->
+  | AST_pre ((e1,_), _) ->
       Format.pp_print_string fmt "pre ";
       if expr_precedence e1 <= expr_precedence e
       then Format.fprintf fmt "(%a)" print_expr e1
@@ -158,7 +153,7 @@ let rec print_expr fmt e =
         
   | AST_identifier (v,_) -> print_id fmt v
 
-  | AST_instance ((i,_),l) ->
+  | AST_instance ((i,_),l, _) ->
         Format.fprintf fmt "%a(%a)"
           print_id i (print_list print_expr ", ") (List.map fst l)
 
@@ -176,19 +171,42 @@ let rec print_eqn ind fmt = function
   | AST_guarantee((i, _), (e, _)) ->
       Format.fprintf fmt "%sguarantee %s: %a;@\n"
           ind i print_expr e
+  | AST_automaton a -> print_automaton ind fmt a
+
+and print_automaton ind fmt (n, sts, r) =
+  Format.fprintf fmt "%sautomaton %s@\n" ind n;
+  List.iter (print_state (indent ind) fmt) sts;
+  Format.fprintf fmt "%sreturns %a;@\n" ind (print_list print_id ", ") r
+
+and print_state ind fmt (st, _) =
+  Format.fprintf fmt "%s%sstate %s@\n"
+    ind (if st.initial then "initial " else "") st.name;
+  if st.locals <> [] then begin
+    Format.fprintf fmt "%svar" ind;
+    List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) st.locals;
+    Format.fprintf fmt "@\n";
+  end;
+  Format.fprintf fmt "%slet@\n%a%stel@\n"
+    ind (print_block ind) st.body ind;
+  if st.until <> [] then begin
+    Format.fprintf fmt "%suntil@\n" ind;
+    List.iter (fun ((e, _),(s, _)) -> 
+        Format.fprintf fmt "%sif %a resume %s;@\n" (indent ind) print_expr e s)
+      st.until
+  end
 
 and print_block ind fmt b =
   List.iter (fun (bb,_) -> print_eqn (indent ind) fmt bb) b
 
 (* declarations *)
 
-let print_var_decl fmt (pr, (i, _), ty) =
+and print_var_decl fmt (pr, (i, _), ty) =
     Format.fprintf fmt "%s%s: %s"
       (if pr then "probe " else "")
       i
       (string_of_typ ty)
 
-let print_node_decl fmt (d : node_decl) =
+and print_node_decl fmt (d : node_decl) =
     Format.fprintf fmt "node %s(%a) returns(%a)@\n"
       d.name
       (print_list print_var_decl "; ") d.args