{-# LANGUAGE ExistentialQuantification #-}
module InterDeep (I, cont, barrier, retrieve, retrieveFun) where

import FOL
import Input

import Control.Applicative
import Control.Monad
import Data.List
import Data.Monoid


-- Deep embedding

type I a = Cont Prop a

data Cont r a = Pure [a]
--              | Choice [Cont r a]
              | C [(a -> r) -> r]
              | forall b. Apply (Cont r (b -> a)) (Cont r b)

instance Functor (Cont r) where
    fmap f x = pure f <*> x

instance Applicative (Cont r) where
    pure a   = Pure [a]
    x <*> y  = Apply x y

runCont :: Cont r a -> [(a -> r) -> r]
runCont (Pure xs) = [\c -> c x | x <- xs]
runCont (C fs) = fs
runCont (Apply x y) | isPure x || isPure y =
     [\c -> a (\a' -> b (\b' -> c (a' b')))
           | a <- runCont x, b <- runCont y]
runCont (Apply x y) = 
    concat [[\c -> a (\a' -> b (\b' -> c (a' b'))),
             \c -> b (\b' -> a (\a' -> c (a' b')))] 
           | a <- runCont x, b <- runCont y]

isPure :: Cont r a -> Bool
isPure (Pure _) = True
isPure (Apply x y) = isPure x && isPure y
isPure _ = False

cont :: ((a -> Prop) -> Prop) -> I a
cont f = C [f]

barrier :: I (Exp -> Prop) -> I (Exp -> Prop)
barrier i = Pure (retrieveFun i)

retrieve :: I Prop -> [Prop]
retrieve = map ($ id) . runCont

retrieveFun :: I (a -> Prop) -> [a -> Prop]
retrieveFun i = [\e -> f ($ e) | f <- runCont i]

--shift :: ((a -> I Prop) -> I Prop) -> I a
--shift h = C [\c -> runCont (h (\v -> C [\c' -> c' (c v)])) id]

reset :: I Prop -> I Prop
reset i = Pure [f id | f <- runCont i]

resetFun :: I (Exp -> Prop) -> I (Exp -> Prop)
resetFun i = Pure [\e -> f ($ e) | f <- runCont i]