-- ##### An Interpreter and Type Checker for the infamous X-Lang #####
-- ###################################################################

-- x-Lang Abstract Syntax (objects not involved)
type Name	= String
data Unop       = UO_neg | UO_not
                deriving (Show, Read, Eq)
data BinOp      = BO_plus
                | BO_minus
                | BO_div
                | BO_times
                | BO_mod
                | BO_and
                | BO_or
                | BO_lt
                | BO_gt
                | BO_leq
                | BO_geq
                | BO_eq
                | BO_neq
                | BO_next
                deriving (Show, Read, Eq)
data Mode       = ByName | ByVal
                deriving (Show, Read, Eq)
data Data       = IntData | BoolData | Fun(Type, Type)
                deriving (Show, Read, Eq)
data Type       = ExpType(Data) | VarType(Data) 
                deriving (Show, Read, Eq)
newtype Var = Var String
  deriving (Eq,Show,Read)
data Expression = Eint(Int)                     -- integers
                | TrueC                         -- true constant
                | FalseC                        -- false constant
                | Eid(Var)                      -- identifiers
                | Eunop(Unop, Expression)
                | Ebinop(Expression, BinOp, Expression)
                | Enext(Expression, Expression)
                | Eif(Expression, Expression, Expression)
                | Evar(Var, Data, Expression)
                | Ederef(Var)
                | Eassign(Expression, Expression)
                | Elambda(Mode, Var, Type, Expression)
                | Eapp(Expression, Expression)
                | Erec(Expression)
                | (Expression)
                deriving (Show, Read, Eq) 

-- Types Environment        
type TypeEnv    = [(Var, Type)]

lookupTEnv :: Var -> TypeEnv -> Type
lookupTEnv (Var x) []   = error "not found!\n"
lookupTEnv (Var x) tenv@(hl:tl) = let (Var z, t) = hl 
                              in if (z == x) then
                                     t 
                                 else
                                     lookupTEnv (Var x) tl
-- Syntactic Sugar
eApplyMany :: Expression -> [Expression] -> Expression
eApplyMany e [] = e
eApplyMany e list@(h:t) = eApplyMany (Eapp(e,h)) t

eNextMany :: [Expression] -> Expression
eNextMany []  = error "pathetic!\n"
eNextMany [a] = a
eNextMany list@(h:t) = Ebinop(h, BO_next, eNextMany t)

-- TypeChecking 
typeOf :: TypeEnv -> Expression -> Type
-- Constant Expressions
typeOf tenv (Eint(i))   = ExpType(IntData)
typeOf tenv TrueC       = ExpType(BoolData)
typeOf tenv FalseC      = ExpType(BoolData)
-- unary operators
typeOf tenv (Eunop(UO_neg, e)) = 
                let t = typeOf tenv e 
                in case t of
                    ExpType(IntData) -> ExpType(IntData)
                    _                -> error "Non-int expression!\n"
typeOf tenv (Eunop(UO_not, e)) = 
                let t = typeOf tenv e 
                in case t of
                    ExpType(BoolData) -> ExpType(IntData)
                    _                 -> error "Non-bool expression!\n"
-- binary operators
typeOf tenv (Ebinop(e1, BO_plus, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(IntData)
                            _ -> error "Not int exression\n"
                        _ -> error "Not int expression\n"                    
                
typeOf tenv (Ebinop(e1, BO_minus, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(IntData)
                            _ -> error "Not int exression\n"
                        _ -> error "Not int expression\n"                    

typeOf tenv (Ebinop(e1, BO_div, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(IntData)
                            _ -> error "Not int exression\n"
                        _ -> error "Not int expression\n"                    

typeOf tenv (Ebinop(e1, BO_mod, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(IntData)
                            _ -> error "Not int exression\n"
                        _ -> error "Not int expression\n"                    

typeOf tenv (Ebinop(e1, BO_times, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(IntData)
                            _ -> error "Not int exression\n"
                        _ -> error "Not int expression\n"                    

typeOf tenv (Ebinop(e1, BO_and, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(BoolData) -> 
                          case t2 of
                            ExpType(BoolData) -> ExpType(BoolData)
                            _ -> error "Not bool exression\n"
                        _ -> error "Not bool expression\n"                    

typeOf tenv (Ebinop(e1, BO_or, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(BoolData) -> 
                          case t2 of
                            ExpType(BoolData) -> ExpType(BoolData)
                            _ -> error "Not bool exression\n"
                        _ -> error "Not bool expression\n"                    

typeOf tenv (Ebinop(e1, BO_eq, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(d) -> 
                          case t2 of
                            ExpType(d) -> ExpType(BoolData)
                            _ -> error "Not same expressions\n"
                        _ -> error "Not same expressions\n"                    

typeOf tenv (Ebinop(e1, BO_neq, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(d) -> 
                          case t2 of
                            ExpType(d) -> ExpType(BoolData)
                            _ -> error "Not same expressions\n"
                        _ -> error "Not same expressions\n"                    

typeOf tenv (Ebinop(e1, BO_next, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(d) -> 
                          case t2 of
                            ExpType(d') -> ExpType(d')
                            _ -> error "Not expression\n"
                        _ -> error "Not expression\n"                    

typeOf tenv (Ebinop(e1, BO_leq, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(BoolData)
                            _ -> error "Not int expression\n"
                        _ -> error "Not int expression\n"                    
typeOf tenv (Ebinop(e1, BO_lt, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(BoolData)
                            _ -> error "Not int expression\n"
                        _ -> error "Not int expression\n"                    
typeOf tenv (Ebinop(e1, BO_gt, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(BoolData)
                            _ -> error "Not int expression\n"
                        _ -> error "Not int expression\n"                    
typeOf tenv (Ebinop(e1, BO_geq, e2)) = 
                let t1 = typeOf tenv e1
                    t2 = typeOf tenv e2  
                in case t1 of 
                        ExpType(IntData) -> 
                          case t2 of
                            ExpType(IntData) -> ExpType(BoolData)
                            _ -> error "Not int expression\n"
                        _ -> error "Not int expression\n"                    

typeOf tenv (Eid(Var x)) = lookupTEnv (Var x) tenv

typeOf tenv (Ederef(Var x)) = let t = typeOf tenv (Eid(Var x))
                              in case t of 
                                  VarType(t') -> ExpType(t')
                                  _ -> error "cannod deref non-var types!\n"    

typeOf tenv (Evar(Var x, t, e)) = typeOf ((Var x, VarType(t)):tenv) e

typeOf tenv (Eassign(i, e)) = 
                let ti = typeOf tenv i 
                in case ti of 
                     VarType(t) -> let te = typeOf tenv e
                                   in case te of
                                       ExpType(t) -> te
                                       _ -> error "not expression\n"
                     _ -> error "l-value not var type\n"

typeOf tenv (Eif(e, x0, x1)) = 
        let te = typeOf tenv e 
            t0 = typeOf tenv x0
            t1 = typeOf tenv x1
        in case te of
            ExpType(BoolData) -> 
              if (t0 == t1) then
                t0
              else error "non same types\n"
            _ -> error "non boolean condition\n"

typeOf tenv (Elambda(m, Var x, t, e)) = 
        let te = typeOf ((Var x, t):tenv) e 
        in ExpType(Fun(t, te))

typeOf tenv (Eapp(a, b)) = 
        let ta = typeOf tenv a 
            tb = typeOf tenv b
        in case ta of
             ExpType(Fun(tb,t')) -> t'
             _ -> error "application to non-function type\n"

typeOf tenv (Erec(e)) = 
        let te = typeOf tenv e
        in case te of 
            ExpType(Fun(t,t')) -> if (t==t') then t else error "!!!\n"
            _ -> error "non proper rec application\n"
              

findType :: Expression -> Type
findType exp = typeOf [] exp

-- Interpreter 
-- ###################################################################

type Location = Int
-- these will be the contents of state
data LiftedValue = LvInt(Int) 
                 | LvBool(Bool)
                 -- and functions from computations to computations
                 | LvFunc(EnvContent -> EnvContent)
                 | LvUnused
--        deriving (Eq, Read)
-- looking up in state returns StateResults:
-- these are either lifted values, or Nothing
data StateResult = Sr(LiftedValue) | NotFound
--        deriving (Eq, Read)

-- state is a function from locations to StateResults
type StateType = Location -> StateResult


-- Computations are functions from states to new states and results
type Epsilon d = StateType -> (d, StateType)

-- EnvContent contains computations on locations or lifted values
type EnvContent = Epsilon EnvInside
data EnvInside = Eiloc(Location) | Eival(LiftedValue)
--        deriving (Eq, Read)

-- environment is a map from vars to EnvContents
type Env = [(Var, EnvContent)]
getFromEnv :: Var -> Env -> EnvContent
getFromEnv (Var x) [] = error "Not found!\n"
getFromEnv (Var x) env@(hx:tx) = 
        case hx of
          (Var s, m) -> 
            if (s == x) then 
              m 
            else getFromEnv (Var x) tx

addToEnv :: Env -> Var -> EnvContent -> Env
addToEnv env v el = (v, el):env

newLoc :: StateType -> Location
newLoc st = let f :: Int -> Int
                f x = case (st x) of 
                       NotFound -> x
                       _  -> f (x+1)
            in f 0

state :: Location -> StateResult
state loc = NotFound
stateUpdate :: Location -> 
                LiftedValue -> 
                  (Location -> StateResult) ->
                     (Location -> StateResult)

stateUpdate loc val prevstate = 
        \q -> if (q == loc) then 
                  Sr(val)
              else 
                  prevstate q


{-- main interpreter ---}
interp :: Expression -> Env -> EnvContent
interp (Eint(i)) u s      = (Eival(LvInt(i)),s)
interp TrueC u s          = (Eival(LvBool(True)),s)
interp FalseC u s         = (Eival(LvBool(False)),s)
interp (Eid(Var x)) u s   = (getFromEnv (Var x) u) s

interp (Eunop(UO_neg, e)) u s = 
                let (r,s') = (interp e u s)
                in case r of 
                    (Eival(LvInt(i))) ->(Eival(LvInt(-i)), s')
                    _ -> error "not good!\n"

interp (Eunop(UO_not, e)) u s = 
                let (r,s') = (interp e u s)
                in case r of 
                    (Eival(LvBool(b))) ->(Eival(LvBool(not b)), s')
                    _ -> error "not good!\n"

interp (Ebinop(e1, BO_plus, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvInt(i1+i2)), s'')
                               
interp (Ebinop(e1, BO_minus, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvInt(i1-i2)), s'')
interp (Ebinop(e1, BO_times, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvInt(i1*i2)), s'')
interp (Ebinop(e1, BO_div, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvInt(i1 `div` i2)), s'')
interp (Ebinop(e1, BO_mod, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvInt(i1 `mod` i2)), s'')

interp (Ebinop(e1, BO_and, e2)) u s = 
                let (Eival(LvBool(b1)), s')  = (interp e1 u s)
                in if not b1 then 
                    (Eival(LvBool(b1)), s')
                   else 
                    let (Eival(LvBool(b2)), s'') = (interp e2 u s')
                    in (Eival(LvBool(b1 && b2)), s'')

interp (Ebinop(e1, BO_or, e2)) u s = 
                let (Eival(LvBool(b1)), s')  = (interp e1 u s)
                in if (b1) then
                     (Eival(LvBool(b1)), s') 
                   else 
                    let (Eival(LvBool(b2)), s'') = (interp e2 u s')
                    in (Eival(LvBool(b1 || b2)), s'')

interp (Ebinop(e1, BO_eq, e2)) u s = 
                case (interp e1 u s) of 
                    (Eival(LvBool(v1)), s')  -> 
                            let (Eival(LvBool(v2)), s'') = (interp e2 u s')
                            in (Eival(LvBool(v1 == v2)), s'')
                    
                    (Eival(LvInt(v1)), s')   ->
                            let (Eival(LvInt(v2)), s'') = (interp e2 u s')
                            in (Eival(LvBool(v1 == v2)), s'')
                    _ -> error "not ok!\n"

interp (Ebinop(e1, BO_neq, e2)) u s = 
                case (interp e1 u s) of 
                    (Eival(LvBool(v1)), s')  -> 
                            let (Eival(LvBool(v2)), s'') = (interp e2 u s')
                            in (Eival(LvBool(v1 /= v2)), s'')
                    
                    (Eival(LvInt(v1)), s')   ->
                            let (Eival(LvInt(v2)), s'') = (interp e2 u s')
                            in (Eival(LvBool(v1 /= v2)), s'')
                    _ -> error "not ok!\n"

interp (Ebinop(e1, BO_lt, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvBool(i1 < i2)), s'')
interp (Ebinop(e1, BO_gt, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvBool(i1 > i2)), s'')
interp (Ebinop(e1, BO_geq, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvBool(i1 >= i2)), s'')
interp (Ebinop(e1, BO_leq, e2)) u s = 
                let (Eival(LvInt(i1)), s')  = (interp e1 u s)
                    (Eival(LvInt(i2)), s'') = (interp e2 u s')
                in 
                    (Eival(LvBool(i1 <= i2)), s'')
interp (Ebinop(e1, BO_next, e2)) u s = 
                let (r, s') = interp e1 u s 
                in interp e2 u s'

interp (Eif(b, e1, e2)) u s = 
                let (Eival(LvBool(b')), s') = interp b u s
                in if b' then
                        interp e1 u s'
                   else 
                        interp e2 u s'

interp (Eassign(v, e)) u s = 
                let (Eiloc(l),s') = interp v u s 
                    (Eival(r), s'') = interp e u s'
                    s''' = stateUpdate l r s''
                in (Eival(r), s''')

interp (Evar(i,t,e)) u s = 
                let l = newLoc s
                    (v,s') = interp e (addToEnv u i 
                                        (\s->(Eiloc(l),s)))
                                        (stateUpdate l LvUnused s)
                in (v, stateUpdate l LvUnused s')

interp (Ederef(v)) u s = 
                let (Eiloc(l),s') = interp (Eid(v)) u s 
                    (Sr(lv)) = s' l
                in case lv of 
                     LvUnused -> error "oops! I have a bug!\n"
                     _ -> (Eival(lv), s')

interp (Elambda(ByName, Var x, t, e)) u s = 
                let f = \d -> interp e (addToEnv u (Var x) d)
                in (Eival(LvFunc(f)), s)

interp (Elambda(ByVal, Var x, t, e)) u s = 
                let f = \d -> \s0 ->
                           -- first evaluate the d argument
                           let (v, s') = d s0
                           -- now see what it was (by val/by ref)
                               f' = \s -> (v, s)
                           in interp e (addToEnv u (Var x) f') s'
                in (Eival(LvFunc(f)), s)

interp (Eapp(e, e')) u s = let (Eival(LvFunc(f)), s') = interp e u s  
                           in f (interp e' u) s'

-- this will type well!!! 
interp (Erec(e)) u s = let fix h = h (fix h) 
                           (Eival(LvFunc(f)), s') = interp e u s
                       in  (fix f) s'

-- this is another way of doing it!!!!!
-- interp (Erec(e)) u s = interp (Eapp(e, Erec(e))) u s

-- no need no more!
--interp _ _ s = (Eival(LvInt(0)),s)                                

interpStrip :: Expression -> Env -> EnvInside
interpStrip e u = let (r, s) = interp e u state 
                  in r

data ResultType = ResultTypeInt(Int) 
                | ResultTypeBool(Bool)
                | ResultTypeFunc(String)
                deriving (Show, Eq, Read)

interpBigStep :: Expression -> ResultType
interpBigStep e = case interpStrip e [] of
                    Eival(LvInt(i)) -> ResultTypeInt(i)
                    Eival(LvBool(b)) -> ResultTypeBool(b)
                    Eival(LvFunc(f)) -> ResultTypeFunc("function")
                    _ -> error "nothing else ...\n"

{------------- sample function application  ---------------------}
sample = (Evar(Var "i", IntData, 
                   eNextMany [
                       Eassign(Eid(Var "i"), Eint(7)), 
                       Eapp(
                        Elambda(ByVal, Var "x", ExpType(IntData), 
                          Eif(
                            Ebinop(Eid(Var "x"), BO_eq, Eint(0)), 
                            Eunop(UO_neg, Ederef(Var "i")),
                            Eassign(Eid(Var "i"), Eid(Var "x"))
                          )
                        ),
                        Eint(0)
                       )]))

{------------ factorial recursive function ----------------------}
fact = (Eapp(Erec(
   Elambda(ByVal, Var "f", ExpType(Fun(ExpType(IntData),
   ExpType(IntData))),      
          Elambda(ByVal, Var "n", ExpType(IntData),     
                      Eif(Ebinop(Eid(Var "n"), BO_eq, Eint(0)),
                      Eint(1), Ebinop(Eid(Var "n"), BO_times,
                      Eapp(Eid(Var "f"), Ebinop(Eid(Var "n"),
                      BO_minus, Eint(1)))))))), Eint(5)))

{--------- da ultimet test 4g4inst 4ll richiz -----------------}
-- i.   lazy  call by value:
--      f2 = lambda ! x : exp[int] . x + x
--      n:=0; f1(n:=n+1;1);n    === 2
f2 = Elambda(ByName, Var "x", ExpType(IntData), 
           Ebinop(Eid(Var "x"), BO_plus, Eid(Var "x")))
-- ii.  eager call by value
--      f1 = lambda x : exp[int] . x + x
--      n:=0; f2(n:=n+1;1);n    === 1
f1 = Elambda(ByVal, Var "x", ExpType(IntData), 
           Ebinop(Eid(Var "x"), BO_plus, Eid(Var "x")))
-- iii. lazy  call by reference
--      f4 = lambda ! x : var[int] . x:= x + 1
--      n:=0; f3(n:=n+1;n);n    === 3
f4 = Elambda(ByName, Var "x", VarType(IntData), 
           Eassign(Eid(Var "x"), 
                  Ebinop(Ederef(Var "x"), BO_plus, Eint(1))))
-- iv.  eager call by reference
--      f3 = lambda x : var[int] . x:= x + 1
--      n:=0; f4(n:=n+1;n);n    === 2
f3 = Elambda(ByVal, Var "x", VarType(IntData), 
           Eassign(Eid(Var "x"), 
                   Ebinop(Ederef(Var "x"), BO_plus, Eint(1))))

codepiece1 f = Evar(Var "n", IntData, 
          eNextMany [Eassign(Eid(Var "n"), Eint(0)), 
                     Eapp(f, Ebinop(Eassign(Eid(Var "n"),
                     Ebinop(Ederef(Var "n"), BO_plus,Eint(1))),BO_next, Eint(1))),
                     Ederef(Var "n")
                    ])
codepiece2 f = Evar(Var "n", IntData, 
          eNextMany [Eassign(Eid(Var "n"), Eint(0)), 
                     Eapp(f, eNextMany [Eassign(Eid(Var "n"),
                     Ebinop(Ederef(Var "n"), BO_plus,Eint(1))),Eid(Var "n")]),
                     Ederef(Var "n")
                    ])

main :: IO ()
main =  print (interpBigStep sample)