module Agda.Syntax.Treeless
( module Agda.Syntax.Abstract.Name
, module Agda.Syntax.Treeless
) where
import Prelude
import Data.Map (Map)
import Data.Typeable (Typeable)
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
data Compiled = Compiled
{ cTreeless :: TTerm
, cArgUsage :: [Bool] }
deriving (Typeable, Show, Eq, Ord)
type Args = [TTerm]
data TTerm = TVar Int
| TPrim TPrim
| TDef QName
| TApp TTerm Args
| TLam TTerm
| TLit Literal
| TCon QName
| TLet TTerm TTerm
| TCase Int CaseType TTerm [TAlt]
| TUnit
| TSort
| TErased
| TError TError
deriving (Typeable, Show, Eq, Ord)
data TPrim = PAdd | PSub | PMul | PQuot | PRem | PGeq | PLt | PEq | PIf | PSeq
deriving (Typeable, Show, Eq, Ord)
mkTApp :: TTerm -> Args -> TTerm
mkTApp x [] = x
mkTApp (TApp x as) bs = TApp x (as ++ bs)
mkTApp x as = TApp x as
tAppView :: TTerm -> [TTerm]
tAppView = view
where
view t = case t of
TApp a bs -> view a ++ bs
_ -> [t]
mkLet :: TTerm -> TTerm -> TTerm
mkLet x body = TLet x body
tInt :: Integer -> TTerm
tInt = TLit . LitNat noRange
intView :: TTerm -> Maybe Integer
intView (TLit (LitNat _ x)) = Just x
intView _ = Nothing
tPlusK :: Integer -> TTerm -> TTerm
tPlusK 0 n = n
tPlusK k n | k < 0 = tOp PSub n (tInt (k))
tPlusK k n = tOp PAdd (tInt k) n
tNegPlusK :: Integer -> TTerm -> TTerm
tNegPlusK k n = tOp PSub (tInt (k)) n
plusKView :: TTerm -> Maybe (Integer, TTerm)
plusKView (TApp (TPrim PAdd) [k, n]) | Just k <- intView k = Just (k, n)
plusKView _ = Nothing
negPlusKView :: TTerm -> Maybe (Integer, TTerm)
negPlusKView (TApp (TPrim PSub) [k, n]) | Just k <- intView k = Just (k, n)
negPlusKView _ = Nothing
tOp :: TPrim -> TTerm -> TTerm -> TTerm
tOp op a b = TApp (TPrim op) [a, b]
tUnreachable :: TTerm
tUnreachable = TError TUnreachable
data CaseType
= CTData QName
| CTChar
| CTString
| CTQName
deriving (Typeable, Show, Eq, Ord)
data TAlt
= TACon { aCon :: QName, aArity :: Int, aBody :: TTerm }
| TAGuard { aGuard :: TTerm, aBody :: TTerm }
| TALit { aLit :: Literal, aBody:: TTerm }
deriving (Typeable, Show, Eq, Ord)
data TError
= TUnreachable
deriving (Typeable, Show, Eq, Ord)
class Unreachable a where
isUnreachable :: a -> Bool
instance Unreachable TAlt where
isUnreachable = isUnreachable . aBody
instance Unreachable TTerm where
isUnreachable (TError TUnreachable{}) = True
isUnreachable (TLet _ b) = isUnreachable b
isUnreachable _ = False
instance KillRange Compiled where
killRange c = c