------------------------------------------------------------------------------ --- 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 November 2018 --- @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 Char ( isAlphaNum ) import List ( nub, intercalate, maximum, minimum ) import Maybe ( fromMaybe ) import Data.FiniteMap ( listToFM, lookupFM ) -- --------------------------------------------------------------------------- -- 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] deriving (Eq, Show) --- 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 [] -> 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) ++ ")" --- 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 :: Eq f => 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 :: Eq f => 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 :: Eq a => [a] -> Bool unique [] = True unique (x:xs) | notElem x xs = unique xs | otherwise = False