| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Auto.Convert
Synopsis
- data Hint = Hint {
- hintIsConstructor :: Bool
- hintQName :: QName
- type O = (Maybe (Int, [Arg QName]), QName)
- data TMode = TMAll
- type MapS a b = (Map a b, [a])
- initMapS :: MapS a b
- popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
- data S = S {}
- type TOM = StateT S TCM
- type MOT = ExceptT String IO
- tomy :: MetaId -> [Hint] -> [Type] -> TCM ([ConstRef O], [MExp O], Map MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]), [(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O))
- getConst :: Bool -> QName -> TMode -> TOM (ConstRef O)
- getdfv :: MetaId -> QName -> TCM Nat
- lookupLocalMetaAuto :: MetaId -> TCM MetaVariable
- getMeta :: MetaId -> TOM (Metavar (Exp O) (RefInfo O))
- getEqs :: TCM [(Bool, Term, Term)]
- literalsNotImplemented :: TCM a
- hitsNotImplemented :: TCM a
- class Conversion m a b where
- convert :: a -> m b
- tomyIneq :: Comparison -> Bool
- fmType :: MetaId -> Type -> Bool
- fmExp :: MetaId -> Term -> Bool
- fmExps :: MetaId -> Args -> Bool
- fmLevel :: MetaId -> PlusLevel -> Bool
- icnvh :: Hiding -> ArgInfo
- frommyExps :: Nat -> MArgList O -> Term -> ExceptT String IO Term
- abslamvarname :: String
- modifyAbstractExpr :: Expr -> Expr
- modifyAbstractClause :: Clause -> Clause
- constructPats :: Map QName (TMode, ConstRef O) -> MetaId -> Clause -> TCM ([(Hiding, MId)], [CSPat O])
- frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO Clause
- contains_constructor :: [CSPat O] -> Bool
- freeIn :: Nat -> MExp o -> Bool
- negtype :: ConstRef o -> MExp o -> MExp o
- findClauseDeep :: InteractionId -> TCM (Maybe (QName, Clause, Bool))
- matchType :: Int -> Int -> Type -> Type -> Maybe (Nat, Nat)
Documentation
Constructors
| TMAll |
Constructors
| S | |
Instances
| Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |
| Conversion TOM Term (MExp O) Source # | |
| Conversion TOM Type (MExp O) Source # | |
| Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # | |
| Conversion TOM (Arg Pattern) (Pat O) Source # | |
| Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
tomy :: MetaId -> [Hint] -> [Type] -> TCM ([ConstRef O], [MExp O], Map MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]), [(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O)) Source #
lookupLocalMetaAuto :: MetaId -> TCM MetaVariable Source #
A variant of lookupLocalMeta that, if applied to a remote
meta-variable, raises a special error message noting that remote
meta-variables are not handled by the auto command.
literalsNotImplemented :: TCM a Source #
hitsNotImplemented :: TCM a Source #
class Conversion m a b where Source #
Instances
| Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # | |
| Conversion TOM Term (MExp O) Source # | |
| Conversion TOM Type (MExp O) Source # | |
| Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # | |
| Conversion MOT (Exp O) Term Source # | |
| Conversion MOT (Exp O) Type Source # | |
| Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # | |
| Conversion TOM (Arg Pattern) (Pat O) Source # | |
| Conversion TOM [Clause] [([Pat O], MExp O)] Source # | |
| Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) Source # | |
| Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # | |
tomyIneq :: Comparison -> Bool Source #
abslamvarname :: String Source #
modifyAbstractExpr :: Expr -> Expr Source #
modifyAbstractClause :: Clause -> Clause Source #
constructPats :: Map QName (TMode, ConstRef O) -> MetaId -> Clause -> TCM ([(Hiding, MId)], [CSPat O]) Source #
contains_constructor :: [CSPat O] -> Bool Source #
findClauseDeep :: InteractionId -> TCM (Maybe (QName, Clause, Bool)) Source #