diff options
| author | Brian Campbell | 2019-04-15 12:08:28 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-04-15 12:08:28 +0100 |
| commit | 1f421b865a87a161a82550443a0cf39aa2642d9c (patch) | |
| tree | 61cd10e0203c7e613ba280c73360abfecad38277 /language | |
| parent | 57443173923e87f33713c99dbab9eba7e3db0660 (diff) | |
Basic loop termination measures for Coq
Currently only supports pure termination measures for loops with effects.
The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).
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 1a3148d0..1956f339 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 |