[Agda] Refectoring Builtins

[Simon Foster]

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?

Thanks,

-Si.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100913/776ebf6b/attachment.html