[ treeless ] look at STATIC pragmas

src/full/Agda/Compiler/ToTreeless.hs

@@ -30,6 +30,7 @@ import Agda.Compiler.Treeless.Pretty
 
 import Agda.Syntax.Common
 import Agda.TypeChecking.Monad as TCM
+import Agda.TypeChecking.Reduce
 
 import Agda.Utils.Functor
 import qualified Agda.Utils.HashMap as HMap
@@ -47,7 +48,7 @@ prettyPure = return . P.pretty
 -- | Converts compiled clauses to treeless syntax.
 ccToTreeless :: QName -> CC.CompiledClauses -> TCM C.TTerm
 ccToTreeless q cc = do
-  reportSDoc "treeless.opt" 30 $ text "compiling" <+> prettyTCM q
+  reportSDoc "treeless.opt" 20 $ text "compiling" <+> prettyTCM q
   reportSDoc "treeless.convert" 30 $ text "-- compiled clauses:" $$ nest 2 (prettyPure cc)
   body <- casetree cc `runReaderT` initCCEnv
   reportSDoc "treeless.opt.converted" 30 $ text "-- converted body:" $$ nest 2 (prettyPure body)
@@ -102,6 +103,7 @@ casetree cc = do
   case cc of
     CC.Fail -> return C.tUnreachable
     CC.Done xs v -> lambdasUpTo (length xs) $ do
+        v <- lift $ putAllowedReductions [ProjectionReductions, StaticReductions] $ normalise v
         substTerm v
     CC.Case n (CC.Branches True conBrs _ _) -> lambdasUpTo n $ do
       mkRecord =<< traverse casetree (CC.content <$> conBrs)

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

@@ -1562,14 +1562,16 @@ instance ToAbstract C.Pragma [A.Pragma] where
     toAbstract (C.NoSmashingPragma _ x) = do
         e <- toAbstract $ OldQName x Nothing
         y <- case e of
-            A.Def x -> return x
-            _       -> __IMPOSSIBLE__
+            A.Def  x -> return x
+            A.Proj x -> return x
+            _        -> genericError "Target of NO_SMASHING pragma should be a function"
         return [ A.NoSmashingPragma y ]
     toAbstract (C.StaticPragma _ x) = do
         e <- toAbstract $ OldQName x Nothing
         y <- case e of
-            A.Def x -> return x
-            _       -> __IMPOSSIBLE__
+            A.Def  x -> return x
+            A.Proj x -> return x
+            _        -> genericError "Target of STATIC pragma should be a function"
         return [ A.StaticPragma y ]
     toAbstract (C.BuiltinPragma _ b e) | isUntypedBuiltin b = do
       bindUntypedBuiltin b =<< toAbstract e

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -1380,6 +1380,7 @@ reduced b = case fmap ignoreSharing <$> b of
 -- | Controlling 'reduce'.
 data AllowedReduction
   = ProjectionReductions     -- ^ (Projection and) projection-like functions may be reduced.
+  | StaticReductions         -- ^ Functions marked STATIC may be reduced.
   | FunctionReductions       -- ^ Functions which are not projections may be reduced.
   | LevelReductions          -- ^ Reduce @'Level'@ terms.
   | NonTerminatingReductions -- ^ Functions that have not passed termination checking.

src/full/Agda/TypeChecking/Monad/Signature.hs

@@ -776,6 +776,11 @@ isProjection_ def =
     Function { funProjection = result } -> result
     _                                   -> Nothing
 
+-- | Is it a function marked STATIC?
+isStaticFun :: Defn -> Bool
+isStaticFun Function{ funStatic = b } = b
+isStaticFun _ = False
+
 -- | Returns @True@ if we are dealing with a proper projection,
 --   i.e., not a projection-like function nor a record field value
 --   (projection applied to argument).

src/full/Agda/TypeChecking/Reduce.hs

@@ -403,7 +403,8 @@ unfoldDefinition' unfoldDelayed keepGoing v0 f es =
                       cls (defCompiled info)
     _  -> do
       if FunctionReductions `elem` allowed ||
-         (isJust (isProjection_ def) && ProjectionReductions `elem` allowed)  -- includes projection-like
+         (isJust (isProjection_ def) && ProjectionReductions `elem` allowed) || -- includes projection-like
+         (isStaticFun def && StaticReductions `elem` allowed)
         then
           reduceNormalE keepGoing v0 f (map notReduced es)
                        dontUnfold