[m-users.] A more precise determinism checker

[Dirk Ziegemeyer]

> Am 19.03.2022 um 17:12 schrieb Philip White <philip at pswhite.org>:
> 
> 
> I'd love to hear what people think of this approach. I haven't yet
> tested it at large scale with huge predicates, so my biggest concern is
> that it will be really, really slow.

Mercury's determinism checker works fine for about 90 percent of my predicates. I wish there would exist some solution to assist Mercury with the remaining 10 percent.

A pattern that happens very frequently to me: I know exactly that a key is not a member of the keys of a map. Inserting this key into the map under this precondition (with map.insert/4) is of determinism det instead of semidet.

Maybe this is a source of inspiration for your project:
"LiquidHaskell (LH) refines Haskell's types with logical predicates that let you enforce important properties at compile time." (from their homepage).
It uses an SMT-LIB solver (e.g. Z3).

The Z3 solver is also used by SPARK/Ada.

Dirk