From 84e431f495f8418a915e84125daca47710ddfffb Mon Sep 17 00:00:00 2001 From: Christian Rasmussen Date: Tue, 28 Apr 2020 22:50:49 +0200 Subject: [PATCH 1/2] Add noNewtype option to data types --- CHANGELOG.md | 4 ++++ src/Idris/Parser.idr | 2 ++ src/TTImp/ProcessData.idr | 9 ++++++++- src/TTImp/TTImp.idr | 4 ++++ 4 files changed, 18 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9ef5742..af87087 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,10 @@ Compiler updates: * Data types with a single constructor, with a single unerased arguments, are translated to just that argument, to save repeated packing and unpacking. (c.f. `newtype` in Haskell) + + A data type can opt out of this behaviour by specifying `noNewtype` in its + options list. `noNewtype` allows code generators to apply special handling + to the generated constructor/deconstructor, for a newtype-like data type, + that would otherwise be optimised away. * 0-multiplicity constructor arguments are now properly erased, not just given a placeholder null value. diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 3a28abc..0117d74 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -924,6 +924,8 @@ dataOpt pure (SearchBy ns) <|> do exactIdent "external" pure External + <|> do exactIdent "noNewtype" + pure NoNewtype dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm -> EmptyRule PDataDecl diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index df24efe..2b6cf44 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -29,6 +29,8 @@ processDataOpt fc ndef UniqueSearch = setUniqueSearch fc ndef True processDataOpt fc ndef External = setExternal fc ndef True +processDataOpt fc ndef NoNewtype + = pure () checkRetType : {auto c : Ref Ctxt Defs} -> Env Term vars -> NF vars -> @@ -330,7 +332,12 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra let ddef = MkData (MkCon dfc n arity fullty) cons addData vars vis tidx ddef - findNewtype cons + + -- Flag data type as a newtype, if possible (See `findNewtype` for criteria). + -- Skip optimisation if the data type has specified `noNewtype` in its + -- options list. + when (not (NoNewtype `elem` opts)) $ + findNewtype cons -- Type is defined mutually with every data type undefined at the -- point it was declared, and every data type undefined right now diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index d3f4aea..0b1bd8e 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -232,6 +232,7 @@ mutual NoHints : DataOpt -- Don't generate search hints for constructors UniqueSearch : DataOpt -- auto implicit search must check result is unique External : DataOpt -- implemented externally + NoNewtype : DataOpt -- don't apply newtype optimisation export Eq DataOpt where @@ -239,6 +240,7 @@ mutual (==) NoHints NoHints = True (==) UniqueSearch UniqueSearch = True (==) External External = True + (==) NoNewtype NoNewtype = True (==) _ _ = False public export @@ -837,6 +839,7 @@ mutual toBuf b NoHints = tag 1 toBuf b UniqueSearch = tag 2 toBuf b External = tag 3 + toBuf b NoNewtype = tag 4 fromBuf b = case !getTag of @@ -845,6 +848,7 @@ mutual 1 => pure NoHints 2 => pure UniqueSearch 3 => pure External + 4 => pure NoNewtype _ => corrupt "DataOpt" export From 69aff544b63cbb5e515ecceb50f2b9713bd631ee Mon Sep 17 00:00:00 2001 From: Christian Rasmussen Date: Wed, 29 Apr 2020 01:15:48 +0200 Subject: [PATCH 2/2] Add test of noNewtype --- tests/Main.idr | 2 +- tests/chez/chez017/Main.idr | 19 +++++++++++++++++++ tests/chez/chez017/expected | 4 ++++ tests/chez/chez017/input | 2 ++ tests/chez/chez017/run | 3 +++ 5 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 tests/chez/chez017/Main.idr create mode 100644 tests/chez/chez017/expected create mode 100644 tests/chez/chez017/input create mode 100755 tests/chez/chez017/run diff --git a/tests/Main.idr b/tests/Main.idr index d0a43d0..45a96a4 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -98,7 +98,7 @@ chezTests : List String chezTests = ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006", "chez007", "chez008", "chez009", "chez010", "chez011", "chez012", - "chez013", "chez014", "chez015", "chez016", + "chez013", "chez014", "chez015", "chez016", "chez017", "reg001"] ideModeTests : List String diff --git a/tests/chez/chez017/Main.idr b/tests/chez/chez017/Main.idr new file mode 100644 index 0000000..6ee5aac --- /dev/null +++ b/tests/chez/chez017/Main.idr @@ -0,0 +1,19 @@ +module Main + +data Foo : Type where + MkFoo : String -> Foo + +data Bar : Type where + [noNewtype] + MkBar : String -> Bar + + +-- This code rely on the fact that `putStr` calls the Chez function `display`, +-- which allows any value to be printed. This will expose the internal +-- structure of each data type. +main : IO () +main = do + putStr (believe_me (MkFoo "foo")) + putChar '\n' + putStr (believe_me (MkBar "bar")) + putChar '\n' diff --git a/tests/chez/chez017/expected b/tests/chez/chez017/expected new file mode 100644 index 0000000..66fb782 --- /dev/null +++ b/tests/chez/chez017/expected @@ -0,0 +1,4 @@ +foo +#(0 bar) +1/1: Building Main (Main.idr) +Main> Main> Bye for now! diff --git a/tests/chez/chez017/input b/tests/chez/chez017/input new file mode 100644 index 0000000..fc5992c --- /dev/null +++ b/tests/chez/chez017/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/chez/chez017/run b/tests/chez/chez017/run new file mode 100755 index 0000000..fe350f8 --- /dev/null +++ b/tests/chez/chez017/run @@ -0,0 +1,3 @@ +$1 --no-banner Main.idr < input + +rm -rf build