Skip to content

Much simpler language for PmCheck

Sebastian Graf requested to merge wip/pmcheck-flat into master

Simon realised that the simple language composed of let bindings, bang patterns and flat constructor patterns is enough to capture the semantics of the source pattern language that are important for pattern-match checking. Well, given that the Oracle is smart enough to connect the dots in this less informationally dense form, which it is now.

So we transform translatePat to return a list of PmGrds relative to an incoming match variable. pmCheck then trivially translates each of the PmGrds into constraints that the oracle understands.

Edited by Sebastian Graf

Merge request reports