idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #1434 from edwinb/ttc-wrangling

Browse Source 
Some TTC loading improvements
This commit is contained in:
Edwin Brady 2021-05-19 13:34:53 +01:00 committed by GitHub
commit b901b2e5ad
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
11 changed files with 200 additions and 64 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libs/contrib/System/Path.idr
View File

@ -1,6 +1,7 @@
module System.Path
import Data.List
import Data.List1
import Data.Maybe
import Data.Nat
import Data.Strings

14
src/Compiler/Common.idr
View File

@ -110,9 +110,9 @@ execute {c} cg tm
-- If an entry isn't already decoded, get the minimal entry we need for
-- compilation, and record the Binary so that we can put it back when we're
-- done (so that we don't obliterate the definition)
getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe Binary)
getMinimalDef : ContextEntry -> Core (GlobalDef, Maybe (Namespace, Binary))
getMinimalDef (Decoded def) = pure (def, Nothing)
getMinimalDef (Coded bin)
getMinimalDef (Coded ns bin)
= do b <- newRef Bin bin
cdef <- fromBuf b
refsRList <- fromBuf b
@ -125,12 +125,12 @@ getMinimalDef (Coded bin)
[] Public (MkTotality Unchecked IsCovering)
[] Nothing refsR False False True
None cdef Nothing []
pure (def, Just bin)
pure (def, Just (ns, bin))
-- ||| Recursively get all calls in a function definition
getAllDesc : {auto c : Ref Ctxt Defs} ->
List Name -> -- calls to check
IOArray (Int, Maybe Binary) ->
IOArray (Int, Maybe (Namespace, Binary)) ->
-- which nodes have been visited. If the entry is
-- present, it's visited. Keep the binary entry, if
-- we partially decoded it, so that we can put back
@ -174,10 +174,10 @@ getNamedDef n
pure (Just (n, location def, d))
replaceEntry : {auto c : Ref Ctxt Defs} ->
(Int, Maybe Binary) -> Core ()
(Int, Maybe (Namespace, Binary)) -> Core ()
replaceEntry (i, Nothing) = pure ()
replaceEntry (i, Just b)
= ignore $ addContextEntry (Resolved i) b
replaceEntry (i, Just (ns, b))
= ignore $ addContextEntry ns (Resolved i) b
natHackNames : List Name
natHackNames

98
src/Core/Binary.idr
View File

@ -1,9 +1,11 @@
module Core.Binary
import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Hash
import Core.Name.Namespace
import Core.Normalise
import Core.Options
import Core.TT
@ -31,7 +33,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 52
ttcVersion = 53
export
checkTTCVersion : String -> Int -> Int -> Core ()
@ -177,11 +179,12 @@ writeTTCFile b file_in
toBuf b (version file)
toBuf b (ifaceHash file)
toBuf b (importHashes file)
toBuf b (imported file)
toBuf b (extraData file)
toBuf b (context file)
toBuf b (userHoles file)
toBuf b (autoHints file)
toBuf b (typeHints file)
toBuf b (imported file)
toBuf b (nextVar file)
toBuf b (currentNS file)
toBuf b (nestedNS file)
@ -191,13 +194,12 @@ writeTTCFile b file_in
toBuf b (namedirectives file)
toBuf b (cgdirectives file)
toBuf b (transforms file)
toBuf b (extraData file)
readTTCFile : TTC extra =>
{auto c : Ref Ctxt Defs} ->
String -> Maybe (Namespace) ->
Bool -> String -> Maybe (Namespace) ->
Ref Bin Binary -> Core (TTCFile extra)
readTTCFile file as b
readTTCFile readall file as b
= do hdr <- fromBuf b
chunk <- get Bin
when (hdr /= "TT2") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
@ -205,42 +207,57 @@ readTTCFile file as b
checkTTCVersion file ver ttcVersion
ifaceHash <- fromBuf b
importHashes <- fromBuf b
defs <- fromBuf b
uholes <- fromBuf b
autohs <- fromBuf b
typehs <- fromBuf b
-- coreLift $ putStrLn ("Hints: " ++ show typehs)
-- coreLift $ putStrLn $ "Read " ++ show (length (map fullname defs)) ++ " defs"
imp <- fromBuf b
nextv <- fromBuf b
cns <- fromBuf b
nns <- fromBuf b
pns <- fromBuf b
rws <- fromBuf b
prims <- fromBuf b
nds <- fromBuf b
cgds <- fromBuf b
trans <- fromBuf b
ex <- fromBuf b
pure (MkTTCFile ver ifaceHash importHashes
defs uholes
autohs typehs imp nextv cns nns
pns rws prims nds cgds trans ex)
if not readall
then pure (MkTTCFile ver ifaceHash importHashes [] [] [] [] []
0 (mkNamespace "") [] Nothing
Nothing
(MkPrimNs Nothing Nothing Nothing Nothing)
[] [] [] ex)
else do
defs <- fromBuf b
uholes <- fromBuf b
autohs <- fromBuf b
typehs <- fromBuf b
nextv <- fromBuf b
cns <- fromBuf b
nns <- fromBuf b
pns <- fromBuf b
rws <- fromBuf b
prims <- fromBuf b
nds <- fromBuf b
cgds <- fromBuf b
trans <- fromBuf b
pure (MkTTCFile ver ifaceHash importHashes
(map (replaceNS cns) defs) uholes
autohs typehs imp nextv cns nns
pns rws prims nds cgds trans ex)
where
-- We don't store full names in 'defs' - we remove the namespace if it's
-- the same as the current namespace. So, this puts it back.
replaceNS : Namespace -> (Name, a) -> (Name, a)
replaceNS ns n@(NS _ _, d) = n
replaceNS ns (n, d) = (NS ns n, d)
-- Pull out the list of GlobalDefs that we want to save
getSaveDefs : List Name -> List (Name, Binary) -> Defs ->
getSaveDefs : Namespace -> List Name -> List (Name, Binary) -> Defs ->
Core (List (Name, Binary))
getSaveDefs [] acc _ = pure acc
getSaveDefs (n :: ns) acc defs
getSaveDefs modns [] acc _ = pure acc
getSaveDefs modns (n :: ns) acc defs
= do Just gdef <- lookupCtxtExact n (gamma defs)
| Nothing => getSaveDefs ns acc defs -- 'n' really should exist though!
| Nothing => getSaveDefs modns ns acc defs -- 'n' really should exist though!
-- No need to save builtins
case definition gdef of
Builtin _ => getSaveDefs ns acc defs
Builtin _ => getSaveDefs modns ns acc defs
_ => do bin <- initBinaryS 16384
toBuf bin !(full (gamma defs) gdef)
toBuf bin (trimNS modns !(full (gamma defs) gdef))
b <- get Bin
getSaveDefs ns ((fullname gdef, b) :: acc) defs
getSaveDefs modns ns ((trimName (fullname gdef), b) :: acc) defs
where
trimName : Name -> Name
trimName n@(NS defns d) = if defns == modns then d else n
trimName n = n
-- Write out the things in the context which have been defined in the
-- current source file
@ -253,7 +270,7 @@ writeToTTC extradata fname
= do bin <- initBinary
defs <- get Ctxt
ust <- get UST
gdefs <- getSaveDefs (keys (toSave defs)) [] defs
gdefs <- getSaveDefs (currentNS defs) (keys (toSave defs)) [] defs
log "ttc.write" 5 $ "Writing " ++ fname ++ " with hash " ++ show (ifaceHash defs)
writeTTCFile bin
(MkTTCFile ttcVersion (ifaceHash defs) (importHashes defs)
@ -278,9 +295,10 @@ writeToTTC extradata fname
pure ()
addGlobalDef : {auto c : Ref Ctxt Defs} ->
(modns : ModuleIdent) -> (importAs : Maybe Namespace) ->
(modns : ModuleIdent) -> Namespace ->
(importAs : Maybe Namespace) ->
(Name, Binary) -> Core ()
addGlobalDef modns asm (n, def)
addGlobalDef modns filens asm (n, def)
= do defs <- get Ctxt
codedentry <- lookupContextEntry n (gamma defs)
-- Don't update the coded entry because some names might not be
@ -290,7 +308,7 @@ addGlobalDef modns asm (n, def)
pure (Just x))
codedentry
unless (completeDef entry) $
ignore $ addContextEntry n def
ignore $ addContextEntry filens n def
whenJust asm $ \ as => addContextAlias (asName modns as n) n
@ -422,16 +440,18 @@ readFromTTC nestedns loc reexp fname modNS importAs
let as = if importAs == miAsNamespace modNS
then Nothing
else Just importAs
ttc <- readTTCFile fname as bin
-- If it's already imported, but without reexporting, then all we're
-- interested in is returning which other modules to load.
-- Otherwise, add the data
let ex = extraData ttc
if alreadyDone modNS importAs (allImported defs)
then pure (Just (ex, ifaceHash ttc, imported ttc))
then do ttc <- readTTCFile False fname as bin
let ex = extraData ttc
pure (Just (ex, ifaceHash ttc, imported ttc))
else do
traverse_ (addGlobalDef modNS as) (context ttc)
ttc <- readTTCFile True fname as bin
let ex = extraData ttc
traverse_ (addGlobalDef modNS (currentNS ttc) as) (context ttc)
traverse_ addUserHole (userHoles ttc)
setNS (currentNS ttc)
when nestedns $ setNestedNS (nestedNS ttc)

26
src/Core/CaseTree.idr
View File

@ -50,6 +50,32 @@ isDefault : CaseAlt vars -> Bool
isDefault (DefaultCase _) = True
isDefault _ = False
mutual
export
StripNamespace (CaseTree vars) where
trimNS ns (Case idx p scTy xs)
= Case idx p (trimNS ns scTy) (map (trimNS ns) xs)
trimNS ns (STerm x t) = STerm x (trimNS ns t)
trimNS ns c = c
restoreNS ns (Case idx p scTy xs)
= Case idx p (restoreNS ns scTy) (map (restoreNS ns) xs)
restoreNS ns (STerm x t) = STerm x (restoreNS ns t)
restoreNS ns c = c
export
StripNamespace (CaseAlt vars) where
trimNS ns (ConCase x tag args t) = ConCase x tag args (trimNS ns t)
trimNS ns (DelayCase ty arg t) = DelayCase ty arg (trimNS ns t)
trimNS ns (ConstCase x t) = ConstCase x (trimNS ns t)
trimNS ns (DefaultCase t) = DefaultCase (trimNS ns t)
restoreNS ns (ConCase x tag args t) = ConCase x tag args (restoreNS ns t)
restoreNS ns (DelayCase ty arg t) = DelayCase ty arg (restoreNS ns t)
restoreNS ns (ConstCase x t) = ConstCase x (restoreNS ns t)
restoreNS ns (DefaultCase t) = DefaultCase (restoreNS ns t)
public export
data Pat : Type where
PAs : FC -> Name -> Pat -> Pat

41
src/Core/Context.idr
View File

@ -311,7 +311,8 @@ data Arr : Type where
-- binary blob yet, so decode it first time
public export
data ContextEntry : Type where
Coded : Binary -> ContextEntry
Coded : Namespace -> -- namespace for decoding into, with restoreNS
Binary -> ContextEntry
Decoded : GlobalDef -> ContextEntry
data PossibleName : Type where
@ -492,8 +493,7 @@ lookupCtxtExactI (Resolved idx) ctxt
Just val =>
pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True val)
Nothing =>
do let a = content ctxt
arr <- get Arr
do arr <- get Arr @{content ctxt}
Just def <- coreLift (readArray arr idx)
| Nothing => pure Nothing
pure $ returnDef (inlineOnly ctxt) idx !(decode ctxt idx True def)
@ -512,8 +512,7 @@ lookupCtxtExact (Resolved idx) ctxt
Nothing => pure Nothing
Just (_, def) => pure (Just def)
Nothing =>
do let a = content ctxt
arr <- get Arr
do arr <- get Arr @{content ctxt}
Just res <- coreLift (readArray arr idx)
| Nothing => pure Nothing
def <- decode ctxt idx True res
@ -793,7 +792,6 @@ HasNames (Term vars) where
export
HasNames Pat where
full gam (PAs fc n p)
= [| PAs (pure fc) (full gam n) (full gam p) |]
full gam (PCon fc n i ar ps)
@ -920,6 +918,31 @@ HasNames Def where
= pure $ Guess !(resolved gam tm) b cs
resolved gam t = pure t
export
StripNamespace Def where
trimNS ns (PMDef i args ct rt pats)
= PMDef i args (trimNS ns ct) rt (map trimNSpat pats)
where
trimNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
(vs ** (Env Term vs, Term vs, Term vs))
trimNSpat (vs ** (env, lhs, rhs))
= (vs ** (env, trimNS ns lhs, trimNS ns rhs))
trimNS ns d = d
restoreNS ns (PMDef i args ct rt pats)
= PMDef i args (restoreNS ns ct) rt (map restoreNSpat pats)
where
restoreNSpat : (vs ** (Env Term vs, Term vs, Term vs)) ->
(vs ** (Env Term vs, Term vs, Term vs))
restoreNSpat (vs ** (env, lhs, rhs))
= (vs ** (env, restoreNS ns lhs, restoreNS ns rhs))
restoreNS ns d = d
export
StripNamespace GlobalDef where
trimNS ns def = record { definition $= trimNS ns } def
restoreNS ns def = record { definition $= restoreNS ns } def
HasNames (NameMap a) where
full gam nmap
= insertAll empty (toList nmap)
@ -1296,10 +1319,10 @@ addDef n def
export
addContextEntry : {auto c : Ref Ctxt Defs} ->
Name -> Binary -> Core Int
addContextEntry n def
Namespace -> Name -> Binary -> Core Int
addContextEntry ns n def
= do defs <- get Ctxt
(idx, gam') <- addEntry n (Coded def) (gamma defs)
(idx, gam') <- addEntry n (Coded ns def) (gamma defs)
put Ctxt (record { gamma = gam' } defs)
pure idx

50
src/Core/TT.idr
View File

@ -743,6 +743,56 @@ data Term : List Name -> Type where
Term vars
TType : FC -> Term vars
-- Remove/restore the given namespace from all Refs. This is to allow
-- writing terms and case trees to disk without repeating the same namespace
-- all over the place.
public export
interface StripNamespace a where
trimNS : Namespace -> a -> a
restoreNS : Namespace -> a -> a
export
StripNamespace (Term vars) where
trimNS ns tm@(Ref fc x (NS tns n))
= if ns == tns then Ref fc x (NS (unsafeFoldNamespace []) n) else tm
-- ^ A blank namespace, rather than a UN, so we don't catch primitive
-- names which are represented as UN.
trimNS ns (Meta fc x y xs)
= Meta fc x y (map (trimNS ns) xs)
trimNS ns (Bind fc x b scope)
= Bind fc x (map (trimNS ns) b) (trimNS ns scope)
trimNS ns (App fc fn arg)
= App fc (trimNS ns fn) (trimNS ns arg)
trimNS ns (As fc s p tm)
= As fc s (trimNS ns p) (trimNS ns tm)
trimNS ns (TDelayed fc x y)
= TDelayed fc x (trimNS ns y)
trimNS ns (TDelay fc x t y)
= TDelay fc x (trimNS ns t) (trimNS ns y)
trimNS ns (TForce fc r y)
= TForce fc r (trimNS ns y)
trimNS ns tm = tm
restoreNS ns tm@(Ref fc x (NS tmns n))
= if isNil (unsafeUnfoldNamespace tmns)
then Ref fc x (NS ns n)
else tm
restoreNS ns (Meta fc x y xs)
= Meta fc x y (map (restoreNS ns) xs)
restoreNS ns (Bind fc x b scope)
= Bind fc x (map (restoreNS ns) b) (restoreNS ns scope)
restoreNS ns (App fc fn arg)
= App fc (restoreNS ns fn) (restoreNS ns arg)
restoreNS ns (As fc s p tm)
= As fc s (restoreNS ns p) (restoreNS ns tm)
restoreNS ns (TDelayed fc x y)
= TDelayed fc x (restoreNS ns y)
restoreNS ns (TDelay fc x t y)
= TDelay fc x (restoreNS ns t) (restoreNS ns y)
restoreNS ns (TForce fc r y)
= TForce fc r (restoreNS ns y)
restoreNS ns tm = tm
export
isErased : Term vars -> Bool
isErased (Erased _ _) = True

4
src/Core/TTC.idr
View File

@ -1079,12 +1079,12 @@ TTC Transform where
pure (MkTransform {vars} n env lhs rhs)
-- decode : Context -> Int -> (update : Bool) -> ContextEntry -> Core GlobalDef
Core.Context.decode gam idx update (Coded bin)
Core.Context.decode gam idx update (Coded ns bin)
= do b <- newRef Bin bin
def <- fromBuf b
let a = getContent gam
arr <- get Arr
def' <- resolved gam def
def' <- resolved gam (restoreNS ns def)
when update $ coreLift $ writeArray arr idx (Decoded def')
pure def'
Core.Context.decode gam idx update (Decoded def) = pure def

24
src/Core/Unify.idr
View File

@ -489,14 +489,28 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm
Hole _ p => precisetype p
_ => False
-- A solution is deemed simple enough to inline if either:
-- * It is smaller than some threshold and has no metavariables in it
-- * It's just a metavariable itself
noMeta : Term vs -> Nat -> Bool
noMeta (App _ f a) (S k) = noMeta f k && noMeta a k
noMeta (Bind _ _ b sc) (S k) = noMeta (binderType b) k && noMeta sc k
noMeta (Meta _ _ _ _) d = False
noMeta (TDelayed _ _ t) d = noMeta t d
noMeta (TDelay _ _ t a) d = noMeta t d && noMeta a d
noMeta (TForce _ _ t) d = noMeta t d
noMeta (As _ _ a p) d = noMeta a d && noMeta p d
noMeta (Local _ _ _ _) _ = True
noMeta (Ref _ _ _) _ = True
noMeta (PrimVal _ _) _ = True
noMeta (TType _) _ = True
noMeta _ _ = False
isSimple : Term vs -> Bool
isSimple (Local _ _ _ _) = True
isSimple (Ref _ _ _) = True
isSimple (Meta _ _ _ _) = True
isSimple (Bind _ _ (Lam _ _ _ _) sc) = isSimple sc
isSimple (PrimVal _ _) = True
isSimple (TType _) = True
isSimple _ = False
isSimple (App _ f a) = noMeta f 6 && noMeta a 3
isSimple tm = noMeta tm 0
updateIVar : {v : Nat} ->
forall vs, newvars . IVars vs newvars -> (0 p : IsVar nm v newvars) ->

1
src/Idris/Main.idr
View File

@ -1,6 +1,7 @@
module Idris.Main
import Idris.Driver
import Compiler.Common
main : IO ()
main = mainWithCodegens []

1
src/Libraries/Utils/Path.idr
View File

@ -1,6 +1,7 @@
module Libraries.Utils.Path
import Data.List
import Data.List1
import Data.Maybe
import Data.Nat
import Data.Strings

4
tests/idris2/basic044/expected
View File

@ -98,7 +98,7 @@ Term> Bye for now!
LOG declare.type:1: Processing Vec.Vec
LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1])
LOG declare.type:1: Processing Vec.Nil
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] ?Vec.{t:N}_[{arg:N}[0]] Data.Fin.Uninhabited implementation at Data/Fin.idr:L:C--L:C)
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data/Fin.idr:L:C--L:C)
LOG declare.type:1: Processing Vec.::
LOG declare.def:2: Case tree for Vec.::: case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
{ Data.Fin.FZ {e:N} => [0] {arg:N}[3]
@ -129,5 +129,5 @@ LOG elab.ambiguous:5: Ambiguous elaboration [($resolvedN 0), ($resolvedN 0)] at
With default. Target type : Prelude.Types.Nat
LOG elab.ambiguous:5: Ambiguous elaboration True [$resolvedN] at Vec.idr:L:C--L:C
Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: ?Vec.{n:N}_[] ?Vec.{a:N}_[] (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z ?Vec.{a:N}_[] (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil ?Vec.{a:N}_[])))
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.:: (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.:: Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.:: Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
Vec> Bye for now!