{-# LANGUAGE Arrows #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies #-}
module GenericInterpreter where

import           Prelude hiding (succ, pred, fail, map)
import           Syntax (Expr(..))

import           Control.Arrow
import           Control.Arrow.Utils
import           Control.Arrow.Fix
import           Control.Arrow.Fail (ArrowFail,failString)
import qualified Control.Arrow.Fail as Fail
import           Control.Arrow.Closure (ArrowClosure)
import qualified Control.Arrow.Closure as Cls
import           Control.Arrow.Environment (ArrowEnv)
import           Control.Arrow.LetRec(ArrowLetRec)
import qualified Control.Arrow.LetRec as LetRec
import qualified Control.Arrow.Environment as Env

import           Data.Text (Text)
import           Data.Kind (Type)

import           Text.Printf

import           GHC.Exts (IsString(..),Constraint)

-- | Shared interpreter for PCF.
eval :: (IsString e,
         IsVal v c,
         ?fixpointAlgorithm :: FixpointAlgorithm (Fix (c Expr v)),
         ArrowChoice c,
         ArrowFix (c Expr v),
         ArrowEnv Text v c,
         ArrowFail e c,
         ArrowClosure Expr v c,
         ArrowLetRec Text v c,
         Env.Join v c,
         Cls.Join v v c,
         Fail.Join v c,
         Join v c)
     => c Expr v
eval = fix $ \ev -> proc e0 -> case e0 of
  Var x _ -> Env.lookup' -< x
  Lam x e l -> Cls.closure -< Lam x e l
  App e1 e2 _ -> do
    fun <- ev -< e1
    arg <- map ev -< e2
    applyClosure' ev -< (fun, arg)
  Zero _ -> zero -< ()
  Succ e _ -> do
    v <- ev -< e
    succ -< v
  Pred e _ -> do
    v <- ev -< e
    pred -< v
  Mult e1 e2 _ -> do
    v1 <- ev -< e1
    v2 <- ev -< e2
    mult -< (v1,v2)
  IfZero e1 e2 e3 _ -> do
    v1 <- ev -< e1
    if_ ev ev -< (v1, (e2, e3))
  Let bnds body _ -> do
    vs <- map ev -< [ e | (_,e) <- bnds ]
    LetRec.letRec ev -< ([ (v,cl) | ((v,_),cl) <- zip bnds vs ], body)
  Apply e _ -> ev -< e
  where
    -- Helper function used to apply closure or a suspended fixpoint computation to its argument.
    applyClosure' ev = Cls.apply $ proc (e,args) -> case e of
      Lam xs body l
        | length xs == length args -> Env.extend' ev -< (zip xs args,Apply body l)
        | otherwise ->
            failString -< printf "Try to apply a function with %s parameters to %s arguments"
                                 (show (length xs)) (show (length xs))
      _ -> failString -< fromString $ "Expected a function but got " ++ show e

-- | Interface for numeric operations
class IsVal v c | c -> v where
  type family Join y (c :: Type -> Type -> Type) :: Constraint

  -- | increments the given number value.
  succ :: c v v

  -- | decrements the given number value.
  pred :: c v v

  -- | creates the numeric value zero.
  zero :: c () v

  mult :: c (v,v) v

  if_ :: Join z c => c x z -> c y z -> c (v, (x, y)) z
