Agda-2.6.1.3: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Auto.CaseSplit

Synopsis

Documentation

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 #

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 #

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

Methods

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

Instances

Instances details
Replace o (ArgList o) (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

Replace o (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

Replace o t u => Replace o (Abs t) (Abs u) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

Replace o t u => Replace o (MM t (RefInfo o)) u Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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

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

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

class Unify o t | t -> o where Source #

Methods

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

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

Instances

Instances details
Unify o (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Unify o (Exp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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

Unify o t => Unify o (Abs t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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

Unify o t => Unify o (MM t (RefInfo o)) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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

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

notequal :: Unify o t => Nat -> Nat -> t -> t -> IO Bool 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 #

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 #

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

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):