Nadrieril/dhall-rust

Record projection by expression

Closed this issue · 3 comments

Nadrieril commented

Steps required:

  • Add a new ProjectionByExpression node to ExprF to represent the new syntax
  • Update the parser to handle the new syntax; you will in particular need to change the return type of the selector rule
  • Implement normalization, and enable the relevant tests in dhall/build.rs
  • Implement typechecking, and enable the relevant tests
Nadrieril commented

It was introduced in dhall-lang/dhall-lang#499, and then refined in several subsequent PRs

Nadrieril commented

Instructions

This issue does require a decent familiarity with rust because this codebase is a bit complex.

For normalization, look in normalize.rs for a relevant unimplemented!() call, and implement the behaviour described in the standard where it says "project by type".
For typecheck, look in typecheck.rs for a relevant unimplemented!() call, and implement the behaviour described in the standard where it says "Record projection can also be done by specifying the target record type".
In both cases, looking at similar cases like Projection will help figure out what to do.

Once either of those is done, look in dhall/build.rs and remove the lines that exclude relevant tests. The corresponding tests will be in dhall-lang/tests/..., and yu can also find the expected output, which can help figure out the expected behaviour.

Nadrieril commented

Closed in #133