Documentation

abspatvarname :: String #

costCaseSplitVeryHigh :: Cost #

costCaseSplitHigh :: Cost #

costCaseSplitLow :: Cost #

costAddVarDepth :: Cost #

data HI a #

drophid :: [HI a] -> [a] #

type CSPat o = HI (CSPatI o) #

type CSCtx o = [HI (MId, MExp o)] #

data CSPatI o #

type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))] #

caseSplitSearch :: forall o. IORef Int -> Int -> [ConstRef o] -> Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o] #

caseSplitSearch' :: forall o. (Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) -> Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o] #

infertypevar :: CSCtx o -> Nat -> MExp o #

class Replace o t u | t u -> o where #

replace :: Replace o t u => Nat -> Nat -> MExp o -> t -> u #

betareduce :: MExp o -> MArgList o -> MExp o #

concatargs :: MArgList o -> MArgList o -> MArgList o #

replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o #

type Assignments o = [(Nat, Exp o)] #

class Unify o t | t -> o where #

unify :: Unify o t => t -> t -> Maybe (Assignments o) #

notequal :: Unify o t => Nat -> Nat -> t -> t -> IO Bool #

unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe () #

unifyexp :: MExp o -> MExp o -> Maybe [(Nat, MExp o)] #

class Lift t where #

lift :: Lift t => Nat -> t -> t #

removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o]) #

findperm :: [MExp o] -> Maybe [Nat] #

freevars :: FreeVars t => t -> [Nat] #

applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] -> (CSCtx o, MExp o, [CSPat o]) #

ren :: [Nat] -> Nat -> Int #

seqctx :: CSCtx o -> CSCtx o #

depthofvar :: Nat -> [CSPat o] -> Nat #

class LocalTerminationEnv a where #

localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat]) #

localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o) #

getblks :: MExp o -> IO [Nat] #