<br>On Mon, Sep 13, 2010 at 1:11 PM, Simon Foster <span dir="ltr"><<a href="mailto:s.foster@dcs.shef.ac.uk">s.foster@dcs.shef.ac.uk</a>></span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
<div style="word-wrap:break-word">Hi,<div><br></div><div>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:</div>
<div><br></div><div><div><font face="Courier">data BuiltinDescriptor = BuiltinType Int -- Type, with number of constructors, if any</font></div><div><font face="Courier"> </font><span style="white-space:pre-wrap"><font face="Courier"> </font></span><font face="Courier"> | BuiltinCons -- Constructor</font></div>
<div><font face="Courier"> | BuiltinPrim String (Term -> TCM Type) -- Primitive </font></div><div><span style="white-space:pre-wrap"><font face="Courier"> </font></span><font face="Courier"> | BuiltinPost -- Postulate (may need more info here)</font></div>
</div><div><font face="Courier"><br></font></div><div><font face="Courier">type BuiltinInfo = (String, (TCM Type, BuiltinDescriptor))</font></div><div><br></div><div>Where BuiltinInfo contains the name, type and description of the new builtin. You can then describe builtins like so:</div>
<div><br></div><div><div><font face="Courier">stdBuiltins :: [BuiltinInfo]</font></div><div><font face="Courier">stdBuiltins = </font></div><div><font face="Courier"> [ (builtinList , (tset --> tset , BuiltinType 2))</font></div>
<div><font face="Courier"> , (builtinBool , (tset , BuiltinType 2))</font></div><div><font face="Courier"> , (builtinNat , (tset , BuiltinType 2))</font></div><div><font face="Courier"> , (builtinInteger , (tset , BuiltinType 0))</font></div>
<div><font face="Courier"> , (builtinAgdaTerm , (tset , BuiltinType 0))</font></div><div><font face="Courier"> , (builtinEquality , (hPi "A" tset (tv0 --> tv0 --> tset) , BuiltinType 0))</font></div>
<div><font face="Courier"> , (builtinNil</font><span style="white-space:pre-wrap"><font face="Courier"> </font></span><font face="Courier"> , (hPi "A" tset (el (list v0)) , BuiltinCons))</font></div>
<div><font face="Courier"> , (builtinCons , (hPi "A" tset tv0 --> el (list v0) --> el (list v0) , BuiltinCons))</font></div><div><font face="Courier"> , (builtinZero , (tnat , BuiltinCons))</font></div>
<div><font face="Courier"> , (builtinSuc , (tnat --> tnat , BuiltinCons))</font></div><div><font face="Courier"> , (builtinTrue , (tbool , BuiltinCons))</font></div><div><font face="Courier"> , (builtinFalse , (tbool , BuiltinCons))</font></div>
<div><font face="Courier"> , (builtinRefl , (hPi "A" tset (hPi "x" tv0 (el (primEquality <#> v1 <@> v0 <@> v0))) , BuiltinCons))</font></div><div><font face="Courier">]</font></div>
</div><div><br></div><div>for example.</div><div><br></div><div>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).</div>
<div><br></div><div>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?</div></div></blockquote><div><br></div>
<div>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.</div>
<div><br></div><div>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:</div><div><br></div><div>data NAT : Set where</div><div>
ZERO : NAT</div><div> SUC : NAT -> NAT</div><div><br></div><div>NATPLUS : NAT -> NAT -> NAT</div><div>NATPLUS ZERO m = m</div><div>NATPLUS (SUC n) m = SUC (NATPLUS n m)</div><div><br></div><div>It shouldn't be that hard to type check that and turn it into your representation.</div>
<div><br></div><div>/ Ulf</div></div>