Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.FileId

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

Documentation

type File = AbsolutePath Source #

newtype FileId Source #

Unique identifier of a file.

Constructors

FileId 

Fields

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

Enum FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

succ :: FileId -> FileId #

pred :: FileId -> FileId #

toEnum :: Int -> FileId #

fromEnum :: FileId -> Int #

enumFrom :: FileId -> [FileId] #

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

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

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

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-inplace" 'True) (C1 ('MetaCons "FileId" 'PrefixI 'True) (S1 ('MetaSel ('Just "theFileId") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Word32)))

Methods

from :: FileId -> Rep FileId x #

to :: Rep FileId x -> FileId #

Num FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

(+) :: FileId -> FileId -> FileId #

(-) :: FileId -> FileId -> FileId #

(*) :: FileId -> FileId -> FileId #

negate :: FileId -> FileId #

abs :: FileId -> FileId #

signum :: FileId -> FileId #

fromInteger :: Integer -> FileId #

Show FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

showsPrec :: Int -> FileId -> ShowS #

show :: FileId -> String #

showList :: [FileId] -> ShowS #

Eq FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

(==) :: FileId -> FileId -> Bool #

(/=) :: FileId -> FileId -> Bool #

Ord FileId Source # 
Instance details

Defined in Agda.Utils.FileId

Methods

compare :: FileId -> FileId -> Ordering #

(<) :: FileId -> FileId -> Bool #

(<=) :: FileId -> FileId -> Bool #

(>) :: FileId -> FileId -> Bool #

(>=) :: FileId -> FileId -> Bool #

max :: FileId -> FileId -> FileId #

min :: FileId -> FileId -> FileId #

type Rep FileId Source # 
Instance details

Defined in Agda.Utils.FileId

type Rep FileId = D1 ('MetaData "FileId" "Agda.Utils.FileId" "Agda-2.8.0-inplace" '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

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

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-inplace" '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 #

to :: Rep FileDict x -> FileDict #

type Rep FileDict Source # 
Instance details

Defined in Agda.Utils.FileId

type Rep FileDict = D1 ('MetaData "FileDict" "Agda.Utils.FileId" "Agda-2.8.0-inplace" '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

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

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-inplace" '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 #

to :: Rep FileDictBuilder x -> FileDictBuilder #

type Rep FileDictBuilder Source # 
Instance details

Defined in Agda.Utils.FileId

type Rep FileDictBuilder = D1 ('MetaData "FileDictBuilder" "Agda.Utils.FileId" "Agda-2.8.0-inplace" '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 #