This page gives the concrete syntax for the framework layer and hence for object files. I’ve now added objects corresponding to datatypes, but I’m not yet computing gadgets. I have implemented the forcing optimization, however. See Datatype.lhs for the code which searches for projections from index values equal to constructor arguments.
I loaded this lump:
*FrameParser> testFrame "Fred"
{A data
{Nat in *}
{zero in {Nat}}{suc (n : {Nat}) in {Nat}}}
{B (X : *)data
{Vec (n : {A.Nat}) in *}
{vnil in {Vec {A.zero}}}
{vcons (n : {A.Nat})(x : X)(xs : {Vec n})
in {Vec {A.suc n}}} }
STOP
The machine correctly figured out how to recover n for vcons and X for both.
Elimination gadgets are next on the hitlist…