diff options
| author | Brian Campbell | 2019-07-31 15:16:17 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-07-31 16:43:51 +0100 |
| commit | 2b64d1215c7b77d8cc37a4ab3c9ff2cc5a07e12b (patch) | |
| tree | b791c70a987fdad72fa7e1be15dea01f303fe32a /src | |
| parent | 98cced7ef3cf89333e0e09d4ebf9ca3262b4e947 (diff) | |
Coq: reasoning for until loops
Loops measures are now abstracted over the variables so that they can be
used in proofs. Add total Hoare logic rules for until.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 1fea72ea..52117a74 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1610,22 +1610,22 @@ let doc_exp, doc_let = ,_),body'),_) -> body' | _ -> body in - let msuffix, measure_pp = - match measure with - | None -> "", [] - | Some exp -> "T", [expY exp] - in let used_vars_body = find_e_ids body in let varstuple_pp, lambda = make_loop_vars [] varstuple in + let msuffix, measure_pp = + match measure with + | None -> "", [] + | Some exp -> "T", [parens (prefix 2 1 (group lambda) (expN exp))] + in parens ( (prefix 2 1) - ((separate space) (string (combinator ^ csuffix ^ msuffix):: - measure_pp@[varstuple_pp])) - ((prefix 0 1) - (parens (prefix 2 1 (group lambda) (expN cond))) - (parens (prefix 2 1 (group lambda) (expN body)))) + (string (combinator ^ csuffix ^ msuffix)) + (separate (break 1) + (varstuple_pp::measure_pp@ + [parens (prefix 2 1 (group lambda) (expN cond)); + parens (prefix 2 1 (group lambda) (expN body))])) ) end | Id_aux (Id "early_return", _) -> |