diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 0e4ce3269..85fecdda4 100644 --- a/src/Compiler/CompileExpr.idr +++ b/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 diff --git a/src/Compiler/ES/Codegen.idr b/src/Compiler/ES/Codegen.idr index e40137cb0..68cf003ab 100644 --- a/src/Compiler/ES/Codegen.idr +++ b/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 diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index 02174db04..36cf81d86 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/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) diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 524f7227c..e9c7994f6 100644 --- a/src/Core/Binary.idr +++ b/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 () diff --git a/src/Core/CompileExpr.idr b/src/Core/CompileExpr.idr index b542dde5e..c760cede5 100644 --- a/src/Core/CompileExpr.idr +++ b/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 diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr index e025f0281..0a0ac678c 100644 --- a/src/Core/Hash.idr +++ b/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 diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 2ed8250de..bc69c7bf4 100644 --- a/src/Core/TTC.idr +++ b/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 diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index 8a0b0f3ec..8ae3ec8e7 100644 --- a/src/TTImp/ProcessData.idr +++ b/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 diff --git a/tests/Main.idr b/tests/Main.idr index 843884a67..2b867ba56 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -272,7 +272,7 @@ nodeTests = MkTestPool "Node backend" [] (Just Node) , "casts" , "memo" , "newints" - , "reg001" + , "reg001", "reg002" , "stringcast" , "syntax001" , "tailrec001" diff --git a/tests/node/reg002/Issue1843.idr b/tests/node/reg002/Issue1843.idr new file mode 100644 index 000000000..fe4904f9c --- /dev/null +++ b/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 diff --git a/tests/node/reg002/expected b/tests/node/reg002/expected new file mode 100644 index 000000000..cf0bb1ac1 --- /dev/null +++ b/tests/node/reg002/expected @@ -0,0 +1,3 @@ +a test +foo +a test diff --git a/tests/node/reg002/run b/tests/node/reg002/run new file mode 100755 index 000000000..707ec9a7d --- /dev/null +++ b/tests/node/reg002/run @@ -0,0 +1,4 @@ +rm -rf build + +$1 --no-color --console-width 0 --cg node Issue1843.idr -x main + diff --git a/tests/refc/reg001/Issue1843.idr b/tests/refc/reg001/Issue1843.idr new file mode 100644 index 000000000..fe4904f9c --- /dev/null +++ b/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 diff --git a/tests/refc/reg001/expected b/tests/refc/reg001/expected new file mode 100644 index 000000000..cf0bb1ac1 --- /dev/null +++ b/tests/refc/reg001/expected @@ -0,0 +1,3 @@ +a test +foo +a test diff --git a/tests/refc/reg001/run b/tests/refc/reg001/run new file mode 100755 index 000000000..910978f2f --- /dev/null +++ b/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