From e8697cb036720cdf75687f0c442c49dd48913bcb Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 21 Jun 2019 14:44:29 +0100
Subject: Coq: add missing property derivation casts for effectful expressions
 These don't appear much, but are now showing up in the sail-arm model due to
 an innocent change elsewhere.

---
 src/pretty_print_coq.ml           |  4 ++++
 test/coq/pass/returnwithfact.sail | 19 +++++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 test/coq/pass/returnwithfact.sail

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 3083fc29..1fea72ea 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1961,6 +1961,10 @@ let doc_exp, doc_let =
          if effects then
            match cast_ex, outer_ex with
            | ExGeneral, ExNone -> string "projT1_m" ^/^ parens epp
+           | ExGeneral, ExGeneral ->
+              if alpha_equivalent env cast_typ outer_typ
+              then epp
+              else string "derive_m" ^/^ parens epp
            | _ -> epp
          else match cast_ex with
               | ExGeneral -> string "projT1" ^/^ parens epp
diff --git a/test/coq/pass/returnwithfact.sail b/test/coq/pass/returnwithfact.sail
new file mode 100644
index 00000000..14179c17
--- /dev/null
+++ b/test/coq/pass/returnwithfact.sail
@@ -0,0 +1,19 @@
+default Order dec
+$include <prelude.sail>
+
+val f : int -> range(2,6) effect {escape}
+
+val g1 : (bool,int) -> range(0,8) effect {escape}
+
+function g1(b,x) = {
+  if b then
+    return f(x)
+  else {
+    return f(x+1);
+    5
+  }
+}
+
+val g2 : int -> range(0,8) effect {escape}
+
+function g2(x) = f(x)
-- 
cgit v1.2.3