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 /language | |
| parent | a9f0b829507e9882efdb59cce4d83ea7e87f5f71 (diff) | |
| parent | 4529e0acc377bed4d1bab4230f4023e4bee3ae85 (diff) | |
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/language/sail.ott b/language/sail.ott index 00a62fe3..0b83ece2 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -494,6 +494,13 @@ loop :: loop ::= {{ phantom }} | while :: :: while | until :: :: until +internal_loop_measure :: 'Measure_' ::= + {{ com internal syntax for an optional termination measure for a loop }} + {{ auxparam 'a }} + {{ aux _ l }} + | :: :: none + | 'termination_measure' { exp } :: :: some + exp :: 'E_' ::= {{ com expression }} {{ aux _ annot }} {{ auxparam 'a }} @@ -529,10 +536,10 @@ exp :: 'E_' ::= {{ com conditional }} | if exp1 then exp2 :: S :: ifnoelse {{ ichlo [[ if exp1 then exp2 else ( ) ]] }} - | loop exp1 exp2 :: :: loop - | while exp1 do exp2 :: S :: while {{ ichlo [[ loop while exp1 exp2 ]] }} - | repeat exp1 until exp2 :: S :: until {{ ichlo [[ loop until exp2 exp1 ]] }} - | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} + | loop internal_loop_measure exp1 exp2 :: :: loop + | while internal_loop_measure exp1 do exp2 :: S :: while {{ ichlo [[ loop internal_loop_measure while exp1 exp2 ]] }} + | repeat internal_loop_measure exp1 until exp2 :: S :: until {{ ichlo [[ loop internal_loop_measure until exp2 exp1 ]] }} + | foreach ( id from exp1 to exp2 by exp3 in order ) exp4 :: :: for {{ com loop }} % vectors | [ exp1 , ... , expn ] :: :: vector {{ com vector (indexed from 0) }} @@ -894,6 +901,10 @@ prec :: '' ::= | infixl :: :: InfixL | infixr :: :: InfixR +loop_measure :: '' ::= + {{ auxparam 'a }} + | loop exp :: :: Loop + def :: 'DEF_' ::= {{ com top-level definition }} {{ auxparam 'a }} @@ -917,6 +928,8 @@ def :: 'DEF_' ::= {{ com scattered function and type definition }} | 'termination_measure' id pat = exp :: :: measure {{ com separate termination measure declaration }} + | 'termination_measure' id loop_measure1 , .. , loop_measuren :: :: loop_measures + {{ com separate termination measure declaration }} | dec_spec :: :: reg_dec {{ com register declaration }} | fundef1 .. fundefn :: I :: internal_mutrec |