[ total ] Make getters TCInline & add a test for getters producing a smaller value

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

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

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)

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!

tests/yaffle/record003/input

@@ -0,0 +1,5 @@
+f (Stop MkUnit)
+:total f
+f' (Stop MkUnit)
+:total f'
+:q

tests/yaffle/record003/run

@@ -0,0 +1,3 @@
+rm -rf build
+$1 --yaffle Record.yaff < input
+