Documentation

abspatvarname :: String Source #

costCaseSplitVeryHigh :: Nat Source #

costCaseSplitHigh :: Nat Source #

costCaseSplitLow :: Nat Source #

costAddVarDepth :: Nat Source #

data HI a Source #

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

type CSPat o = HI (CSPatI o) Source #

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

data CSPatI o Source #

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

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

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

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

replace :: Nat -> Nat -> MExp o -> MExp o -> MExp o Source #

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

concatargs :: MM (ArgList o) (RefInfo o) -> MArgList o -> MArgList o Source #

eqelr :: Elr o -> Elr o -> Bool Source #

replacep :: Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o Source #

rm :: MM a b -> a Source #

mm :: a -> MM a b Source #

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

lift :: Nat -> MExp o -> MExp o Source #

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

notequal :: Nat -> Nat -> MExp o -> MExp o -> IO Bool Source #

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

freevars :: MExp o -> [Nat] Source #

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

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

rename :: (Nat -> Nat) -> MExp o -> MExp o Source #

renamep :: (Nat -> Nat) -> CSPat o -> CSPat o Source #

seqctx :: CSCtx o -> CSCtx o Source #

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

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

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

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