From 211fc359ca2913e6a32873a9e951ce0b6653111a Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Thu, 9 Apr 2020 00:20:37 +0100 Subject: [PATCH] Erase %World for the purpose of newtypes We never inspect it, so it carries no information - it just needs to be there as a token to make sure that IO operations run at the right time. So, IORes can be a newtype now and therefore optimised away. --- libs/prelude/PrimIO.idr | 1 + src/Compiler/CompileExpr.idr | 5 +++++ src/Compiler/Scheme/Chez.idr | 7 +------ src/Compiler/Scheme/Common.idr | 2 +- src/Compiler/Scheme/Racket.idr | 7 +------ src/Idris/Elab/Interface.idr | 1 + src/TTImp/ProcessData.idr | 4 ++++ 7 files changed, 14 insertions(+), 13 deletions(-) diff --git a/libs/prelude/PrimIO.idr b/libs/prelude/PrimIO.idr index 591df69..e379bd3 100644 --- a/libs/prelude/PrimIO.idr +++ b/libs/prelude/PrimIO.idr @@ -27,6 +27,7 @@ prim_io_bind : (1 act : PrimIO a) -> (1 k : a -> PrimIO b) -> PrimIO b prim_io_bind fn k w = let MkIORes x' w' = fn w in k x' w' +%inline export io_bind : (1 act : IO a) -> (1 k : a -> IO b) -> IO b io_bind (MkIO fn) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 84ec26c..8a81800 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -223,6 +223,7 @@ mutual pure $ natHack res mutual + -- In the below, treat %World, and newtypes, as default cases conCases : {auto c : Ref Ctxt Defs} -> NameTags -> Name -> List (CaseAlt vars) -> Core (List (CConAlt vars)) @@ -243,6 +244,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) @@ -255,6 +258,8 @@ mutual getDef fc scr tags n [] = pure Nothing getDef fc scr tags n (DefaultCase sc :: ns) = pure $ Just !(toCExpTree tags n sc) + getDef fc scr tags n (ConstCase WorldVal sc :: ns) + = pure $ 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 diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index cc53b8d..6a6c1ce 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -202,16 +202,11 @@ cCall fc cfn clib args ret applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as - getVal : String -> String - getVal str = "(vector-ref " ++ str ++ "2)" - mkFun : List CFType -> CFType -> String -> String 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 diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index d1db2be..b23ad90 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/src/Compiler/Scheme/Common.idr @@ -234,7 +234,7 @@ toPrim pn = Unknown pn export mkWorld : String -> String -mkWorld res = schConstructor 0 ["#f", res, "#f"] -- MkIORes +mkWorld res = res -- MkIORes is a newtype now! schConstructor 0 ["#f", res, "#f"] -- MkIORes schConstant : (String -> String) -> Constant -> String schConstant _ (I x) = show x diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 8ff0fd8..0ebf814 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -180,16 +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 ++ "2)") - mkFun : List CFType -> CFType -> String -> String mkFun args ret n = let argns = mkNs 0 args in "(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++ - (case ret of - CFIORes rt => getVal rt (applyLams n argns) ++ ")" - _ => applyLams n argns ++ ")") + (applyLams n argns ++ ")") notWorld : CFType -> Bool notWorld CFWorld = False diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 8c77cd1..e072332 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -308,6 +308,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body log 5 $ "Top level methods: " ++ show fns traverse (processDecl [] nest env) fns traverse_ (\n => do mn <- inCurrentNS n + setFlag fc mn Inline setFlag fc mn TCInline setFlag fc mn Overloadable) meth_names diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 31818e6..52a9363 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -197,6 +197,10 @@ getRelevantArg : Defs -> Nat -> Maybe Nat -> NF [] -> Core (Maybe Nat) getRelevantArg defs i rel (NBind fc _ (Pi Rig0 _ _) sc) = getRelevantArg defs (1 + i) rel !(sc defs (toClosure defaultOpts [] (Erased fc False))) +-- %World is never inspected, so might as well be deleted from data types +getRelevantArg defs i rel (NBind fc _ (Pi _ _ (NPrimVal _ WorldType)) sc) + = getRelevantArg defs (1 + i) rel + !(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) !(sc defs (toClosure defaultOpts [] (Erased fc False)))