Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Auto.Convert

Synopsis

Documentation

data Hint Source #

Constructors

Hint 

Fields

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 #

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

data S Source #

Constructors

S 

Fields

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 #

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.

getEqs :: TCM [(Bool, Term, Term)] 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 #

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

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

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

frommyExps :: Nat -> MArgList O -> Term -> ExceptT String IO Term Source #

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

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

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

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