Agda.Auto.Convert

Documentation

data Hint

Constructors

Hint

Fields

• hintIsConstructor :: Bool
• hintQName :: QName

type O = (Maybe (Int, [Arg QName]), QName)

data TMode

Constructors

TMAll

Instances

Eq TMode

Defined in Agda.Auto.Convert

Methods

(==) :: TMode -> TMode -> Bool

(/=) :: TMode -> TMode -> Bool

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

Constructors

S

Fields

• sConsts :: MapS QName (TMode, ConstRef O)
• sMetas :: MapS MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
• sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
• sCurMeta :: Maybe MetaId
• sMainMeta :: MetaId

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b)

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

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.

getMeta :: MetaId -> TOM (Metavar (Exp O) (RefInfo O))

getEqs :: TCM [(Bool, Term, Term)]

literalsNotImplemented :: TCM a

hitsNotImplemented :: TCM a

class Conversion (m :: Type -> Type) a b where

Methods

convert :: a -> m b

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Conversion MOT a b => Conversion MOT (Abs a) (Abs b)

Defined in Agda.Auto.Convert

Methods

convert :: Abs a -> MOT (Abs b)

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b)

Defined in Agda.Auto.Convert

Methods

convert :: Arg a -> TOM (Hiding, b)

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT 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)