{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}

-- Tagless Staged interpreter
-- `Tagless Staged Interpreters for Typed Languages'
-- Pasalic, Taha, Sheard: ICFP02.

module Staged where

import Language.Haskell.TH hiding (Exp)
import qualified Language.Haskell.TH as TH (Exp)
import Language.Haskell.TH.Ppr
import Interp

-- Typed Expressions (standard TH expressions are untyped!)

newtype TE t = TE (Q TH.Exp)
unTE (TE x) = x

-- builders
bint :: Int -> TE Int
bint = TE . litE . intPrimL . fromIntegral

bapp :: TE (a->b) -> TE a -> TE b
bapp (TE c1) (TE c2) = TE (appE c1 c2)

blam :: a -> Name -> TE b -> TE (a->b)
blam _ name (TE c) = TE (lamE [varP name] c)

bvar :: a -> Name -> TE a
bvar _ name = TE (varE name)

-- Staged evaluator

class SEval gamma exp result | gamma exp -> result where
    seval :: exp -> gamma -> TE result

instance SEval gamma B Int where  -- rule Nat in Fig 1
    seval (B i) _ = bint i

instance SEval (HCons (TE v) g) (V Z) v where -- rule Var in Fig 1
    seval _ (HCons v _) = v

-- rule Weak in Fig 1
instance SEval g (V n) r => SEval (HCons v g) (V (S n)) r where 
    seval (V (S n)) (HCons _ g) = seval (V n) g

-- rule Lam in Fig 1
instance (TypEval t tr, SEval (HCons (TE tr) g) e r)
    => SEval g (L t e) (tr->r) where 
    seval (L _ exp) g = TE (do
                             x <- newName "x"
                             let v = bvar (undefined::tr) x
                             let b = seval exp (HCons v g)
                             unTE $ blam (undefined::tr) x b
                           )
                            
-- rule App in Fig 1
instance (SEval g e1 (a->r), SEval g e2 a) => SEval g (A e1 e2) r where 
    seval (A e1 e2) g = bapp (seval e1 g) (seval e2 g)



-- Show the code expression
show_code cde = runQ cde >>= putStrLn . pprint

ttest1 = show_code (litE (intPrimL 1))

ttest2 = show_code $ do
                     x <- newName "x"
                     lamE [varP x] (varE x)
                      

show_tcode (TE c) = show_code c


stest1 = show_tcode $ seval (L TInt (B 1)) HNil

stest2 = show_tcode $ seval (A (L TInt (B 1)) (B 2)) HNil

stest3 = show_tcode $ seval (A (L TInt (V Z)) (B 2)) HNil

stest4 = show_tcode $ seval (L (TArr TInt TInt) (V Z)) HNil