0 | -- like name map, but able to return ambiguous names
  1 | module Libraries.Data.ANameMap
  2 |
  3 | import Core.Name
  4 |
  5 | import Libraries.Data.NameMap
  6 | import Libraries.Data.UserNameMap
  7 |
  8 | %default total
  9 |
 10 | export
 11 | record ANameMap a where
 12 |      constructor MkANameMap
 13 |      -- for looking up by exact (completely qualified) names
 14 |      exactNames : NameMap a
 15 |      -- for looking up by name root or partially qualified (so possibly
 16 |      -- ambiguous) names. This doesn't store machine generated names.
 17 |      hierarchy : UserNameMap (List (Name, a))
 18 |
 19 | export
 20 | empty : ANameMap a
 21 | empty = MkANameMap empty empty
 22 |
 23 | ||| Given a Name, and an ANameMap, look up that name exactly
 24 | export
 25 | lookupExact : Name -> ANameMap a -> Maybe a
 26 | lookupExact n dict = lookup n (exactNames dict)
 27 |
 28 | export
 29 | lookupName : Name -> ANameMap a -> List (Name, a)
 30 | lookupName n dict
 31 |     = case userNameRoot n of
 32 |            Nothing => case lookupExact n dict of
 33 |                            Nothing => []
 34 |                            Just res => [(n, res)]
 35 |            Just r => case lookup r (hierarchy dict) of
 36 |                           Nothing => []
 37 |                           Just ns => filter (matches n . fst) ns
 38 |
 39 | addToHier : Name -> a ->
 40 |             UserNameMap (List (Name, a)) -> UserNameMap (List (Name, a))
 41 | addToHier n val hier
 42 |      -- Only add user defined names. Machine generated names can only be
 43 |      -- found with the exactNames
 44 |      = case userNameRoot n of
 45 |             Nothing => hier
 46 |             Just root =>
 47 |                  case lookup root hier of
 48 |                       Nothing => insert root [(n, val)] hier
 49 |                       Just ns => insert root (update val ns) hier
 50 |   where
 51 |     update : a -> List (Name, a) -> List (Name, a)
 52 |     update val [] = [(n, val)]
 53 |     update val (old :: xs)
 54 |       = if n == fst old
 55 |           then (n, val) :: xs
 56 |           else old :: update val xs
 57 |
 58 | export
 59 | addName : Name -> a -> ANameMap a -> ANameMap a
 60 | addName n val (MkANameMap dict hier)
 61 |      = let dict' = insert n val dict
 62 |            hier' = addToHier n val hier in
 63 |            MkANameMap dict' hier'
 64 |
 65 | ||| Remove a fully qualified name
 66 | export
 67 | removeExact : Show a => Name -> ANameMap a -> ANameMap a
 68 | removeExact n (MkANameMap dict hier)
 69 |     = let dict' = delete n dict
 70 |           n' = userNameRoot n
 71 |           hier' = maybe hier
 72 |                      (\foundName => deleteFromList foundName hier) n'
 73 |       in MkANameMap dict' hier'
 74 |   where
 75 |     -- When we find the list of namespace candidates, we need to remove the one that we are pointing
 76 |     -- at and leave the others untouched. We do this by filtering the list of candidates and removing
 77 |     -- the one that matches the namespace of the given name `n`. While we're using `filter`, there should
 78 |     -- only be one of them.
 79 |     deleteFromList : (un : UserName) -> (um : UserNameMap (List (Name, a))) -> UserNameMap (List (Name, a))
 80 |     deleteFromList un = adjust un (filter (\(key, _) => not $ key `matches` n))
 81 |
 82 | export
 83 | toList : ANameMap a -> List (Name, a)
 84 | toList dict = toList (exactNames dict)
 85 |
 86 | ||| Export the list of name which are ambiguous without their namespace
 87 | export
 88 | toAmbiguousList : ANameMap a -> List (UserName, List a)
 89 | toAmbiguousList dict = map (mapSnd (map snd)) (toList dict.hierarchy)
 90 |
 91 | export
 92 | fromList : List (Name, a) -> ANameMap a
 93 | fromList = fromList' empty
 94 |   where
 95 |     fromList' : ANameMap a -> List (Name, a) -> ANameMap a
 96 |     fromList' acc [] = acc
 97 |     fromList' acc ((k, v) :: ns) = fromList' (addName k v acc) ns
 98 |
 99 | -- Merge two contexts, with entries in the first overriding entries in
100 | -- the second
101 | export
102 | merge : ANameMap a -> ANameMap a -> ANameMap a
103 | merge (MkANameMap exact hier) ctxt
104 |     = insertFrom (toList exact) ctxt
105 |   where
106 |     insertFrom : List (Name, a) -> ANameMap a -> ANameMap a
107 |     insertFrom [] ctxt = ctxt
108 |     insertFrom ((n, val) :: cs) ctxt
109 |         = insertFrom cs (addName n val ctxt)
110 |