From d39b91db5c37bd852fee19c2ab2e61bb02028cdb Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 29 May 2018 17:38:25 +0100
Subject: Coq: update foreach handling, correct field accesses

---
 src/pretty_print_coq.ml | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 2742b856..3c1d87c0 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -681,12 +681,14 @@ let doc_exp_lem, doc_let_lem =
             match args with
             | [exp1; exp2; exp3; ord_exp; vartuple; body] ->
                let loopvar, body = match body with
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body
-                 | E_aux (E_let (LB_aux (LB_val (
-                     P_aux (P_id id, _), _), _), body), _) -> id, body
+                 | E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_let (LB_aux (LB_val (_, _), _),
+                   E_aux (E_if (_,
+                   E_aux (E_let (LB_aux (LB_val (
+                     ((P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _))
+                     | (P_aux (P_var (P_aux (P_id id, _), _), _))
+                     | (P_aux (P_id id, _))), _), _),
+                     body), _), _), _)), _)), _) -> id, body
                  | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in
                let step = match ord_exp with
                  | E_aux (E_lit (L_aux (L_false, _)), _) ->
@@ -818,7 +820,7 @@ let doc_exp_lem, doc_let_lem =
              if prefix_recordtype && string_of_id tid <> "regstate"
              then (string (string_of_id tid ^ "_")) ^^ doc_id id
              else doc_id id in
-           expY fexp ^^ dot ^^ fname
+           expY fexp ^^ dot ^^ parens fname
         | _ ->
            raise (report l "E_field expression with no register or record type"))
     | E_block [] -> string "tt"
-- 
cgit v1.2.3