-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Bertram Felgenhauer

module Data.Rewriting.Term.Type (
    Term (..),
    fold,
    map,
) where

import Prelude hiding (map)

data Term f v
    = Var v            -- ^ Variable
    | Fun f [Term f v] -- ^ Function application
    deriving (Int -> Term f v -> ShowS
[Term f v] -> ShowS
Term f v -> String
(Int -> Term f v -> ShowS)
-> (Term f v -> String) -> ([Term f v] -> ShowS) -> Show (Term f v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f v. (Show v, Show f) => Int -> Term f v -> ShowS
forall f v. (Show v, Show f) => [Term f v] -> ShowS
forall f v. (Show v, Show f) => Term f v -> String
$cshowsPrec :: forall f v. (Show v, Show f) => Int -> Term f v -> ShowS
showsPrec :: Int -> Term f v -> ShowS
$cshow :: forall f v. (Show v, Show f) => Term f v -> String
show :: Term f v -> String
$cshowList :: forall f v. (Show v, Show f) => [Term f v] -> ShowS
showList :: [Term f v] -> ShowS
Show, Term f v -> Term f v -> Bool
(Term f v -> Term f v -> Bool)
-> (Term f v -> Term f v -> Bool) -> Eq (Term f v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f v. (Eq v, Eq f) => Term f v -> Term f v -> Bool
$c== :: forall f v. (Eq v, Eq f) => Term f v -> Term f v -> Bool
== :: Term f v -> Term f v -> Bool
$c/= :: forall f v. (Eq v, Eq f) => Term f v -> Term f v -> Bool
/= :: Term f v -> Term f v -> Bool
Eq, Eq (Term f v)
Eq (Term f v) =>
(Term f v -> Term f v -> Ordering)
-> (Term f v -> Term f v -> Bool)
-> (Term f v -> Term f v -> Bool)
-> (Term f v -> Term f v -> Bool)
-> (Term f v -> Term f v -> Bool)
-> (Term f v -> Term f v -> Term f v)
-> (Term f v -> Term f v -> Term f v)
-> Ord (Term f v)
Term f v -> Term f v -> Bool
Term f v -> Term f v -> Ordering
Term f v -> Term f v -> Term f 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 f v. (Ord v, Ord f) => Eq (Term f v)
forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Bool
forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Ordering
forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Term f v
$ccompare :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Ordering
compare :: Term f v -> Term f v -> Ordering
$c< :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Bool
< :: Term f v -> Term f v -> Bool
$c<= :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Bool
<= :: Term f v -> Term f v -> Bool
$c> :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Bool
> :: Term f v -> Term f v -> Bool
$c>= :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Bool
>= :: Term f v -> Term f v -> Bool
$cmax :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Term f v
max :: Term f v -> Term f v -> Term f v
$cmin :: forall f v. (Ord v, Ord f) => Term f v -> Term f v -> Term f v
min :: Term f v -> Term f v -> Term f v
Ord)

-- | Folding terms.
--
-- >>> fold (\v -> 1) (\f xs -> 1 + sum xs) (Fun 'f' [Var 1, Fun 'g' []])
-- 3 -- size of the given term
fold :: (v -> a) -> (f -> [a] -> a) -> Term f v -> a
fold :: forall v a f. (v -> a) -> (f -> [a] -> a) -> Term f v -> a
fold v -> a
var f -> [a] -> a
fun (Var v
v) = v -> a
var v
v
fold v -> a
var f -> [a] -> a
fun (Fun f
f [Term f v]
ts) = f -> [a] -> a
fun f
f ((Term f v -> a) -> [Term f v] -> [a]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((v -> a) -> (f -> [a] -> a) -> Term f v -> a
forall v a f. (v -> a) -> (f -> [a] -> a) -> Term f v -> a
fold v -> a
var f -> [a] -> a
fun) [Term f v]
ts)

-- | Mapping terms: Rename function symbols and variables.
--
-- >>> map succ pred (Fun 'f' [Var 2, Fun 'g' []])
-- Fun 'e' [Var 3,Fun 'f' []]
map :: (f -> f') -> (v -> v') -> Term f v -> Term f' v'
map :: forall f f' v v'. (f -> f') -> (v -> v') -> Term f v -> Term f' v'
map f -> f'
fun v -> v'
var = (v -> Term f' v')
-> (f -> [Term f' v'] -> Term f' v') -> Term f v -> Term f' v'
forall v a f. (v -> a) -> (f -> [a] -> a) -> Term f v -> a
fold (v' -> Term f' v'
forall f v. v -> Term f v
Var (v' -> Term f' v') -> (v -> v') -> v -> Term f' v'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> v'
var) (f' -> [Term f' v'] -> Term f' v'
forall f v. f -> [Term f v] -> Term f v
Fun (f' -> [Term f' v'] -> Term f' v')
-> (f -> f') -> f -> [Term f' v'] -> Term f' v'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f -> f'
fun)