A Hugo incarnation of the blog.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364
  1. data ExprType
  2. = IntType
  3. | BoolType
  4. | StringType
  5. repr : ExprType -> Type
  6. repr IntType = Int
  7. repr BoolType = Bool
  8. repr StringType = String
  9. data Op
  10. = Add
  11. | Subtract
  12. | Multiply
  13. | Divide
  14. data Expr
  15. = IntLit Int
  16. | BoolLit Bool
  17. | StringLit String
  18. | BinOp Op Expr Expr
  19. data SafeExpr : ExprType -> Type where
  20. IntLiteral : Int -> SafeExpr IntType
  21. BoolLiteral : Bool -> SafeExpr BoolType
  22. StringLiteral : String -> SafeExpr StringType
  23. BinOperation : (repr a -> repr b -> repr c) -> SafeExpr a -> SafeExpr b -> SafeExpr c
  24. typecheckOp : Op -> (a : ExprType) -> (b : ExprType) -> Either String (c : ExprType ** repr a -> repr b -> repr c)
  25. typecheckOp Add IntType IntType = Right (IntType ** (+))
  26. typecheckOp Subtract IntType IntType = Right (IntType ** (-))
  27. typecheckOp Multiply IntType IntType = Right (IntType ** (*))
  28. typecheckOp Divide IntType IntType = Right (IntType ** div)
  29. typecheckOp _ _ _ = Left "Invalid binary operator application"
  30. typecheck : Expr -> Either String (n : ExprType ** SafeExpr n)
  31. typecheck (IntLit i) = Right (_ ** IntLiteral i)
  32. typecheck (BoolLit b) = Right (_ ** BoolLiteral b)
  33. typecheck (StringLit s) = Right (_ ** StringLiteral s)
  34. typecheck (BinOp o l r) = do
  35. (lt ** le) <- typecheck l
  36. (rt ** re) <- typecheck r
  37. (ot ** f) <- typecheckOp o lt rt
  38. pure (_ ** BinOperation f le re)
  39. eval : SafeExpr t -> repr t
  40. eval (IntLiteral i) = i
  41. eval (BoolLiteral b) = b
  42. eval (StringLiteral s) = s
  43. eval (BinOperation f l r) = f (eval l) (eval r)
  44. resultStr : {t : ExprType} -> repr t -> String
  45. resultStr {t=IntType} i = show i
  46. resultStr {t=BoolType} b = show b
  47. resultStr {t=StringType} s = show s
  48. tryEval : Expr -> String
  49. tryEval ex =
  50. case typecheck ex of
  51. Left err => "Type error: " ++ err
  52. Right (t ** e) => resultStr $ eval {t} e
  53. main : IO ()
  54. main = putStrLn $ tryEval $ BinOp Add (IntLit 6) (BinOp Multiply (IntLit 160) (IntLit 2))