Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Infered

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 |
Instance |
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

Instances

Refinable (ConstRef o) (RefInfo o) |

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 (ICExp o) (RefInfo o) |
Refinable (Exp o) (RefInfo o) |
Trav (Exp o) (RefInfo o) |
Trav (MId, CExp o) (RefInfo o) |

dontCare :: Exp 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 |

Instances

Refinable (ICExp o) (RefInfo o) |
Trav (MId, CExp o) (RefInfo o) |

data TrBr a o

Constructors

TrBr [MExp o] a |

Instances

Trav (MId, CExp o) (RefInfo o) |
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)