module Term.Term (
FunSym(..)
, ACSym(..)
, NonACSym
, FunSig
, dhFunSig
, xorFunSig
, msetFunSig
, pairFunSig
, dhReducibleFunSig
, implicitFunSig
, Term
, TermView (..)
, viewTerm
, TermView2 (..)
, viewTerm2
, traverseTerm
, fmapTerm
, bindTerm
, lits
, prettyTerm
, lit
, fApp
, fAppAC
, fAppNonAC
, fAppList
, unsafefApp
, fAppMult
, fAppOne
, fAppExp
, fAppInv
, fAppXor
, fAppZero
, fAppUnion
, fAppEmpty
, fAppPair
, fAppFst
, fAppSnd
, expSymString
, invSymString
, destPair
, destInverse
, destProduct
, destXor
, destUnion
, isPair
, isInverse
, isProduct
, isXor
, isUnion
, module Term.Classes
) 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 Data.Maybe (isJust)
import Control.DeepSeq
import Control.Basics
import Data.ByteString (ByteString)
import qualified Data.ByteString.Char8 as BC
import Extension.Data.ByteString ()
import Data.Set (Set)
import qualified Data.Set as S
import Text.PrettyPrint.Class
import Term.Classes
data ACSym = Union | Xor | Mult
deriving (Eq, Ord, Typeable, Data, Show)
type NonACSym = (ByteString, Int)
data FunSym = NonAC NonACSym
| AC ACSym
| List
deriving (Eq, Ord, Typeable, Data, Show)
type FunSig = Set NonACSym
expSymString :: ByteString
expSymString = "exp"
invSymString :: ByteString
invSymString = "inv"
pairSym, expSym, invSym, oneSym, zeroSym, emptySym, fstSym, sndSym :: NonACSym
pairSym = ("pair",2)
expSym = (expSymString,2)
invSym = (invSymString,1)
oneSym = ("one", 0)
zeroSym = ("zero",0)
emptySym = ("empty",0)
fstSym = ("fst",1)
sndSym = ("snd",1)
dhFunSig :: FunSig
dhFunSig = S.fromList [ expSym, oneSym, invSym ]
xorFunSig :: FunSig
xorFunSig = S.fromList [ zeroSym ]
msetFunSig :: FunSig
msetFunSig = S.fromList [ emptySym ]
pairFunSig :: FunSig
pairFunSig = S.fromList [ pairSym, fstSym, sndSym ]
dhReducibleFunSig :: FunSig
dhReducibleFunSig = S.fromList [ expSym, invSym ]
implicitFunSig :: FunSig
implicitFunSig = S.fromList [ invSym, pairSym ]
data Term a = LIT a
| FAPP FunSym [Term a]
deriving (Eq, Ord, Typeable, Data )
destFunApp :: FunSym -> Term a -> Maybe [Term a]
destFunApp fsym (FAPP fsym' args) | fsym == fsym' = Just args
destFunApp _ _ = Nothing
destPair :: Term a -> Maybe (Term a, Term a)
destPair t = do [t1, t2] <- destFunApp (NonAC pairSym) t; return (t1, t2)
destInverse :: Term a -> Maybe (Term a)
destInverse t = do [t1] <- destFunApp (NonAC invSym) t; return t1
destProduct :: Term a -> Maybe [Term a]
destProduct (FAPP (AC Mult) ts) = return ts
destProduct _ = Nothing
destXor :: Term a -> Maybe [Term a]
destXor (FAPP (AC Xor) ts) = return ts
destXor _ = Nothing
destUnion :: Term a -> Maybe [Term a]
destUnion (FAPP (AC Union) ts) = return ts
destUnion _ = Nothing
isPair :: Term a -> Bool
isPair = isJust . destPair
isInverse :: Term a -> Bool
isInverse = isJust . destInverse
isProduct :: Term a -> Bool
isProduct = isJust . destProduct
isXor :: Term a -> Bool
isXor = isJust . destXor
isUnion :: Term a -> Bool
isUnion = isJust . destXor
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 o ts = FAPP o 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 ]
fAppNonAC :: NonACSym -> [Term a] -> Term a
fAppNonAC nacsym = FAPP (NonAC nacsym)
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
| FXor [Term a] | Zero
| FUnion [Term a] | Empty
| FPair (Term a) (Term a)
| FAppNonAC NonACSym [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 Xor = FXor
acSymToConstr Union = FUnion
viewTerm2 t@(FAPP (NonAC o) ts) = case ts of
[ t1, t2 ] | o == expSym -> FExp t1 t2
[ t1, t2 ] | o == pairSym -> FPair t1 t2
[ t1 ] | o == invSym -> FInv t1
[] | o == oneSym -> One
[] | o == zeroSym -> Zero
[] | o == emptySym -> Empty
_ | o `elem` ssyms -> error $ "viewTerm2: malformed term `"++show t++"'"
_ -> FAppNonAC o ts
where
ssyms = [ expSym, pairSym, invSym, oneSym, zeroSym, emptySym ]
fAppMult, fAppUnion, fAppXor :: Ord a => [Term a] -> Term a
fAppMult ts = fApp (AC Mult) ts
fAppUnion ts = fApp (AC Union) ts
fAppXor ts = fApp (AC Xor) ts
fAppOne, fAppZero, fAppEmpty :: Term a
fAppOne = fAppNonAC oneSym []
fAppZero = fAppNonAC zeroSym []
fAppEmpty = fAppNonAC emptySym []
fAppPair, fAppExp :: (Term a, Term a) -> Term a
fAppPair (x,y) = fAppNonAC pairSym [x, y]
fAppExp (b,e) = fAppNonAC expSym [b, e]
fAppInv, fAppFst, fAppSnd :: Term a -> Term a
fAppInv e = fAppNonAC invSym [e]
fAppFst a = fAppNonAC fstSym [a]
fAppSnd a = fAppNonAC sndSym [a]
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 (LIT l) = show l
show (FAPP (NonAC (s,_)) []) = BC.unpack s
show (FAPP (NonAC (s,_)) as) = BC.unpack s++"("++(intercalate "," (map show as))++")"
show (FAPP List as) = "LIST"++"("++(intercalate "," (map show as))++")"
show (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)
lits :: Ord a => Term a -> [a]
lits = foldMap return
prettyTerm :: Document d => (l -> d) -> Term l -> d
prettyTerm ppLit = ppTerm
where
ppTerm t = case t of
LIT l -> ppLit l
FAPP (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts
FAPP (NonAC ("exp",2)) [t1,t2] -> ppTerm t1 <> text "^" <> ppTerm t2
FAPP (NonAC ("pair",2)) _ -> ppTerms ", " 1 "<" ">" (split t)
FAPP (NonAC (f,_)) ts -> ppFun f ts
FAPP List ts -> ppFun "LIST" ts
ppACOp Mult = "*"
ppACOp Union = "#"
ppACOp Xor = "+"
ppTerms sepa n lead finish ts =
fcat . (text lead :) . (++[text finish]) .
map (nest n) . punctuate (text sepa) . map ppTerm $ ts
split (FAPP (NonAC ("pair",2)) [t1,t2]) = t1 : split t2
split t = [t]
ppFun f ts =
text (BC.unpack f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")"
$( derive makeNFData ''FunSym)
$( derive makeNFData ''ACSym)
$( derive makeNFData ''Term )
$( derive makeBinary ''FunSym)
$( derive makeBinary ''ACSym)
$( derive makeBinary ''Term )