diff options
Diffstat (limited to 'language/sail.ott')
| -rw-r--r-- | language/sail.ott | 25 |
1 files changed, 19 insertions, 6 deletions
diff --git a/language/sail.ott b/language/sail.ott index 1a3148d0..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) }} @@ -822,8 +829,8 @@ val_spec {{ ocaml 'a val_spec }} {{ lem val_spec 'a }} :: 'VS_' ::= val_spec_aux :: 'VS_' ::= {{ com value type specification }} - {{ ocaml VS_val_spec of typschm * id * (string -> string option) * bool }} - {{ lem VS_val_spec of typschm * id * (string -> maybe string) * bool }} + {{ ocaml VS_val_spec of typschm * id * (string * string) list * bool }} + {{ lem VS_val_spec of typschm * id * list (string * string) * bool }} | val typschm id :: S :: val_spec {{ com specify the type of an upcoming definition }} {{ ocaml (VS_val_spec [[typschm]] [[id]] None false) }} {{ lem }} @@ -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 |