Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
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

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 #

Constructors

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

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

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

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

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

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

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