edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-23 20:22:34 +03:00
Code Issues Projects Releases Wiki Activity

Erase the World, with care

Browse Source 
We can erase things of type %World, which opens up more possibilities of
newtype and helps optimise IO, but we need to be sure that the side
effecting operations aren't optimised away as a result because we no
longer have to inspect the newtype. Therefore, if optimising away a case
analysis on a newtype with a %World deleted, add a let binding for the
scrutinee of the case, and flag it as non-inlinable.
This commit is contained in:
Edwin Brady 2020-04-21 10:42:00 +01:00
parent 5ea11cf0f5
commit ac277ce6d0
11 changed files with 89 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

50
src/Compiler/CompileExpr.idr
View File

@ -35,7 +35,7 @@ numArgs defs (Ref _ _ n)
| Nothing => pure (Arity 0)
case definition gdef of
DCon _ arity Nothing => pure (EraseArgs arity (eraseArgs gdef))
DCon _ arity (Just pos) => pure (NewTypeBy arity pos)
DCon _ arity (Just (_, pos)) => pure (NewTypeBy arity pos)
PMDef _ args _ _ _ => pure (Arity (length args))
ExternDef arity => pure (Arity arity)
ForeignDef arity _ => pure (Arity arity)
@ -162,7 +162,7 @@ natBranch (MkConAlt n _ _ _) = isNatCon n
trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
trySBranch n (MkConAlt (NS ["Prelude"] (UN "S")) _ [arg] sc)
= let fc = getFC n in
Just (CLet fc arg (CApp fc (CRef fc (UN "prim__sub_Integer"))
Just (CLet fc arg True (CApp fc (CRef fc (UN "prim__sub_Integer"))
[n, CPrimVal fc (BI 1)]) sc)
trySBranch _ _ = Nothing
@ -216,7 +216,7 @@ mutual
toCExpTm tags n (Bind fc x (Let Rig0 val _) sc)
= pure $ shrinkCExp (DropCons SubRefl) !(toCExp tags n sc)
toCExpTm tags n (Bind fc x (Let _ val _) sc)
= pure $ CLet fc x !(toCExp tags n val) !(toCExp tags n sc)
= pure $ CLet fc x True !(toCExp tags n val) !(toCExp tags n sc)
toCExpTm tags n (Bind fc x (Pi c e ty) sc)
= pure $ CCon fc (UN "->") 1 [!(toCExp tags n ty),
CLam fc x !(toCExp tags n sc)]
@ -289,6 +289,8 @@ mutual
NameTags -> 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)
@ -297,16 +299,25 @@ mutual
getDef : {auto c : Ref Ctxt Defs} ->
FC -> CExp vars ->
NameTags -> Name -> List (CaseAlt vars) ->
Core (Maybe (CExp vars))
getDef fc scr tags n [] = pure Nothing
Core (Bool, Maybe (CExp vars))
getDef fc scr tags n [] = pure (False, Nothing)
getDef fc scr tags n (DefaultCase sc :: ns)
= pure $ Just !(toCExpTree tags n sc)
= pure $ (False, Just !(toCExpTree tags n sc))
getDef fc scr tags n (ConstCase WorldVal sc :: ns)
= pure $ (False, Just !(toCExpTree tags n sc))
getDef {vars} fc scr tags n (ConCase x tag args sc :: ns)
= do defs <- get Ctxt
case !(lookupDefExact x (gamma defs)) of
Just (DCon _ arity (Just pos)) =>
-- If the flag is False, we still take the
-- default, but need to evaluate the scrutinee of the
-- case anyway - if the data structure contains a %World,
-- that we've erased, it means it has interacted with the
-- outside world, so we need to evaluate to keep the
-- side effect.
Just (DCon _ arity (Just (noworld, pos))) =>
let env : SubstCEnv args vars = mkSubst 0 pos args in
pure $ Just (substs env !(toCExpTree tags n sc))
pure $ (not noworld,
Just (substs env !(toCExpTree tags n sc)))
_ => getDef fc scr tags n ns
where
mkSubst : Nat -> Nat -> (args : List Name) -> SubstCEnv args vars
@ -323,8 +334,8 @@ mutual
toCExpTree tags n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
= let fc = getLoc scTy in
pure $
CLet fc arg (CForce fc (CLocal (getLoc scTy) x)) $
CLet fc ty (CErased fc)
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
@ -335,9 +346,13 @@ mutual
= let fc = getLoc scTy in
do defs <- get Ctxt
cases <- conCases tags n alts
def <- getDef fc (CLocal fc x) tags n alts
(keepSc, def) <- getDef fc (CLocal fc x) tags n alts
if isNil cases
then pure (fromMaybe (CErased fc) def)
then (if keepSc
then pure $ CLet fc (MN "eff" 0) False
(CLocal fc x)
(weaken (fromMaybe (CErased fc) def))
else pure (fromMaybe (CErased fc) def))
else pure $ natHackTree $
CConCase fc (CLocal fc x) cases def
toCExpTree' tags n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
@ -345,9 +360,13 @@ mutual
toCExpTree' tags n (Case fc x scTy alts@(ConstCase _ _ :: _))
= let fc = getLoc scTy in
do cases <- constCases tags n alts
def <- getDef fc (CLocal fc x) tags n alts
(keepSc, def) <- getDef fc (CLocal fc x) tags n alts
if isNil cases
then pure (fromMaybe (CErased fc) def)
then (if keepSc
then pure $ CLet fc (MN "eff" 0) False
(CLocal fc x)
(weaken (fromMaybe (CErased fc) def))
else 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
@ -498,7 +517,8 @@ toCDef tags n ty (Builtin {arity} op)
getVars NoArgs = []
getVars (ConsArg a rest) = MkVar First :: map weakenVar (getVars rest)
toCDef tags n _ (DCon tag arity pos)
= pure $ MkCon (fromMaybe tag $ lookup n tags) arity pos
= let nt = maybe Nothing (Just . snd) pos in
pure $ MkCon (fromMaybe tag $ lookup n tags) arity nt
toCDef tags n _ (TCon tag arity _ _ _ _ _ _)
= pure $ MkCon (fromMaybe tag $ lookup n tags) arity Nothing
-- We do want to be able to compile these, but also report an error at run time

12
src/Compiler/Inline.idr
View File

@ -62,7 +62,7 @@ mutual
used : Name -> CExp free -> Bool
used n (CRef _ n') = n == n'
used n (CLam _ _ sc) = used n sc
used n (CLet _ _ val sc) = used n val || used n sc
used n (CLet _ _ _ val sc) = used n val || used n sc
used n (CApp _ x args) = used n x || or (map Delay (map (used n) args))
used n (CCon _ _ _ args) = or (map Delay (map (used n) args))
used n (COp _ _ args) = or (map Delay (map (used n) args))
@ -133,12 +133,12 @@ mutual
sc' <- eval rec (CRef fc xn :: env) [] sc
pure $ CLam fc x (refToLocal xn x sc')
eval rec env (e :: stk) (CLam fc x sc) = eval rec (e :: env) stk sc
eval {vars} {free} rec env stk (CLet fc x val sc)
eval {vars} {free} rec env stk (CLet fc x inl val sc)
= do xn <- genName "letv"
sc' <- eval rec (CRef fc xn :: env) [] sc
if used xn sc'
if inl && used xn sc'
then do val' <- eval rec env [] val
pure (unload stk $ CLet fc x val' (refToLocal xn x sc'))
pure (unload stk $ CLet fc x inl val' (refToLocal xn x sc'))
else pure sc'
eval rec env stk (CApp fc f args)
= eval rec env (!(traverse (eval rec env []) args) ++ stk) f
@ -249,9 +249,9 @@ fixArityTm (CRef fc n) args
pure $ expandToArity arity (CApp fc (CRef fc n) []) args
fixArityTm (CLam fc x sc) args
= pure $ expandToArity Z (CLam fc x !(fixArityTm sc [])) args
fixArityTm (CLet fc x val sc) args
fixArityTm (CLet fc x inl val sc) args
= pure $ expandToArity Z
(CLet fc x !(fixArityTm val []) !(fixArityTm sc [])) args
(CLet fc x inl !(fixArityTm val []) !(fixArityTm sc [])) args
fixArityTm (CApp fc f fargs) args
= fixArityTm f (!(traverse (\tm => fixArityTm tm []) fargs) ++ args)
fixArityTm (CCon fc n t args) []

2
src/Compiler/LambdaLift.idr
View File

@ -174,7 +174,7 @@ mutual
liftExp (CLocal fc prf) = pure $ LLocal fc prf
liftExp (CRef fc n) = pure $ LAppName fc n [] -- probably shouldn't happen!
liftExp (CLam fc x sc) = makeLam fc [x] sc
liftExp (CLet fc x val sc) = pure $ LLet fc x !(liftExp val) !(liftExp sc)
liftExp (CLet fc x _ val sc) = pure $ LLet fc x !(liftExp val) !(liftExp sc)
liftExp (CApp fc (CRef _ n) args) -- names are applied exactly in compileExp
= pure $ LAppName fc n !(traverse liftExp args)
liftExp (CApp fc f args)

4
src/Compiler/Scheme/Chez.idr
View File

@ -209,9 +209,7 @@ cCall fc cfn clib args ret
mkFun args ret n
= let argns = mkNs 0 args in
"(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
(case ret of
CFIORes _ => getVal (applyLams n argns) ++ ")"
_ => applyLams n argns ++ ")")
(applyLams n argns ++ ")")
notWorld : CFType -> Bool
notWorld CFWorld = False

2
src/Compiler/Scheme/Common.idr
View File

@ -234,7 +234,7 @@ toPrim pn = Unknown pn
export
mkWorld : String -> String
mkWorld res = schConstructor 0 [res, "#f"] -- MkIORes
mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 [res, "#f"] -- MkIORes
schConstant : (String -> String) -> Constant -> String
schConstant _ (I x) = show x

8
src/Compiler/Scheme/Racket.idr
View File

@ -180,15 +180,11 @@ cCall fc cfn libspec args ret
applyLams n (Just (a, ty) :: as)
= applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as
getVal : CFType -> String -> String
getVal ty str = rktToC ty ("(vector-ref " ++ str ++ "1)")
mkFun : List CFType -> CFType -> String -> String
mkFun args ret n
= let argns = mkNs 0 args in
(case ret of
CFIORes rt => getVal rt (applyLams n argns) ++ ")"
_ => applyLams n argns ++ ")")
"(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++
(applyLams n argns ++ ")")
notWorld : CFType -> Bool
notWorld CFWorld = False

2
src/Core/Binary.idr
View File

@ -27,7 +27,7 @@ import Data.Buffer
-- TTC files can only be compatible if the version number is the same
export
ttcVersion : Int
ttcVersion = 21
ttcVersion = 22
export
checkTTCVersion : String -> Int -> Int -> Core ()

29
src/Core/CompileExpr.idr
View File

@ -19,7 +19,8 @@ mutual
-- Lambda expression
CLam : FC -> (x : Name) -> CExp (x :: vars) -> CExp vars
-- Let bindings
CLet : FC -> (x : Name) -> CExp vars -> CExp (x :: vars) -> CExp vars
CLet : FC -> (x : Name) -> (inlineOK : Bool) -> -- Don't inline if set
CExp vars -> CExp (x :: vars) -> CExp vars
-- Application of a defined function. The length of the argument list is
-- exactly the same length as expected by its definition (so saturate with
-- lambdas if necessary, or overapply with additional CApps)
@ -224,7 +225,7 @@ mutual
forgetExp locs (CLam fc x sc)
= let locs' = addLocs [x] locs in
NmLam fc (getLocName _ locs' First) (forgetExp locs' sc)
forgetExp locs (CLet fc x val sc)
forgetExp locs (CLet fc x _ val sc)
= let locs' = addLocs [x] locs in
NmLet fc (getLocName _ locs' First)
(forgetExp locs val)
@ -326,9 +327,9 @@ mutual
thin {outer} {inner} n (CLam fc x sc)
= let sc' = thin {outer = x :: outer} {inner} n sc in
CLam fc x sc'
thin {outer} {inner} n (CLet fc x val sc)
thin {outer} {inner} n (CLet fc x inl val sc)
= let sc' = thin {outer = x :: outer} {inner} n sc in
CLet fc x (thin n val) sc'
CLet fc x inl (thin n val) sc'
thin n (CApp fc x xs)
= CApp fc (thin n x) (assert_total (map (thin n) xs))
thin n (CCon fc x tag xs)
@ -372,9 +373,9 @@ mutual
insertNames {outer} {inner} ns (CLam fc x sc)
= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
CLam fc x sc'
insertNames {outer} {inner} ns (CLet fc x val sc)
insertNames {outer} {inner} ns (CLet fc x inl val sc)
= let sc' = insertNames {outer = x :: outer} {inner} ns sc in
CLet fc x (insertNames ns val) sc'
CLet fc x inl (insertNames ns val) sc'
insertNames ns (CApp fc x xs)
= CApp fc (insertNames ns x) (assert_total (map (insertNames ns) xs))
insertNames ns (CCon fc x tag xs)
@ -416,7 +417,7 @@ mutual
embed (CLocal fc prf) = CLocal fc (varExtend prf)
embed (CRef fc n) = CRef fc n
embed (CLam fc x sc) = CLam fc x (embed sc)
embed (CLet fc x val sc) = CLet fc x (embed val) (embed sc)
embed (CLet fc x inl val sc) = CLet fc x inl (embed val) (embed sc)
embed (CApp fc f args) = CApp fc (embed f) (assert_total (map embed args))
embed (CCon fc n t args) = CCon fc n t (assert_total (map embed args))
embed (COp fc p args) = COp fc p (assert_total (map embed args))
@ -454,9 +455,9 @@ mutual
shrinkCExp sub (CLam fc x sc)
= let sc' = shrinkCExp (KeepCons sub) sc in
CLam fc x sc'
shrinkCExp sub (CLet fc x val sc)
shrinkCExp sub (CLet fc x inl val sc)
= let sc' = shrinkCExp (KeepCons sub) sc in
CLet fc x (shrinkCExp sub val) sc'
CLet fc x inl (shrinkCExp sub val) sc'
shrinkCExp sub (CApp fc x xs)
= CApp fc (shrinkCExp sub x) (assert_total (map (shrinkCExp sub) xs))
shrinkCExp sub (CCon fc x tag xs)
@ -525,9 +526,9 @@ mutual
substEnv {outer} env (CLam fc x sc)
= let sc' = substEnv {outer = x :: outer} env sc in
CLam fc x sc'
substEnv {outer} env (CLet fc x val sc)
substEnv {outer} env (CLet fc x inl val sc)
= let sc' = substEnv {outer = x :: outer} env sc in
CLet fc x (substEnv env val) sc'
CLet fc x inl (substEnv env val) sc'
substEnv env (CApp fc x xs)
= CApp fc (substEnv env x) (assert_total (map (substEnv env) xs))
substEnv env (CCon fc x tag xs)
@ -591,9 +592,9 @@ mutual
mkLocals {later} {vars} bs (CLam fc x sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLam fc x sc'
mkLocals {later} {vars} bs (CLet fc x val sc)
mkLocals {later} {vars} bs (CLet fc x inl val sc)
= let sc' = mkLocals bs {later = x :: later} {vars} sc in
CLet fc x (mkLocals bs val) sc'
CLet fc x inl (mkLocals bs val) sc'
mkLocals bs (CApp fc f xs)
= CApp fc (mkLocals bs f) (assert_total (map (mkLocals bs) xs))
mkLocals bs (CCon fc x tag xs)
@ -641,7 +642,7 @@ getFC : CExp args -> FC
getFC (CLocal fc _) = fc
getFC (CRef fc _) = fc
getFC (CLam fc _ _) = fc
getFC (CLet fc _ _ _) = fc
getFC (CLet fc _ _ _ _) = fc
getFC (CApp fc _ _) = fc
getFC (CCon fc _ _ _) = fc
getFC (COp fc _ _) = fc

10
src/Core/Context.idr
View File

@ -65,8 +65,14 @@ data Def : Type where
Def
Builtin : {arity : Nat} -> PrimFn arity -> Def
DCon : (tag : Int) -> (arity : Nat) ->
(newtypeArg : Maybe Nat) -> -- if only constructor, and only one
-- argument is non-Rig0, flag it here,
(newtypeArg : Maybe (Bool, Nat)) ->
-- if only constructor, and only one argument is non-Rig0,
-- flag it here. The Nat is the unerased argument position.
-- The Bool is 'True' if there is no %World token in the
-- structure, which means it is safe to completely erase
-- when pattern matching (otherwise we still have to ensure
-- that the value is inspected, to make sure external effects
-- happen)
Def -- data constructor
TCon : (tag : Int) -> (arity : Nat) ->
(parampos : List Nat) -> -- parameters

6
src/Core/TTC.idr
View File

@ -583,7 +583,7 @@ mutual
toBuf b (CLocal fc {x} {idx} h) = do tag 0; toBuf b fc; toBuf b x; toBuf b idx
toBuf b (CRef fc n) = do tag 1; toBuf b fc; toBuf b n
toBuf b (CLam fc x sc) = do tag 2; toBuf b fc; toBuf b x; toBuf b sc
toBuf b (CLet fc x val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b val; toBuf b sc
toBuf b (CLet fc x inl val sc) = do tag 3; toBuf b fc; toBuf b x; toBuf b inl; toBuf b val; toBuf b sc
toBuf b (CApp fc f as) = assert_total $ do tag 4; toBuf b fc; toBuf b f; toBuf b as
toBuf b (CCon fc t n as) = assert_total $ do tag 5; toBuf b fc; toBuf b t; toBuf b n; toBuf b as
toBuf b (COp {arity} fc op as) = assert_total $ do tag 6; toBuf b fc; toBuf b arity; toBuf b op; toBuf b as
@ -608,8 +608,8 @@ mutual
x <- fromBuf b; sc <- fromBuf b
pure (CLam fc x sc)
3 => do fc <- fromBuf b
x <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
pure (CLet fc x val sc)
x <- fromBuf b; inl <- fromBuf b; val <- fromBuf b; sc <- fromBuf b
pure (CLet fc x inl val sc)
4 => do fc <- fromBuf b
f <- fromBuf b; as <- fromBuf b
pure (CApp fc f as)

24
src/TTImp/ProcessData.idr
View File

@ -195,16 +195,24 @@ getDetags fc tys
else pure rest
-- If exactly one argument is unerased, return its position
getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat)
getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc)
= getRelevantArg defs (1 + i) rel
getRelevantArg : Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
Core (Maybe (Bool, Nat))
getRelevantArg defs i rel world (NBind fc _ (Pi Rig0 _ _) sc)
= getRelevantArg defs (1 + i) rel world
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i Nothing (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
= getRelevantArg defs (1 + i) (Just i)
-- %World is never inspected, so might as well be deleted from data types,
-- although it needs care when compiling to ensure that the function that
-- returns the IO/%World type isn't erased
getRelevantArg defs i rel world (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc)
= getRelevantArg defs (1 + i) rel False
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i (Just _) (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
getRelevantArg defs i Nothing world (NBind fc _ (Pi _ _ _) sc) -- found a relevant arg
= getRelevantArg defs (1 + i) (Just i) world
!(sc defs (toClosure defaultOpts [] (Erased fc False)))
getRelevantArg defs i (Just _) world (NBind _ _ (Pi _ _ _) sc) -- more than one relevant
= pure Nothing
getRelevantArg defs i rel tm = pure rel
getRelevantArg defs i rel world tm
= pure (maybe Nothing (\r => Just (world, r)) rel)
-- If there's one constructor with only one non-Rig0 argument, flag it as
-- a newtype for optimisation
@ -213,7 +221,7 @@ findNewtype : {auto c : Ref Ctxt Defs} ->
List Constructor -> Core ()
findNewtype [con]
= do defs <- get Ctxt
Just arg <- getRelevantArg defs 0 Nothing !(nf defs [] (type con))
Just arg <- getRelevantArg defs 0 Nothing True !(nf defs [] (type con))
| Nothing => pure ()
updateDef (name con)
(\d => case d of