summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
Diffstat (limited to 'frontend')
-rw-r--r--frontend/ast.ml34
-rw-r--r--frontend/ast_printer.ml10
-rw-r--r--frontend/parser.mly14
3 files changed, 29 insertions, 29 deletions
diff --git a/frontend/ast.ml b/frontend/ast.ml
index 8392bc6..fbf099c 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -62,18 +62,18 @@ 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;
+ initial : bool;
+ st_name : id;
+ st_locals : var_def list;
+ body : eqn ext list;
+ until : transition list;
}
and transition = (expr ext) * (id ext) * bool (* bool : does it reset ? *)
and activate_block = {
- id : id;
- locals : var_def list;
- body : eqn ext list;
+ act_id : id;
+ act_locals : var_def list;
+ body : eqn ext list;
}
and activate_if =
| AST_activate_body of activate_block
@@ -82,23 +82,23 @@ and activate = activate_if * id list
and eqn =
| AST_assign of (id ext list) * (expr ext)
- | AST_guarantee of (id ext) * (expr ext)
| AST_assume of (id ext) * (expr ext)
+ | AST_guarantee of (id ext) * (expr ext)
| AST_automaton of automaton
| AST_activate of activate
type node_decl = {
- name : id;
- args : var_def list;
- ret : var_def list;
- var : var_def list;
- body : eqn ext list;
+ n_name : id;
+ args : var_def list;
+ ret : var_def list;
+ var : var_def list;
+ body : eqn ext list;
}
type const_decl = {
- name : id;
- typ : typ;
- value : expr ext;
+ c_name : id;
+ typ : typ;
+ value : expr ext;
}
type toplevel =
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index edd27e9..08f4fb4 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -205,7 +205,7 @@ and print_activate_if ind fmt = function
Format.fprintf fmt "%selse@\n" ind;
print_activate_if (indent ind) fmt e
| AST_activate_body(b) ->
- print_vars ind fmt b.locals;
+ print_vars ind fmt b.act_locals;
print_body ind fmt b.body
and print_automaton ind fmt (n, sts, r) =
@@ -215,8 +215,8 @@ and print_automaton ind fmt (n, sts, r) =
and print_state ind fmt (st, _) =
Format.fprintf fmt "%s%sstate %s@\n"
- ind (if st.initial then "initial " else "") st.name;
- print_vars ind fmt st.locals;
+ ind (if st.initial then "initial " else "") st.st_name;
+ print_vars ind fmt st.st_locals;
print_body ind fmt st.body;
if st.until <> [] then begin
Format.fprintf fmt "%suntil@\n" ind;
@@ -233,7 +233,7 @@ and print_block ind fmt b =
and print_node_decl fmt (d : node_decl) =
Format.fprintf fmt "node %s(%a) returns(%a)@\n"
- d.name
+ d.n_name
(print_list print_var_decl "; ") d.args
(print_list print_var_decl "; ") d.ret;
print_vars "" fmt d.var;
@@ -242,7 +242,7 @@ and print_node_decl fmt (d : node_decl) =
let print_const_decl fmt (d : const_decl) =
Format.fprintf fmt
"const %s: %s = %a@\n@\n"
- d.name (string_of_typ d.typ)
+ d.c_name (string_of_typ d.typ)
print_expr (fst d.value)
let print_toplevel fmt = function
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 2483f09..0d257dd 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -118,8 +118,8 @@ state:
until=trans(UNTIL)
{ if unless <> [] then failwith "UNLESS transitions not supported.";
{ initial = i;
- name = n;
- locals = (match v with Some v -> v | None -> []);
+ st_name = n;
+ st_locals = (match v with Some v -> v | None -> []);
body = b;
until = until;
} }
@@ -138,8 +138,8 @@ activate_if:
| IF c=ext(expr) THEN t=activate_if ELSE e=activate_if { AST_activate_if(c, t, e) }
| lv=option(var_decl) b=body
{ AST_activate_body {
- id = "activate"^uid();
- locals = (match lv with Some v -> v | None -> []);
+ act_id = "act"^uid();
+ act_locals = (match lv with Some v -> v | None -> []);
body = b;
} }
@@ -179,7 +179,7 @@ vars:
const_decl:
| CONST i=IDENT COLON t=typ EQUAL e=ext(expr) SEMICOLON
{ {
- name = i;
+ c_name = i;
typ = t;
value = e;
} }
@@ -195,7 +195,7 @@ node_decl:
| node_kw id=IDENT LPAREN v=vars RPAREN
RETURNS LPAREN rv=vars RPAREN
e = dbody
-{ { name = id;
+{ { n_name = id;
args = v;
ret = rv;
var = [];
@@ -205,7 +205,7 @@ node_decl:
RETURNS LPAREN rv=vars RPAREN
lv=var_decl
b=body
-{ { name = id;
+{ { n_name = id;
args = v;
ret = rv;
var = lv;