1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198

------------------------------------------------------------------------------
--- Library for representation of first-order terms.
---
--- This library is the basis of other libraries for the manipulation of
--- first-order terms, e.g., unification of terms. Therefore, this library
--- also defines other structures, like term equations.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------

module Rewriting.Term
  ( VarIdx, Term (..), TermEq, TermEqs
  , showVarIdx, showTerm, showTermEq, showTermEqs, tConst, tOp, tRoot, tCons
  , tConsAll, tVars, tVarsAll, isConsTerm, isVarTerm, isGround, isLinear
  , isNormal, maxVarInTerm, minVarInTerm, normalizeTerm, renameTermVars
  , mapTerm, eqConsPattern
  ) where

import FiniteMap (listToFM, lookupFM)
import List (nub, intercalate, maximum, minimum)
import Maybe (fromMaybe)

-- ---------------------------------------------------------------------------
-- Representation of first-order terms and term equations
-- ---------------------------------------------------------------------------

--- A variable represented as an integer greater than or equal to zero.
type VarIdx = Int

--- Representation of a first-order term, parameterized over the kind of
--- function symbols, e.g., strings.
---
--- @cons TermVar v     - The variable term with variable `v`.
--- @cons TermCons c ts - The constructor term with constructor `c` and
---                       argument terms `ts`.
data Term f = TermVar VarIdx | TermCons f [Term f]

--- A term equation represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type TermEq f = (Term f, Term f)

--- Multiple term equations represented as a list of term equations and
--- parameterized over the kind of function symbols, e.g., strings.
type TermEqs f = [TermEq f]

-- ---------------------------------------------------------------------------
-- Pretty-printing of first-order terms and term equations
-- ---------------------------------------------------------------------------

--- Transforms a variable into a string representation.
showVarIdx :: VarIdx -> String
showVarIdx v | v >= 0    = if q == 0 then [c] else c:(show q)
             | otherwise = ""
  where
    (q, r) = divMod v 26
    c = "abcdefghijklmnopqrstuvwxyz" !! r

--- Transforms a term into a string representation.
showTerm :: (f -> String) -> Term f -> String
showTerm s = showTerm' False
  where
    showTerm' _ (TermVar v)     = showVarIdx v
    showTerm' b (TermCons c ts)
      = case ts of
          []     -> s c
          [l, r] -> parensIf b ((showTerm' True l) ++ " " ++ (s c) ++ " "
                      ++ (showTerm' True r))
          _      -> (s c) ++ "("
                      ++ (intercalate "," (map (showTerm' False) ts)) ++ ")"

--- Transforms a term equation into a string representation.
showTermEq :: (f -> String) -> TermEq f -> String
showTermEq s (l, r) = (showTerm s l) ++ " = " ++ (showTerm s r)

--- Transforms a list of term equations into a string representation.
showTermEqs :: (f -> String) -> TermEqs f -> String
showTermEqs s = unlines . (map (showTermEq s))

-- ---------------------------------------------------------------------------
-- Functions for first-order terms
-- ---------------------------------------------------------------------------

--- Returns a term with the given constructor and no argument terms.
tConst :: f -> Term f
tConst c = TermCons c []

--- Returns an infix operator term with the given constructor and the given
--- left and right argument term.
tOp :: Term f -> f -> Term f -> Term f
tOp l c r = TermCons c [l, r]

--- Returns the root symbol (variable or constructor) of a term.
tRoot :: Term f -> Either VarIdx f
tRoot (TermVar v)    = Left v
tRoot (TermCons c _) = Right c

--- Returns a list without duplicates of all constructors in a term.
tCons :: Term f -> [f]
tCons = nub . tConsAll

--- Returns a list of all constructors in a term. The resulting list may
--- contain duplicates.
tConsAll :: Term f -> [f]
tConsAll (TermVar _)     = []
tConsAll (TermCons c ts) = c:(concatMap tConsAll ts)

--- Returns a list without duplicates of all variables in a term.
tVars :: Term _ -> [VarIdx]
tVars = nub . tVarsAll

--- Returns a list of all variables in a term. The resulting list may contain
--- duplicates.
tVarsAll :: Term _ -> [VarIdx]
tVarsAll (TermVar v)     = [v]
tVarsAll (TermCons _ ts) = concatMap tVarsAll ts

--- Checks whether a term is a constructor term.
isConsTerm :: Term _ -> Bool
isConsTerm (TermVar _)    = False
isConsTerm (TermCons _ _) = True

--- Checks whether a term is a variable term.
isVarTerm :: Term _ -> Bool
isVarTerm = not . isConsTerm

--- Checks whether a term is a ground term (contains no variables).
isGround :: Term _ -> Bool
isGround = null . tVarsAll

--- Checks whether a term is linear (contains no variable more than once).
isLinear :: Term _ -> Bool
isLinear = unique . tVarsAll

--- Checks whether a term is normal (behind a variable is not a constructor).
isNormal :: Term _ -> Bool
isNormal (TermVar _)         = True
isNormal (TermCons _ [])     = True
isNormal (TermCons c (t:ts))
  = case t of
      (TermVar _)    -> all isVarTerm ts
      (TermCons _ _) -> (isNormal t) && (isNormal (TermCons c ts))

--- Returns the maximum variable in a term or `Nothing` if no variable exists.
maxVarInTerm :: Term _ -> Maybe VarIdx
maxVarInTerm t = case tVars t of
                   []       -> Nothing
                   vs@(_:_) -> Just (maximum vs)

--- Returns the minimum variable in a term or `Nothing` if no variable exists.
minVarInTerm :: Term _ -> Maybe VarIdx
minVarInTerm t = case tVars t of
                   []       -> Nothing
                   vs@(_:_) -> Just (minimum vs)

--- Normalizes a term by renaming all variables with an increasing order,
--- starting from the minimum possible variable.
normalizeTerm :: Term f -> Term f
normalizeTerm t = normalize t
  where
    sub = listToFM (<) (zip (tVars t) (map TermVar [0..]))

    normalize t'@(TermVar v)  = fromMaybe t' (lookupFM sub v)
    normalize (TermCons c ts) = TermCons c (map normalize ts)

--- Renames the variables in a term by the given number.
renameTermVars :: Int -> Term f -> Term f
renameTermVars i (TermVar v)     = TermVar (v + i)
renameTermVars i (TermCons c ts) = TermCons c (map (renameTermVars i) ts)

--- Transforms a term by applying a transformation on all constructors.
mapTerm :: (a -> b) -> Term a -> Term b
mapTerm _ (TermVar v)     = TermVar v
mapTerm f (TermCons c ts) = TermCons (f c) (map (mapTerm f) ts)

--- Checks whether the constructor pattern of the first term is equal to the
--- constructor pattern of the second term. Returns `True` if both terms have
--- the same constructor and the same arity.
eqConsPattern :: Term f -> Term f -> Bool
eqConsPattern (TermVar _)       _                 = False
eqConsPattern (TermCons _ _)    (TermVar _)       = False
eqConsPattern (TermCons c1 ts1) (TermCons c2 ts2) =
  c1 == c2 && length ts1 == length ts2

-- ---------------------------------------------------------------------------
-- Definition of helper functions
-- ---------------------------------------------------------------------------

--- Encloses a string in parenthesis if the given condition is true.
parensIf :: Bool -> String -> String
parensIf b s = if b then "(" ++ s ++ ")" else s

--- Checks whether a list contains no element more than once.
unique :: [_] -> Bool
unique []                    = True
unique (x:xs) | notElem x xs = unique xs
              | otherwise    = False