{-# LINE 21 "SLEvaluate.lag" #-}
{
import UU.Pretty
}
{
data Value           =  UnitVal
                          |  BoolVal Bool
                          |  IntVal Int
                          |  Function (Value -> Value)
                          |  ViolationPre String
                          |  ViolationPost String
type Env             =  [(String,Value)]
type EnvTransformer  =  Env -> Env
type Computation     =  Env -> (NewVal,Env)
type NewVal          =  (Value,PP_Doc)

instance Show Value where
  show  UnitVal        =  "()"
  show  (BoolVal b)    =  show b
  show  (IntVal i)     =  show i
  show  (Function _)   =  "<! Function value !>"
  show  (ViolationPre s)  =  "Violation: precondition " ++ s 
  show  (ViolationPost s)  =  "Violation: postcondition " ++ s 
}

ATTR Root [  |  | val : NewVal]
SEM Root
  | Root lhs.val          = computeNewVal  @expr.comp []


ATTR Expr [  |  | comp : Computation]
SEM Expr
  | Unit        lhs.comp  = \env ->  ((UnitVal,text "()"),env)
  | Intexpr     lhs.comp  = \env ->  ((IntVal  @int, text $ show  @int), env)
  | Boolexpr    lhs.comp  = \env ->  ((BoolVal  @bool,text $ show  @bool),env)
  | Ident       lhs.comp  = \env ->  ((lookupValue  @var env,text  @var >|<  @errmsg), env)
  | Op          lhs.comp  = \env ->  let  (lVal,lpp) =  computeNewVal  @le.comp env
                                          (rVal,rpp) =  computeNewVal  @re.comp env
                                     in ((evalOp  @op (lVal,rVal),lpp >#<  @lerr >#< text  @op >#<  @rerr >#<  rpp), env)
  | If          lhs.comp  = \env ->  let  (condVal,condpp)  = computeNewVal  @cond.comp env 
                                          (thenVal,thenpp)  = computeNewVal  @thenExpr.comp env
                                          (elseVal,elsepp)  = computeNewVal  @elseExpr.comp env
                                     in ((evalIf condVal thenVal elseVal,pp_ite "if " " then " " else " " fi"
                                              (condpp >|<  @condErr)  (thenpp) (elsepp >|<  @ifErr)   ), env)
  | Let         lhs.comp  = \env ->  let ((l,lpp),r) = @expr.comp (@decls.envTransformer env) 
                                     in ((l,text  "let" >|< pp_block "" "" "; "  (map (\x -> snd (fst (x env))) @decls.pps)
                                            >-< " in" >#< lpp
                                            >-< " ni"),r)
  | Assign      lhs.comp  = \env ->  let ((val,valpp),_) =  @expr.comp env
                                     in ((UnitVal,text  @var >|<  @varErr >#< text ":=" >#<  valpp >|<  @exprErr), (@var,val) : env)
  | Apply       lhs.comp  = \env ->  let (funcVal,funcpp)  = computeNewVal  @func.comp env
                                         (argVal,argpp)   = computeNewVal  @arg.comp env
                                         res = evalApply funcVal argVal
                                     in ((res
                                         ,case res of
                                            ViolationPre t ->   pp_parens (funcpp >|<  @funcErr) >#< 
                                                                pp_parens (argpp >|<  text "!!argument!!") 
                                            ViolationPost t -> pp_parens (funcpp >|<  text "!!function!!") >#< 
                                                                pp_parens (argpp >|<  @argErr)
                                            otherwise  -> pp_parens (funcpp >|<  @funcErr) >#< 
                                                                pp_parens (argpp >|<  @argErr)), env)
  | Lam         lhs.comp  = \env ->  ((Function (\v -> let extend_env  = ((@var,v):env)
                                                           (precond,precondpp)     = computeNewVal @pre.comp extend_env
                                                           (val,valpp)         = computeNewVal @expr.comp extend_env
                                                           (postcond,postcondpp)    = computeNewVal @post.comp ((@postvar,val):env)
                                                       in case precond of
                                                            BoolVal True -> case postcond of
                                                                              BoolVal True -> val
                                                                              otherwise    -> ViolationPost @postmess
                                                            otherwise    -> ViolationPre @premess),text "\\" >#<  text @var >|<  @argErr >#< text "->" >#<  snd (computeNewVal @expr.comp env) >|<  @bodyErr), env) 
  | Seq         lhs.comp  = \env -> let ((l,lpp),r) = @exprs.comp env in ((l,lpp),r)
    
ATTR Exprs [  |  | comp : Computation null : Bool ] 
SEM Exprs 
  | Nil   lhs.comp        = \env ->  ((UnitVal, text "()"),env)
          lhs.null        = True
  | Cons  lhs.comp        = \env ->  let (val,env') = @hd.comp env 
                                     in  if  @tl.null 
                                         then (val,env') 
                                         else  @tl.comp env'
          lhs.null        = False

ATTR Decls [  |  | envTransformer : EnvTransformer pps : {[Computation]}]
SEM Decls
  | Nil   lhs.envTransformer  =  id
          lhs.pps   =  []
  | Cons  lhs.envTransformer  =  \env ->  @tl.envTransformer (@hd.envTransformer env)
          lhs.pps   =  @hd.comp :  @tl.pps
         
ATTR Decl [  |  | envTransformer : EnvTransformer comp : Computation]
SEM Decl
  | Decl  lhs.envTransformer  =  \env -> (@var, computeVal  @expr.comp env) : env
          loc.ppTp  =  if isAnnotated  @type 
                           then text "::" >#< show  @type 
                           else text "::" >#< show  @inferredType
          lhs.comp = \env -> ((UnitVal,text  @var >#<  @ppTp >|<  @declErr >#< text "=" >#<  snd (computeNewVal @expr.comp env)),env)



{
computeVal :: (Env -> ((Value,PP_Doc),Env)) -> Env -> Value
computeVal comp env = fst (fst (comp env))

computeNewVal comp env = (fst (comp env))

lookupValue :: String -> Env -> Value
lookupValue v env = maybe (lookUpError v) id (lookup v env)

evalOp :: String -> (Value,Value) -> Value
evalOp op vals  = 
  case op of
    "&&"  -> evalLogicalOp (&&) "&&" vals
    "||"  -> evalLogicalOp (||) "||" vals
    "=="  -> evalRelOp (==) "==" vals
    "/="  -> evalRelOp (/=) "/=" vals
    ">="  -> evalRelOp (>=) ">=" vals
    "<="  -> evalRelOp (<=) "<=" vals
    "<"   -> evalRelOp (<) "<" vals
    ">"   -> evalRelOp (>) ">" vals
    "+"   -> evalIntOp (+) "+" vals
    "-"   -> evalIntOp (-) "-" vals
    "*"   -> evalIntOp (*) "*" vals
    "/"   -> evalIntOp div "/" vals
    
evalLogicalOp :: (Bool -> Bool -> Bool) -> String -> (Value,Value) -> Value
evalLogicalOp op opString (lVal,rVal) =
  case (lVal,rVal) of
    (BoolVal b1, BoolVal b2)  -> BoolVal (b1 `op` b2)
    _                         -> opError opString  

evalRelOp :: (Int -> Int -> Bool) -> String -> (Value,Value) -> Value
evalRelOp op opString (lVal,rVal) = 
  case (lVal,rVal) of
    (IntVal n, IntVal m)  -> BoolVal (n `op` m)
    _                     -> opError opString

evalIntOp :: (Int -> Int -> Int) -> String -> (Value,Value) -> Value
evalIntOp op opString (lVal,rVal) = 
  case (lVal,rVal) of
    (IntVal n, IntVal m)  -> IntVal (n `op` m)
    _                     -> opError opString

evalIf :: Value -> Value -> Value -> Value
evalIf cond thenVal elseVal =
  case cond of
    (BoolVal True)   -> thenVal
    (BoolVal False)  -> elseVal
    _                -> ifCondError

evalApply :: Value -> Value -> Value
evalApply funcVal argVal =
  case funcVal of
    Function f  -> f argVal
    _           -> applyError

lookUpError v  =  error $ 
                    "The variable " ++ v ++ " is unbound."
opError x      =  error $ 
                    "The operator " ++ x ++ " is applied to arguments of the wrong type."
ifCondError    =  error $ 
                    "A non-boolean value occurred in the condition of an if statement."
applyError     =  error $ 
                    "A non-function value occurs on the left hand side of an application."
}