adding automaton

This commit is contained in:
Antoine Grimod 2022-12-13 11:45:40 +01:00
parent c4ad75e4cb
commit e9d586dfe7
5 changed files with 67 additions and 1 deletions

View File

@ -48,6 +48,7 @@ type t_expression =
| EConst of full_ty * const | EConst of full_ty * const
| ETuple of full_ty * (t_expression list) | ETuple of full_ty * (t_expression list)
| EApp of full_ty * t_node * t_expression | 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) 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_eqlist = t_equation list
and t_state = | State of ident * t_eqlist * t_expression * ident
and t_node = and t_node =
{ {
n_name : ident; n_name : ident;

View File

@ -30,6 +30,12 @@
("true", CONST_BOOL(true)); ("true", CONST_BOOL(true));
("false", CONST_BOOL(false)); ("false", CONST_BOOL(false));
("fby", BO_fby); ("fby", BO_fby);
("automaton", AUTOMAT);
("match", MATCH);
("with", WITH);
("until", UNTIL);
("do", DO);
("done", DONE);
]; ];
fun s -> fun s ->
try Hashtbl.find h s with Not_found -> IDENT s try Hashtbl.find h s with Not_found -> IDENT s
@ -61,6 +67,7 @@ rule token = parse
| '/' { BO_div } | '/' { BO_div }
| '%' { BO_mod } | '%' { BO_mod }
| "->" { BO_arrow } | "->" { BO_arrow }
| '|' { CASE }
| "--" { read_single_line_comment lexbuf } | "--" { read_single_line_comment lexbuf }
| eof { EOF } | eof { EOF }
| _ { raise (Lexing_error (Format.sprintf "Error when seeing %s" (lexeme lexbuf)))} | _ { raise (Lexing_error (Format.sprintf "Error when seeing %s" (lexeme lexbuf)))}

View File

@ -2,6 +2,7 @@
open Ast open Ast
open Utils open Utils
let bloop () = Format.printf "bloop\n"
let current_location () = symbol_start_pos (), symbol_end_pos () let current_location () = symbol_start_pos (), symbol_end_pos ()
let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar
@ -146,6 +147,14 @@
%token THEN %token THEN
%token ELSE %token ELSE
%token AUTOMAT
%token CASE
%token MATCH
%token WITH
%token DO
%token DONE
%token UNTIL
%token<int> CONST_INT %token<int> CONST_INT
%token<bool> CONST_BOOL %token<bool> CONST_BOOL
%token<Ast.real> CONST_REAL %token<Ast.real> CONST_REAL
@ -383,3 +392,18 @@ ident_comma_list:
| IDENT COMMA ident_comma_list { $1 :: $3 } | 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 }
;

View File

@ -51,6 +51,28 @@ let pp_expression =
(pp_expression_list prefix) (ETuple (tt, exprs)) (pp_expression_list prefix) (ETuple (tt, exprs))
| _ -> raise (MyTypeError "This exception should not have been raised.") | _ -> raise (MyTypeError "This exception should not have been raised.")
in 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 match expression with
| EWhen (_, e1, e2) -> | EWhen (_, e1, e2) ->
begin begin
@ -129,7 +151,10 @@ let pp_expression =
(pp_expression_list prefix) args (pp_expression_list prefix) args
| ETuple _ -> | ETuple _ ->
Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix 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 in
pp_expression_aux "" pp_expression_aux ""

View File

@ -10,3 +10,10 @@ let
(l1, l2) = diagonal_int(i); (l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true; o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel tel
node automaton () returns (o : bool);
let
automaton
| Incr -> do o = (pre o) + 1 done
| Decr -> do o = (pre o) - 1 done
tel