
   0 | module Core.Name
   1 | 
   2 | import Data.Maybe
   3 | import Data.String
   4 | import Libraries.Decidable.Equality as L
   5 | import Libraries.Text.PrettyPrint.Prettyprinter
   6 | import Libraries.Text.PrettyPrint.Prettyprinter.Util
   7 | import Libraries.Utils.String
   8 | 
   9 | import Libraries.Text.Distance.Levenshtein as Distance
  10 | 
  11 | import public Core.Name.Namespace
  12 | 
  13 | %default total
  14 | 
  15 | ||| A username has some structure
  16 | public export
  17 | data UserName : Type where
  18 |   Basic : String -> UserName -- default name constructor       e.g. map
  19 |   Field : String -> UserName -- field accessor                 e.g. .fst
  20 |   Underscore : UserName      -- no name                        e.g. _
  21 | 
  22 | %name UserName un
  23 | 
  24 | ||| A smart constructor taking a string and parsing it as the appropriate
  25 | ||| username
  26 | export
  27 | mkUserName : String -> UserName
  28 | mkUserName "_" = Underscore
  29 | mkUserName str with (strM str)
  30 |   mkUserName _   | StrCons '.' n = Field n
  31 |   mkUserName str | _             = Basic str
  32 | 
  33 | ||| Name helps us track a name's structure as well as its origin:
  34 | ||| was it user-provided or machine-manufactured? For what reason?
  35 | public export
  36 | data Name : Type where
  37 |      NS : Namespace -> Name -> Name -- in a namespace
  38 |      UN : UserName -> Name -- user defined name
  39 |      MN : String -> Int -> Name -- machine generated name
  40 |      PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
  41 |      DN : String -> Name -> Name -- a name and how to display it
  42 |      Nested : (Int, Int) -> Name -> Name -- nested function name
  43 |      CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
  44 |      WithBlock : String -> Int -> Name -- with block nested in (resolved) name
  45 |      Resolved : Int -> Name -- resolved, index into context
  46 | 
  47 | %name Name n
  48 | 
  49 | export
  50 | mkNamespacedName : Maybe Namespace -> UserName -> Name
  51 | mkNamespacedName Nothing nm = UN nm
  52 | mkNamespacedName (Just ns) nm = NS ns (UN nm)
  53 | 
  54 | ||| `matches a b` checks that the name `a` matches `b` assuming
  55 | ||| the name roots are already known to be matching.
  56 | ||| For instance, both `reverse` and `List.reverse` match the fully
  57 | ||| qualified name `Data.List.reverse`.
  58 | export
  59 | matches : Name -> Name -> Bool
  60 | matches (NS ns _) (NS cns _) = isApproximationOf ns cns
  61 | matches (NS {}) _
  62 |   -- gallais: I don't understand this case but that's what was there.
  63 |   = True -- no in library name, so root doesn't match
  64 | matches _ _ = True -- no prefix, so root must match, so good
  65 | 
  66 | -- Update a name imported with 'import as', for creating an alias
  67 | export
  68 | asName : ModuleIdent -> -- Initial module name
  69 |          Namespace -> -- 'as' module name
  70 |          Name -> -- identifier
  71 |          Name
  72 | asName old new (DN s n) = DN s (asName old new n)
  73 | asName old new (NS ns n)
  74 |     = NS (replace old new ns) n
  75 | asName _ _ n = n
  76 | 
  77 | export
  78 | userNameRoot : Name -> Maybe UserName
  79 | userNameRoot (NS _ n) = userNameRoot n
  80 | userNameRoot (UN n) = Just n
  81 | userNameRoot (DN _ n) = userNameRoot n
  82 | userNameRoot _ = Nothing
  83 | 
  84 | export
  85 | isOpChar : Char -> Bool
  86 | isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")
  87 | 
  88 | export
  89 | ||| Test whether a user name begins with an operator symbol.
  90 | isOpUserName : UserName -> Bool
  91 | isOpUserName (Basic n) = fromMaybe False $ do
  92 |    c <- fst <$> strUncons n
  93 |    guard (isOpChar c)
  94 |    pure True
  95 | isOpUserName (Field _) = False
  96 | isOpUserName Underscore = False
  97 | 
  98 | export
  99 | ||| Test whether a name begins with an operator symbol.
 100 | isOpName : Name -> Bool
 101 | isOpName = maybe False isOpUserName . userNameRoot
 102 | 
 103 | export
 104 | isUnderscoreName : Name -> Bool
 105 | isUnderscoreName (UN Underscore) = True
 106 | isUnderscoreName (MN "_" _) = True
 107 | isUnderscoreName _ = False
 108 | 
 109 | export
 110 | isPatternVariable : UserName -> Bool
 111 | isPatternVariable (Basic nm) = lowerFirst nm
 112 | isPatternVariable (Field _) = False
 113 | isPatternVariable Underscore = True
 114 | 
 115 | export
 116 | isUserName : Name -> Bool
 117 | isUserName (PV {}) = False
 118 | isUserName (MN {}) = False
 119 | isUserName (NS _ n) = isUserName n
 120 | isUserName (DN _ n) = isUserName n
 121 | isUserName _ = True
 122 | 
 123 | ||| True iff name can be traced back to a source name.
 124 | ||| Used to determine whether it needs semantic highlighting.
 125 | export
 126 | isSourceName : Name -> Bool
 127 | isSourceName (NS _ n) = isSourceName n
 128 | isSourceName (UN {}) = True
 129 | isSourceName (MN {}) = False
 130 | isSourceName (PV n _) = isSourceName n
 131 | isSourceName (DN _ n) = isSourceName n
 132 | isSourceName (Nested _ n) = isSourceName n
 133 | isSourceName (CaseBlock {}) = False
 134 | isSourceName (WithBlock {}) = False
 135 | isSourceName (Resolved {}) = False
 136 | 
 137 | export
 138 | isRF : Name -> Maybe (Namespace, String)
 139 | isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n)
 140 | isRF (UN (Field n)) = Just (emptyNS, n)
 141 | isRF _ = Nothing
 142 | 
 143 | export
 144 | isUN : Name -> Maybe (Namespace, UserName)
 145 | isUN (UN un) = Just (emptyNS, un)
 146 | isUN (NS ns n) = map (mapFst (ns <.>)) (isUN n)
 147 | isUN _ = Nothing
 148 | 
 149 | export
 150 | isBasic : UserName -> Maybe String
 151 | isBasic (Basic str) = Just str
 152 | isBasic _ = Nothing
 153 | 
 154 | export
 155 | isField : UserName -> Maybe String
 156 | isField (Field str) = Just str
 157 | isField _ = Nothing
 158 | 
 159 | export
 160 | caseFn : Name -> Bool
 161 | caseFn (CaseBlock {}) = True
 162 | caseFn (DN _ n) = caseFn n
 163 | caseFn (NS _ n) = caseFn n
 164 | caseFn _ = False
 165 | 
 166 | 
 167 | export
 168 | displayUserName : UserName -> String
 169 | displayUserName (Basic n) = n
 170 | displayUserName (Field n) = n
 171 | displayUserName Underscore = "_"
 172 | 
 173 | export
 174 | nameRoot : Name -> String
 175 | nameRoot (NS _ n) = nameRoot n
 176 | nameRoot (UN n) = displayUserName n
 177 | nameRoot (MN n _) = n
 178 | nameRoot (PV n _) = nameRoot n
 179 | nameRoot (DN _ n) = nameRoot n
 180 | nameRoot (Nested _ inner) = nameRoot inner
 181 | nameRoot (CaseBlock n _) = "$" ++ show n
 182 | nameRoot (WithBlock n _) = "$" ++ show n
 183 | nameRoot (Resolved i) = "$" ++ show i
 184 | 
 185 | export
 186 | displayName : Name -> (Maybe Namespace, String)
 187 | displayName (NS ns n) = mapFst (pure . maybe ns (ns <.>)) $ displayName n
 188 | displayName (UN n) = (Nothing, displayUserName n)
 189 | displayName (MN n _) = (Nothing, n)
 190 | displayName (PV n _) = displayName n
 191 | displayName (DN n _) = (Nothing, n)
 192 | displayName (Nested _ n) = displayName n
 193 | displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer)
 194 | displayName (WithBlock outer _) = (Nothing, "with block in " ++ show outer)
 195 | displayName (Resolved i) = (Nothing, "$resolved" ++ show i)
 196 | 
 197 | export
 198 | splitNS : Name -> (Namespace, Name)
 199 | splitNS (NS ns nm) = mapFst (ns <.>) (splitNS nm)
 200 | splitNS nm = (emptyNS, nm)
 201 | 
 202 | --- Drop a namespace from a name
 203 | export
 204 | dropNS : Name -> Name
 205 | dropNS (NS _ n) = n
 206 | dropNS n = n
 207 | 
 208 | -- Drop all of the namespaces from a name
 209 | export
 210 | dropAllNS : Name -> Name
 211 | dropAllNS (NS _ n) = dropAllNS n
 212 | dropAllNS n = n
 213 | 
 214 | export
 215 | mbApplyNS : Maybe Namespace -> Name -> Name
 216 | mbApplyNS Nothing n = n
 217 | mbApplyNS (Just ns) n = NS ns n
 218 | 
 219 | export
 220 | isUnsafeBuiltin : Name -> Bool
 221 | isUnsafeBuiltin nm = case splitNS nm of
 222 |   (ns, UN (Basic str)) =>
 223 |        (ns == builtinNS || ns == emptyNS)
 224 |     && any {t = List} id
 225 |            [ "assert_" `isPrefixOf` str
 226 |            , str `elem` [ "prim__believe_me", "believe_me"
 227 |                         , "prim__crash", "idris_crash"
 228 |                         ]
 229 |            ]
 230 |   _ => False
 231 | 
 232 | export
 233 | Show UserName where
 234 |   show (Basic n) = n
 235 |   show (Field n) = "." ++ n
 236 |   show Underscore = "_"
 237 | 
 238 | export
 239 | Show Name where
 240 |   show (NS ns n@(UN (Field _))) = show ns ++ ".(" ++ show n ++ ")"
 241 |   show (NS ns (UN (Basic n))) = if any isOpChar (unpack n)
 242 |                        then "\{show ns}.(\{n})"
 243 |                        else "\{show ns}.\{n}"
 244 |   show (NS ns n) = "\{show ns}.\{show n}"
 245 |   show (UN x) = show x
 246 |   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
 247 |   show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
 248 |   show (DN str n) = str
 249 |   show (Nested (outer, idx) inner)
 250 |       = show outer ++ ":" ++ show idx ++ ":" ++ show inner
 251 |   show (CaseBlock outer i) = "case block in " ++ outer
 252 |   show (WithBlock outer i) = "with block in " ++ outer
 253 |   show (Resolved x) = "$resolved" ++ show x
 254 | 
 255 | export
 256 | [RawUN] Show UserName where
 257 |   showPrec d (Basic n) = showCon d "Basic " n
 258 |   showPrec d (Field n) = showCon d "Field " n
 259 |   showPrec d Underscore = "Underscore"
 260 | 
 261 | export
 262 | covering
 263 | [Raw] Show Name where
 264 |   showPrec d (NS ns n) = showCon d "NS" $ showArg ns ++ showArg n
 265 |   showPrec d (UN x) = showCon d "UN" $ showArg @{RawUN} x
 266 |   showPrec d (MN x y) = showCon d "MN" $ showArg x ++ showArg y
 267 |   showPrec d (PV n i) = showCon d "PV" $ showArg n ++ showArg i
 268 |   showPrec d (DN str n) = showCon d "DN" $ showArg str ++ showArg n
 269 |   showPrec d (Nested ij n) = showCon d "Nested" $ showArg ij ++ showArg n
 270 |   showPrec d (CaseBlock str i) = showCon d "CaseBlock" $ showArg str ++ showArg i
 271 |   showPrec d (WithBlock str i) = showCon d "WithBlock" $ showArg str ++ showArg i
 272 |   showPrec d (Resolved i) = showCon d "Resolved" $ showArg i
 273 | 
 274 | export
 275 | Pretty Void UserName where
 276 |   pretty (Basic n) = pretty n
 277 |   pretty (Field n) = "." <+> pretty n
 278 |   pretty Underscore = "_"
 279 | 
 280 | export
 281 | ||| Will it be an operation once prettily displayed?
 282 | ||| The first boolean states whether the operator is prefixed.
 283 | isPrettyOp : Bool -> Name -> Bool
 284 | isPrettyOp b (UN nm@(Field _)) = b -- prefixed fields need to be parenthesised
 285 | isPrettyOp b (UN nm@(Basic _)) = isOpUserName nm
 286 | isPrettyOp b (DN str _) = isOpUserName (Basic str)
 287 | isPrettyOp b nm = False
 288 | 
 289 | mutual
 290 | 
 291 |   export
 292 |   covering
 293 |   prettyOp : Bool -> Name -> Doc Void
 294 |   prettyOp b nm = parenthesise (isPrettyOp b nm) (pretty nm)
 295 | 
 296 |   export
 297 |   covering
 298 |   Pretty Void Name where
 299 |     pretty (NS ns n) = pretty ns <+> dot <+> prettyOp True n
 300 |     pretty (UN x) = pretty x
 301 |     pretty (MN x y) = braces (pretty x <+> colon <+> byShow y)
 302 |     pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> byShow d)
 303 |     pretty (DN str _) = pretty str
 304 |     pretty (Nested (outer, idx) inner)
 305 |       = byShow outer <+> colon <+> byShow idx <+> colon <+> pretty inner
 306 |     pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
 307 |     pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
 308 |     pretty (Resolved x) = pretty "$resolved" <+> pretty (show x)
 309 | 
 310 | export
 311 | Eq UserName where
 312 |   (==) (Basic x) (Basic y) = x == y
 313 |   (==) (Field x) (Field y) = x == y
 314 |   (==) Underscore Underscore = True
 315 |   (==) _ _ = False
 316 | 
 317 | export
 318 | Eq Name where
 319 |     (==) (NS ns n) (NS ns' n') = n == n' && ns == ns'
 320 |     (==) (UN x) (UN y) = x == y
 321 |     (==) (MN x y) (MN x' y') = y == y' && x == x'
 322 |     (==) (PV x y) (PV x' y') = x == x' && y == y'
 323 |     (==) (DN _ n) (DN _ n') = n == n'
 324 |     (==) (Nested x y) (Nested x' y') = x == x' && y == y'
 325 |     (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
 326 |     (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
 327 |     (==) (Resolved x) (Resolved x') = x == x'
 328 |     (==) _ _ = False
 329 | 
 330 | usernameTag : UserName -> Int
 331 | usernameTag (Basic _) = 0
 332 | usernameTag (Field _) = 2
 333 | usernameTag Underscore = 3
 334 | 
 335 | export
 336 | Ord UserName where
 337 |   compare (Basic x) (Basic y) = compare x y
 338 |   compare (Field x) (Field y) = compare x y
 339 |   compare Underscore Underscore = EQ
 340 |   compare x y = compare (usernameTag x) (usernameTag y)
 341 | 
 342 | nameTag : Name -> Int
 343 | nameTag (NS {}) = 0
 344 | nameTag (UN {}) = 1
 345 | nameTag (MN {}) = 2
 346 | nameTag (PV {}) = 3
 347 | nameTag (DN {}) = 4
 348 | nameTag (Nested {}) = 6
 349 | nameTag (CaseBlock {}) = 7
 350 | nameTag (WithBlock {}) = 8
 351 | nameTag (Resolved {}) = 9
 352 | 
 353 | export
 354 | Ord Name where
 355 |     compare (NS x y) (NS x' y')
 356 |         = case compare y y' of -- Compare base name first (more likely to differ)
 357 |                EQ => compare x x'
 358 |                -- Because of the terrible way Idris 1 compiles 'case', this
 359 |                -- is actually faster than just having 't => t'...
 360 |                GT => GT
 361 |                LT => LT
 362 |     compare (UN x) (UN y) = compare x y
 363 |     compare (MN x y) (MN x' y')
 364 |         = case compare y y' of
 365 |                EQ => compare x x'
 366 |                GT => GT
 367 |                LT => LT
 368 |     compare (PV x y) (PV x' y')
 369 |         = case compare y y' of
 370 |                EQ => compare x x'
 371 |                GT => GT
 372 |                LT => LT
 373 |     compare (DN _ n) (DN _ n') = compare n n'
 374 |     compare (Nested x y) (Nested x' y')
 375 |         = case compare y y' of
 376 |                EQ => compare x x'
 377 |                GT => GT
 378 |                LT => LT
 379 |     compare (CaseBlock x y) (CaseBlock x' y')
 380 |         = case compare y y' of
 381 |                EQ => compare x x'
 382 |                GT => GT
 383 |                LT => LT
 384 |     compare (WithBlock x y) (WithBlock x' y')
 385 |         = case compare y y' of
 386 |                EQ => compare x x'
 387 |                GT => GT
 388 |                LT => LT
 389 |     compare (Resolved x) (Resolved y) = compare x y
 390 | 
 391 |     compare x y = compare (nameTag x) (nameTag y)
 392 | 
 393 | 
 394 | export
 395 | userNameEq : (x, y : UserName) -> Maybe (x = y)
 396 | userNameEq (Basic x) (Basic y) = L.maybeCong Basic (L.maybeEq x y)
 397 | userNameEq (Field x) (Field y) = L.maybeCong Field (L.maybeEq x y)
 398 | userNameEq Underscore Underscore = Just Refl
 399 | userNameEq _ _ = Nothing
 400 | 
 401 | 
 402 | export
 403 | nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
 404 | nameEq (NS xs x) (NS ys y) = L.maybeCong2 NS (L.maybeEq xs ys) (nameEq x y)
 405 | nameEq (UN x) (UN y) = L.maybeCong UN (userNameEq x y)
 406 | nameEq (MN x t) (MN x' t') = L.maybeCong2 MN (L.maybeEq x x') (L.maybeEq t t')
 407 | nameEq (PV x t) (PV y t') = L.maybeCong2 PV (nameEq x y) (L.maybeEq t t')
 408 | nameEq (DN x t) (DN y t') = L.maybeCong2 DN (L.maybeEq x y) (nameEq t t')
 409 | nameEq (Nested x y) (Nested x' y') = L.maybeCong2 Nested (L.maybeEq x x') (nameEq y y')
 410 | nameEq (CaseBlock x y) (CaseBlock x' y') = L.maybeCong2 CaseBlock (L.maybeEq x x') (L.maybeEq y y')
 411 | nameEq (WithBlock x y) (WithBlock x' y') = L.maybeCong2 WithBlock (L.maybeEq x x') (L.maybeEq y y')
 412 | nameEq (Resolved x) (Resolved y) = L.maybeCong Resolved (L.maybeEq x y)
 413 | nameEq _ _ = Nothing
 414 | 
 415 | export
 416 | namesEq : (xs, ys : List Name) -> Maybe (xs = ys)
 417 | namesEq [] [] = Just Refl
 418 | namesEq (x :: xs) (y :: ys) = L.maybeCong2 (::) (nameEq x y) (namesEq xs ys)
 419 | namesEq _ _ = Nothing
 420 | 
 421 | ||| Generate the next machine name
 422 | export
 423 | next : Name -> Name
 424 | next (MN n i) = MN n (i + 1)
 425 | next (UN n) = MN (show n) 0
 426 | next (NS ns n) = NS ns (next n)
 427 | next n = MN (show n) 0
 428 | 
 429 | ||| levenstein distance that needs to be reached in order for a
 430 | ||| namespace path to closely match another one.
 431 | closeNamespaceDistance : Nat
 432 | closeNamespaceDistance = 3
 433 | 
 434 | ||| Check if two strings are close enough to be similar, using the namespace
 435 | ||| distance criteria.
 436 | closeDistance : String -> String -> IO Bool
 437 | closeDistance s1 s2 = pure (!(Distance.compute s1 s2) < closeNamespaceDistance)
 438 | 
 439 | ||| Check if the test closely match the reference.
 440 | ||| We only check for namespaces and user-defined names.
 441 | export
 442 | closeMatch : (test, reference : Name) -> IO Bool
 443 | closeMatch (NS pathTest nameTest) (NS pathRef nameRef)
 444 |   = let extractNameString = toList . (map snd . isUN >=> isBasic)
 445 |         unfoldedTest = unsafeUnfoldNamespace pathTest ++ extractNameString nameTest
 446 |         unfoldedRef = unsafeUnfoldNamespace pathRef ++ extractNameString nameRef
 447 |         tests : IO (List Nat) = traverse (uncurry Distance.compute) (zip unfoldedTest unfoldedRef)
 448 |     in map ((<= closeNamespaceDistance) . sum) tests
 449 | closeMatch (UN (Basic test)) (UN (Basic ref)) = closeDistance test ref
 450 | closeMatch _ _ = pure False
 451 | 
 452 |