diff --git a/freest/data/StandardLib/Prelude.fst b/freest/data/StandardLib/Prelude.fst
index d2efbcb8..3cd119fb 100644
--- a/freest/data/StandardLib/Prelude.fst
+++ b/freest/data/StandardLib/Prelude.fst
@@ -21,26 +21,26 @@ data Bool = True | False
 (||) = undefined @(Bool -> Bool -> Bool)
 (&&) = undefined @(Bool -> Bool -> Bool)
 
-not : Bool -> Bool
-not True  = False
-not False = True
+-- not : Bool -> Bool
+-- not True  = False
+-- not False = True
 
-otherwise : Bool
-otherwise = True
+-- otherwise : Bool
+-- otherwise = True
 
 type Maybe : *T -> *T
 data Maybe a = Nothing | Just a
 
-maybe : forall (a : *T) (b : *T). b -> (a -> b) -> Maybe a -> b
-maybe @a @b n _ Nothing  = n
-maybe @a @b _ f (Just x) = f x
+-- maybe : forall (a : *T) (b : *T). b -> (a -> b) -> Maybe a -> b
+-- maybe @a @b n _ Nothing  = n
+-- maybe @a @b _ f (Just x) = f x
 
 type Either : *T -> *T -> *T
 data Either a b = Left a | Right b
 
-either : forall (a b : *T) (c : 1T). (a -> c) -> (b -> c) -> Either a b -> c
-either @a @b @c f _ (Left x)     =  f x
-either @a @b @c _ g (Right y)    =  g y
+-- either : forall (a b : *T) (c : 1T). (a -> c) -> (b -> c) -> Either a b -> c
+-- either @a @b @c f _ (Left x)     =  f x
+-- either @a @b @c _ g (Right y)    =  g y
 
 type Ordering : *T
 data Ordering = LT | EQ | GT
@@ -62,44 +62,44 @@ type Diverge = ()
 
 -- ** Tuples
 
-fst : forall (a : 1T) (b : *T) . (a, b) -> a
-fst @a @b (x,_) = x
+-- fst : forall (a : 1T) (b : *T) . (a, b) -> a
+-- fst @a @b (x,_) = x
 
-snd : forall (a : *T) (b : 1T) . (a, b) -> b
-snd @a @b (_,y) = y
+-- snd : forall (a : *T) (b : 1T) . (a, b) -> b
+-- snd @a @b (_,y) = y
 
-swap : forall (a b : 1T). (a, b) -> (b, a)
-swap @a @b (x, y) = (y, x)
+-- swap : forall (a b : 1T). (a, b) -> (b, a)
+-- swap @a @b (x, y) = (y, x)
 
-curry : forall (a : *T) (b c : 1T). ((a, b) -> c) -> a -> b -> c
-curry @a @b @c f x y =  f (x, y)
+-- curry : forall (a : *T) (b c : 1T). ((a, b) -> c) -> a -> b -> c
+-- curry @a @b @c f x y =  f (x, y)
 
-uncurry : forall (a b c : 1T). (a -> b -> c) -> ((a, b) -> c)
-uncurry @a @b @c f (x, y) =  f x y
+-- uncurry : forall (a b c : 1T). (a -> b -> c) -> ((a, b) -> c)
+-- uncurry @a @b @c f (x, y) =  f x y
 
 -- ** Lists
-(++) : forall (a : 1T). [a] -> [a] -> [a]
-(++) @a []      ys = ys
-(++) @a (x::xs) ys = x :: ((++) @a xs ys) 
+-- (++) : forall (a : 1T). [a] -> [a] -> [a]
+-- (++) @a []      ys = ys
+-- (++) @a (x::xs) ys = x :: ((++) @a xs ys) 
 
-head : forall (a : *T). [a] -> a
-head @a []       = error @a "*** List.head: empty list"
-head @a (x :: _) = x
+-- head : forall (a : *T). [a] -> a
+-- head @a []       = error @a "*** List.head: empty list"
+-- head @a (x :: _) = x
 
-last : forall (a : *T). [a] -> a
-last @a []        = error @a "*** List.last: empty list"
-last @a (x :: []) = x
-last @a (_ :: xs) = last @a xs
+-- last : forall (a : *T). [a] -> a
+-- last @a []        = error @a "*** List.last: empty list"
+-- last @a (x :: []) = x
+-- last @a (_ :: xs) = last @a xs
 
-tail : forall (a : *T). [a] -> [a]
-tail @a []        = error @[a] "*** List.tail: empty list"
-tail @a (_ :: []) = [] @a
-tail @a (_ :: xs) = xs
+-- tail : forall (a : *T). [a] -> [a]
+-- tail @a []        = error @[a] "*** List.tail: empty list"
+-- tail @a (_ :: []) = [] @a
+-- tail @a (_ :: xs) = xs
 
-init : forall (a : *T). [a] -> [a]
-init @a []        = error @[a] "*** List.init: empty list"
-init @a (_ :: []) = [] @a
-init @a (x::xs)   = x :: init @a xs
+-- init : forall (a : *T). [a] -> [a]
+-- init @a []        = error @[a] "*** List.init: empty list"
+-- init @a (_ :: []) = [] @a
+-- init @a (x::xs)   = x :: init @a xs
 
 -- ** Comparison (only Int and Float, for now)
 (<), (<=), (==), (>=), (>), (/=) : Int -> Int -> Bool
@@ -197,400 +197,403 @@ fromInteger = undefined @(Int -> Float)
 
 -- ** Miscellaneous functions
 
-id : forall (a : 1T). a -> a
-id @a x = x
+-- id : forall (a : 1T). a -> a
+-- id @a x = x
 
-const : forall (a : 1T) (b : *T). a -> b -> a
-const @a @b x _ = x
+-- const : forall (a : 1T) (b : *T). a -> b -> a
+-- const @a @b x _ = x
 
-(.) : forall (a b c : *T). (b -> c) -> (a -> b) -> a -> c
-(.) @a @b @c f g x = f (g x)
+-- (.) : forall (a b c : *T). (b -> c) -> (a -> b) -> a -> c
+-- (.) @a @b @c f g x = f (g x)
 
-flip : forall (a b c : *T). (a -> b -> c) -> b -> a -> c
-flip @a @b @c f x y = f y x
+-- flip : forall (a b c : *T). (a -> b -> c) -> b -> a -> c
+-- flip @a @b @c f x y = f y x
 
-($) : forall (a b : 1T). (a -> b) -> a -> b
-($) @a @b f = f
+-- ($) : forall (a b : 1T). (a -> b) -> a -> b
+-- ($) @a @b f = f
 
-(|>) : forall (a b : 1T). a -> (a -> b) -> b
-(|>) @a @b x f = f x
+-- (|>) : forall (a b : 1T). a -> (a -> b) -> b
+-- (|>) @a @b x f = f x
 
-until : forall (a : *T). (a -> Bool) -> (a -> a) -> a -> a
-until @a p f = go
-  where
-    go : a -> a
-    go x | p x          = x
-         | otherwise    = go (f x)
+-- until : forall (a : *T). (a -> Bool) -> (a -> a) -> a -> a
+-- until @a p f = go
+--   where
+--     go : a -> a
+--     go x | p x          = x
+--          | otherwise    = go (f x)
 
-(;) : forall (a : *T) (b : 1T). a -> b -> b
-(;) @a @b _ x = x
+-- (;) : forall (a : *T) (b : 1T). a -> b -> b
+-- (;) @a @b _ x = x
 
 -- * Concurrency
 
-fork : forall (a : *T). (() 1-> a) -> ()
-fork = undefined @(forall (a : *T). (() 1-> a) -> ())
-
-send : forall (a : 1T). a -> forall (b : 1S). !a;b 1-> b
-send = undefined @(forall (a : 1T). a -> forall (b : 1S). !a;b 1-> b)
-
-receive : forall (a : 1T) (b : 1S). ?a;b -> (a, b)
-receive = undefined @(forall (a : 1T) (b : 1S). ?a;b -> (a, b))
-
-wait : Wait -> ()
-wait = undefined @(Wait -> ())
-
-close : Close -> ()
-close = undefined @(Close -> ())
-
--- | Sends a value on a given channel and then waits for the channel to be
--- | closed. Returns ().
-sendAndWait : forall (a : 1T). a -> !a ; Wait 1-> ()
-sendAndWait @a x c = c |> send x |> wait
-
--- | Sends a value on a given channel and then closes the channel.
--- | Returns ().
-sendAndClose : forall (a : 1T). a -> !a ; Close 1-> ()
-sendAndClose @a x c = c |> send x |> close
-
--- | Receives a value from a channel that continues to `Wait`, closes the 
--- | continuation and returns the value.
--- | 
--- | ```
--- | main : ()
--- | main =
--- |   -- create channel endpoints
--- |   let (c, s) = new @(?String ; Wait) () in
--- |   -- fork a thread that prints the received value (and closes the channel)
--- |   fork (\(_ : ()) 1-> c |> receiveAndWait @String |> putStrLn);
--- |   -- send a string through the channel (and close it)
--- |   s |> send "Hello!" |> close
--- | ```
-receiveAndWait : forall (a : 1T). ?a ; Wait -> a 
-receiveAndWait @a c =
-  let (x, c) = receive @a @Wait c in 
-  wait c;
-  x
-
--- | As in receiveAndWait only that the type is Wait and the function closes the
--- | channel rather the waiting for the channel to be closed.
-receiveAndClose : forall (a : 1T). ?a ; Close -> a 
-receiveAndClose @a c =
-  let (x, c) = receive @a @Close c in 
-  close c;
-  x
-
--- | Receives a value from a linear channel and applies a function to it.
--- | Discards the result and returns the continuation channel.
--- | 
--- | ```
--- | main : ()
--- | main =
--- |   -- create channel endpoints
--- |   let (c, s) = new @(?String ; Wait) () in
--- |   -- fork a thread that prints the received value (and closes the channel)
--- |   fork (\_:() 1-> c |> readApply @String @End putStrLn |> wait);
--- |   -- send a string through the channel (and close it)
--- |   s |> send "Hello!" |> close
--- | ```
-readApply : forall (a : *T) (b : 1S) . (a -> ()) {- Consumer a -} -> ?a ; b 1-> b
-readApply @a @b f c =
-  let (x, c) = receive c in
-  f x;
-  c
-
--- | Sends a value on a star channel. Unrestricted version of `send`.
-send_ : forall (a : 1T) . a -> *!a 1-> ()
-send_ = undefined @(forall (a : 1T) . a -> *!a 1-> ()) -- @a x c = c |> send x |> sink @*!a
-
--- | Receives a value from a star channel. Unrestricted version of `receive`.
-receive_ : forall (a : 1T) . *?a -> a
-receive_ = undefined @(forall (a : 1T) . *?a -> a) -- @a c =  c |> receive @a @*?a |> fst @a @*?a
-
-accept : forall (a : 1C). *!a -> Dual a
-accept @a c =
-  let (x, y) = channel @a in
-  send x c;
-  y
-
-forkWith : forall (a : 1C) (b : *T). (Dual a 1-> b) -> a
-forkWith @a @b f =
-  let (x, y) = channel @a in
-  fork (\(_ : ()) 1-> f y);
-  x
-
--- | Runs an infinite shared server thread given a function to serve a client (a
--- | handle), the initial state, and the server's shared channel endpoint. It can
--- | be seen as an infinite sequential application of the handle function over a
--- | newly accepted session, while continuously updating the state.
--- |   
--- | Note: this only works with session types that use session initiation.
--- | 
--- | ```
--- | type SharedCounter : *S = *?Counter
--- | type Counter : 1S = +{ Inc: Close
--- |                      , Dec: Close
--- |                      , Get: ?Int ; Close
--- |                      }
--- | 
--- | -- | Handler for a counter
--- | counterService : Int -> dualof Counter 1-> Int
--- | counterService i (Inc c) = wait c ; i + 1 
--- | counterService i (Dec c) = wait c ; i - 1
--- | counterService i (Get c) = c |> send i |> wait ; i
--- | 
--- | -- | Counter server
--- | runCounterServer : dualof SharedCounter -> Diverge
--- | runCounterServer = runServer @Counter @Int counterService 0 
--- | ```
-runServer : forall (a : 1C) (b : *T). (b -> Dual a 1-> b) -> b -> *!a -> Diverge
-runServer @a @b handle state c =
-  runServer @a @b handle (handle state (accept @a c)) c 
+-- fork : forall (a : *T). (() 1-> a) -> ()
+-- fork = undefined @(forall (a : *T). (() 1-> a) -> ())
+
+-- send : forall (a : 1T). a -> forall (b : 1S). !a;b 1-> b
+-- send = undefined @(forall (a : 1T). a -> forall (b : 1S). !a;b 1-> b)
+
+-- receive : forall (a : 1T) (b : 1S). ?a;b -> (a, b)
+-- receive = undefined @(forall (a : 1T) (b : 1S). ?a;b -> (a, b))
+
+-- wait : Wait -> ()
+-- wait = undefined @(Wait -> ())
+
+-- close : Close -> ()
+-- close = undefined @(Close -> ())
+
+-- -- | Sends a value on a given channel and then waits for the channel to be
+-- -- | closed. Returns ().
+-- sendAndWait : forall (a : 1T). a -> !a ; Wait 1-> ()
+-- sendAndWait @a x c = c |> send x |> wait
+
+-- -- | Sends a value on a given channel and then closes the channel.
+-- -- | Returns ().
+-- sendAndClose : forall (a : 1T). a -> !a ; Close 1-> ()
+-- sendAndClose @a x c = c |> send x |> close
+
+-- -- | Receives a value from a channel that continues to `Wait`, closes the 
+-- -- | continuation and returns the value.
+-- -- | 
+-- -- | ```
+-- -- | main : ()
+-- -- | main =
+-- -- |   -- create channel endpoints
+-- -- |   let (c, s) = new @(?String ; Wait) () in
+-- -- |   -- fork a thread that prints the received value (and closes the channel)
+-- -- |   fork (\(_ : ()) 1-> c |> receiveAndWait @String |> putStrLn);
+-- -- |   -- send a string through the channel (and close it)
+-- -- |   s |> send "Hello!" |> close
+-- -- | ```
+-- receiveAndWait : forall (a : 1T). ?a ; Wait -> a 
+-- receiveAndWait @a c =
+--   let (x, c) = receive @a @Wait c in 
+--   wait c;
+--   x
+
+-- -- | As in receiveAndWait only that the type is Wait and the function closes the
+-- -- | channel rather the waiting for the channel to be closed.
+-- receiveAndClose : forall (a : 1T). ?a ; Close -> a 
+-- receiveAndClose @a c =
+--   let (x, c) = receive @a @Close c in 
+--   close c;
+--   x
+
+-- -- | Receives a value from a linear channel and applies a function to it.
+-- -- | Discards the result and returns the continuation channel.
+-- -- | 
+-- -- | ```
+-- -- | main : ()
+-- -- | main =
+-- -- |   -- create channel endpoints
+-- -- |   let (c, s) = new @(?String ; Wait) () in
+-- -- |   -- fork a thread that prints the received value (and closes the channel)
+-- -- |   fork (\_:() 1-> c |> readApply @String @End putStrLn |> wait);
+-- -- |   -- send a string through the channel (and close it)
+-- -- |   s |> send "Hello!" |> close
+-- -- | ```
+-- readApply : forall (a : *T) (b : 1S) . (a -> ()) {- Consumer a -} -> ?a ; b 1-> b
+-- readApply @a @b f c =
+--   let (x, c) = receive c in
+--   f x;
+--   c
+
+-- -- | Sends a value on a star channel. Unrestricted version of `send`.
+-- -- send_ : forall (a : 1T) . a -> *!a 1-> ()
+-- -- send_ @a x c = c |> send @a @*!a x |> sink @*!a
+
+-- -- | Receives a value from a star channel. Unrestricted version of `receive`.
+-- -- receive_ : forall (a : 1T) . *?a -> a
+-- -- receive_ @a c =  c |> receive @a @*?a |> fst @a @*?a
+
+-- accept : forall (a : 1C). *!a -> Dual a
+-- accept @a c =
+--   let (x, y) = channel @a in
+--   send x c;
+--   y
+
+-- forkWith : forall (a : 1C) (b : *T). (Dual a 1-> b) -> a
+-- forkWith @a @b f =
+--   let (x, y) = channel @a in
+--   fork (\(_ : ()) 1-> f y);
+--   x
+
+-- -- | Runs an infinite shared server thread given a function to serve a client (a
+-- -- | handle), the initial state, and the server's shared channel endpoint. It can
+-- -- | be seen as an infinite sequential application of the handle function over a
+-- -- | newly accepted session, while continuously updating the state.
+-- -- |   
+-- -- | Note: this only works with session types that use session initiation.
+-- -- | 
+-- -- | ```
+-- -- | type SharedCounter : *S = *?Counter
+-- -- | type Counter : 1S = +{ Inc: Close
+-- -- |                      , Dec: Close
+-- -- |                      , Get: ?Int ; Close
+-- -- |                      }
+-- -- | 
+-- -- | -- | Handler for a counter
+-- -- | counterService : Int -> dualof Counter 1-> Int
+-- -- | counterService i (Inc c) = wait c ; i + 1 
+-- -- | counterService i (Dec c) = wait c ; i - 1
+-- -- | counterService i (Get c) = c |> send i |> wait ; i
+-- -- | 
+-- -- | -- | Counter server
+-- -- | runCounterServer : dualof SharedCounter -> Diverge
+-- -- | runCounterServer = runServer @Counter @Int counterService 0 
+-- -- | ```
+-- runServer : forall (a : 1C) (b : *T). (b -> Dual a 1-> b) -> b -> *!a -> Diverge
+-- runServer @a @b handle state c =
+--   runServer @a @b handle (handle state (accept @a c)) c 
 
 -- * I/O
 
--- ** I/O Streams
-
--- *** Input Stream
-
--- | The `InStream` type describes input streams (such as `stdin` and read
--- | files). `GetChar` reads a single character, `GetLine` reads a line, and
--- | `IsEOF` checks for the EOF (End-Of-File) token, i.e., if an input stream
--- | reached the end. Operations in this channel end with the `SWait` option.
-type InStream : 1C
-type InStream = +{ GetChar: ?Char   ; InStream
-                 , GetLine: ?String ; InStream
-                 , IsEOF  : ?Bool   ; InStream
-                 , SWait  : Wait
-                 }
-
--- | Unrestricted session type for the `OutStream` type.
-type InStreamProvider : *C
-type InStreamProvider = *?InStream
-
--- | Closes an `InStream` channel endpoint. Behaves as a `close`.
-hCloseIn : InStream -> ()
-hCloseIn c = c |> select SWait |> wait
-
-hGenericGet : forall (a : *T). (InStream -> ?a; InStream) -> InStream -> (a, InStream)
-hGenericGet @a sel c = receive @a @InStream (sel c)
-
--- | Reads a character from an `InStream` channel endpoint. Behaves as 
--- | `|> select GetChar |> receive`.
-hGetChar : InStream -> (Char, InStream)
-hGetChar = hGenericGet @Char (\(c : InStream) -> select GetChar c)
-
--- | Reads a line (as a string) from an `InStream` channel endpoint. Behaves as 
--- | `|> select GetLine |> receive`.
-hGetLine : InStream -> (String, InStream)
-hGetLine = hGenericGet @String (\(c : InStream) -> select GetLine c)
-
--- | Checks if an `InStream` reached the EOF token that marks where no more input can be read. 
--- | Does the same as `|> select IsEOF |> receive`.
-hIsEOF : InStream -> (Bool, InStream)
-hIsEOF = hGenericGet @Bool (\(c : InStream) -> select IsEOF c)
-
--- | Reads the entire content from an `InStream` (i.e. until EOF is reached). Returns the content
--- | as a single string and the continuation channel.
-hGetContent : InStream -> (String, InStream)
-hGetContent c = 
-  let (isEOF, c) = hIsEOF c in
-  if isEOF
-  then ("", c)
-  else 
-    let (line, c) = hGetLine c in 
-    let (contents, c) = hGetContent c in
-    ((++) @Char ((++) @Char line "\n") contents, c)
-
-hGenericGet_ : forall (a : *T) . (InStream -> (a, InStream)) -> InStreamProvider -> a
-hGenericGet_ @a getF inp = 
-  let (x, c) = getF $ receive_ @InStream inp in
-  hCloseIn c; 
-  x
-
--- | Unrestricted version of `hGetChar`. Behaves the same, except it first receives an `InStream` 
--- | channel endpoint (via session initiation), executes an `hGetChar` and then closes the 
--- | enpoint with `hCloseIn`.
-hGetChar_ : InStreamProvider -> Char
-hGetChar_ = hGenericGet_ @Char hGetChar
-
--- | Unrestricted version of `hGetLine`. Behaves the same, except it first receives an `InStream` 
--- | channel endpoint (via session initiation), executes an `hGetLine` and then closes the 
--- | enpoint with `hCloseIn`.
-hGetLine_ : InStreamProvider -> String
-hGetLine_ = hGenericGet_ @String hGetLine
-
--- | Unrestricted version of `hGetContent`. Behaves the same, except it first receives an `InStream`
--- | channel endpoint (via session initiation), executes an `hGetContent` and then closes the
--- | endpoint with `hCloseIn`.
-hGetContent_ : InStreamProvider -> String
-hGetContent_ inp = 
-  let (s, c) = receive_ @InStream inp |> hGetContent in
-  hCloseIn c;
-  s
-
--- *** Output Stream
-
--- | The `OutStream` type describes output streams (such as `stdout`, `stderr`
--- | and write mode files). `PutChar` outputs a character, `PutStr` outputs a string,
--- | and `PutStrLn` outputs a string followed by the newline character (`\n`).
--- | Operations in this channel must end with the `Close` option.
-type OutStream : 1C
-type OutStream = +{ PutChar : !Char ; OutStream
-                  , PutStr  : !String ; OutStream
-                  , PutStrLn: !String ; OutStream
-                  , SWait   : Wait
-                  }
-
--- | Unrestricted session type for the `OutStream` type.
-type OutStreamProvider : *C
-type OutStreamProvider = *?OutStream
-
--- | Closes an `OutStream` channel endpoint. Behaves as a `close`.
-hCloseOut : OutStream -> ()
-hCloseOut c = c |> select SWait |> wait
-
-hGenericPut : forall (a : *T) . (OutStream -> !a; OutStream) -> a -> OutStream -> OutStream
-hGenericPut @a sel x outStream = sel outStream |> send x
-
--- | Sends a character through an `OutStream` channel endpoint. Behaves as 
--- | `|> select PutChar |> send`.
-hPutChar : Char -> OutStream -> OutStream
-hPutChar = hGenericPut @Char (\(ch : OutStream) -> select PutChar ch)
-
--- | Sends a String through an `OutStream` channel endpoint. Behaves as 
--- | `|> select PutString |> send`.
-hPutStr : String -> OutStream -> OutStream
-hPutStr = hGenericPut @String (\(c : OutStream) -> select PutStr c)
-
--- | Sends a string through an `OutStream` channel endpoint, to be output with
--- | the newline character. Behaves as `|> select PutStringLn |> send`.
-hPutStrLn : String -> OutStream -> OutStream
-hPutStrLn = hGenericPut @String (\(c : OutStream) -> select PutStrLn c)
-
--- | Sends the string representation of a value through an `OutStream` channel
--- | endpoint, to be outputed with the newline character. Behaves as `hPutStrLn
--- | (show @t v)`, where `v` is the value to be sent and `t` its type.
-hPrint : forall (a : *T). a -> OutStream -> OutStream
-hPrint @a x = hPutStrLn (show @a x)
-
-hGenericPut_ : forall (a : *T). (a -> OutStream -> OutStream) -> a -> OutStreamProvider -> ()
-hGenericPut_ @a putF x outProv = 
-  hCloseOut $ putF x $ receive_ @OutStream outProv 
-
--- | Unrestricted version of `hPutChar`. Behaves the same, except it first
--- | receives an `OutStream` channel endpoint (via session initiation), executes
--- | an `hPutChar` and then closes the enpoint with `hCloseOut`.
-hPutChar_ : Char -> OutStreamProvider -> ()
-hPutChar_ = hGenericPut_ @Char hPutChar
-
--- | Unrestricted version of `hPutStr`. Behaves similarly, except that it first
--- | receives an `OutStream` channel endpoint (via session initiation), executes
--- | an `hPutStr` and then closes the enpoint with `hCloseOut`.
-hPutStr_ : String -> OutStreamProvider -> ()
-hPutStr_ = hGenericPut_ @String hPutStr
-
--- | Unrestricted version of `hPutStrLn`. Behaves similarly, except that it
--- | first receives an `OutStream` channel endpoint (via session initiation),
--- | executes an `hPutStrLn` and then closes the enpoint with `hCloseOut`.
-hPutStrLn_ : String -> OutStreamProvider -> ()
-hPutStrLn_ = hGenericPut_ @String hPutStrLn
-
--- | Unrestricted version of `hPrint`. Behaves similarly, except that it first
--- | receives an `OutStream` channel endpoint (via session initiation), executes
--- | an `hPrint` and then closes the enpoint with `hCloseOut`.
-hPrint_ : forall (a : *T). a -> OutStreamProvider -> ()
-hPrint_ @a x c = hGenericPut_ @a (hPrint @a) x c
+-- -- ** I/O Streams
+
+-- -- *** Input Stream
+
+-- -- | The `InStream` type describes input streams (such as `stdin` and read
+-- -- | files). `GetChar` reads a single character, `GetLine` reads a line, and
+-- -- | `IsEOF` checks for the EOF (End-Of-File) token, i.e., if an input stream
+-- -- | reached the end. Operations in this channel end with the `SWait` option.
+-- type InStream : 1C
+-- type InStream = +{ GetChar: ?Char   ; InStream
+--                  , GetLine: ?String ; InStream
+--                  , IsEOF  : ?Bool   ; InStream
+--                  , SWait  : Wait
+--                  }
+
+-- -- | Unrestricted session type for the `OutStream` type.
+-- type InStreamProvider : *C
+-- type InStreamProvider = *?InStream
+
+-- -- | Closes an `InStream` channel endpoint. Behaves as a `close`.
+-- hCloseIn : InStream -> ()
+-- hCloseIn c = c |> select SWait |> wait
+
+-- hGenericGet : forall (a : *T). (InStream -> ?a; InStream) -> InStream -> (a, InStream)
+-- hGenericGet @a sel c = receive @a @InStream (sel c)
+
+-- -- | Reads a character from an `InStream` channel endpoint. Behaves as 
+-- -- | `|> select GetChar |> receive`.
+-- hGetChar : InStream -> (Char, InStream)
+-- hGetChar = hGenericGet @Char (\(c : InStream) -> select GetChar c)
+
+-- -- | Reads a line (as a string) from an `InStream` channel endpoint. Behaves as 
+-- -- | `|> select GetLine |> receive`.
+-- hGetLine : InStream -> (String, InStream)
+-- hGetLine = hGenericGet @String (\(c : InStream) -> select GetLine c)
+
+-- -- | Checks if an `InStream` reached the EOF token that marks where no more input can be read. 
+-- -- | Does the same as `|> select IsEOF |> receive`.
+-- hIsEOF : InStream -> (Bool, InStream)
+-- hIsEOF = hGenericGet @Bool (\(c : InStream) -> select IsEOF c)
+
+-- -- | Reads the entire content from an `InStream` (i.e. until EOF is reached). Returns the content
+-- -- | as a single string and the continuation channel.
+-- hGetContent : InStream -> (String, InStream)
+-- hGetContent c = 
+--   let (isEOF, c) = hIsEOF c in
+--   if isEOF
+--   then ("", c)
+--   else 
+--     let (line, c) = hGetLine c in 
+--     let (contents, c) = hGetContent c in
+--     ((++) @Char ((++) @Char line "\n") contents, c)
+
+-- -- hGenericGet_ : forall (a : *T) . (InStream -> (a, InStream)) -> InStreamProvider -> a
+-- -- hGenericGet_ @a getF inp = 
+-- --   let (x, c) = getF $ receive_ @InStream inp in
+-- --   hCloseIn c; 
+-- --   x
+
+-- -- | Unrestricted version of `hGetChar`. Behaves the same, except it first receives an `InStream` 
+-- -- | channel endpoint (via session initiation), executes an `hGetChar` and then closes the 
+-- -- | enpoint with `hCloseIn`.
+-- -- hGetChar_ : InStreamProvider -> Char
+-- -- hGetChar_ = hGenericGet_ @Char hGetChar
+
+-- -- | Unrestricted version of `hGetLine`. Behaves the same, except it first receives an `InStream` 
+-- -- | channel endpoint (via session initiation), executes an `hGetLine` and then closes the 
+-- -- | enpoint with `hCloseIn`.
+-- -- hGetLine_ : InStreamProvider -> String
+-- -- hGetLine_ = hGenericGet_ @String hGetLine
+
+-- -- | Unrestricted version of `hGetContent`. Behaves the same, except it first receives an `InStream`
+-- -- | channel endpoint (via session initiation), executes an `hGetContent` and then closes the
+-- -- | endpoint with `hCloseIn`.
+-- -- hGetContent_ : InStreamProvider -> String
+-- -- hGetContent_ inp = 
+-- --   let (s, c) = receive_ @InStream inp |> hGetContent in
+-- --   hCloseIn c;
+-- --   s
+
+-- -- *** Output Stream
+
+-- -- | The `OutStream` type describes output streams (such as `stdout`, `stderr`
+-- -- | and write mode files). `PutChar` outputs a character, `PutStr` outputs a string,
+-- -- | and `PutStrLn` outputs a string followed by the newline character (`\n`).
+-- -- | Operations in this channel must end with the `Close` option.
+-- type OutStream : 1C
+-- type OutStream = +{ PutChar : !Char ; OutStream
+--                   , PutStr  : !String ; OutStream
+--                   , PutStrLn: !String ; OutStream
+--                   , SWait   : Wait
+--                   }
+
+-- -- | Unrestricted session type for the `OutStream` type.
+-- type OutStreamProvider : *C
+-- type OutStreamProvider = *?OutStream
+
+-- -- | Closes an `OutStream` channel endpoint. Behaves as a `close`.
+-- hCloseOut : OutStream -> ()
+-- hCloseOut c = c |> select SWait |> wait
+
+-- hGenericPut : forall (a : *T) . (OutStream -> !a; OutStream) -> a -> OutStream -> OutStream
+-- hGenericPut @a sel x outStream = sel outStream |> send x
+
+-- -- | Sends a character through an `OutStream` channel endpoint. Behaves as 
+-- -- | `|> select PutChar |> send`.
+-- hPutChar : Char -> OutStream -> OutStream
+-- hPutChar = hGenericPut @Char (\(ch : OutStream) -> select PutChar ch)
+
+-- -- | Sends a String through an `OutStream` channel endpoint. Behaves as 
+-- -- | `|> select PutString |> send`.
+-- hPutStr : String -> OutStream -> OutStream
+-- hPutStr = hGenericPut @String (\(c : OutStream) -> select PutStr c)
+
+-- -- | Sends a string through an `OutStream` channel endpoint, to be output with
+-- -- | the newline character. Behaves as `|> select PutStringLn |> send`.
+-- hPutStrLn : String -> OutStream -> OutStream
+-- hPutStrLn = hGenericPut @String (\(c : OutStream) -> select PutStrLn c)
+
+-- -- | Sends the string representation of a value through an `OutStream` channel
+-- -- | endpoint, to be outputed with the newline character. Behaves as `hPutStrLn
+-- -- | (show @t v)`, where `v` is the value to be sent and `t` its type.
+-- hPrint : forall (a : *T). a -> OutStream -> OutStream
+-- hPrint @a x = hPutStrLn (show @a x)
+
+-- -- hGenericPut_ : forall (a : *T). (a -> OutStream -> OutStream) -> a -> OutStreamProvider -> ()
+-- -- hGenericPut_ @a putF x outProv = 
+-- --   hCloseOut $ putF x $ receive_ @OutStream outProv 
+
+-- -- | Unrestricted version of `hPutChar`. Behaves the same, except it first
+-- -- | receives an `OutStream` channel endpoint (via session initiation), executes
+-- -- | an `hPutChar` and then closes the enpoint with `hCloseOut`.
+-- -- hPutChar_ : Char -> OutStreamProvider -> ()
+-- -- hPutChar_ = hGenericPut_ @Char hPutChar
+
+-- -- | Unrestricted version of `hPutStr`. Behaves similarly, except that it first
+-- -- | receives an `OutStream` channel endpoint (via session initiation), executes
+-- -- | an `hPutStr` and then closes the enpoint with `hCloseOut`.
+-- -- hPutStr_ : String -> OutStreamProvider -> ()
+-- -- hPutStr_ = hGenericPut_ @String hPutStr
+
+-- -- | Unrestricted version of `hPutStrLn`. Behaves similarly, except that it
+-- -- | first receives an `OutStream` channel endpoint (via session initiation),
+-- -- | executes an `hPutStrLn` and then closes the enpoint with `hCloseOut`.
+-- -- hPutStrLn_ : String -> OutStreamProvider -> ()
+-- -- hPutStrLn_ = hGenericPut_ @String hPutStrLn
+
+-- -- | Unrestricted version of `hPrint`. Behaves similarly, except that it first
+-- -- | receives an `OutStream` channel endpoint (via session initiation), executes
+-- -- | an `hPrint` and then closes the enpoint with `hCloseOut`.
+-- -- hPrint_ : forall (a : *T). a -> OutStreamProvider -> ()
+-- -- hPrint_ @a x c = hGenericPut_ @a (hPrint @a) x c
+
+putStrOut : forall (a: *T) . a -> ()
+putStrOut @a x = undefined @()
 
 -- ** Standard I/O
 
--- *** stdin
-
--- | Standard input stream. Reads from the console.
-stdinChan : (InStreamProvider, Dual InStreamProvider)
-stdinChan = channel @InStreamProvider
-
-stdin : InStreamProvider
-stdin = let (i,_) = stdinChan in i
-
-dualStdin : Dual InStreamProvider
-dualStdin = let (_,o) = stdinChan in o
-
--- | Reads a single character from `stdin`.
-getChar : () -> Char
-getChar _ = hGetChar_ stdin
-
--- | Reads a single line from `stdin`. 
-getLine : () -> String
-getLine _ = hGetLine_ stdin
-
--- **** Internal stdin functions
-
-internalGetChar : () -> Char
-internalGetChar = undefined @(() -> Char)
-internalGetLine : () -> String
-internalGetLine = undefined @(() -> String)
-internalGetContents : () -> String
-internalGetContents = undefined @(() -> String)
-
-runReader : () -> Dual InStream 1-> ()
-runReader _ (&GetChar reader) = runReader () $ send (internalGetChar ()) reader
-runReader _ (&GetLine reader) = runReader () $ send (internalGetLine ()) reader
-runReader _ (&IsEOF   reader) = runReader () $ send False reader -- stdin is always open
-runReader _ (&SWait   reader) = close reader
-
-runStdin : ()
-runStdin = fork (\(_ : ()) 1-> runServer @InStream @() runReader () dualStdin)
-
--- *** stdout
-
--- | Standard output stream. Prints to the console.
-stdoutChan : (OutStreamProvider, Dual OutStreamProvider)
-stdoutChan = channel @OutStreamProvider
-
-stdout : OutStreamProvider
-stdout = let (o,_) = stdoutChan in o
-
-dualStdout : Dual OutStreamProvider
-dualStdout = let (_,i) = stdoutChan in i
-
--- | Prints a character to `stdout`. Behaves the same as `hPutChar_ c stdout`, where `c`
--- | is the character to be printed.
-putChar : Char -> ()
-putChar = flip @Char @OutStreamProvider @() hPutChar_ stdout
-
--- | Prints a string to `stdout`. Behaves the same as `hPutStr_ s stdout`, where `s` is
--- | the string to be printed.
-putStr : String -> ()
-putStr = flip @String @OutStreamProvider @() hPutStr_ stdout
-
--- | Prints a string to `stdout`, followed by the newline character `\n`. Behaves
--- | as `hPutStrLn_ s stdout`, where `s` is the string to be printed.
-putStrLn : String -> ()
-putStrLn = flip @String @OutStreamProvider @() hPutStrLn_ stdout
-
--- | Prints the string representation of a given value to `stdout`, followed by
--- | the newline character `\n`. Behaves the same as `hPrint_ @t v stdout`, where `v` is
--- | the value to be printed and `t` its type.
-print : forall (a : *T) . a -> ()
-print @a x = putStrLn $ show @a x
-
--- **** Internal stdout functions
-
-internalPutStrOut : String -> ()
-internalPutStrOut = undefined @(String -> ())
-
-runPrinter : () -> Dual OutStream 1-> ()
-runPrinter _ (&PutChar printer) = 
-  readApply @Char   @(Dual OutStream) (\(c : Char) -> internalPutStrOut (show @Char c)) printer 
-    |> runPrinter ()
-runPrinter _ (&PutStr printer) = 
-  readApply @String @(Dual OutStream) internalPutStrOut printer 
-    |> runPrinter ()
-runPrinter _ (&PutStrLn printer) = 
-  readApply @String @(Dual OutStream) (\(s : String) -> internalPutStrOut ((++) @Char s "\n")) printer 
-    |> runPrinter ()
-runPrinter _ (&SWait printer) = 
-  close printer
-
-runStdout  : ()
-runStdout = fork (\(_ : ()) 1-> runServer @OutStream @() runPrinter () dualStdout)
\ No newline at end of file
+-- -- *** stdin
+
+-- -- | Standard input stream. Reads from the console.
+-- stdinChan : (InStreamProvider, Dual InStreamProvider)
+-- stdinChan = channel @InStreamProvider
+
+-- stdin : InStreamProvider
+-- stdin = let (i,_) = stdinChan in i
+
+-- dualStdin : Dual InStreamProvider
+-- dualStdin = let (_,o) = stdinChan in o
+
+-- -- | Reads a single character from `stdin`.
+-- -- getChar : () -> Char
+-- -- getChar _ = hGetChar_ stdin
+
+-- -- | Reads a single line from `stdin`. 
+-- -- getLine : () -> String
+-- -- getLine _ = hGetLine_ stdin
+
+-- -- **** Internal stdin functions
+
+-- -- internalGetChar : () -> Char
+-- -- internalGetChar = undefined @(() -> Char)
+-- -- internalGetLine : () -> String
+-- -- internalGetLine = undefined @(() -> String)
+-- -- internalGetContents : () -> String
+-- -- internalGetContents = undefined @(() -> String)
+
+-- -- runReader : () -> Dual InStream 1-> ()
+-- -- runReader _ (&GetChar reader) = runReader () $ send (internalGetChar ()) reader
+-- -- runReader _ (&GetLine reader) = runReader () $ send (internalGetLine ()) reader
+-- -- runReader _ (&IsEOF   reader) = runReader () $ send False reader -- stdin is always open
+-- -- runReader _ (&SWait   reader) = close reader
+
+-- -- runStdin : ()
+-- -- runStdin = fork (\(_ : ()) 1-> runServer @InStream @() runReader () dualStdin)
+
+-- -- *** stdout
+
+-- -- | Standard output stream. Prints to the console.
+-- stdoutChan : (OutStreamProvider, Dual OutStreamProvider)
+-- stdoutChan = channel @OutStreamProvider
+
+-- stdout : OutStreamProvider
+-- stdout = let (o,_) = stdoutChan in o
+
+-- dualStdout : Dual OutStreamProvider
+-- dualStdout = let (_,i) = stdoutChan in i
+
+-- -- | Prints a character to `stdout`. Behaves the same as `hPutChar_ c stdout`, where `c`
+-- -- | is the character to be printed.
+-- -- putChar : Char -> ()
+-- -- putChar = flip @Char @OutStreamProvider @() hPutChar_ stdout
+
+-- -- | Prints a string to `stdout`. Behaves the same as `hPutStr_ s stdout`, where `s` is
+-- -- | the string to be printed.
+-- -- putStr : String -> ()
+-- -- putStr = flip @String @OutStreamProvider @() hPutStr_ stdout
+
+-- -- | Prints a string to `stdout`, followed by the newline character `\n`. Behaves
+-- -- | as `hPutStrLn_ s stdout`, where `s` is the string to be printed.
+-- -- putStrLn : String -> ()
+-- -- putStrLn = flip @String @OutStreamProvider @() hPutStrLn_ stdout
+
+-- -- | Prints the string representation of a given value to `stdout`, followed by
+-- -- | the newline character `\n`. Behaves the same as `hPrint_ @t v stdout`, where `v` is
+-- -- | the value to be printed and `t` its type.
+-- -- print : forall (a : *T) . a -> ()
+-- -- print @a x = putStrLn $ show @a x
+
+-- -- **** Internal stdout functions
+
+-- -- internalPutStrOut : String -> ()
+-- -- internalPutStrOut = undefined @(String -> ())
+
+-- -- runPrinter : () -> Dual OutStream 1-> ()
+-- -- runPrinter _ (&PutChar printer) = 
+-- --   readApply @Char   @(Dual OutStream) (\(c : Char) -> internalPutStrOut (show @Char c)) printer 
+-- --     |> runPrinter ()
+-- -- runPrinter _ (&PutStr printer) = 
+-- --   readApply @String @(Dual OutStream) internalPutStrOut printer 
+-- --     |> runPrinter ()
+-- -- runPrinter _ (&PutStrLn printer) = 
+-- --   readApply @String @(Dual OutStream) (\(s : String) -> internalPutStrOut ((++) @Char s "\n")) printer 
+-- --     |> runPrinter ()
+-- -- runPrinter _ (&SWait printer) = 
+-- --   close printer
+
+-- -- runStdout  : ()
+-- -- runStdout = fork (\(_ : ()) 1-> runServer @OutStream @() runPrinter () dualStdout)
diff --git a/freest/src/FreeST.hs b/freest/src/FreeST.hs
index ee0456f1..61bc147e 100644
--- a/freest/src/FreeST.hs
+++ b/freest/src/FreeST.hs
@@ -21,6 +21,9 @@ import Validation.Base
 import Validation.Kinding
 import Validation.Typing
 
+import FstToLst.FstToLst ( fstToLst, removeBuiltins )
+import LeaST.Interpreter ( interpret, Value(VIO) )
+import qualified LeaST.PrettyPrint as LPP
 
 import Control.Monad.State ( runState )
 import Data.Function ( (&) )
@@ -36,25 +39,45 @@ main = do
 
 -- | The FreeST compiler pipeline.
 freest :: RunOpts -> IO ()
-freest RunOpts{file=programPath} = do
-  -- Read the source code of the Prelude.
-  preludeSrc <- getDataFileName preludePath >>= readFile
-  -- Read the source code of the program.
-  programSrc <- readFile programPath
-  -- Parse the source code of both the Prelude and the program, and
-  -- include the former in the latter, resulting in a single module.
-  mappend <$> runParseModule preludePath preludeSrc
-          <*> runParseModule programPath programSrc
-    -- Scope the module.
-    >>= runScopeModule & \case 
-      Left es -> putStrLn "[Scoping failed]" >> mapM_ print es >> exitFailure
-      Right m -> do 
-        -- putStrLn ("[Scoping passed]\n"++unlines (map ("> "++) (lines $ show m)))
-        -- Validate the module.
-        runValidate m & \case 
-          Left es -> putStrLn "[Validation failed]" >> mapM_ print es >> exitFailure     
-          Right m -> {- putStrLn "[Validation passed]" >> -} exitSuccess
+freest RunOpts{file=programPath, least=l} = do
+  source <- readFile programPath
+  if l then case runLexer parseLeaST programPath source of
+    Right (_,_,_,leastAST) -> do
+      LPP.prettyPrint leastAST
+      res <- interpret leastAST
+      case res of
+        VIO io -> do _ <- io
+                     return ()
+        _ -> return ()
+    Left err -> print err
+  else do
+    -- Read the source code of the Prelude.
+    preludeSrc <- getDataFileName preludePath >>= readFile
+    -- Read the source code of the program.
+    programSrc <- readFile programPath
+    -- Parse the source code of both the Prelude and the program, and
+    -- include the former in the latter, resulting in a single module.
+    mappend <$> runParseModule preludePath preludeSrc
+            <*> runParseModule programPath programSrc
+      -- Scope the module.
+      >>= runScopeModule & \case 
+        Left es -> putStrLn "[Scoping failed]" >> mapM_ print es >> exitFailure
+        Right m -> do 
+          -- putStrLn ("[Scoping passed]\n"++unlines (map ("> "++) (lines $ show m)))
+          -- Validate the module.
+          runValidate m & \case 
+            Left es -> putStrLn "[Validation failed]" >> mapM_ print es >> exitFailure     
+            Right m -> do
+              {- putStrLn "[Validation passed]" >> -}
+                let leastAST = fstToLst [removeBuiltins m]
+                print leastAST
+                LPP.prettyPrint leastAST
+                res <- interpret leastAST
+                case res of
+                  VIO io -> do _ <- io
+                               return ()
+                  _ -> return ()
 
 -- | The path to the source code of the Prelude.
 preludePath :: FilePath
-preludePath = "StandardLib/Prelude.fst"
\ No newline at end of file
+preludePath = "StandardLib/Prelude.fst"
diff --git a/freest/src/FstToLst/FstToLst.hs b/freest/src/FstToLst/FstToLst.hs
new file mode 100644
index 00000000..9715ff4a
--- /dev/null
+++ b/freest/src/FstToLst/FstToLst.hs
@@ -0,0 +1,377 @@
+module FstToLst.FstToLst where
+
+import qualified Syntax.Module as M
+import qualified LeaST.LeaST as L
+import LeaST.Interpreter ( builtins )
+import qualified Syntax.Expression as E
+import qualified Syntax.Base as B
+import qualified Syntax.Type as T
+
+import Data.List ( find )
+import Data.Maybe ( maybe )
+import Debug.Trace
+
+fstToLst :: [M.Module] -> L.Exp
+fstToLst modules = traceShow modules $ translateTopLevelLetDecls (concatMap M.definitions modules) 
+
+translateTopLevelLetDecls :: [E.LetDecl] -> L.Exp
+translateTopLevelLetDecls letDecls = fst $ translateLetDecls 0 letDecls [] generateUnit
+
+translateLetDecls :: Int -> [E.LetDecl] -> [(B.Variable, T.Type)] -> L.Exp -> (L.Exp, Int)
+translateLetDecls counter [] _ cont = (cont, counter)
+translateLetDecls counter ((E.ValDef pat@(E.VarPat _ var) rhs):letDecls) typeSigs cont =
+  let (rhsExp, counter1) = translateRHS counter rhs
+      (translateLetDeclsRes, counter2) = translateLetDecls counter1 letDecls typeSigs cont in
+  (L.App (translatePat (pat, getTypeFromTypeSigs typeSigs var) translateLetDeclsRes) (L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") rhsExp) generateError), counter2)
+translateLetDecls counter ((E.ValDef pat rhs):letDecls) typeSigs cont =
+  let (translateLetDeclsRes, counter1) = translateLetDecls counter letDecls typeSigs cont
+      (counter2, var) = nextFreshVar counter1
+      (compileEquationsRes, counter3) = compileEquations counter2 [var] [([removeAsPat pat], foldr (\(var, exp) acc -> L.App (L.Abs var (T.Int B.nullSpan) acc) exp) translateLetDeclsRes (getAsPatBindings pat))] generateError
+      (translateRhsRes, counter4) = translateRHS counter3 rhs in
+  (L.App (L.Abs var (T.Int B.nullSpan) (L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") compileEquationsRes) generateError)) translateRhsRes, counter3)
+translateLetDecls counter ((E.FnDef var patRhss):letDecls) typeSigs cont =
+  let (translateLetDeclsRes, counter1) = translateLetDecls counter letDecls typeSigs cont
+      (eqs, counter2) = bar counter1 patRhss
+      argsNum = length $ (fst . head) eqs
+      (counter3, vars) = nextFreshVars counter2 argsNum
+      (compileEquationsRes, _) = compileEquations counter3 vars (handleAsPatInEqs eqs) generateError
+      (generateArgsRes, counter5) = generateArgs counter2 argsNum (L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") compileEquationsRes) generateError) in
+  (L.App (L.Abs var (T.Int B.nullSpan) translateLetDeclsRes) (L.App generateFixPoint (L.Abs var (T.Int B.nullSpan) generateArgsRes)), counter5)
+-- TODO: remover ctx das assinaturas
+translateLetDecls counter ((E.Mutual mutualLetDecls):letDecls) typeSigs cont = undefined
+translateLetDecls counter ((E.TypeSig vars ty):letDecls) typeSigs cont = translateLetDecls counter letDecls [] cont
+
+-- TODO: generate TAbs, for now TAbs is an Abs with a varPat
+generateArgs :: Int -> Int -> L.Exp -> (L.Exp, Int)
+generateArgs n 0 cont = (cont, n)
+generateArgs n size cont =
+  let (counter, var) = nextFreshVar n
+      (generateArgsRes, counter1) = generateArgs counter (size-1) cont in
+  (L.Abs var (T.Int B.nullSpan) generateArgsRes, counter1)
+
+-- Removes AsPats transforming the expression in the equation
+handleAsPatInEqs :: [Equation] -> [Equation]
+handleAsPatInEqs = map (\(pats, exp) ->
+  let newPats = map removeAsPat pats
+      patsBindings = concatMap getAsPatBindings pats in
+  (newPats, foldr (\(var, bindingExp) acc -> L.App (L.Abs var (T.Int B.nullSpan) acc) bindingExp) exp patsBindings))
+
+removeAsPat :: E.Pat -> E.Pat
+removeAsPat (E.DConsPat span iden pats) = E.DConsPat span iden (map removeAsPat pats) 
+removeAsPat (E.ChoicePat span iden pat) = (E.ChoicePat span iden (removeAsPat pat))
+removeAsPat (E.AsPat _ _ pat) = removeAsPat pat
+removeAsPat pat = pat
+
+getAsPatBindings :: E.Pat -> [(B.Variable, L.Exp)]
+getAsPatBindings (E.DConsPat _ __ pats) = concat $ map getAsPatBindings pats
+getAsPatBindings (E.ChoicePat _ _ pat) = getAsPatBindings pat
+getAsPatBindings (E.AsPat _ var pat) = (var, patToLExp pat) : (getAsPatBindings pat)
+getAsPatBindings _ = []
+
+translateRHS :: Int -> E.RHS -> (L.Exp, Int)
+translateRHS counter (E.UnguardedRHS exp (Just letDecls)) =
+  let (cont, counter1) = translateExp counter exp in translateLetDecls counter letDecls [] cont
+translateRHS counter (E.UnguardedRHS exp Nothing) = translateExp counter exp
+translateRHS counter (E.GuardedRHS guards (Just letDecls)) =
+  let (cont, counter1) =
+        foldr (\(cond, exp) (accExp, accCounter) ->
+        let (cond1, counter1) = translateExp accCounter cond
+            (exp1, counter2) = translateExp counter1 exp
+        in (generateLeastIf cond1 exp1 accExp, counter2)) (generateFail, counter) guards
+  in translateLetDecls counter1 letDecls [] cont
+translateRHS counter (E.GuardedRHS guards Nothing) = foldr (\(cond, exp) (accExp, accCounter) ->
+  let (cond1, counter1) = translateExp accCounter cond
+      (exp1, counter2) = translateExp counter1 exp
+  in (generateLeastIf cond1 exp1 accExp, counter2)) (generateFail, counter) guards
+
+translateExp :: Int -> E.Exp -> (L.Exp, Int)
+translateExp counter (E.Int _ int) = (L.Lit (L.LInt int), counter)
+translateExp counter (E.Float _ float) = (L.Lit (L.LFloat float), counter)
+translateExp counter (E.Char _ char) = (L.Lit (L.LChar char), counter)
+translateExp counter (E.DCons _ iden) = (L.Con iden, counter)
+translateExp counter (E.Var _ var) = (L.Var var, counter)
+translateExp counter (E.App _ exp args) =
+  foldl (\(accExp, accCounter) arg -> case arg of
+    B.ExpLevel exp -> let (exp3, counter) = translateExp accCounter exp in (L.App accExp exp3, counter)
+    B.TypeLevel ty -> (L.TApp accExp (L.Type ty), accCounter)) (translateExp counter exp) args
+translateExp counter (E.Abs _ levels _ exp) = foldr (\abs (accExp, accCounter) -> case abs of
+  B.ExpLevel (pat, ty) ->
+    let (counter1, var) = nextFreshVar accCounter
+        (compileEquationsRes, counter2) = compileEquations counter1 [var] [([removeAsPat pat], foldr (\(var, exp) acc -> L.App (L.Abs var (T.Int B.nullSpan) acc) exp) accExp (getAsPatBindings pat))] generateError in
+    ((L.Abs var (T.Int B.nullSpan) compileEquationsRes), counter2)
+-- TODO: give the correct type
+  B.TypeLevel (var, kind) -> (translatePat (E.VarPat B.nullSpan var, T.Int B.nullSpan) accExp,  accCounter)) (translateExp counter exp) levels
+translateExp counter (E.Let _ letDecls exp) =
+  let (exp2, counter1) = translateExp counter exp in translateLetDecls counter1 letDecls [] exp2
+translateExp counter (E.If _ cond t f) =
+  let (condExp, counter1) = translateExp counter cond
+      (tExp, counter2) = translateExp counter1 t
+      (fExp, counter3) = translateExp counter2 f in
+  (generateLeastIf condExp tExp fExp, counter3)
+translateExp counter (E.Case _ exp patRhss) =
+  let (caseExp, counter1) = translateExp counter exp
+      (counter2, var) = nextFreshVar counter1
+      (rhss, counter3) = mapWithCounter counter2 (\counter (pat, rhs) -> let (rhsExp, counter1) = translateRHS counter rhs in (([removeAsPat pat], foldr (\(var, exp) acc -> L.App (L.Abs var (T.Int B.nullSpan) acc) exp) rhsExp (getAsPatBindings pat)), counter1)) patRhss
+      (compiledEquationsExp, counter4) = compileEquations counter3 [var] rhss generateError in
+  (L.App (L.Abs var (T.Int B.nullSpan) compiledEquationsExp) caseExp, counter4)
+translateExp counter (E.Channel _ _) = (L.App (L.Var $ generatePrimitiveVar "chan") generateUnit, counter)
+translateExp counter (E.Select _ (B.Identifier _ iden)) =
+  ((L.TApp (L.TApp (L.TApp (L.Var $ generatePrimitiveVar "send") generateUnit) generateUnit) (lstString iden)) , counter)
+
+mapWithCounter :: Int -> (Int -> a -> (b, Int)) -> [a] -> ([b], Int)
+mapWithCounter n _ [] = ([], n)
+mapWithCounter n f (x:xs) =
+  let (xs', counter1) = mapWithCounter n f xs
+      (x', counter2) = f counter1 x in
+  (x':xs', counter2)
+
+generateLeastIf :: L.Exp -> L.Exp -> L.Exp -> L.Exp
+-- generateLeastIf cond t f = L.Case cond [(L.ACon (B.Identifier B.nullSpan "True") [], t), (L.ACon (B.Identifier B.nullSpan "False") [], f)]
+generateLeastIf cond t f = L.App (L.App (L.App (L.Var $ generatePrimitiveVar "if__") cond) t) f
+
+generatePrimitiveVar :: String -> B.Variable
+generatePrimitiveVar name = B.Variable {B.internal=(-1), B.external=name, B.varSpan=B.Span{B.filepath="", B.startPos=(0,0), B.endPos=(0,0)}}
+
+generateFail :: L.Exp
+generateFail = L.Con (B.Identifier B.nullSpan "Fail__")
+
+generateUnit :: L.Exp
+generateUnit = L.Con (B.Identifier B.nullSpan "()")
+
+lstString :: String -> L.Exp
+lstString = foldr (\char acc ->
+  L.App (L.App (L.Con $ B.Identifier B.nullSpan "::") (L.Lit $ L.LChar char)) acc) (L.TApp (L.Con $ B.Identifier B.nullSpan "[]") (L.Type $ T.Char B.nullSpan))
+
+-- TODO: am i using this?
+-- Transforms a pattern in the "equivalent" least expression
+-- used for compiling Choice patterns and as-patterns
+patToLExp :: E.Pat -> L.Exp
+patToLExp (E.IntPat _ n) = L.Lit $ L.LInt n
+patToLExp (E.FloatPat _ n) = L.Lit $ L.LFloat n
+patToLExp (E.CharPat _ c) = L.Lit $ L.LChar c
+patToLExp (E.WildPat _ _) = L.Var $ generatePrimitiveVar "wild__"
+patToLExp (E.VarPat _ var) = L.Var var
+patToLExp (E.DConsPat _ iden pats) = foldl (\acc pat -> L.App acc (patToLExp pat)) (L.Con iden) pats
+patToLExp (E.ChoicePat _ iden (E.VarPat _ var)) = L.Var var
+-- TODO: can treat asPat as varPat??
+patToLExp (E.AsPat _ _ pat) = patToLExp pat
+
+-- TODO: necessario um variavel fresca para o wildpat??
+translatePat :: (E.Pat, T.Type) -> L.Exp -> L.Exp
+translatePat ((E.VarPat _ var), ty) cont = L.Abs var ty cont  
+translatePat ((E.WildPat _ var), ty) cont = L.Abs var ty cont  
+
+getTypeFromTypeSigs :: [(B.Variable, T.Type)] -> B.Variable -> T.Type
+getTypeFromTypeSigs typeSigs var = case find ((var ==) . fst) typeSigs of
+  Just (_, ty) -> ty
+  Nothing -> T.Int B.nullSpan
+
+generateFixPoint :: L.Exp
+generateFixPoint = L.Abs (generatePrimitiveVar "f__") (T.Int B.nullSpan) (
+  L.App 
+  (L.Abs (generatePrimitiveVar "x__") (T.Int B.nullSpan) (
+    L.App (L.Var $ generatePrimitiveVar "f__") 
+      (L.Abs (generatePrimitiveVar "v__") (T.Int B.nullSpan)
+        (L.App 
+          (L.App 
+            (L.Var $ generatePrimitiveVar "x__")
+            (L.Var $ generatePrimitiveVar "x__"))
+          (L.Var $ generatePrimitiveVar "v__")))))
+  (L.Abs (generatePrimitiveVar "x__") (T.Int B.nullSpan) (
+    L.App (L.Var $ generatePrimitiveVar "f__") 
+      (L.Abs (generatePrimitiveVar "v__") (T.Int B.nullSpan)
+        (L.App 
+          (L.App 
+            (L.Var $ generatePrimitiveVar "x__")
+            (L.Var $ generatePrimitiveVar "x__"))
+          (L.Var $ generatePrimitiveVar "v__"))))))
+
+nextFreshVar :: Int -> (Int, B.Variable)
+nextFreshVar n = (n+1, generatePrimitiveVar $ "var"++show n++"__")
+
+nextFreshVars :: Int -> Int -> (Int, [B.Variable])
+nextFreshVars n size = (n+size, [generatePrimitiveVar $ "var"++show n++"__" | n <- [n..n+size-1]])
+
+type Equation = ([E.Pat], L.Exp)
+
+compileEquations :: Int -> [B.Variable] -> [Equation] -> L.Exp -> (L.Exp, Int)
+-- TODO: empty rule is not correct, maybe?
+-- compileEquations _ [] eqs def = let (hd:tl) = [e |(_,e) <- eqs] in 
+--   L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") (foldl (\acc exp -> L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") acc) exp) hd tl)) def
+compileEquations counter [] [] def = (def, counter)
+compileEquations counter [] [(_, exp)] _ = (exp, counter)
+compileEquations counter [] eqs _ = (foldr (\(_, exp) acc-> L.App (L.App (L.Var $ generatePrimitiveVar "fatbar__") exp) acc) (snd . last $ eqs) (init eqs), counter)
+compileEquations counter vars eqs def | allVars eqs =
+                                        compileEquations counter (tail vars) (updateHeadPattern (replaceVar (head vars) eqs)) def
+                                      | allCons eqs && firstEqIsChoicePat eqs =
+                                        let (counter1, freshVars) = nextFreshVars counter 2
+                                            (fooRes, counter2) = foo counter1 (tail freshVars ++ tail vars ) (groupEqs eqs) def
+                                        in (L.Case (generateReceive generateUnit generateUnit (L.Var $ head vars)) [(L.ACon (B.Identifier B.nullSpan "(,)") freshVars, (L.Case (L.Var (head freshVars)) fooRes))], counter2)
+                                      | allCons eqs = let (fooRes, counter1) = foo counter (tail vars) (groupEqs eqs) def in (L.Case (L.Var (head vars)) fooRes, counter1)
+                                      | otherwise = foldr (\groupedEqs (accExp, accCounter) -> compileEquations accCounter vars groupedEqs accExp) (def, counter) (reverse $ mixtureGroup eqs)
+
+allVars :: [Equation] -> Bool
+allVars [] = True 
+allVars (eq:eqs) = case (head . fst) eq of
+  E.VarPat _ _ -> allVars eqs
+  E.WildPat _ _ -> allVars eqs
+  _ -> False
+
+allCons :: [Equation] -> Bool
+allCons [] = True
+allCons (eq:eqs) = case (head . fst) eq of
+  E.DConsPat _ _ _ -> allCons eqs
+  E.IntPat _ _ -> allCons eqs
+  E.FloatPat _ _ -> allCons eqs
+  E.CharPat _ _ -> allCons eqs
+  E.ChoicePat _ _ _ -> allCons eqs
+  _ -> False
+
+firstEqIsChoicePat :: [Equation] -> Bool
+firstEqIsChoicePat ((((E.ChoicePat _ _ _):_), _):_) = True
+firstEqIsChoicePat _ = False
+
+generateReceive :: L.Exp -> L.Exp -> L.Exp -> L.Exp
+generateReceive arg1 arg2 arg3 = L.App (L.TApp (L.TApp (L.Var $ generatePrimitiveVar "receive") arg1) arg2) arg3
+
+replaceVar :: B.Variable -> [Equation] -> [Equation]
+replaceVar var eqs = map (\(pats, exp) -> case pats of
+  ((E.VarPat _ patVar):_) -> (pats, subs patVar var exp)
+  ((E.WildPat _ _):_) -> (pats, exp)
+  _ -> traceShow pats undefined) eqs
+
+subs :: B.Variable -> B.Variable -> L.Exp -> L.Exp
+subs target var exp@(L.Var v) = if v == target then (L.Var var) else exp
+subs target var exp@(L.Abs v ty e) = if v == target then exp else (L.Abs v ty (subs target var e))
+subs target var (L.App e1 e2) = L.App (subs target var e1) (subs target var e2)
+subs target var (L.Case e alts) = L.Case (subs target var e) (altsSubs target var alts)
+subs target var exp = exp
+
+altsSubs :: B.Variable -> B.Variable -> [(L.Alt, L.Exp)] -> [(L.Alt, L.Exp)]
+altsSubs target var alts = map (altSub target var) alts
+
+altSub :: B.Variable -> B.Variable -> (L.Alt, L.Exp) -> (L.Alt, L.Exp)
+altSub target var (L.ACon iden vars, exp) =
+  if elem target vars then
+    (L.ACon iden vars, exp)
+  else
+    (L.ACon iden vars, subs target var exp)
+altSub target var (pat, exp) = (pat, subs target var exp)
+
+-- TODO Verificar que a ordem nao muda
+-- Only called if all are constructor
+groupEqs :: [Equation] -> [[Equation]]
+groupEqs [] = [[]]
+groupEqs (eq:eqs) = addEq eq (groupEqs eqs)
+
+-- Ewwwwww
+addEq :: Equation -> [[Equation]] -> [[Equation]]
+addEq eq [] = [[eq]]
+addEq eq [[]] = [[eq]]
+addEq eq@((patX:_),_) (eqs@(((patY:_), _):_):eqss) = if patIsEq patX patY then (eq:eqs):eqss else (eqs: addEq eq eqss)
+
+mixtureGroup :: [Equation] -> [[Equation]]
+mixtureGroup [] = [[]]
+mixtureGroup (eq:eqs) = addEqMix eq (mixtureGroup eqs)
+
+addEqMix :: Equation -> [[Equation]] -> [[Equation]]
+addEqMix eq [] = [[eq]]
+addEqMix eq [[]] = [[eq]]
+addEqMix eq@((patX:_),_) (eqs@(((patY:_), _):_):eqss) = if patIsEqMix patX patY then (eq:eqs): eqss else (eqs: (addEqMix eq eqss))
+
+patIsEq :: E.Pat -> E.Pat -> Bool
+patIsEq (E.IntPat _ x) (E.IntPat _ y) = x == y
+patIsEq (E.FloatPat _ x) (E.FloatPat _ y) = x == y
+patIsEq (E.CharPat _ x) (E.CharPat _ y) = x == y
+patIsEq (E.WildPat _ x) (E.WildPat _ y) = undefined
+patIsEq (E.VarPat _ x) (E.VarPat _ y) = undefined
+patIsEq (E.DConsPat _ (B.Identifier _ x) _) (E.DConsPat _ (B.Identifier _ y) _) = x == y
+patIsEq (E.AsPat _ x xPat) (E.AsPat _ y yPat) = undefined
+patIsEq _ _ = False
+
+patIsEqMix :: E.Pat -> E.Pat -> Bool
+patIsEqMix (E.VarPat _ _) (E.VarPat _ _) = True
+patIsEqMix (E.IntPat _ _) (E.IntPat _ _) = True 
+patIsEqMix (E.FloatPat _ _) (E.FloatPat _ _) = True 
+patIsEqMix (E.CharPat _ _) (E.CharPat _ _) = True 
+patIsEqMix (E.WildPat _ _) (E.WildPat _ _) = undefined
+patIsEqMix (E.DConsPat _ _ _) (E.DConsPat _ _ _) = undefined
+patIsEqMix _ _ = False
+
+-- TODO: relembrar o que isto faz e dar um nome adequado
+foo :: Int -> [B.Variable] -> [[Equation]] -> L.Exp -> ([(L.Alt, L.Exp)], Int)
+-- def makes sense here?
+foo counter vars [] def = ([(L.AWildCard, def)], counter)
+-- foo counter vars (eqs:eqss) def =
+--   let E.DConsPat _ iden pats = (head . fst . head) eqs
+--       freshVars = (newKVars counter (length pats))
+--   in (L.ACon iden freshVars, compileEquations (counter+length freshVars) (freshVars++vars) (updateHeadPattern eqs) def):(foo counter vars eqss def)
+foo counter vars (eqs:eqss) def = 
+  case (head . fst . head) eqs of
+    E.DConsPat _ iden pats ->
+      let (counter1, nextVars) = nextFreshVars counter (length pats)
+          (compileEquationsRes, counter2) = compileEquations counter1 (nextVars++vars) (updateHeadPattern eqs) def 
+          (fooRes, counter3) = foo counter2 vars eqss def in
+      ((L.ACon iden nextVars, compileEquationsRes):fooRes, counter3)
+    E.IntPat _ n ->
+      let (compileEquationsRes, counter1) = compileEquations counter vars (updateHeadPattern eqs) def
+          (fooRes, counter2) = foo counter1 vars eqss def in
+      ((L.ALit $ L.LInt n, compileEquationsRes):fooRes, counter2)
+    E.FloatPat _ n ->
+      let (compileEquationsRes, counter1) = compileEquations counter vars (updateHeadPattern eqs) def
+          (fooRes, counter2) = foo counter1 vars eqss def in
+      ((L.ALit $ L.LFloat n, compileEquationsRes):fooRes, counter2)
+    E.CharPat _ n ->
+      let (compileEquationsRes, counter1) = compileEquations counter vars (updateHeadPattern eqs) def
+          (fooRes, counter2) = foo counter1 vars eqss def in
+      ((L.ALit $ L.LChar n, compileEquationsRes):fooRes, counter2)
+    E.ChoicePat _ label (E.VarPat _ var) ->
+      let (compileEquationsRes, counter1) = compileEquations counter vars (updateHeadPattern eqs) def 
+          (fooRes, counter2) = foo counter1 vars eqss def in
+      ((L.ACon label [], compileEquationsRes):fooRes, counter2)
+    E.ChoicePat _ label (E.WildPat _ var) ->
+      let (compileEquationsRes, counter1) = compileEquations counter vars (updateHeadPattern eqs) def 
+          (fooRes, counter2) = foo counter1 vars eqss def in
+      ((L.ACon label [], compileEquationsRes):fooRes, counter2)
+    E.ChoicePat _ _ _ -> undefined
+
+-- TODO: remove this function
+newKVars :: Int -> Int -> [B.Variable]
+newKVars from size = [generatePrimitiveVar ("arg"++(show n)++"__") | n <- [from..from+size]]
+
+updateHeadPattern :: [Equation] -> [Equation]
+updateHeadPattern eqs = map (\(pats, exp) -> (updateHeadPattern' pats, exp)) eqs
+
+updateHeadPattern' :: [E.Pat] -> [E.Pat]
+updateHeadPattern' ((E.DConsPat _ _ []):pats) = pats 
+updateHeadPattern' ((E.DConsPat _ _ innerPats):pats) = innerPats++pats 
+updateHeadPattern' ((E.ChoicePat _ _ varPat@(E.VarPat _ _)):pats) = varPat:pats 
+updateHeadPattern' ((E.ChoicePat _ _ varPat@(E.WildPat _ _)):pats) = varPat:pats 
+updateHeadPattern' ((E.ChoicePat _ _ pat):pats) = undefined 
+updateHeadPattern' (pat:pats) = pats
+
+-- TODO: rename this for function for something better
+bar :: Int -> [([B.Level E.Pat B.Variable], E.RHS)] -> ([([E.Pat], L.Exp)], Int)
+bar counter patRHS =
+  mapWithCounter counter (\counter (levels, rhs) ->
+    let (translateRHSRes, counter1) = translateRHS counter rhs in
+    (((map (\level -> case level of
+      B.ExpLevel pat -> pat
+      B.TypeLevel var -> E.VarPat B.nullSpan var) levels), translateRHSRes), counter1)) patRHS
+
+generateError :: L.Exp
+generateError = L.Var $ generatePrimitiveVar "error__"
+
+removeBuiltins :: M.Module -> M.Module
+removeBuiltins m = m{M.definitions = filter notBuiltin (M.definitions m)}
+  where notBuiltin = \case
+          (E.ValDef (E.VarPat _ x) _) ->
+            case lookup (B.external x) builtins of
+              Nothing -> True
+              Just _  -> False
+          (E.FnDef x _) ->
+            case lookup (B.external x) builtins of
+              Nothing -> True
+              Just _  -> False
+          _ -> True
+  
diff --git a/freest/src/LeaST/Interpreter.hs b/freest/src/LeaST/Interpreter.hs
new file mode 100644
index 00000000..5ac2399b
--- /dev/null
+++ b/freest/src/LeaST/Interpreter.hs
@@ -0,0 +1,297 @@
+module LeaST.Interpreter where
+
+import LeaST.LeaST qualified as L
+import Syntax.Base qualified as B
+import Utils (internalError)
+
+import Control.Concurrent ( forkIO )
+import Control.Concurrent.Chan qualified as Chan
+import Data.Functor ( ($>), (<&>), void )
+import Data.Char (chr, ord)
+import Data.List ( find )
+import Data.Map qualified as Map
+import GHC.Float ( Floating(log1mexp, expm1, log1p, log1pexp) )
+import System.IO ( Handle, putStr, hPutStr, getChar, getLine, getContents, stderr, openFile, IOMode(..), hGetChar, hGetLine, hIsEOF, hClose )
+
+import Debug.Trace
+
+interpret :: L.Exp -> IO Value
+interpret = eval builtins
+
+-- TODO: Fatbar implementation will not work because language is strict
+
+type ChannelEnd = (Chan.Chan Value, Chan.Chan Value)
+
+data Value = VInt Int
+  | VFloat Double
+  | VChar Char
+  | VCon String [Value]
+  | VClosure Context B.Variable L.Exp
+  | VBuiltin (Value -> Value)
+  | VIO (IO Value)
+  | VChan ChannelEnd
+  | VFork
+  | VIf [(L.Exp, Context)]
+  | VFatbar [(L.Exp,Context)]
+
+instance Show Value where
+  show = \case 
+    (VInt   x)  -> show x
+    (VFloat x)  -> show x
+    (VChar  x)  -> show x
+    (VCon c vs) -> c ++ if null vs then "" else " " ++ "(" ++ unwords (map show vs)++")"
+    VClosure{}  -> "<closure>"
+    VBuiltin{}  -> "<builtin>"
+    VIO{}       -> "<vio>"
+    VChan{}     -> "<channel end>"
+    VFork       -> "<vfork>"
+
+eval :: Context -> L.Exp -> IO Value
+eval ctx = \case 
+  L.Var x -> case B.external x of
+    "fork"      -> return VFork
+    "undefined" -> error ("undefined, called at "++show (B.getSpan x))
+    -- TODO: substitute all error__ for error
+    "error__"   -> error "Error"
+    "error" -> error "Error"
+    "fatbar__"  -> return $ VFatbar []
+    "if__" -> return $ VIf []
+    _ -> return $ getVar ctx (B.external x)
+  L.Lit l -> return case l of 
+    L.LInt   x -> VInt   x
+    L.LFloat x -> VFloat x
+    L.LChar  x -> VChar  x
+  L.Abs x _ e -> return $ VClosure ctx x e
+  L.App e1 e2 -> do
+    v1 <- eval ctx e1
+    case v1 of
+      VFork -> forkIO (void $ eval ctx (unpackAbs e2)) $> VCon "()" []
+      VIf args -> if length args == 2
+        then do
+          let (condExp, condCtx) = head args
+          let (tExp, tCtx) = args!!1
+          condVal <- eval condCtx condExp 
+          if lstToHsBool condVal then eval tCtx tExp else eval ctx e2
+        else return $ VIf (args++[(e2, ctx)])
+      VFatbar args -> if length args == 1
+        then do
+          let (leftExp, leftCtx) = head args
+          leftVal <- eval leftCtx leftExp
+          case leftVal of
+            VCon "Fail__" [] -> eval ctx e2
+            _ -> return leftVal
+        else return $ VFatbar (args++[(e2, ctx)])
+      _ -> do 
+        v2 <- eval ctx e2
+        case v1 of
+          VCon i vs         -> return $ VCon i (vs ++ [v2])
+          VClosure ctx' x e -> eval ((B.external x, v2) : ctx') e
+          VBuiltin f        -> case f v2 of VIO iov -> iov
+                                            v       -> return v
+          VIO iov -> iov
+  L.Con i -> return $ VCon (show i) []
+  L.Case e as -> do
+    v <- eval ctx e
+    -- uncurry eval $ patternMatch ctx v as
+    baz ctx v as
+  L.TAbs x _ e -> return $ VClosure ctx x e
+  L.TApp e1 e2 -> do
+    v1 <- eval ctx e1
+    v2 <- eval ctx e2
+    -- TODO: make sure all cases are handled (lists causes troble here)
+    case v1 of
+      VClosure cctx _ cExp -> eval cctx cExp
+      VBuiltin b -> return $ b v2 
+      con@(VCon _ _) -> return con
+      _ -> undefined
+  L.Type _ -> return $ VCon "()" []
+
+-- patternMatch :: Context -> Value -> [(L.Alt, L.Exp)] -> (Context, L.Exp)
+-- patternMatch _ _ [] = error "Pattern matching was not exhaustive"
+-- patternMatch ctx val@(VInt int2) ((L.ALit (L.LInt int), exp) : alts) = if int2 == int then (ctx, exp) else patternMatch ctx val alts
+-- patternMatch ctx val@(VFloat float2) ((L.ALit (L.LFloat float), exp) : alts) = if float2 == float then (ctx, exp) else patternMatch ctx val alts
+-- patternMatch ctx val@(VChar char2) ((L.ALit (L.LChar char), exp) : alts) = if char2 == char then (ctx, exp) else patternMatch ctx val alts
+-- patternMatch ctx _ ((L.AWildCard, exp) : _) = (ctx, exp)
+-- patternMatch ctx val@(VCon iden2 conArgs) ((L.ACon iden vars, exp) : alts) = if iden2 == show iden then (zip (map B.external vars) conArgs ++ ctx, exp) else patternMatch ctx val alts
+
+patternMatch :: Context -> Value -> (L.Alt, L.Exp) -> Maybe (Context, L.Exp)
+patternMatch ctx val@(VInt int2) (L.ALit (L.LInt int), exp) = if int2 == int then Just (ctx, exp) else Nothing
+patternMatch ctx val@(VFloat int2) (L.ALit (L.LFloat int), exp) = if int2 == int then Just (ctx, exp) else Nothing
+patternMatch ctx val@(VChar int2) (L.ALit (L.LChar int), exp) = if int2 == int then Just (ctx, exp) else Nothing
+patternMatch ctx _ (L.AWildCard, exp) = Just (ctx, exp)
+patternMatch ctx val@(VCon iden2 conArgs) (L.ACon iden vars, exp) = if iden2 == show iden then Just (zip (map B.external vars) conArgs ++ ctx, exp) else Nothing
+
+-- TODO: better name
+baz :: Context -> Value -> [(L.Alt, L.Exp)] -> IO Value
+baz _ _ [] = undefined
+baz ctx val (alt:alts) = case patternMatch ctx val alt of
+    Just (ctx, exp) -> do
+      altVal <- eval ctx exp
+      case altVal of
+        VCon "Fail__" [] -> baz ctx val alts
+        _ -> return altVal
+    Nothing -> baz ctx val alts
+  
+
+
+unpackAbs :: L.Exp -> L.Exp
+unpackAbs (L.Abs _ _ exp) = exp
+unpackAbs exp = traceShow exp undefined
+
+type Context = [(String, Value)]
+
+getVar :: Context -> String -> Value
+getVar ctx x = case lookup x ctx of
+  Just v  -> v
+  Nothing -> internalError ("variable `" ++ x ++ "` not in scope.")
+
+builtins :: Context
+builtins = [
+  ("chan", VIO $ do (chanL, chanR) <- chan
+                    return $ VCon "(,)" [VChan chanL, VChan chanR]),
+  ("receive", VBuiltin (\_ty1 -> VBuiltin (\_ty2 -> VBuiltin (\(VChan c) -> VIO $ receive c >>= \(val, c) -> return $ VCon "(,)" [val, VChan c])))),
+  ("send", VBuiltin (\_ty1 -> VBuiltin (\_ty2 -> VBuiltin (\val -> VBuiltin (\(VChan c) -> VIO $ VChan <$> send val c))))),
+  ("wait", VBuiltin wait),
+  ("close", VBuiltin (VIO . close)),
+
+  ("(+)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (x + y)))),
+  ("(-)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (x - y)))),
+  ("subtract", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (x - y)))),
+  ("(*)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (x * y)))),
+  ("(/)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (div x y)))),
+  ("(^)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (x ^ y)))),
+  ("abs", VBuiltin (\(VInt x) -> VInt (abs x))),
+  ("mod", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (mod x y)))),
+  ("rem", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (rem x y)))),
+  ("negate", VBuiltin (\(VInt x) -> VInt (-x))),
+  ("max", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (max x y)))),
+  ("min", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (min x y)))),
+  ("succ", VBuiltin (\(VInt x) -> VInt (succ x))),
+  ("pred", VBuiltin (\(VInt x) -> VInt (pred x))),
+  ("quot", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (quot x y)))),
+  ("div", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (div x y)))),
+  ("even", VBuiltin (\(VInt x) -> hsToLstBool (even x))),
+  ("odd", VBuiltin (\(VInt x) -> hsToLstBool (odd x))),
+  ("gcd", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (gcd x y)))),
+  ("lcm", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> VInt (lcm x y)))),
+
+  ("(+.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (x + y)))),
+  ("(-.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (x - y)))),
+  ("(*.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (x * y)))),
+  ("(/.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (x / y)))),
+  ("negateF", VBuiltin (\(VFloat x) -> VFloat (negate x))),
+  ("absF", VBuiltin (\(VFloat x) -> VFloat (abs x))),
+  ("maxF", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (max x y)))),
+  ("minF", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (min x y)))),
+  ("truncate", VBuiltin (\(VFloat x) -> VInt (truncate x))),
+  ("round", VBuiltin (\(VFloat x) -> VInt (round x))),
+  ("ceiling", VBuiltin (\(VFloat x) -> VInt (ceiling x))),
+  ("floor", VBuiltin (\(VFloat x) -> VInt (floor x))),
+  ("recip", VBuiltin (\(VFloat x) -> VFloat (recip x))),
+  ("pi", VFloat pi),
+  ("exp", VBuiltin (\(VFloat x) -> VFloat (exp x))),
+  ("log", VBuiltin (\(VFloat x) -> VFloat (log x))),
+  ("sqrt", VBuiltin (\(VFloat x) -> VFloat (sqrt x))),
+  ("(**)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (x ** y)))),
+  ("logBase", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> VFloat (logBase x y)))),
+  ("sin", VBuiltin (\(VFloat x) -> VFloat (sin x))),
+  ("cos", VBuiltin (\(VFloat x) -> VFloat (cos x))),
+  ("tan", VBuiltin (\(VFloat x) -> VFloat (tan x))),
+  ("asin", VBuiltin (\(VFloat x) -> VFloat (asin x))),
+  ("acos", VBuiltin (\(VFloat x) -> VFloat (acos x))),
+  ("atan", VBuiltin (\(VFloat x) -> VFloat (atan x))),
+  ("sinh", VBuiltin (\(VFloat x) -> VFloat (sinh x))),
+  ("cosh", VBuiltin (\(VFloat x) -> VFloat (cosh x))),
+  ("tanh", VBuiltin (\(VFloat x) -> VFloat (tanh x))),
+  ("expm1", VBuiltin (\(VFloat x) -> VFloat (expm1 x))),
+  ("log1p", VBuiltin (\(VFloat x) -> VFloat (log1p x))),
+  ("log1pexp", VBuiltin (\(VFloat x) -> VFloat (log1pexp x))),
+  ("log1mexp", VBuiltin (\(VFloat x) -> VFloat (log1mexp x))),
+  ("fromInteger", VBuiltin (\(VInt x) -> VFloat (fromInteger (toInteger x)))),
+
+  ("(&&)", VBuiltin (\x -> VBuiltin (\y -> hsToLstBool (lstToHsBool x && lstToHsBool y)))),
+  ("(||)", VBuiltin (\x -> VBuiltin (\y -> hsToLstBool (lstToHsBool x || lstToHsBool y)))),
+
+  ("(==)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x == y)))),
+  ("(/=)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x /= y)))),
+  ("(>)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x > y)))),
+  ("(>=)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x >= y)))),
+  ("(<)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x < y)))),
+  ("(<=)", VBuiltin (\(VInt x) -> VBuiltin (\(VInt y) -> hsToLstBool (x <= y)))),
+  ("(>.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> hsToLstBool (x > y)))),
+  ("(>=.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> hsToLstBool (x >= y)))),
+  ("(<.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> hsToLstBool (x < y)))),
+  ("(<=.)", VBuiltin (\(VFloat x) -> VBuiltin (\(VFloat y) -> hsToLstBool (x <= y)))),
+
+  ("chr", VBuiltin (\(VInt x) -> VChar (chr x))),
+  ("ord", VBuiltin (\(VChar c) -> VInt (ord c))),
+
+  -- ("(^^)", VBuiltin (\(VString str1) -> VBuiltin (\(VString str2) -> VString (str1++str2)))),
+
+  ("show", VBuiltin (hsToLstStr . show)),
+  -- ("readBool", VBuiltin (\(VString str) -> hsToFstBool (read str))),
+  -- ("readInt", VBuiltin (\(VString x) -> VInt (read x))),
+  -- ("readInt", VBuiltin (\(VString c) -> VChar (read c))),
+
+  ("putStrOut", VBuiltin (\_ty -> VBuiltin (\val -> VIO $ putStr (show val) $> VCon "()" []))),
+  ("putStrErr", VBuiltin (\val -> VIO $ hPutStr stderr (show val) $> VCon "()" [])),
+  -- ("getChar", VIO $ getChar <&> VChar),
+  -- ("getLine", VIO $ getLine <&> VString),
+  -- ("getContents", VIO $ getContents <&> VString),
+
+  -- ("openFile", VBuiltin (\(VString path) -> VBuiltin (\(VCon mode []) -> VIO $ case mode of
+  --   "ReadMode" -> openFile path ReadMode <&> VCon "FileHandle" . (:[]) . VHandle
+  --   "WriteMode" -> openFile path WriteMode <&> VCon "FileHandle" . (:[]) . VHandle
+  --   "AppendMode" -> openFile path AppendMode <&> VCon "FileHandle" . (:[]) . VHandle
+  --   _ -> undefined))),
+  -- ("putFileStr", VBuiltin (\(VCon "FileHandle" [VHandle handle]) -> VBuiltin (\(VString str) -> VIO $ hPutStr handle str $> VUnit))),
+  -- ("readFileChar", VBuiltin (\(VCon "FileHandle" [VHandle handle]) -> VIO $ hGetChar handle <&> VChar)),
+  -- ("readFileLine", VBuiltin (\(VCon "FileHandle" [VHandle handle]) -> VIO $ hGetLine handle <&> VString)),
+  -- ("isEOF", VBuiltin (\(VCon "FileHandle" [VHandle handle]) -> VIO $ hIsEOF handle <&> hsToFstBool)),
+  -- ("closeFile", VBuiltin (\(VCon "FileHandle" [VHandle handle]) -> VIO $ hClose handle $> VUnit)),
+
+  ("id", VBuiltin id),
+  ("undefined", VBuiltin undefined),
+  -- TODO: improve
+  ("error", VBuiltin undefined),
+  ("fork", VFork),
+  ("if_", VIf [])
+  ]
+
+-- haskell bool to least bool
+hsToLstBool :: Bool -> Value
+hsToLstBool True = VCon "True" []
+hsToLstBool False = VCon "False" []
+
+-- freeST bool to least bool
+lstToHsBool :: Value -> Bool
+lstToHsBool (VCon "True" []) = True
+lstToHsBool (VCon "False" []) = False
+
+hsToLstStr :: String -> Value
+hsToLstStr = foldr (\char acc -> VCon "::" [VChar char, acc]) (VCon "[]" [])
+
+chan :: IO (ChannelEnd, ChannelEnd)
+chan = do
+  c1 <- Chan.newChan
+  c2 <- Chan.newChan
+  return ((c1, c2), (c2, c1))
+
+receive :: ChannelEnd -> IO (Value, ChannelEnd)
+receive c = do
+  v <- Chan.readChan (fst c)
+  return (v, c)
+
+send :: Value -> ChannelEnd -> IO ChannelEnd
+send v c = do
+  Chan.writeChan (snd c) v
+  return c
+
+wait :: Value -> Value
+wait (VChan c) =
+  VIO $ Chan.readChan (fst c)
+
+close :: Value -> IO Value
+close (VChan c) = do
+  Chan.writeChan (snd c) (VCon "()" [])
+  return (VCon "()" [])
diff --git a/freest/src/LeaST/LeaST.hs b/freest/src/LeaST/LeaST.hs
new file mode 100644
index 00000000..d5daba27
--- /dev/null
+++ b/freest/src/LeaST/LeaST.hs
@@ -0,0 +1,33 @@
+module LeaST.LeaST where
+
+import qualified Syntax.Base as B
+import qualified Syntax.Type as T
+import qualified Syntax.Kind as K
+import qualified Syntax.Module as M
+
+type LeastProg = (M.DataDeclList, M.TypeDeclList, M.KindSigList, Exp)
+
+data Exp 
+  = Var B.Variable
+  | Lit Literal
+  | Abs B.Variable T.Type Exp
+  | App Exp Exp
+  | Con B.Identifier
+  | Case Exp [(Alt, Exp)]
+  | Type T.Type
+  | TAbs B.Variable K.Kind Exp
+  | TApp Exp Exp
+  -- | Source B.Span Exp
+  deriving Show
+
+data Literal = LInt Int
+  | LFloat Double
+  | LChar Char
+  deriving Show
+
+data Alt = ACon B.Identifier [B.Variable]
+  | ALit Literal
+  | AWildCard
+  deriving Show
+
+-- type Bind = B.Level (B.Variable T.Type Exp) (B.Variable K.Kind Exp)
diff --git a/freest/src/LeaST/PrettyPrint.hs b/freest/src/LeaST/PrettyPrint.hs
new file mode 100644
index 00000000..c17e23e0
--- /dev/null
+++ b/freest/src/LeaST/PrettyPrint.hs
@@ -0,0 +1,40 @@
+module LeaST.PrettyPrint where
+
+import qualified LeaST.LeaST as L
+import qualified Syntax.Base as B
+
+import Debug.Trace
+import Data.List ( intersperse )
+
+prettyPrint :: L.Exp -> IO ()
+prettyPrint exp = putStrLn $ (prettyStr exp 0)
+
+prettyStr :: L.Exp -> Int -> String
+prettyStr (L.Var var) _ = getStringFromVariable var 
+prettyStr (L.Lit lit) _ = literalStr lit
+prettyStr (L.Abs var _ exp) indent = "(\\" ++ (getStringFromVariable var) ++ " -> " ++ "\n" ++ replicate (indent+2) ' ' ++ (prettyStr exp (indent+2)) ++ "\n" ++ replicate (indent) ' ' ++ ")"
+prettyStr (L.App lExp rExp) indent = prettyStr lExp indent ++ " " ++ prettyStr rExp indent
+prettyStr (L.Con iden) _ = getStringFromIdentifier iden
+prettyStr (L.Case exp alts) indent = "case " ++ prettyStr exp indent ++ " of\n" ++ alternativesStr alts (indent+2)
+prettyStr (L.Type ty) _ = show ty
+prettyStr (L.TAbs var _ exp) indent = "(\\@" ++ (getStringFromVariable var) ++ " -> " ++ "\n" ++ replicate (indent+2) ' ' ++ (prettyStr exp (indent+2)) ++ "\n" ++ replicate (indent) ' ' ++ ")"
+prettyStr (L.TApp lExp rExp) indent = prettyStr lExp indent ++ " " ++ prettyStr rExp indent
+
+literalStr :: L.Literal -> String
+literalStr (L.LInt int) = show int
+literalStr (L.LFloat float) = show float
+literalStr (L.LChar char) = show char
+
+alternativesStr :: [(L.Alt, L.Exp)] -> Int -> String
+alternativesStr alts indent = concat $ intersperse "\n" $ map (\(alt, exp) -> replicate indent ' ' ++ (altStr alt ) ++ " -> " ++ (prettyStr exp indent)) alts 
+
+altStr :: L.Alt -> String
+altStr (L.ACon iden vars) = getStringFromIdentifier iden ++ " " ++ (unwords $ map getStringFromVariable vars)
+altStr (L.ALit lit) = literalStr lit
+altStr L.AWildCard = "_"
+
+getStringFromVariable :: B.Variable -> String
+getStringFromVariable (B.Variable { B.varSpan=_, B.internal=_, B.external=var}) = var
+
+getStringFromIdentifier :: B.Identifier -> String
+getStringFromIdentifier (B.Identifier _ str) = str
diff --git a/freest/src/LeaST/examples.lst b/freest/src/LeaST/examples.lst
new file mode 100644
index 00000000..f9ad63e1
--- /dev/null
+++ b/freest/src/LeaST/examples.lst
@@ -0,0 +1,42 @@
+-- abstraction
+-- (\x:Int -> + x x)
+
+-- aplication
+-- (\x:Int -> + x x) 2
+
+-- higher-order function
+-- (\f:(Int -> Int) -> (\x:Int -> f x)) (\x:Int -> + x x) 2
+
+-- Fixed point combinator - Y Combinator (Desde que adicionei o IO que não funciona)
+-- (\f:A -> (\x:B -> f (x x)) (\x:C -> f (x x)))
+
+-- Fixed point combinator for strict languages - Z Combinator
+-- (\f:A -> (\x:B -> f (\v:C -> x x v)) (\x:D -> f (\v:E -> x x )))
+
+-- factorial
+-- (\f:A -> (\x:B -> f (x x)) (\x:C -> f (x x))) (\fac:(Int -> Int) -> (\n:Int -> case n { 0 -> 1, _ -> (* n (fac (- n 1)))})) 5
+-- (\f:A -> (\x:B -> f (\v:C -> x x v)) (\x:D -> f (\v:E -> x x v))) (\fac:(Int -> Int) -> (\n:Int -> case n { 0 -> 1, _ -> (* n (fac (- n 1)))})) 5
+
+-- fibonacci
+-- (\f:A -> (\x:B -> f (x x)) (\x:C -> f (x x))) (\fib:(Int -> Int) -> (\n:Int -> case n { 0 -> 0, 1 -> 1, _ -> + (fib (- n 1)) (fib (- n 2))})) 1
+-- (\f:A -> (\x:B -> f (\v:C -> x x v)) (\x:D -> f (\v:E -> x x v))) (\fib:(Int -> Int) -> (\n:Int -> case n { 0 -> 0, 1 -> 1, _ -> + (fib (- n 1)) (fib (- n 2))})) 10
+
+-- create a channel
+-- chan ()
+
+-- tuples
+-- (1, 2)
+
+-- deconstruct constructors
+-- case A 1 2 {A x y -> x}
+
+-- deconstruct a tuple
+-- case (1, 2, 3) {(,,) a b c -> b}
+
+-- fork, close and wait
+--case chan () {
+--	(,) cL cR -> (\x:A -> (\y:B -> y)) (fork (\a:C -> (\x:A -> (\y:B -> y)) (putStrOut 1) (close cR))) ((\x:A -> (\y:B -> y)) (putStrOut 2) (wait cL))}
+
+
+-- id function with type abstraction and type application
+-- (\@a:*T -> (\x:B -> x)) @Int 1
diff --git a/freest/src/Parser/Parser.y b/freest/src/Parser/Parser.y
index 72c0c0fe..f1f28f1b 100644
--- a/freest/src/Parser/Parser.y
+++ b/freest/src/Parser/Parser.y
@@ -19,6 +19,7 @@ import Syntax.Kind qualified as K
 import Syntax.Type qualified as T 
 import Syntax.Module qualified as M
 import UI.Error
+import LeaST.LeaST qualified as L
 
 import Control.Monad.Except
 import Data.Bifunctor
@@ -33,6 +34,7 @@ import Data.List.NonEmpty qualified as NE
 %name parseModule Module
 %name parseEquivalenceTests EquivalenceTestCases
 %name parseKindingTests KindingTestCases
+%name parseLeaST LeastProg
 
 %tokentype { Token }
 %monad { Lexer }
@@ -587,6 +589,71 @@ TypeTestDecl :: { M.Module -> M.Module }
   | TypeDecl { $1 }
   | DataDecl { $1 }
 
+-- Least
+
+LeastProg :: { L.LeastProg }
+  : '{' LeastDecls '}' LExp { let (dat, ty, kind) = $2 in (dat, ty, kind, $4) }
+  | LExp {([], [], [], $1)}
+
+LeastDecls :: { (M.DataDeclList, M.TypeDeclList, M.KindSigList) }
+  : LeastDataDecl LeastDecls { let (dat, ty, kind) = $2 in (dat++[$1], ty, kind) }
+  | LeastTypeDecl LeastDecls { let (dat, ty, kind) = $2 in (dat, ty++[$1], kind) }
+  | LeastKindSig LeastDecls { let (dat, ty, kind) = $2 in (dat, ty, kind++[$1]) }
+  | {- empty -} { ([], [], []) }
+
+LeastDataDecl :: { (Identifier, T.Lambda M.ConsDeclList) }
+  : 'data' UPPER_ID KindedVarListWS '=' DataConsListPipe { (mkIdTk $2, ($3, $5)) }
+
+LeastTypeDecl :: { (Identifier, T.Lambda T.Type) }
+  : 'type' UPPER_ID KindedVarListWS '=' Type { (mkIdTk $2, ($3, $5)) }
+
+LeastKindSig :: { ([Identifier], K.Kind) }
+  : 'type' UpperIdListComma ':' Kind { ($2, $4)  }
+
+LExp :: { L.Exp }
+  : '\\' LOWER_ID ':' TypePrimary '->' LExp { L.Abs (mkVarTk $2) $4 $6 }
+  | '\\' '@' LOWER_ID ':' Kind '->' LExp { L.TAbs (mkVarTk $3) $5 $7 }
+-- TODO make use of the case sensitive parser ??
+  | 'case' LExp '{' LAlternatives '}' { L.Case $2 $4 }
+  | LExpApp { $1 }
+
+LExpPrimary :: { L.Exp }
+  : INT_LIT { L.Lit $ L.LInt (read $ getText $1) } 
+  | FLOAT_LIT { L.Lit $ L.LFloat (read $ getText $1) }
+  | CHAR_LIT { L.Lit $ L.LChar (read $ getText $1) }
+  | LOWER_ID { L.Var (mkVarTk $1) }
+  | UPPER_ID { L.Con (mkIdTk $1) }
+  | '(' LExp ')' { $2 }
+  | Op { L.Var $1 }
+  | '(' ')' { L.Con (mkTupleId 0 (spanFromTo $1 $2)) }
+  | '(' LExp ',' LExpListComma ')' { tupleLExp (spanFromTo $1 $5) (length $4) (reverse ($2 : $4)) }
+
+LExpApp :: { L.Exp }
+  : LExpApp LExpPrimary { L.App $1 $2 }
+  | LExpApp '@' TypePrimary { L.TApp $1 (L.Type $3) }
+  | LExpPrimary { $1 }
+
+LAlternatives :: { [(L.Alt, L.Exp)] }
+  : LAlt '->' LExp ',' LAlternatives { ($1, $3):$5 }
+  | LAlt '->' LExp { [($1, $3)] }
+
+LAlt :: { L.Alt }
+  : INT_LIT { L.ALit (L.LInt (read $ getText $1)) }
+  | FLOAT_LIT { L.ALit (L.LFloat (read $ getText $1)) }
+  | CHAR_LIT { L.ALit (L.LChar (read $ getText $1)) }
+  | WILDCARD { L.AWildCard }
+  | UPPER_ID LVarList { (L.ACon (mkIdTk $1) $2)} 
+-- implement (x, y) syntax for tuples in pattern
+  | '(' Commas ')' LVarList{ L.ACon (mkTupleId $2 (spanFromTo $1 $3)) $4 }
+
+LExpListComma :: { [L.Exp] }
+  : LExp ',' LExpListComma { $1 : $3 }
+  | LExp                  { [$1] }
+
+LVarList :: { [Variable] }
+  : {- empty -} { [] }
+  | ExpVar LVarList { $1 : $2 }
+
 {
 
 lexer cont = scan >>= cont
diff --git a/freest/src/Parser/ParserUtils.hs b/freest/src/Parser/ParserUtils.hs
index c430abcf..bcf79bd8 100644
--- a/freest/src/Parser/ParserUtils.hs
+++ b/freest/src/Parser/ParserUtils.hs
@@ -16,6 +16,7 @@ import Syntax.Names
 import Syntax.Expression qualified as E
 import Syntax.Kind qualified as K
 import Syntax.Type qualified as T
+import LeaST.LeaST qualified as L
 
 import Data.List.NonEmpty qualified as NE
 
@@ -51,3 +52,7 @@ addArgExp a e              = E.App (spanFromTo e a) e [a]
 addArgType :: T.Type -> T.Type -> T.Type
 addArgType t (T.App s u us)   = T.App s u (us ++ [t])
 addArgType t u                = T.App (spanFromTo u t) u [t]
+
+tupleLExp :: Span -> Int -> [L.Exp] -> L.Exp
+tupleLExp s n [e] = L.App (L.Con (mkTupleId n s)) e
+tupleLExp s n (e:es) = L.App (tupleLExp s n es) e
diff --git a/freest/src/UI/CLI.hs b/freest/src/UI/CLI.hs
index d49d5ffd..d743724b 100644
--- a/freest/src/UI/CLI.hs
+++ b/freest/src/UI/CLI.hs
@@ -11,7 +11,7 @@ module UI.CLI where
 import Options.Applicative
 
 -- | The command line options accepted by the FreeST compiler.
-data RunOpts = RunOpts{file :: FilePath}
+data RunOpts = RunOpts{file :: FilePath, least :: Bool}
 
 -- | The parser for the command line options.
 freestOpts :: Parser RunOpts
@@ -20,6 +20,9 @@ freestOpts = RunOpts
     ( help "FreeST (.fst) file"
     <> metavar "FILEPATH"
     )
+  <*> switch
+    ( long "least" 
+    <> help "Parse file as a LeaST file" )
 
 -- | The man page of the FreeST compiler.
 opts :: ParserInfo RunOpts