added automaton to ast

This commit is contained in:
Antoine Grimod 2022-12-13 15:02:54 +01:00
parent ad1f529863
commit bb017afe39
6 changed files with 41 additions and 42 deletions

View File

@ -48,7 +48,6 @@ 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)
@ -58,6 +57,10 @@ and t_eqlist = t_equation list
and t_state = | State of ident * t_eqlist * t_expression * ident and t_state = | State of ident * t_eqlist * t_expression * ident
and t_automaton = t_state * t_state list
and t_autolist = t_automaton list
and t_node = and t_node =
{ {
n_name : ident; n_name : ident;
@ -65,6 +68,7 @@ and t_node =
n_outputs: t_varlist; n_outputs: t_varlist;
n_local_vars: t_varlist; n_local_vars: t_varlist;
n_equations: t_eqlist; n_equations: t_eqlist;
n_automata: t_autolist;
n_inputs_type : full_ty; n_inputs_type : full_ty;
n_outputs_type : full_ty; n_outputs_type : full_ty;
} }

View File

@ -64,6 +64,7 @@ let _ =
let inchan = open_in !source_file in let inchan = open_in !source_file in
try try
begin begin
let _ = Parsing.set_trace true in
let res = Parser.main Lexer.token (Lexing.from_channel inchan) in let res = Parser.main Lexer.token (Lexing.from_channel inchan) in
close_in inchan; res close_in inchan; res
end end

View File

@ -7,7 +7,7 @@
let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar
let defined_vars : (ident, t_var * bool) Hashtbl.t = Hashtbl.create Config.maxvar let defined_vars : (ident, t_var) Hashtbl.t = Hashtbl.create Config.maxvar
let fetch_node (n: ident) = let fetch_node (n: ident) =
match Hashtbl.find_opt defined_nodes n with match Hashtbl.find_opt defined_nodes n with
@ -21,8 +21,9 @@
| None -> | None ->
raise (MyParsingError raise (MyParsingError
("The var "^n^" does not exist.", current_location())) ("The var "^n^" does not exist.", current_location()))
| Some (var, _) -> var | Some var -> var
(*
let fetch_var_def (n: ident) : t_var = let fetch_var_def (n: ident) : t_var =
match Hashtbl.find_opt defined_vars n with match Hashtbl.find_opt defined_vars n with
| None -> | None ->
@ -34,6 +35,7 @@
current_location())) current_location()))
| Some (var, false) -> | Some (var, false) ->
(Hashtbl.replace defined_vars n (var, true) ; var) (Hashtbl.replace defined_vars n (var, true) ; var)
*)
let concat_varlist (t1, e1) (t2, e2) = (t1 @ t2, e1 @ e2) let concat_varlist (t1, e1) (t2, e2) = (t1 @ t2, e1 @ e2)
@ -179,8 +181,9 @@ node_content:
IDENT LPAREN in_params RPAREN IDENT LPAREN in_params RPAREN
RETURNS LPAREN out_params RPAREN OPTIONAL_SEMICOL RETURNS LPAREN out_params RPAREN OPTIONAL_SEMICOL
local_params local_params
LET equations TEL OPTIONAL_SEMICOL LET node_body TEL OPTIONAL_SEMICOL
{ let node_name = $1 in { let node_name = $1 in
let (eqs, aut) = $12 in
let (t_in, e_in) = $3 in let (t_in, e_in) = $3 in
let (t_out, e_out) = $7 in let (t_out, e_out) = $7 in
let n: t_node = let n: t_node =
@ -188,11 +191,17 @@ node_content:
n_inputs = (t_in, e_in); n_inputs = (t_in, e_in);
n_outputs = (t_out, e_out); n_outputs = (t_out, e_out);
n_local_vars = $10; n_local_vars = $10;
n_equations = $12; n_equations = eqs;
n_automata = aut;
n_inputs_type = t_in; n_inputs_type = t_in;
n_outputs_type = t_out; } in n_outputs_type = t_out; } in
Hashtbl.add defined_nodes node_name n; n }; Hashtbl.add defined_nodes node_name n; n };
node_body:
| /* empty */ { ([], []) }
| equations node_body { let (eq, aut) = $2 in ($1@eq, aut) }
| automaton node_body { let (eq, aut) = $2 in (eq, $1::aut) }
OPTIONAL_SEMICOL: OPTIONAL_SEMICOL:
| /* empty */ {} | /* empty */ {}
| SEMICOL {} | SEMICOL {}
@ -227,13 +236,13 @@ param:
match typ with match typ with
| TBool -> | TBool ->
List.map (fun s -> List.map (fun s ->
Hashtbl.add defined_vars s (BVar s, false); BVar s) idents Hashtbl.add defined_vars s (BVar s); BVar s) idents
| TReal -> | TReal ->
List.map (fun s -> List.map (fun s ->
Hashtbl.add defined_vars s (RVar s, false); RVar s) idents Hashtbl.add defined_vars s (RVar s); RVar s) idents
| TInt -> | TInt ->
List.map (fun s -> List.map (fun s ->
Hashtbl.add defined_vars s (IVar s, false); IVar s) idents) } Hashtbl.add defined_vars s (IVar s); IVar s) idents) }
; ;
ident_comma_list: ident_comma_list:
@ -247,22 +256,25 @@ equations:
; ;
equation: equation:
pattern EQUAL expr | pattern EQUAL expr
{ let (t_patt, patt) = $1 in { let (t_patt, patt) = $1 in
let expr = $3 in let texpr = type_exp expr in let expr = $3 in let texpr = type_exp expr in
if t_patt = texpr if t_patt = texpr
then ((t_patt, patt), expr) then ((t_patt, patt), expr)
else (raise (MyParsingError ("The equation does not type check!", else (raise (MyParsingError ("The equation does not type check!",
current_location()))) }; current_location()))) };
automaton:
| AUTOMAT transition_list { (List.hd $2, $2)}
;
pattern: pattern:
| IDENT | IDENT
{ let v = fetch_var_def $1 in (type_var v, [v]) } { let v = fetch_var $1 in (type_var v, [v]) }
| LPAREN ident_comma_list_patt RPAREN { $2 }; | LPAREN ident_comma_list_patt RPAREN { $2 };
ident_comma_list_patt: ident_comma_list_patt:
| IDENT { make_ident (fetch_var_def $1) } | IDENT { make_ident (fetch_var $1) }
| IDENT COMMA ident_comma_list_patt { add_ident (fetch_var_def $1) $3 } | IDENT COMMA ident_comma_list_patt { add_ident (fetch_var $1) $3 }
expr: expr:
/* Note: EQUAL does not follow the nomenclature CMP_, ... */ /* Note: EQUAL does not follow the nomenclature CMP_, ... */
@ -368,6 +380,8 @@ expr:
else raise (MyParsingError ("The application does not type check!", else raise (MyParsingError ("The application does not type check!",
current_location())) current_location()))
} }
/* Automaton */
; ;
expr_comma_list: expr_comma_list:
@ -392,10 +406,6 @@ 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: transition:
| CASE IDENT BO_arrow DO equations DONE { | CASE IDENT BO_arrow DO equations DONE {
State($2, $5, EConst([TBool], CBool(true)), $2) } State($2, $5, EConst([TBool], CBool(true)), $2) }
@ -406,4 +416,5 @@ transition:
transition_list: transition_list:
| transition { [$1] } | transition { [$1] }
| transition transition_list { $1 :: $2 } | transition transition_list { $1 :: $2 }
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
; ;

View File

@ -19,6 +19,7 @@ let equation_pass f ast: t_nodelist option =
n_outputs = node.n_outputs; n_outputs = node.n_outputs;
n_local_vars = node.n_local_vars; n_local_vars = node.n_local_vars;
n_equations = eqs; n_equations = eqs;
n_automata = node.n_automata;
n_inputs_type = node.n_inputs_type; n_inputs_type = node.n_inputs_type;
n_outputs_type = node.n_outputs_type; n_outputs_type = node.n_outputs_type;
} }

View File

@ -51,28 +51,6 @@ 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
@ -152,9 +130,6 @@ let pp_expression =
| 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

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