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 /src/rewrites.mli | |
| 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 'src/rewrites.mli')
| -rw-r--r-- | src/rewrites.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli index 330f10b4..e30a4206 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -63,6 +63,9 @@ val opt_dmono_continue : bool ref (* Generate a fresh id with the given prefix *) val fresh_id : string -> l -> id +(* Move loop termination measures into loop AST nodes *) +val move_loop_measures : 'a defs -> 'a defs + (* Re-write undefined to functions created by -undefined_gen flag *) val rewrite_undefined : bool -> Env.t -> tannot defs -> tannot defs |