From c084d285db20fc5f6b0449cde0aee41727828b25 Mon Sep 17 00:00:00 2001 From: Giuseppe Lomurno Date: Sun, 21 Mar 2021 13:05:04 +0100 Subject: [PATCH] Add some documentation about PosMap --- src/Core/Metadata.idr | 16 ++++++++-------- src/Idris/REPL.idr | 2 +- src/Libraries/Data/PosMap.idr | 16 +++++++++++++--- src/TTImp/Elab/App.idr | 3 +-- src/TTImp/Elab/Hole.idr | 4 ++-- src/TTImp/Elab/ImplicitBind.idr | 4 ++-- 6 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 02027d950..fb768c4c3 100644 --- a/src/Core/Metadata.idr +++ b/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} -> diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 506df55b6..6029e3a27 100644 --- a/src/Idris/REPL.idr +++ b/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) diff --git a/src/Libraries/Data/PosMap.idr b/src/Libraries/Data/PosMap.idr index 5f0b869f9..b7fd286f0 100644 --- a/src/Libraries/Data/PosMap.idr +++ b/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 = diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 10ec62822..2c327ccf1 100644 --- a/src/TTImp/Elab/App.idr +++ b/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 diff --git a/src/TTImp/Elab/Hole.idr b/src/TTImp/Elab/Hole.idr index 6e2692db6..e2861bc5a 100644 --- a/src/TTImp/Elab/Hole.idr +++ b/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) diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index 67d5b9fa5..c1e6d8e63 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/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