module Term.Term.Raw (
Term
, TermView (..)
, viewTerm
, TermView2 (..)
, viewTerm2
, traverseTerm
, fmapTerm
, bindTerm
, lit
, fApp
, fAppAC
, fAppC
, fAppNoEq
, fAppList
, unsafefApp
) where
import Data.List
import Data.Monoid
import Data.Foldable (Foldable, foldMap)
import Data.Traversable
import Data.Typeable
import Data.Generics
import Data.DeriveTH
import Data.Binary
import Control.DeepSeq
import Control.Basics
import qualified Data.ByteString.Char8 as BC
import Extension.Data.ByteString ()
import Term.Term.Classes
import Term.Term.FunctionSymbols
data Term a = LIT a
| FAPP FunSym [Term a]
deriving (Eq, Ord, Typeable, Data )
data TermView a = Lit a
| FApp FunSym [Term a]
deriving (Show, Eq, Ord)
viewTerm :: Term a -> TermView a
viewTerm (LIT l) = Lit l
viewTerm (FAPP sym ts) = FApp sym ts
fApp :: Ord a => FunSym -> [Term a] -> Term a
fApp (AC acSym) ts = fAppAC acSym ts
fApp (C o) ts = fAppC o ts
fApp List ts = FAPP List ts
fApp s@(NoEq _) ts = FAPP s ts
fAppAC :: Ord a => ACSym -> [Term a] -> Term a
fAppAC _ [] = error "Term.fAppAC: empty argument list"
fAppAC _ [a] = a
fAppAC acsym as =
FAPP (AC acsym) (sort (o_as ++ non_o_as))
where
o = AC acsym
isOTerm (FAPP o' _) | o' == o = True
isOTerm _ = False
(o_as0, non_o_as) = partition isOTerm as
o_as = [ a | FAPP _ ts <- o_as0, a <- ts ]
fAppC :: Ord a => CSym -> [Term a] -> Term a
fAppC nacsym as = FAPP (C nacsym) (sort as)
fAppNoEq :: NoEqSym -> [Term a] -> Term a
fAppNoEq freesym = FAPP (NoEq freesym)
fAppList :: [Term a] -> Term a
fAppList = FAPP List
lit :: a -> Term a
lit l = LIT l
unsafefApp :: FunSym -> [Term a] -> Term a
unsafefApp fsym as = FAPP fsym as
data TermView2 a = FExp (Term a) (Term a) | FInv (Term a) | FMult [Term a] | One
| FPMult (Term a) (Term a) | FEMap (Term a) (Term a)
| FUnion [Term a]
| FPair (Term a) (Term a)
| FAppNoEq NoEqSym [Term a]
| FAppC CSym [Term a]
| FList [Term a]
| Lit2 a
deriving (Show, Eq, Ord)
viewTerm2 :: Show a => Term a -> TermView2 a
viewTerm2 (LIT l) = Lit2 l
viewTerm2 (FAPP List ts) = FList ts
viewTerm2 t@(FAPP (AC o) ts)
| length ts < 2 = error $ "viewTerm2: malformed term `"++show t++"'"
| otherwise = (acSymToConstr o) ts
where
acSymToConstr Mult = FMult
acSymToConstr Union = FUnion
viewTerm2 (FAPP (C EMap) [ t1 ,t2 ]) = FEMap t1 t2
viewTerm2 t@(FAPP (C _) _) = error $ "viewTerm2: malformed term `"++show t++"'"
viewTerm2 t@(FAPP (NoEq o) ts) = case ts of
[ t1, t2 ] | o == expSym -> FExp t1 t2
[ t1, t2 ] | o == pmultSym -> FPMult t1 t2
[ t1, t2 ] | o == pairSym -> FPair t1 t2
[ t1 ] | o == invSym -> FInv t1
[] | o == oneSym -> One
_ | o `elem` ssyms -> error $ "viewTerm2: malformed term `"++show t++"'"
_ -> FAppNoEq o ts
where
ssyms = [ expSym, pairSym, invSym, oneSym, pmultSym ]
traverseTerm :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Term a -> f (Term b)
traverseTerm f (LIT x) = LIT <$> f x
traverseTerm f (FAPP fsym as) = fApp fsym <$> traverse (traverseTerm f) as
fmapTerm :: (Ord a, Ord b) => (a -> b) -> Term a -> Term b
fmapTerm f = foldTerm (lit . f) fApp
bindTerm :: (Ord a, Ord b) => Term a -> (a -> Term b) -> Term b
bindTerm m f = foldTerm f fApp m
instance Foldable Term where
foldMap f = foldTerm f (const mconcat)
instance Show a => Show (Term a) where
show t =
case viewTerm t of
Lit l -> show l
FApp (NoEq (s,_)) [] -> BC.unpack s
FApp (NoEq (s,_)) as -> BC.unpack s++"("++(intercalate "," (map show as))++")"
FApp (C EMap) as -> BC.unpack emapSymString++"("++(intercalate "," (map show as))++")"
FApp List as -> "LIST"++"("++(intercalate "," (map show as))++")"
FApp (AC o) as -> show o++"("++(intercalate "," (map show as))++")"
foldTerm :: (t -> b) -> (FunSym -> [b] -> b)
-> Term t -> b
foldTerm fLIT fFAPP t = go t
where go (LIT a) = fLIT a
go (FAPP fsym a) = fFAPP fsym $ map go a
instance Sized a => Sized (Term a) where
size = foldTerm size (const $ \xs -> sum xs + 1)
$( derive makeNFData ''Term )
$( derive makeBinary ''Term )