Safe Haskell	None
Language	Haskell2010

Agda.Auto.Typecheck

Synopsis

tcExp :: Bool -> Ctx o -> CExp o -> MExp o -> EE (MyPB o)
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 :: Hiding -> 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
- = 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
- = 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
- = 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
- = 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 -> Prio -> 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)

Documentation

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

Typechecker drives the solution of metas.

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

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

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

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

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

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

addend :: Hiding -> MExp o -> MM (Exp o) blk -> MM (Exp o) blk Source #

copyarg :: MExp o -> Bool Source #

type HNNBlks o = [HNExp o] Source #

noblks :: HNNBlks o Source #

addblk :: HNExp o -> HNNBlks o -> HNNBlks o Source #

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

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

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

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

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

data HNRes o Source #

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) Source #

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

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

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

data PEval o Source #

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) Source #

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

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

data CMode o Source #

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 Source #

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) Source #

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

maybeor :: Bool -> Prio -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) -> IO (PB (RefInfo o)) Source #

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

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

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

pickid :: MId -> MId -> MId Source #

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