SparseCheck

Documentation

newtype LP a

Constructors

LP

Fields

unLP :: State -> (State -> a -> [[Exp]]) -> [[Exp]]

Instances

Monad LP

MonadPlus LP

runLP :: Int -> LP [Exp] -> [[Exp]]

data State

Constructors

State

Fields

env :: IntMap Status

fresh :: Int

caseType :: CaseType

depthBound :: Int

initState :: Int -> State

data Status

Constructors

Unbound Int [Residual]

Bound Exp

type Residual = Exp -> LP ()

newtype Term a

Constructors

Term

Fields

expr :: Exp

Instances

Tuple (Term a)

data Exp

Constructors

Var Var

Ctr Int [Exp]

type Var = Int

data CaseType

Constructors

Residuate

Instantiate

data Pair a b

Constructors

a :- b

Instances

(Eq a, Eq b) => Eq (Pair a b)

(Show a, Show b) => Show (Pair a b)

(Convert a, Convert b) => Convert (Pair a b)

(Tuple a, Tuple b) => Tuple (Pair a b)

class Tuple a where

Methods

free :: LP a

(===) :: a -> a -> LP ()

match :: Tuple b => a -> a -> (LP () -> LP b) -> LP b

Instances

Tuple ()

Tuple (Term a)

(Tuple a, Tuple b) => Tuple (a, b)

(Tuple a, Tuple b) => Tuple (Pair a b)

(Tuple a, Tuple b, Tuple c) => Tuple (a, b, c)

(Tuple a, Tuple b, Tuple c, Tuple d) => Tuple (a, b, c, d)

class Convert a where

Methods

term :: a -> Term a

unterm :: (Term a -> LP (), Exp -> a)

Instances

Convert Bool

Convert Int

Convert a => Convert [a]

Convert a => Convert (Maybe a)

(Convert a, Convert b) => Convert (Either a b)

(Convert a, Convert b) => Convert (a, b)

(Convert a, Convert b) => Convert (Pair a b)

newVar :: LP Var

readVar :: Var -> LP Status

writeVar :: Var -> Status -> LP ()

ifBound :: Var -> (Exp -> LP a) -> LP a -> LP a

root :: Exp -> LP Exp

deepRoot :: Exp -> LP Exp

unifyExp :: Exp -> Exp -> LP ()

unifyVar :: Var -> Var -> LP ()

bindVar :: Var -> Exp -> LP ()

setDepth :: Int -> Exp -> LP ()

resumeOn :: [Residual] -> Exp -> LP ()

rigidExp :: Tuple b => (Exp -> LP b) -> Exp -> LP b

rigid :: Tuple b => (Term a -> LP b) -> Term a -> LP b

resid :: LP a -> LP a

eq :: Exp -> Exp -> LP () -> LP ()

(=/=) :: Term a -> Term a -> LP ()

matchExp :: Tuple a => Exp -> Exp -> (LP () -> LP a) -> LP a

data Alts a b

Constructors

a :-> b

(Alts a b) :|: (Alts a b)

flattenAlts :: Alts a b -> [(a, b)]

getCaseType :: LP CaseType

instantiate :: Tuple a => a -> [(a, LP b)] -> LP b

residuate :: (Tuple a, Tuple b) => a -> [(a, LP b)] -> LP b

caseOf :: (Tuple a, Tuple b, Tuple c) => a -> (b -> Alts a (LP c)) -> LP c

type Pred = LP ()

(?) :: LP a -> LP a -> LP a

(&) :: LP a -> LP b -> LP b

exists :: Tuple a => (a -> LP b) -> LP b

true :: LP ()

false :: LP a

solveHelp :: Int -> ([Exp] -> LP a) -> LP [Exp]

solve :: Convert a => Int -> (Term a -> Pred) -> [a]

solve2 :: (Convert a, Convert b) => Int -> (Term a -> Term b -> Pred) -> [(a, b)]

solve3 :: (Convert a, Convert b, Convert c) => Int -> (Term a -> Term b -> Term c -> Pred) -> [(a, b, c)]

solve4 :: (Convert a, Convert b, Convert c, Convert d) => Int -> (Term a -> Term b -> Term c -> Term d -> Pred) -> [(a, b, c, d)]

check :: Convert b => Int -> (Term b -> Pred) -> (b -> Bool) -> [b]

check2 :: (Convert t, Convert t1) => Int -> (Term t -> Term t1 -> Pred) -> (t -> t1 -> Bool) -> [(t, t1)]

check3 :: (Convert t, Convert t1, Convert t2) => Int -> (Term t -> Term t1 -> Term t2 -> Pred) -> (t -> t1 -> t2 -> Bool) -> [(t, t1, t2)]

check4 :: (Convert t, Convert t1, Convert t2, Convert t3) => Int -> (Term t -> Term t1 -> Term t2 -> Term t3 -> Pred) -> (t -> t1 -> t2 -> t3 -> Bool) -> [(t, t1, t2, t3)]

lower :: Convert a1 => (Term a1 -> LP a) -> a1 -> Bool

lower2 :: (Convert a1, Convert a2) => (Term a1 -> Term a2 -> LP a) -> a1 -> a2 -> Bool

lower3 :: (Convert a1, Convert a2, Convert a3) => (Term a1 -> Term a2 -> Term a3 -> LP a) -> a1 -> a2 -> a3 -> Bool

lower4 :: (Convert a1, Convert a2, Convert a3, Convert a4) => (Term a1 -> Term a2 -> Term a3 -> Term a4 -> LP a) -> a1 -> a2 -> a3 -> a4 -> Bool

ctr0 :: a -> Int -> Term a

ctr1 :: (a -> b) -> Int -> Term a -> Term b

ctr2 :: (a -> b -> c) -> Int -> Term a -> Term b -> Term c

ctr3 :: (a -> b -> c -> d) -> Int -> Term a -> Term b -> Term c -> Term d

ctr4 :: (a -> b -> c -> d -> e) -> Int -> Term a -> Term b -> Term c -> Term d -> Term e

(\/) :: (Int -> b) -> (Int -> c) -> Int -> Pair b c

datatype :: (Int -> b) -> b

type Family = [(Int, Int)]

type Conv a = (Term a -> Pred, Exp -> Maybe a)

instCtr :: Var -> (Int, Int) -> Pred

mkInst :: Int -> Int -> ([Exp] -> Pred) -> Term a -> Pred

mkConv :: Int -> ([Exp] -> a) -> Exp -> Maybe a

conv0 :: a -> Int -> Conv a

conv1 :: Convert a => (a -> b) -> Int -> Conv b

conv2 :: (Convert a, Convert b) => (a -> b -> c) -> Int -> Conv c

conv3 :: (Convert a, Convert b, Convert c) => (a -> b -> c -> d) -> Int -> Conv d

conv4 :: (Convert a, Convert b, Convert c, Convert d) => (a -> b -> c -> d -> e) -> Int -> Conv e

(-+-) :: (Num a, MonadPlus m, MonadPlus m1) => (a -> (t -> m a1, t1 -> m1 a2)) -> (a -> (t -> m a1, t1 -> m1 a2)) -> a -> (t -> m a1, t1 -> m1 a2)

converter :: Num a => (a -> (t, a1 -> Maybe c)) -> (t, a1 -> c)

(***) :: Term a -> Term b -> Term (Pair a b)

pair :: Term a -> Term b -> Term (a, b)

fal :: Term Bool

nothing :: Term (Maybe a)

nil :: Term [a]

left :: Term a -> Term (Either a b)

zeroInt :: Int

succInt :: Int -> Int

zero :: Term Int

add :: Term Int -> Term Int -> Term Int -> Pred

sub' :: Term Int -> Term Int -> Term (Either Int Int) -> Pred

sub :: Term Int -> Term Int -> Term Int -> Pred

mul :: Term Int -> Term Int -> Term Int -> Pred

pow :: Term Int -> Term Int -> Term Int -> Pred

quotrem :: Term Int -> Term Int -> Term Int -> Term Int -> Pred

class Ordered a where

Methods

(|<|) :: Term a -> Term a -> Pred

(|>|) :: Term a -> Term a -> Pred

(|<=|) :: Term a -> Term a -> Pred

(|>=|) :: Term a -> Term a -> Pred

Instances

Ordered Int

i :: Int -> Term Int

append :: Term [a] -> Term [a] -> Term [a] -> Pred

len :: Term [a] -> Term Int -> Pred

forall :: Term [a] -> (Term a -> Pred) -> Pred

forany :: Term [a] -> (Term a -> Pred) -> Pred

mapP :: (Term a -> Term b -> Pred) -> Term [a] -> Term [b] -> Pred