summaryrefslogtreecommitdiff
path: root/src/parse_ast.ml
diff options
context:
space:
mode:
authorAlasdair Armstrong2017-09-26 17:10:06 +0100
committerAlasdair Armstrong2017-09-26 17:10:06 +0100
commitced56765ec9324a0e690cbb4e790280d17413f99 (patch)
tree18584c77dc93b553b840008774fae4b46a622500 /src/parse_ast.ml
parent15309c879d2c877953512c401e66a7a48af6df97 (diff)
Added while-do and repeat-until loops to sail for translating ASL
Diffstat (limited to 'src/parse_ast.ml')
-rw-r--r--src/parse_ast.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml
index b259611d..6424d682 100644
--- a/src/parse_ast.ml
+++ b/src/parse_ast.ml
@@ -253,6 +253,7 @@ and fpat_aux = (* Field pattern *)
and fpat =
FP_aux of fpat_aux * l
+type loop = While | Until
type
exp_aux = (* Expression *)
@@ -265,6 +266,7 @@ exp_aux = (* Expression *)
| E_app_infix of exp * id * exp (* infix function application *)
| E_tuple of (exp) list (* tuple *)
| E_if of exp * exp * exp (* conditional *)
+ | E_loop of loop * exp * exp
| E_for of id * exp * exp * exp * atyp * exp (* loop *)
| E_vector of (exp) list (* vector (indexed from 0) *)
| E_vector_indexed of (exp) list * opt_default (* vector (indexed consecutively) *)