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.

TypesafeIntrV3.idr 3.9KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120
  1. data ExprType
  2. = IntType
  3. | BoolType
  4. | StringType
  5. | PairType ExprType ExprType
  6. repr : ExprType -> Type
  7. repr IntType = Int
  8. repr BoolType = Bool
  9. repr StringType = String
  10. repr (PairType t1 t2) = Pair (repr t1) (repr t2)
  11. decEq : (a : ExprType) -> (b : ExprType) -> Maybe (a = b)
  12. decEq IntType IntType = Just Refl
  13. decEq BoolType BoolType = Just Refl
  14. decEq StringType StringType = Just Refl
  15. decEq (PairType lt1 lt2) (PairType rt1 rt2) = do
  16. subEq1 <- decEq lt1 rt1
  17. subEq2 <- decEq lt2 rt2
  18. let firstEqual = replace {P = \t1 => PairType lt1 lt2 = PairType t1 lt2} subEq1 Refl
  19. let secondEqual = replace {P = \t2 => PairType lt1 lt2 = PairType rt1 t2} subEq2 firstEqual
  20. pure secondEqual
  21. decEq _ _ = Nothing
  22. data Op
  23. = Add
  24. | Subtract
  25. | Multiply
  26. | Divide
  27. data Expr
  28. = IntLit Int
  29. | BoolLit Bool
  30. | StringLit String
  31. | BinOp Op Expr Expr
  32. | IfElse Expr Expr Expr
  33. | Pair Expr Expr
  34. | Fst Expr
  35. | Snd Expr
  36. data SafeExpr : ExprType -> Type where
  37. IntLiteral : Int -> SafeExpr IntType
  38. BoolLiteral : Bool -> SafeExpr BoolType
  39. StringLiteral : String -> SafeExpr StringType
  40. BinOperation : (repr a -> repr b -> repr c) -> SafeExpr a -> SafeExpr b -> SafeExpr c
  41. IfThenElse : SafeExpr BoolType -> SafeExpr t -> SafeExpr t -> SafeExpr t
  42. NewPair : SafeExpr t1 -> SafeExpr t2 -> SafeExpr (PairType t1 t2)
  43. First : SafeExpr (PairType t1 t2) -> SafeExpr t1
  44. Second : SafeExpr (PairType t1 t2) -> SafeExpr t2
  45. typecheckOp : Op -> (a : ExprType) -> (b : ExprType) -> Either String (c : ExprType ** repr a -> repr b -> repr c)
  46. typecheckOp Add IntType IntType = Right (IntType ** (+))
  47. typecheckOp Subtract IntType IntType = Right (IntType ** (-))
  48. typecheckOp Multiply IntType IntType = Right (IntType ** (*))
  49. typecheckOp Divide IntType IntType = Right (IntType ** div)
  50. typecheckOp _ _ _ = Left "Invalid binary operator application"
  51. requireBool : (n : ExprType ** SafeExpr n) -> Either String (SafeExpr BoolType)
  52. requireBool (BoolType ** e) = Right e
  53. requireBool _ = Left "Not a boolean."
  54. typecheck : Expr -> Either String (n : ExprType ** SafeExpr n)
  55. typecheck (IntLit i) = Right (_ ** IntLiteral i)
  56. typecheck (BoolLit b) = Right (_ ** BoolLiteral b)
  57. typecheck (StringLit s) = Right (_ ** StringLiteral s)
  58. typecheck (BinOp o l r) = do
  59. (lt ** le) <- typecheck l
  60. (rt ** re) <- typecheck r
  61. (ot ** f) <- typecheckOp o lt rt
  62. pure (_ ** BinOperation f le re)
  63. typecheck (IfElse c t e) =
  64. do
  65. ce <- typecheck c >>= requireBool
  66. (tt ** te) <- typecheck t
  67. (et ** ee) <- typecheck e
  68. case decEq tt et of
  69. Just p => pure (_ ** IfThenElse ce (replace p te) ee)
  70. Nothing => Left "Incompatible branch types."
  71. typecheck (Pair l r) =
  72. do
  73. (lt ** le) <- typecheck l
  74. (rt ** re) <- typecheck r
  75. pure (_ ** NewPair le re)
  76. typecheck (Fst p) =
  77. do
  78. (pt ** pe) <- typecheck p
  79. case pt of
  80. PairType _ _ => pure $ (_ ** First pe)
  81. _ => Left "Applying fst to non-pair."
  82. typecheck (Snd p) =
  83. do
  84. (pt ** pe) <- typecheck p
  85. case pt of
  86. PairType _ _ => pure $ (_ ** Second pe)
  87. _ => Left "Applying snd to non-pair."
  88. eval : SafeExpr t -> repr t
  89. eval (IntLiteral i) = i
  90. eval (BoolLiteral b) = b
  91. eval (StringLiteral s) = s
  92. eval (BinOperation f l r) = f (eval l) (eval r)
  93. eval (IfThenElse c t e) = if (eval c) then (eval t) else (eval e)
  94. eval (NewPair l r) = (eval l, eval r)
  95. eval (First p) = fst (eval p)
  96. eval (Second p) = snd (eval p)
  97. resultStr : {t : ExprType} -> repr t -> String
  98. resultStr {t=IntType} i = show i
  99. resultStr {t=BoolType} b = show b
  100. resultStr {t=StringType} s = show s
  101. resultStr {t=PairType t1 t2} (l,r) = "(" ++ resultStr l ++ ", " ++ resultStr r ++ ")"
  102. tryEval : Expr -> String
  103. tryEval ex =
  104. case typecheck ex of
  105. Left err => "Type error: " ++ err
  106. Right (t ** e) => resultStr $ eval {t} e
  107. main : IO ()
  108. main = putStrLn $ tryEval $ BinOp Add (Fst (IfElse (BoolLit True) (Pair (IntLit 6) (BoolLit True)) (Pair (IntLit 7) (BoolLit False)))) (BinOp Multiply (IntLit 160) (IntLit 2))