Merge branch 'experiments' of bitbucket.org:Peter_Sewell/sail into experiments

1 files changed, 20 insertions, 0 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 58a96e62..fdb65386 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -519,6 +519,26 @@ let doc_exp_lem, doc_let_lem =
                    (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body))
                 )
             )
+       | Id_aux ((Id (("while_PP" | "while_PM" |
+                       "while_MP" | "while_MM" ) as loopf),_)) ->
+          let [is_while;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_aux (Id name,_)),_)) -> string name) vars in
+               begin match vars with
+               | [v] -> v
+               | _ -> parens (separate comma vars) end
+            | E_aux (E_id (Id_aux (Id name,_)),_) ->
+               string name
+            | E_aux (E_lit (L_aux (L_unit,_)),_) ->
+               string "_" in
+          parens (
+              (prefix 2 1)
+                ((separate space) [string loopf;expY is_while;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))))
+            )
        (* | Id_aux (Id "append",_) ->
           let [e1;e2] = args in
           let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in