Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

Expressions assigned to let variables within State Transition functions are not evaluated

Open Pytheas01 opened this issue 6 years ago • 0 comments

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)

Pytheas01 avatar May 21 '19 10:05 Pytheas01