ModuleAgda-2.8.0.2Haskell2010
Agda.Utils.FileId
Translating between file paths and ids.
This module allows you to build a dictionary from file paths to some unique identifier and to look up both file paths and identifiers in that dictionary.
Contents
Synopsis
- type File
- newtype FileId
- type FileToId
- type IdToFile
- data FileDict
- class GetFileId
- class GetIdFile
- data FileDictBuilder
- value registerFileId
- value registerFileId'
- value registerFileId''
- class MonadFileId
- PackageAgda-2.8.0.2
- Exports12
- LanguageHaskell2010
- LicenceMIT
- SourceFileId.hs
Instances10Enum, Eq, Num, Ord, Show, Generic, …
Enum FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdEq FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNum FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdOrd FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdShow FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGeneric FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNFData FileIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileToIdDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile IdToFileDefined in Agda-2.8.0.2 · Agda.Utils.FileIdtype Rep FileId = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Utils.FileId"FileId"
"Agda.Utils.FileId"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'True) (C1 ('MetaCons"FileId"
'PrefixI 'True) (S1 ('MetaSel ('Just"theFileId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))
Mapping between files and their unique identifiers.
Instances6Generic, NFData, Null, GetFileId, GetIdFile, Rep
Generic FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNFData FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNull FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdtype Rep FileDict = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Utils.FileId"FileDict"
"Agda.Utils.FileId"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"FileDict"
'PrefixI 'True) (S1 ('MetaSel ('Just"fileToId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileToId) :*: S1 ('MetaSel ('Just"idToFile"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdToFile)))
Translate a file to an ID; mapping must exist.
Methods
getFileId :: HasCallStack => a -> File -> FileId
Instances4GetFileId
GetFileId FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanGetFileId FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileToIdDefined in Agda-2.8.0.2 · Agda.Utils.FileId
Instances4GetIdFile
GetIdFile FileDictWithBuiltinsDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Base · orphanGetIdFile FileDictDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile IdToFileDefined in Agda-2.8.0.2 · Agda.Utils.FileId
Constructing a mapping between files and their unique identifiers.
Constructors
Instances6Generic, NFData, Null, GetFileId, GetIdFile, Rep
Generic FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNFData FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdNull FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetFileId FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdGetIdFile FileDictBuilderDefined in Agda-2.8.0.2 · Agda.Utils.FileIdtype Rep FileDictBuilder = D1 ('MetaDataDefined in Agda-2.8.0.2 · Agda.Utils.FileId"FileDictBuilder"
"Agda.Utils.FileId"
"Agda-2.8.0.2-9KjOINxE5a7DfnJbtdetJP"
'False) (C1 ('MetaCons"FileDictBuilder"
'PrefixI 'True) (S1 ('MetaSel ('Just"nextFileId"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just"fileDict"
) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))
Register a new file identifier or retrieve an existing one.
Register a new file identifier or retrieve an existing one.
If Nothing is returned, the file was already registered.
Monadic interface
Methods
fileFromId :: FileId -> m FileidFromFile :: File -> m FileId
Instances6MonadFileId
MonadFileId ReplMDefined in Agda-2.8.0.2 · Agda.Interaction.CommandLineMonadFileId IMDefined in Agda-2.8.0.2 · Agda.Interaction.MonadMonadIO m => MonadFileId (TCMT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.State · orphanMonadFileId m => MonadFileId (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.Utils.FileIdMonadFileId m => MonadFileId (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.Utils.FileIdMonadFileId m => MonadFileId (StateT s m)Defined in Agda-2.8.0.2 · Agda.Utils.FileId