Mentions légales du service

Skip to content

typed holes (with subterms) for shrinking

SCHERER Gabriel requested to merge gscherer/inferno:typed-holes into master

A typed hole can have any type (it imposes no typing constraints on the context around it), and its subterms can have any type (the hole imposes no constraint on them).

This is the ultimate language construct to do type-preserving shrinking. When shrinking it is important to be able to remove subterms that do not participate to the error.

Holes with no subterms can be used to completely erase a term. Holes with subterms can be used to selectively erase parts of a term (for example, the application "t u" can be rewritten into the hole "...[t, u]", erasing only the application rule).

The MR also contains some independent improvements to the shrinking strategy; in particular convenient shrinking for products, which I hope to possibly upstream in QCheck directly.

Edited by SCHERER Gabriel

Merge request reports