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

--------------------------------------------------------------------------------
--- Library for representation of positions in first-order terms.
---
--- @author Jan-Hendrik Matthes
--- @version February 2020
--- @category algorithm
--------------------------------------------------------------------------------

module Rewriting.Position
  ( Pos
  , showPos, eps, above, below, leftOf, rightOf, disjoint, positions, (.>), (|>)
  , replaceTerm
  ) where

import List           (intercalate, isPrefixOf)

import Rewriting.Term (Term (..))

-- -----------------------------------------------------------------------------
-- Representation of positions in first-order terms
-- -----------------------------------------------------------------------------

--- A position in a term represented as a list of integers greater than zero.
type Pos = [Int]

-- -----------------------------------------------------------------------------
-- Pretty-printing of positions in first-order terms
-- -----------------------------------------------------------------------------

-- \x00b7 = MIDDLE DOT
-- \x03b5 = GREEK SMALL LETTER EPSILON

--- Transforms a position into a string representation.
showPos :: Pos -> String
showPos []       = "\949"
showPos ps@(_:_) = intercalate "\183"   (map show ps)

-- -----------------------------------------------------------------------------
-- Functions for positions in first-order terms
-- -----------------------------------------------------------------------------

--- The root position of a term.
eps :: Pos
eps = []

--- Checks whether the first position is above the second position.
above :: Pos -> Pos -> Bool
above = isPrefixOf

--- Checks whether the first position is below the second position.
below :: Pos -> Pos -> Bool
below = flip above

--- Checks whether the first position is left from the second position.
leftOf :: Pos -> Pos -> Bool
leftOf []     _      = False
leftOf (_:_)  []     = False
leftOf (p:ps) (q:qs) = case compare p q of
                         LT -> True
                         EQ -> leftOf ps qs
                         GT -> False

--- Checks whether the first position is right from the second position.
rightOf :: Pos -> Pos -> Bool
rightOf = flip leftOf

--- Checks whether two positions are disjoint.
disjoint :: Pos -> Pos -> Bool
disjoint p q = not (above p q || below p q)

--- Returns a list of all positions in a term.
positions :: Term _ -> [Pos]
positions (TermVar _)     = [eps]
positions (TermCons _ ts) = eps:[i:p | (i, t) <- zip [1..] ts, p <- positions t]

--- Concatenates two positions.
(.>) :: Pos -> Pos -> Pos
(.>) = (++)

-- -----------------------------------------------------------------------------
-- Functions for subterm selection and term replacement
-- -----------------------------------------------------------------------------

--- Returns the subterm of a term at the given position if the position exists
--- within the term.
(|>) :: Term f -> Pos -> Term f
t             |> []    = t
TermCons _ ts |> (i:p) = (ts !! (i - 1)) |> p
TermVar _     |> (_:_) = error "(|>): A term variable has no subterms!"

--- Replaces the subterm of a term at the given position with the given term if
--- the position exists within the term.
replaceTerm :: Term f -> Pos -> Term f -> Term f
replaceTerm _                 []    s = s
replaceTerm t@(TermVar _)     (_:_) _ = t
replaceTerm t@(TermCons c ts) (i:p) s
  | i > 0 && i <= length ts           = TermCons c ts'
  | otherwise                         = t
  where
    (ts1, ti:ts2) = splitAt (i - 1) ts
    ts' = ts1 ++ (replaceTerm ti p s : ts2)