Term.curry 7.74 KB
Newer Older
1 2 3 4 5 6 7 8
------------------------------------------------------------------------------
--- 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
9
--- @version November 2018
10 11 12 13 14 15 16 17 18 19 20
--- @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

21 22 23
import Char      ( isAlphaNum )
import List      ( nub, intercalate, maximum, minimum )
import Maybe     ( fromMaybe )
24

Michael Hanus 's avatar
Michael Hanus committed
25 26
import Data.FiniteMap ( listToFM, lookupFM )

27 28 29 30 31 32 33 34 35 36 37 38 39 40
-- ---------------------------------------------------------------------------
-- 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]
Michael Hanus 's avatar
Michael Hanus committed
41
 deriving (Eq, Show)
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

--- 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
68 69 70 71 72 73 74 75 76 77 78
    showTerm' b (TermCons c ts) = case ts of
      []     -> cstr
      [l, r] -> if any isAlphaNum cstr
                  then prefixString -- no infix notation
                  else parensIf b (showTerm' True l ++ " " ++ cstr ++ " " ++
                                   showTerm' True r)
      _      -> prefixString
     where
      cstr         = s c
      prefixString = cstr ++ "("
                          ++ intercalate "," (map (showTerm' False) ts) ++ ")"
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

--- 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.
Michael Hanus 's avatar
Michael Hanus committed
107
tCons :: Eq f => Term f -> [f]
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
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.
Michael Hanus 's avatar
Michael Hanus committed
187
eqConsPattern :: Eq f => Term f -> Term f -> Bool
188 189 190 191 192 193 194 195 196 197 198 199 200 201
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.
Michael Hanus 's avatar
Michael Hanus committed
202
unique :: Eq a => [a] -> Bool
203 204
unique []                    = True
unique (x:xs) | notElem x xs = unique xs
Michael Hanus 's avatar
Michael Hanus committed
205
              | otherwise    = False