Yet another attempt to normalise linear logic (not working)

GS2.hs

module GS2 where

import Data.STRef
import Control.Monad.ST
import qualified Data.Map as Map
import Data.Map (Map)

-- Terms to normalise
type Arity = (Int, Int, Int)
data Tm
    = Link0 Int
    | Link1 Int
    | None
    | Pair Tm Tm
    | Inl Tm
    | Inr Tm
    | Inst Tm
    | Opt Int Tm Tm
    | On  Int Tm Tm
    | Exp Int Arity Tm
    | At  Int Tm
    | Alt [(Guard, Tm)] -- TODO: figure out how to restructure.
    | Undef
    deriving (Eq, Show)

data Sem s
    = Unbound
    | Nil
    | Ref0 (STEvent s (Sem s))
    | Ref1 (STEvent s (Sem s))
    | Cons (Sem s) (Sem s)
    | X (Sem s)
    | Y (Sem s)
    | MK (Sem s)
    | SOpt (OptRef s) (Sem s) (Sem s)
    | SOn  (OptRef s) (Sem s) (Sem s)
    | SExp (ExpRef s) (ST s (Env s, Sem s))
    | SAt (ExpRef s)  (Env s -> Sem s)
    | Delay (Guard -> Sem s -> ST s ())
    | Syn Tm

type Guard = [(Int, Maybe Bool)]

add_guard :: Int -> Maybe Bool -> Guard -> Guard
add_guard i b g = ((i,b):g)

merge :: Guard -> Guard -> Maybe Guard
merge ((a,flag):as) bs = (merge as bs) >>= merge_check a flag
merge [] bs = pure bs

merge_check :: Int -> Maybe Bool -> Guard -> Maybe Guard
merge_check a flag ((b,f):bs) | (a == b) = if flag == f then Just bs else Nothing 
merge_check a flag (b:bs)                = fmap (b:) (merge_check a flag bs)
merge_check a flag []                    = Just [(a,flag)]

type STEvent s a = STRef s ([(Guard, Guard -> a -> ST s ())], [(Guard, a)])

newSTEvent :: ST s (STEvent s a)
newSTEvent = newSTRef ([], [])

waiton :: (STEvent s a) -> Guard -> (Guard -> a -> ST s ()) -> ST s ()
waiton evt guard f = do
    (cont, answers) <- readSTRef evt 
    writeSTRef evt ((guard, f):cont, answers)
    mapM_ impl answers
    where impl (g,val) = case merge guard g of
            Nothing -> pure ()
            Just q  -> f q val

signal :: (STEvent s a) -> Guard -> a -> ST s ()
signal evt guard answer = do
    (cont, answers) <- readSTRef evt
    writeSTRef evt (cont, (guard,answer):answers)
    mapM_ (\(q, f) -> case merge guard q of
        Nothing -> pure ()
        Just q' -> f q' answer) cont

type OptRef s = STEvent s Bool
type ExpRef s = STEvent s (ExpRefI s)

data ExpRefI s = EInst (Env s)
               | EDup (ExpRef s) (ExpRef s)
               | EDrop

data Env s = Env
    { linkref :: [STEvent s (Sem s)]
    , optref :: [OptRef s]
    , expref :: [ExpRef s] }

empty :: Env s
empty = Env { linkref = [], optref = [], expref = [] }

extend :: Env s -> Arity -> ST s (Env s)
extend env (n, o, e) = do
    linkref' <- sequence (replicate n newSTEvent)
    optref' <- sequence (replicate o newSTEvent)
    expref' <- sequence (replicate e newSTEvent)
    pure (env { linkref = linkref'
              , optref = (optref env) ++ optref'
              , expref = expref' })

eval :: Env s -> Tm -> Sem s
eval env (Link0 n)   = Ref0 (linkref env !! n)
eval env (Link1 n)   = Ref1 (linkref 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 y)    = Y (eval env y)
eval env (Inst x)   = MK (eval env x)
eval env (Opt k x y) = SOpt (optref env !! k) (eval env x) (eval env y)
eval env (On k x y)  = SOn  (optref env !! k) (eval env x) (eval env y)
eval env (Exp k a x) = SExp (expref env !! k) (extend env a >>= \e -> pure (e, eval e x))
eval env (At k x)    = SAt  (expref env !! k) (\e -> eval e x)

cut :: Guard -> Sem s -> Sem s -> ST s ()
cut cond (Ref0 s)      y           = signal s cond y
cut cond x            (Ref0 s)     = signal s cond x
cut cond (Ref1 s)      y           = waiton s cond (\g x -> cut g x y)
cut cond x            (Ref1 s)     = waiton s cond (\g y -> cut g x y)
cut cond (Delay f)    y            = f cond y
cut cond x            (Delay f)    = f cond x
cut cond Nil          Nil          = pure ()
cut cond (Cons x1 x2) (Cons y1 y2) = cut cond x1 y1 >> cut cond x2 y2
cut cond (SOpt k x y) (X a)        = (signal k cond False >> cut cond x a)
cut cond (SOpt k x y) (Y b)        = (signal k cond True  >> cut cond y b)
cut cond (X a)        (SOpt k x y) = (signal k cond False >> cut cond x a)
cut cond (Y b)        (SOpt k x y) = (signal k cond True  >> cut cond y b)
cut cond (SOn k x y)  z            = waiton k cond (delay x y z)
cut cond z            (SOn k x y)  = waiton k cond (delay x y z)
cut cond (MK x)       (SExp k g)   = instantiate k cond x g
cut cond (SExp k g)   (MK x)       = instantiate k cond x g
cut cond (Cons x y)   (SExp k g)   = duplicate k cond x y g
cut cond (SExp k g)   (Cons x y)   = duplicate k cond x y g
cut cond Nil          (SExp k g)   = signal k cond EDrop
cut cond (SExp k g)   Nil          = signal k cond EDrop
cut cond (SAt j f)    (SExp k g)   = waiton j cond (atexp f k g)
cut cond (SExp k g)   (SAt j f)    = waiton j cond (atexp f k g)

cut_stref :: STRef s (Sem s) -> Sem s -> (Sem s -> ST s ()) -> ST s ()
cut_stref s y f = do
    x <- readSTRef s
    case x of
        Unbound -> writeSTRef s y
        _     -> f x

delay :: Sem s -> Sem s -> Sem s -> Guard -> Bool -> ST s ()
delay x y z cond False = cut cond x z
delay x y z cond True  = cut cond y z

instantiate k cond x g = do
    (env, y) <- g
    signal k cond (EInst env)
    cut cond x y

duplicate k cond x y g = do
    i <- newSTEvent
    j <- newSTEvent
    signal k cond (EDup i j)
    cut cond x (SExp i g)
    cut cond y (SExp j g)

atexp f k g cond (EInst env) = cut cond (f env) (SExp k g)
atexp f k g cond (EDup x y)  = waiton x cond (atexp f k g)
                            >> waiton y cond (atexp f k g)
atexp f k g cond EDrop       = pure ()

data Readback s = Readback
    { get_guard :: Guard
    , get_guard_counter :: STRef s Int }

start_readback :: ST s (Readback s)
start_readback = do
    stref <- newSTRef 1
    pure (Readback { get_guard = []
                   , get_guard_counter = stref })

new_guard :: Readback s -> ST s Int
new_guard rb = do
    num <- readSTRef (get_guard_counter rb)
    writeSTRef (get_guard_counter rb) (num+1)
    pure num

data Box s a = FlappingInBreeze
             | Bare a
             | Guarded [(Guard, Box s a)]
             | Indirect (STRef s (Box s a))
             | Build (a -> a) (Box s a)
             | Fap (a -> a -> a) (Box s a) (Box s a)

readback :: Readback s -> Sem s -> ST s (Box s Tm)
readback rb Unbound = undefined
readback rb Nil     = pure (Bare None)
readback rb (Ref0 s) = do
    stref <- newSTRef FlappingInBreeze
    let r = get_guard rb
        handler g x = (readback (rb { get_guard = g }) x >>= guardedSTRef r g stref)
    signal s (get_guard rb) (Delay handler)
    pure (Indirect stref)
readback rb (Ref1 s) = do
    stref <- newSTRef FlappingInBreeze
    let r = get_guard rb
        handler g x = (readback (rb { get_guard = g }) x >>= guardedSTRef r g stref)
    waiton s (get_guard rb) handler
    pure (Indirect stref)
readback rb (Cons x y) = do
    a <- readback rb x
    b <- readback rb y
    pure (Fap Pair a b)
readback rb (X x) = do
    a <- readback rb x
    pure (Build Inl a)
readback rb (Y x) = do
    a <- readback rb x
    pure (Build Inr a)
readback rb (MK x) = do
    a <- readback rb x
    pure (Build Inst a)
readback rb (SOpt ref x y) = do
    let g = get_guard rb
    n <- new_guard rb
    a <- readback (rb { get_guard = add_guard n (Just False) g }) x
    b <- readback (rb { get_guard = add_guard n (Just True) g }) y
    signal ref (add_guard n (Just False) g) False
    signal ref (add_guard n (Just True) g) True
    pure (Fap (Opt n) a b)
readback rb (SOn ref x y) = do
    stref <- newSTRef FlappingInBreeze
    let g = get_guard rb
        u h False = readback (rb { get_guard = h }) x >>= guardedSTRef g h stref
        u h True  = readback (rb { get_guard = h }) y >>= guardedSTRef g h stref
    waiton ref g u
    pure (Indirect stref)
readback rb (SAt ref f) = do
    stref <- newSTRef FlappingInBreeze
    let g = get_guard rb
        u h (EInst env) = readback (rb { get_guard = h }) (f env) >>= guardedSTRef g h stref
        u h (EDup x y) = do
            waiton x g u
            waiton y g u
        u h (EDrop) = do
            guardedSTRef g h stref (Bare None)
    waiton ref g u
    pure (Indirect stref)
readback rb (SExp ref stev) = do
    let g = get_guard rb
    n <- new_guard rb
    (env, x) <- stev
    a <- readback (rb { get_guard = add_guard n Nothing g }) x
    signal ref (add_guard n Nothing g) (EInst env)
    pure (Build (Exp n (0,0,0)) a)
readback rb (Delay f) = do
    n <- new_guard rb
    f (get_guard rb) (Syn (Link1 n))
    pure (Bare (Link0 n))
readback rb (Syn tm) = pure (Bare tm)

guardedSTRef :: Guard -> Guard -> STRef s (Box s Tm) -> Box s Tm -> ST s ()
guardedSTRef p q stref box = do
    let g = q -- clean_guard p q
    status <- readSTRef stref
    case status of
        FlappingInBreeze -> writeSTRef stref (Guarded [(g,box)])
        Guarded gs -> writeSTRef stref (Guarded ((g,box):gs))

clean_guard :: Guard -> Guard -> Guard
clean_guard [] q     = q
clean_guard (g:gs) q = filter (/=g) (clean_guard gs q)

finish_readback :: Box s Tm -> ST s Tm
finish_readback FlappingInBreeze = pure Undef
finish_readback (Bare tm) = pure tm
finish_readback (Guarded []) = pure Undef
finish_readback (Guarded [([],x)]) = finish_readback x
finish_readback (Guarded gs) = fmap Alt (headscratcher gs)
finish_readback (Indirect ind) = readSTRef ind >>= finish_readback
finish_readback (Build f box) = fmap f (finish_readback box)
finish_readback (Fap f a b) = f <$> finish_readback a <*> finish_readback b

headscratcher :: [(Guard, Box s Tm)] -> ST s [(Guard, Tm)]
headscratcher [(g,x)] = do
    x' <- finish_readback x
    pure [(g,x')]
headscratcher ((g,x):xs) = do
    gs <- headscratcher xs
    x' <- finish_readback x
    pure ((g,x'):gs)

tryout1 = runST $ do
    let prog_a0 = (Link0 0)
        prog_a1 = (Link1 0)
        prog_b0 = (Link0 0)
        prog_b1 = (Link1 0)
    env1 <- extend empty (1,0,0)
    env2 <- extend empty (1,0,0)
    cut [] (eval env1 prog_a0) (eval env2 prog_b0)
    rb <- start_readback
    box1 <- readback rb (eval env1 prog_a1)
    box2 <- readback rb (eval env2 prog_b1)
    tm1 <- finish_readback box1
    tm2 <- finish_readback box2
    pure (Pair tm1 tm2)

tryout2 = runST $ do
    let prog_a0 = (Opt 0 (Link0 0) (Link0 0))
        prog_a1 = (On 0 (Link1 0) (Link1 0))
        prog_b0 = (On 0 (Link0 0) (Link0 0))
        prog_b1 = (Opt 0 (Link1 0) (Link1 0))
    env1 <- extend empty (1,1,0)
    env2 <- extend empty (1,1,0)
    cut [] (eval env1 prog_a0) (eval env2 prog_b0)
    rb <- start_readback
    box1 <- readback rb (eval env1 prog_a1)
    box2 <- readback rb (eval env2 prog_b1)
    tm1 <- finish_readback box1
    tm2 <- finish_readback box2
    pure (Pair tm1 tm2)

-- Result:
-- Pair (Alt [([(5,Just True)],
--             Alt [
--               ([(2,Just False)],Link0 15),
--               ([(2,Just True)],Link0 14),
--               ([],Link0 13)]),
--            ([(5,Just False)],
--             Alt [
--               ([(2,Just False)],Link0 12),
--               ([(2,Just True)],Link0 11),
--               ([],Link0 10)]),
--            ([(2,Just True)],
--             Alt [
--               ([(5,Just True)],Link0 8),
--               ([(5,Just False)],Link0 6),
--               ([],Link0 4)]),
--            ([(2,Just False)],
--             Alt [
--               ([(5,Just True)],Link0 9),
--               ([(5,Just False)],Link0 7),
--               ([],Link0 3)])])
--      (Opt 1
--       (Opt 2
--        (Alt [([(5,Just True)],Link1 15),([(5,Just False)],Link1 12),([],Link1 3)])
--        (Alt [([(5,Just True)],Link1 14),([(5,Just False)],Link1 11),([],Link1 4)]))
--       (Opt 5
--        (Alt [([],Link1 10),([(2,Just False)],Link1 7),([(2,Just True)],Link1 6)])
--        (Alt [([],Link1 13),([(2,Just False)],Link1 9),([(2,Just True)],Link1 8)])))
--
-- Same thing without cleaning guards
-- Pair (Alt [
--         ([(5,Just True)],
--          Alt [
--             ([(2,Just False),(5,Just True)],Link0 15),
--             ([(2,Just True),(5,Just True)],Link0 14),
--             ([],Link0 13)]),
--         ([(5,Just False)],
--          Alt [
--             ([(2,Just False),(5,Just False)],Link0 12),
--             ([(2,Just True),(5,Just False)],Link0 11),
--             ([],Link0 10)]),
--         ([(2,Just True)],
--          Alt [
--             ([(2,Just True),(5,Just True)],Link0 8),
--             ([(2,Just True),(5,Just False)],Link0 6),
--             ([],Link0 4)]),
--         ([(2,Just False)],
--          Alt [
--             ([(2,Just False),(5,Just True)],Link0 9),
--             ([(2,Just False),(5,Just False)],Link0 7),
--             ([],Link0 3)])])
--      (Opt 1
--       (Opt 2
--           (Alt [
--             ([(2,Just False),(5,Just True)],Link1 15),
--             ([(2,Just False),(5,Just False)],Link1 12),
--             ([],Link1 3)])
--           (Alt [
--             ([(2,Just True),(5,Just True)],Link1 14),
--             ([(2,Just True),(5,Just False)],Link1 11),
--             ([],Link1 4)]))
--       (Opt 5
--           (Alt [
--             ([],Link1 10),
--             ([(2,Just False), (5,Just False)],Link1 7),
--             ([(2,Just True), (5,Just False)],Link1 6)])
--           (Alt [
--             ([],Link1 13),
--             ([(2,Just False),(5,Just True)],Link1 9),
--             ([(2,Just True),(5,Just True)],Link1 8)])))


--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)