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.
---
 test/typecheck/pass/pure_record.sail  | 4 +++-
 test/typecheck/pass/pure_record2.sail | 4 +++-
 test/typecheck/pass/pure_record3.sail | 4 +++-
 3 files changed, 9 insertions(+), 3 deletions(-)

(limited to 'test')

diff --git a/test/typecheck/pass/pure_record.sail b/test/typecheck/pass/pure_record.sail
index b56a1a98..15f14a3b 100644
--- a/test/typecheck/pass/pure_record.sail
+++ b/test/typecheck/pass/pure_record.sail
@@ -5,7 +5,9 @@ struct State ('a : Type) = {
   Z : vector(1, dec, bit)
 }
 
-let myStateM : State(bit) = {
+val myStateM : unit -> State(bit) effect {undef}
+
+function myStateM () = {
   r : State(bit) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
diff --git a/test/typecheck/pass/pure_record2.sail b/test/typecheck/pass/pure_record2.sail
index 2ca42541..cbdb2c9d 100644
--- a/test/typecheck/pass/pure_record2.sail
+++ b/test/typecheck/pass/pure_record2.sail
@@ -5,7 +5,9 @@ struct State ('a : Type) ('n : Int) = {
   Z : vector(1, dec, bit)
 }
 
-let myStateM : State(bit, 1) = {
+val myStateM : unit -> State(bit, 1) effect {undef}
+
+function myStateM () = {
   r : State(bit, 1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
diff --git a/test/typecheck/pass/pure_record3.sail b/test/typecheck/pass/pure_record3.sail
index 6db6dc5e..cd3e849a 100644
--- a/test/typecheck/pass/pure_record3.sail
+++ b/test/typecheck/pass/pure_record3.sail
@@ -7,7 +7,9 @@ struct State ('a : Type) ('n : Int) = {
 
 register procState : State(bit, 1)
 
-let myStateM : State(bit, 1) = {
+val myStateM : unit -> State(bit, 1) effect {undef}
+
+function myStateM () = {
   r : State(bit, 1) = undefined;
   r.N = 0b1;
   r.Z = 0b1;
-- 
cgit v1.2.3