Agda.Auto.CaseSplit

Documentation

abspatvarname :: String

costCaseSplitVeryHigh :: Cost

costCaseSplitHigh :: Cost

costCaseSplitLow :: Cost

costAddVarDepth :: Cost

data HI a

Constructors

HI Hiding a

Instances

LocalTerminationEnv a => LocalTerminationEnv (HI a)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: HI a -> (Sum Nat, [Nat])

Renaming t => Renaming (HI t)

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t

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

type CSPat o = HI (CSPatI o)

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

data CSPatI o

Constructors

CSPatConApp (ConstRef o) [CSPat o]

CSPatProj (ConstRef o)

CSPatVar Nat

CSPatExp (MExp o)

CSWith (MExp o)

CSAbsurd

CSOmittedArg

Instances

LocalTerminationEnv (CSPatI o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat])

Renaming (CSPatI o)

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> 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 t u where

Associated Types

type ReplaceWith t u

Methods

replace' :: Nat -> MExp (ReplaceWith t u) -> t -> Reader (Nat, Nat) u

Instances

Replace t u => Replace (Abs t) (Abs u)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Abs t) (Abs u)

Methods

replace' :: Nat -> MExp (ReplaceWith (Abs t) (Abs u)) -> Abs t -> Reader (Nat, Nat) (Abs u)

Replace (ArgList o) (ArgList o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (ArgList o) (ArgList o)

Methods

replace' :: Nat -> MExp (ReplaceWith (ArgList o) (ArgList o)) -> ArgList o -> Reader (Nat, Nat) (ArgList o)

Replace (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o)

Replace t u => Replace (MM t (RefInfo o)) u

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (MM t (RefInfo o)) u

Methods

replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u

replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> 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 t where

Associated Types

type UnifiesTo t

Methods

unify' :: t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()

notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) IO) Bool

Instances

Unify t => Unify (Abs t)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Abs t)

Methods

unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe ()

notequal' :: Abs t -> Abs t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool

Unify (ArgList o)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (ArgList o)

Methods

unify' :: ArgList o -> ArgList o -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe ()

notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool

Unify (Exp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Exp o)

Methods

unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()

notequal' :: Exp o -> Exp o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool

(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o))

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (MM t (RefInfo o))

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool

unify :: Unify t => t -> t -> Maybe (Assignments (UnifiesTo t))

notequal :: Unify 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

Methods

lift' :: Nat -> Nat -> t -> t

Instances

Lift t => Lift (Abs t)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Abs t -> Abs t

Lift (ArgList o)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> ArgList o -> ArgList o

Lift (Exp o)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Exp o -> Exp o

Lift t => Lift (MM t r)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> MM t r -> MM t r

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

Speculation: Type class computing the size (?) of a pattern and collecting the vars it introduces

Methods

sizeAndBoundVars :: a -> (Sum Nat, [Nat])

Instances

LocalTerminationEnv (CSPatI o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat])

LocalTerminationEnv a => LocalTerminationEnv (HI a)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: HI a -> (Sum Nat, [Nat])

LocalTerminationEnv (MArgList o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

LocalTerminationEnv (MExp o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

LocalTerminationEnv a => LocalTerminationEnv [a]

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: [a] -> (Sum Nat, [Nat])

(LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: (a, b) -> (Sum Nat, [Nat])

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

Take a list of patterns and returns (is, size, vars) where (speculation):

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

getblks :: MExp o -> IO [Nat]