Idris-dev
Idris-dev copied to clipboard
Expressions assigned to let variables within State Transition functions are not evaluated
Idris version : 1.31 OS : MacOS X 10.14.4
Steps to Reproduce
Create a let variable within a State Transition function's do section and apply a function to a value on it's rhs ; e.g. let a = hd snd2 below.
module Main
-- State
import Control.ST
hd : String -> Char
hd s = strHead s
tl : String -> String
tl s = strTail s
extract : (tu : Var) -> STrans m () [ tu ::: State ((Char,String)) ]
(const [ tu ::: State ((Char,String)) ])
extract tpl0 = do
tupl <- read tpl0
let snd2 = snd tupl
let a = hd snd2
let b = tl snd2
write tpl0 $ (a,b)
m2 : (Char,String) -> (STrans m ((Char,String)) [] (const []))
m2 tupl0 = do
var0 <- new tupl0
extract var0
x <- read var0
delete var0
pure x
t2 : (Char, String)
t2 =
let tu0 = (('a', "hello")) in
runPure $ m2 tu0
Expected Behavior
*./src/monadeStateTupleString> t2
('h', "ello") : (Char, String)
Observed Behavior
*./src/monadeStateTupleString> t2
(hd "hello", tl "hello") : (Char, String)