[ cleanup ] Compiler/* modules (#2694)

* cleanup(Compiler/*) cleanup some messy/unclear code Also use primitives directly where possible, instead of idris's wrappers * Fix tests
2024-11-28 02:23:44 +03:00 · 2022-10-06 09:17:38 +01:00 · 2022-10-06 09:17:38 +01:00 · c69f439c2d
commit c69f439c2d
parent ff6ffad907
9 changed files with 98 additions and 121 deletions
--- a/src/Compiler/Common.idr
+++ b/src/Compiler/Common.idr
@ -211,11 +211,11 @@ replaceEntry (i, Just (ns, b))
    = ignore $ addContextEntry ns (Resolved i) b

 natHackNames : List Name
-natHackNames
-    = [UN (Basic "prim__add_Integer"),
-       UN (Basic "prim__sub_Integer"),
-       UN (Basic "prim__mul_Integer"),
-       NS typesNS (UN $ Basic "prim__integerToNat")]
+natHackNames =
+    [ UN (Basic "prim__sub_Integer")
+    , NS typesNS (UN $ Basic "prim__integerToNat")
+    , NS eqOrdNS (UN $ Basic "compareInteger")
+    ]

 dumpIR : Show def => String -> List (Name, def) -> Core ()
 dumpIR fn lns
--- a/src/Compiler/CompileExpr.idr
+++ b/src/Compiler/CompileExpr.idr
@ -182,15 +182,15 @@ magic__integerToNat fc fc' [k]
  = CApp fc (CRef fc' (NS typesNS (UN $ Basic "prim__integerToNat"))) [k]

 magic__natMinus : FC -> FC -> forall vars. Vect 2 (CExp vars) -> CExp vars
-magic__natMinus fc fc' [m,n]
+magic__natMinus fc fc' [m, n]
  = magic__integerToNat fc fc'
-    [CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, n]]
+    [COp fc (Sub IntegerType) [m, n]]

 -- We don't reuse natMinus here because we assume that unsuc will only be called
 -- on S-headed numbers so we do not need the truncating integerToNat call!
 magic__natUnsuc : FC -> FC -> forall vars. Vect 1 (CExp vars) -> CExp vars
 magic__natUnsuc fc fc' [m]
-  = CApp fc (CRef fc' (UN $ Basic "prim__sub_Integer")) [m, CPrimVal fc (BI 1)]
+  = COp fc (Sub IntegerType) [m, CPrimVal fc (BI 1)]

 -- TODO: next release remove this and use %builtin pragma
 natHack : List Magic
@ -198,19 +198,19 @@ natHack =
    [ MagicCRef (NS typesNS (UN $ Basic "natToInteger")) 1 (\ _, _, [k] => k)
    , MagicCRef (NS typesNS (UN $ Basic "integerToNat")) 1 magic__integerToNat
    , MagicCRef (NS typesNS (UN $ Basic "plus")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__add_Integer")) [m, n])
+         (\ fc, fc', [m,n] => COp fc (Add IntegerType) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "mult")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__mul_Integer")) [m, n])
+         (\ fc, fc', [m,n] => COp fc (Mul IntegerType) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "minus")) 2 magic__natMinus
    , MagicCRef (NS typesNS (UN $ Basic "equalNat")) 2
-         (\ fc, fc', [m,n] => CApp fc (CRef fc' (UN $ Basic "prim__eq_Integer")) [m, n])
+         (\ fc, fc', [m,n] => COp fc (EQ IntegerType) [m, n])
    , MagicCRef (NS typesNS (UN $ Basic "compareNat")) 2
         (\ fc, fc', [m,n] => CApp fc (CRef fc' (NS eqOrdNS (UN $ Basic "compareInteger"))) [m, n])
    ]

-- get all transformation from %builtin pragmas
-builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
-builtinMagic = pure $ magic natHack
+-- get all builtin transformations
+builtinMagic : forall vars. CExp vars -> CExp vars
+builtinMagic = magic natHack

 data NextMN : Type where
 newMN : {auto s : Ref NextMN Int} -> String -> Core Name
@ -235,11 +235,11 @@ tryZBranch _ = Nothing

 getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
 getSBranch n [] = Nothing
-getSBranch n (x :: xs) = trySBranch n x <+> getSBranch n xs
+getSBranch n (x :: xs) = trySBranch n x <|> getSBranch n xs

 getZBranch : List (CConAlt vars) -> Maybe (CExp vars)
 getZBranch [] = Nothing
-getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs
+getZBranch (x :: xs) = tryZBranch x <|> getZBranch xs

 -- Rewrite case trees on Nat to be case trees on Integer
 builtinNatTree : {auto s : Ref NextMN Int} -> CExp vars -> Core (CExp vars)
@ -302,82 +302,80 @@ dconFlag n
    ciFlags def (ConType ci :: xs) = ci
    ciFlags def (x :: xs) = ciFlags def xs

-mutual
-  toCExpTm : {vars : _} ->
-             {auto c : Ref Ctxt Defs} ->
-             {auto s : Ref NextMN Int} ->
-             (magic : forall vars. CExp vars -> CExp vars) ->
-             Name -> Term vars ->
-             Core (CExp vars)
-  toCExpTm m n (Local fc _ _ prf)
-      = pure $ CLocal fc prf
-  toCExpTm m n (Ref fc (DataCon tag arity) fn)
-      = do -- get full name for readability, and %builtin Natural
-           cn <- getFullName fn
-           fl <- dconFlag cn
-           case fl of
-                (ENUM n) => pure $ CPrimVal fc (enumTag n tag)
-                ZERO => pure $ CPrimVal fc (BI 0)
-                SUCC => do x <- newMN "succ"
-                           pure $ CLam fc x $ COp fc (Add IntegerType) [CPrimVal fc (BI 1), CLocal fc First]
-                _ => pure $ CCon fc cn fl (Just tag) []
-  toCExpTm m n (Ref fc (TyCon tag arity) fn)
-      = pure $ CCon fc fn TYCON Nothing []
-  toCExpTm m n (Ref fc _ fn)
-      = do full <- getFullName fn
-               -- ^ For readability of output code, and the Nat hack,
-           pure $ CApp fc (CRef fc full) []
-  toCExpTm m n (Meta fc mn i args)
-      = pure $ CApp fc (CRef fc mn) !(traverse (toCExp m n) args)
-  toCExpTm m n (Bind fc x (Lam _ _ _ _) sc)
-      = pure $ CLam fc x !(toCExp m n sc)
-  toCExpTm m n (Bind fc x (Let _ rig val _) sc)
-      = do sc' <- toCExp m n sc
-           pure $ branchZero (shrinkCExp (DropCons SubRefl) sc')
-                          (CLet fc x True !(toCExp m n val) sc')
-                          rig
-  toCExpTm m n (Bind fc x (Pi _ c e ty) sc)
-      = pure $ CCon fc (UN (Basic "->")) TYCON Nothing
-                       [ !(toCExp m n ty)
-                       , CLam fc x !(toCExp m n sc)]
-  toCExpTm m n (Bind fc x b tm) = pure $ CErased fc
-  -- We'd expect this to have been dealt with in toCExp, but for completeness...
-  toCExpTm m n (App fc tm arg)
-      = pure $ CApp fc !(toCExp m n tm) [!(toCExp m n arg)]
-  -- This shouldn't be in terms any more, but here for completeness
-  toCExpTm m n (As _ _ _ p) = toCExpTm m n p
-  -- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
-  toCExpTm m n (TDelayed fc _ _) = pure $ CErased fc
-  toCExpTm m n (TDelay fc lr _ arg)
-      = pure (CDelay fc lr !(toCExp m n arg))
-  toCExpTm m n (TForce fc lr arg)
-      = pure (CForce fc lr !(toCExp m n arg))
-  toCExpTm m n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant
-  toCExpTm m n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant
-  toCExpTm m n (Erased fc _) = pure $ CErased fc
-  toCExpTm m n (TType fc _) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []
-
-  toCExp : {vars : _} ->
+toCExpTm : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto s : Ref NextMN Int} ->
-           (magic : forall vars. CExp vars -> CExp vars) ->
           Name -> Term vars ->
           Core (CExp vars)
-  toCExp m n tm
-      = case getFnArgs tm of
-             (f, args) =>
-                do args' <- traverse (toCExp m n) args
-                   defs <- get Ctxt
-                   f' <- toCExpTm m n f
-                   Arity a <- numArgs defs f
-                      | NewTypeBy arity pos =>
-                            do let res = applyNewType arity pos f' args'
-                               pure $ m res
-                      | EraseArgs arity epos =>
-                            do let res = eraseConArgs arity epos f' args'
-                               pure $ m res
-                   let res = expandToArity a f' args'
-                   pure $ m res
+toCExp : {vars : _} ->
+         {auto c : Ref Ctxt Defs} ->
+         {auto s : Ref NextMN Int} ->
+         Name -> Term vars ->
+         Core (CExp vars)
+
+toCExpTm n (Local fc _ _ prf)
+    = pure $ CLocal fc prf
+toCExpTm n (Ref fc (DataCon tag arity) fn)
+    = do -- get full name for readability, and %builtin Natural
+         cn <- getFullName fn
+         fl <- dconFlag cn
+         case fl of
+              (ENUM n) => pure $ CPrimVal fc (enumTag n tag)
+              ZERO => pure $ CPrimVal fc (BI 0)
+              SUCC => do x <- newMN "succ"
+                         pure $ CLam fc x $ COp fc (Add IntegerType) [CPrimVal fc (BI 1), CLocal fc First]
+              _ => pure $ CCon fc cn fl (Just tag) []
+toCExpTm n (Ref fc (TyCon tag arity) fn)
+    = pure $ CCon fc fn TYCON Nothing []
+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 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 n (Bind fc x (Pi _ c e ty) sc)
+    = pure $ CCon fc (UN (Basic "->")) TYCON 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 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 n (As _ _ _ p) = toCExpTm n p
+-- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
+toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
+toCExpTm n (TDelay fc lr _ arg)
+    = pure (CDelay fc lr !(toCExp n arg))
+toCExpTm n (TForce fc lr arg)
+    = pure (CForce fc lr !(toCExp n arg))
+toCExpTm n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant
+toCExpTm n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant
+toCExpTm n (Erased fc _) = pure $ CErased fc
+toCExpTm n (TType fc _) = pure $ CCon fc (UN (Basic "Type")) TYCON Nothing []
+
+toCExp n tm
+    = case getFnArgs tm of
+           (f, 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 f' args'
+                             pure $ builtinMagic res
+                    | EraseArgs arity epos =>
+                          do let res = eraseConArgs arity epos f' args'
+                             pure $ builtinMagic res
+                 let res = expandToArity a f' args'
+                 pure $ builtinMagic res

 mutual
  conCases : {vars : _} ->
@ -535,7 +533,7 @@ mutual
      = toCExpTree n sc
  toCExpTree' n (Case _ x scTy [])
      = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n
-  toCExpTree' n (STerm _ tm) = toCExp !builtinMagic n tm
+  toCExpTree' n (STerm _ tm) = toCExp n tm
  toCExpTree' n (Unmatched msg)
      = pure $ CCrash emptyFC msg
  toCExpTree' n Impossible
@ -779,9 +777,8 @@ export
 compileExp : {auto c : Ref Ctxt Defs} ->
             ClosedTerm -> Core (CExp [])
 compileExp tm
-    = do m <- builtinMagic
-         s <- newRef NextMN 0
-         exp <- toCExp m (UN $ Basic "main") tm
+    = do s <- newRef NextMN 0
+         exp <- toCExp (UN $ Basic "main") tm
         pure exp

 ||| Given a name, look up an expression, and compile it to a CExp in the environment
--- a/src/Compiler/Inline.idr
+++ b/src/Compiler/Inline.idr
@ -568,7 +568,7 @@ compileAndInlineAll
         -- in incremental mode, add the arity of the definitions to the hash,
         -- because if these change we need to recompile dependencies
         -- accordingly
-         when (not (isNil (incrementalCGs !getSession))) $
+         unless (isNil (incrementalCGs !getSession)) $
           traverse_ addArityHash cns
  where
    transform : Nat -> List Name -> Core ()
--- a/tests/codegen/.gitignore
+++ b/tests/codegen/.gitignore
@ -0,0 +1 @@
+*.cases
--- a/tests/codegen/builtin001/CatCases.idr
+++ b/tests/codegen/builtin001/CatCases.idr
@ -1,7 +0,0 @@
-import System.File
-
-main : IO ()
-main = do
-    Right str <- readFile "Main.cases"
-        | Left err => putStrLn "Error:" *> printLn err
-    putStrLn str
--- a/tests/codegen/builtin001/expected
+++ b/tests/codegen/builtin001/expected
@ -1,10 +1,3 @@
 Dumping case trees to Main.cases
-prim__add_Integer = [{arg:N}, {arg:N}]: (+Integer [!{arg:N}, !{arg:N}])
-prim__sub_Integer = [{arg:N}, {arg:N}]: (-Integer [!{arg:N}, !{arg:N}])
-prim__mul_Integer = [{arg:N}, {arg:N}]: (*Integer [!{arg:N}, !{arg:N}])
 Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [(Main.plus [!{e:N}, !{arg:N}]), 1])))
 Main.main = [{ext:N}]: (Main.plus [1, 2])
-Prelude.Types.prim__integerToNat = [{arg:N}]: (%case (%case (<=Integer [0, !{arg:N}]) [(%constcase 0 0)] Just 1) [(%constcase 1 (believe_me [___, ___, !{arg:N}])), (%constcase 0 0)] Nothing)
-PrimIO.unsafePerformIO = [{arg:N}]: (%let {eff:N} !{arg:N} (PrimIO.unsafeCreateWorld [(%lam w (%let {eff:N} (!{eff:N} [!w]) !{eff:N}))]))
-PrimIO.unsafeCreateWorld = [{arg:N}]: (!{arg:N} [%MkWorld])
-
--- a/tests/codegen/builtin001/run
+++ b/tests/codegen/builtin001/run
@ -1,6 +1,6 @@
+rm -rf build
+rm Main.cases
+
 $1 --no-color --console-width 0 --no-banner --dumpcases Main.cases -o Main Main.idr

-$1 --no-color --console-width 0 --no-banner --exec main CatCases.idr | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g"
-
-rm -rf build
-rm Main.cases
+cat Main.cases | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g" | grep 'Main.plus\|Main.bah'
--- a/tests/codegen/con001/CatCases.idr
+++ b/tests/codegen/con001/CatCases.idr
@ -1,7 +0,0 @@
-import System.File
-
-main : IO ()
-main = do
-    Right str <- readFile "Main.cases"
-        | Left err => putStrLn "Error:" *> printLn err
-    putStrLn str
--- a/tests/codegen/con001/run
+++ b/tests/codegen/con001/run
@ -1,6 +1,6 @@
+rm -rf build
+rm Main.cases
+
 $1 --no-color --console-width 0 --no-banner --dumpcases Main.cases -o Main Main.idr

 cat Main.cases | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g" | sed '/Constructor/!d'
-
-rm -rf build
-rm Main.cases