Core.Name.Namespace

Definitions

data Namespace : Type

  Nested namespaces are stored in reverse order.
  i.e. `X.Y.Z.foo` will be represented as `NS [Z,Y,X] foo`
  As a consequence we hide the representation behind an opaque type alias
  and force users to manufacture and manipulate namespaces via the safe
  functions we provide.

Totality: total
Visibility: export
Constructor: 

MkNS : List String -> Namespace

Hints:

DecEq Namespace

Eq Namespace

Hashable Namespace

Injective MkNS

Ord Namespace

Pretty Void Namespace

Show Namespace

TTC Namespace

data ModuleIdent : Type

  A Module Identifier is, similarly to a namespace, stored inside out.

Totality: total
Visibility: export
Constructor: 

MkMI : List String -> ModuleIdent

Hints:

Eq ModuleIdent

Ord ModuleIdent

Pretty Void ModuleIdent

Show ModuleIdent

TTC ModuleIdent

miAsNamespace : ModuleIdent -> Namespace

  Sometimes we need to convert a module identifier to the corresponding
  namespace. It is still useful to have them as distinct types as it
  clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
  namespace in `import X.Y.Z as S.T.U`.

Totality: total
Visibility: export

nsAsModuleIdent : Namespace -> ModuleIdent

  Sometimes we need to convert a namespace to the corresponding
  module identifier. It is still useful to have them as distinct types as
  it clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
  namespace in `import X.Y.Z as S.T.U`.

Totality: total
Visibility: export

mkNamespacedIdent : String -> (Maybe Namespace, String)

Totality: total
Visibility: export

mkNestedNamespace : Maybe Namespace -> String -> Namespace

Totality: total
Visibility: export

mkNamespace : String -> Namespace

Totality: total
Visibility: export

mkModuleIdent : Maybe Namespace -> String -> ModuleIdent

Totality: total
Visibility: export

(<.>) : Namespace -> Namespace -> Namespace

  Extend an existing namespace with additional name parts to form a more local one.
  e.g. `X.Y.Z <.> S.T.U` to get `X.Y.Z.S.T.U`.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

replace : ModuleIdent -> Namespace -> Namespace -> Namespace

Totality: total
Visibility: export

unsafeUnfoldNamespace : Namespace -> List String

  Use at your own risks!

Totality: total
Visibility: export

unsafeFoldNamespace : List String -> Namespace

Totality: total
Visibility: export

unsafeUnfoldModuleIdent : ModuleIdent -> List String

Totality: total
Visibility: export

unsafeFoldModuleIdent : List String -> ModuleIdent

Totality: total
Visibility: export

toPath : ModuleIdent -> String

  A.B.C -> "A/B/C"

Totality: total
Visibility: export

parent : ModuleIdent -> Maybe ModuleIdent

Totality: total
Visibility: export

allParents : Namespace -> List Namespace

  Nested namespaces naturally give rise to a hierarchical structure. In particular
  from a given namespace we can compute all of the parent (aka englobing) ones.
  For instance `allParents Data.List.Properties` should yield a set containing
  both `Data.List` and `Data` (no guarantee is given on the order).

Totality: total
Visibility: export

isParentOf : Namespace -> Namespace -> Bool

  We can check whether a given namespace is a parent (aka englobing) namespace
  of a candidate namespace.
  We expect that `all (\ p => isParentOf p ns) (allParents ns)` holds true.

Totality: total
Visibility: export

isApproximationOf : Namespace -> Namespace -> Bool

  When writing qualified names users often do not want to spell out the full
  namespace, rightly considering that an unambiguous segment should be enough.
  This function checks whether a candidate is an approximation of a given
  namespace.
  We expect `isApproximationOf List.Properties Data.List.Properties` to hold true
  while `isApproximationOf Data.List Data.List.Properties` should not.

Totality: total
Visibility: export

isInPathOf : String -> Namespace -> Bool

  We can check whether a given string (assumed to be a valid Namespace ident)
  is in the path of a given namespace.

Totality: total
Visibility: export

showSep : String -> List String -> String

Totality: total
Visibility: export

showNSWithSep : String -> Namespace -> String

Totality: total
Visibility: export

emptyNS : Namespace

  This is used when evaluating things in the REPL

Totality: total
Visibility: export

mainNS : Namespace

Totality: total
Visibility: export

partialEvalNS : Namespace

Totality: total
Visibility: export

builtinNS : Namespace

Totality: total
Visibility: export

preludeNS : Namespace

Totality: total
Visibility: export

numNS : Namespace

Totality: total
Visibility: export

typesNS : Namespace

Totality: total
Visibility: export

basicsNS : Namespace

Totality: total
Visibility: export

eqOrdNS : Namespace

Totality: total
Visibility: export

primIONS : Namespace

Totality: total
Visibility: export

ioNS : Namespace

Totality: total
Visibility: export

reflectionNS : Namespace

Totality: total
Visibility: export

reflectionTTNS : Namespace

Totality: total
Visibility: export

reflectionTTImpNS : Namespace

Totality: total
Visibility: export

dpairNS : Namespace

Totality: total
Visibility: export

natNS : Namespace

Totality: total
Visibility: export