123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126 |
- Built-in things
- ---------------
- - Where are they defined?
- + Haskell-module?
- Not so nice. Hard to find out what's predefined.
- + Agda2 prelude
- Nicer, but what would this look like?
- - How are they accessed?
- + Problem in Agda 1: Bool already defined.
- + import Prelude / import Builtin ?
- - Could we use a more general FFI?
- + Maybe.. but requires more work (hs-plugins, or the like)
- Literals/sugar
- --------------
- - What does sugar expand to? When?
- - What is the type of a literal?
- + Where is it specified?
- + Pragmas?
- {-# LITERAL NATURAL is PRIMITIVE Integer #-}
- {-# LITERAL LIST is SUGAR nil, (::) #-}
- Nice, because we can allow either sugar or builtin for some types (like
- strings or naturals):
- {-# LITERAL NUMBER is PRIMITIVE Integer #-} or
- {-# LITERAL NUMBER is SUGAR FOR zero, suc #-}
- Builtin: NATURAL, FLOAT, CHAR, STRING
- Possible solution
- -----------------
- - Add a primitive keyword:
- + primitive integerPlus : Integer -> Integer -> Integer
- - Add "primitive" definitions:
- + data Defn = ... | Primitive Arity ([Term] -> TC Term)
- + The function is responsible for normalising its arguments if needed.
- - Primitive functions are defined in TypeChecking.Primitive
- + primitives :: Map String (Arity, [Term] -> TC Term)
- primitives = Map.fromList
- [ "integerPlus", (2, integerPlus)
- , ...
- ]
- integerPlus :: [Term] -> TC Term
- integerPlus [x, y] = do
- (x,y) <- normalise (x,y)
- case (x,y) of
- (LitInt n, LitInt m) -> return $ LitInt $ n + m
- _ -> ...
- integerEquals (Lit n) (Lit m)
- | n == m = primTrue
- primTrue :: TC Term
- primTrue = lookupPrim "TRUE"
- - Define a prelude/builtin module
- {-# BUILTIN NATURAL Integer #-}
- {-# BUILTIN FLOAT Float #-}
- {-# BUILTIN CHAR Char #-}
- postulate Integer : Set
- Float : Set
- Char : Set
- {-# SUGAR LIST nil :: #-}
- data List (A:Set) : Set where
- nil : List A
- (::) : A -> List A -> List A
- {-# SUGAR STRING nil, (::) #-}
- String : Set
- String = List Char
- {-# BUILTIN FALSE false #-}
- {-# BUILTIN TRUE true #-}
- data Bool : Set where
- false : Bool
- true : Bool
- primitive
- integerPlus : Integer -> Integer -> Integer
- integerEqual : Integer -> Integer -> Bool
- postulate
- integerPlusAssoc : (x,y,z:Integer) ->
- Built-in things and Parameterised Modules
- -----------------------------------------
- What is the type of 1 in the following example:
- module Int (I:Set) where
- {-# BUILTIN INTEGER I #-}
- postulate Int1 : Set
- Int2 : Set
- module Int1 = Int Int1
- module Int2 = Int Int2
- Possible solution: don't allow BUILTIN in parameterised modules.
- vim: sts=2 sw=2 tw=80
|