mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Do compiling/inlining per module
Compiled and inlined code is now written to the ttc, to save having to compile everything at the end even if some definitions don't need recompiling.
This commit is contained in:
Edwin Brady
parent
18b6449657
commit
87c54caa27
4
dist/rts/idris_rts.c
vendored
4
dist/rts/idris_rts.c
vendored
@ -287,8 +287,10 @@ static VAL mkstrlen(VM* vm, const char * str, size_t len, int outer) {
|
||||
String * cl = allocStr(vm, len, outer);
|
||||
// hdr.u8 used to mark a null string
|
||||
cl->hdr.u8 = str == NULL;
|
||||
if (!cl->hdr.u8)
|
||||
if (!cl->hdr.u8) {
|
||||
memcpy(cl->str, str, len);
|
||||
cl->str[len] = '\0';
|
||||
}
|
||||
return (VAL)cl;
|
||||
}
|
||||
|
||||
|
||||
@ -33,7 +33,6 @@ public export
|
||||
record CompileData where
|
||||
constructor MkCompileData
|
||||
allNames : List Name -- names which need to be compiled
|
||||
nameTags : NameTags -- a mapping from type names to constructor tags
|
||||
mainExpr : CExp [] -- main expression to execute. This also appears in
|
||||
-- the definitions below as MN "__mainExpression" 0
|
||||
lambdaLifted : List (Name, LiftedDef)
|
||||
@ -84,22 +83,14 @@ getAllDesc (n@(Resolved i) :: rest) arr defs
|
||||
case !(lookupCtxtExact n (gamma defs)) of
|
||||
Nothing => getAllDesc rest arr defs
|
||||
Just def =>
|
||||
do coreLift $ writeArray arr i i
|
||||
let refs = refersToRuntime def
|
||||
getAllDesc (keys refs ++ rest) arr defs
|
||||
if multiplicity def /= erased
|
||||
then do coreLift $ writeArray arr i i
|
||||
let refs = refersToRuntime def
|
||||
getAllDesc (keys refs ++ rest) arr defs
|
||||
else getAllDesc rest arr defs
|
||||
getAllDesc (n :: rest) arr defs
|
||||
= getAllDesc rest arr defs
|
||||
|
||||
-- Calculate a unique tag for each type constructor name we're compiling
|
||||
-- This is so that type constructor names get globally unique tags
|
||||
mkNameTags : Defs -> NameTags -> Int -> List Name -> Core NameTags
|
||||
mkNameTags defs tags t [] = pure tags
|
||||
mkNameTags defs tags t (n :: ns)
|
||||
= case !(lookupDefExact n (gamma defs)) of
|
||||
Just (TCon _ _ _ _ _ _ _ _)
|
||||
=> mkNameTags defs (insert n t tags) (t + 1) ns
|
||||
_ => mkNameTags defs tags t ns
|
||||
|
||||
natHackNames : List Name
|
||||
natHackNames
|
||||
= [UN "prim__add_Integer",
|
||||
@ -206,33 +197,20 @@ getCompileData tm_in
|
||||
let allNs = mapMaybe (maybe Nothing (Just . Resolved))
|
||||
!(coreLift (toList arr))
|
||||
cns <- traverse toFullNames allNs
|
||||
-- Initialise the type constructor list with explicit names for
|
||||
-- the primitives (this is how we look up the tags)
|
||||
-- Use '1' for '->' constructor
|
||||
let tyconInit = insert (UN "->") 1 $
|
||||
insert (UN "Type") 2 $
|
||||
primTags 3 empty
|
||||
[IntType, IntegerType, StringType,
|
||||
CharType, DoubleType, WorldType]
|
||||
tycontags <- mkNameTags defs tyconInit 100 cns
|
||||
logTime ("Compile defs " ++ show (length cns) ++ "/" ++ show asize) $
|
||||
traverse_ (compileDef tycontags) cns
|
||||
logTime "Inline" $ traverse_ inlineDef cns
|
||||
logTime "Merge lambda" $ traverse_ mergeLamDef cns
|
||||
logTime "Fix arity" $ traverse_ fixArityDef cns
|
||||
-- Do another round, since merging lambdas might expose more
|
||||
-- optimisation opportunities, especially a really important one
|
||||
-- for io_bind.
|
||||
logTime "Inline" $ traverse_ inlineDef cns
|
||||
logTime "Merge lambda" $ traverse_ mergeLamDef cns
|
||||
logTime "Fix arity" $ traverse_ fixArityDef cns
|
||||
logTime "Forget names" $ traverse_ mkForgetDef cns
|
||||
|
||||
compiledtm <- fixArityExp !(compileExp tycontags tm)
|
||||
-- Do a round of merging/arity fixing for any names which were
|
||||
-- unknown due to cyclic modules (i.e. declared in one, defined in
|
||||
-- another)
|
||||
rcns <- filterM nonErased cns
|
||||
logTime "Merge lambda" $ traverse_ mergeLamDef rcns
|
||||
logTime "Fix arity" $ traverse_ fixArityDef rcns
|
||||
logTime "Forget names" $ traverse_ mkForgetDef rcns
|
||||
|
||||
compiledtm <- fixArityExp !(compileExp tm)
|
||||
let mainname = MN "__mainExpression" 0
|
||||
(liftedtm, ldefs) <- liftBody mainname compiledtm
|
||||
|
||||
lifted_in <- logTime "Lambda lift" $ traverse lambdaLift cns
|
||||
lifted_in <- logTime "Lambda lift" $ traverse lambdaLift rcns
|
||||
|
||||
let lifted = (mainname, MkLFun [] [] liftedtm) ::
|
||||
ldefs ++ concat lifted_in
|
||||
@ -243,7 +221,7 @@ getCompileData tm_in
|
||||
defs <- get Ctxt
|
||||
maybe (pure ())
|
||||
(\f => do coreLift $ putStrLn $ "Dumping case trees to " ++ f
|
||||
dumpCases defs f cns)
|
||||
dumpCases defs f rcns)
|
||||
(dumpcases sopts)
|
||||
maybe (pure ())
|
||||
(\f => do coreLift $ putStrLn $ "Dumping lambda lifted defs to " ++ f
|
||||
@ -257,13 +235,15 @@ getCompileData tm_in
|
||||
(\f => do coreLift $ putStrLn $ "Dumping VM defs to " ++ f
|
||||
dumpVMCode f vmcode)
|
||||
(dumpvmcode sopts)
|
||||
pure (MkCompileData cns tycontags compiledtm
|
||||
pure (MkCompileData rcns compiledtm
|
||||
lifted anf vmcode)
|
||||
where
|
||||
primTags : Int -> NameTags -> List Constant -> NameTags
|
||||
primTags t tags [] = tags
|
||||
primTags t tags (c :: cs)
|
||||
= primTags (t + 1) (insert (UN (show c)) t tags) cs
|
||||
nonErased : Name -> Core Bool
|
||||
nonErased n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure True
|
||||
pure (multiplicity gdef /= erased)
|
||||
|
||||
-- Some things missing from Prelude.File
|
||||
|
||||
|
||||
@ -14,13 +14,6 @@ import Data.Vect
|
||||
|
||||
%default covering
|
||||
|
||||
-- Calculate tags for type constructors from all of the modules - they need
|
||||
-- to be globally unique so we don't do this until just before compilation,
|
||||
-- which is when we know how many we have
|
||||
public export
|
||||
NameTags : Type
|
||||
NameTags = NameMap Int
|
||||
|
||||
data Args
|
||||
= NewTypeBy Nat Nat
|
||||
| EraseArgs Nat (List Nat)
|
||||
@ -213,118 +206,118 @@ boolHackTree t = t
|
||||
|
||||
mutual
|
||||
toCExpTm : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> Term vars -> Core (CExp vars)
|
||||
toCExpTm tags n (Local fc _ _ prf)
|
||||
Name -> Term vars -> Core (CExp vars)
|
||||
toCExpTm n (Local fc _ _ prf)
|
||||
= pure $ CLocal fc prf
|
||||
-- TMP HACK: extend this to all types which look like enumerations
|
||||
-- after erasure
|
||||
toCExpTm tags n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "True")))
|
||||
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "True")))
|
||||
= pure $ CPrimVal fc (I tag)
|
||||
toCExpTm tags n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "False")))
|
||||
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "False")))
|
||||
= pure $ CPrimVal fc (I tag)
|
||||
toCExpTm tags n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "LT")))
|
||||
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "LT")))
|
||||
= pure $ CPrimVal fc (I tag)
|
||||
toCExpTm tags n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "EQ")))
|
||||
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "EQ")))
|
||||
= pure $ CPrimVal fc (I tag)
|
||||
toCExpTm tags n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "GT")))
|
||||
toCExpTm n (Ref fc (DataCon tag Z) (NS ["Prelude"] (UN "GT")))
|
||||
= pure $ CPrimVal fc (I tag)
|
||||
toCExpTm tags n (Ref fc (DataCon tag arity) fn)
|
||||
toCExpTm n (Ref fc (DataCon tag arity) fn)
|
||||
= -- get full name for readability, and the Nat hack
|
||||
pure $ CCon fc !(getFullName fn) (Just tag) []
|
||||
toCExpTm tags n (Ref fc (TyCon tag arity) fn)
|
||||
toCExpTm n (Ref fc (TyCon tag arity) fn)
|
||||
= pure $ CCon fc fn Nothing []
|
||||
toCExpTm tags n (Ref fc _ fn)
|
||||
toCExpTm n (Ref fc _ fn)
|
||||
= do full <- getFullName fn
|
||||
-- ^ For readability of output code, and the Nat hack,
|
||||
pure $ CApp fc (CRef fc full) []
|
||||
toCExpTm tags n (Meta fc mn i args)
|
||||
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp tags n) args)
|
||||
toCExpTm tags n (Bind fc x (Lam _ _ _) sc)
|
||||
= pure $ CLam fc x !(toCExp tags n sc)
|
||||
toCExpTm tags n (Bind fc x (Let rig val _) sc)
|
||||
= pure $ branchZero (shrinkCExp (DropCons SubRefl) !(toCExp tags n sc))
|
||||
(CLet fc x True !(toCExp tags n val) !(toCExp tags n sc))
|
||||
toCExpTm n (Meta fc mn i args)
|
||||
= pure $ CApp fc (CRef fc mn) !(traverse (toCExp n) args)
|
||||
toCExpTm n (Bind fc x (Lam _ _ _) sc)
|
||||
= pure $ CLam fc x !(toCExp n sc)
|
||||
toCExpTm n (Bind fc x (Let rig val _) sc)
|
||||
= do sc' <- toCExp n sc
|
||||
pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
|
||||
(CLet fc x True !(toCExp n val) sc')
|
||||
rig
|
||||
toCExpTm tags n (Bind fc x (Pi c e ty) sc)
|
||||
= pure $ CCon fc (UN "->") Nothing [!(toCExp tags n ty),
|
||||
CLam fc x !(toCExp tags n sc)]
|
||||
toCExpTm tags n (Bind fc x b tm) = pure $ CErased fc
|
||||
toCExpTm n (Bind fc x (Pi c e ty) sc)
|
||||
= pure $ CCon fc (UN "->") Nothing [!(toCExp n ty),
|
||||
CLam fc x !(toCExp n sc)]
|
||||
toCExpTm n (Bind fc x b tm) = pure $ CErased fc
|
||||
-- We'd expect this to have been dealt with in toCExp, but for completeness...
|
||||
toCExpTm tags n (App fc tm arg)
|
||||
= pure $ CApp fc !(toCExp tags n tm) [!(toCExp tags n arg)]
|
||||
toCExpTm n (App fc tm arg)
|
||||
= pure $ CApp fc !(toCExp n tm) [!(toCExp n arg)]
|
||||
-- This shouldn't be in terms any more, but here for completeness
|
||||
toCExpTm tags n (As _ _ _ p) = toCExpTm tags n p
|
||||
toCExpTm n (As _ _ _ p) = toCExpTm n p
|
||||
-- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
|
||||
toCExpTm tags n (TDelayed fc _ _) = pure $ CErased fc
|
||||
toCExpTm tags n (TDelay fc _ _ arg)
|
||||
= pure (CDelay fc !(toCExp tags n arg))
|
||||
toCExpTm tags n (TForce fc _ arg)
|
||||
= pure (CForce fc !(toCExp tags n arg))
|
||||
toCExpTm tags n (PrimVal fc c)
|
||||
toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
|
||||
toCExpTm n (TDelay fc _ _ arg)
|
||||
= pure (CDelay fc !(toCExp n arg))
|
||||
toCExpTm n (TForce fc _ arg)
|
||||
= pure (CForce fc !(toCExp n arg))
|
||||
toCExpTm n (PrimVal fc c)
|
||||
= let t = constTag c in
|
||||
if t == 0
|
||||
then pure $ CPrimVal fc c
|
||||
else pure $ CCon fc (UN (show c)) Nothing []
|
||||
toCExpTm tags n (Erased fc _) = pure $ CErased fc
|
||||
toCExpTm tags n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
|
||||
toCExpTm n (Erased fc _) = pure $ CErased fc
|
||||
toCExpTm n (TType fc) = pure $ CCon fc (UN "Type") Nothing []
|
||||
|
||||
toCExp : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> Term vars -> Core (CExp vars)
|
||||
toCExp tags n tm
|
||||
Name -> Term vars -> Core (CExp vars)
|
||||
toCExp n tm
|
||||
= case getFnArgs tm of
|
||||
(f, args) =>
|
||||
do args' <- traverse (toCExp tags n) args
|
||||
do args' <- traverse (toCExp n) args
|
||||
defs <- get Ctxt
|
||||
f' <- toCExpTm n f
|
||||
Arity a <- numArgs defs f
|
||||
| NewTypeBy arity pos =>
|
||||
do let res = applyNewType arity pos !(toCExpTm tags n f) args'
|
||||
do let res = applyNewType arity pos f' args'
|
||||
pure $ natHack res
|
||||
| EraseArgs arity epos =>
|
||||
do let res = eraseConArgs arity epos !(toCExpTm tags n f) args'
|
||||
do let res = eraseConArgs arity epos f' args'
|
||||
pure $ natHack res
|
||||
let res = expandToArity a !(toCExpTm tags n f) args'
|
||||
let res = expandToArity a f' args'
|
||||
pure $ natHack res
|
||||
|
||||
mutual
|
||||
conCases : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> List (CaseAlt vars) ->
|
||||
Name -> List (CaseAlt vars) ->
|
||||
Core (List (CConAlt vars))
|
||||
conCases tags n [] = pure []
|
||||
conCases {vars} tags n (ConCase x tag args sc :: ns)
|
||||
conCases n [] = pure []
|
||||
conCases {vars} n (ConCase x tag args sc :: ns)
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact x (gamma defs)
|
||||
| Nothing => -- primitive type match
|
||||
do xn <- getFullName x
|
||||
pure $ MkConAlt xn Nothing args !(toCExpTree tags n sc)
|
||||
:: !(conCases tags n ns)
|
||||
pure $ MkConAlt xn Nothing args !(toCExpTree n sc)
|
||||
:: !(conCases n ns)
|
||||
case (definition gdef) of
|
||||
DCon _ arity (Just pos) => conCases tags n ns -- skip it
|
||||
DCon _ arity (Just pos) => conCases n ns -- skip it
|
||||
_ => do xn <- getFullName x
|
||||
let (args' ** sub)
|
||||
= mkDropSubst 0 (eraseArgs gdef) vars args
|
||||
sc' <- toCExpTree n sc
|
||||
ns' <- conCases n ns
|
||||
if dcon (definition gdef)
|
||||
then pure $ MkConAlt xn (Just tag) args'
|
||||
(shrinkCExp sub !(toCExpTree tags n sc))
|
||||
:: !(conCases tags n ns)
|
||||
else pure $ MkConAlt xn Nothing args'
|
||||
(shrinkCExp sub !(toCExpTree tags n sc))
|
||||
:: !(conCases tags n ns)
|
||||
then pure $ MkConAlt xn (Just tag) args' (shrinkCExp sub sc') :: ns'
|
||||
else pure $ MkConAlt xn Nothing args' (shrinkCExp sub sc') :: ns'
|
||||
where
|
||||
dcon : Def -> Bool
|
||||
dcon (DCon _ _ _) = True
|
||||
dcon _ = False
|
||||
conCases tags n (_ :: ns) = conCases tags n ns
|
||||
conCases n (_ :: ns) = conCases n ns
|
||||
|
||||
constCases : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> List (CaseAlt vars) ->
|
||||
Name -> List (CaseAlt vars) ->
|
||||
Core (List (CConstAlt vars))
|
||||
constCases tags n [] = pure []
|
||||
constCases tags n (ConstCase WorldVal sc :: ns)
|
||||
= constCases tags n ns
|
||||
constCases tags n (ConstCase x sc :: ns)
|
||||
= pure $ MkConstAlt x !(toCExpTree tags n sc) ::
|
||||
!(constCases tags n ns)
|
||||
constCases tags n (_ :: ns) = constCases tags n ns
|
||||
constCases n [] = pure []
|
||||
constCases n (ConstCase WorldVal sc :: ns)
|
||||
= constCases n ns
|
||||
constCases n (ConstCase x sc :: ns)
|
||||
= pure $ MkConstAlt x !(toCExpTree n sc) ::
|
||||
!(constCases n ns)
|
||||
constCases n (_ :: ns) = constCases n ns
|
||||
|
||||
-- If there's a case which matches on a 'newtype', return the RHS
|
||||
-- without matching.
|
||||
@ -333,12 +326,12 @@ mutual
|
||||
-- once.
|
||||
getNewType : {auto c : Ref Ctxt Defs} ->
|
||||
FC -> CExp vars ->
|
||||
NameTags -> Name -> List (CaseAlt vars) ->
|
||||
Name -> List (CaseAlt vars) ->
|
||||
Core (Maybe (CExp vars))
|
||||
getNewType fc scr tags n [] = pure Nothing
|
||||
getNewType fc scr tags n (DefaultCase sc :: ns)
|
||||
getNewType fc scr n [] = pure Nothing
|
||||
getNewType fc scr n (DefaultCase sc :: ns)
|
||||
= pure $ Nothing
|
||||
getNewType {vars} fc scr tags n (ConCase x tag args sc :: ns)
|
||||
getNewType {vars} fc scr n (ConCase x tag args sc :: ns)
|
||||
= do defs <- get Ctxt
|
||||
case !(lookupDefExact x (gamma defs)) of
|
||||
-- If the flag is False, we still take the
|
||||
@ -359,12 +352,12 @@ mutual
|
||||
-- then
|
||||
let env : SubstCEnv args vars
|
||||
= mkSubst 0 scr pos args in
|
||||
pure $ Just (substs env !(toCExpTree tags n sc))
|
||||
pure $ Just (substs env !(toCExpTree n sc))
|
||||
-- else -- let bind the scrutinee, and substitute the
|
||||
-- -- name into the RHS
|
||||
-- let env : SubstCEnv args (MN "eff" 0 :: vars)
|
||||
-- = mkSubst 0 (CLocal fc First) pos args in
|
||||
-- do sc' <- toCExpTree tags n sc
|
||||
-- do sc' <- toCExpTree n sc
|
||||
-- let scope = thin {outer=args}
|
||||
-- {inner=vars}
|
||||
-- (MN "eff" 0) sc'
|
||||
@ -379,61 +372,61 @@ mutual
|
||||
= if i == pos
|
||||
then scr :: mkSubst (1 + i) scr pos as
|
||||
else CErased fc :: mkSubst (1 + i) scr pos as
|
||||
getNewType fc scr tags n (_ :: ns) = getNewType fc scr tags n ns
|
||||
getNewType fc scr n (_ :: ns) = getNewType fc scr n ns
|
||||
|
||||
getDef : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> List (CaseAlt vars) ->
|
||||
Name -> List (CaseAlt vars) ->
|
||||
Core (Maybe (CExp vars))
|
||||
getDef tags n [] = pure Nothing
|
||||
getDef tags n (DefaultCase sc :: ns)
|
||||
= pure $ Just !(toCExpTree tags n sc)
|
||||
getDef tags n (ConstCase WorldVal sc :: ns)
|
||||
= pure $ Just !(toCExpTree tags n sc)
|
||||
getDef tags n (_ :: ns) = getDef tags n ns
|
||||
getDef n [] = pure Nothing
|
||||
getDef n (DefaultCase sc :: ns)
|
||||
= pure $ Just !(toCExpTree n sc)
|
||||
getDef n (ConstCase WorldVal sc :: ns)
|
||||
= pure $ Just !(toCExpTree n sc)
|
||||
getDef n (_ :: ns) = getDef n ns
|
||||
|
||||
toCExpTree : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> CaseTree vars ->
|
||||
Name -> CaseTree vars ->
|
||||
Core (CExp vars)
|
||||
toCExpTree tags n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
|
||||
toCExpTree n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
|
||||
= let fc = getLoc scTy in
|
||||
pure $
|
||||
CLet fc arg True (CForce fc (CLocal (getLoc scTy) x)) $
|
||||
CLet fc ty True (CErased fc)
|
||||
!(toCExpTree tags n sc)
|
||||
toCExpTree tags n alts
|
||||
= toCExpTree' tags n alts
|
||||
!(toCExpTree n sc)
|
||||
toCExpTree n alts
|
||||
= toCExpTree' n alts
|
||||
|
||||
toCExpTree' : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> CaseTree vars ->
|
||||
Name -> CaseTree vars ->
|
||||
Core (CExp vars)
|
||||
toCExpTree' tags n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
|
||||
toCExpTree' n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
|
||||
= let fc = getLoc scTy in
|
||||
do Nothing <- getNewType fc (CLocal fc x) tags n alts
|
||||
do Nothing <- getNewType fc (CLocal fc x) n alts
|
||||
| Just def => pure def
|
||||
defs <- get Ctxt
|
||||
cases <- conCases tags n alts
|
||||
def <- getDef tags n alts
|
||||
cases <- conCases n alts
|
||||
def <- getDef n alts
|
||||
if isNil cases
|
||||
then pure (fromMaybe (CErased fc) def)
|
||||
else pure $ boolHackTree $ natHackTree $
|
||||
CConCase fc (CLocal fc x) cases def
|
||||
toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
|
||||
toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
|
||||
= throw (InternalError "Unexpected DelayCase")
|
||||
toCExpTree' tags n (Case fc x scTy alts@(ConstCase _ _ :: _))
|
||||
toCExpTree' n (Case fc x scTy alts@(ConstCase _ _ :: _))
|
||||
= let fc = getLoc scTy in
|
||||
do cases <- constCases tags n alts
|
||||
def <- getDef tags n alts
|
||||
do cases <- constCases n alts
|
||||
def <- getDef n alts
|
||||
if isNil cases
|
||||
then pure (fromMaybe (CErased fc) def)
|
||||
else pure $ CConstCase fc (CLocal fc x) cases def
|
||||
toCExpTree' tags n (Case _ x scTy alts@(DefaultCase sc :: _))
|
||||
= toCExpTree tags n sc
|
||||
toCExpTree' tags n (Case _ x scTy [])
|
||||
toCExpTree' n (Case _ x scTy alts@(DefaultCase sc :: _))
|
||||
= toCExpTree n sc
|
||||
toCExpTree' n (Case _ x scTy [])
|
||||
= pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
|
||||
toCExpTree' tags n (STerm tm) = toCExp tags n tm
|
||||
toCExpTree' tags n (Unmatched msg)
|
||||
toCExpTree' n (STerm tm) = toCExp n tm
|
||||
toCExpTree' n (Unmatched msg)
|
||||
= pure $ CCrash emptyFC msg
|
||||
toCExpTree' tags n Impossible
|
||||
toCExpTree' n Impossible
|
||||
= pure $ CCrash emptyFC ("Impossible case encountered in " ++ show n)
|
||||
|
||||
-- Need this for ensuring that argument list matches up to operator arity for
|
||||
@ -507,9 +500,10 @@ nfToCFType _ False (NBind fc _ (Pi _ _ ty) sc)
|
||||
pure (CFFun sty tty)
|
||||
nfToCFType _ True (NBind fc _ _ _)
|
||||
= throw (GenericMsg fc "Function types not allowed in a foreign struct")
|
||||
nfToCFType _ s (NTCon fc n _ _ args)
|
||||
nfToCFType _ s (NTCon fc n_in _ _ args)
|
||||
= do defs <- get Ctxt
|
||||
case !(getNArgs defs !(toFullNames n) args) of
|
||||
n <- toFullNames n_in
|
||||
case !(getNArgs defs n args) of
|
||||
User un uargs =>
|
||||
do nargs <- traverse (evalClosure defs) uargs
|
||||
cargs <- traverse (nfToCFType fc s) nargs
|
||||
@ -527,6 +521,10 @@ nfToCFType _ s (NTCon fc n _ _ args)
|
||||
do narg <- evalClosure defs uarg
|
||||
carg <- nfToCFType fc s narg
|
||||
pure (CFIORes carg)
|
||||
nfToCFType _ s (NType _)
|
||||
= pure (CFUser (UN "Type") [])
|
||||
nfToCFType _ s (NErased _ _)
|
||||
= pure (CFUser (UN "__") [])
|
||||
nfToCFType fc s t
|
||||
= do defs <- get Ctxt
|
||||
ty <- quote defs [] t
|
||||
@ -546,13 +544,13 @@ getCFTypes args t
|
||||
= pure (reverse args, !(nfToCFType (getLoc t) False t))
|
||||
|
||||
toCDef : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> Name -> ClosedTerm -> Def ->
|
||||
Name -> ClosedTerm -> Def ->
|
||||
Core CDef
|
||||
toCDef tags n ty None
|
||||
toCDef n ty None
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
|
||||
toCDef tags n ty (PMDef _ args _ tree _)
|
||||
= pure $ MkFun _ !(toCExpTree tags n tree)
|
||||
toCDef tags n ty (ExternDef arity)
|
||||
toCDef n ty (PMDef _ args _ tree _)
|
||||
= pure $ MkFun _ !(toCExpTree n tree)
|
||||
toCDef n ty (ExternDef arity)
|
||||
= let (ns ** args) = mkArgList 0 arity in
|
||||
pure $ MkFun _ (CExtPrim emptyFC !(getFullName n) (map toArgExp (getVars args)))
|
||||
where
|
||||
@ -562,11 +560,11 @@ toCDef tags n ty (ExternDef arity)
|
||||
getVars : ArgList k ns -> List (Var ns)
|
||||
getVars NoArgs = []
|
||||
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
|
||||
toCDef tags n ty (ForeignDef arity cs)
|
||||
toCDef n ty (ForeignDef arity cs)
|
||||
= do defs <- get Ctxt
|
||||
(atys, retty) <- getCFTypes [] !(nf defs [] ty)
|
||||
pure $ MkForeign cs atys retty
|
||||
toCDef tags n ty (Builtin {arity} op)
|
||||
toCDef n ty (Builtin {arity} op)
|
||||
= let (ns ** args) = mkArgList 0 arity in
|
||||
pure $ MkFun _ (COp emptyFC op (map toArgExp (getVars args)))
|
||||
where
|
||||
@ -576,41 +574,41 @@ toCDef tags n ty (Builtin {arity} op)
|
||||
getVars : ArgList k ns -> Vect k (Var ns)
|
||||
getVars NoArgs = []
|
||||
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
|
||||
toCDef tags n _ (DCon tag arity pos)
|
||||
toCDef n _ (DCon tag arity pos)
|
||||
= let nt = maybe Nothing (Just . snd) pos in
|
||||
pure $ MkCon (Just tag) arity nt
|
||||
toCDef tags n _ (TCon tag arity _ _ _ _ _ _)
|
||||
toCDef n _ (TCon tag arity _ _ _ _ _ _)
|
||||
= pure $ MkCon Nothing arity Nothing
|
||||
-- We do want to be able to compile these, but also report an error at run time
|
||||
-- (and, TODO: warn at compile time)
|
||||
toCDef tags n ty (Hole _ _)
|
||||
toCDef n ty (Hole _ _)
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered unimplemented hole " ++
|
||||
show !(getFullName n))
|
||||
toCDef tags n ty (Guess _ _ _)
|
||||
toCDef n ty (Guess _ _ _)
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered constrained hole " ++
|
||||
show !(getFullName n))
|
||||
toCDef tags n ty (BySearch _ _ _)
|
||||
toCDef n ty (BySearch _ _ _)
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered incomplete proof search " ++
|
||||
show !(getFullName n))
|
||||
toCDef tags n ty def
|
||||
toCDef n ty def
|
||||
= pure $ MkError $ CCrash emptyFC ("Encountered uncompilable name " ++
|
||||
show (!(getFullName n), def))
|
||||
|
||||
export
|
||||
compileExp : {auto c : Ref Ctxt Defs} ->
|
||||
NameTags -> ClosedTerm -> Core (CExp [])
|
||||
compileExp tags tm
|
||||
= do exp <- toCExp tags (UN "main") tm
|
||||
ClosedTerm -> Core (CExp [])
|
||||
compileExp tm
|
||||
= do exp <- toCExp (UN "main") tm
|
||||
pure exp
|
||||
|
||||
||| Given a name, look up an expression, and compile it to a CExp in the environment
|
||||
export
|
||||
compileDef : {auto c : Ref Ctxt Defs} -> NameTags -> Name -> Core ()
|
||||
compileDef tags n
|
||||
compileDef : {auto c : Ref Ctxt Defs} -> Name -> Core ()
|
||||
compileDef n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => throw (InternalError ("Trying to compile unknown name " ++ show n))
|
||||
ce <- toCDef tags n (type gdef)
|
||||
ce <- toCDef n (type gdef)
|
||||
!(toFullNames (definition gdef))
|
||||
setCompiled n ce
|
||||
|
||||
|
||||
@ -7,8 +7,9 @@ import Core.Context
|
||||
import Core.FC
|
||||
import Core.TT
|
||||
|
||||
import Data.Vect
|
||||
import Data.LengthMatch
|
||||
import Data.NameMap
|
||||
import Data.Vect
|
||||
|
||||
%default covering
|
||||
|
||||
@ -419,3 +420,27 @@ mergeLamDef n
|
||||
Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure ()
|
||||
let Just cexpr = compexpr def | Nothing => pure ()
|
||||
setCompiled n !(mergeLam cexpr)
|
||||
|
||||
export
|
||||
compileAndInlineAll : {auto c : Ref Ctxt Defs} ->
|
||||
Core ()
|
||||
compileAndInlineAll
|
||||
= do defs <- get Ctxt
|
||||
let ns = keys (toIR defs)
|
||||
cns <- filterM nonErased ns
|
||||
|
||||
traverse_ compileDef cns
|
||||
|
||||
traverse_ inlineDef cns
|
||||
traverse_ mergeLamDef cns
|
||||
traverse_ fixArityDef cns
|
||||
traverse_ inlineDef cns
|
||||
traverse_ mergeLamDef cns
|
||||
traverse_ fixArityDef cns
|
||||
where
|
||||
nonErased : Name -> Core Bool
|
||||
nonErased n
|
||||
= do defs <- get Ctxt
|
||||
Just gdef <- lookupCtxtExact n (gamma defs)
|
||||
| Nothing => pure False
|
||||
pure (multiplicity gdef /= erased)
|
||||
|
||||
@ -328,7 +328,6 @@ compileToSS c appdir tm outfile
|
||||
traverse_ copyLib libs
|
||||
cdata <- getCompileData tm
|
||||
let ns = allNames cdata
|
||||
let tags = nameTags cdata
|
||||
let ctm = forget (mainExpr cdata)
|
||||
|
||||
defs <- get Ctxt
|
||||
|
||||
@ -291,7 +291,6 @@ compileToRKT : Ref Ctxt Defs ->
|
||||
compileToRKT c tm outfile
|
||||
= do cdata <- getCompileData tm
|
||||
let ns = allNames cdata
|
||||
let tags = nameTags cdata
|
||||
let ctm = forget (mainExpr cdata)
|
||||
|
||||
defs <- get Ctxt
|
||||
|
||||
@ -27,7 +27,7 @@ import Data.Buffer
|
||||
-- TTC files can only be compatible if the version number is the same
|
||||
export
|
||||
ttcVersion : Int
|
||||
ttcVersion = 24
|
||||
ttcVersion = 25
|
||||
|
||||
export
|
||||
checkTTCVersion : String -> Int -> Int -> Core ()
|
||||
@ -200,7 +200,8 @@ readTTCFile : TTC extra =>
|
||||
Ref Bin Binary -> Core (TTCFile extra)
|
||||
readTTCFile modns as b
|
||||
= do hdr <- fromBuf b
|
||||
when (hdr /= "TTC") $ corrupt "TTC header"
|
||||
chunk <- get Bin
|
||||
when (hdr /= "TTC") $ corrupt ("TTC header in " ++ show modns ++ " " ++ show hdr)
|
||||
ver <- fromBuf b
|
||||
checkTTCVersion (show modns) ver ttcVersion
|
||||
ifaceHash <- fromBuf b
|
||||
@ -449,7 +450,7 @@ getImportHashes : String -> Ref Bin Binary ->
|
||||
Core (List (List String, Int))
|
||||
getImportHashes file b
|
||||
= do hdr <- fromBuf {a = String} b
|
||||
when (hdr /= "TTC") $ corrupt "TTC header"
|
||||
when (hdr /= "TTC") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
|
||||
ver <- fromBuf {a = Int} b
|
||||
checkTTCVersion file ver ttcVersion
|
||||
ifaceHash <- fromBuf {a = Int} b
|
||||
@ -458,7 +459,7 @@ getImportHashes file b
|
||||
getHash : String -> Ref Bin Binary -> Core Int
|
||||
getHash file b
|
||||
= do hdr <- fromBuf {a = String} b
|
||||
when (hdr /= "TTC") $ corrupt "TTC header"
|
||||
when (hdr /= "TTC") $ corrupt ("TTC header in " ++ file ++ " " ++ show hdr)
|
||||
ver <- fromBuf {a = Int} b
|
||||
checkTTCVersion file ver ttcVersion
|
||||
fromBuf b
|
||||
|
||||
@ -826,8 +826,11 @@ record Defs where
|
||||
cgdirectives : List (CG, String)
|
||||
-- ^ Code generator directives, which are free form text and thus to
|
||||
-- be interpreted however the specific code generator requires
|
||||
toCompile : List Name
|
||||
toCompileCase : List Name
|
||||
-- ^ Names which need to be compiled to run time case trees
|
||||
toIR : NameMap ()
|
||||
-- ^ Names which need to be compiled to IR at the end of processing
|
||||
-- the current module
|
||||
userHoles : NameMap ()
|
||||
-- ^ Metavariables the user still has to fill in. In practice, that's
|
||||
-- everything with a user accessible name and a definition of Hole
|
||||
@ -853,7 +856,7 @@ initDefs
|
||||
= do gam <- initCtxt
|
||||
pure (MkDefs gam [] ["Main"] [] defaults empty 100
|
||||
empty empty empty [] [] empty []
|
||||
empty 5381 [] [] [] [] [] empty empty empty)
|
||||
empty 5381 [] [] [] [] [] empty empty empty empty)
|
||||
|
||||
-- Reset the context, except for the options
|
||||
export
|
||||
@ -1061,9 +1064,12 @@ depth
|
||||
export
|
||||
addToSave : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
addToSave n
|
||||
addToSave n_in
|
||||
= do defs <- get Ctxt
|
||||
put Ctxt (record { toSave $= insert !(full (gamma defs) n) () } defs)
|
||||
n <- full (gamma defs) n_in
|
||||
put Ctxt (record { toSave $= insert n (),
|
||||
toIR $= insert n ()
|
||||
} defs)
|
||||
|
||||
-- Specific lookup functions
|
||||
export
|
||||
|
||||
@ -1,18 +1,18 @@
|
||||
module Core.InitPrimitives
|
||||
|
||||
import Compiler.CompileExpr
|
||||
|
||||
import Core.Context
|
||||
import Core.Primitives
|
||||
import Core.TT
|
||||
|
||||
-- import Data.NameMap
|
||||
|
||||
%default covering
|
||||
|
||||
addPrim : {auto c : Ref Ctxt Defs} ->
|
||||
Prim -> Core ()
|
||||
addPrim p
|
||||
= do addBuiltin (opName (fn p)) (type p) (totality p) (fn p)
|
||||
-- compileDef empty (opName (fn p))
|
||||
compileDef (opName (fn p))
|
||||
|
||||
export
|
||||
addPrimitives : {auto c : Ref Ctxt Defs} -> Core ()
|
||||
|
||||
@ -918,13 +918,13 @@ TTC GlobalDef where
|
||||
toBuf b (map toList (refersToM gdef))
|
||||
toBuf b (map toList (refersToRuntimeM gdef))
|
||||
toBuf b (location gdef)
|
||||
toBuf b (multiplicity gdef)
|
||||
when (isUserName (fullname gdef) || cwName (fullname gdef)) $
|
||||
do toBuf b (type gdef)
|
||||
toBuf b (eraseArgs gdef)
|
||||
toBuf b (safeErase gdef)
|
||||
toBuf b (specArgs gdef)
|
||||
toBuf b (inferrable gdef)
|
||||
toBuf b (multiplicity gdef)
|
||||
toBuf b (vars gdef)
|
||||
toBuf b (visibility gdef)
|
||||
toBuf b (totality gdef)
|
||||
@ -946,11 +946,12 @@ TTC GlobalDef where
|
||||
let refs = map fromList refsList
|
||||
let refsR = map fromList refsRList
|
||||
loc <- fromBuf b
|
||||
mul <- fromBuf b
|
||||
if isUserName name
|
||||
then do ty <- fromBuf b; eargs <- fromBuf b;
|
||||
seargs <- fromBuf b; specargs <- fromBuf b
|
||||
iargs <- fromBuf b;
|
||||
mul <- fromBuf b; vars <- fromBuf b
|
||||
vars <- fromBuf b
|
||||
vis <- fromBuf b; tot <- fromBuf b
|
||||
fl <- fromBuf b
|
||||
inv <- fromBuf b
|
||||
@ -960,7 +961,7 @@ TTC GlobalDef where
|
||||
mul vars vis
|
||||
tot fl refs refsR inv c True def cdef Nothing sc)
|
||||
else pure (MkGlobalDef loc name (Erased loc False) [] [] [] []
|
||||
top [] Public unchecked [] refs refsR
|
||||
mul [] Public unchecked [] refs refsR
|
||||
False False True def cdef Nothing [])
|
||||
|
||||
export
|
||||
|
||||
@ -1,5 +1,7 @@
|
||||
module Idris.ProcessIdr
|
||||
|
||||
import Compiler.Inline
|
||||
|
||||
import Core.Binary
|
||||
import Core.Context
|
||||
import Core.Directory
|
||||
@ -288,6 +290,8 @@ processMod srcf ttcf msg sourcecode
|
||||
errs <- logTime "Processing decls" $
|
||||
processDecls (decls mod)
|
||||
|
||||
logTime "Compile defs" $ compileAndInlineAll
|
||||
|
||||
-- Save the import hashes for the imports we just read.
|
||||
-- If they haven't changed next time, and the source
|
||||
-- file hasn't changed, no need to rebuild.
|
||||
|
||||
@ -607,11 +607,11 @@ compileRunTime : {auto c : Ref Ctxt Defs} ->
|
||||
Name -> Core ()
|
||||
compileRunTime atotal
|
||||
= do defs <- get Ctxt
|
||||
traverse_ mkRunTime (toCompile defs)
|
||||
traverse (calcRefs True atotal) (toCompile defs)
|
||||
traverse_ mkRunTime (toCompileCase defs)
|
||||
traverse (calcRefs True atotal) (toCompileCase defs)
|
||||
|
||||
defs <- get Ctxt
|
||||
put Ctxt (record { toCompile = [] } defs)
|
||||
put Ctxt (record { toCompileCase = [] } defs)
|
||||
|
||||
toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs))
|
||||
toPats (MkClause {vars} env lhs rhs)
|
||||
@ -662,7 +662,7 @@ processDef opts nest env fc n_in cs_in
|
||||
|
||||
-- Flag this name as one which needs compiling
|
||||
defs <- get Ctxt
|
||||
put Ctxt (record { toCompile $= (n ::) } defs)
|
||||
put Ctxt (record { toCompileCase $= (n ::) } defs)
|
||||
|
||||
atotal <- toResolvedNames (NS ["Builtin"] (UN "assert_total"))
|
||||
when (not (InCase `elem` opts)) $
|
||||
|
||||
@ -5,6 +5,7 @@ Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: Constructor tag Just 0 arity 1 (newtype by 0)
|
||||
Refers to: []
|
||||
Refers to (runtime): []
|
||||
Main> Main.MkBar ==> DataCon 0 1
|
||||
@ -13,6 +14,7 @@ Erasable args: []
|
||||
Detaggable arg types: []
|
||||
Specialise args: []
|
||||
Inferrable args: []
|
||||
Compiled: Constructor tag Just 0 arity 1
|
||||
Refers to: []
|
||||
Refers to (runtime): []
|
||||
Main> Bye for now!
|
||||
|
||||
Loading…
Reference in New Issue
Block a user