tempus-0.1.0: Tempus/Evaluation.hs

-- | Evaluation of Tempus expressions.
module Tempus.Evaluation (
    EvalEnv,
    Value (..),

    evalExpr
) where


import Tempus.Syntax
import Tempus.TypeCheck

import Data.List

-- | Representation of evaluation environments as a list of pairs of a variable with its expression.
type EvalEnv = [(Var, Expr)]

-- | Internal format for the value of an expression.
data Value = Natural Integer
           | Unit
           | Function (Value -> Value)
           | Pair Value Value
           | ChoiceLeft Value
           | ChoiceRight Value
           | Behavior (RelTime -> Value)
           | Event RelTime Value

-- | Number of time steps with corresponding values to include when showing a bahavior.
behaviorShowFuture :: Integer
behaviorShowFuture = 7

-- | Number of time steps to look ahead when deciding if to show an event as never occuring or not.
eventShowLookAhead :: Integer
eventShowLookAhead = 100

-- TODO: make length of behavior future scalable
-- TODO: make mu/nu expression depth scalable
instance Show Value where
    showsPrec _ (Natural i) = shows i
    showsPrec _ (Unit) = showString "()"
    showsPrec _ (Function _) = showString "<function>"
    showsPrec p (Pair e1 e2) = showParen (p > 0) $
        showsPrec 1 e1 . showString " , " . showsPrec 0 e2
    showsPrec p (ChoiceLeft e) = showParen (p > 3) $
        showString "left " . showsPrec 4 e
    showsPrec p (ChoiceRight e) = showParen (p > 3) $
        showString "right " . showsPrec 4 e
    showsPrec p (Behavior f) = showParen (True) $ showString $ (
        concat . intersperse "; "
        . map (\ps -> case ps of
                          [(v, t)] -> "@" ++ show (fromTime t) ++ ": " ++ v
                          ps -> "@" ++ (let ps' = map snd ps in
                                    show (head ps') ++ ".." ++ show (last ps')) ++ ": " ++ fst (head ps))
        . groupBy (\x y -> fst x == fst y) . map (\t -> (show $ f t, t)) $
              map fromInteger [1..behaviorShowFuture]) ++ "; ..."
    showsPrec p (Event t e) = showParen (p > 3) $
        if t > fromInteger eventShowLookAhead
            then showString "?"
            else showString "@" . shows t . showString ": " . shows e

-- | Time representation for events and behaviors
data RelTime = One
             | Succ RelTime
             deriving (Eq)

-- | A 'RelTime' value for an infinite number of time steps.
infinite :: RelTime
infinite = Succ infinite

instance Show RelTime where
    show t = show $ fromTime t

-- | Conversion from 'RelTime' values to 'Integer' values
fromTime :: RelTime -> Integer
fromTime One      = 1
fromTime (Succ t) = 1 + fromTime t

instance Ord RelTime where
    compare One       One       = EQ
    compare One       _         = LT
    compare (Succ t1) (Succ t2) = compare t1 t2
    compare (Succ _)  _         = GT

    min One      t'        = One
    min t        One       = One
    min (Succ t) (Succ t') = Succ $ min t t'

instance Num RelTime where
    t + t' = Succ $ case t of
                        One    -> t'
                        Succ t -> t + t'

    Succ t - One     = t
    Succ t - Succ t' = t - t'
    _      - _       = error "undefined value for RelTime"

    fromInteger = genericIndex (iterate Succ One) . pred

    (*) = undefined
    abs = undefined
    signum = undefined

{- |
    @evalExpr sEnv tEnv eEnv e@ evaluates an expression @e@ given 

        [@sEnv@] the list of type synonyms,

        [@tEnv@] the list of global variables with their types, and

        [@eEnv@] the list of global variables with their expressions.
-}
evalExpr :: TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value
evalExpr = eval []

{- |
    Helper function for 'evalExpr'. @eval lEnv sEnv tEnv eEnv e@ evaluates an expression @e@
    given

        [@lEnv@] the list of local variables with their values,

        [@sEnv@] the list of type synonyms,

        [@tEnv@] the list of global variables with their types, and

        [@eEnv@] the list of global variables with their expressions.
-}
eval :: [(Var, Value)] -> TypeSynEnv -> TypeEnv -> EvalEnv -> Expr -> Value
eval lEnv sEnv tEnv eEnv expr = let eval' = eval lEnv sEnv tEnv eEnv in case expr of
    ExPair e1 e2 -> Pair (eval' e1) (eval' e2)
    ExNatLit i -> Natural i
    ExUnit -> Unit
    ExLeft -> Function $ \v -> ChoiceLeft v
    ExRight -> Function $ \v -> ChoiceRight v
    ExNull -> Function $ \_ -> error "eval: received value of type 0"
    ExFst -> Function $ \p -> case p of
                                  Pair l _ -> l
                                  _ -> error "eval: argument to ExFst not a pair"
    ExSnd -> Function $ \p -> case p of
                                  Pair _ r -> r
                                  _ -> error "eval: argument to ExSnd not a pair"
    ExCase -> Function $ \(Function l) -> Function $ \(Function r) -> Function $ \c -> case c of
        ChoiceLeft e -> l e
        ChoiceRight e -> r e
        _ -> error "third argument to case not left/right"

    ExVar (Var "add") -> withNat $ \i -> withNat $ \j -> Natural $ i + j
    ExVar (Var "mult") -> withNat $ \i -> withNat $ \j -> Natural $ i * j
    ExVar v -> case lookup v lEnv of
                   Just x -> x
                   Nothing -> maybe (error $ "eval: undefined var `" ++ show (SrcCode v) ++ "'")
                                  eval' $ lookup v eEnv

    ExLam v e -> Function (\x -> eval (replVar v x lEnv) sEnv tEnv eEnv e)
    ExApp f x -> case eval' f of
                     Function fun -> fun $ eval' x
                     _ -> error "eval: first argument to ExApp not a function"

    ExBehav f -> case eval' f of
                     Function f -> Behavior (f . Natural . fromTime)
                     _ -> error "first argument to ExBehav not a function"
    ExEvent t e -> case eval' t of
                       Natural i -> Event (fromInteger i) $ eval' e
                       _ -> error "first argument to ExEvent not a positive"
    ExNever -> Event infinite $ error "secret value of type 0"
    ExConst e -> Behavior $ \_ -> eval' e
    ExLiftAppB f b -> case (eval' f, eval' b) of
        (Behavior f, Behavior g) -> Behavior $ \t -> case f t of
            Function f -> f (g t)
            _ -> error "wrong argument type(s) to ExLiftAppB"
        _ -> error "wrong argument type(s) to ExLiftAppB"
    ExLiftAppE f e -> case (eval' f, eval' e) of
        (Behavior f, Event t v) -> Event t $ case f t of
            Function f -> f v
            _ -> error "wrong argument type(s) to ExLiftAppE"
        _ -> error "wrong argument type(s) to ExLiftAppE"
    ExRace -> Function $ \e1 -> case e1 of
        Event t1 v1 -> Function $ \e2 -> case e2 of
            Event t2 v2 -> Event (min t1 t2) $ case compare t1 t2 of
                LT -> ChoiceRight $ ChoiceLeft $ Pair v1 (Event (t2 - t1) v2)
                EQ -> ChoiceLeft $ Pair v1 v2
                GT -> ChoiceRight $ ChoiceRight $ Pair v2 (Event (t1 - t2) v1)
            _ -> error "second argument to ExRace not an event"
        _ -> error "first argument to ExRace not an event"
    ExExpand -> Function $ \e -> case e of
        Behavior f -> Behavior $ \t -> Pair (f t) (Behavior $ \t' -> f $ t + t')
        _ -> error "first argument to ExExpand not a behavior"
    ExPack _ -> Function id
    ExUnpack _ -> Function id
    ExReflect -> Function $ \v -> let nat 1 = ChoiceLeft Unit
                                      nat n = ChoiceRight $ nat (n-1)
                                  in case v of
                                         Natural n -> nat n
                                         _ -> error "eval: argument to ExReflect not a positive"

    -- fold :: (Functor shape) => (shape accu -> accu) -> Fix shape -> accu
    -- fold fun = fun . fmap (fold fun) . unFix
    ExFold mu f ->
        let Right (MuType var t) = expandMuType sEnv mu
            fold fun = fun . genmap CoVariant sEnv var t (fold fun)
        in case eval' f of
               Function fun -> Function $ fold fun
               _ -> error "eval: first argument to ExFold not a function"

    -- unfold :: (Functor shape) => (accu -> shape accu) -> accu -> Fix shape
    -- unfold fun = Fix . fmap (unfold fun) . fun
    ExUnfold nu f ->
        let Right (NuType var t) = expandNuType sEnv nu
            unfold fun = genmap CoVariant sEnv var t (unfold fun) . fun
        in case eval' f of
               Function fun -> Function $ unfold fun
               _ -> error "eval: first argument to ExUnfold not a function"

    ExUJump ->
        let jump e = case e of
                Event t v ->
                    let (t', v') = case v of
                                       ChoiceLeft v'  -> (One, v')
                                       ChoiceRight e' -> jump e'
                                       _ -> error "eval: inner argument to ExUJump not a choice"
                    in (t + t', v')
                _ -> error "eval: argument to ExUJump not an event"
        in Function $ \e -> let (Succ t, v) = jump e in Event t v

    ExUSwitch ->
        let switch p = case p of
                Pair (Behavior f) (Event t ~(Pair v p')) -> \t' -> case compare t' t of
                    LT -> f t'
                    EQ -> v
                    GT -> switch p' (t' - t)
                _ -> error "wrong argument type(s) to ExUSwitch"
        in Function $ \p -> let f = switch p in Behavior f


{- |
    @genmap var sEnv v t f@ generates a generic comap\/contramap function for a type @t@ that
    applies a function @f@ to values of a type @t@. If @var == CoVariant@ a comap function will be
    produced, a contramap function for @var == ContraVariant@, where @v@ is the type variable the
    map is generated for and @sEnv@ the list of type synonyms.
-}
genmap :: Variance -> TypeSynEnv -> Var -> Type -> (Value -> Value) -> Value -> Value
genmap var sEnv v t f = case t of
    TyZero -> id
    TyUnit -> id
    TyNat -> id

    TyBehav t -> \e -> case e of
        Behavior g -> Behavior $ genmap var sEnv v t f . g
        _ -> error "genmap: value of type TyBehav is not a behavior"
        
    TyEvent t -> \e -> case e of
        Event n e' -> Event n $ genmap var sEnv v t f e'
        _ -> error "genmap: value of type TyBehav is not a behavior"

    TyPair t1 t2 -> \e -> case e of
        Pair e1 e2 -> Pair (genmap var sEnv v t1 f e1) (genmap var sEnv v t2 f e2)
        _ -> error "genmap: value of type TyPair is not a pair"

    TyPlus t1 t2 -> \e -> case e of
        ChoiceLeft e'  -> ChoiceLeft $ genmap var sEnv v t1 f e'
        ChoiceRight e' -> ChoiceRight $ genmap var sEnv v t2 f e'
        _ -> error "genmap: value of type TyPlus is not a choice"

    TyFun t1 t2 -> \e -> case e of
{-
        -- comap f function = comap f . function . contramap f
        (Function g, CoVariant) -> Function $
            genmap CoVariant sEnv rEnv t2 . g . genmap ContraVariant sEnv rEnv t1
        -- contramap f function = contramap f . function . comap f
        (Function g, ContraVariant) -> Function $
            genmap ContraVariant sEnv rEnv t2 . g . genmap CoVariant sEnv rEnv t1
-}
        Function g -> Function $ genmap var sEnv v t2 f
                                 . g . genmap (invertVariance var) sEnv v t1 f
        _ -> error "genmap: value of type TyFun not a function"

    TyApp v' [] | v' == v -> f
    TyApp v' ts -> case expandTypeSyn sEnv v' ts of
                       Left _  -> id
                       Right t -> genmap var sEnv v t f

    TyMu (MuType v' t') ->
        -- TODO: TyUnit here assures we get the subtrees as they are. That is a type error but 
        --       shouldn't be a problem for evaluation (only if v is mapped to a type including v
        --       itself, which shouldn't happen). Should be thoroughly thought through, though :-)
        let temp = TyUnit
        in genmap var sEnv v (substVar v' temp t') f
           . genmap var sEnv v' t' (genmap var sEnv v t f)

    TyNu (NuType v' t') ->
        -- TODO: see above
        let temp = TyUnit
        in genmap var sEnv v (substVar v' temp t') f
           . genmap var sEnv v' t' (genmap var sEnv v t f)

    TyVar _ -> error "genmap: called with TyVar"
    TyCon _ -> error "genmap: called with TyCon"


withNat :: (Integer -> Value) -> Value
withNat f = Function $ \x -> case x of
    Natural n -> f n
    _ -> error "eval: function argument type mismatches expected type positive"

-- | @replVar v val@ adds a new variable @v@ with a value @var@ to a list of variable-value-pairs,
-- replacing the old value of @v@ if @v@ is already present.
replVar v v' = ((v, v') :) . filter ((/= v) . fst)