From 1d7d07a667196d2c562b6194d7792e51c21634a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9=20Videla?= <andre.videla@gmail.com>
Date: Wed, 18 Oct 2023 12:06:36 +0100
Subject: [PATCH] add test file

---
 src/Idris/Doc/Keywords.idr                   | 25 ++++++++++++++++++--
 src/Parser/Lexer/Source.idr                  |  2 +-
 tests/Main.idr                               |  4 ++++
 tests/idris2/operators/operators001/Test.idr |  6 +++++
 tests/idris2/operators/operators001/expected |  1 +
 tests/idris2/operators/operators001/run      |  3 +++
 6 files changed, 38 insertions(+), 3 deletions(-)
 create mode 100644 tests/idris2/operators/operators001/Test.idr
 create mode 100644 tests/idris2/operators/operators001/expected
 create mode 100755 tests/idris2/operators/operators001/run

diff --git a/src/Idris/Doc/Keywords.idr b/src/Idris/Doc/Keywords.idr
index 65084e008..1544b5ab4 100644
--- a/src/Idris/Doc/Keywords.idr
+++ b/src/Idris/Doc/Keywords.idr
@@ -458,6 +458,27 @@ namespaceblock = vcat $
     You can use `export` or `public export` to control whether a function
     declared in a namespace is available outside of it.
     """]
+autobindDoc : Doc IdrisDocAnn
+autobindDoc = """
+  Autobind
+
+    `autobind` is a modifier for operator precedence and fixity declaration.
+    It tells the parser that this operator behaves like a binding operator,
+    allowing you to give a name to the left-hand-side of the operator and
+    use it on the right-hand-side.
+
+    A typical example of an autobind operator is `(**)` the type constructor
+    for dependent pairs. It is used like this: `(x : Nat ** Vect x String)`
+
+    If you declare a new operator to be autobind you can use it the same
+    way.
+
+    Start by defining `autobind infixr 1 =@`, and then you can use it
+    like so: `(n : Nat =@ f n)`.
+
+    `autobind` only applies to `infixr` operators and cannot be used as
+    operator sections.
+  """
 
 rewriteeq : Doc IdrisDocAnn
 rewriteeq = vcat $
@@ -487,8 +508,7 @@ withabstraction = vcat $
     If we additionally need to remember that the link between the patterns and
     the intermediate computation we can use the `proof` keyword to retain an
     equality proof.
-    """, "",
-    """
+
     In the following example we want to implement a `filter` function that not
     only returns values that satisfy the input predicate but also proofs that
     they do. The `with (p x)` construct introduces a value of type `Bool`
@@ -564,6 +584,7 @@ keywordsDoc =
   :: "else" ::= ifthenelse
   :: "forall" ::= forallquantifier
   :: "rewrite" ::= rewriteeq
+  :: "autobind" ::= autobindDoc
   :: "using" ::= ""
   :: "interface" ::= interfacemechanism
   :: "implementation" ::= interfacemechanism
diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr
index bc4c3d60c..3bfaa700e 100644
--- a/src/Parser/Lexer/Source.idr
+++ b/src/Parser/Lexer/Source.idr
@@ -245,7 +245,7 @@ keywords : List String
 keywords = ["data", "module", "where", "let", "in", "do", "record",
             "auto", "default", "implicit", "failing", "mutual", "namespace",
             "parameters", "with", "proof", "impossible", "case", "of",
-            "if", "then", "else", "forall", "rewrite",
+            "if", "then", "else", "forall", "rewrite", "autobind",
             "using", "interface", "implementation", "open", "import",
             "public", "export", "private"] ++
             fixityKeywords ++
diff --git a/tests/Main.idr b/tests/Main.idr
index 0ee17265e..52016ca93 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -112,6 +112,9 @@ idrisTestsReflection = testsInDir "idris2/reflection" "Quotation and Reflection"
 idrisTestsWith : IO TestPool
 idrisTestsWith = testsInDir "idris2/with" "With abstraction"
 
+idrisTestsOperators : IO TestPool
+idrisTestsOperators = testsInDir "idris2/operators" "Operator and fixities"
+
 idrisTestsIPKG : IO TestPool
 idrisTestsIPKG = testsInDir "idris2/pkg" "Package and .ipkg files"
 
@@ -216,6 +219,7 @@ main = runner $
   , !idrisTestsSchemeEval
   , !idrisTestsReflection
   , !idrisTestsWith
+  , !idrisTestsOperators
   , !idrisTestsDebug
   , !idrisTestsIPKG
   , testPaths "idris2/misc" idrisTests
diff --git a/tests/idris2/operators/operators001/Test.idr b/tests/idris2/operators/operators001/Test.idr
new file mode 100644
index 000000000..c113aa3d8
--- /dev/null
+++ b/tests/idris2/operators/operators001/Test.idr
@@ -0,0 +1,6 @@
+
+autobind infixr 0 =@
+
+(=@) : (a : Type) -> (a -> Type) -> Type
+(=@) a f = (1 x : a) -> f x
+
diff --git a/tests/idris2/operators/operators001/expected b/tests/idris2/operators/operators001/expected
new file mode 100644
index 000000000..31e5db7f3
--- /dev/null
+++ b/tests/idris2/operators/operators001/expected
@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)
diff --git a/tests/idris2/operators/operators001/run b/tests/idris2/operators/operators001/run
new file mode 100755
index 000000000..d35387bb3
--- /dev/null
+++ b/tests/idris2/operators/operators001/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr