module TestTypeHelpers where

import TypeHelpers
import Environments
import Subst
import TypeAttributes

data Syntax = Expr LambdaExp

instance Annotatable Syntax where
  annotate pi (Expr e) =
    case annotate pi e of
      (Tree_Subst (e:::a) substl) -> (Tree_Subst (Expr e ::: a) substl)

instance Show Syntax where
   showsPrec p (Expr e) = showsPrec p e

data LambdaExp = Varref String | Call LambdaExp LambdaExp | Lambda String LambdaExp
     deriving (Eq, Show)

t0, t1, t2, t3, t4, t5 :: LogicalVar
t0 = (0, "t0")
t1 = (0, "t1")
t2 = (0, "t2")
t3 = (0, "t3")
t4 = (0, "t4")
t5 = (0, "t5")

instance Annotatable LambdaExp where
  annotate pi e@(Varref x) =
      ruleIf nohyp                       (\_ -> x `elem` (dom pi))
                                         (\_ -> (t0 ->- justApply pi x))
           ---------------------------
           (pi :- e ::: (Avar t0))
              where nohyp :: [Judgement
                               (AttribTree LambdaExp PrimitiveAttrib)]
                    nohyp = []

  annotate pi e@(Call e1 e2) =
      rule [pi :- e1 ::: (Avar t1 :-> Avar t2),
            pi :- e2 ::: (Avar t1)]
           ---------------------------------------
          (pi :- e ::: Avar t2)

  annotate pi e@(Lambda formal body) =
      rule [update pi formal (Avar t3) :- body ::: Avar t4 ]
           ---------------------------------------
          (pi :- e ::: (Avar t3 :-> Avar t4))

justApply pi i =
   case applyEnv pi i of
     (Just theta) -> theta
     Nothing -> Aerr

test1 = annotate (update emptyEnv "add1" (Aint :-> Aint))
                 (Lambda "x" (Call (Varref "add1") (Varref "x")))

go :: IO()
go = do putStrLn (show test1)