<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">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 class="Apple-style-span" face="Courier">data BuiltinDescriptor = BuiltinType Int -- Type, with number of constructors, if any</font></div><div><font class="Apple-style-span" face="Courier"> </font><span class="Apple-tab-span" style="white-space:pre"><font class="Apple-style-span" face="Courier"> </font></span><font class="Apple-style-span" face="Courier"> | BuiltinCons -- Constructor</font></div><div><font class="Apple-style-span" face="Courier"> | BuiltinPrim String (Term -> TCM Type) -- Primitive </font></div><div><span class="Apple-tab-span" style="white-space:pre"><font class="Apple-style-span" face="Courier"> </font></span><font class="Apple-style-span" face="Courier"> | BuiltinPost -- Postulate (may need more info here)</font></div></div><div><font class="Apple-style-span" face="Courier"><br></font></div><div><font class="Apple-style-span" 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 class="Apple-style-span" face="Courier">stdBuiltins :: [BuiltinInfo]</font></div><div><font class="Apple-style-span" face="Courier">stdBuiltins = </font></div><div><font class="Apple-style-span" face="Courier"> [ (builtinList , (tset --> tset , BuiltinType 2))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinBool , (tset , BuiltinType 2))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinNat , (tset , BuiltinType 2))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinInteger , (tset , BuiltinType 0))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinAgdaTerm , (tset , BuiltinType 0))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinEquality , (hPi "A" tset (tv0 --> tv0 --> tset) , BuiltinType 0))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinNil</font><span class="Apple-tab-span" style="white-space:pre"><font class="Apple-style-span" face="Courier"> </font></span><font class="Apple-style-span" face="Courier"> , (hPi "A" tset (el (list v0)) , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinCons , (hPi "A" tset tv0 --> el (list v0) --> el (list v0) , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinZero , (tnat , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinSuc , (tnat --> tnat , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinTrue , (tbool , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinFalse , (tbool , BuiltinCons))</font></div><div><font class="Apple-style-span" face="Courier"> , (builtinRefl , (hPi "A" tset (hPi "x" tv0 (el (primEquality <#> v1 <@> v0 <@> v0))) , BuiltinCons))</font></div><div><font class="Apple-style-span" 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><br></div><div>Thanks,</div><div><br></div><div>-Si.</div></body></html>