Working prototype for an interpret ! But very messy.

4 files changed, 110 insertions, 45 deletions

diff --git a/frontend/ast.ml b/frontend/ast.ml
index b245119..50fa3f4 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -14,7 +14,6 @@ type typ =
     | AST_TINT
     | AST_TBOOL
     | AST_TREAL
-    | AST_TGROUP of typ list
 
 type unary_op =
     | AST_UPLUS
@@ -56,20 +55,29 @@ type expr =
     | AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
     | AST_not         of expr ext
     (* temporal primitives *)
-    | AST_pre         of expr ext
+    | AST_pre         of expr ext * id
     | AST_arrow       of (expr ext) * (expr ext)
     (* other *)
     | AST_if          of (expr ext) * (expr ext) * (expr ext)
-    | AST_instance    of (id ext) * (expr ext list)
-    (* (TODO) and more : when, merge, activate instances, ... *)
+    | AST_instance    of (id ext) * (expr ext list) * id
 
-type eqn =
+type var_def = bool * (id ext) * typ
+
+type automaton = id * state ext list * id list
+and  state = {
+    initial : bool;
+    name    : id;
+    locals  : var_def list;
+    body    : eqn ext list;
+    until   : transition list;
+}
+and transition = (expr ext) * (id ext)
+
+and eqn =
     | AST_assign     of (id ext list) * (expr ext)
     | AST_guarantee  of (id ext) * (expr ext)
     | AST_assume     of (id ext) * (expr ext)
-    (* (TODO) and more : automaton, activate... *)
-
-type var_def = bool * (id ext) * typ
+    | AST_automaton  of automaton
 
 type node_decl = {
     name : id;
@@ -90,3 +98,4 @@ type toplevel =
     | AST_const_decl of const_decl ext
 
 type prog = toplevel list
+
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
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index 1fd638b..9dc7da3 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -6,32 +6,39 @@
   let kwd_table = Hashtbl.create 10
   let () = List.iter (fun (a, b) -> Hashtbl.add kwd_table a b)
     [
-      "bool",     BOOL;
-      "int",      INT;
-      "real",     REAL;
+      "bool",       BOOL;
+      "int",        INT;
+      "real",       REAL;
 
-      "const",    CONST;
-      "node",     NODE;
-      "returns",  RETURNS;
-      "var",      VAR;
-      "let",      LET;
-      "tel",      TEL;
+      "const",      CONST;
+      "node",       NODE;
+      "returns",    RETURNS;
+      "var",        VAR;
+      "let",        LET;
+      "tel",        TEL;
 
-      "if",       IF;
-      "then",     THEN;
-      "else",     ELSE;
-      "pre",      PRE;
-      "not",      NOT;
-      "and",      AND;
-      "or",       OR;
-      "mod",      MOD;
+      "if",         IF;
+      "then",       THEN;
+      "else",       ELSE;
+      "pre",        PRE;
+      "not",        NOT;
+      "and",        AND;
+      "or",         OR;
+      "mod",        MOD;
 
-      "true",     TRUE;
-      "false",    FALSE;
+      "automaton",  AUTOMATON;
+      "state",      STATE;
+      "initial",    INITIAL;
+      "unless",     UNLESS;
+      "until",      UNTIL;
+      "resume",     RESUME;
 
-      "assume",   ASSUME;
-      "guarantee",GUARANTEE;
-      "probe",    PROBE;
+      "true",       TRUE;
+      "false",      FALSE;
+
+      "assume",     ASSUME;
+      "guarantee",  GUARANTEE;
+      "probe",      PROBE;
     ]
 }
 
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 51974d1..fb00478 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -1,5 +1,6 @@
 %{
 open Ast
+open Util
 %}
 
 %token BOOL INT REAL
@@ -12,6 +13,7 @@ open Ast
 %token VAR LET TEL
 %token PRE
 %token ASSUME GUARANTEE
+%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME
 
 %token LPAREN RPAREN
 %token LCURLY RCURLY
@@ -57,12 +59,12 @@ primary_expr:
 | TRUE                      { AST_bool_const true }
 | FALSE                     { AST_bool_const false }
 | e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN 
-                            { AST_instance (e, l) }
+                            { AST_instance (e, l, fst e ^ uid ()) }
 
 unary_expr:
 | e=primary_expr                   { e }
 | NOT e=ext(unary_expr)            { AST_not(e) }
-| PRE e=ext(unary_expr)            { AST_pre(e) }
+| PRE e=ext(unary_expr)            { AST_pre(e, "pre"^uid()) }
 | o=unary_op e=ext(unary_expr)     { AST_unary (o, e) }
 
 %inline unary_op:
@@ -103,23 +105,52 @@ expr:
 
 
 (* Equations (can be asserts, automata, ...) *)
+automaton:
+| AUTOMATON a=IDENT? s=list(ext(state)) RETURNS r=separated_list(COMMA, IDENT)
+    { ((match a with Some n -> n | None -> "aut") ^ uid (), s, r) }
+
+state:
+| i=boption(INITIAL) STATE n=IDENT
+  unless=trans(UNLESS)
+  v=option(var_decl)
+  b=body
+  until=trans(UNTIL)
+{ if unless <> [] then failwith "UNLESS transitions not supported.";
+  { initial = i;
+    name = n;
+    locals = (match v with Some v -> v | None -> []);
+    body = b;
+    until = until;
+} }
+
+trans(TT):
+| TT t=nonempty_list(terminated(transition, SEMICOLON))   { t }
+|                                                         { [] }
+
+transition:
+| IF e=ext(expr) RESUME s=ext(IDENT)                      { (e, s) }
+
+
 eqn:
 | i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr)         
                                                 { AST_assign(i, e) }
 | ASSUME i=ext(IDENT) COLON e=ext(expr)         { AST_assume(i, e) }
 | GUARANTEE i=ext(IDENT) COLON e=ext(expr)      { AST_guarantee(i, e) }
+| a=automaton                                   { AST_automaton(a) }
 
 typ:
 | INT                                           { AST_TINT }
 | BOOL                                          { AST_TBOOL }
 | REAL                                          { AST_TREAL }
-| LPAREN l=separated_list(COMMA, typ) RPAREN    { AST_TGROUP(l) }
 
 (* Declarations *)
 dbody:
 | e=ext(eqn) SEMICOLON                          { [e] }
+| l=body                                        { l }
+
+body:
 | LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
-                                                { l }
+  { l }
 
 var:
 |   p=boption(PROBE) i=ext(IDENT)   { (p, i) }
@@ -157,7 +188,7 @@ node_decl:
 | NODE id=IDENT LPAREN v=vars RPAREN
     RETURNS LPAREN rv=vars RPAREN
     lv=var_decl
-    LET b=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
+    b=body
 { { name = id;
     args = v;
     ret = rv;