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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225

------------------------------------------------------------------------------
--- Library for representation and computation of reductions on first-order
--- terms and representation of reduction strategies.
---
--- @author Jan-Hendrik Matthes
--- @version February 2020
------------------------------------------------------------------------------

module Rewriting.Strategy
  ( RStrategy, Reduction (..)
  , showReduction, redexes, seqRStrategy, parRStrategy, liRStrategy
  , loRStrategy, riRStrategy, roRStrategy, piRStrategy, poRStrategy, reduce
  , reduceL, reduceBy, reduceByL, reduceAt, reduceAtL, reduction, reductionL
  , reductionBy, reductionByL
  ) where

import Data.List (nub, intercalate, groupBy, sortBy, minimumBy)
import Rewriting.Position
import Rewriting.Rules (TRS, renameRuleVars, renameTRSVars)
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, maxVarInTerm)
import Rewriting.Unification (unify)

-- ---------------------------------------------------------------------------
-- Representation of reduction strategies
-- ---------------------------------------------------------------------------

--- A reduction strategy represented as a function that takes a term rewriting
--- system and a term and returns the redex positions where the term should be
--- reduced, parameterized over the kind of function symbols, e.g., strings.
type RStrategy f = TRS f -> Term f -> [Pos]

-- ---------------------------------------------------------------------------
-- Representation of reductions on first-order terms
-- ---------------------------------------------------------------------------

--- Representation of a reduction on first-order terms, parameterized over the
--- kind of function symbols, e.g., strings.
---
--- @cons NormalForm t - The normal form with term `t`.
--- @cons RStep t ps r - The reduction of term `t` at positions `ps` to
---                      reduction `r`.
data Reduction f = NormalForm (Term f) | RStep (Term f) [Pos] (Reduction f)

-- ---------------------------------------------------------------------------
-- Pretty-printing of reductions on first-order terms
-- ---------------------------------------------------------------------------

-- \x2192 = RIGHTWARDS ARROW

--- Transforms a reduction into a string representation.
showReduction :: (f -> String) -> Reduction f -> String
showReduction s (NormalForm t) = showTerm s t
showReduction s (RStep t ps r) =
  showTerm s t ++ "\n\8594"  ++ "[" ++ intercalate "," (map showPos ps) ++ "] "
               ++ showReduction s r

-- ---------------------------------------------------------------------------
-- Functions for definition of reduction strategies
-- ---------------------------------------------------------------------------

--- Returns the redex positions of a term according to the given term
--- rewriting system.
redexes :: Eq f => TRS f -> Term f -> [Pos]
redexes trs t =
  let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTerm t)
   in nub [p | p <- positions t, let tp = t |> p,
               (l, _) <- trs',
               Right sub <- [unify [(l, tp)]],
               tp == applySubst sub l]

--- Returns a sequential reduction strategy according to the given ordering
--- function.
seqRStrategy :: Eq f => (Pos -> Pos -> Ordering) -> RStrategy f
seqRStrategy cmp trs t = case redexes trs t of
                           []       -> []
                           ps@(_:_) -> [minimumBy cmp ps]

--- Returns a parallel reduction strategy according to the given ordering
--- function.
parRStrategy :: Eq f => (Pos -> Pos -> Ordering) -> RStrategy f
parRStrategy cmp trs t = case redexes trs t of
                           []       -> []
                           ps@(_:_) -> head (groupBy g (sortBy s ps))
  where
    g :: Pos -> Pos -> Bool
    g p q = (cmp p q) == EQ
    s :: Pos -> Pos -> Bool
    s p q = (cmp p q) /= GT

-- ---------------------------------------------------------------------------
-- Definition of common reduction strategies
-- ---------------------------------------------------------------------------

--- The leftmost innermost reduction strategy.
liRStrategy :: Eq f => RStrategy f
liRStrategy = seqRStrategy liOrder
  where
    liOrder :: Pos -> Pos -> Ordering
    liOrder p q | p == q     = EQ
                | leftOf p q = LT
                | below p q  = LT
                | otherwise  = GT

--- The leftmost outermost reduction strategy.
loRStrategy :: Eq f => RStrategy f
loRStrategy = seqRStrategy loOrder
  where
    loOrder :: Pos -> Pos -> Ordering
    loOrder p q | p == q     = EQ
                | leftOf p q = LT
                | above p q  = LT
                | otherwise  = GT

--- The rightmost innermost reduction strategy.
riRStrategy :: Eq f => RStrategy f
riRStrategy = seqRStrategy riOrder
  where
    riOrder :: Pos -> Pos -> Ordering
    riOrder p q | p == q      = EQ
                | rightOf p q = LT
                | below p q   = LT
                | otherwise   = GT

--- The rightmost outermost reduction strategy.
roRStrategy :: Eq f => RStrategy f
roRStrategy = seqRStrategy roOrder
  where
    roOrder :: Pos -> Pos -> Ordering
    roOrder p q | p == q      = EQ
                | rightOf p q = LT
                | above p q   = LT
                | otherwise   = GT

--- The parallel innermost reduction strategy.
piRStrategy :: Eq f => RStrategy f
piRStrategy = parRStrategy piOrder
  where
    piOrder :: Pos -> Pos -> Ordering
    piOrder p q | p == q    = EQ
                | below p q = LT
                | above p q = GT
                | otherwise = EQ

--- The parallel outermost reduction strategy.
poRStrategy :: Eq f => RStrategy f
poRStrategy = parRStrategy poOrder
  where
    poOrder :: Pos -> Pos -> Ordering
    poOrder p q | p == q    = EQ
                | above p q = LT
                | below p q = GT
                | otherwise = EQ

-- ---------------------------------------------------------------------------
-- Functions for reductions on first-order terms
-- ---------------------------------------------------------------------------

--- Reduces a term with the given strategy and term rewriting system.
reduce :: Eq f => RStrategy f -> TRS f -> Term f -> Term f
reduce s trs t = case s trs t of
                   []       -> t
                   ps@(_:_) -> reduce s trs (reduceAtL trs ps t)

--- Reduces a term with the given strategy and list of term rewriting systems.
reduceL :: Eq f => RStrategy f -> [TRS f] -> Term f -> Term f
reduceL s trss = reduce s (concat trss)

--- Reduces a term with the given strategy and term rewriting system by the
--- given number of steps.
reduceBy :: Eq f => RStrategy f -> TRS f -> Int -> Term f -> Term f
reduceBy s trs n t | n <= 0    = t
                   | otherwise = case s trs t of
  []       -> t
  ps@(_:_) -> reduceBy s trs (n - 1) (reduceAtL trs ps t)

--- Reduces a term with the given strategy and list of term rewriting systems
--- by the given number of steps.
reduceByL :: Eq f => RStrategy f -> [TRS f] -> Int -> Term f -> Term f
reduceByL s trss = reduceBy s (concat trss)

--- Reduces a term with the given term rewriting system at the given redex
--- position.
reduceAt :: Eq f => TRS f -> Pos -> Term f -> Term f
reduceAt []     _ t = t
reduceAt (x:rs) p t = case unify [(l, tp)] of
  Left _                         -> reduceAt rs p t
  Right s | tp == applySubst s l -> replaceTerm t p (applySubst s r)
          | otherwise            -> reduceAt rs p t
 where
   tp = t |> p
   (l, r) = maybe x (\v -> renameRuleVars (v + 1) x) (maxVarInTerm tp)

--- Reduces a term with the given term rewriting system at the given redex
--- positions.
reduceAtL :: Eq f => TRS f -> [Pos] -> Term f -> Term f
reduceAtL _   []     t = t
reduceAtL trs (p:ps) t = reduceAtL trs ps (reduceAt trs p t)

--- Returns the reduction of a term with the given strategy and term rewriting
--- system.
reduction :: Eq f => RStrategy f -> TRS f -> Term f -> Reduction f
reduction s trs t = case s trs t of
  []       -> NormalForm t
  ps@(_:_) -> RStep t ps (reduction s trs (reduceAtL trs ps t))

--- Returns the reduction of a term with the given strategy and list of term
--- rewriting systems.
reductionL :: Eq f => RStrategy f -> [TRS f] -> Term f -> Reduction f
reductionL s trss = reduction s (concat trss)

--- Returns the reduction of a term with the given strategy, the given term
--- rewriting system and the given number of steps.
reductionBy :: Eq f => RStrategy f -> TRS f -> Int -> Term f -> Reduction f
reductionBy s trs n t
  | n <= 0    = NormalForm t
  | otherwise = case s trs t of
                  []       -> NormalForm t
                  ps@(_:_) -> let t' = reduceAtL trs ps t
                               in RStep t ps (reductionBy s trs (n - 1) t')

--- Returns the reduction of a term with the given strategy, the given list of
--- term rewriting systems and the given number of steps.
reductionByL :: Eq f => RStrategy f -> [TRS f] -> Int -> Term f -> Reduction f
reductionByL s trss = reductionBy s (concat trss)