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.

TypesafeImp.idr 2.8KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102
  1. data Reg = A | B | R
  2. data Ty = IntTy | BoolTy
  3. TypeState : Type
  4. TypeState = (Ty, Ty, Ty)
  5. getRegTy : Reg -> TypeState -> Ty
  6. getRegTy A (a, _, _) = a
  7. getRegTy B (_, b, _) = b
  8. getRegTy R (_, _, r) = r
  9. setRegTy : Reg -> Ty -> TypeState -> TypeState
  10. setRegTy A a (_, b, r) = (a, b, r)
  11. setRegTy B b (a, _, r) = (a, b, r)
  12. setRegTy R r (a, b, _) = (a, b, r)
  13. data Expr : TypeState -> Ty -> Type where
  14. Lit : Int -> Expr s IntTy
  15. Load : (r : Reg) -> Expr s (getRegTy r s)
  16. Add : Expr s IntTy -> Expr s IntTy -> Expr s IntTy
  17. Leq : Expr s IntTy -> Expr s IntTy -> Expr s BoolTy
  18. Not : Expr s BoolTy -> Expr s BoolTy
  19. mutual
  20. data Stmt : TypeState -> TypeState -> TypeState -> Type where
  21. Store : (r : Reg) -> Expr s t -> Stmt l s (setRegTy r t s)
  22. If : Expr s BoolTy -> Prog l s n -> Prog l s n -> Stmt l s n
  23. Loop : Prog s s s -> Stmt l s s
  24. Break : Stmt s s s
  25. data Prog : TypeState -> TypeState -> TypeState -> Type where
  26. Nil : Prog l s s
  27. (::) : Stmt l s n -> Prog l n m -> Prog l s m
  28. initialState : TypeState
  29. initialState = (IntTy, IntTy, IntTy)
  30. testProg : Prog Main.initialState Main.initialState Main.initialState
  31. testProg =
  32. [ Store A (Lit 1 `Leq` Lit 2)
  33. , If (Load A)
  34. [ Store A (Lit 1) ]
  35. [ Store A (Lit 2) ]
  36. , Store B (Lit 2)
  37. , Store R (Add (Load A) (Load B))
  38. ]
  39. prodProg : Prog Main.initialState Main.initialState Main.initialState
  40. prodProg =
  41. [ Store A (Lit 7)
  42. , Store B (Lit 9)
  43. , Store R (Lit 0)
  44. , Loop
  45. [ If (Load A `Leq` Lit 0)
  46. [ Break ]
  47. [ Store R (Load R `Add` Load B)
  48. , Store A (Load A `Add` Lit (-1))
  49. ]
  50. ]
  51. ]
  52. repr : Ty -> Type
  53. repr IntTy = Int
  54. repr BoolTy = Bool
  55. data State : TypeState -> Type where
  56. MkState : (repr a, repr b, repr c) -> State (a, b, c)
  57. getReg : (r : Reg) -> State s -> repr (getRegTy r s)
  58. getReg A (MkState (a, _, _)) = a
  59. getReg B (MkState (_, b, _)) = b
  60. getReg R (MkState (_, _, r)) = r
  61. setReg : (r : Reg) -> repr t -> State s -> State (setRegTy r t s)
  62. setReg A a (MkState (_, b, r)) = MkState (a, b, r)
  63. setReg B b (MkState (a, _, r)) = MkState (a, b, r)
  64. setReg R r (MkState (a, b, _)) = MkState (a, b, r)
  65. expr : Expr s t -> State s -> repr t
  66. expr (Lit i) _ = i
  67. expr (Load r) s = getReg r s
  68. expr (Add l r) s = expr l s + expr r s
  69. expr (Leq l r) s = expr l s <= expr r s
  70. expr (Not e) s = not $ expr e s
  71. mutual
  72. stmt : Stmt l s n -> State s -> Either (State l) (State n)
  73. stmt (Store r e) s = Right $ setReg r (expr e s) s
  74. stmt (If c t e) s = if expr c s then prog t s else prog e s
  75. stmt (Loop p) s =
  76. case prog p s >>= stmt (Loop p) of
  77. Right s => Right s
  78. Left s => Right s
  79. stmt Break s = Left s
  80. prog : Prog l s n -> State s -> Either (State l) (State n)
  81. prog Nil s = Right s
  82. prog (st::p) s = stmt st s >>= prog p
  83. run : Prog l s l -> State s -> State l
  84. run p s = either id id $ prog p s