From a5c2c211a1647739fe61592262536325cf9d7571 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Fri, 22 May 2020 16:01:47 +0100
Subject: [PATCH] Add %tcinline flag to high level syntax

This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.
---
 CHANGELOG.md              | 4 ++++
 src/Idris/Parser.idr      | 3 +++
 src/TTImp/ProcessType.idr | 2 ++
 src/TTImp/TTImp.idr       | 5 +++++
 4 files changed, 14 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a0ace263f..696665016 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -11,6 +11,10 @@ Language changes:
 * Fields of records can be accessed (and updated) using the dot syntax,
   such as `r.field1.field2` or `record { field1.field2 = 42 }`.
   For details, see https://idris2.readthedocs.io/en/latest/reference/records.html
+* New function flag `%tcinline` which means that the function should be
+  inlined for the purposes of totality checking (but otherwise not inlined).
+  This can be used as a hint for totality checking, to make the checker look
+  inside functions that it otherwise might not.
 * %transform directive, for declaring transformation rules on runtime
   expressions. Transformation rules are automatically added for top level
   implementations of interfaces.
diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr
index 2db3deea1..a3e52de50 100644
--- a/src/Idris/Parser.idr
+++ b/src/Idris/Parser.idr
@@ -1174,6 +1174,9 @@ fnDirectOpt fname
   <|> do pragma "inline"
          commit
          pure $ IFnOpt Inline
+  <|> do pragma "tcinline"
+         commit
+         pure $ IFnOpt TCInline
   <|> do pragma "extern"
          pure $ IFnOpt ExternFn
   <|> do pragma "macro"
diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr
index 27becefe8..87d659e5d 100644
--- a/src/TTImp/ProcessType.idr
+++ b/src/TTImp/ProcessType.idr
@@ -33,6 +33,8 @@ processFnOpt : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> FnOpt -> Core ()
 processFnOpt fc ndef Inline
     = setFlag fc ndef Inline
+processFnOpt fc ndef TCInline
+    = setFlag fc ndef TCInline
 processFnOpt fc ndef (Hint d)
     = do defs <- get Ctxt
          Just ty <- lookupTyExact ndef (gamma defs)
diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr
index 681416a2f..8de68096d 100644
--- a/src/TTImp/TTImp.idr
+++ b/src/TTImp/TTImp.idr
@@ -179,6 +179,7 @@ mutual
   public export
   data FnOpt : Type where
        Inline : FnOpt
+       TCInline : FnOpt
        -- Flag means the hint is a direct hint, not a function which might
        -- find the result (e.g. chasing parent interface dictionaries)
        Hint : Bool -> FnOpt
@@ -196,6 +197,7 @@ mutual
   export
   Show FnOpt where
     show Inline = "%inline"
+    show TCInline = "%tcinline"
     show (Hint t) = "%hint " ++ show t
     show (GlobalHint t) = "%globalhint " ++ show t
     show ExternFn = "%extern"
@@ -210,6 +212,7 @@ mutual
   export
   Eq FnOpt where
     Inline == Inline = True
+    TCInline == TCInline = True
     (Hint x) == (Hint y) = x == y
     (GlobalHint x) == (GlobalHint y) = x == y
     ExternFn == ExternFn = True
@@ -895,6 +898,7 @@ mutual
   export
   TTC FnOpt where
     toBuf b Inline = tag 0
+    toBuf b TCInline = tag 11
     toBuf b (Hint t) = do tag 1; toBuf b t
     toBuf b (GlobalHint t) = do tag 2; toBuf b t
     toBuf b ExternFn = tag 3
@@ -919,6 +923,7 @@ mutual
                8 => pure (Totality PartialOK)
                9 => pure Macro
                10 => do ns <- fromBuf b; pure (SpecArgs ns)
+               11 => pure TCInline
                _ => corrupt "FnOpt"
 
   export