edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-12-25 13:54:55 +03:00
Code Issues Projects Releases Wiki Activity

Build and save references for metavars too

Browse Source 
This wasn't necessary before, since we always inlined, but since we can
now postpone things longer and don't always inline until much later, we
need to know what names everything refers to earlier.
This commit is contained in:
Edwin Brady 2019-06-27 09:01:59 +01:00
parent 2cd81a9eb0
commit ce78abaaef
7 changed files with 62 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Compiler/Common.idr
View File

@ -75,7 +75,7 @@ findUsedNames tm
let cns = keys allNs
-- Initialise the type constructor list with explicit names for
-- the primitives (this is how we look up the tags)
-- Use '1' for '->' constructor (although we can't match it yet!)
-- Use '1' for '->' constructor
let tyconInit = insert (UN "->") 1 $
insert (UN "Type") 2 $
primTags 3 empty

7
src/Core/Binary.idr
View File

@ -78,13 +78,6 @@ HasNames (Name, Name, Bool) where
full c (n1, n2, b) = pure (!(full c n1), !(full c n2), b)
resolved c (n1, n2, b) = pure (!(resolved c n1), !(resolved c n2), b)
HasNames (Maybe Name) where
full c Nothing = pure Nothing
full c (Just n) = pure $ Just !(full c n)
resolved c Nothing = pure Nothing
resolved c (Just n) = pure $ Just !(resolved c n)
HasNames e => HasNames (TTCFile e) where
full gam (MkTTCFile version ifaceHash iHashes
holes guesses constraints

12
src/Core/CaseTree.idr
View File

@ -114,8 +114,8 @@ Weaken CaseTree where
weakenNs ns t = insertCaseNames {outer = []} ns t
getNames : ({vs : _} -> NameMap Bool -> Term vs -> NameMap Bool) ->
CaseTree vars -> NameMap Bool
getNames add sc = getSet empty sc
NameMap Bool -> CaseTree vars -> NameMap Bool
getNames add ns sc = getSet ns sc
where
mutual
getAltSet : NameMap Bool -> CaseAlt vs -> NameMap Bool
@ -137,11 +137,15 @@ getNames add sc = getSet empty sc
export
getRefs : (aTotal : Name) -> CaseTree vars -> NameMap Bool
getRefs at = getNames (addRefs False at)
getRefs at = getNames (addRefs False at) empty
export
addRefs : (aTotal : Name) -> NameMap Bool -> CaseTree vars -> NameMap Bool
addRefs at ns = getNames (addRefs False at) ns
export
getMetas : CaseTree vars -> NameMap Bool
getMetas = getNames addMetas
getMetas = getNames addMetas empty
export
mkPat' : List Pat -> ClosedTerm -> ClosedTerm -> Pat

17
src/Core/Context.idr
View File

@ -154,7 +154,7 @@ record GlobalDef where
visibility : Visibility
totality : Totality
flags : List DefFlag
refersTo : NameMap Bool
refersToM : Maybe (NameMap Bool)
noCycles : Bool -- for metavariables, whether they can be cyclic (this
-- would only be allowed when using a metavariable as a
-- placeholder for a yet to be elaborated arguments, but
@ -165,6 +165,10 @@ record GlobalDef where
compexpr : Maybe CDef
sizeChange : List SCCall
export
refersTo : GlobalDef -> NameMap Bool
refersTo def = maybe empty id (refersToM def)
-- Label for array references
export
data Arr : Type where
@ -602,6 +606,13 @@ HasNames SCCall where
full gam sc = pure $ record { fnCall = !(full gam (fnCall sc)) } sc
resolved gam sc = pure $ record { fnCall = !(resolved gam (fnCall sc)) } sc
export
HasNames a => HasNames (Maybe a) where
full gam Nothing = pure Nothing
full gam (Just x) = pure $ Just !(full gam x)
resolved gam Nothing = pure Nothing
resolved gam (Just x) = pure $ Just !(resolved gam x)
export
HasNames GlobalDef where
full gam def
@ -613,14 +624,14 @@ HasNames GlobalDef where
pure $ record { type = !(full gam (type def)),
definition = !(full gam (definition def)),
totality = !(full gam (totality def)),
refersTo = !(full gam (refersTo def)),
refersToM = !(full gam (refersToM def)),
sizeChange = !(traverse (full gam) (sizeChange def))
} def
resolved gam def
= pure $ record { type = !(resolved gam (type def)),
definition = !(resolved gam (definition def)),
totality = !(resolved gam (totality def)),
refersTo = !(resolved gam (refersTo def)),
refersToM = !(resolved gam (refersToM def)),
sizeChange = !(traverse (resolved gam) (sizeChange def))
} def

8
src/Core/TTC.idr
View File

@ -777,6 +777,7 @@ TTC GlobalDef where
do toBuf b (fullname gdef)
toBuf b (definition gdef)
toBuf b (compexpr gdef)
toBuf b (map toList (refersToM gdef))
when (isUserName (fullname gdef)) $
do toBuf b (location gdef)
toBuf b (type gdef)
@ -785,7 +786,6 @@ TTC GlobalDef where
toBuf b (visibility gdef)
toBuf b (totality gdef)
toBuf b (flags gdef)
toBuf b (toList (refersTo gdef))
toBuf b (noCycles gdef)
toBuf b (sizeChange gdef)
@ -793,21 +793,21 @@ TTC GlobalDef where
= do name <- fromBuf b
def <- fromBuf b
cdef <- fromBuf b
refsList <- fromBuf b;
let refs = map fromList refsList
if isUserName name
then do loc <- fromBuf b;
ty <- fromBuf b; mul <- fromBuf b
vars <- fromBuf b
vis <- fromBuf b; tot <- fromBuf b
fl <- fromBuf b
refsList <- fromBuf b;
let refs = fromList refsList
c <- fromBuf b
sc <- fromBuf b
pure (MkGlobalDef loc name ty mul vars vis
tot fl refs c True def cdef sc)
else do let fc = emptyFC
pure (MkGlobalDef fc name (Erased fc)
RigW [] Public unchecked [] empty
RigW [] Public unchecked [] refs
False True def cdef [])
-- decode : Context -> Int -> ContextEntry -> Core GlobalDef

48
src/TTImp/ProcessDef.idr
View File

@ -534,6 +534,23 @@ compileRunTime
defs <- get Ctxt
put Ctxt (record { toCompile = [] } defs)
-- Calculate references for the given name, and recursively if they haven't
-- been calculated already
calcRefs : {auto c : Ref Ctxt Defs} ->
(aTotal : Name) -> (fn : Name) -> Core ()
calcRefs at fn
= do defs <- get Ctxt
Just gdef <- lookupCtxtExact fn (gamma defs)
| _ => pure ()
let PMDef cargs tree_ct _ pats = definition gdef
| _ => pure () -- not a function definition
let Nothing = refersToM gdef
| Just _ => pure () -- already done
let metas = getMetas tree_ct
let refs = addRefs at metas tree_ct
addDef fn (record { refersToM = Just refs } gdef)
traverse_ (calcRefs at) (keys refs)
toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
toPats (MkClause {vars} env lhs rhs)
= (_ ** (env, lhs, rhs))
@ -566,35 +583,38 @@ processDef opts nest env fc n_in cs_in
logC 5 (do t <- toFullNames tree_ct
pure ("Case tree for " ++ show n ++ ": " ++ show t))
atotal <- toResolvedNames (NS ["Builtin"] (UN "assert_total"))
let refs = getRefs atotal tree_ct
let rmetas = getMetas tree_ct
-- Add compile time tree as a placeholder for the runtime tree,
-- but we'll rebuild that in a later pass once all the case
-- blocks etc are resolved
addDef n (record { definition = PMDef cargs tree_ct tree_ct pats,
refersTo = refs } gdef)
addDef (Resolved nidx)
(record { definition = PMDef cargs tree_ct tree_ct pats
} gdef)
let rmetas = getMetas tree_ct
traverse_ addToSave (keys rmetas)
addToSave n
log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys rmetas)
when (not (InCase `elem` opts)) $
do sc <- calculateSizeChange fc n
setSizeChange fc n sc
cov <- checkCoverage nidx mult cs tree_ct
setCovering fc n cov
-- Flag this name as one which needs compiling
defs <- get Ctxt
put Ctxt (record { toCompile $= (n ::) } defs)
-- Then if we're not in a case tree, do all the outstanding case
when (not (InCase `elem` opts)) $
do atotal <- toResolvedNames (NS ["Builtin"] (UN "assert_total"))
calcRefs atotal (Resolved nidx)
sc <- calculateSizeChange fc n
setSizeChange fc n sc
-- If we're not in a case tree, compile all the outstanding case
-- trees
when (not (elem InCase opts)) $
compileRunTime
cov <- checkCoverage nidx mult cs tree_ct
setCovering fc n cov
where
simplePat : Term vars -> Bool
simplePat (Local _ _ _ _) = True

2
tests/Main.idr
View File

@ -40,7 +40,7 @@ idrisTests
chezTests : List String
chezTests
= ["chez001", "chez002", "chez003"]
= ["chez001", "chez002", "chez003", "chez004"]
chdir : String -> IO Bool
chdir dir