[ #2492 ] Folding ℕs during Abstract to Concrete

We turn `suc^n zero` into `Lit n` when converting from Abstract
to Concrete. The most obvious benefit is that Auto doesn't spit
out massive terms when it has built a big natural number (however
it still takes a long time: internally Auto does generate the big
chain of `suc`s and we need to go through it.

There is another opportunity to call `tryToRecoverNatural` in
`toConcrete` in the `Con` case:

    toConcrete (Con (AmbQ (x:_))) = Ident <$> toConcrete x

However that turns the warning about `{-# BUILTIN ZERO zero #-}`
into a weird warning about `{-# BUILTIN ZERO 0 #-}` so I figured
it was not worth the trouble.

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

@@ -27,6 +27,7 @@ import Prelude hiding (null)
 
 import Control.Applicative hiding (empty)
 import Control.Monad.Reader
+import Control.Monad.State
 
 import qualified Data.Map as Map
 import Data.Maybe
@@ -41,14 +42,15 @@ import Agda.Syntax.Position
 import Agda.Syntax.Literal
 import Agda.Syntax.Info
 import Agda.Syntax.Internal (MetaId(..))
+import qualified Agda.Syntax.Internal as I
 import Agda.Syntax.Fixity
 import Agda.Syntax.Concrete as C
 import Agda.Syntax.Abstract as A
 import Agda.Syntax.Abstract.Views as AV
 import Agda.Syntax.Scope.Base
 
 import Agda.TypeChecking.Monad.State (getScope)
-import Agda.TypeChecking.Monad.Base  (TCM, NamedMeta(..))
+import Agda.TypeChecking.Monad.Base  (TCM, NamedMeta(..), stBuiltinThings, BuiltinThings, Builtin(..))
 import Agda.TypeChecking.Monad.Options
 
 import qualified Agda.Utils.AssocList as AssocList
@@ -392,6 +394,7 @@ instance ToConcrete A.Expr C.Expr where
 
     toConcrete e@(A.App i e1 e2)    =
         tryToRecoverOpApp e
+        $ tryToRecoverNatural e
         -- or fallback to App
         $ bracket appBrackets
         $ do e1' <- toConcreteCtx FunctionCtx e1
@@ -970,6 +973,29 @@ cOpApp r x n es =
   C.OpApp r x (Set.singleton n)
           (map (defaultNamedArg . noPlaceholder . Ordinary) es)
 
+tryToRecoverNatural :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
+tryToRecoverNatural e def = do
+  builtins <- stBuiltinThings <$> lift get
+  let reified = do
+        zero <- getAQName "ZERO" builtins
+        suc  <- getAQName "SUC"  builtins
+        explore zero suc 0 e
+  case reified of
+    Just n  -> return $ C.Lit $ LitNat noRange n
+    Nothing -> def
+  where
+
+    getAQName :: String -> BuiltinThings a -> Maybe A.QName
+    getAQName str bs = do
+      Builtin (I.Con hd _ _) <- Map.lookup str bs
+      return $ I.conName hd
+
+    explore :: A.QName -> A.QName -> Integer -> A.Expr -> Maybe Integer
+    explore z s k (A.App _ (A.Con (AmbQ [f])) t) | f == s = explore z s (1+k) $ namedArg t
+    explore z s k (A.Con (AmbQ [x]))             | x == z = Just k
+    explore z s k (A.Lit (LitNat _ l))                    = Just (k + l)
+    explore _ _ _ _ = Nothing
+
 tryToRecoverOpApp :: A.Expr -> AbsToCon C.Expr -> AbsToCon C.Expr
 tryToRecoverOpApp e def = caseMaybeM (recoverOpApp bracket cOpApp view e) def return
   where

test/Fail/NonTerminatingReduce.err

@@ -1,3 +1,3 @@
 NonTerminatingReduce.agda:16,9-13
-loop n != suc 41 of type Nat
+loop n != 42 of type Nat
 when checking that the expression refl has type loop n ≡ 42

test/interaction/Issue2492.agda

@@ -0,0 +1,10 @@
+module Issue2492 where
+
+open import Agda.Builtin.Nat
+
+infix 0 _!
+data Singleton {A : Set} : A → Set where
+  _! : (a : A) → Singleton a
+
+_ : Singleton 10
+_ = {!!}

test/interaction/Issue2492.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_auto ""

test/interaction/Issue2492.out

@@ -0,0 +1,15 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Type-checking*" "Checking Issue2492 (Issue2492.agda). " t)
+(agda2-info-action "*Type-checking*" " Checking Agda.Builtin.Nat (agda-default-include-path/Agda/Builtin/Nat.agda). " t)
+(agda2-info-action "*Type-checking*" " Checking Agda.Builtin.Bool (agda-default-include-path/Agda/Builtin/Bool.agda). " t)
+(agda2-info-action "*Type-checking*" " Finished Agda.Builtin.Bool. " t)
+(agda2-info-action "*Type-checking*" " Finished Agda.Builtin.Nat. " t)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : Singleton 10 " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-give-action 0 "10 !")
+(agda2-status-action "")
+(agda2-info-action "*All Done*" "" nil)
+((last . 1) . (agda2-goals-action '()))