{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PatternSynonyms #-}
module Agda.Syntax.Treeless
( module Agda.Syntax.Abstract.Name
, module Agda.Syntax.Treeless
) where
import Control.Arrow (first, second)
import Data.Map (Map)
import Data.Data (Data)
import Data.Word
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
data Compiled = Compiled
{ cTreeless :: TTerm
, cArgUsage :: [Bool] }
deriving (Data, Show, Eq, Ord)
data EvaluationStrategy = LazyEvaluation | EagerEvaluation
deriving (Eq, Show)
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 CaseInfo TTerm [TAlt]
| TUnit
| TSort
| TErased
| TCoerce TTerm
| TError TError
deriving (Data, Show, Eq, Ord)
data TPrim
= PAdd | PAdd64
| PSub | PSub64
| PMul | PMul64
| PQuot | PQuot64
| PRem | PRem64
| PGeq
| PLt | PLt64
| PEqI | PEq64
| PEqF
| PEqS
| PEqC
| PEqQ
| PIf
| PSeq
| PITo64 | P64ToI
deriving (Data, Show, Eq, Ord)
isPrimEq :: TPrim -> Bool
isPrimEq p = p `elem` [PEqI, PEqF, PEqS, PEqC, PEqQ, PEq64]
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]
tLetView :: TTerm -> ([TTerm], TTerm)
tLetView (TLet e b) = first (e :) $ tLetView b
tLetView e = ([], e)
tLamView :: TTerm -> (Int, TTerm)
tLamView = go 0
where go n (TLam b) = go (n + 1) b
go n t = (n, t)
mkTLam :: Int -> TTerm -> TTerm
mkTLam n b = foldr ($) b $ replicate n TLam
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
word64View :: TTerm -> Maybe Word64
word64View (TLit (LitWord64 _ x)) = Just x
word64View _ = 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 (TApp (TPrim PSub) [n, k]) | 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 = TPOp op a b
pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
pattern TPOp op a b = TApp (TPrim op) [a, b]
pattern TPFn :: TPrim -> TTerm -> TTerm
pattern TPFn op a = TApp (TPrim op) [a]
tUnreachable :: TTerm
tUnreachable = TError TUnreachable
tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
tIfThenElse c i e = TApp (TPrim PIf) [c, i, e]
data CaseType
= CTData QName
| CTNat
| CTInt
| CTChar
| CTString
| CTFloat
| CTQName
deriving (Data, Show, Eq, Ord)
data CaseInfo = CaseInfo
{ caseLazy :: Bool
, caseType :: CaseType }
deriving (Data, Show, Eq, Ord)
data TAlt
= TACon { aCon :: QName, aArity :: Int, aBody :: TTerm }
| TAGuard { aGuard :: TTerm, aBody :: TTerm }
| TALit { aLit :: Literal, aBody:: TTerm }
deriving (Data, Show, Eq, Ord)
data TError
= TUnreachable
deriving (Data, 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