{-# LANGUAGE CPP #-}

module Agda.Syntax.Strict where

import Data.Generics (everything)

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

-- | @force@ is the recursive @const 0@ function, to force Haskell to evaluate.
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
        Level l     -> force l
	Pi a b	    -> force (a,b)
	Sort s	    -> force s
	MetaV _ ts  -> force ts
        DontCare mt -> force mt

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
        Inf        -> 0
        DLub s1 s2 -> force (s1, s2)

instance Strict Level where
  force (Max as) = force as

instance Strict PlusLevel where
  force ClosedLevel{} = 0
  force (Plus _ l) = force l

instance Strict LevelAtom where
  force l = case l of
    MetaLevel _ vs   -> force vs
    NeutralLevel v   -> force v
    BlockedLevel _ v -> force v
    UnreducedLevel v -> force v

instance Strict ClauseBody where
    force (Body t)   = force t
    force (Bind 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 (Maybe a) where
    force = maybe 0 force

instance Strict a => Strict (Abs a) where
    force = force . unAbs

instance Strict Token where
  -- TODO: This is just a dummy instance. Why can't we just use the
  -- NFData derivation provided by Drift?
  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