
   0 | module Core.Name.Namespace
   1 | 
   2 | import Data.List
   3 | import Data.String
   4 | import Decidable.Equality
   5 | import Libraries.Data.String.Extra
   6 | import Libraries.Text.PrettyPrint.Prettyprinter
   7 | import Libraries.Utils.Path
   8 | 
   9 | %default total
  10 | 
  11 | -------------------------------------------------------------------------------------
  12 | -- TYPES
  13 | -------------------------------------------------------------------------------------
  14 | 
  15 | ||| Nested namespaces are stored in reverse order.
  16 | ||| i.e. `X.Y.Z.foo` will be represented as `NS [Z,Y,X] foo`
  17 | ||| As a consequence we hide the representation behind an opaque type alias
  18 | ||| and force users to manufacture and manipulate namespaces via the safe
  19 | ||| functions we provide.
  20 | export
  21 | data Namespace : Type where
  22 |   MkNS : List String -> Namespace
  23 | 
  24 | %name Namespace ns
  25 | 
  26 | ||| A Module Identifier is, similarly to a namespace, stored inside out.
  27 | export
  28 | data ModuleIdent : Type where
  29 |   MkMI : List String -> ModuleIdent
  30 | 
  31 | %name Namespace mi
  32 | 
  33 | ||| Sometimes we need to convert a module identifier to the corresponding
  34 | ||| namespace. It is still useful to have them as distinct types as it
  35 | ||| clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
  36 | ||| namespace in `import X.Y.Z as S.T.U`.
  37 | export
  38 | miAsNamespace : ModuleIdent -> Namespace
  39 | miAsNamespace (MkMI mi) = MkNS mi
  40 | 
  41 | ||| Sometimes we need to convert a namespace to the corresponding
  42 | ||| module identifier. It is still useful to have them as distinct types as
  43 | ||| it clarifies the distinct roles of X.Y.Z as a module name vs. S.T.U as a
  44 | ||| namespace in `import X.Y.Z as S.T.U`.
  45 | export
  46 | nsAsModuleIdent : Namespace -> ModuleIdent
  47 | nsAsModuleIdent (MkNS ns) = MkMI ns
  48 | 
  49 | -------------------------------------------------------------------------------------
  50 | -- SMART CONSTRUCTORS
  51 | -------------------------------------------------------------------------------------
  52 | 
  53 | export
  54 | mkNamespacedIdent : String -> (Maybe Namespace, String)
  55 | mkNamespacedIdent str
  56 |     = let nns = reverse (split (== '.') str)
  57 |           name = head nns
  58 |           ns = tail nns in
  59 |           case ns of
  60 |                [] => (Nothing, name)
  61 |                _ => (Just (MkNS ns), name)
  62 | 
  63 | export
  64 | mkNestedNamespace : Maybe Namespace -> String -> Namespace
  65 | mkNestedNamespace Nothing n = MkNS [n]
  66 | mkNestedNamespace (Just (MkNS ns)) n = MkNS (n :: ns)
  67 | 
  68 | export
  69 | mkNamespace : String -> Namespace
  70 | mkNamespace ""  = MkNS []
  71 | mkNamespace str = uncurry mkNestedNamespace (mkNamespacedIdent str)
  72 | 
  73 | export
  74 | mkModuleIdent : Maybe Namespace -> String -> ModuleIdent
  75 | mkModuleIdent Nothing n = MkMI [n]
  76 | mkModuleIdent (Just (MkNS ns)) n = MkMI (n :: ns)
  77 | 
  78 | -------------------------------------------------------------------------------------
  79 | -- MANIPULATING NAMESPACES
  80 | -------------------------------------------------------------------------------------
  81 | 
  82 | ||| Extend an existing namespace with additional name parts to form a more local one.
  83 | ||| e.g. `X.Y.Z <.> S.T.U` to get `X.Y.Z.S.T.U`.
  84 | export
  85 | (<.>) : (existing, local : Namespace) -> Namespace
  86 | (MkNS existing) <.> (MkNS local)
  87 |    -- The namespaces are stored in reverse order so the local should end up at
  88 |    -- the front of the existing one
  89 |    = MkNS (local ++ existing)
  90 | 
  91 | export
  92 | replace : (old : ModuleIdent) -> (new, ns : Namespace) -> Namespace
  93 | replace (MkMI old) (MkNS new) (MkNS ns) = MkNS (go ns) where
  94 | 
  95 |   go : List String -> List String
  96 |   go [] = []
  97 |   go (m :: ms)
  98 |         = if old == (m :: ms)
  99 |              then new
 100 |              else m :: go ms
 101 | 
 102 | ||| Use at your own risks!
 103 | export
 104 | unsafeUnfoldNamespace : Namespace -> List String
 105 | unsafeUnfoldNamespace (MkNS ns) = ns
 106 | 
 107 | export
 108 | unsafeFoldNamespace : List String -> Namespace
 109 | unsafeFoldNamespace = MkNS
 110 | 
 111 | export
 112 | unsafeUnfoldModuleIdent : ModuleIdent -> List String
 113 | unsafeUnfoldModuleIdent (MkMI ns) = ns
 114 | 
 115 | export
 116 | unsafeFoldModuleIdent : List String -> ModuleIdent
 117 | unsafeFoldModuleIdent = MkMI
 118 | 
 119 | namespace ModuleIdent
 120 |   ||| A.B.C -> "A/B/C"
 121 |   export
 122 |   toPath : ModuleIdent -> String
 123 |   toPath = joinPath . reverse . unsafeUnfoldModuleIdent
 124 | 
 125 |   export
 126 |   parent : ModuleIdent -> Maybe ModuleIdent
 127 |   parent (MkMI (_::rest)) = Just $ MkMI rest
 128 |   parent _ = Nothing
 129 | 
 130 | -------------------------------------------------------------------------------------
 131 | -- HIERARCHICAL STRUCTURE
 132 | -------------------------------------------------------------------------------------
 133 | 
 134 | -- We don't use the prefix/suffix terminology as it is confusing: are we talking
 135 | -- about the namespaces or their representation? Instead our library is structured
 136 | -- around the parent/child relation induced by nested namespaces.
 137 | 
 138 | ||| Nested namespaces naturally give rise to a hierarchical structure. In particular
 139 | ||| from a given namespace we can compute all of the parent (aka englobing) ones.
 140 | ||| For instance `allParents Data.List.Properties` should yield a set containing
 141 | ||| both `Data.List` and `Data` (no guarantee is given on the order).
 142 | export
 143 | allParents : Namespace -> List Namespace
 144 | allParents (MkNS ns) = go ns where
 145 | 
 146 |   go : List String -> List Namespace
 147 |   go [] = []
 148 |   go (n :: ns) = MkNS (n :: ns) :: go ns
 149 | 
 150 | ||| We can check whether a given namespace is a parent (aka englobing) namespace
 151 | ||| of a candidate namespace.
 152 | ||| We expect that `all (\ p => isParentOf p ns) (allParents ns)` holds true.
 153 | export
 154 | isParentOf : (given, candidate : Namespace) -> Bool
 155 | isParentOf (MkNS ms) (MkNS ns)
 156 |   -- This is not a typo: namespaces are stored in reverse order so a namespace is
 157 |   -- a prefix of another if its reversed list of identifiers is a suffix of that
 158 |   -- other's list of identifiers
 159 |   = isSuffixOf ms ns
 160 | 
 161 | ||| When writing qualified names users often do not want to spell out the full
 162 | ||| namespace, rightly considering that an unambiguous segment should be enough.
 163 | ||| This function checks whether a candidate is an approximation of a given
 164 | ||| namespace.
 165 | ||| We expect `isApproximationOf List.Properties Data.List.Properties` to hold true
 166 | ||| while `isApproximationOf Data.List Data.List.Properties` should not.
 167 | export
 168 | isApproximationOf : (given, candidate : Namespace) -> Bool
 169 | isApproximationOf (MkNS ms) (MkNS ns)
 170 |   -- This is not a typo: namespaces are stored in reverse order so a namespace matches
 171 |   -- the end of another if its representation as a list of identifiers is a prefix of
 172 |   -- the other's.
 173 |   = isPrefixOf ms ns
 174 | 
 175 | ||| We can check whether a given string (assumed to be a valid Namespace ident)
 176 | ||| is in the path of a given namespace.
 177 | export
 178 | isInPathOf : (i : String) -> (candidate : Namespace) -> Bool
 179 | isInPathOf i (MkNS ns) = i `elem` ns
 180 | 
 181 | -------------------------------------------------------------------------------------
 182 | -- INSTANCES
 183 | -------------------------------------------------------------------------------------
 184 | 
 185 | export
 186 | Eq Namespace where
 187 |   (MkNS ms) == (MkNS ns) = ms == ns
 188 | 
 189 | export
 190 | Eq ModuleIdent where
 191 |   (MkMI ms) == (MkMI ns) = ms == ns
 192 | 
 193 | export
 194 | Ord Namespace where
 195 |     compare (MkNS ms) (MkNS ns) = compare ms ns
 196 | 
 197 | export
 198 | Ord ModuleIdent where
 199 |     compare (MkMI ms) (MkMI ns) = compare ms ns
 200 | 
 201 | Injective MkNS where
 202 |   injective Refl = Refl
 203 | 
 204 | export
 205 | DecEq Namespace where
 206 |   decEq (MkNS ms) (MkNS ns) = decEqCong (decEq ms ns)
 207 | 
 208 | -- TODO: move somewhere more appropriate
 209 | export
 210 | showSep : String -> List String -> String
 211 | showSep sep = Libraries.Data.String.Extra.join sep
 212 | 
 213 | export
 214 | showNSWithSep : String -> Namespace -> String
 215 | showNSWithSep sep (MkNS ns) = showSep sep (reverse ns)
 216 | 
 217 | export
 218 | Show Namespace where
 219 |   show = showNSWithSep "."
 220 | 
 221 | export
 222 | Show ModuleIdent where
 223 |   show = showNSWithSep "." . miAsNamespace
 224 | 
 225 | export
 226 | Pretty Void Namespace where
 227 |   pretty (MkNS ns) = concatWith (surround dot) (pretty <$> reverse ns)
 228 | 
 229 | export
 230 | Pretty Void ModuleIdent where
 231 |   pretty = pretty . miAsNamespace
 232 | 
 233 | 
 234 | -------------------------------------------------------------------------------------
 235 | -- CONSTANTS
 236 | -------------------------------------------------------------------------------------
 237 | 
 238 | ||| This is used when evaluating things in the REPL
 239 | export
 240 | emptyNS : Namespace
 241 | emptyNS = mkNamespace ""
 242 | 
 243 | export
 244 | mainNS : Namespace
 245 | mainNS = mkNamespace "Main"
 246 | 
 247 | export
 248 | partialEvalNS : Namespace
 249 | partialEvalNS = mkNamespace "_PE"
 250 | 
 251 | export
 252 | builtinNS : Namespace
 253 | builtinNS = mkNamespace "Builtin"
 254 | 
 255 | export
 256 | preludeNS : Namespace
 257 | preludeNS = mkNamespace "Prelude"
 258 | 
 259 | export
 260 | numNS : Namespace
 261 | numNS = mkNamespace "Prelude.Num"
 262 | 
 263 | export
 264 | typesNS : Namespace
 265 | typesNS = mkNamespace "Prelude.Types"
 266 | 
 267 | export
 268 | basicsNS : Namespace
 269 | basicsNS = mkNamespace "Prelude.Basics"
 270 | 
 271 | export
 272 | eqOrdNS : Namespace
 273 | eqOrdNS = mkNamespace "Prelude.EqOrd"
 274 | 
 275 | export
 276 | primIONS : Namespace
 277 | primIONS = mkNamespace "PrimIO"
 278 | 
 279 | export
 280 | ioNS : Namespace
 281 | ioNS = mkNamespace "Prelude.IO"
 282 | 
 283 | export
 284 | reflectionNS : Namespace
 285 | reflectionNS = mkNamespace "Language.Reflection"
 286 | 
 287 | export
 288 | reflectionTTNS : Namespace
 289 | reflectionTTNS = mkNamespace "Language.Reflection.TT"
 290 | 
 291 | export
 292 | reflectionTTImpNS : Namespace
 293 | reflectionTTImpNS = mkNamespace "Language.Reflection.TTImp"
 294 | 
 295 | export
 296 | dpairNS : Namespace
 297 | dpairNS = mkNamespace "Builtin.DPair"
 298 | 
 299 | export
 300 | natNS : Namespace
 301 | natNS = mkNamespace "Data.Nat"
 302 |