Semantics (Subtyping)

91 views Asked by At

I am trying to bring the following grammar into the Haskell language :

data Expr
  = Var String
  | Bool Bool
  | Int Int
  | Float Float
  | BinaryOp Op Expr Expr
  | UnaryOp UnaryOp Expr
  | App Expr Expr
  | If Expr Expr Expr
  | Let String Expr Expr
  | Lambda String Type Expr
  | Record [(String, Expr)]
  | Prj String Expr
  | Pair Expr Expr
  | Fst Expr
  | Snd Expr
  | Inl Type Expr
  | Inr Type Expr
  | Case Expr String Expr String Expr
  deriving (Show, Eq)

data UnaryOp = Negate | Not | Pot | Sqrt deriving (Show, Eq)

data Op
  = ArithOp ArithOp
  | CompOp CompOp
  | LogicalOp LogicalOp
  deriving (Show, Eq)

data ArithOp = Plus | Times | Minus | Div | Mod deriving (Show, Eq)

data CompOp = Eq | Lt | Gt | Leq | Geq deriving (Show, Eq)

data LogicalOp = And | Or deriving (Show, Eq)

And roughly speaking I have the evalStep function that does a single evaluation step anxiously:

-- Function to perform one evaluation step.
evalStep :: Expr -> Expr
-- Evaluation of integer expressions (Int).
evalStep (Int x) = Int x
-- Evaluation of Boolean expressions (Bool)
evalStep (Bool b) = Bool b
evalStep (Float f) = Float f
-- Evaluation of variable expressions (Var)
evalStep (Var v) = Var v
-- Evaluation of binary expressions
evalStep (BinaryOp op e1 e2) =
    case evalBinaryOp (BinaryOp op (evalStep e1) (evalStep e2)) of
        Just result -> result
        Nothing -> error ("Binary operation cannot be processed" ++ show op ++ show e1 ++ show e2)
-- Evaluation of unary expressions
evalStep (UnaryOp Negate (Int x)) = Int (-x)
evalStep (UnaryOp Not (Bool b)) = Bool (not b)
-- Remaining unary operations...
-- Evaluation of conditional expressions
evalStep (If (Bool True) e2 _) = e2
evalStep (If (Bool False) _ e3) = e3
evalStep (If e1 e2 e3) =
    let e1' = evalStep e1
     in If e1' e2 e3
-- Evaluation of let expressions
evalStep (Let var e1 e2) = substituteVar var e1 e2
evalStep (App (Lambda argName argType body) argExpr) = substituteVar argName argExpr body
-- Evaluation of lambda expressions (Lambda)
evalStep (Lambda argName argName argType body) = Lambda argName argType (evalStep body)
evalStep (Fst e) = case evalStep e of
    Pair fst _ -> evalStep fst
    _ -> error "Expected a Pair in Fst"
evalStep (Snd e) = case evalStep e of
    Pair _ snd -> evalStep snd
    _ -> error "Expected a Pair in Snd"
evalStep (Pair e1 e2) = Pair (evalStep e1) (evalStep e2)
-- Rest of the cases of expressions according to the grammar
evalStep expr = error ("NO pull" ++ show expr) -- For expressions that don't have an evaluation step

The problem is that with some tests I get to something like App (Var v) e2 and I don't know if my function is doing something wrong or I should treat that issue separately (in theory it should happen that I always have App (Lambda v e1 e2) e2').

0

There are 0 answers