-- | A Term is a expression representing a domain element.  It is
-- composed of variables which can be bound to domain elements, or
-- functions which can be applied to terms to yield other domain
-- elements.

{-# 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
    ( -- * Variables
      IsVariable(variant, prefix)
    , variants
    --, showVariable
    , V(V)
    -- * Functions
    , IsFunction
    , Arity
    , FName(FName)
    -- * Terms
    , 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

---------------
-- VARIABLES --
---------------

class (Ord v, IsString v, Pretty v, Show v) => IsVariable v where
    variant :: v -> Set v -> v
    -- ^ Return a variable based on v but different from any set
    -- element.  The result may be v itself if v is not a member of
    -- the set.
    prefix :: String -> v -> v
    -- ^ Modify a variable by adding a prefix.  This unfortunately
    -- assumes that v is "string-like" but at least one algorithm in
    -- Harrison currently requires this.

-- | Return an infinite list of variations on 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'

-- | Because IsString is a superclass we can just output a string expression
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

---------------
-- FUNCTIONS --
---------------

class (IsString function, Ord function, Pretty function, Show function) => IsFunction function

type Arity = Int

-- | A simple type to use as the function parameter of Term.  The only
-- reason to use this instead of String is to get nicer pretty
-- printing.
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

-----------
-- TERMS --
-----------

-- | A term is an expression representing a domain element, either as
-- a variable reference or a function applied to a list of terms.
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
    -- ^ The associated variable type
    type FunOf term
    -- ^ The associated function type
    vt :: TVarOf term -> term
    -- ^ Build a term which is a variable reference.
    fApp :: FunOf term -> [term] -> term
    -- ^ Build a term by applying terms to an atomic function ('FunOf' @term@).
    foldTerm :: (TVarOf term -> r)          -- ^ Variable references are dispatched here
             -> (FunOf term -> [term] -> r) -- ^ Function applications are dispatched here
             -> term -> r
    -- ^ A fold over instances of 'IsTerm'.

-- | Combine two terms if they are similar (i.e. two variables or
-- two function applications.)
zipTerms :: (IsTerm term1, v1 ~ TVarOf term1, function1 ~ FunOf term1,
             IsTerm term2, v2 ~ TVarOf term2, function2 ~ FunOf term2) =>
            (v1 -> v2 -> Maybe r) -- ^ Combine two variables
         -> (function1 -> [term1] -> function2 -> [term2] -> Maybe r) -- ^ Combine two function applications
         -> term1
         -> term2
         -> Maybe r -- ^ Result for dissimilar terms is 'Nothing'.
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

-- | Convert between two instances of IsTerm
convertTerm :: (IsTerm term1, v1 ~ TVarOf term1, f1 ~ FunOf term1,
                IsTerm term2, v2 ~ TVarOf term2, f2 ~ FunOf term2) =>
               (v1 -> v2) -- ^ convert a variable
            -> (f1 -> f2) -- ^ convert a function
            -> 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

-- | Implementation of pPrint for any term
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)

-- | Format a function application: F(x,y)
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)))

-- | Implementation of show for any term
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

-- | Build an expression for a function application: fApp (F) [x, y]
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

-- | A term type with no Skolem functions
type FTerm = Term FName V

-- Example.
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])