mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Added context for global names, store in an array
This commit is contained in:
parent
77e634cd33
commit
e03a2ba4b5
127
src/Core/Context.idr
Normal file
127
src/Core/Context.idr
Normal file
@ -0,0 +1,127 @@
|
||||
module Core.Context
|
||||
|
||||
import Core.Core
|
||||
import Core.Name
|
||||
import Core.TT
|
||||
|
||||
import Data.IOArray
|
||||
import Data.NameMap
|
||||
import Data.StringMap
|
||||
|
||||
%default total
|
||||
|
||||
-- Label for array references
|
||||
data Arr : Type where
|
||||
|
||||
export
|
||||
record Context a where
|
||||
constructor MkContext
|
||||
nextEntry : Int
|
||||
-- Map from full name to it position in the context
|
||||
resolvedAs : NameMap Int
|
||||
-- Map from strings to all the possible names in all namespaces
|
||||
possibles : StringMap (List (Name, Int))
|
||||
-- Reference to the actual content, indexed by Int
|
||||
content : Ref Arr (IOArray a)
|
||||
|
||||
-- Namespaces which are visible (i.e. have been imported)
|
||||
-- This only matters during evaluation and type checking, to control
|
||||
-- access in a program - in all other cases, we'll assume everything is
|
||||
-- visible
|
||||
visibleNS : List (List String)
|
||||
|
||||
initSize : Int
|
||||
initSize = 10000
|
||||
|
||||
Grow : Int
|
||||
Grow = initSize
|
||||
|
||||
export
|
||||
initCtxt : Core (Context a)
|
||||
initCtxt
|
||||
= do arr <- coreLift $ newArray initSize
|
||||
aref <- newRef Arr arr
|
||||
pure (MkContext 0 empty empty aref [])
|
||||
|
||||
-- Get the position of the next entry in the context array, growing the
|
||||
-- array if it's out of bounds.
|
||||
getPosition : Name -> Context a -> Core (Int, Context a)
|
||||
getPosition n ctxt
|
||||
= case lookup n (resolvedAs ctxt) of
|
||||
Just idx => pure (idx, ctxt)
|
||||
Nothing =>
|
||||
do let idx = nextEntry ctxt + 1
|
||||
let a = content ctxt
|
||||
arr <- get Arr
|
||||
when (idx >= max arr) $
|
||||
do arr' <- coreLift $ newArrayCopy (max arr + Grow) arr
|
||||
put Arr arr'
|
||||
pure (idx, record { nextEntry = idx } ctxt)
|
||||
|
||||
-- Add the name to the context, or update the existing entry if it's already
|
||||
-- there.
|
||||
export
|
||||
addCtxt : Name -> a -> Context a -> Core (Context a)
|
||||
addCtxt n val ctxt_in
|
||||
= do (idx, ctxt) <- getPosition n ctxt_in
|
||||
let a = content ctxt
|
||||
arr <- get Arr
|
||||
coreLift $ writeArray arr idx val
|
||||
pure ctxt
|
||||
|
||||
export
|
||||
lookupCtxtExact : Name -> Context a -> Core (Maybe a)
|
||||
lookupCtxtExact (Resolved idx) ctxt
|
||||
= do let a = content ctxt
|
||||
arr <- get Arr
|
||||
coreLift (readArray arr idx)
|
||||
lookupCtxtExact n ctxt
|
||||
= do let Just idx = lookup n (resolvedAs ctxt)
|
||||
| Nothing => pure Nothing
|
||||
let a = content ctxt
|
||||
arr <- get Arr
|
||||
coreLift (readArray arr idx)
|
||||
|
||||
export
|
||||
lookupCtxtName : Name -> Context a -> Core (List (Name, a))
|
||||
lookupCtxtName n ctxt
|
||||
= case userNameRoot n of
|
||||
Nothing => do Just res <- lookupCtxtExact n ctxt
|
||||
| Nothing => pure []
|
||||
pure [(n, res)]
|
||||
Just r =>
|
||||
do let Just ps = lookup r (possibles ctxt)
|
||||
| Nothing => pure []
|
||||
ps' <- the (Core (List (Maybe (Name, a)))) $
|
||||
traverse (\ (n, i) =>
|
||||
do Just res <- lookupCtxtExact (Resolved i) ctxt
|
||||
| pure Nothing
|
||||
pure (Just (n, res))) ps
|
||||
getMatches ps'
|
||||
where
|
||||
matches : Name -> (Name, a) -> Bool
|
||||
matches (NS ns _) (NS cns _, _) = ns `isPrefixOf` cns
|
||||
matches (NS _ _) _ = True -- no in library name, so root doesn't match
|
||||
matches _ _ = True -- no prefix, so root must match, so good
|
||||
|
||||
getMatches : List (Maybe (Name, a)) -> Core (List (Name, a))
|
||||
getMatches [] = pure []
|
||||
getMatches (Nothing :: rs) = getMatches rs
|
||||
getMatches (Just r :: rs)
|
||||
= if matches n r
|
||||
then do rs' <- getMatches rs
|
||||
pure (r :: rs')
|
||||
else getMatches rs
|
||||
|
||||
public export
|
||||
data Def : Type where
|
||||
None : Def -- Not yet defined
|
||||
Fn : ClosedTerm -> Def -- Ordinary function definition
|
||||
DCon : (tag : Int) -> (arity : Nat) -> Def -- data constructor
|
||||
TCon : (tag : Int) -> (arity : Nat) ->
|
||||
(parampos : List Nat) -> -- parameters
|
||||
(detpos : List Nat) -> -- determining arguments
|
||||
(datacons : List Name) ->
|
||||
Def
|
||||
Hole : (numlocs : Nat) -> (invertible : Bool) -> Def
|
||||
|
@ -15,6 +15,12 @@ data Name : Type where
|
||||
export Show Name where
|
||||
show n = "[not done yet]"
|
||||
|
||||
export
|
||||
userNameRoot : Name -> Maybe String
|
||||
userNameRoot (NS _ n) = userNameRoot n
|
||||
userNameRoot (UN n) = Just n
|
||||
userNameRoot _ = Nothing
|
||||
|
||||
export
|
||||
showSep : String -> List String -> String
|
||||
showSep sep [] = ""
|
||||
|
96
src/Data/IOArray.idr
Normal file
96
src/Data/IOArray.idr
Normal file
@ -0,0 +1,96 @@
|
||||
module Data.IOArray
|
||||
|
||||
%default total
|
||||
|
||||
-- Raw access to IOArrays. This interface is unsafe because there's no
|
||||
-- bounds checking, and is merely intended to provide primitive access via
|
||||
-- the RTS. Safe interfaces (either with run time or compile time
|
||||
-- bounds checking) can be implemented on top of this
|
||||
|
||||
-- Implemented entirely by the array primitives in the RTS
|
||||
data ArrayData : Type -> Type where
|
||||
|
||||
export
|
||||
data IORawArray elem = MkIORawArray (ArrayData elem)
|
||||
|
||||
||| Create a new array of the given size, with all entries set to the
|
||||
||| given default element.
|
||||
export
|
||||
newRawArray : Int -> elem -> IO (IORawArray elem)
|
||||
newRawArray size default
|
||||
= do vm <- getMyVM
|
||||
MkRaw p <- foreign FFI_C "idris_newArray"
|
||||
(Ptr -> Int -> Raw elem -> IO (Raw (ArrayData elem)))
|
||||
vm size (MkRaw default)
|
||||
pure (MkIORawArray p)
|
||||
|
||||
||| Write an element at a location in an array.
|
||||
||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can
|
||||
||| be implemented on top of this, either with a run time or compile time
|
||||
||| check.
|
||||
export
|
||||
unsafeWriteArray : IORawArray elem -> Int -> elem -> IO ()
|
||||
unsafeWriteArray (MkIORawArray p) i val
|
||||
= foreign FFI_C "idris_arraySet"
|
||||
(Raw (ArrayData elem) -> Int -> Raw elem -> IO ())
|
||||
(MkRaw p) i (MkRaw val)
|
||||
|
||||
||| Read the element at a location in an array.
|
||||
||| There is *no* bounds checking, hence this is unsafe. Safe interfaces can
|
||||
||| be implemented on top of this, either with a run time or compile time
|
||||
||| check.
|
||||
export
|
||||
unsafeReadArray : IORawArray elem -> Int -> IO elem
|
||||
unsafeReadArray (MkIORawArray p) i
|
||||
= do MkRaw val <- foreign FFI_C "idris_arrayGet"
|
||||
(Raw (ArrayData elem) -> Int -> IO (Raw elem))
|
||||
(MkRaw p) i
|
||||
pure val
|
||||
|
||||
-- As IORawArray, but wrapped in dynamic checks that elements exist and
|
||||
-- are in bounds
|
||||
public export
|
||||
record IOArray elem where
|
||||
constructor MkIOArray
|
||||
max : Int
|
||||
content : IORawArray (Maybe elem)
|
||||
|
||||
export
|
||||
newArray : Int -> IO (IOArray elem)
|
||||
newArray size
|
||||
= pure (MkIOArray size !(newRawArray size Nothing))
|
||||
|
||||
export
|
||||
writeArray : IOArray elem -> Int -> elem -> IO ()
|
||||
writeArray arr pos el
|
||||
= if pos < 0 || pos >= max arr
|
||||
then pure ()
|
||||
else unsafeWriteArray (content arr) pos (Just el)
|
||||
|
||||
export
|
||||
readArray : IOArray elem -> Int -> IO (Maybe elem)
|
||||
readArray arr pos
|
||||
= if pos < 0 || pos >= max arr
|
||||
then pure Nothing
|
||||
else unsafeReadArray (content arr) pos
|
||||
|
||||
-- Make a new array of the given size with the elements copied from the
|
||||
-- other array
|
||||
export
|
||||
newArrayCopy : (newsize : Int) -> IOArray elem -> IO (IOArray elem)
|
||||
newArrayCopy newsize arr
|
||||
= do let newsize' = if newsize < max arr then max arr else newsize
|
||||
arr' <- newArray newsize'
|
||||
copyFrom (content arr) (content arr') (max arr - 1)
|
||||
pure arr'
|
||||
where
|
||||
copyFrom : IORawArray (Maybe elem) ->
|
||||
IORawArray (Maybe elem) ->
|
||||
Int -> IO ()
|
||||
copyFrom old new pos
|
||||
= if pos < 0
|
||||
then pure ()
|
||||
else do el <- unsafeReadArray old pos
|
||||
unsafeWriteArray new pos el
|
||||
assert_total (copyFrom old new (pos - 1))
|
||||
|
@ -3,6 +3,7 @@ package yaffle
|
||||
modules =
|
||||
Control.Delayed,
|
||||
|
||||
Core.Context,
|
||||
Core.Core,
|
||||
Core.Env,
|
||||
Core.FC,
|
||||
@ -11,7 +12,7 @@ modules =
|
||||
Core.Value,
|
||||
|
||||
Data.Bool.Extra,
|
||||
Data.IntMap,
|
||||
Data.IOArray,
|
||||
Data.NameMap,
|
||||
Data.StringMap,
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user