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

--------------------------------------------------------------------------------
--- Library for representation of rules and term rewriting systems.
---
--- @author Jan-Hendrik Matthes
--- @version February 2020
--- @category algorithm
--------------------------------------------------------------------------------

module Rewriting.Rules
  ( Rule, TRS
  , showRule, showTRS, rRoot, rCons, rVars, maxVarInRule, minVarInRule
  , maxVarInTRS, minVarInTRS, renameRuleVars, renameTRSVars, normalizeRule
  , normalizeTRS, isVariantOf, isLeftLinear, isLeftNormal, isRedex, isPattern
  , isConsBased, isDemandedAt
  ) where

import Function               (both, on)
import List                   (maximum, minimum, union)
import Maybe                  (mapMaybe)

import Rewriting.Substitution (applySubst, listToSubst)
import Rewriting.Term

-- -----------------------------------------------------------------------------
-- Representation of rules and term rewriting systems
-- -----------------------------------------------------------------------------

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

--- A term rewriting system represented as a list of rules and parameterized
--- over the kind of function symbols, e.g., strings.
type TRS f = [Rule f]

-- -----------------------------------------------------------------------------
-- Pretty-printing of rules and term rewriting systems
-- -----------------------------------------------------------------------------

-- \x2192 = RIGHTWARDS ARROW

--- Transforms a rule into a string representation.
showRule :: (f -> String) -> Rule f -> String
showRule s (l, r) = showTerm s l ++ " \8594 "  ++ showTerm s r

--- Transforms a term rewriting system into a string representation.
showTRS :: (f -> String) -> TRS f -> String
showTRS s = unlines . map (showRule s)

-- -----------------------------------------------------------------------------
-- Functions for rules and term rewriting systems
-- -----------------------------------------------------------------------------

--- Returns the root symbol (variable or constructor) of a rule.
rRoot :: Rule f -> Either VarIdx f
rRoot = tRoot . fst

--- Returns a list without duplicates of all constructors in a rule.
rCons :: Eq f => Rule f -> [f]
rCons (l, r) = union (tCons l) (tCons r)

--- Returns a list without duplicates of all variables in a rule.
rVars :: Rule _ -> [VarIdx]
rVars = tVars . fst

--- Returns the maximum variable in a rule or `Nothing` if no variable exists.
maxVarInRule :: Rule _ -> Maybe VarIdx
maxVarInRule = maxVarInTerm . fst

--- Returns the minimum variable in a rule or `Nothing` if no variable exists.
minVarInRule :: Rule _ -> Maybe VarIdx
minVarInRule = minVarInTerm . fst

--- Returns the maximum variable in a term rewriting system or `Nothing` if no
--- variable exists.
maxVarInTRS :: TRS _ -> Maybe VarIdx
maxVarInTRS trs = case mapMaybe maxVarInRule trs of
                    []       -> Nothing
                    vs@(_:_) -> Just (maximum vs)

--- Returns the minimum variable in a term rewriting system or `Nothing` if no
--- variable exists.
minVarInTRS :: TRS _ -> Maybe VarIdx
minVarInTRS trs = case mapMaybe minVarInRule trs of
                    []       -> Nothing
                    vs@(_:_) -> Just (minimum vs)

--- Renames the variables in a rule by the given number.
renameRuleVars :: Int -> Rule f -> Rule f
renameRuleVars i = both (renameTermVars i)

--- Renames the variables in every rule of a term rewriting system by the given
--- number.
renameTRSVars :: Int -> TRS f -> TRS f
renameTRSVars i = map (renameRuleVars i)

--- Normalizes a rule by renaming all variables with an increasing order,
--- starting from the minimum possible variable.
normalizeRule :: Rule f -> Rule f
normalizeRule r = let sub = listToSubst (zip (rVars r) (map TermVar [0..]))
                   in both (applySubst sub) r

--- Normalizes all rules in a term rewriting system by renaming all variables
--- with an increasing order, starting from the minimum possible variable.
normalizeTRS :: TRS f -> TRS f
normalizeTRS = map normalizeRule

--- Checks whether the first rule is a variant of the second rule.
isVariantOf :: Eq f => Rule f -> Rule f -> Bool
isVariantOf = on (==) normalizeRule

--- Checks whether a term rewriting system is left-linear.
isLeftLinear :: TRS _ -> Bool
isLeftLinear = all (isLinear . fst)

--- Checks whether a term rewriting system is left-normal.
isLeftNormal :: TRS _ -> Bool
isLeftNormal = all (isNormal . fst)

--- Checks whether a term is reducible with some rule of the given term
--- rewriting system.
isRedex :: Eq f => TRS f -> Term f -> Bool
isRedex trs t = any (eqConsPattern t . fst) trs

--- Checks whether a term is a pattern, i.e., a root-reducible term according to
--- the given term rewriting system.
isPattern :: Eq f => TRS f -> Term f -> Bool
isPattern _   (TermVar _)       = False
isPattern trs t@(TermCons _ ts) = isRedex trs t && all isVarOrCons ts
  where
    isVarOrCons (TermVar _)         = True
    isVarOrCons t'@(TermCons _ ts') =
      not (isRedex trs t') && all isVarOrCons ts'

--- Checks whether a term rewriting system is constructor-based.
isConsBased :: Eq f => TRS f -> Bool
isConsBased trs = all (isPattern trs . fst) trs

--- Checks whether the given argument position of a rule is demanded. Returns
--- `True` if the corresponding argument term is a constructor term.
isDemandedAt :: Int -> Rule _ -> Bool
isDemandedAt _ (TermVar _, _)     = False
isDemandedAt i (TermCons _ ts, _) =
  i > 0 && i <= length ts && isConsTerm (ts !! (i - 1))