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]

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Type (MExp O)

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Replace o (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp o)

Conversion TOM [Clause] [([Pat O], MExp O)]

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Unify o t => Unify o (MM t (RefInfo o))

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments o) Maybe ()

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT * (Nat, Nat) (StateT (Assignments o) IO) Bool

Replace o t u => Replace o (MM t (RefInfo o)) u

Methods

replace' :: Nat -> MExp o -> MM t (RefInfo o) -> Reader (Nat, Nat) u

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Methods

convert :: MM a (RefInfo O) -> MOT b

LocalTerminationEnv (MArgList o)

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

LocalTerminationEnv (MExp o)

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

type MyPB o = PB (RefInfo o)

type MyMB a o = MB a (RefInfo o)

type Nat = Int

data MId

Constructors

Id String

NoId

data Abs a

Abstraction with maybe a name.

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

Constructors

Abs MId a

Instances

Unify o t => Unify o (Abs t)

Methods

unify' :: Abs t -> Abs t -> StateT (Assignments o) Maybe ()

notequal' :: Abs t -> Abs t -> ReaderT * (Nat, Nat) (StateT (Assignments o) IO) Bool

Replace o t u => Replace o (Abs t) (Abs u)

Methods

replace' :: Nat -> MExp o -> Abs t -> Reader (Nat, Nat) (Abs u)

Conversion MOT a b => Conversion MOT (Abs a) (Abs b)

Methods

convert :: Abs a -> MOT (Abs b)

Renaming t => Renaming (Abs t)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t

FreeVars t => FreeVars (Abs t)

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat

ExpandMetas t => ExpandMetas (Abs t)

Methods

expandMetas :: Abs t -> IO (Abs t)

MetaliseOKH t => MetaliseOKH (Abs t)

Methods

metaliseOKH :: Abs t -> IO (Abs t)

Lift t => Lift (Abs t)

Methods

lift' :: Nat -> Nat -> Abs t -> Abs t

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.

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM [Clause] [([Pat O], MExp O)]

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion TOM (Arg Pattern) (Pat O)

Methods

convert :: Arg Pattern -> TOM (Pat O)

type ConstRef o = IORef (ConstDef o)

data Elr o

Head of application (elimination).

Constructors

Var Nat

Const (ConstRef o)

Instances

Eq (Elr o)

Methods

(==) :: Elr o -> Elr o -> Bool

(/=) :: Elr o -> Elr o -> Bool

Renaming (Elr o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o

FreeVars (Elr o)

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat

Weakening (Elr o)

Methods

weak' :: Nat -> Elr o -> Elr o

getVar :: Elr o -> Maybe Nat

getConst :: Elr o -> Maybe (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 Hiding (Abs (MExp o))

Lambda with hiding information.

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

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

Sort Sort

AbsurdLambda Hiding

Absurd lambda with hiding information.

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Type (MExp O)

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Term (MExp O)

Methods

convert :: Term -> TOM (MExp O)

Unify o (Exp o)

Methods

unify' :: Exp o -> Exp o -> StateT (Assignments o) Maybe ()

notequal' :: Exp o -> Exp o -> ReaderT * (Nat, Nat) (StateT (Assignments o) IO) Bool

Conversion MOT (Exp O) Type

Methods

convert :: Exp O -> MOT Type

Conversion MOT (Exp O) Term

Methods

convert :: Exp O -> MOT Term

Replace o (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp o)

Conversion TOM [Clause] [([Pat O], MExp O)]

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Renaming (Exp o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o

FreeVars (Exp o)

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat

ExpandMetas (Exp o)

Methods

expandMetas :: Exp o -> IO (Exp o)

MetaliseOKH (Exp o)

Methods

metaliseOKH :: Exp o -> IO (Exp o)

LocalTerminationEnv (MExp o)

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

Lift (Exp o)

Methods

lift' :: Nat -> Nat -> Exp o -> Exp o

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 Hiding (MExp o) (MArgList o)

Application and tail.

ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (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

Instances

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Unify o (ArgList o)

Methods

unify' :: ArgList o -> ArgList o -> StateT (Assignments o) Maybe ()

notequal' :: ArgList o -> ArgList o -> ReaderT * (Nat, Nat) (StateT (Assignments o) IO) Bool

Replace o (ArgList o) (ArgList o)

Methods

replace' :: Nat -> MExp o -> ArgList o -> Reader (Nat, Nat) (ArgList o)

Renaming (ArgList o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o

FreeVars (ArgList o)

Methods

freeVarsOffset :: Nat -> ArgList o -> Set Nat

ExpandMetas (ArgList o)

Methods

expandMetas :: ArgList o -> IO (ArgList o)

MetaliseOKH (ArgList o)

Methods

metaliseOKH :: ArgList o -> IO (ArgList o)

LocalTerminationEnv (MArgList o)

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

Lift (ArgList o)

Methods

lift' :: Nat -> Nat -> ArgList o -> ArgList o

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

data WithSeenUIds a o

Constructors

WithSeenUIds

Fields

• seenUIds :: [Maybe (UId o)]
• rawValue :: a

type HNExp o = WithSeenUIds (HNExp' o) o

data HNExp' o

Constructors

HNApp (Elr o) (ICArgList o)

HNLam Hiding (Abs (ICExp o))

HNPi Hiding 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 Hiding (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)

Instances

Weakening (ICArgList o)

Methods

weak' :: Nat -> ICArgList 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

Instances

Weakening (Clos a o)

Methods

weak' :: Nat -> Clos a o -> Clos a o

type CExp o = TrBr (ICExp o) o

data TrBr a o

Constructors

TrBr [MExp o] a

Instances

Weakening a => Weakening (TrBr a o)

Methods

weak' :: Nat -> TrBr a o -> TrBr a o

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 ()

class MetaliseOKH t where

Minimal complete definition

metaliseOKH

Methods

metaliseOKH :: t -> IO t

Instances

MetaliseOKH (ArgList o)

Methods

metaliseOKH :: ArgList o -> IO (ArgList o)

MetaliseOKH (Exp o)

Methods

metaliseOKH :: Exp o -> IO (Exp o)

MetaliseOKH t => MetaliseOKH (Abs t)

Methods

metaliseOKH :: Abs t -> IO (Abs t)

MetaliseOKH t => MetaliseOKH (MM t a)

Methods

metaliseOKH :: MM t a -> IO (MM t a)

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

class ExpandMetas t where

Minimal complete definition

expandMetas

Methods

expandMetas :: t -> IO t

Instances

ExpandMetas (ArgList o)

Methods

expandMetas :: ArgList o -> IO (ArgList o)

ExpandMetas (Exp o)

Methods

expandMetas :: Exp o -> IO (Exp o)

ExpandMetas t => ExpandMetas (Abs t)

Methods

expandMetas :: Abs t -> IO (Abs t)

ExpandMetas t => ExpandMetas (MM t a)

Methods

expandMetas :: MM t a -> IO (MM t a)

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 :: Weakening t => Nat -> t -> t

class Weakening t where

Minimal complete definition

weak'

Methods

weak' :: Nat -> t -> t

Instances

Weakening (ICArgList o)

Methods

weak' :: Nat -> ICArgList o -> ICArgList o

Weakening (Elr o)

Methods

weak' :: Nat -> Elr o -> Elr o

Weakening a => Weakening (TrBr a o)

Methods

weak' :: Nat -> TrBr a o -> TrBr a o

Weakening (Clos a o)

Methods

weak' :: Nat -> Clos a o -> Clos a o

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

Substituting for a variable.

freeVars :: FreeVars t => t -> Set Nat

FreeVars class and instances

class FreeVars t where

Minimal complete definition

freeVarsOffset

Methods

freeVarsOffset :: Nat -> t -> Set Nat

Instances

FreeVars (ArgList o)

Methods

freeVarsOffset :: Nat -> ArgList o -> Set Nat

FreeVars (Exp o)

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat

FreeVars (Elr o)

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat

FreeVars t => FreeVars (Abs t)

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat

(FreeVars a, FreeVars b) => FreeVars (a, b)

Methods

freeVarsOffset :: Nat -> (a, b) -> Set Nat

FreeVars t => FreeVars (MM t a)

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat

rename :: Renaming t => (Nat -> Nat) -> t -> t

Renaming Typeclass and instances

class Renaming t where

Minimal complete definition

renameOffset

Methods

renameOffset :: Nat -> (Nat -> Nat) -> t -> t

Instances

Renaming (ArgList o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o

Renaming (Exp o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o

Renaming (Elr o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o

Renaming t => Renaming (Abs t)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t

Renaming (CSPatI o)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o

Renaming t => Renaming (HI t)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t

(Renaming a, Renaming b) => Renaming (a, b)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> (a, b) -> (a, b)

Renaming t => Renaming (MM t a)

Methods

renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a