Agda.Auto.Syntax

Documentation

type UId o = Metavar (Exp o) (RefInfo o)

data HintMode

Constructors

HMNormal

HMRecCall

data EqReasoningConsts o

Constructors

EqReasoningConsts

Fields

eqrcId :: ConstRef o

eqrcBegin :: ConstRef o

eqrcStep :: ConstRef o

eqrcEnd :: ConstRef o

eqrcSym :: ConstRef o

eqrcCong :: ConstRef o

data EqReasoningState

Constructors

EqRSNone

EqRSChain

EqRSPrf1

EqRSPrf2

EqRSPrf3

Instances

Eq EqReasoningState

Show EqReasoningState

data RefInfo o

Constructors

RIEnv

Fields

rieHints :: [(ConstRef o, HintMode)]

rieDefFreeVars :: Nat

rieEqReasoningConsts :: Maybe (EqReasoningConsts o)

RIMainInfo Nat (HNExp o) Bool

forall a . RIUnifInfo [CAction o] (HNExp o)

RICopyInfo (ICExp o)

RIIotaStep Bool

RIInferredTypeUnknown

RINotConstructor

RIUsedVars [UId o] [Elr o]

RIPickSubsvar

RIEqRState EqReasoningState

RICheckElim Bool

RICheckProjIndex [ConstRef o]

Instances

Refinable (ICExp o) (RefInfo o)

Refinable (ArgList o) (RefInfo o)

Refinable (Exp o) (RefInfo o)

Refinable (ConstRef o) (RefInfo o)

Trav (ArgList o) (RefInfo o)

Trav (Exp o) (RefInfo o)

Trav (MId, CExp o) (RefInfo o)

Trav (TrBr a o) (RefInfo o)

type MyPB o = PB (RefInfo o)

type MyMB a o = MB a (RefInfo o)

type Nat = Int

data FMode

Constructors

Hidden

NotHidden

Instances

Eq FMode

data MId

Constructors

Id String

NoId

Instances

Trav (MId, CExp o) (RefInfo o)

data Abs a

Constructors

Abs MId a

data ConstDef o

Constructors

ConstDef

Fields

cdname :: String

cdorigin :: o

cdtype :: MExp o

cdcont :: DeclCont o

cddeffreevars :: Nat

data DeclCont o

Constructors

Def Nat [Clause o] (Maybe Nat) (Maybe Nat)

Datatype [ConstRef o] [ConstRef o]

Constructor Nat

Postulate

type Clause o = ([Pat o], MExp o)

data Pat o

Constructors

PatConApp (ConstRef o) [Pat o]

PatVar String

PatExp

type ConstRef o = IORef (ConstDef o)

data Elr o

Constructors

Var Nat

Const (ConstRef o)

data Sort

Constructors

Set Nat

UnknownSort

Type

data Exp o

Constructors

App (Maybe (UId o)) (OKHandle (RefInfo o)) (Elr o) (MArgList o)

Lam FMode (Abs (MExp o))

Pi (Maybe (UId o)) FMode Bool (MExp o) (Abs (MExp o))

Sort Sort

AbsurdLambda FMode

Instances

Refinable (Exp o) (RefInfo o)

Trav (Exp o) (RefInfo o)

type MExp o = MM (Exp o) (RefInfo o)

data ArgList o

Constructors

ALNil

ALCons FMode (MExp o) (MArgList o)

ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) FMode (MArgList o)

ALConPar (MArgList o)

Instances

Refinable (ArgList o) (RefInfo o)

Trav (ArgList o) (RefInfo o)

type MArgList o = MM (ArgList o) (RefInfo o)

data HNExp o

Constructors

HNApp [Maybe (UId o)] (Elr o) (ICArgList o)

HNLam [Maybe (UId o)] FMode (Abs (ICExp o))

HNPi [Maybe (UId o)] FMode Bool (ICExp o) (Abs (ICExp o))

HNSort Sort

data HNArgList o

Constructors

HNALNil

HNALCons FMode (ICExp o) (ICArgList o)

HNALConPar (ICArgList o)

type ICExp o = Clos (MExp o) o

type CExp o = TrBr (ICExp o) o

data ICArgList o

Constructors

CALNil

CALConcat (Clos (MArgList o) o) (ICArgList o)

data Clos a o

Constructors

Clos [CAction o] a

data TrBr a o

Constructors

TrBr [MExp o] a

Instances

Trav (TrBr a o) (RefInfo o)

data CAction o

Constructors

Sub (ICExp o)

Skip

Weak Nat

type Ctx o = [(MId, CExp o)]

type EE = IO

detecteliminand :: [Clause o] -> Maybe Nat

detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool

categorizedecl :: ConstRef o -> IO ()

metaliseokh :: MExp o -> IO (MExp o)

expandExp :: MExp o -> IO (MExp o)

addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o

closify :: MExp o -> CExp o

sub :: MExp o -> CExp o -> CExp o

subi :: MExp o -> ICExp o -> ICExp o

weak :: Nat -> CExp o -> CExp o

weaki :: Nat -> Clos a o -> Clos a o

weakarglist :: Nat -> ICArgList o -> ICArgList o

weakelr :: Nat -> Elr o -> Elr o

doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)