Agda.Auto.Syntax

Documentation

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

Unique identifiers for variable occurrences in unification.

data HintMode

Constructors

HMNormal

HMRecCall

data EqReasoningConsts o

Constructors

EqReasoningConsts

Fields

• eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o

data EqReasoningState

Constructors

EqRSNone

EqRSChain

EqRSPrf1

EqRSPrf2

EqRSPrf3

Instances

Eq EqReasoningState

Methods

(==) :: EqReasoningState -> EqReasoningState -> Bool

(/=) :: EqReasoningState -> EqReasoningState -> Bool

Show EqReasoningState

Methods

showsPrec :: Int -> EqReasoningState -> ShowS

show :: EqReasoningState -> String

showList :: [EqReasoningState] -> ShowS

data RefInfo o

The concrete instance of the blk parameter in Metavar. I.e., the information passed to the search control.

Constructors

RIEnv

Fields

• rieHints :: [(ConstRef o, HintMode)]
• rieDefFreeVars :: Nat

  Nat - deffreevars (to make cost of using module parameters correspond to that of hints).

• rieEqReasoningConsts :: Maybe (EqReasoningConsts o)

RIMainInfo

Fields

• riMainCxtLength :: Nat

  Size of typing context in which meta was created.

• riMainType :: HNExp o

  Head normal form of type of meta.

• riMainIota :: Bool

  True if iota steps performed when normalising target type (used to put cost when traversing a definition by construction instantiation).

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]

type MyPB o = PB (RefInfo o)

type MyMB a o = MB a (RefInfo o)

type Nat = Int

data FMode

Hiding in Agda.

Constructors

Hidden

Instance

NotHidden

Instances

Eq FMode

Methods

(==) :: FMode -> FMode -> Bool

(/=) :: FMode -> FMode -> Bool

data MId

Constructors

Id String

NoId

stringToMyId :: String -> MId

data Abs a

Abstraction with maybe a name.

Different from Agda, where there is also info whether function is constant.

Constructors

Abs MId a

data ConstDef o

Constant signatures.

Constructors

ConstDef

Fields

• cdname :: String

  For debug printing.

• cdorigin :: o

  Reference to the Agda constant.

• cdtype :: MExp o

  Type of constant.

• cdcont :: DeclCont o

  Constant definition.

• cddeffreevars :: Nat

  Free vars of the module where the constant is defined..

data DeclCont o

Constant definitions.

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

Dot pattern.

type ConstRef o = IORef (ConstDef o)

data Elr o

Head of application (elimination).

Constructors

Var Nat

Const (ConstRef o)

data Sort

Constructors

Set Nat

UnknownSort

Type

data Exp o

Agsy's internal syntax.

Constructors

App

Fields

• appUId :: Maybe (UId o)

  Unique identifier of the head.

• appOK :: OKHandle (RefInfo o)

  This application has been type-checked.

• appHead :: Elr o

  Head.

• appElims :: MArgList o

  Arguments.

Lam FMode (Abs (MExp o))

Lambda with hiding information.

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

True if possibly dependent (var not known to not occur). False if non-dependent.

Sort Sort

AbsurdLambda FMode

Absurd lambda with hiding information.

dontCare :: Exp o

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

"Maybe expression": Expression or reference to meta variable.

data ArgList o

Constructors

ALNil

No more eliminations.

ALCons FMode (MExp o) (MArgList o)

Application and tail.

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

proj pre args, projfcn idx, tail

ALConPar (MArgList o)

Constructor parameter (missing in Agda). Agsy has monomorphic constructors. Inserted to cover glitch of polymorphic constructor applications coming from Agda

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

Head-normal form of ICArgList. First entry is exposed.

Q: Why are there no projection eliminations?

Constructors

HNALNil

HNALCons FMode (ICExp o) (ICArgList o)

HNALConPar (ICArgList o)

data ICArgList o

Lazy concatenation of argument lists under explicit substitutions.

Constructors

CALNil

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

type ICExp o = Clos (MExp o) o

An expression a in an explicit substitution [CAction a].

data Clos a o

Constructors

Clos [CAction o] a

type CExp o = TrBr (ICExp o) o

data TrBr a o

Constructors

TrBr [MExp o] a

data CAction o

Entry of an explicit substitution.

An explicit substitution is a list of CActions. This is isomorphic to the usual presentation where Skip and Weak would be constructors of exp. substs.

Constructors

Sub (ICExp o)

Instantation of variable.

Skip

For going under a binder, often called Lift.

Weak Nat

Shifting substitution (going to a larger context).

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)

Substituting for a variable.