Add some documentation about PosMap

src/Core/Metadata.idr

@@ -42,17 +42,17 @@ record Metadata where
        -- to know what the recursive call is, if applicable)
        currentLHS : Maybe ClosedTerm
        holeLHS : List (Name, ClosedTerm)
-       declsLoc : PosMap (NonEmptyFC, Name)
+       nameLocMap : PosMap (NonEmptyFC, Name)
 
 Show Metadata where
-  show (MkMetadata apps names tydecls currentLHS holeLHS declsLoc)
+  show (MkMetadata apps names tydecls currentLHS holeLHS nameLocMap)
     = "Metadata:\n" ++
       " lhsApps: " ++ show apps ++ "\n" ++
       " names: " ++ show names ++ "\n" ++
       " type declarations: " ++ show tydecls ++ "\n" ++
       " current LHS: " ++ show currentLHS ++ "\n" ++
       " holes: " ++ show holeLHS ++ "\n" ++
-      " declsLoc: " ++ show declsLoc
+      " nameLocMap: " ++ show nameLocMap
 
 export
 initMetadata : Metadata
@@ -62,7 +62,7 @@ initMetadata = MkMetadata
   , tydecls = []
   , currentLHS = Nothing
   , holeLHS = []
-  , declsLoc = empty
+  , nameLocMap = empty
   }
 
 -- A label for metadata in the global state
@@ -75,7 +75,7 @@ TTC Metadata where
            toBuf b (names m)
            toBuf b (tydecls m)
            toBuf b (holeLHS m)
-           toBuf b (declsLoc m)
+           toBuf b (nameLocMap m)
 
   fromBuf b
       = do apps <- fromBuf b
@@ -145,14 +145,14 @@ addTyDecl loc n env tm
            put MD $ record { tydecls $= ( (neloc, (n', length env, bindEnv loc env tm)) ::) } meta
 
 export
-addDeclLoc : {auto m : Ref MD Metadata} ->
+addNameLoc : {auto m : Ref MD Metadata} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> Name -> Core ()
-addDeclLoc loc n
+addNameLoc loc n
     = do meta <- get MD
          n' <- getFullName n
          whenJust (isNonEmptyFC loc) $ \neloc =>
-           put MD $ record { declsLoc $= insert (neloc, n') } meta
+           put MD $ record { nameLocMap $= insert (neloc, n') } meta
 
 export
 setHoleLHS : {auto m : Ref MD Metadata} ->

src/Idris/REPL.idr

@@ -385,7 +385,7 @@ processEdit (TypeAt line col name)
 
          -- Search the correct name by location for more precise search
          -- and fallback to given name if nothing found
-         let name = fromMaybe name $ findInTree (line - 1, col - 1) name (declsLoc meta)
+         let name = fromMaybe name $ findInTree (line - 1, col - 1) name (nameLocMap meta)
 
          -- Lookup the name globally
          globals <- lookupCtxtName name (gamma defs)

src/Libraries/Data/PosMap.idr

@@ -1,3 +1,9 @@
+||| Specialized implementation of an interval map with finger trees [1].
+||| This data structure is meant to get efficiently data with a correlated NonEmptyFC.
+||| The element data type must implement the `Measure` interface. An implementation
+||| is provided already for NonEmptyFC and tuples with NonEmptyFC as first element.
+|||
+||| [1] https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf
 module Libraries.Data.PosMap
 
 import Data.List
@@ -51,6 +57,7 @@ Cast FileRange Interval where
 Cast RMFileRange Interval where
   cast = MkInterval
 
+||| Things that have an associated interval in the source files.
 public export
 interface Measure a where
   measure : a -> FileRange
@@ -521,6 +528,7 @@ larger' : FileRange -> Interval -> Bool
 larger' i (MkInterval (MkRange k _)) = k > i
 larger' i NoInterval = False
 
+||| Inserts a new element in the map, in lexicographical order.
 export
 insert : Measure a => a -> PosMap a -> PosMap a
 insert v m = let (l, r) = split (larger (measure v)) m in l ++ (v <| r)
@@ -544,21 +552,19 @@ merge2 xs ys =
        b <: bs' => let (l, r) = split (larger' (measure b)) xs in
                        l ++ (b <| assert_total (merge1 r bs'))
 
+||| Merges two interval maps.
 export
 union : Measure a => PosMap a -> PosMap a -> PosMap a
 union xs ys = merge1 xs ys
 
-export
 atleast : FilePos -> Interval -> Bool
 atleast k (MkInterval (MkRange _ high)) = k <= high
 atleast k NoInterval = False
 
-export
 greater : FilePos -> Interval -> Bool
 greater k (MkInterval (MkRange low _)) = fst low > k
 greater k NoInterval = False
 
-export
 inRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a
 inRange low high t = matches (takeUntil (greater high) t)
   where matches : PosMap a -> List a
@@ -566,18 +572,22 @@ inRange low high t = matches (takeUntil (greater high) t)
                           EmptyL => []
                           x <: xs' => x :: assert_total (matches xs')
 
+||| Returns all the interval that contains the given point.
 export
 searchPos : MeasureRM a => FilePos -> PosMap a -> List a
 searchPos p = inRange p p
 
+||| Returns all the interval that intersects the given interval.
 export
 intersections : MeasureRM a => FileRange -> PosMap a -> List a
 intersections i = inRange (fst i) (snd i)
 
+||| Returns all the interval that contains the given interval.
 export
 dominators : MeasureRM a => FileRange -> PosMap a -> List a
 dominators i = inRange (snd i) (fst i)
 
+||| Returns the extreme boundaries of the map, if non empty.
 export
 bounds : Measure a => PosMap a -> Maybe FileRange
 bounds t =

src/TTImp/Elab/App.idr

@@ -109,7 +109,6 @@ getVarType rigc nest env fc x
                                 -- Add the type to the metadata
                                 log "metadata.names" 7 $ "getVarType is adding ↓"
                                 addNameType fc x env tyenv
-                                -- addDeclLoc fc x
 
                                 pure (tm, arglen, gnf env tyenv)
     where
@@ -712,7 +711,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
         prims <- getPrimitiveNames
         elabinfo <- updateElabInfo prims (elabMode elabinfo) n expargs elabinfo
 
-        addDeclLoc fc' n
+        addNameLoc fc' n
 
         logC "elab" 10
                 (do defs <- get Ctxt

src/TTImp/Elab/Hole.idr

@@ -53,7 +53,7 @@ checkHole rig elabinfo nest env fc n_in (Just gexpty)
          mkPrecise !(getNF gexpty)
          -- Record the LHS for this hole in the metadata
          withCurrentLHS (Resolved idx)
-         addDeclLoc fc nm
+         addNameLoc fc nm
          addUserHole nm
          saveHole nm
          pure (metaval, gexpty)
@@ -70,7 +70,7 @@ checkHole rig elabinfo nest env fc n_in exp
                        throw (AlreadyDefined fc nm)
          (idx, metaval) <- metaVarI fc rig env' nm ty
          withCurrentLHS (Resolved idx)
-         addDeclLoc fc nm
+         addNameLoc fc nm
          addUserHole nm
          saveHole nm
          pure (metaval, gnf env ty)

src/TTImp/Elab/ImplicitBind.idr

@@ -432,7 +432,7 @@ checkBindVar rig elabinfo nest env fc str topexp
 
                    log "metadata.names" 7 $ "checkBindVar is adding ↓"
                    addNameType fc (UN str) env exp
-                   addDeclLoc fc (UN str)
+                   addNameLoc fc (UN str)
 
                    checkExp rig elabinfo env fc tm (gnf env exp) topexp
               Just bty =>
@@ -444,7 +444,7 @@ checkBindVar rig elabinfo nest env fc str topexp
 
                    log "metadata.names" 7 $ "checkBindVar is adding ↓"
                    addNameType fc (UN str) env ty
-                   addDeclLoc fc (UN str)
+                   addNameLoc fc (UN str)
 
                    checkExp rig elabinfo env fc tm (gnf env ty) topexp
   where