Useful Dhall operations/tools:
Common subexpr elimination:
[ < L | R | X >.L, < L | R | X >.R ]
=cse=>
let _ = < L | R | X > in [ _.L, _.R ]
For any expr e
cse(e) =normalize=> e
Simplify unions (recursively over records and lists):
[ < L | R | X >.L, < L | R | X >.R ]
=simpl=>
[ < L | R >.L, < L | R >.R ]
Generalize (a la TIDL):
(< A >.A as < A | B >) => < A | B >.A
{ foo = 1 } as { foo : Int, bar : Optional Bool } => { foo = 1, bar = None Bool }
etc.
For any type T and (x : T), where T is constructed out of records, unions, lists, optional and primitives:
simpl(x) as T : T
simpl(x) as T = x