From 9c59542081d9e61653cdd15c8e6f0165d5c6ee0c Mon Sep 17 00:00:00 2001
From: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
Date: Fri, 28 Aug 2020 11:06:10 +0100
Subject: [PATCH] [ new ] allow `auto` fields in records

---
 src/Idris/Parser.idr            | 3 ++-
 tests/Main.idr                  | 1 +
 tests/idris2/record007/Fld.idr  | 6 ++++++
 tests/idris2/record007/expected | 3 +++
 tests/idris2/record007/input    | 3 +++
 tests/idris2/record007/run      | 3 +++
 6 files changed, 18 insertions(+), 1 deletion(-)
 create mode 100644 tests/idris2/record007/Fld.idr
 create mode 100644 tests/idris2/record007/expected
 create mode 100644 tests/idris2/record007/input
 create mode 100755 tests/idris2/record007/run

diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 7a3ac1270..86aa81a9b 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1251,7 +1251,8 @@ fieldDecl fname indents
       = do doc <- option "" documentation
            symbol "{"
            commit
-           fs <- fieldBody doc Implicit
+           impl <- option Implicit (AutoImplicit <$ keyword "auto")
+           fs <- fieldBody doc impl
            symbol "}"
            atEnd indents
            pure fs
diff --git a/tests/Main.idr b/tests/Main.idr
index 358a02d20..30b5d1d85 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -95,6 +95,7 @@ idrisTests
        "real001", "real002",
        -- Records, access and dependent update
        "record001", "record002", "record003", "record004", "record005",
+       "record007",
        -- Quotation and reflection
        "reflection001", "reflection002", "reflection003", "reflection004",
        "reflection005", "reflection006", "reflection007", "reflection008",
diff --git a/tests/idris2/record007/Fld.idr b/tests/idris2/record007/Fld.idr
new file mode 100644
index 000000000..dac17e38d
--- /dev/null
+++ b/tests/idris2/record007/Fld.idr
@@ -0,0 +1,6 @@
+record Is3 (n : Nat) where
+  constructor MkThree
+  {auto prf : n === 3}
+
+three : Is3 3
+three = MkThree
diff --git a/tests/idris2/record007/expected b/tests/idris2/record007/expected
new file mode 100644
index 000000000..a78d16249
--- /dev/null
+++ b/tests/idris2/record007/expected
@@ -0,0 +1,3 @@
+1/1: Building Fld (Fld.idr)
+Main> Main> MkThree {n = 3} {prf = Refl {a = Nat} {x = 3}}
+Main> Bye for now!
diff --git a/tests/idris2/record007/input b/tests/idris2/record007/input
new file mode 100644
index 000000000..bfb093213
--- /dev/null
+++ b/tests/idris2/record007/input
@@ -0,0 +1,3 @@
+:set showimplicits
+three
+:q
diff --git a/tests/idris2/record007/run b/tests/idris2/record007/run
new file mode 100755
index 000000000..075d41092
--- /dev/null
+++ b/tests/idris2/record007/run
@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 --no-banner Fld.idr < input
+
+rm -rf build