Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Auto.CaseSplit

Synopsis

Documentation

data HI a Source #

Constructors

HI Hiding a 

Instances

Instances details
LocalTerminationEnv a => LocalTerminationEnv (HI a) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

Renaming t => Renaming (HI t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t 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
LocalTerminationEnv (CSPatI o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

Renaming (CSPatI o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> 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 -> 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 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 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 (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 (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 #

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 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 (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, 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 t => Lift (Abs t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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 (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 #

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 (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 (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 a => LocalTerminationEnv [a] Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

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

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