{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-}
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 :: forall v. IsVariable v => v -> [v]
variants v
v0 =
Set v -> v -> [v]
forall {t}. IsVariable t => Set t -> t -> [t]
loop Set v
forall a. Set a
Set.empty v
v0
where loop :: Set t -> t -> [t]
loop Set t
s t
v = let v' :: t
v' = t -> Set t -> t
forall v. IsVariable v => v -> Set v -> v
variant t
v Set t
s in t
v' t -> [t] -> [t]
forall a. a -> [a] -> [a]
: Set t -> t -> [t]
loop (t -> Set t -> Set t
forall a. Ord a => a -> Set a -> Set a
Set.insert t
v Set t
s) t
v'
showVariable :: IsVariable v => v -> String
showVariable :: forall v. IsVariable v => v -> String
showVariable v
v = String -> String
forall a. Show a => a -> String
show (v -> String
forall a. Pretty a => a -> String
prettyShow v
v)
newtype V = V String deriving (V -> V -> Bool
(V -> V -> Bool) -> (V -> V -> Bool) -> Eq V
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: V -> V -> Bool
== :: V -> V -> Bool
$c/= :: V -> V -> Bool
/= :: V -> V -> Bool
Eq, Eq V
Eq V =>
(V -> V -> Ordering)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> Bool)
-> (V -> V -> V)
-> (V -> V -> V)
-> Ord V
V -> V -> Bool
V -> V -> Ordering
V -> V -> V
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: V -> V -> Ordering
compare :: V -> V -> Ordering
$c< :: V -> V -> Bool
< :: V -> V -> Bool
$c<= :: V -> V -> Bool
<= :: V -> V -> Bool
$c> :: V -> V -> Bool
> :: V -> V -> Bool
$c>= :: V -> V -> Bool
>= :: V -> V -> Bool
$cmax :: V -> V -> V
max :: V -> V -> V
$cmin :: V -> V -> V
min :: V -> V -> V
Ord, Typeable V
Typeable V =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V)
-> (V -> Constr)
-> (V -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V))
-> ((forall b. Data b => b -> b) -> V -> V)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r)
-> (forall u. (forall d. Data d => d -> u) -> V -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> V -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V)
-> Data V
V -> Constr
V -> DataType
(forall b. Data b => b -> b) -> V -> V
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> V -> u
forall u. (forall d. Data d => d -> u) -> V -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> V -> c V
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c V
$ctoConstr :: V -> Constr
toConstr :: V -> Constr
$cdataTypeOf :: V -> DataType
dataTypeOf :: V -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c V)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c V)
$cgmapT :: (forall b. Data b => b -> b) -> V -> V
gmapT :: (forall b. Data b => b -> b) -> V -> V
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> V -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> V -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> V -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> V -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> V -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> V -> m V
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> V -> m V
Data, Typeable, ReadPrec [V]
ReadPrec V
Int -> ReadS V
ReadS [V]
(Int -> ReadS V)
-> ReadS [V] -> ReadPrec V -> ReadPrec [V] -> Read V
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS V
readsPrec :: Int -> ReadS V
$creadList :: ReadS [V]
readList :: ReadS [V]
$creadPrec :: ReadPrec V
readPrec :: ReadPrec V
$creadListPrec :: ReadPrec [V]
readListPrec :: ReadPrec [V]
Read)
instance IsVariable String where
variant :: String -> Set String -> String
variant String
v Set String
vs = if String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member String
v Set String
vs then String -> Set String -> String
forall v. IsVariable v => v -> Set v -> v
variant (String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'") Set String
vs else String
v
prefix :: String -> String -> String
prefix String
pre String
s = String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
instance IsVariable V where
variant :: V -> Set V -> V
variant v :: V
v@(V String
s) Set V
vs = if V -> Set V -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member V
v Set V
vs then V -> Set V -> V
forall v. IsVariable v => v -> Set v -> v
variant (String -> V
V (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"'")) Set V
vs else V
v
prefix :: String -> V -> V
prefix String
pre (V String
s) = String -> V
V (String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
instance IsString V where
fromString :: String -> V
fromString = String -> V
V
instance Show V where
show :: V -> String
show (V String
s) = String -> String
forall a. Show a => a -> String
show String
s
instance Pretty V where
pPrint :: V -> Doc
pPrint (V String
s) = String -> Doc
text String
s
class (IsString function, Ord function, Pretty function, Show function) => IsFunction function
type Arity = Int
newtype FName = FName String deriving (FName -> FName -> Bool
(FName -> FName -> Bool) -> (FName -> FName -> Bool) -> Eq FName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FName -> FName -> Bool
== :: FName -> FName -> Bool
$c/= :: FName -> FName -> Bool
/= :: FName -> FName -> Bool
Eq, Eq FName
Eq FName =>
(FName -> FName -> Ordering)
-> (FName -> FName -> Bool)
-> (FName -> FName -> Bool)
-> (FName -> FName -> Bool)
-> (FName -> FName -> Bool)
-> (FName -> FName -> FName)
-> (FName -> FName -> FName)
-> Ord FName
FName -> FName -> Bool
FName -> FName -> Ordering
FName -> FName -> FName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FName -> FName -> Ordering
compare :: FName -> FName -> Ordering
$c< :: FName -> FName -> Bool
< :: FName -> FName -> Bool
$c<= :: FName -> FName -> Bool
<= :: FName -> FName -> Bool
$c> :: FName -> FName -> Bool
> :: FName -> FName -> Bool
$c>= :: FName -> FName -> Bool
>= :: FName -> FName -> Bool
$cmax :: FName -> FName -> FName
max :: FName -> FName -> FName
$cmin :: FName -> FName -> FName
min :: FName -> FName -> FName
Ord)
instance IsFunction FName
instance IsString FName where fromString :: String -> FName
fromString = String -> FName
FName
instance Show FName where show :: FName -> String
show (FName String
s) = String
s
instance Pretty FName where pPrint :: FName -> Doc
pPrint (FName String
s) = String -> Doc
text String
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 :: forall term1 v1 function1 term2 v2 function2 r.
(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 v1 -> v2 -> Maybe r
v function1 -> [term1] -> function2 -> [term2] -> Maybe r
ap term1
t1 term2
t2 =
(TVarOf term1 -> Maybe r)
-> (FunOf term1 -> [term1] -> Maybe r) -> term1 -> Maybe r
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term1 -> r) -> (FunOf term1 -> [term1] -> r) -> term1 -> r
foldTerm v1 -> Maybe r
TVarOf term1 -> Maybe r
v' function1 -> [term1] -> Maybe r
FunOf term1 -> [term1] -> Maybe r
ap' term1
t1
where
v' :: v1 -> Maybe r
v' v1
v1 = (TVarOf term2 -> Maybe r)
-> (FunOf term2 -> [term2] -> Maybe r) -> term2 -> Maybe r
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term2 -> r) -> (FunOf term2 -> [term2] -> r) -> term2 -> r
foldTerm (v1 -> v2 -> Maybe r
v v1
v1) (\FunOf term2
_ [term2]
_ -> Maybe r
forall a. Maybe a
Nothing) term2
t2
ap' :: function1 -> [term1] -> Maybe r
ap' function1
p1 [term1]
ts1 = (TVarOf term2 -> Maybe r)
-> (FunOf term2 -> [term2] -> Maybe r) -> term2 -> Maybe r
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term2 -> r) -> (FunOf term2 -> [term2] -> r) -> term2 -> r
foldTerm (\TVarOf term2
_ -> Maybe r
forall a. Maybe a
Nothing) (\FunOf term2
p2 [term2]
ts2 -> if [term1] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term1]
ts1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [term2] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term2]
ts2 then function1 -> [term1] -> function2 -> [term2] -> Maybe r
ap function1
p1 [term1]
ts1 function2
FunOf term2
p2 [term2]
ts2 else Maybe r
forall a. Maybe a
Nothing) term2
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 :: forall term1 v1 f1 term2 v2 f2.
(IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1, IsTerm term2,
v2 ~ TVarOf term2, f2 ~ FunOf term2) =>
(v1 -> v2) -> (f1 -> f2) -> term1 -> term2
convertTerm v1 -> v2
cv f1 -> f2
cf = (TVarOf term1 -> term2)
-> (FunOf term1 -> [term1] -> term2) -> term1 -> term2
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term1 -> r) -> (FunOf term1 -> [term1] -> r) -> term1 -> r
foldTerm (v2 -> term2
TVarOf term2 -> term2
forall term. IsTerm term => TVarOf term -> term
vt (v2 -> term2) -> (v1 -> v2) -> v1 -> term2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v1 -> v2
cv) (\FunOf term1
f [term1]
ts -> FunOf term2 -> [term2] -> term2
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (f1 -> f2
cf f1
FunOf term1
f) ((term1 -> term2) -> [term1] -> [term2]
forall a b. (a -> b) -> [a] -> [b]
map ((v1 -> v2) -> (f1 -> f2) -> term1 -> term2
forall term1 v1 f1 term2 v2 f2.
(IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1, IsTerm term2,
v2 ~ TVarOf term2, f2 ~ FunOf term2) =>
(v1 -> v2) -> (f1 -> f2) -> term1 -> term2
convertTerm v1 -> v2
cv f1 -> f2
cf) [term1]
ts))
precedenceTerm :: IsTerm term => term -> Precedence
precedenceTerm :: forall term. IsTerm term => term -> Precedence
precedenceTerm = a -> term -> a
forall a b. a -> b -> a
const a
0
associativityTerm :: IsTerm term => term -> Associativity
associativityTerm :: forall term. IsTerm term => term -> Associativity
associativityTerm = Associativity -> term -> Associativity
forall a b. a -> b -> a
const Associativity
InfixN
prettyTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, HasFixity term, Pretty v, Pretty function) =>
PrettyLevel -> Rational -> term -> Doc
prettyTerm :: forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term,
HasFixity term, Pretty v, Pretty function) =>
PrettyLevel -> Rational -> term -> Doc
prettyTerm PrettyLevel
l Rational
r term
tm = Bool -> Doc -> Doc
maybeParens (PrettyLevel
l PrettyLevel -> PrettyLevel -> Bool
forall a. Ord a => a -> a -> Bool
> PrettyLevel
prettyNormal Bool -> Bool -> Bool
|| Rational
r Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> term -> Precedence
forall x. HasFixity x => x -> Precedence
precedence term
tm) ((TVarOf term -> Doc)
-> (FunOf term -> [term] -> Doc) -> term -> Doc
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Doc
TVarOf term -> Doc
forall a. Pretty a => a -> Doc
pPrint (PrettyLevel -> function -> [term] -> Doc
forall function term.
(function ~ FunOf term, IsTerm term, HasFixity term) =>
PrettyLevel -> function -> [term] -> Doc
prettyFunctionApply PrettyLevel
l) term
tm)
prettyFunctionApply :: (function ~ FunOf term, IsTerm term, HasFixity term) => PrettyLevel -> function -> [term] -> Doc
prettyFunctionApply :: forall function term.
(function ~ FunOf term, IsTerm term, HasFixity term) =>
PrettyLevel -> function -> [term] -> Doc
prettyFunctionApply PrettyLevel
_l function
f [] = function -> Doc
forall a. Pretty a => a -> Doc
pPrint function
f
prettyFunctionApply PrettyLevel
l function
f [term]
ts = function -> Doc
forall a. Pretty a => a -> Doc
pPrint function
f Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
parens ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ((term -> Doc) -> [term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (PrettyLevel -> Rational -> term -> Doc
forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term,
HasFixity term, Pretty v, Pretty function) =>
PrettyLevel -> Rational -> term -> Doc
prettyTerm PrettyLevel
l Rational
0) [term]
ts)))
showTerm :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v, Pretty function) => term -> String
showTerm :: forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v,
Pretty function) =>
term -> String
showTerm = (TVarOf term -> String)
-> (FunOf term -> [term] -> String) -> term -> String
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> String
TVarOf term -> String
forall v. IsVariable v => v -> String
showVariable function -> [term] -> String
FunOf term -> [term] -> String
forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term) =>
function -> [term] -> String
showFunctionApply
showFunctionApply :: (v ~ TVarOf term, function ~ FunOf term, IsTerm term) => function -> [term] -> String
showFunctionApply :: forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term) =>
function -> [term] -> String
showFunctionApply function
f [term]
ts = String
"fApp (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> function -> String
forall a. Show a => a -> String
show function
f String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Doc -> String
forall a. Show a => a -> String
show (Doc -> Doc
brackets ([Doc] -> Doc
fsep (Doc -> [Doc] -> [Doc]
punctuate (Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
space) ((term -> Doc) -> [term] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Doc
text (String -> Doc) -> (term -> String) -> term -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term -> String
forall a. Show a => a -> String
show) [term]
ts))))
funcs :: (IsTerm term, function ~ FunOf term) => term -> Set (function, Arity)
funcs :: forall term function.
(IsTerm term, function ~ FunOf term) =>
term -> Set (function, Int)
funcs = (TVarOf term -> Set (function, Int))
-> (FunOf term -> [term] -> Set (function, Int))
-> term
-> Set (function, Int)
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm (\TVarOf term
_ -> Set (function, Int)
forall a. Set a
Set.empty) (\FunOf term
f [term]
ts -> (function, Int) -> Set (function, Int)
forall a. a -> Set a
Set.singleton (function
FunOf term
f, [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
ts))
data Term function v
= Var v
| FApply function [Term function v]
deriving (Term function v -> Term function v -> Bool
(Term function v -> Term function v -> Bool)
-> (Term function v -> Term function v -> Bool)
-> Eq (Term function v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall function v.
(Eq v, Eq function) =>
Term function v -> Term function v -> Bool
$c== :: forall function v.
(Eq v, Eq function) =>
Term function v -> Term function v -> Bool
== :: Term function v -> Term function v -> Bool
$c/= :: forall function v.
(Eq v, Eq function) =>
Term function v -> Term function v -> Bool
/= :: Term function v -> Term function v -> Bool
Eq, Eq (Term function v)
Eq (Term function v) =>
(Term function v -> Term function v -> Ordering)
-> (Term function v -> Term function v -> Bool)
-> (Term function v -> Term function v -> Bool)
-> (Term function v -> Term function v -> Bool)
-> (Term function v -> Term function v -> Bool)
-> (Term function v -> Term function v -> Term function v)
-> (Term function v -> Term function v -> Term function v)
-> Ord (Term function v)
Term function v -> Term function v -> Bool
Term function v -> Term function v -> Ordering
Term function v -> Term function v -> Term function v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall function v. (Ord v, Ord function) => Eq (Term function v)
forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Bool
forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Ordering
forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Term function v
$ccompare :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Ordering
compare :: Term function v -> Term function v -> Ordering
$c< :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Bool
< :: Term function v -> Term function v -> Bool
$c<= :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Bool
<= :: Term function v -> Term function v -> Bool
$c> :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Bool
> :: Term function v -> Term function v -> Bool
$c>= :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Bool
>= :: Term function v -> Term function v -> Bool
$cmax :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Term function v
max :: Term function v -> Term function v -> Term function v
$cmin :: forall function v.
(Ord v, Ord function) =>
Term function v -> Term function v -> Term function v
min :: Term function v -> Term function v -> Term function v
Ord, Typeable (Term function v)
Typeable (Term function v) =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term function v -> c (Term function v))
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term function v))
-> (Term function v -> Constr)
-> (Term function v -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Term function v)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term function v)))
-> ((forall b. Data b => b -> b)
-> Term function v -> Term function v)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r)
-> (forall u.
(forall d. Data d => d -> u) -> Term function v -> [u])
-> (forall u.
Int -> (forall d. Data d => d -> u) -> Term function v -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v))
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v))
-> Data (Term function v)
Term function v -> Constr
Term function v -> DataType
(forall b. Data b => b -> b) -> Term function v -> Term function v
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Term function v -> u
forall u. (forall d. Data d => d -> u) -> Term function v -> [u]
forall function v.
(Data v, Data function) =>
Typeable (Term function v)
forall function v.
(Data v, Data function) =>
Term function v -> Constr
forall function v.
(Data v, Data function) =>
Term function v -> DataType
forall function v.
(Data v, Data function) =>
(forall b. Data b => b -> b) -> Term function v -> Term function v
forall function v u.
(Data v, Data function) =>
Int -> (forall d. Data d => d -> u) -> Term function v -> u
forall function v u.
(Data v, Data function) =>
(forall d. Data d => d -> u) -> Term function v -> [u]
forall function v r r'.
(Data v, Data function) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
forall function v r r'.
(Data v, Data function) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
forall function v (m :: * -> *).
(Data v, Data function, Monad m) =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
forall function v (m :: * -> *).
(Data v, Data function, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
forall function v (c :: * -> *).
(Data v, Data function) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term function v)
forall function v (c :: * -> *).
(Data v, Data function) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term function v -> c (Term function v)
forall function v (t :: * -> *) (c :: * -> *).
(Data v, Data function, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Term function v))
forall function v (t :: * -> * -> *) (c :: * -> *).
(Data v, Data function, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term function v))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term function v)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term function v -> c (Term function v)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Term function v))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term function v))
$cgfoldl :: forall function v (c :: * -> *).
(Data v, Data function) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term function v -> c (Term function v)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Term function v -> c (Term function v)
$cgunfold :: forall function v (c :: * -> *).
(Data v, Data function) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term function v)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Term function v)
$ctoConstr :: forall function v.
(Data v, Data function) =>
Term function v -> Constr
toConstr :: Term function v -> Constr
$cdataTypeOf :: forall function v.
(Data v, Data function) =>
Term function v -> DataType
dataTypeOf :: Term function v -> DataType
$cdataCast1 :: forall function v (t :: * -> *) (c :: * -> *).
(Data v, Data function, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Term function v))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Term function v))
$cdataCast2 :: forall function v (t :: * -> * -> *) (c :: * -> *).
(Data v, Data function, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term function v))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Term function v))
$cgmapT :: forall function v.
(Data v, Data function) =>
(forall b. Data b => b -> b) -> Term function v -> Term function v
gmapT :: (forall b. Data b => b -> b) -> Term function v -> Term function v
$cgmapQl :: forall function v r r'.
(Data v, Data function) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
$cgmapQr :: forall function v r r'.
(Data v, Data function) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Term function v -> r
$cgmapQ :: forall function v u.
(Data v, Data function) =>
(forall d. Data d => d -> u) -> Term function v -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Term function v -> [u]
$cgmapQi :: forall function v u.
(Data v, Data function) =>
Int -> (forall d. Data d => d -> u) -> Term function v -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> Term function v -> u
$cgmapM :: forall function v (m :: * -> *).
(Data v, Data function, Monad m) =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
$cgmapMp :: forall function v (m :: * -> *).
(Data v, Data function, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
$cgmapMo :: forall function v (m :: * -> *).
(Data v, Data function, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Term function v -> m (Term function v)
Data, Typeable, ReadPrec [Term function v]
ReadPrec (Term function v)
Int -> ReadS (Term function v)
ReadS [Term function v]
(Int -> ReadS (Term function v))
-> ReadS [Term function v]
-> ReadPrec (Term function v)
-> ReadPrec [Term function v]
-> Read (Term function v)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall function v.
(Read v, Read function) =>
ReadPrec [Term function v]
forall function v.
(Read v, Read function) =>
ReadPrec (Term function v)
forall function v.
(Read v, Read function) =>
Int -> ReadS (Term function v)
forall function v.
(Read v, Read function) =>
ReadS [Term function v]
$creadsPrec :: forall function v.
(Read v, Read function) =>
Int -> ReadS (Term function v)
readsPrec :: Int -> ReadS (Term function v)
$creadList :: forall function v.
(Read v, Read function) =>
ReadS [Term function v]
readList :: ReadS [Term function v]
$creadPrec :: forall function v.
(Read v, Read function) =>
ReadPrec (Term function v)
readPrec :: ReadPrec (Term function v)
$creadListPrec :: forall function v.
(Read v, Read function) =>
ReadPrec [Term function v]
readListPrec :: ReadPrec [Term function v]
Read)
instance (IsVariable v, IsFunction function) => IsString (Term function v) where
fromString :: String -> Term function v
fromString = v -> Term function v
forall function v. v -> Term function v
Var (v -> Term function v)
-> (String -> v) -> String -> Term function v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> v
forall a. IsString a => String -> a
fromString
instance (IsVariable v, IsFunction function) => Show (Term function v) where
show :: Term function v -> String
show = Term function v -> String
forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term, Pretty v,
Pretty function) =>
term -> String
showTerm
instance (IsFunction function, IsVariable v) => HasFixity (Term function v) where
precedence :: Term function v -> Precedence
precedence = Term function v -> a
Term function v -> Precedence
forall term. IsTerm term => term -> Precedence
precedenceTerm
associativity :: Term function v -> Associativity
associativity = Term function v -> Associativity
forall term. IsTerm term => term -> 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 :: TVarOf (Term function v) -> Term function v
vt = v -> Term function v
TVarOf (Term function v) -> Term function v
forall function v. v -> Term function v
Var
fApp :: FunOf (Term function v) -> [Term function v] -> Term function v
fApp = function -> [Term function v] -> Term function v
FunOf (Term function v) -> [Term function v] -> Term function v
forall function v. function -> [Term function v] -> Term function v
FApply
foldTerm :: forall r.
(TVarOf (Term function v) -> r)
-> (FunOf (Term function v) -> [Term function v] -> r)
-> Term function v
-> r
foldTerm TVarOf (Term function v) -> r
vf FunOf (Term function v) -> [Term function v] -> r
fn Term function v
t =
case Term function v
t of
Var v
v -> TVarOf (Term function v) -> r
vf v
TVarOf (Term function v)
v
FApply function
f [Term function v]
ts -> FunOf (Term function v) -> [Term function v] -> r
fn function
FunOf (Term function v)
f [Term function v]
ts
instance (IsTerm (Term function v)) => Pretty (Term function v) where
pPrintPrec :: PrettyLevel -> Rational -> Term function v -> Doc
pPrintPrec = PrettyLevel -> Rational -> Term function v -> Doc
forall v term function.
(v ~ TVarOf term, function ~ FunOf term, IsTerm term,
HasFixity term, Pretty v, Pretty function) =>
PrettyLevel -> Rational -> term -> Doc
prettyTerm
type FTerm = Term FName V
test00 :: Test
test00 :: Test
test00 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"print an expression"
String
"sqrt(-(1, cos(power(+(x, y), 2))))"
(Term FName V -> String
forall a. Pretty a => a -> String
prettyShow (FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"sqrt" [FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"-" [FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"1" [],
FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"cos" [FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"power" [FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"+" [V -> Term FName V
forall function v. v -> Term function v
Var V
"x", V -> Term FName V
forall function v. v -> Term function v
Var V
"y"],
FunOf (Term FName V) -> [Term FName V] -> Term FName V
forall term. IsTerm term => FunOf term -> [term] -> term
fApp FunOf (Term FName V)
FName
"2" []]]]] :: Term FName V))
testTerm :: Test
testTerm :: Test
testTerm = String -> Test -> Test
TestLabel String
"Term" ([Test] -> Test
TestList [Test
test00])