Yet another evaluator

GS2.hs

-- Haven't tested this, may contain trivial bugs.
module GS2 where

import Control.Concurrent
import Control.Concurrent.MVar
-- import qualified Data.Map as Map
-- import Data.Map (Map)

data Ty
    = Initial
    | Terminal
    | Unit
    | ParUnit
    | Sum Ty Ty
    | Prod Ty Ty
    | Tensor Ty Ty
    | Par Ty Ty
    | OfCourse Ty
    | WhyNot Ty
    | Pos Int
    | Neg Int
    deriving (Show, Eq)
 
type Arity = (Int, Int, Int)
data Tm
    = Link Int
    | None
    | Pair Tm Tm
    | Inl Tm
    | Inr Tm
    | Opt Int Tm Tm
    | On Int Tm Tm
    | Exp Int Arity Tm
    | At Int Tm
    | Inst Tm
    deriving (Eq, Show)

eval :: Env -> Tm -> Sem
eval env (Link n)   = link env !! n
eval env None       = Nil
eval env (Pair x y) = Cons (eval env x) (eval env y)
eval env (Inl x)  = X (eval env x)
eval env (Inr x)  = Y (eval env x)
eval env (Inst x) = X (eval env x)
eval env (At k x) = Ptr (expon env !! k) x
eval env (Opt k x y) = Serv (opt_fn env (option env !! k) x y)
eval env (On k x y)  = Serv (on_server env (option env !! k) x y)
eval env (Exp k a x) = Serv (exp_fn env (expon env !! k) a x)

opt_fn :: Env -> MVar OptS -> Tm -> Tm -> Sem -> IO ()
opt_fn env o x _ (X v) = do
    putMVar o XOpt
    cut (eval env x) v
opt_fn env o _ y (Y v) = do
    putMVar o YOpt
    cut (eval env y) v
opt_fn env o x y other = do
    mv <- newEmptyMVar
    forkIO (cut other (Ref mv))
    takeMVar mv >>= opt_fn env o x y

on_server :: Env -> MVar OptS -> Tm -> Tm -> Sem -> IO ()
on_server env o x y v = do
    choice <- readMVar o
    case choice of
        XOpt -> cut (eval env x) v
        YOpt -> cut (eval env y) v

exp_fn :: Env -> (MVar ExpS, MVar (MStream Env)) -> Arity -> Tm -> Sem -> IO ()
exp_fn env e a x Nil = do
    putMVar (fst e) Drop
exp_fn env e a x (Cons y z) = do
    putMVar (fst e) Rep
    forkIO (exp_fn env e a x y)
    exp_fn env e a x z
exp_fn env e a x (X z) = do 
    nenv <- extend env a
    putMVar (fst e) (Make nenv)
    cut (eval nenv x) z
exp_fn env e a x (Ptr f y) =
    wait_on (snd f) (\p -> exp_fn env e a x (eval p y))
exp_fn env e a x other = do
    mv <- newEmptyMVar
    forkIO (cut other (Ref mv))
    takeMVar mv >>= exp_fn env e a x

cut :: Sem -> Sem -> IO ()
cut (Ref s) v = putMVar s v
cut v (Ref s) = putMVar s v
cut Nil Nil = pure ()
cut (Cons x y) (Cons z w) = forkIO (cut x z) >> cut y w
cut (Serv f) v = f v
cut v (Serv f) = f v

empty :: Env
empty = Env { link = [], option = [], expon = [] }

extend :: Env -> Arity -> IO Env
extend env (linkc,optc,expc) = do
    links <- mapM id (replicate linkc link_server)
    opts <- mapM id (replicate optc opt_server)
    exps <- mapM id (replicate expc exp_server)
    pure (Env
        { link = links
        , option = opts ++ option env
        , expon = exps })

data Sem = Nil
         | Ref (MVar Sem)
         | Cons Sem Sem
         | X Sem
         | Y Sem
         | Ptr (MVar ExpS, MVar (MStream Env)) Tm
         | Serv (Sem -> IO ())

data Env = Env { link   :: [Sem]
               , option :: [MVar OptS]
               , expon  :: [(MVar ExpS, MVar (MStream Env))] }

data OptS = XOpt | YOpt
data ExpS = Drop | Rep | Make Env
data MStream a = Fin | Next a (MVar (MStream a))

opt_server :: IO (MVar OptS)
opt_server = newEmptyMVar

link_server :: IO Sem
link_server = do
    mv <- newEmptyMVar
    forkIO $ do
        x <- takeMVar mv
        y <- takeMVar mv
        cut x y
    pure (Ref mv)

exp_server :: IO (MVar ExpS, MVar (MStream Env))
exp_server = do
    mv <- newEmptyMVar
    ms <- newEmptyMVar
    forkIO (takeMVar mv >>= exp_count mv ms 1)
    pure (mv, ms)
    where exp_count m s n Rep = (takeMVar m >>= exp_count m s (n+1))
          exp_count _ s 1 Drop = putMVar s Fin
          exp_count _ s 0 (Make env) = do
            sv <- newMVar Fin
            putMVar s (Next env sv)
          exp_count m s n (Make env) = do
            sv <- newEmptyMVar
            putMVar s (Next env sv)
            takeMVar m >>= exp_count m sv (n-1)

wait_on :: MVar (MStream Env) -> (Env -> IO ()) -> IO ()
wait_on mv cb = do
    opt <- readMVar mv
    case opt of
        Fin -> pure ()
        Next a nv -> forkIO (cb a) >> wait_on nv cb