From f83f88f4762629cdf6d97b9058a340d25f256e4e Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Wed, 19 Apr 2023 15:18:43 +0300
Subject: [PATCH] [ total ] Make getters TCInline, add a test for getters
 producing smaller

---
 src/TTImp/ProcessRecord.idr        |  2 +-
 tests/Main.idr                     |  2 +-
 tests/yaffle/record003/Record.yaff | 22 ++++++++++++++++++++++
 tests/yaffle/record003/expected    |  7 +++++++
 tests/yaffle/record003/input       |  5 +++++
 tests/yaffle/record003/run         |  3 +++
 6 files changed, 39 insertions(+), 2 deletions(-)
 create mode 100644 tests/yaffle/record003/Record.yaff
 create mode 100644 tests/yaffle/record003/expected
 create mode 100644 tests/yaffle/record003/input
 create mode 100755 tests/yaffle/record003/run

diff --git a/src/TTImp/ProcessRecord.idr b/src/TTImp/ProcessRecord.idr
index 3cea7e92..ed5c7894 100644
--- a/src/TTImp/ProcessRecord.idr
+++ b/src/TTImp/ProcessRecord.idr
@@ -264,7 +264,7 @@ elabRecord {vars} eopts fc env nest newns vis mbtot tn_in params0 opts conName_i
 
                    let mkProjClaim = \ nm =>
                           let ty = MkImpTy EmptyFC EmptyFC nm projTy
-                          in IClaim bfc rig isVis [Inline] ty
+                          in IClaim bfc rig isVis [Inline, TCInline] ty
 
                    log "declare.record.projection" 5 $
                       "Projection " ++ show rfNameNS ++ " : " ++ show projTy
diff --git a/tests/Main.idr b/tests/Main.idr
index 746325c6..5ed886d6 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -27,7 +27,7 @@ yaffleTests = MkTestPool "Yaffle" [] Nothing
       "compile001", "compile002",
       "coverage001",
       "qtt001", "qtt002", "qtt003", "qtt004",
-      "record001", "record002",
+      "record001", "record002", "record003",
       "rewrite001",
       "with001",
       -- Below are things that don't test anything specific, but are useful exercises
diff --git a/tests/yaffle/record003/Record.yaff b/tests/yaffle/record003/Record.yaff
new file mode 100644
index 00000000..ec2e25e7
--- /dev/null
+++ b/tests/yaffle/record003/Record.yaff
@@ -0,0 +1,22 @@
+data Unit : Type where
+  MkUnit : Unit
+
+record Id a where
+  constructor MkId
+  field : a
+
+data X : Type where
+  Stop : Unit -> X
+  Cont : Id X -> X
+
+f : X -> Unit
+f (Stop n) = n
+f (Cont x) = f (field x)
+
+field' : Id a -> a
+field' x = case x of
+  MkId y => y
+
+f' : X -> Unit
+f' (Stop n) = n
+f' (Cont x) = f' (field' x)
diff --git a/tests/yaffle/record003/expected b/tests/yaffle/record003/expected
new file mode 100644
index 00000000..c0fcfb69
--- /dev/null
+++ b/tests/yaffle/record003/expected
@@ -0,0 +1,7 @@
+Processing as TTImp
+Written TTC
+Yaffle> Main.MkUnit
+Yaffle> Main.f is total
+Yaffle> Main.MkUnit
+Yaffle> Main.f' is total
+Yaffle> Bye for now!
diff --git a/tests/yaffle/record003/input b/tests/yaffle/record003/input
new file mode 100644
index 00000000..abd0974a
--- /dev/null
+++ b/tests/yaffle/record003/input
@@ -0,0 +1,5 @@
+f (Stop MkUnit)
+:total f
+f' (Stop MkUnit)
+:total f'
+:q
diff --git a/tests/yaffle/record003/run b/tests/yaffle/record003/run
new file mode 100755
index 00000000..be0e1a04
--- /dev/null
+++ b/tests/yaffle/record003/run
@@ -0,0 +1,3 @@
+rm -rf build
+$1 --yaffle Record.yaff < input
+