summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
Diffstat (limited to 'frontend')
-rw-r--r--frontend/ast.ml17
-rw-r--r--frontend/ast_printer.ml1
-rw-r--r--frontend/file_parser.ml10
-rw-r--r--frontend/lexer.mll1
-rw-r--r--frontend/parser.mly9
5 files changed, 19 insertions, 19 deletions
diff --git a/frontend/ast.ml b/frontend/ast.ml
index cf04166..8392bc6 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -1,10 +1,6 @@
open Lexing
+open Util
-type position = Lexing.position
-let position_unknown = Lexing.dummy_pos
-
-type extent = position * position
-let extent_unknown = (position_unknown, position_unknown)
type 'a ext = 'a * extent
@@ -44,6 +40,7 @@ type bin_bool_op =
type expr =
| AST_identifier of id ext
+ | AST_idconst of id ext
(* on numerical values *)
| AST_int_const of string ext
| AST_real_const of string ext
@@ -74,13 +71,13 @@ and state = {
and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *)
and activate_block = {
- id : id;
- locals : var_def list;
- body : eqn ext list;
+ id : id;
+ locals : var_def list;
+ body : eqn ext list;
}
and activate_if =
- | AST_activate_body of activate_block
- | AST_activate_if of expr ext * activate_if * activate_if
+ | AST_activate_body of activate_block
+ | AST_activate_if of expr ext * activate_if * activate_if
and activate = activate_if * id list
and eqn =
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 25b1c11..edd27e9 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -152,6 +152,7 @@ let rec print_expr fmt e =
print_expr c print_expr t print_expr e
| AST_identifier (v,_) -> print_id fmt v
+ | AST_idconst (v,_) -> print_id fmt v
| AST_instance ((i,_),l, _) ->
Format.fprintf fmt "%a(%a)"
diff --git a/frontend/file_parser.ml b/frontend/file_parser.ml
index 672c695..85eb9cd 100644
--- a/frontend/file_parser.ml
+++ b/frontend/file_parser.ml
@@ -10,10 +10,8 @@ let parse_file (filename : string) : prog =
Parser.file Lexer.token lex
with
| Parser.Error ->
- Printf.eprintf "Parse error (invalid syntax) near %s\n"
- (string_of_position lex.lex_start_p);
- failwith "Parse error"
+ Util.error (Printf.sprintf "Parse error (invalid syntax) near %s"
+ (string_of_position lex.lex_start_p))
| Failure "lexing: empty token" ->
- Printf.eprintf "Parse error (invalid token) near %s\n"
- (string_of_position lex.lex_start_p);
- failwith "Parse error"
+ Util.error (Printf.sprintf "Parse error (invalid token) near %s"
+ (string_of_position lex.lex_start_p))
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index 8a4ef26..ef40aa7 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -12,6 +12,7 @@
"const", CONST;
"node", NODE;
+ "function", FUNCTION;
"returns", RETURNS;
"var", VAR;
"let", LET;
diff --git a/frontend/parser.mly b/frontend/parser.mly
index ec283c3..2483f09 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -9,7 +9,7 @@ open Util
%token IF THEN ELSE
%token NOT AND OR
%token MOD
-%token CONST NODE RETURNS
+%token CONST NODE FUNCTION RETURNS
%token VAR LET TEL
%token PRE
%token ASSUME GUARANTEE
@@ -188,8 +188,11 @@ var_decl:
| VAR l=nonempty_list(terminated(vari, SEMICOLON))
{ List.flatten l }
+node_kw:
+| NODE {}
+| FUNCTION {}
node_decl:
-| NODE id=IDENT LPAREN v=vars RPAREN
+| node_kw id=IDENT LPAREN v=vars RPAREN
RETURNS LPAREN rv=vars RPAREN
e = dbody
{ { name = id;
@@ -198,7 +201,7 @@ node_decl:
var = [];
body = e;
} }
-| NODE id=IDENT LPAREN v=vars RPAREN
+| node_kw id=IDENT LPAREN v=vars RPAREN
RETURNS LPAREN rv=vars RPAREN
lv=var_decl
b=body