From e9d586dfe7dc02a08f77b41bcf60b00b4d77cbc7 Mon Sep 17 00:00:00 2001
From: Antoine Grimod <antoine.grimod@gmail.com>
Date: Tue, 13 Dec 2022 11:45:40 +0100
Subject: [PATCH] adding automaton

---
 src/ast.ml     |  3 +++
 src/lexer.mll  |  7 +++++++
 src/parser.mly | 24 ++++++++++++++++++++++++
 src/pp.ml      | 27 ++++++++++++++++++++++++++-
 src/test.node  |  7 +++++++
 5 files changed, 67 insertions(+), 1 deletion(-)

diff --git a/src/ast.ml b/src/ast.ml
index c7e96df..5491e59 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -48,6 +48,7 @@ type t_expression =
   | EConst of full_ty * const
   | ETuple of full_ty * (t_expression list)
   | EApp   of full_ty * t_node * t_expression
+  | EAuto  of full_ty * t_state * t_state list (* initial state and transitions *)
 
 and t_varlist = full_ty * (t_var list)
 
@@ -55,6 +56,8 @@ and t_equation = t_varlist * t_expression
 
 and t_eqlist = t_equation list
 
+and t_state = | State of ident * t_eqlist * t_expression * ident
+
 and t_node =
   {
     n_name : ident;
diff --git a/src/lexer.mll b/src/lexer.mll
index 5802800..b11ee74 100644
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -30,6 +30,12 @@
       ("true", CONST_BOOL(true));
       ("false", CONST_BOOL(false));
       ("fby", BO_fby);
+      ("automaton", AUTOMAT);
+      ("match", MATCH);
+      ("with", WITH);
+      ("until", UNTIL);
+      ("do", DO);
+      ("done", DONE);
       ];
     fun s ->
       try Hashtbl.find h s with Not_found -> IDENT s
@@ -61,6 +67,7 @@ rule token = parse
   | '/'             { BO_div }
   | '%'             { BO_mod }
   | "->"            { BO_arrow }
+  | '|'             { CASE }
   | "--"            { read_single_line_comment lexbuf }
   | eof             { EOF }
   | _               { raise (Lexing_error (Format.sprintf "Error when seeing %s" (lexeme lexbuf)))}
diff --git a/src/parser.mly b/src/parser.mly
index d2f84fe..cd3b358 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -2,6 +2,7 @@
   open Ast
   open Utils
 
+  let bloop () = Format.printf "bloop\n"
   let current_location () = symbol_start_pos (), symbol_end_pos ()
 
   let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar
@@ -146,6 +147,14 @@
 %token THEN
 %token ELSE
 
+%token AUTOMAT
+%token CASE
+%token MATCH
+%token WITH
+%token DO
+%token DONE
+%token UNTIL
+
 %token<int> CONST_INT
 %token<bool> CONST_BOOL
 %token<Ast.real> CONST_REAL
@@ -383,3 +392,18 @@ ident_comma_list:
   | IDENT COMMA ident_comma_list { $1 :: $3 }
 ;
 
+automaton:
+  AUTOMAT transition_list { bloop(); EAuto( [], List.hd $2, $2 ) }
+;
+
+transition:
+  | CASE IDENT BO_arrow DO equations DONE { 
+      State($2, $5, EConst([TBool], CBool(true)), $2) }
+  | CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
+      State($2, $5, $7, $9)}
+;
+
+transition_list:
+  | transition { [$1] }
+  | transition transition_list { $1 :: $2 }
+;
diff --git a/src/pp.ml b/src/pp.ml
index cda000b..cf817ef 100644
--- a/src/pp.ml
+++ b/src/pp.ml
@@ -51,6 +51,28 @@ let pp_expression =
             (pp_expression_list prefix) (ETuple (tt, exprs))
       | _ -> raise (MyTypeError "This exception should not have been raised.")
     in
+    let rec pp_equations prefix fmt equations = 
+      match equations with
+        | [] -> ()
+        | (patt, expr) :: eqs ->
+            Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t  left side: %a\n\t\t  right side:\n%a\n%a"
+              debug_type_pp (Utils.type_exp expr)
+              pp_varlist patt
+              (pp_expression_aux prefix) expr
+              (pp_equations prefix) eqs
+    in
+    let rec pp_state_list prefix fmt states = 
+      match states with
+      | [] -> ()
+      | State(name, actions, condition, next)::q ->
+          Format.fprintf fmt "%s|%s->DO\n%a%sUNTIL\n%aTHEN%s"
+            prefix
+            name
+            (pp_equations prefix) actions
+            prefix
+            (pp_expression_aux (upd_prefix prefix)) condition
+            next
+    in
     match expression with
     | EWhen (_, e1, e2) ->
         begin
@@ -129,7 +151,10 @@ let pp_expression =
           (pp_expression_list prefix) args
     | ETuple _ ->
         Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix
-          (pp_expression_list prefix) expression;
+          (pp_expression_list prefix) expression
+    | EAuto (_, _, states) ->
+        Format.fprintf fmt "\t\t\t%sAutomaton\n%a" prefix 
+          (pp_state_list prefix) states;
     in
   pp_expression_aux ""
 
diff --git a/src/test.node b/src/test.node
index 81545bb..ed4b77a 100644
--- a/src/test.node
+++ b/src/test.node
@@ -10,3 +10,10 @@ let
 	(l1, l2) = diagonal_int(i);
 	o = (not (not (l1 = l2))) and (l1 = l2) and true;
 tel
+
+node automaton () returns (o : bool);
+let
+	automaton
+	| Incr -> do o = (pre o) + 1 done
+	| Decr -> do o = (pre o) - 1 done
+tel