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

Safe Haskell | None
Language | Haskell2010

Agda.Auto.Syntax

Synopsis

- type UId o = Metavar (Exp o) (RefInfo o)
- data HintMode
  - = HMNormal
  - | HMRecCall
- data EqReasoningConsts o = EqReasoningConsts {
  - eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o
  }
- data EqReasoningState
  - = EqRSNone
  - | EqRSChain
  - | EqRSPrf1
  - | EqRSPrf2
  - | EqRSPrf3
- data RefInfo o
  - = RIEnv {
    - rieHints :: [(ConstRef o, HintMode)]
    - rieDefFreeVars :: Nat
    - rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
    }
  - | RIMainInfo {
    - riMainCxtLength :: Nat
    - riMainType :: HNExp o
    - riMainIota :: Bool
    }
  - | RIUnifInfo [CAction o] (HNExp o)
  - | RICopyInfo (ICExp o)
  - | RIIotaStep Bool
  - | RIInferredTypeUnknown
  - | RINotConstructor
  - | RIUsedVars [UId o] [Elr o]
  - | RIPickSubsvar
  - | RIEqRState EqReasoningState
  - | RICheckElim Bool
  - | RICheckProjIndex [ConstRef o]
- type MyPB o = PB (RefInfo o)
- type MyMB a o = MB a (RefInfo o)
- type Nat = Int
- data MId
  - = Id String
  - | NoId
- data Abs a = Abs MId a
- data ConstDef o = ConstDef {
  - cdname :: String
  - cdorigin :: o
  - cdtype :: MExp o
  - cdcont :: DeclCont o
  - cddeffreevars :: Nat
  }
- data DeclCont o
  - = Def Nat [Clause o] (Maybe Nat) (Maybe Nat)
  - | Datatype [ConstRef o] [ConstRef o]
  - | Constructor Nat
  - | Postulate
- type Clause o = ([Pat o], MExp o)
- data Pat o
  - = PatConApp (ConstRef o) [Pat o]
  - | PatVar String
  - | PatExp
- type ConstRef o = IORef (ConstDef o)
- data Elr o
  - = Var Nat
  - | Const (ConstRef o)
- getVar :: Elr o -> Maybe Nat
- getConst :: Elr o -> Maybe (ConstRef o)
- data Sort
  - = Set Nat
  - | UnknownSort
  - | Type
- data Exp o
  - = App {
    - appUId :: Maybe (UId o)
    - appOK :: OKHandle (RefInfo o)
    - appHead :: Elr o
    - appElims :: MArgList o
    }
  - | Lam Hiding (Abs (MExp o))
  - | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
  - | Sort Sort
  - | AbsurdLambda Hiding
- dontCare :: Exp o
- type MExp o = MM (Exp o) (RefInfo o)
- data ArgList o
  - = ALNil
  - | ALCons Hiding (MExp o) (MArgList o)
  - | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
  - | ALConPar (MArgList o)
- type MArgList o = MM (ArgList o) (RefInfo o)
- data WithSeenUIds a o = WithSeenUIds {
  - seenUIds :: [Maybe (UId o)]
  - rawValue :: a
  }
- type HNExp o = WithSeenUIds (HNExp' o) o
- data HNExp' o
  - = HNApp (Elr o) (ICArgList o)
  - | HNLam Hiding (Abs (ICExp o))
  - | HNPi Hiding Bool (ICExp o) (Abs (ICExp o))
  - | HNSort Sort
- data HNArgList o
  - = HNALNil
  - | HNALCons Hiding (ICExp o) (ICArgList o)
  - | HNALConPar (ICArgList o)
- data ICArgList o
  - = CALNil
  - | CALConcat (Clos (MArgList o) o) (ICArgList o)
- type ICExp o = Clos (MExp o) o
- data Clos a o = Clos [CAction o] a
- type CExp o = TrBr (ICExp o) o
- data TrBr a o = TrBr [MExp o] a
- data CAction o
  - = Sub (ICExp o)
  - | Skip
  - | Weak Nat
- type Ctx o = [(MId, CExp o)]
- type EE = IO
- detecteliminand :: [Clause o] -> Maybe Nat
- detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
- categorizedecl :: ConstRef o -> IO ()
- class MetaliseOKH t where
  - metaliseOKH :: t -> IO t
- metaliseokh :: MExp o -> IO (MExp o)
- class ExpandMetas t where
  - expandMetas :: t -> IO t
- addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
- closify :: MExp o -> CExp o
- sub :: MExp o -> CExp o -> CExp o
- subi :: MExp o -> ICExp o -> ICExp o
- weak :: Weakening t => Nat -> t -> t
- class Weakening t where
  - weak' :: Nat -> t -> t
- doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
- freeVars :: FreeVars t => t -> Set Nat
- class FreeVars t where
  - freeVarsOffset :: Nat -> t -> Set Nat
- rename :: Renaming t => (Nat -> Nat) -> t -> t
- class Renaming t where
  - renameOffset :: Nat -> (Nat -> Nat) -> t -> t

# Documentation

type UId o = Metavar (Exp o) (RefInfo o) Source #

Unique identifiers for variable occurrences in unification.

data HintMode Source #

Constructors

HMNormal |
HMRecCall |

data EqReasoningConsts o Source #

Constructors

EqReasoningConsts |

Fields

- eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o

data EqReasoningState Source #

Constructors

EqRSNone |
EqRSChain |
EqRSPrf1 |
EqRSPrf2 |
EqRSPrf3 |

Instances

Eq EqReasoningState Source # |
Instance details Defined in Agda.Auto.Syntax Methods (==) :: EqReasoningState -> EqReasoningState -> Bool Source # (/=) :: EqReasoningState -> EqReasoningState -> Bool Source #
Show EqReasoningState Source # |
Instance details Defined in Agda.Auto.Syntax Methods showsPrec :: Int -> EqReasoningState -> ShowS Source # show :: EqReasoningState -> String Source # showList :: [EqReasoningState] -> ShowS Source #

data RefInfo o Source #

The concrete instance of the `blk` parameter in `Metavar`. I.e., the information passed to the search control.

Constructors

RIEnv |

Fields

- rieHints :: [(ConstRef o, HintMode)]
- rieDefFreeVars :: Nat

  Nat - deffreevars (to make cost of using module parameters correspond to that of hints).

- rieEqReasoningConsts :: Maybe (EqReasoningConsts o)

RIMainInfo |

Fields

- riMainCxtLength :: Nat

  Size of typing context in which meta was created.

- riMainType :: HNExp o

  Head normal form of type of meta.

- riMainIota :: Bool

  True if iota steps performed when normalising target type (used to put cost when traversing a definition by construction instantiation).

RIUnifInfo [CAction o] (HNExp o) |
RICopyInfo (ICExp o) |
RIIotaStep Bool |
RIInferredTypeUnknown |
RINotConstructor |
RIUsedVars [UId o] [Elr o] |
RIPickSubsvar |
RIEqRState EqReasoningState |
RICheckElim Bool |
RICheckProjIndex [ConstRef o] |

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo 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 #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] 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 #
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 #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b 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 #
Refinable (ICExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Refinable (ArgList o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Refinable (Exp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Refinable (ConstRef o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #
Trav (ArgList o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> ArgList o -> m () Source #
Trav (Exp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> Exp o -> m () Source #
Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #
Trav (TrBr a o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> TrBr a o -> m () Source #

type MyPB o = PB (RefInfo o) Source #

type MyMB a o = MB a (RefInfo o) Source #

type Nat = Int Source #

data MId Source #

Constructors

Id String |
NoId |

Instances

Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #

data Abs a Source #

Abstraction with maybe a name.

Different from Agda, where there is also info whether function is constant.

Constructors

Abs MId a |

Instances

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 #
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 #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) Source #
Renaming t => Renaming (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #
FreeVars t => FreeVars (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Abs t -> Set Nat Source #
ExpandMetas t => ExpandMetas (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Abs t -> IO (Abs t) Source #
MetaliseOKH t => MetaliseOKH (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Abs t -> IO (Abs t) Source #
Lift t => Lift (Abs t) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Abs t -> Abs t Source #

data ConstDef o Source #

Constant signatures.

Constructors

ConstDef |

Fields

- cdname :: String

  For debug printing.

- cdorigin :: o

  Reference to the Agda constant.

- cdtype :: MExp o

  Type of constant.

- cdcont :: DeclCont o

  Constant definition.

- cddeffreevars :: Nat

  Free vars of the module where the constant is defined..

Instances

Refinable (ConstRef o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

data DeclCont o Source #

Constant definitions.

Constructors

Def Nat [Clause o] (Maybe Nat) (Maybe Nat) |
Datatype [ConstRef o] [ConstRef o] |
Constructor Nat |
Postulate |

type Clause o = ([Pat o], MExp o) Source #

data Pat o Source #

Constructors

PatConApp (ConstRef o) [Pat o] |
PatVar String |
PatExp | Dot pattern.

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion TOM (Arg Pattern) (Pat O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #

type ConstRef o = IORef (ConstDef o) Source #

data Elr o Source #

Head of application (elimination).

Constructors

Var Nat |
Const (ConstRef o) |

Instances

Eq (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods (==) :: Elr o -> Elr o -> Bool Source # (/=) :: Elr o -> Elr o -> Bool Source #
Renaming (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #
FreeVars (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Elr o -> Set Nat Source #
Weakening (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Elr o -> Elr o Source #

getVar :: Elr o -> Maybe Nat Source #

getConst :: Elr o -> Maybe (ConstRef o) Source #

data Sort Source #

Constructors

Set Nat |
UnknownSort |
Type |

data Exp o Source #

Agsy's internal syntax.

Constructors

App |

Fields

- appUId :: Maybe (UId o)

  Unique identifier of the head.

- appOK :: OKHandle (RefInfo o)

  This application has been type-checked.

- appHead :: Elr o

  Head.

- appElims :: MArgList o

  Arguments.

Lam Hiding (Abs (MExp o)) | Lambda with hiding information.
Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o)) | `True` if possibly dependent (var not known to not occur). `False` if non-dependent.
Sort Sort |
AbsurdLambda Hiding | Absurd lambda with hiding information.

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
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 #
Conversion MOT (Exp O) Type Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term 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 #
Conversion TOM [Clause] [([Pat O], MExp O)] Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Renaming (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #
FreeVars (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Exp o -> Set Nat Source #
ExpandMetas (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Exp o -> IO (Exp o) Source #
MetaliseOKH (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Exp o -> IO (Exp o) Source #
LocalTerminationEnv (MExp o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #
Lift (Exp o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Exp o -> Exp o Source #
Refinable (ICExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Refinable (Exp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Trav (Exp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> Exp o -> m () Source #
Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #

dontCare :: Exp o Source #

type MExp o = MM (Exp o) (RefInfo o) Source #

"Maybe expression": Expression or reference to meta variable.

data ArgList o Source #

Constructors

ALNil | No more eliminations.
ALCons Hiding (MExp o) (MArgList o) | Application and tail.
ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o) | proj pre args, projfcn idx, tail
ALConPar (MArgList o) | Constructor parameter (missing in Agda). Agsy has monomorphic constructors. Inserted to cover glitch of polymorphic constructor applications coming from Agda

Instances

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # |
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Unify o (ArgList o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods unify' :: ArgList o -> ArgList o -> StateT (Assignments o) Maybe () Source # notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool Source #
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 #
Renaming (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #
FreeVars (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> ArgList o -> Set Nat Source #
ExpandMetas (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: ArgList o -> IO (ArgList o) Source #
MetaliseOKH (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: ArgList o -> IO (ArgList o) Source #
LocalTerminationEnv (MArgList o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #
Lift (ArgList o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> ArgList o -> ArgList o Source #
Refinable (ArgList o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Trav (ArgList o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> ArgList o -> m () Source #

type MArgList o = MM (ArgList o) (RefInfo o) Source #

data WithSeenUIds a o Source #

Constructors

WithSeenUIds |

Fields

- seenUIds :: [Maybe (UId o)]
- rawValue :: a

type HNExp o = WithSeenUIds (HNExp' o) o Source #

data HNExp' o Source #

Constructors

HNApp (Elr o) (ICArgList o) |
HNLam Hiding (Abs (ICExp o)) |
HNPi Hiding Bool (ICExp o) (Abs (ICExp o)) |
HNSort Sort |

data HNArgList o Source #

Head-normal form of `ICArgList`. First entry is exposed.

Q: Why are there no projection eliminations?

Constructors

HNALNil |
HNALCons Hiding (ICExp o) (ICArgList o) |
HNALConPar (ICArgList o) |

data ICArgList o Source #

Lazy concatenation of argument lists under explicit substitutions.

Constructors

CALNil |
CALConcat (Clos (MArgList o) o) (ICArgList o) |

Instances

Weakening (ICArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> ICArgList o -> ICArgList o Source #

type ICExp o = Clos (MExp o) o Source #

An expression `a` in an explicit substitution `[CAction a]`.

data Clos a o Source #

Constructors

Clos [CAction o] a |

Instances

Refinable (ICExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Weakening (Clos a o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Clos a o -> Clos a o Source #
Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #

type CExp o = TrBr (ICExp o) o Source #

data TrBr a o Source #

Constructors

TrBr [MExp o] a |

Instances

Weakening a => Weakening (TrBr a o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> TrBr a o -> TrBr a o Source #
Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #
Trav (TrBr a o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> TrBr a o -> m () Source #

data CAction o Source #

Entry of an explicit substitution.

An explicit substitution is a list of `CAction`s. This is isomorphic to the usual presentation where `Skip` and `Weak` would be constructors of exp. substs.

Constructors

Sub (ICExp o) | Instantation of variable.
Skip | For going under a binder, often called Lift.
Weak Nat | Shifting substitution (going to a larger context).

type Ctx o = [(MId, CExp o)] Source #

type EE = IO Source #

detecteliminand :: [Clause o] -> Maybe Nat Source #

detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool Source #

categorizedecl :: ConstRef o -> IO () Source #

class MetaliseOKH t where Source #

Methods

metaliseOKH :: t -> IO t Source #

Instances

MetaliseOKH (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: ArgList o -> IO (ArgList o) Source #
MetaliseOKH (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Exp o -> IO (Exp o) Source #
MetaliseOKH t => MetaliseOKH (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Abs t -> IO (Abs t) Source #
MetaliseOKH t => MetaliseOKH (MM t a) Source # |
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: MM t a -> IO (MM t a) Source #

metaliseokh :: MExp o -> IO (MExp o) Source #

class ExpandMetas t where Source #

Methods

expandMetas :: t -> IO t Source #

Instances

ExpandMetas (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: ArgList o -> IO (ArgList o) Source #
ExpandMetas (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Exp o -> IO (Exp o) Source #
ExpandMetas t => ExpandMetas (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Abs t -> IO (Abs t) Source #
ExpandMetas t => ExpandMetas (MM t a) Source # |
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: MM t a -> IO (MM t a) Source #

addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o Source #

closify :: MExp o -> CExp o Source #

sub :: MExp o -> CExp o -> CExp o Source #

subi :: MExp o -> ICExp o -> ICExp o Source #

weak :: Weakening t => Nat -> t -> t Source #

class Weakening t where Source #

Methods

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

Instances

Weakening (ICArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> ICArgList o -> ICArgList o Source #
Weakening (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Elr o -> Elr o Source #
Weakening a => Weakening (TrBr a o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> TrBr a o -> TrBr a o Source #
Weakening (Clos a o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Clos a o -> Clos a o Source #

doclos :: [CAction o] -> Nat -> Either Nat (ICExp o) Source #

Substituting for a variable.

freeVars :: FreeVars t => t -> Set Nat Source #

FreeVars class and instances

class FreeVars t where Source #

Methods

freeVarsOffset :: Nat -> t -> Set Nat Source #

Instances

FreeVars (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> ArgList o -> Set Nat Source #
FreeVars (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Exp o -> Set Nat Source #
FreeVars (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Elr o -> Set Nat Source #
FreeVars t => FreeVars (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Abs t -> Set Nat Source #
(FreeVars a, FreeVars b) => FreeVars (a, b) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> (a, b) -> Set Nat Source #
FreeVars t => FreeVars (MM t a) Source # |
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> MM t a -> Set Nat Source #

rename :: Renaming t => (Nat -> Nat) -> t -> t Source #

Renaming Typeclass and instances

class Renaming t where Source #

Methods

renameOffset :: Nat -> (Nat -> Nat) -> t -> t Source #

Instances

Renaming (ArgList o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #
Renaming (Exp o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #
Renaming (Elr o) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #
Renaming t => Renaming (Abs t) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #
Renaming (CSPatI o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o Source #
Renaming t => Renaming (HI t) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t Source #
(Renaming a, Renaming b) => Renaming (a, b) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> (a, b) -> (a, b) Source #
Renaming t => Renaming (MM t a) Source # |
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a Source #