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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.FileId

Contents

- Mapping between files and their unique identifiers.
- Constructing a mapping between files and their unique identifiers.
- Monadic interface

Description

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.

Synopsis

- type File = AbsolutePath
- newtype FileId = FileId {
  - theFileId :: Word32
  }
- type FileToId = Map File FileId
- type IdToFile = EnumMap FileId File
- data FileDict = FileDict {
  - fileToId :: FileToId
  - idToFile :: IdToFile
  }
- class GetFileId a where
  - getFileId :: a -> File -> FileId
- class GetIdFile a where
  - getIdFile :: a -> FileId -> File
- data FileDictBuilder = FileDictBuilder {
  - nextFileId :: FileId
  - fileDict :: FileDict
  }
- registerFileId :: File -> FileDictBuilder -> (FileId, FileDictBuilder)
- registerFileId' :: File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder)
- registerFileId'' :: File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder)
- class Monad m => MonadFileId (m :: Type -> Type) where
  - fileFromId :: FileId -> m File
  - idFromFile :: File -> m FileId

# Documentation

type File = AbsolutePath Source #

newtype FileId Source #

Unique identifier of a file.

Constructors

FileId |

Fields

- theFileId :: Word32

#### Instances

Instances details

GetFileId FileToId Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileToId -> File -> FileId Source #
GetIdFile IdToFile Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: IdToFile -> FileId -> File Source #
NFData FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods rnf :: FileId -> () Source #
Enum FileId Source # |

Instance details

Defined in Agda.Utils.FileId

Methods

succ :: FileId -> FileId Source #

pred :: FileId -> FileId Source #

toEnum :: Int -> FileId Source #

fromEnum :: FileId -> Int Source #

enumFrom :: FileId -> [FileId] Source #

enumFromThen :: FileId -> FileId -> [FileId] Source #

enumFromTo :: FileId -> FileId -> [FileId] Source #

enumFromThenTo :: FileId -> FileId -> FileId -> [FileId] Source #

Generic FileId Source # |

Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileId |
Instance details Defined in Agda.Utils.FileId type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

Methods

from :: FileId -> Rep FileId x Source #

to :: Rep FileId x -> FileId Source #

Num FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods (+) :: FileId -> FileId -> FileId Source # (-) :: FileId -> FileId -> FileId Source # (*) :: FileId -> FileId -> FileId Source # negate :: FileId -> FileId Source # abs :: FileId -> FileId Source # signum :: FileId -> FileId Source # fromInteger :: Integer -> FileId Source #
Show FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods showsPrec :: Int -> FileId -> ShowS Source # show :: FileId -> String Source # showList :: [FileId] -> ShowS Source #
Eq FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods (==) :: FileId -> FileId -> Bool Source # (/=) :: FileId -> FileId -> Bool Source #
Ord FileId Source # |
Instance details Defined in Agda.Utils.FileId Methods compare :: FileId -> FileId -> Ordering Source # (<) :: FileId -> FileId -> Bool Source # (<=) :: FileId -> FileId -> Bool Source # (>) :: FileId -> FileId -> Bool Source # (>=) :: FileId -> FileId -> Bool Source # max :: FileId -> FileId -> FileId Source # min :: FileId -> FileId -> FileId Source #
type Rep FileId Source # |
Instance details Defined in Agda.Utils.FileId type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

# Mapping between files and their unique identifiers.

type FileToId = Map File FileId Source #

type IdToFile = EnumMap FileId File Source #

data FileDict Source #

Constructors

FileDict |

Fields

- fileToId :: FileToId
- idToFile :: IdToFile

#### Instances

Instances details

GetFileId FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileDict -> File -> FileId Source #
GetIdFile FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: FileDict -> FileId -> File Source #
Null FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods empty :: FileDict Source # null :: FileDict -> Bool Source #
NFData FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods rnf :: FileDict -> () Source #
Generic FileDict Source # |

Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileDict |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDict = D1 ('MetaData "FileDict" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDict" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileToId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileToId) :*: S1 ('MetaSel ('Just "idToFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdToFile)))

Methods

from :: FileDict -> Rep FileDict x Source #

to :: Rep FileDict x -> FileDict Source #

type Rep FileDict Source # |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDict = D1 ('MetaData "FileDict" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDict" 'PrefixI 'True) (S1 ('MetaSel ('Just "fileToId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileToId) :*: S1 ('MetaSel ('Just "idToFile") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 IdToFile)))

class GetFileId a where Source #

Translate a file to an ID; mapping must exist.

Methods

getFileId :: a -> File -> FileId Source #

#### Instances

Instances details

GetFileId FileDictWithBuiltins Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getFileId :: FileDictWithBuiltins -> File -> FileId Source #
GetFileId FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileDict -> File -> FileId Source #
GetFileId FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileDictBuilder -> File -> FileId Source #
GetFileId FileToId Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileToId -> File -> FileId Source #

class GetIdFile a where Source #

Translate a ID to a file; mapping must exist.

Methods

getIdFile :: a -> FileId -> File Source #

#### Instances

Instances details

GetIdFile FileDictWithBuiltins Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods getIdFile :: FileDictWithBuiltins -> FileId -> File Source #
GetIdFile FileDict Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: FileDict -> FileId -> File Source #
GetIdFile FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: FileDictBuilder -> FileId -> File Source #
GetIdFile IdToFile Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: IdToFile -> FileId -> File Source #

# Constructing a mapping between files and their unique identifiers.

data FileDictBuilder Source #

Constructors

FileDictBuilder |

Fields

- nextFileId :: FileId
- fileDict :: FileDict

#### Instances

Instances details

GetFileId FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getFileId :: FileDictBuilder -> File -> FileId Source #
GetIdFile FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods getIdFile :: FileDictBuilder -> FileId -> File Source #
Null FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods empty :: FileDictBuilder Source # null :: FileDictBuilder -> Bool Source #
NFData FileDictBuilder Source # |
Instance details Defined in Agda.Utils.FileId Methods rnf :: FileDictBuilder -> () Source #
Generic FileDictBuilder Source # |

Instance details

Defined in Agda.Utils.FileId

Associated Types

type Rep FileDictBuilder |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

Methods

from :: FileDictBuilder -> Rep FileDictBuilder x Source #

to :: Rep FileDictBuilder x -> FileDictBuilder Source #

type Rep FileDictBuilder Source # |

Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "FileDictBuilder" 'PrefixI 'True) (S1 ('MetaSel ('Just "nextFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileId) :*: S1 ('MetaSel ('Just "fileDict") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 FileDict)))

registerFileId :: File -> FileDictBuilder -> (FileId, FileDictBuilder) Source #

Register a new file identifier or retrieve an existing one.

registerFileId' :: File -> FileDictBuilder -> ((FileId, Bool), FileDictBuilder) Source #

Register a new file identifier (`True`) or retrieve an existing one (`False`).

registerFileId'' :: File -> FileDictBuilder -> (FileId, Maybe FileDictBuilder) Source #

Register a new file identifier or retrieve an existing one.

If `Nothing` is returned, the file was already registered.

# Monadic interface

class Monad m => MonadFileId (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

fileFromId :: FileId -> m File Source #

default fileFromId :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadFileId n, m ~ t n) => FileId -> m File Source #

idFromFile :: File -> m FileId Source #

default idFromFile :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, MonadFileId n, m ~ t n) => File -> m FileId Source #

#### Instances

Instances details

MonadFileId IM Source # |
Instance details Defined in Agda.Interaction.Monad Methods fileFromId :: FileId -> IM File Source # idFromFile :: File -> IM FileId Source #
MonadIO m => MonadFileId (TCMT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.State Methods fileFromId :: FileId -> TCMT m File Source # idFromFile :: File -> TCMT m FileId Source #
MonadFileId m => MonadFileId (ExceptT e m) Source # |
Instance details Defined in Agda.Utils.FileId Methods fileFromId :: FileId -> ExceptT e m File Source # idFromFile :: File -> ExceptT e m FileId Source #
MonadFileId m => MonadFileId (ReaderT r m) Source # |
Instance details Defined in Agda.Utils.FileId Methods fileFromId :: FileId -> ReaderT r m File Source # idFromFile :: File -> ReaderT r m FileId Source #
MonadFileId m => MonadFileId (StateT s m) Source # |
Instance details Defined in Agda.Utils.FileId Methods fileFromId :: FileId -> StateT s m File Source # idFromFile :: File -> StateT s m FileId Source #