builtin 2.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126
  1. Built-in things
  2. ---------------
  3. - Where are they defined?
  4. + Haskell-module?
  5. Not so nice. Hard to find out what's predefined.
  6. + Agda2 prelude
  7. Nicer, but what would this look like?
  8. - How are they accessed?
  9. + Problem in Agda 1: Bool already defined.
  10. + import Prelude / import Builtin ?
  11. - Could we use a more general FFI?
  12. + Maybe.. but requires more work (hs-plugins, or the like)
  13. Literals/sugar
  14. --------------
  15. - What does sugar expand to? When?
  16. - What is the type of a literal?
  17. + Where is it specified?
  18. + Pragmas?
  19. {-# LITERAL NATURAL is PRIMITIVE Integer #-}
  20. {-# LITERAL LIST is SUGAR nil, (::) #-}
  21. Nice, because we can allow either sugar or builtin for some types (like
  22. strings or naturals):
  23. {-# LITERAL NUMBER is PRIMITIVE Integer #-} or
  24. {-# LITERAL NUMBER is SUGAR FOR zero, suc #-}
  25. Builtin: NATURAL, FLOAT, CHAR, STRING
  26. Possible solution
  27. -----------------
  28. - Add a primitive keyword:
  29. + primitive integerPlus : Integer -> Integer -> Integer
  30. - Add "primitive" definitions:
  31. + data Defn = ... | Primitive Arity ([Term] -> TC Term)
  32. + The function is responsible for normalising its arguments if needed.
  33. - Primitive functions are defined in TypeChecking.Primitive
  34. + primitives :: Map String (Arity, [Term] -> TC Term)
  35. primitives = Map.fromList
  36. [ "integerPlus", (2, integerPlus)
  37. , ...
  38. ]
  39. integerPlus :: [Term] -> TC Term
  40. integerPlus [x, y] = do
  41. (x,y) <- normalise (x,y)
  42. case (x,y) of
  43. (LitInt n, LitInt m) -> return $ LitInt $ n + m
  44. _ -> ...
  45. integerEquals (Lit n) (Lit m)
  46. | n == m = primTrue
  47. primTrue :: TC Term
  48. primTrue = lookupPrim "TRUE"
  49. - Define a prelude/builtin module
  50. {-# BUILTIN NATURAL Integer #-}
  51. {-# BUILTIN FLOAT Float #-}
  52. {-# BUILTIN CHAR Char #-}
  53. postulate Integer : Set
  54. Float : Set
  55. Char : Set
  56. {-# SUGAR LIST nil :: #-}
  57. data List (A:Set) : Set where
  58. nil : List A
  59. (::) : A -> List A -> List A
  60. {-# SUGAR STRING nil, (::) #-}
  61. String : Set
  62. String = List Char
  63. {-# BUILTIN FALSE false #-}
  64. {-# BUILTIN TRUE true #-}
  65. data Bool : Set where
  66. false : Bool
  67. true : Bool
  68. primitive
  69. integerPlus : Integer -> Integer -> Integer
  70. integerEqual : Integer -> Integer -> Bool
  71. postulate
  72. integerPlusAssoc : (x,y,z:Integer) ->
  73. Built-in things and Parameterised Modules
  74. -----------------------------------------
  75. What is the type of 1 in the following example:
  76. module Int (I:Set) where
  77. {-# BUILTIN INTEGER I #-}
  78. postulate Int1 : Set
  79. Int2 : Set
  80. module Int1 = Int Int1
  81. module Int2 = Int Int2
  82. Possible solution: don't allow BUILTIN in parameterised modules.
  83. vim: sts=2 sw=2 tw=80