Safe Haskell	None
Language	Haskell2010

Agda.Auto.Convert

Documentation

data Hint #

Constructors

Hint
Fields hintIsConstructor :: Bool hintQName :: QName

type O = (Maybe Int, QName) #

data TMode #

Constructors

TMAll

Instances

Eq TMode #
Instance details 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)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
Conversion TOM (Arg Pattern) (Pat O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) #
Instance details 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 #

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

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

copatternsNotImplemented :: TCM a #

literalsNotImplemented :: TCM a #

class Conversion m a b where #

Minimal complete definition

convert

Methods

convert :: a -> m b #

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
Conversion MOT (Exp O) Type #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type #
Conversion MOT (Exp O) Term #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term #
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
Conversion TOM (Arg Pattern) (Pat O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) #
Conversion TOM a b => Conversion TOM (Arg a) (Hiding, b) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg a -> TOM (Hiding, b) #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b #
Instance details 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) #