Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Auto.Convert

Documentation

data Hint Source #

Constructors

Hint
Fields hintIsConstructor :: Bool hintQName :: QName

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

data TMode Source #

Constructors

TMAll

Instances

Instances details

Eq TMode Source #
Instance details Defined in Agda.Auto.Convert Methods (==) :: TMode -> TMode -> Bool # (/=) :: TMode -> TMode -> Bool #

type MapS a b = (Map a b, [a]) Source #

initMapS :: MapS a b Source #

popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b) Source #

data S Source #

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

Instances details

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

type TOM = StateT S TCM Source #

type MOT = ExceptT String IO 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 #

getConst :: Bool -> QName -> TMode -> TOM (ConstRef O) Source #

getdfv :: MetaId -> QName -> TCM Nat Source #

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

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

copatternsNotImplemented :: TCM a Source #

literalsNotImplemented :: TCM a Source #

hitsNotImplemented :: TCM a Source #

class Conversion m a b where Source #

Methods

convert :: a -> m b Source #

Instances

Instances details

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

tomyIneq :: Comparison -> Bool Source #

fmType :: MetaId -> Type -> Bool Source #

fmExp :: MetaId -> Term -> Bool Source #

fmExps :: MetaId -> Args -> Bool Source #

fmLevel :: MetaId -> PlusLevel -> Bool Source #

icnvh :: Hiding -> ArgInfo Source #

frommyExps :: Nat -> MArgList O -> Term -> ExceptT String IO Term 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 #

frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO Clause Source #

contains_constructor :: [CSPat O] -> Bool Source #

freeIn :: Nat -> MExp o -> Bool Source #

negtype :: ConstRef o -> MExp o -> MExp o Source #

findClauseDeep :: InteractionId -> TCM (Maybe (QName, Clause, Bool)) Source #

matchType :: Int -> Int -> Type -> Type -> Maybe (Nat, Nat) Source #