Safe Haskell	None
Language	Haskell2010

Agda.Auto.CaseSplit

Synopsis

abspatvarname :: String
costCaseSplitVeryHigh :: Cost
costCaseSplitHigh :: Cost
costCaseSplitLow :: Cost
costAddVarDepth :: Cost
data HI a = HI Hiding a
drophid :: [HI a] -> [a]
type CSPat o = HI (CSPatI o)
type CSCtx o = [HI (MId, MExp o)]
data CSPatI o
- = CSPatConApp (ConstRef o) [CSPat o]
- | CSPatVar Nat
- | CSPatExp (MExp o)
- | CSWith (MExp o)
- | CSAbsurd
- | CSOmittedArg
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
- type ReplaceWith t u
- replace' :: Nat -> MExp (ReplaceWith t u) -> t -> 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
- type UnifiesTo t
- unify' :: t -> t -> StateT (Assignments (UnifiesTo t)) Maybe ()
- notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo t)) 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
- lift' :: Nat -> Nat -> t -> t
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
- sizeAndBoundVars :: a -> (Sum Nat, [Nat])
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
getblks :: MExp o -> IO [Nat]

Documentation

abspatvarname :: String Source #

costCaseSplitVeryHigh :: Cost Source #

costCaseSplitHigh :: Cost Source #

costCaseSplitLow :: Cost Source #

costAddVarDepth :: Cost Source #

data HI a Source #

Constructors

HI Hiding a

Instances

Instances details

Renaming t => Renaming (HI t) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t Source #
LocalTerminationEnv a => LocalTerminationEnv (HI a) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: HI a -> (Sum Nat, [Nat]) 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 #

Constructors

CSPatConApp (ConstRef o) [CSPat o]
CSPatVar Nat
CSPatExp (MExp o)
CSWith (MExp o)
CSAbsurd
CSOmittedArg

Instances

Instances details

Renaming (CSPatI o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o Source #
LocalTerminationEnv (CSPatI o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat]) Source #

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

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

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] Source #

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

class Replace t u where Source #

Associated Types

type ReplaceWith t u Source #

Methods

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

Instances

Instances details

Replace (ArgList o) (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (ArgList o) (ArgList o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (ArgList o) (ArgList o)) -> ArgList o -> Reader (Nat, Nat) (ArgList o) Source #
Replace (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Exp o) (MExp o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #
Replace t u => Replace (Abs t) (Abs u) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Abs t) (Abs u) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Abs t) (Abs u)) -> Abs t -> Reader (Nat, Nat) (Abs u) Source #
Replace t u => Replace (MM t (RefInfo o)) u Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (MM t (RefInfo o)) u Source # Methods replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u Source #

replace :: Replace t u => Nat -> Nat -> MExp (ReplaceWith t u) -> t -> u Source #

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

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

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

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

class Unify t where Source #

Associated Types

type UnifiesTo t Source #

Methods

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

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

Instances

Instances details

Unify (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (ArgList o) Source # Methods unify' :: ArgList o -> ArgList o -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe () Source # notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool Source #
Unify (Exp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (Exp o) Source # Methods unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe () Source # notequal' :: Exp o -> Exp o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool Source #
Unify t => Unify (Abs t) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (Abs t) Source # Methods unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe () Source # notequal' :: Abs t -> Abs t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool Source #
(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (MM t (RefInfo o)) Source # Methods unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe () Source # notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool Source #

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

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

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

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

class Lift t where Source #

Methods

lift' :: Nat -> Nat -> t -> t Source #

Instances

Instances details

Lift (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> ArgList o -> ArgList o Source #
Lift (Exp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Exp o -> Exp o Source #
Lift t => Lift (Abs t) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Abs t -> Abs t Source #
Lift t => Lift (MM t r) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> MM t r -> MM t r Source #

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

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

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

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

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

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

seqctx :: CSCtx o -> CSCtx o Source #

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

class LocalTerminationEnv a where Source #

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

Methods

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

Instances

Instances details

LocalTerminationEnv a => LocalTerminationEnv [a] Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: [a] -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv (MArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv (CSPatI o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: CSPatI o -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv a => LocalTerminationEnv (HI a) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: HI a -> (Sum Nat, [Nat]) Source #
(LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: (a, b) -> (Sum Nat, [Nat]) Source #

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

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

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

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