Enable --no-projection-like by default (and recommend users to do the same)

Author: jespercockx

docs/source/introduction.md

@@ -71,3 +71,13 @@ You can use agda2hs with the [Haskell
 Stack](https://docs.haskellstack.org/en/stable/) tool.
 
 TODO: integrate agda2hs as a preprocessor for stack
+
+### Creating an Agda2Hs project
+
+All agda2hs projects should have a dependency on the `base` library provided by
+Agda, and can also optionally depend on the `containers` library. Using Agda's
+standard library with agda2hs is not supported.
+
+All agda2hs projects should enable the `--erasure` option of Agda. It is also
+recommended to  enable the `--no-projection-like` flag since otherwise functions
+might get inlined inadvertently.

docs/source/tutorials.md

@@ -23,14 +23,14 @@ This is how the `example-basics.agda-lib` file looks for our project:
 ```
 name: example-basics
 include: .
-depend: agda2hs
-flags: --erasure
+depend: base
+flags: --erasure --no-projection-like
 ```
 The `include` label specifies the current folder as the path for files to be included in the library. For our toy example it works perfectly, but for a bigger library it might be handy to place all the `.agda` files in a single repository such as `src`.
 
 The only dependency we need so far is `agda2hs`, as that is where `Haskell.Prelude` and agda2hs pragmas live. 
 
-Finally, to be able to  import modules we need in this example, erasure needs to be enabled. We add it as a flag.
+Finally, to be able to  import modules we need in this example, erasure needs to be enabled. We add it as a flag. We also enable the `--no-projection-like` flag since otherwise functions might get inlined inadvertently.
 
 Let's look at the `HelloWorld.agda` file now:
 

lib/base/base.agda-lib

@@ -5,4 +5,4 @@
 name: base
 depend:
 include: .
-flags: -W noUnsupportedIndexedMatch --erasure
+flags: -W noUnsupportedIndexedMatch --erasure --no-projection-like

lib/containers/containers.agda-lib

@@ -2,4 +2,4 @@ name: containers
 include: agda
 depend:
   base
-flags: --erasure --no-import-sorts
+flags: --erasure --no-import-sorts --no-projection-like

test/ProjLike.agda

@@ -1,3 +1,5 @@
+{-# OPTIONS --projection-like #-}
+
 module ProjLike where
 
 open import Haskell.Prelude

test/agda2hs-test.agda-lib

@@ -1,4 +1,4 @@
 name: agda2hs-test
 depend:
 include: . ../lib/base/
-flags: --sized-types --erasure
+flags: --sized-types --erasure --no-projection-like

test/golden/Issue302.hs

@@ -1,5 +1,5 @@
 module Issue302 where
 
 not0 :: Int -> Bool
-not0 n = not (n == 0)
+not0 n = n /= 0
 

test/golden/Superclass.hs

@@ -28,5 +28,5 @@ baz :: DiscreteOrd a => a -> Bool
 baz x = x < x
 
 usebaz :: Bool
-usebaz = True < True
+usebaz = baz True
 

test/golden/Test.hs

@@ -114,7 +114,7 @@ double :: Monoid a => a -> a
 double x = x <> x
 
 doubleSum :: NatSum -> NatSum
-doubleSum = \ x -> x <> x
+doubleSum = double
 
 hd :: [a] -> a
 hd [] = error "hd: empty list"

tutorials/example-basics/example-basics.agda-lib

@@ -1,4 +1,4 @@
 name: example-basics
 include: . 
 depend: agda2hs
-flags: --erasure
+flags: --erasure --no-projection-like