idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-03 00:55:00 +03:00
Code Issues Projects Releases Wiki Activity

Added insertion to interval map and usage in TypeAt command

Browse Source
This commit is contained in:
Giuseppe Lomurno 2021-03-20 22:01:08 +01:00 committed by G. Allais
parent 76697e7f85
commit 7fa6dc5f48
11 changed files with 72 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
src/Core/Metadata.idr
View File

@ -12,6 +12,7 @@ import Core.TTC
import Data.List
import System.File
import Libraries.Data.PosMap
import Libraries.Utils.Binary
%default covering
@ -41,15 +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)
Show Metadata where
show (MkMetadata apps names tydecls currentLHS holeLHS)
show (MkMetadata apps names tydecls currentLHS holeLHS declsLoc)
= "Metadata:\n" ++
" lhsApps: " ++ show apps ++ "\n" ++
" names: " ++ show names ++ "\n" ++
" type declarations: " ++ show tydecls ++ "\n" ++
" current LHS: " ++ show currentLHS ++ "\n" ++
" holes: " ++ show holeLHS
" holes: " ++ show holeLHS ++ "\n" ++
" declsLoc: " ++ show declsLoc
export
initMetadata : Metadata
@ -59,6 +62,7 @@ initMetadata = MkMetadata
, tydecls = []
, currentLHS = Nothing
, holeLHS = []
, declsLoc = empty
}
-- A label for metadata in the global state
@ -71,13 +75,15 @@ TTC Metadata where
toBuf b (names m)
toBuf b (tydecls m)
toBuf b (holeLHS m)
toBuf b (declsLoc m)
fromBuf b
= do apps <- fromBuf b
ns <- fromBuf b
tys <- fromBuf b
hlhs <- fromBuf b
pure (MkMetadata apps ns tys Nothing hlhs)
dlocs <- fromBuf b
pure (MkMetadata apps ns tys Nothing hlhs dlocs)
export
addLHS : {vars : _} ->
@ -138,6 +144,16 @@ addTyDecl loc n env tm
whenJust (isNonEmptyFC loc) $ \ neloc =>
put MD $ record { tydecls $= ( (neloc, (n', length env, bindEnv loc env tm)) ::) } meta
export
addDeclLoc : {auto m : Ref MD Metadata} ->
{auto c : Ref Ctxt Defs} ->
FC -> Name -> Core ()
addDeclLoc loc n
= do meta <- get MD
n' <- getFullName n
whenJust (isNonEmptyFC loc) $ \neloc =>
put MD $ record { declsLoc $= insert (neloc, n') } meta
export
setHoleLHS : {auto m : Ref MD Metadata} ->
ClosedTerm -> Core ()
@ -233,12 +249,13 @@ TTC TTMFile where
pure (MkTTMFile ver md)
HasNames Metadata where
full gam (MkMetadata lhs ns tys clhs hlhs)
full gam (MkMetadata lhs ns tys clhs hlhs dlocs)
= pure $ MkMetadata !(traverse fullLHS lhs)
!(traverse fullTy ns)
!(traverse fullTy tys)
Nothing
!(traverse fullHLHS hlhs)
(fromList !(traverse fullDecls (toList dlocs)))
where
fullLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
fullLHS (fc, (i, tm)) = pure (fc, (i, !(full gam tm)))
@ -249,12 +266,16 @@ HasNames Metadata where
fullHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
fullHLHS (n, tm) = pure (!(full gam n), !(full gam tm))
resolved gam (MkMetadata lhs ns tys clhs hlhs)
fullDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
fullDecls (fc, n) = pure (fc, !(full gam n))
resolved gam (MkMetadata lhs ns tys clhs hlhs dlocs)
= pure $ MkMetadata !(traverse resolvedLHS lhs)
!(traverse resolvedTy ns)
!(traverse resolvedTy tys)
Nothing
!(traverse resolvedHLHS hlhs)
(fromList !(traverse resolvedDecls (toList dlocs)))
where
resolvedLHS : (NonEmptyFC, (Nat, ClosedTerm)) -> Core (NonEmptyFC, (Nat, ClosedTerm))
resolvedLHS (fc, (i, tm)) = pure (fc, (i, !(resolved gam tm)))
@ -265,6 +286,9 @@ HasNames Metadata where
resolvedHLHS : (Name, ClosedTerm) -> Core (Name, ClosedTerm)
resolvedHLHS (n, tm) = pure (!(resolved gam n), !(resolved gam tm))
resolvedDecls : (NonEmptyFC, Name) -> Core (NonEmptyFC, Name)
resolvedDecls (fc, n) = pure (fc, !(resolved gam n))
export
writeToTTM : {auto c : Ref Ctxt Defs} ->
{auto m : Ref MD Metadata} ->

1
src/Core/TTC.idr
View File

@ -11,6 +11,7 @@ import Core.Options
import Core.TT
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Vect
import Libraries.Utils.Binary

6
src/Idris/REPL.idr
View File

@ -58,6 +58,7 @@ import Data.List1
import Data.Maybe
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Stream
import Data.Strings
import Libraries.Data.String.Extra
@ -367,6 +368,11 @@ processEdit : {auto c : Ref Ctxt Defs} ->
EditCmd -> Core EditResult
processEdit (TypeAt line col name)
= do defs <- get Ctxt
meta <- get MD
-- Search the correct name by location for more precise search
-- and fallback to given name if nothing found
let name = maybe name snd (match (line, col) (declsLoc meta))
-- Lookup the name globally
globals <- lookupCtxtName name (gamma defs)

21
src/Libraries/Data/PosMap.idr
View File

@ -1,5 +1,6 @@
module Libraries.Data.PosMap
import Data.List
import Core.FC
%default total
@ -57,6 +58,7 @@ interface Measure a where
interface MeasureRM a where
measureRM : a -> RMFileRange
public export
Measure a => MeasureRM a where
measureRM = cast . measure
@ -197,6 +199,7 @@ Empty |> a = Single a
(Deep _ pr m (Three d c b)) |> a = deep pr m (Four d c b a)
(Deep _ pr m (Four e d c b)) |> a = deep pr (m |> node3 e d c) (Two b a)
export
Foldable PosMap where
foldr f init Empty = init
foldr f init (Single x) = f x init
@ -564,8 +567,18 @@ inRange low high t = matches (takeUntil (greater high) t)
x <: xs' => x :: assert_total (matches xs')
export
search : MeasureRM a => FilePos -> PosMap a -> List a
search p = inRange p p
searchPos : MeasureRM a => FilePos -> PosMap a -> List a
searchPos p = inRange p p
export
match : Measure a => FilePos -> PosMap a -> Maybe a
match p m = head' $ sortBy (\x, y => cmp (measure x) (measure y)) $ inRange p p m
where cmp : FileRange -> FileRange -> Ordering
cmp ((sr1, sc1), (er1, ec1)) ((sr2, sc2), (er2, ec2)) =
case compare (er1 - sr1) (er2 - sr2) of
LT => LT
EQ => compare (ec1 - sc1) (ec2 - sr2)
GT => GT
export
intersections : MeasureRM a => FileRange -> PosMap a -> List a
@ -585,10 +598,10 @@ bounds t =
EmptyL => Nothing
x <: _ => Just (fst (measure x), high)
export
public export
Measure NonEmptyFC where
measure = snd
export
public export
Measure (NonEmptyFC, a) where
measure = measure . fst

6
src/Libraries/Utils/Binary.idr
View File

@ -12,6 +12,7 @@ import Data.Nat
import Data.Vect
import System.File
import Libraries.Data.PosMap
-- Serialising data as binary. Provides an interface TTC which allows
-- reading and writing to chunks of memory, "Binary", which can be written
@ -378,6 +379,11 @@ export
rewrite (plusSuccRightSucc k done)
readElems (val :: xs) k
export
(TTC a, Measure a) => TTC (PosMap a) where
toBuf b = toBuf b . toList
fromBuf b = fromList <$> fromBuf b
%hide Fin.fromInteger
count : List.Elem.Elem x xs -> Int

3
src/TTImp/Elab/App.idr
View File

@ -109,6 +109,7 @@ 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
@ -711,6 +712,8 @@ 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
logC "elab" 10
(do defs <- get Ctxt
fnty <- quote defs env nty

2
src/TTImp/Elab/Hole.idr
View File

@ -53,6 +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
addUserHole nm
saveHole nm
pure (metaval, gexpty)
@ -69,6 +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
addUserHole nm
saveHole nm
pure (metaval, gnf env ty)

2
src/TTImp/Elab/ImplicitBind.idr
View File

@ -432,6 +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)
checkExp rig elabinfo env fc tm (gnf env exp) topexp
Just bty =>
@ -443,6 +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)
checkExp rig elabinfo env fc tm (gnf env ty) topexp
where

2
src/TTImp/ProcessData.idr
View File

@ -278,6 +278,7 @@ processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
traverse_ addToSave (keys (getMetas ty))
addToSave n
addDeclLoc fc n
log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
case vis of
@ -358,6 +359,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra
traverse_ addToSave (keys (getMetas ty))
addToSave n
addDeclLoc fc n
log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
let connames = map conName cons

1
src/TTImp/ProcessDef.idr
View File

@ -866,6 +866,7 @@ processDef opts nest env fc n_in cs_in
do let tymetas = getMetas (type gdef)
traverse_ addToSave (keys tymetas)
addToSave n
addDeclLoc fc n
-- Flag this name as one which needs compiling
defs <- get Ctxt

3
src/TTImp/ProcessType.idr
View File

@ -317,6 +317,9 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra
log "metadata.names" 7 $ "processType is adding ↓"
addNameType nameFC (Resolved idx) env ty -- for looking up types
addDeclLoc fc n -- for lookup with location
addDeclLoc nameFC n
traverse_ addToSave (keys (getMetas ty))
addToSave n
log "declare.type" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))