Use implicit parameters in primitives and opentype format #449
Conversation
| } = | ||
| fun num_tables table_records table_id => array16_find num_tables (Repr table_record) (fun table_record => table_record.table_id == table_id) table_records; | ||
| } = fun @num_tables table_records table_id => array16_find @num_tables @{ | ||
| table_id : U32, | ||
| checksum : U32, | ||
| offset : U32, | ||
| length : U32, | ||
| } (fun table_record => table_record.table_id == table_id) table_records; |
There was a problem hiding this comment.
Note that this results bloated terms in the elaborated output. I’d imagine that glued evaluation might be able to keep these terms small.
| array16_find _ (Repr table_record) | ||
| (fun table_record => table_record.table_id == table_id) | ||
| array16_find | ||
| (fun (table_record : Repr table_record) => table_record.table_id == table_id) | ||
| table_records; |
There was a problem hiding this comment.
Not sure if postponement would help with avoiding the need for a type annotation here? The issue is that we don’t know how to elaborate table_record.table_id without knowing the type of table_record parameter before hand which comes from the table_records argument that is supplied later.
| option_fold (Repr table_record) Format {} | ||
| option_fold ({} : Format) |
There was a problem hiding this comment.
It would be nice to postpone the elaboration of {} and () until later. At the moment we eagerly synthesise them to record literals.
brendanzab
force-pushed
the
implicit-prims
branch
2 times, most recently
from
a438999
to
994483e
Compare
|
This should be ready to merge – but it highlights some areas where our elaboration could be improved. |
We were forgetting to take into account the type parameters in the binary interpreter and the implementation of some of the primitives.
brendanzab
force-pushed
the
implicit-prims
branch
from
994483e
to
c5f9b4e
Compare
This uses implicit parameters to clean up some functions in the opentype format description, and updates the primitives to make use of implicit parameters.