module Agda.Syntax.Strict where
import Data.Generics
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Parser.Tokens
import qualified Agda.Syntax.Concrete as C
import qualified Agda.Syntax.Concrete.Definitions as C
#include "../undefined.h"
import Agda.Utils.Impossible
class Strict a where
force :: a -> Int
instance Strict Term where
force t = case t of
Var _ ts -> force ts
Def _ ts -> force ts
Con _ ts -> force ts
Lam _ t -> force t
Lit _ -> 0
Pi a b -> force (a,b)
Fun a b -> force (a,b)
Sort s -> force s
MetaV _ ts -> force ts
instance Strict Type where
force (El s t) = force (s,t)
instance Strict Sort where
force s = case s of
Type n -> force n
Prop -> 0
Lub s1 s2 -> force (s1,s2)
Suc s -> force s
MetaS _ as -> force as
Inf -> 0
DLub s1 s2 -> force (s1, s2)
instance Strict ClauseBody where
force (Body t) = force t
force (Bind b) = force b
force (NoBind b) = force b
force NoBody = 0
instance Strict C.Expr where
force e = everything (+) (const 1) e
instance Strict C.Declaration where
force e = everything (+) (const 1) e
instance Strict C.Pragma where
force e = everything (+) (const 1) e
instance Strict C.NiceDeclaration where
force d = everything (+) (const 1) d
instance (Strict a, Strict b) => Strict (a,b) where
force (x,y) = force x + force y
instance Strict a => Strict (Arg a) where
force = force . unArg
instance Strict a => Strict [a] where
force = sum . map force
instance Strict a => Strict (Abs a) where
force = force . absBody
instance Strict Token where
force = (`seq` 0)
infixr 0 $!!
($!!) :: Strict a => (a -> b) -> a -> b
f $!! x = force x `seq` f x
strict :: Strict a => a -> a
strict x = id $!! x