diff options
| author | Thomas Bauereiss | 2017-10-31 17:30:56 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-11-02 12:58:40 +0000 |
| commit | e8cc2e365b7171635eb43853273cc9109e0e2553 (patch) | |
| tree | a3e31040295523902b8893af874f520399f59a7d /src/pretty_print_lem.ml | |
| parent | fe486c7b4126131920157c9348478fe6b40d3636 (diff) | |
Fix translation of repeat-until loops to Lem
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 67febd0a..3832c187 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -662,8 +662,10 @@ let doc_exp_lem, doc_let_lem = ) ) | Id_aux ((Id (("while_PP" | "while_PM" | - "while_MP" | "while_MM" ) as loopf),_)) -> - let [is_while;cond;body;e5] = args in + "while_MP" | "while_MM" | + "until_PP" | "until_PM" | + "until_MP" | "until_MM") as loopf),_)) -> + let [cond;body;e5] = args in let varspp = match e5 with | E_aux (E_tuple vars,_) -> let vars = List.map (fun (E_aux (E_id id,_)) -> doc_id_lem id) vars in @@ -676,7 +678,7 @@ let doc_exp_lem, doc_let_lem = string "_" in parens ( (prefix 2 1) - ((separate space) [string loopf;expY is_while;expY e5]) + ((separate space) [string loopf; expY e5]) ((prefix 0 1) (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN cond))) (parens (prefix 1 1 (separate space [string "fun";varspp;arrow]) (expN body)))) |