{-# LANGUAGE QuasiQuotes, TypeFamilies, FlexibleInstances,
  MultiParamTypeClasses, GADTs, PatternGuards #-}

{-# OPTIONS_GHC -fcontext-stack=200 #-}

{- |

Module      :  Examples.TermTest
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

A denotational semantics for the simple-typed lambda calculus via
"Data.Yoko.Cata".

-}
module Examples.TermTest where

import Examples.TermBase
import qualified Examples.TermGeneric as G

import Type.Yoko
import Data.Yoko.Cata
import Data.Yoko


-- | Since our family of abstract data types don't correspond to the
-- object-language types, we need a tagged universal value space.
data Val = VBool Bool | VInt Int | VFun (Val -> Val)
instance Show Val where
  show (VBool b) = show b; show (VInt i) = show i; show (VFun _) = "<fun>"



eLam (G.Lam _ t) e = VFun $ t . (: e)
eVar (G.Var i) = (!! i)
eApp (G.App t1 t2) e
  | VFun f <- t1 e = f (t2 e)
  | otherwise = error "failed projection in reduce[App]"
eLet (G.Let ds t) = foldr cons t ds where cons (_, s) t e = t (s e : e)

eDecl (G.Decl ty t) = (ty, t)


-- | The semantic domain of the reduction.
type Sem = [Val] -> Val

-- | The recursion mediator for our denotation.
data SemM = SemM
type instance Med SemM Term = Sem
type instance Med SemM Decl = (Type, Sem)

instance AlgebraDT SemM Term where algebraDT = algebraFin
instance AlgebraDC SemM G.Lam where algebraDC = eLam
instance AlgebraDC SemM G.Var where algebraDC = eVar
instance AlgebraDC SemM G.App where algebraDC = eApp
instance AlgebraDC SemM G.Let where algebraDC = eLet

instance AlgebraDT SemM Decl where algebraDT = eDecl . uniqueRMN

-- | 'eval' will work for any family of mutually recursive types that all have
-- @'AlgebraDT' SemM@ instances.
eval x = ($ x) $ cata $ algebras [qP|SemM|]

eval'     x = ($ x) $ cata $ (algebraDT  .|. algebraDT :: SiblingAlgs Term SemM)
eval''    x = ($ x) $ cata $ (algebraDT  .|. algebraDT)
eval'''   x = ($ x) $ cata $ (algebraFin .|. algebraDT :: SiblingAlgs Term SemM)
eval''''  x = ($ x) $ cata $ (algebraFin .|. algebraDT)
eval''''' x = ($ x) $ cata $ (algebraDT  .|. (eDecl . uniqueRMN'))

--instance AlgebraDT SemM Decl where algebraDT = algebraFin
--instance AlgebraDC SemM G.Decl where algebraDC = eDecl
--eval''''' x = ($ x) $ cata $ (algebraFin .|. algebraFin :: SiblingAlgs Term SemM)





vSucc = VFun $ \(VInt i) -> VInt $ i + 1


ex0 = eval (Var 0) [VBool True]
ex1 = eval (Let [Decl (TInt `TArrow` TInt) $ Lam TInt (Var 0) `App` Var 0 `App` Var 1]
                (Var 0)) [vSucc, VInt 9]
ex2' = eval (Decl TInt (Var 0))
ex2 = snd ex2' [VInt 3]


--ex1' = eval' (Let [Decl (TInt `TArrow` TInt) (Var 0 `App` Var 1)]
--                (Var 0)) [vSucc, VInt 9]