From a24882a531822ed8f71c1a5e050343ac1a8cbcfa Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 9 Mar 2018 18:32:03 +0000
Subject: Disallow impure global let bindings

Effectful expressions are monadic in Lem, causing type errors when binding them
to global immutable variables.
---
 src/type_check.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/type_check.ml b/src/type_check.ml
index ff4240aa..74e7cc80 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -3425,13 +3425,19 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
   begin
     match letbind with
     | LB_val (P_aux (P_typ (typ_annot, pat), _), bind) ->
-       let checked_bind = crule check_exp orig_env (strip_exp bind) typ_annot in
+       let checked_bind = propagate_exp_effect (crule check_exp orig_env (strip_exp bind) typ_annot) in
        let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) typ_annot in
-       [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+       if (BESet.is_empty (effect_set (effect_of checked_bind)) || !opt_no_effects)
+       then
+         [DEF_val (LB_aux (LB_val (P_aux (P_typ (typ_annot, tpat), (l, Some (orig_env, typ_annot, no_effect))), checked_bind), (l, None)))], env
+       else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of checked_bind))
     | LB_val (pat, bind) ->
-       let inferred_bind = irule infer_exp orig_env (strip_exp bind) in
+       let inferred_bind = propagate_exp_effect (irule infer_exp orig_env (strip_exp bind)) in
        let tpat, env = bind_pat_no_guard orig_env (strip_pat pat) (typ_of inferred_bind) in
-       [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
+       if (BESet.is_empty (effect_set (effect_of inferred_bind)) || !opt_no_effects)
+       then
+         [DEF_val (LB_aux (LB_val (tpat, inferred_bind), (l, None)))], env
+       else typ_error l ("Top-level definition with effects " ^ string_of_effect (effect_of inferred_bind))
   end
 
 let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
-- 
cgit v1.2.3