diff options
| author | Jon French | 2019-04-15 16:23:44 +0100 |
|---|---|---|
| committer | Jon French | 2019-04-15 16:23:44 +0100 |
| commit | a230fb980a70f0484daa01bb69c0204b431c9267 (patch) | |
| tree | 5fb4b9749afff963635b0d31301ebc3af124f208 /src/parse_ast.ml | |
| parent | a9f0b829507e9882efdb59cce4d83ea7e87f5f71 (diff) | |
| parent | 4529e0acc377bed4d1bab4230f4023e4bee3ae85 (diff) | |
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'src/parse_ast.ml')
| -rw-r--r-- | src/parse_ast.ml | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/parse_ast.ml b/src/parse_ast.ml index fcf921b7..91fb0610 100644 --- a/src/parse_ast.ml +++ b/src/parse_ast.ml @@ -238,7 +238,14 @@ and fpat = type loop = While | Until -type +type measure_aux = (* optional termination measure for a loop *) + | Measure_none + | Measure_some of exp + +and measure = + | Measure_aux of measure_aux * l + +and exp_aux = (* Expression *) E_block of (exp) list (* block (parsing conflict with structs?) *) | E_nondet of (exp) list (* block that can evaluate the contained expressions in any ordering *) @@ -251,7 +258,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_loop of loop * measure * exp * exp | E_for of id * exp * exp * exp * atyp * exp (* loop *) | E_vector of (exp) list (* vector (indexed from 0) *) | E_vector_access of exp * exp (* vector access *) @@ -489,6 +496,10 @@ dec_spec = DEC_aux of dec_spec_aux * l +type loop_measure = + | Loop of loop * exp + + type scattered_def = SD_aux of scattered_def_aux * l @@ -509,6 +520,7 @@ def = (* Top-level definition *) | DEF_default of default_typing_spec (* default kind and type assumptions *) | DEF_scattered of scattered_def (* scattered definition *) | DEF_measure of id * pat * exp (* separate termination measure declaration *) + | DEF_loop_measures of id * loop_measure list (* separate termination measure declaration *) | DEF_reg_dec of dec_spec (* register declaration *) | DEF_pragma of string * string * l | DEF_internal_mutrec of fundef list |