yoko-0.1: Examples/TermTest.hs

{-# 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.Algebra".

-}
module Examples.TermTest where

import Examples.TermBase
import qualified Examples.TermGeneric as G

import Type.Yoko
import Data.Yoko.Algebra


-- | 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 ReduceDC SemM G.Lam where reduceDC = eLam
instance ReduceDC SemM G.Var where reduceDC = eVar
instance ReduceDC SemM G.App where reduceDC = eApp
instance ReduceDC SemM G.Let where reduceDC = eLet

instance ReduceDC SemM G.Decl where reduceDC = eDecl

eval x = ($ x) $ cata $ algebras [qP|SemM|]

-- NB equivalent
eval' x = ($ x) $ cata $ (reduce .|. reduce) -- :: AlgebraFam 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]