From e87d2f43beb17cec230d359189842afc5dfcb3b7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 4 May 2018 18:52:13 +0100
Subject: Rewrite constant nexps in specs (from Thomas)

---
 src/rewrites.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index a61f2622..debce3d1 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -241,8 +241,19 @@ let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
     | (l, None) -> (l, None)
   in
 
-  rewrite_defs_base {
-    rewriters_base with rewrite_exp = (fun _ -> map_exp_annot rewrite_annot)
+  let rewrite_def rewriters = function
+    | DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, Some (env, typ, eff)))) ->
+       let typschm = match typschm with
+         | TypSchm_aux (TypSchm_ts (tq, typ), l) ->
+            TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l)
+       in
+       let a = rewrite_annot (l, Some (env, typ, eff)) in
+       DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a))
+    | d -> Rewriter.rewrite_def rewriters d
+  in
+
+  rewrite_defs_base { rewriters_base with
+    rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def
     },
   rewrite_typ
 
-- 
cgit v1.2.3