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

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

module Interp where

-- Interpreter in Sec 1.1, in SML and untyped

{-
datatype exp = B of int | V of string
              | L of string * exp | A of exp * exp
fun eval e env =
 case e of
   B i      =>  i
 | V s      =>  env s
 | L (s,e)  =>  fn v => eval e (ext env s v)
 | A (f,e)  =>  (eval f env) (eval e env)
-}

-- The following is the typed interpreter for the above
-- Actually, we almost literally implement the typing rules
-- from fig 1. Actually, we implement code from Fig 3, without
-- any need for dependent types.
-- As in Fig 1, the binders should have the type annotation

-- We use DeBruijn indices, denoted by the numerals
data Z   = Z deriving Show
data S a = S a deriving Show

-- Well-formedness constraint
class Nat n
instance Nat Z
instance Nat a => Nat (S a)


-- The language of type expressions, needed for type annotations, see Fig 1
data TInt = TInt
data TArr t1 t2 = TArr t1 t2
-- Well-formedness constraint
class Typ t
instance Typ TInt
instance (Typ t1, Typ t2) => Typ (TArr t1 t2)

newtype B        = B Int
newtype V v      = V v
data L typ exp   = L typ exp
data A e1 e2     = A e1 e2 

-- Well-formedness constraint
class Exp e
instance Exp B
instance Nat v => Exp (V v)
instance (Typ typ, Exp exp) => Exp (L typ exp)
instance (Exp e1, Exp e2) => Exp (A e1 e2)

-- The evaluator. The 'env' is the heterogeneous list of
-- variable values

data HNil = HNil deriving Show
data HCons a b = HCons a b deriving Show

class Typ t => TypEval t r | t -> r
instance TypEval TInt Int
instance (Typ t1, Typ t2, TypEval t1 r1, TypEval t2 r2) 
    => TypEval (TArr t1 t2) (r1->r2)

class Eval gamma exp result | gamma exp -> result where
    eval :: exp -> gamma -> result

instance Eval gamma B Int where  -- rule Nat in Fig 1
    eval (B i) _ = i

instance Eval (HCons v g) (V Z) v where -- rule Var in Fig 1
    eval _ (HCons v _) = v

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


-- rule Lam in Fig 1
instance (TypEval t tr, Eval (HCons tr g) e r) => Eval g (L t e) (tr->r) where 
    eval (L _ exp) g = \x -> eval exp (HCons x g)

-- rule App in Fig 1
instance (Eval g e1 (a->r), Eval g e2 a) => Eval g (A e1 e2) r where 
    eval (A e1 e2) g = (eval e1 g) (eval e2 g)


-- tests

test1 = eval (L TInt (B 1)) HNil

test2 = eval (A (L TInt (B 1)) (B 2)) HNil

test3 = eval (A (L TInt (V Z)) (B 2)) HNil

test4 = eval (L (TArr TInt TInt) (V Z)) HNil