{-# 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 _) = "" 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]