Merge pull request #340 from chrrasmussen/add-nonewtype

Add noNewtype option to data types

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.
 

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

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,6 +332,11 @@ 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
+
+         -- 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

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

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

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'

tests/chez/chez017/expected

@@ -0,0 +1,4 @@
+foo
+#(0 bar)
+1/1: Building Main (Main.idr)
+Main> Main> Bye for now!

tests/chez/chez017/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/chez/chez017/run

@@ -0,0 +1,3 @@
+$1 --no-banner Main.idr < input
+
+rm -rf build