content: {-# LANGUAGE Arrows #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FunctionalDependencies #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE TypeFamilies #-}
  -- | Generic interpreter for the While-Language.
  module GenericInterpreter where
  
  import           Prelude hiding (lookup, and, or, not, div, read)
  
  import           Data.Label
  
  import           Control.Arrow
  import           Control.Arrow.Fail as Fail
  import           Control.Arrow.Fix
  import           Control.Arrow.Environment(ArrowEnv)
  import qualified Control.Arrow.Environment as Env
  import           Control.Arrow.Except(ArrowExcept)
  import qualified Control.Arrow.Except as Except
  import           Control.Arrow.Random
  import           Control.Arrow.Store(ArrowStore,read',write)
  import qualified Control.Arrow.Store as Store
  import           Control.Arrow.Utils
  
  import           Data.Text (Text)
  import           Data.String
  import           Data.Kind(Type)
  
  import           Syntax
  import           GHC.Exts
  
  type Prog = [Statement]
  
  -- | Generic interpreter for expressions of the While-language. It is
  -- an arrow computation @c Expr v@ that consumes expressions and
  -- produces values. The interpreter is parameterized by the type of
  -- values @v@, addresses @addr@, environment @env@ and arrow type
  -- @c@. It uses the @IsVal@ interface to combine values and uses the
  -- @ArrowEnv@ and @ArrowStore@ interface to access the environment.
  eval :: (Show addr, ArrowChoice c, ArrowRand v c,
           ArrowEnv Text addr c, ArrowStore addr v c,
           ArrowExcept exc c, ArrowFail e c,
           IsVal v c, IsException exc v c, IsString e,
           Env.Join v c, Store.Join v c, Fail.Join v c
          )
       => c Expr v
  eval = proc e -> case e of
    Var x _ -> Env.lookup'' read' -< x
    BoolLit b _ -> boolLit -< b
    And e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      and -< (v1,v2)
    Or e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      or -< (v1,v2)
    Not e1 _ -> do
      v1 <- eval -< e1
      not -< v1
    NumLit n _ -> numLit -< n
    RandomNum _ -> random -< ()
    Add e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      add -< (v1,v2)
    Sub e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      sub -< (v1,v2)
    Mul e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      mul -< (v1,v2)
    Div e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      div -< (v1,v2)
    Eq e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      eq -< (v1,v2)
    Lt e1 e2 _ -> do
      v1 <- eval -< e1
      v2 <- eval -< e2
      lt -< (v1,v2)
    Throw ex e1 _ -> do
      v <- eval -< e1
      Except.throw <<< namedException -< (ex,v)
  
  -- | Generic interpreter for statements of the While-language. It is
  -- an arrow computation @c [Statement] ()@ that consumes statements
  -- and does not produces a result. The interpreter is parameterized by
  -- the type of values @v@, addresses @addr@, environment @env@ and
  -- arrow type @c@.
  run :: (Show addr,
          ?fixpointAlgorithm :: FixpointAlgorithm (Fix (c [Statement] ())),
          ArrowChoice c, ArrowFix (c [Statement] ()),
          ArrowEnv Text addr c, ArrowStore addr v c,
          ArrowAlloc addr c, ArrowFail err c,
          ArrowExcept exc c, ArrowRand v c,
          IsString err, IsVal v c, IsException exc v c,
          Env.Join v c, Env.Join addr c, Store.Join v c, Except.Join () c,
          Fail.Join v c, JoinVal () c, JoinExc () c
         )
      => c [Statement] ()
  run = fix $ \run' -> proc stmts -> case stmts of
    Assign x e l:ss -> do
      v <- eval -< e
      addr <- Env.lookup (proc (addr,_) -> returnA -< addr)
                         (proc (x,v,l) -> alloc -< (x,v,l))
                -< (x,(x,v,l))
      write -< (addr,v)
      Env.extend run' -< (x,addr,ss)
    If cond s1 s2 _:ss -> do
      b <- eval -< cond
      if_ run' run' -< (b,([s1],[s2]))
      run' -< ss
    While cond body l:ss ->
      run' -< If cond (Begin [body,While cond body l] l) (Begin [] l) l : ss
    Begin ss _:ss' -> do
      run' -< ss
      run' -< ss'
    TryCatch body ex x handler l:ss -> do
      Except.catch
        (proc (body,_) -> run' -< [body])
        (proc ((_,(ex,x,handler,l)),e) ->
          matchException
            (proc (v,(x,handler,l)) -> do
              addr <- Env.lookup pi1 alloc -< (x,(x,v,l))
              write -< (addr,v)
              Env.extend run' -< (x, addr, [handler]))
            (proc _ -> returnA -< ())
            -< (ex,e,(x,handler,l)))
        -< (body,(ex,x,handler,l))
      run' -< ss
    Finally body fin _:ss -> do
      Except.finally (proc (body,_) -> run' -< [body])
              (proc (_,fin)  -> run' -< [fin])
        -< (body,fin)
      run' -< ss
    [] ->
      returnA -< ()
  
  -- | Interface for value operations.
  class Arrow c => IsVal v c | c -> v where
    -- | In case of the abstract interpreter allows to join the result
    -- of an @if@ statement.
    type family JoinVal x (c :: Type -> Type -> Type) :: Constraint
  
    boolLit :: c Bool v
    and :: c (v,v) v
    or :: c (v,v) v
    not :: c v v
    numLit :: c Int v
    add :: c (v,v) v
    sub :: c (v,v) v
    mul :: c (v,v) v
    div :: c (v,v) v
    eq :: c (v,v) v
    lt :: c (v,v) v
    if_ :: JoinVal z c => c x z -> c y z -> c (v, (x, y)) z
  
  class ArrowAlloc addr c where
    alloc :: c (Text,v,Label) addr
  
  class IsException exc v c | c -> v where
    type family JoinExc y (c :: Type -> Type -> Type) :: Constraint
    namedException :: c (Text,v) exc
    matchException :: JoinExc y c => c (v,x) y -> c x y -> c (Text,exc,x) y
  