content: {-# LANGUAGE
    GADTs,
    TemplateHaskell,
    MultiParamTypeClasses,
    FlexibleInstances,
    FlexibleContexts,
    UndecidableInstances,
    TypeOperators,
    ScopedTypeVariables,
    TypeSynonymInstances#-}
  
  module Multi.Functions.Comp.Eval where
  
  import Multi.DataTypes.Comp
  import Multi.Functions.Comp.Desugar
  import Data.Comp.Multi
  import Data.Comp.Multi.HEquality
  
  -- evaluation
  
  class Eval e v where
      evalAlg :: Alg e (Term v)
  
  eval :: (HFunctor e, Eval e v) => Term e :-> (Term v)
  eval = cata evalAlg
  
  instance (Eval f v, Eval g v) => Eval (f :++: g) v where
      evalAlg (HInl v) = evalAlg v
      evalAlg (HInr v) = evalAlg v
  
  instance (Value :<<: v) => Eval Value v where
      evalAlg = inject
  
  
  getInt :: (Value :<<: v) => Term v Int -> Int
  getInt t = case project t of
               Just (VInt x) -> x
               Nothing -> undefined
  getBool :: (Value :<<: v) => Term v Bool -> Bool
  getBool t = case project t of
               Just (VBool x) -> x
               Nothing -> undefined
  
  getPair :: (Value :<<: v) => Term v (s,t) -> ((Term v s), (Term v t))
  getPair t = case project t of
                Just (VPair x y) -> (x, y)
                Nothing -> undefined
  
  
  instance (Value :<<: v, HEqF v) => Eval Op v where
      evalAlg (Plus x y) = iVInt $ getInt x + getInt y
      evalAlg (Mult x y) = iVInt $ getInt x * getInt y
      evalAlg (If b x y) = if getBool b then x else y
      evalAlg (Eq x y) = iVBool $ x == y
      evalAlg (Lt x y) = iVBool $ getInt x < getInt y
      evalAlg (And x y) = iVBool $ getBool x && getBool y
      evalAlg (Not x) = iVBool $ not $ getBool x
      evalAlg (ProjLeft x) = fst $ getPair x
      evalAlg (ProjRight x) = snd $ getPair x
  
  instance (Value :<<: v) => Eval Sugar v where
      evalAlg (Neg x) = iVInt $ negate $ getInt x
      evalAlg (Minus x y) = iVInt $ getInt x - getInt y
      evalAlg (Gt x y) = iVBool $ getInt x > getInt y
      evalAlg (Or x y) = iVBool $ getBool x || getBool y
      evalAlg (Impl x y) = iVBool $ not (getBool x) || getBool y
  
  desugarEval :: SugarExpr :-> ValueExpr
  desugarEval = eval . (desugar :: SugarExpr :-> Expr)
  
  evalSugar :: SugarExpr :-> ValueExpr
  evalSugar = eval
  
  desugarEvalAlg  :: Alg SugarSig ValueExpr
  desugarEvalAlg = evalAlg  `compAlg` (desugarAlg :: Hom SugarSig ExprSig)
  
  desugarEval' :: SugarExpr :-> ValueExpr
  desugarEval' e = cata desugarEvalAlg e