liquid-fixpoint-0.8.10.1: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver

Safe HaskellNone
LanguageHaskell98

Language.Fixpoint.Solver.UniqifyKVars

Description

This module creates new bindings for each argument of each kvar. It also makes sure that all arguments to each kvar are explicit.

For example,

``` bind 0 x bind 1 v constraint: env [0; 1] rhs $k_42 // implicit substitutions [x:=x], [v:=v] wf: env [0] reft {v : int | [$k_42]} ```

becomes

``` bind 0 x bind 1 v bind 2 lq_karg$x$k_42 constraint: env [0; 1] rhs $k_42[lq_karg$x$k_42:=x][lq_karg$v$k_42:=v]

wf: env [2] reft {lq_karg$v$k_42 : int | [$k_42]} ```

Documentation