[Agda] Refectoring Builtins

[Ulf Norell]

On Mon, Sep 13, 2010 at 1:11 PM, Simon Foster <s.foster at dcs.shef.ac.uk>wrote:

> Hi,
>
> I'm trying to refactor the code for builtins to allow new builtins to be
> registered easier. At the moment I have the following types to represent
> builtins:
>
> data BuiltinDescriptor = BuiltinType Int -- Type, with number of
> constructors, if any
>             | BuiltinCons     -- Constructor
>                        | BuiltinPrim String (Term -> TCM Type) --
> Primitive
>        | BuiltinPost     -- Postulate (may need more info here)
>
> type BuiltinInfo = (String, (TCM Type, BuiltinDescriptor))
>
> Where BuiltinInfo contains the name, type and description of the new
> builtin. You can then describe builtins like so:
>
> stdBuiltins :: [BuiltinInfo]
> stdBuiltins =
>   [ (builtinList      , (tset --> tset            , BuiltinType 2))
>   , (builtinBool      , (tset                     , BuiltinType 2))
>   , (builtinNat       , (tset                     , BuiltinType 2))
>   , (builtinInteger   , (tset                     , BuiltinType 0))
>   , (builtinAgdaTerm  , (tset                     , BuiltinType 0))
>   , (builtinEquality  , (hPi "A" tset (tv0 --> tv0 --> tset) , BuiltinType
> 0))
>   , (builtinNil      , (hPi "A" tset (el (list v0))         ,
> BuiltinCons))
>   , (builtinCons      , (hPi "A" tset tv0 --> el (list v0) --> el (list v0)
> , BuiltinCons))
>   , (builtinZero      , (tnat                     , BuiltinCons))
>   , (builtinSuc       , (tnat --> tnat            , BuiltinCons))
>   , (builtinTrue      , (tbool                    , BuiltinCons))
>   , (builtinFalse     , (tbool                    , BuiltinCons))
>   , (builtinRefl      , (hPi "A" tset (hPi "x" tv0 (el (primEquality <#> v1
> <@> v0 <@> v0))) , BuiltinCons))
> ]
>
> for example.
>
> Since I don't fully understand the Agda code yet, I want to check if this
> representation is adequate. One immediate problem I have is that the
> constructors for AgdaTerm do not have types assigned in the old system, and
> so I'd have to make the type check optional by making the type a Maybe (or
> else do something strange using TCM).
>
> Should the AgdaTerm constructors have types, or have they deliberately been
> left type-less? Also in general should a builtin's type be mandatory or
> optional?
>

I think it looks good. The AgdaTerm constructors should definitely have
types, I think we omitted them when prototyping and then forgot to add them.
One thing you need to add to cover the existing built-ins is a way to
specify equations that need to hold for a built-in. For instance, when you
bind natural number plus it checks that the appropriate definitional
equations hold.

Eventually I guess we want a nice readable format for specifying built-ins,
so you could specify the natural number built-ins something like this:

data NAT : Set where
  ZERO : NAT
  SUC : NAT -> NAT

NATPLUS : NAT -> NAT -> NAT
NATPLUS ZERO m = m
NATPLUS (SUC n) m = SUC (NATPLUS n m)

It shouldn't be that hard to type check that and turn it into your
representation.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100913/11ad42e6/attachment-0001.html