A Hugo incarnation of the blog.
Vous ne pouvez pas sélectionner plus de 25 sujets Les noms de sujets doivent commencer par une lettre ou un nombre, peuvent contenir des tirets ('-') et peuvent comporter jusqu'à 35 caractères.

TypesafeIntr.idr 1.8KB

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))