module Data.Logic.ATP.Term
(
IsVariable(variant, prefix)
, variants
, V(V)
, IsFunction
, Arity
, FName(FName)
, IsTerm(TVarOf, FunOf, vt, fApp, foldTerm)
, zipTerms
, convertTerm
, precedenceTerm
, associativityTerm
, prettyTerm
, prettyFunctionApply
, showTerm
, showFunctionApply
, funcs
, Term(Var, FApply)
, FTerm
, testTerm
) where
import Data.Data (Data)
import Data.Logic.ATP.Pretty ((<>), Associativity(InfixN), Doc, HasFixity(associativity, precedence), Precedence, prettyShow, text)
import Data.Set as Set (empty, insert, member, Set, singleton)
import Data.String (IsString(fromString))
import Data.Typeable (Typeable)
import Prelude hiding (pred)
import Text.PrettyPrint (parens, brackets, punctuate, comma, fsep, space)
import Text.PrettyPrint.HughesPJClass (maybeParens, Pretty(pPrint, pPrintPrec), PrettyLevel, prettyNormal)
import Test.HUnit
class (Ord v, IsString v, Pretty v, Show v) => IsVariable v where
variant :: v -> Set v -> v
prefix :: String -> v -> v
variants :: IsVariable v => v -> [v]
variants v0 =
loop Set.empty v0
where loop s v = let v' = variant v s in v' : loop (Set.insert v s) v'
showVariable :: IsVariable v => v -> String
showVariable v = show (prettyShow v)
newtype V = V String deriving (Eq, Ord, Data, Typeable, Read)
instance IsVariable String where
variant v vs = if Set.member v vs then variant (v ++ "'") vs else v
prefix pre s = pre ++ s
instance IsVariable V where
variant v@(V s) vs = if Set.member v vs then variant (V (s ++ "'")) vs else v
prefix pre (V s) = V (pre ++ s)
instance IsString V where
fromString = V
instance Show V where
show (V s) = show s
instance Pretty V where
pPrint (V s) = text s
class (IsString function, Ord function, Pretty function, Show function) => IsFunction function
type Arity = Int
newtype FName = FName String deriving (Eq, Ord)
instance IsFunction FName
instance IsString FName where fromString = FName
instance Show FName where show (FName s) = s
instance Pretty FName where pPrint (FName s) = text s
class (Eq term, Ord term, Pretty term, Show term, IsString term, HasFixity term,
IsVariable (TVarOf term), IsFunction (FunOf term)) => IsTerm term where
type TVarOf term
type FunOf term
vt :: TVarOf term -> term
fApp :: FunOf term -> [term] -> term
foldTerm :: (TVarOf term -> r)
-> (FunOf term -> [term] -> r)
-> term -> r
zipTerms :: (IsTerm term1, v1 ~ TVarOf term1, function1 ~ FunOf term1,
IsTerm term2, v2 ~ TVarOf term2, function2 ~ FunOf term2) =>
(v1 -> v2 -> Maybe r)
-> (function1 -> [term1] -> function2 -> [term2] -> Maybe r)
-> term1
-> term2
-> Maybe r
zipTerms v ap t1 t2 =
foldTerm v' ap' t1
where
v' v1 = foldTerm (v v1) (\_ _ -> Nothing) t2
ap' p1 ts1 = foldTerm (\_ -> Nothing) (\p2 ts2 -> if length ts1 == length ts2 then ap p1 ts1 p2 ts2 else Nothing) t2
convertTerm :: (IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1,
IsTerm term2, v2 ~ TVarOf term2, f2 ~ FunOf term2) =>
(v1 -> v2)
-> (f1 -> f2)
-> term1 -> term2
convertTerm cv cf = foldTerm (vt . cv) (\f ts -> fApp (cf f) (map (convertTerm cv cf) ts))
precedenceTerm :: IsTerm term => term -> Precedence
precedenceTerm = const 0
associativityTerm :: IsTerm term => term -> Associativity
associativityTerm = const InfixN
prettyTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, HasFixity term, Pretty v, Pretty function) =>
PrettyLevel -> Rational -> term -> Doc
prettyTerm l r tm = maybeParens (l > prettyNormal || r > precedence tm) (foldTerm pPrint (prettyFunctionApply l) tm)
prettyFunctionApply :: (function ~ FunOf term, IsTerm term, HasFixity term) => PrettyLevel -> function -> [term] -> Doc
prettyFunctionApply _l f [] = pPrint f
prettyFunctionApply l f ts = pPrint f <> parens (fsep (punctuate comma (map (prettyTerm l 0) ts)))
showTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v, Pretty function) => term -> String
showTerm = foldTerm showVariable showFunctionApply
showFunctionApply :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term) => function -> [term] -> String
showFunctionApply f ts = "fApp (" <> show f <> ")" <> show (brackets (fsep (punctuate (comma <> space) (map (text . show) ts))))
funcs :: (IsTerm term, function ~ FunOf term) => term -> Set (function, Arity)
funcs = foldTerm (\_ -> Set.empty) (\f ts -> Set.singleton (f, length ts))
data Term function v
= Var v
| FApply function [Term function v]
deriving (Eq, Ord, Data, Typeable, Read)
instance (IsVariable v, IsFunction function) => IsString (Term function v) where
fromString = Var . fromString
instance (IsVariable v, IsFunction function) => Show (Term function v) where
show = showTerm
instance (IsFunction function, IsVariable v) => HasFixity (Term function v) where
precedence = precedenceTerm
associativity = associativityTerm
instance (IsFunction function, IsVariable v) => IsTerm (Term function v) where
type TVarOf (Term function v) = v
type FunOf (Term function v) = function
vt = Var
fApp = FApply
foldTerm vf fn t =
case t of
Var v -> vf v
FApply f ts -> fn f ts
instance (IsTerm (Term function v)) => Pretty (Term function v) where
pPrintPrec = prettyTerm
type FTerm = Term FName V
test00 :: Test
test00 = TestCase $ assertEqual "print an expression"
"sqrt(-(1, cos(power(+(x, y), 2))))"
(prettyShow (fApp "sqrt" [fApp "-" [fApp "1" [],
fApp "cos" [fApp "power" [fApp "+" [Var "x", Var "y"],
fApp "2" []]]]] :: Term FName V))
testTerm :: Test
testTerm = TestLabel "Term" (TestList [test00])