Agda.Auto.Typecheck

Documentation

tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)

Typechecker drives the solution of metas.

getDatatype :: ICExp o -> EE (MyMB (Maybe (ICArgList o, [ConstRef o])) o)

constructorImpossible :: ICArgList o -> ConstRef o -> EE (MyPB o)

unequals :: ICArgList o -> ICArgList o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)

unequal :: ICExp o -> ICExp o -> ([(Nat, HNExp o)] -> EE (MyPB o)) -> [(Nat, HNExp o)] -> EE (MyPB o)

traversePi :: Int -> ICExp o -> EE (MyMB (HNExp o) o)

tcargs :: Nat -> Bool -> Ctx o -> CExp o -> MArgList o -> MExp o -> Bool -> (CExp o -> MExp o -> EE (MyPB o)) -> EE (MyPB o)

addend :: FMode -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk

copyarg :: MExp o -> Bool

type HNNBlks o = [HNExp o]

noblks :: HNNBlks o

addblk :: HNExp o -> HNNBlks o -> HNNBlks o

hnn :: ICExp o -> EE (MyMB (HNExp o) o)

hnn_blks :: ICExp o -> EE (MyMB (HNExp o, HNNBlks o) o)

hnn_checkstep :: ICExp o -> EE (MyMB (HNExp o, Bool) o)

hnn' :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o, HNNBlks o) o)

hnb :: ICExp o -> ICArgList o -> EE (MyMB (HNExp o) o)

data HNRes o

Constructors

HNDone (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)

HNMeta (ICExp o) (ICArgList o) [Maybe (UId o)]

hnc :: Bool -> ICExp o -> ICArgList o -> [Maybe (UId o)] -> EE (MyMB (HNRes o) o)

hnarglist :: ICArgList o -> EE (MyMB (HNArgList o) o)

getNArgs :: Nat -> ICArgList o -> EE (MyMB (Maybe ([ICExp o], ICArgList o)) o)

getAllArgs :: ICArgList o -> EE (MyMB [ICExp o] o)

data PEval o

Constructors

PENo (ICExp o)

PEConApp (ICExp o) (ConstRef o) [PEval o]

iotastep :: Bool -> HNExp o -> EE (MyMB (Either (ICExp o, ICArgList o) (HNNBlks o)) o)

noiotastep :: HNExp o -> EE (MyPB o)

noiotastep_term :: ConstRef o -> MArgList o -> EE (MyPB o)

data CMode o

Constructors

CMRigid (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)

forall b . Refinable b (RefInfo o) => CMFlex (MM b (RefInfo o)) (CMFlex o)

data CMFlex o

Constructors

CMFFlex (ICExp o) (ICArgList o) [Maybe (UId o)]

CMFSemi (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)

CMFBlocked (Maybe (Metavar (Exp o) (RefInfo o))) (HNExp o)

comp' :: forall o. Bool -> CExp o -> CExp o -> EE (MyPB o)

checkeliminand :: MExp o -> EE (MyPB o)

maybeor :: Bool -> Int -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o))

iotapossmeta :: ICExp o -> ICArgList o -> EE Bool

meta_not_constructor :: ICExp o -> EE (MB Bool (RefInfo o))

calcEqRState :: EqReasoningConsts o -> MExp o -> EE (MyPB o)

pickid :: MId -> MId -> MId

tcSearch :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)