Optimise away case statements on unit-y types (#1844)

src/Compiler/CompileExpr.idr

@@ -213,12 +213,12 @@ natHack =
 builtinMagic : Ref Ctxt Defs => Core (forall vars. CExp vars -> CExp vars)
 builtinMagic = pure $ magic natHack
 
-data NextSucc : Type where
-newSuccName : {auto s : Ref NextSucc Int} -> Core Name
-newSuccName = do
-    x <- get NextSucc
-    put NextSucc $ x + 1
-    pure $ MN "succ" x
+data NextMN : Type where
+newMN : {auto s : Ref NextMN Int} -> String -> Core Name
+newMN base = do
+    x <- get NextMN
+    put NextMN $ x + 1
+    pure $ MN base x
 
 natBranch :  CConAlt vars -> Bool
 natBranch (MkConAlt n ZERO _ _ _) = True
@@ -243,7 +243,7 @@ getZBranch [] = Nothing
 getZBranch (x :: xs) = tryZBranch x <+> getZBranch xs
 
 -- Rewrite case trees on Nat to be case trees on Integer
-builtinNatTree : {auto s : Ref NextSucc Int} -> CExp vars -> Core (CExp vars)
+builtinNatTree : {auto s : Ref NextMN Int} -> CExp vars -> Core (CExp vars)
 builtinNatTree (CConCase fc sc@(CLocal _ _) alts def)
    = pure $ if any natBranch alts
                then let defb = fromMaybe (CCrash fc "Nat case not covered") def
@@ -252,7 +252,7 @@ builtinNatTree (CConCase fc sc@(CLocal _ _) alts def)
                         CConstCase fc sc [MkConstAlt (BI 0) zalt] (Just salt)
                else CConCase fc sc alts def
 builtinNatTree (CConCase fc sc alts def)
-    = do x <- newSuccName
+    = do x <- newMN "succ"
          pure $ CLet fc x True sc
                 !(builtinNatTree $ CConCase fc (CLocal fc First) (map weaken alts) (map weaken def))
 builtinNatTree t = pure t
@@ -270,6 +270,16 @@ enumTree (CConCase fc sc alts def)
     toEnum _ = Nothing
 enumTree t = t
 
+-- remove pattern matches on unit
+unitTree : {auto u : Ref NextMN Int} -> CExp vars -> Core (CExp vars)
+unitTree exp@(CConCase fc sc alts def) = fromMaybe (pure exp)
+    $ do let [MkConAlt _ UNIT _ [] e] = alts
+             | _ => Nothing
+         Just $ case sc of -- TODO: Check scrutinee has no effect, and skip let binding
+                     CLocal _ _ => pure e
+                     _ => pure $ CLet fc !(newMN "_unit") False sc (weaken e)
+unitTree t = pure t
+
 -- See if the constructor is a special constructor type, e.g a nil or cons
 -- shaped thing.
 dconFlag : {auto c : Ref Ctxt Defs} ->
@@ -288,7 +298,7 @@ dconFlag n
 mutual
   toCExpTm : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
-             {auto s : Ref NextSucc Int} ->
+             {auto s : Ref NextMN Int} ->
              (magic : forall vars. CExp vars -> CExp vars) ->
              Name -> Term vars ->
              Core (CExp vars)
@@ -301,7 +311,7 @@ mutual
            case fl of
                 ENUM => pure $ CPrimVal fc (I tag)
                 ZERO => pure $ CPrimVal fc (BI 0)
-                SUCC => do x <- newSuccName
+                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)
@@ -345,7 +355,7 @@ mutual
 
   toCExp : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
-           {auto s : Ref NextSucc Int} ->
+           {auto s : Ref NextMN Int} ->
            (magic : forall vars. CExp vars -> CExp vars) ->
            Name -> Term vars ->
            Core (CExp vars)
@@ -368,7 +378,7 @@ mutual
 mutual
   conCases : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
-             {auto s : Ref NextSucc Int} ->
+             {auto s : Ref NextMN Int} ->
              Name -> List (CaseAlt vars) ->
              Core (List (CConAlt vars))
   conCases n [] = pure []
@@ -397,7 +407,7 @@ mutual
 
   constCases : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
-               {auto s : Ref NextSucc Int} ->
+               {auto s : Ref NextMN Int} ->
                Name -> List (CaseAlt vars) ->
                Core (List (CConstAlt vars))
   constCases n [] = pure []
@@ -415,7 +425,7 @@ mutual
   -- once.
   getNewType : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
-               {auto s : Ref NextSucc Int} ->
+               {auto s : Ref NextMN Int} ->
                FC -> CExp vars ->
                Name -> List (CaseAlt vars) ->
                Core (Maybe (CExp vars))
@@ -467,7 +477,7 @@ mutual
 
   getDef : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
-           {auto s : Ref NextSucc Int} ->
+           {auto s : Ref NextMN Int} ->
            Name -> List (CaseAlt vars) ->
            Core (Maybe (CExp vars))
   getDef n [] = pure Nothing
@@ -479,7 +489,7 @@ mutual
 
   toCExpTree : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
-               {auto s : Ref NextSucc Int} ->
+               {auto s : Ref NextMN Int} ->
                Name -> CaseTree vars ->
                Core (CExp vars)
   toCExpTree n alts@(Case _ x scTy (DelayCase ty arg sc :: rest))
@@ -493,7 +503,7 @@ mutual
 
   toCExpTree' : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
-                {auto s : Ref NextSucc Int} ->
+                {auto s : Ref NextMN Int} ->
                 Name -> CaseTree vars ->
                 Core (CExp vars)
   toCExpTree' n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
@@ -505,7 +515,7 @@ mutual
                def <- getDef n alts
                if isNil cases
                   then pure (fromMaybe (CErased fc) def)
-                  else pure $ enumTree !(builtinNatTree $
+                  else unitTree $ enumTree !(builtinNatTree $
                             CConCase fc (CLocal fc x) cases def)
   toCExpTree' n (Case _ x scTy alts@(DelayCase _ _ _ :: _))
       = throw (InternalError "Unexpected DelayCase")
@@ -701,7 +711,7 @@ toCDef n ty _ None
     = pure $ MkError $ CCrash emptyFC ("Encountered undefined name " ++ show !(getFullName n))
 toCDef n ty erased (PMDef pi args _ tree _)
     = do let (args' ** p) = mkSub 0 args erased
-         s <- newRef NextSucc 0
+         s <- newRef NextMN 0
          comptree <- toCExpTree n tree
          pure $ toLam (externalDecl pi) $ if isNil erased
             then MkFun args comptree
@@ -765,7 +775,7 @@ compileExp : {auto c : Ref Ctxt Defs} ->
              ClosedTerm -> Core (CExp [])
 compileExp tm
     = do m <- builtinMagic
-         s <- newRef NextSucc 0
+         s <- newRef NextMN 0
          exp <- toCExp m (UN $ Basic "main") tm
          pure exp
 

src/Compiler/ES/Codegen.idr

@@ -149,6 +149,7 @@ applyCon NOTHING _ [] = "{h" <+> softColon <+> "0}"
 applyCon CONS    _ as = applyObj (conTags as)
 applyCon JUST    _ as = applyObj (conTags as)
 applyCon RECORD  _ as = applyObj (conTags as)
+applyCon UNIT    _ [] = "undefined"
 applyCon _       t as = applyObj (("h" <+> softColon <+> tag2es t)::conTags as)
 
 -- applys the given list of arguments to the given function.
@@ -647,6 +648,7 @@ mutual
         alt (MkEConAlt _ CONS b)    = ("undefined",) <$> stmt b
         alt (MkEConAlt _ NOTHING b) = ("0",) <$> stmt b
         alt (MkEConAlt _ JUST b)    = ("undefined",) <$> stmt b
+        alt (MkEConAlt _ UNIT b)    = ("undefined",) <$> stmt b
         alt (MkEConAlt t _ b)       = (tag2es t,) <$> stmt b
 
   stmt (ConstSwitch r sc alts def) = do

src/Compiler/RefC/RefC.idr

@@ -645,6 +645,8 @@ mutual
         registerVariableForAutomaticFreeing $ "var_" ++ (show var)
         bodyAssignment <- cStatementsFromANF body
         pure $ bodyAssignment
+    cStatementsFromANF (ACon fc n UNIT tag []) = do
+        pure $ MkRS "(Value*)NULL" "(Value*)NULL"
     cStatementsFromANF (ACon fc n _ tag args) = do
         c <- getNextCounter
         let constr = "constructor_" ++ (show c)

src/Core/Binary.idr

@@ -33,7 +33,7 @@ import public Libraries.Utils.Binary
 ||| (Increment this when changing anything in the data format)
 export
 ttcVersion : Int
-ttcVersion = 65
+ttcVersion = 66
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/CompileExpr.idr

@@ -24,8 +24,9 @@ data ConInfo = DATACON -- normal data constructor
              | NOTHING -- nothing of an option shaped thing
              | JUST -- just of an option shaped thing
              | RECORD -- record constructor (no tag)
-             | ZERO
-             | SUCC
+             | ZERO -- zero of a nat-like type
+             | SUCC -- successor of a nat-like type
+             | UNIT -- unit
 
 export
 Show ConInfo where
@@ -39,6 +40,7 @@ Show ConInfo where
   show RECORD  = "[record]"
   show ZERO    = "[zero]"
   show SUCC    = "[succ]"
+  show UNIT    = "[unit]"
 
 export
 Eq ConInfo where
@@ -52,6 +54,7 @@ Eq ConInfo where
   RECORD == RECORD = True
   ZERO == ZERO = True
   SUCC == SUCC = True
+  UNIT == UNIT = True
   _ == _ = False
 
 mutual

src/Core/Hash.idr

@@ -436,6 +436,7 @@ Hashable ConInfo where
     RECORD => h `hashWithSalt` 7
     ZERO => h `hashWithSalt` 8
     SUCC => h `hashWithSalt` 9
+    UNIT => h `hashWithSalt` 10
 
 mutual
   export

src/Core/TTC.idr

@@ -670,6 +670,7 @@ TTC ConInfo where
   toBuf b RECORD = tag 7
   toBuf b ZERO = tag 8
   toBuf b SUCC = tag 9
+  toBuf b UNIT = tag 10
 
   fromBuf b
       = case !getTag of
@@ -683,6 +684,7 @@ TTC ConInfo where
              7 => pure RECORD
              8 => pure ZERO
              9 => pure SUCC
+             10 => pure UNIT
              _ => corrupt "ConInfo"
 
 mutual

src/TTImp/ProcessData.idr

@@ -357,12 +357,23 @@ calcNaty fc tyCon cs@[_, _]
             else pure False
 calcNaty _ _ _ = pure False
 
+-- has 1 constructor with 0 args (so skip case on it)
+calcUnity : {auto c : Ref Ctxt Defs} ->
+            FC -> Name -> List Constructor -> Core Bool
+calcUnity fc tyCon cs@[_]
+    = do Just mkUnit <- shaped (hasArgs 0) cs
+              | Nothing => pure False
+         setFlag fc mkUnit (ConType UNIT)
+         pure True
+calcUnity _ _ _ = pure False
 
 calcConInfo : {auto c : Ref Ctxt Defs} ->
               FC -> Name -> List Constructor -> Core ()
 calcConInfo fc type cons
    = do False <- calcNaty fc type cons
            | True => pure ()
+        False <- calcUnity fc type cons
+           | True => pure ()
         False <- calcListy fc cons
            | True => pure ()
         False <- calcMaybe fc cons

tests/Main.idr

@@ -272,7 +272,7 @@ nodeTests = MkTestPool "Node backend" [] (Just Node)
     , "casts"
     , "memo"
     , "newints"
-    , "reg001"
+    , "reg001", "reg002"
     , "stringcast"
     , "syntax001"
     , "tailrec001"

tests/node/reg002/Issue1843.idr

@@ -0,0 +1,7 @@
+test : () -> IO ()
+test () = putStrLn "a test"
+test _  = putStrLn "oopsie"
+
+main : IO ()
+main = do test ()
+          putStrLn "foo" >>= test

tests/node/reg002/expected

@@ -0,0 +1,3 @@
+a test
+foo
+a test

tests/node/reg002/run

@@ -0,0 +1,4 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --cg node Issue1843.idr -x main
+

tests/refc/reg001/Issue1843.idr

@@ -0,0 +1,7 @@
+test : () -> IO ()
+test () = putStrLn "a test"
+test _  = putStrLn "oopsie"
+
+main : IO ()
+main = do test ()
+          putStrLn "foo" >>= test

tests/refc/reg001/expected

@@ -0,0 +1,3 @@
+a test
+foo
+a test

tests/refc/reg001/run

@@ -0,0 +1,5 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --cg refc Issue1843.idr -o test
+
+./build/exec/test