module Term.Term (
prettyTerm
, showFunSymName
, lits
, fAppOne
, fAppExp
, fAppInv
, fAppPMult
, fAppEMap
, fAppPair
, fAppFst
, fAppSnd
, isPair
, isInverse
, isProduct
, isUnion
, isEMap
, isNullaryPublicFunction
, isPrivateFunction
, FunSym(..)
, ACSym(..)
, CSym(..)
, Privacy(..)
, NoEqSym
, FunSig
, NoEqFunSig
, expSymString
, invSymString
, pmultSymString
, emapSymString
, unionSymString
, expSym
, pmultSym
, dhFunSig
, bpFunSig
, msetFunSig
, pairFunSig
, dhReducibleFunSig
, bpReducibleFunSig
, implicitFunSig
, module Term.Term.Classes
, module Term.Term.Raw
) where
import Data.Monoid
import Data.Foldable (Foldable, foldMap)
import qualified Data.ByteString.Char8 as BC
import Extension.Data.ByteString ()
import Text.PrettyPrint.Class
import Term.Term.Classes
import Term.Term.FunctionSymbols
import Term.Term.Raw
fAppOne :: Term a
fAppOne = fAppNoEq oneSym []
fAppPair, fAppExp,fAppPMult, fAppEMap :: Ord a => (Term a, Term a) -> Term a
fAppPair (x,y) = fAppNoEq pairSym [x, y]
fAppExp (b,e) = fAppNoEq expSym [b, e]
fAppPMult (s,p) = fAppNoEq pmultSym [s, p]
fAppEMap (x,y) = fAppC EMap [x, y]
fAppInv, fAppFst, fAppSnd :: Term a -> Term a
fAppInv e = fAppNoEq invSym [e]
fAppFst a = fAppNoEq fstSym [a]
fAppSnd a = fAppNoEq sndSym [a]
lits :: Ord a => Term a -> [a]
lits = foldMap return
isPair :: Show a => Term a -> Bool
isPair (viewTerm2 -> FPair _ _) = True
isPair _ = False
isInverse :: Show a => Term a -> Bool
isInverse (viewTerm2 -> FInv _) = True
isInverse _ = False
isProduct :: Show a => Term a -> Bool
isProduct (viewTerm2 -> FMult _) = True
isProduct _ = False
isEMap :: Show a => Term a -> Bool
isEMap (viewTerm2 -> FEMap _ _) = True
isEMap _ = False
isUnion :: Show a => Term a -> Bool
isUnion (viewTerm2 -> FUnion _) = True
isUnion _ = False
isNullaryPublicFunction :: Term a -> Bool
isNullaryPublicFunction (viewTerm -> FApp (NoEq (_, (0, Public))) _) = True
isNullaryPublicFunction _ = False
isPrivateFunction :: Term a -> Bool
isPrivateFunction (viewTerm -> FApp (NoEq (_, (_,Private))) _) = True
isPrivateFunction _ = False
showFunSymName :: FunSym -> String
showFunSymName (NoEq (bs, _)) = BC.unpack bs
showFunSymName (AC op) = show op
showFunSymName (C op ) = show op
showFunSymName List = "List"
prettyTerm :: (Document d, Show l) => (l -> d) -> Term l -> d
prettyTerm ppLit = ppTerm
where
ppTerm t = case viewTerm t of
Lit l -> ppLit l
FApp (AC o) ts -> ppTerms (ppACOp o) 1 "(" ")" ts
FApp (NoEq s) [t1,t2] | s == expSym -> ppTerm t1 <> text "^" <> ppTerm t2
FApp (NoEq s) _ | s == pairSym -> ppTerms ", " 1 "<" ">" (split t)
FApp (NoEq (f, _)) [] -> text (BC.unpack f)
FApp (NoEq (f, _)) ts -> ppFun f ts
FApp (C EMap) ts -> ppFun emapSymString ts
FApp List ts -> ppFun "LIST" ts
ppACOp Mult = "*"
ppACOp Union = "+"
ppTerms sepa n lead finish ts =
fcat . (text lead :) . (++[text finish]) .
map (nest n) . punctuate (text sepa) . map ppTerm $ ts
split (viewTerm2 -> FPair t1 t2) = t1 : split t2
split t = [t]
ppFun f ts =
text (BC.unpack f ++"(") <> fsep (punctuate comma (map ppTerm ts)) <> text ")"