| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Agda.Auto.Syntax
- type UId o = Metavar (Exp o) (RefInfo o)
- data HintMode
- data EqReasoningConsts o = EqReasoningConsts {}
- data EqReasoningState
- data RefInfo o
- = RIEnv {
- rieHints :: [(ConstRef o, HintMode)]
- rieDefFreeVars :: Nat
- rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
- | RIMainInfo {
- riMainCxtLength :: Nat
- riMainType :: HNExp o
- riMainIota :: Bool
- | 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]
- = RIEnv {
- type MyPB o = PB (RefInfo o)
- type MyMB a o = MB a (RefInfo o)
- type Nat = Int
- data FMode
- data MId
- stringToMyId :: String -> MId
- data Abs a = Abs MId a
- data ConstDef o = ConstDef {}
- data DeclCont o
- type Clause o = ([Pat o], MExp o)
- data Pat o
- type ConstRef o = IORef (ConstDef o)
- data Elr o
- data Sort
- = Set Nat
- | UnknownSort
- | Type
- data Exp o
- dontCare :: Exp o
- type MExp o = MM (Exp o) (RefInfo o)
- data ArgList o
- type MArgList o = MM (ArgList o) (RefInfo o)
- data HNExp o
- data HNArgList o
- data ICArgList o
- type ICExp o = Clos (MExp o) o
- data Clos a o = Clos [CAction o] a
- type CExp o = TrBr (ICExp o) o
- data TrBr a o = TrBr [MExp o] a
- data CAction o
- 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)
Documentation
type UId o = Metavar (Exp o) (RefInfo o) Source
Unique identifiers for variable occurrences in unification.
data EqReasoningConsts o Source
data EqReasoningState Source
Instances
The concrete instance of the blk parameter in Metavar.
I.e., the information passed to the search control.
Constructors
| RIEnv | |
Fields
| |
| RIMainInfo | |
Fields
| |
| 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] | |
stringToMyId :: String -> MId Source
Abstraction with maybe a name.
Different from Agda, where there is also info whether function is constant.
Constant signatures.
Constructors
| ConstDef | |
Constant definitions.
Agsy's internal syntax.
type MExp o = MM (Exp o) (RefInfo o) Source
"Maybe expression": Expression or reference to meta variable.
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 |
Head-normal form of ICArgList. First entry is exposed.
Q: Why are there no projection eliminations?
Lazy concatenation of argument lists under explicit substitutions.
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.
detecteliminand :: [Clause o] -> Maybe Nat Source
categorizedecl :: ConstRef o -> IO () Source
metaliseokh :: MExp o -> IO (MExp o) Source
weakarglist :: Nat -> ICArgList o -> ICArgList o Source