-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Christian Sternagel, Bertram Felgenhauer, Martin Avanzini

module Data.Rewriting.Pos (
    Pos,
    -- * Comparing Positions
    -- | Note that positions are not totally ordered. Nevertheless there are
    -- some commonly useful comparisons between positions.
    above,
    below,
    parallelTo,
    leftOf,
    rightOf,
) where

import Data.Rewriting.Utils
import Data.List

-- | A position in a term. Arguments are counted from 0.
--
-- A position describes a path in the tree representation of a term. The empty
-- position @[]@ denotes the root of the term. A position @[0,1]@ denotes the
-- 2nd child of the 1st child of the root (counting children from left to
-- right).
type Pos = [Int]

-- | @p \`above\` q@ checks whether @p@ is above @q@ (in the tree representation of
-- a term). A position @p@ is above a position @q@, whenever @p@ is a prefix of
-- @q@.
above :: Pos -> Pos -> Bool
above :: Pos -> Pos -> Bool
above = Pos -> Pos -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf

-- | @p \`below\` q@ checks whether @p@ is below @q@, that is to say that @q@ is
-- above @p@.
below :: Pos -> Pos -> Bool
below :: Pos -> Pos -> Bool
below = (Pos -> Pos -> Bool) -> Pos -> Pos -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip Pos -> Pos -> Bool
above

-- | @p \`parallelTo\` q@ checks whether @p@ is parallel to @q@, that is to say
-- that @p@ and @q@ do not lie on the same path.
parallelTo :: Pos -> Pos -> Bool
parallelTo :: Pos -> Pos -> Bool
parallelTo Pos
p Pos
q = Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
p') Bool -> Bool -> Bool
&& Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
q') where
    (Pos
p', Pos
q') = Pos -> Pos -> (Pos, Pos)
forall a. Ord a => [a] -> [a] -> ([a], [a])
dropCommonPrefix Pos
p Pos
q

-- | @p \`leftOf\` q@ checks whether @p@ is left of @q@. This is only possible if
-- @p@ and @q@ do not lie on the same path (i.e., are parallel to each other).
leftOf :: Pos -> Pos -> Bool
leftOf :: Pos -> Pos -> Bool
leftOf Pos
p Pos
q = Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
p') Bool -> Bool -> Bool
&& Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
q') Bool -> Bool -> Bool
&& Pos -> Int
forall a. HasCallStack => [a] -> a
head Pos
p' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Pos -> Int
forall a. HasCallStack => [a] -> a
head Pos
q' where
    (Pos
p', Pos
q') = Pos -> Pos -> (Pos, Pos)
forall a. Ord a => [a] -> [a] -> ([a], [a])
dropCommonPrefix Pos
p Pos
q

-- | @p \`rightOf\` q@ checks whether @p@ is right of @q@.
rightOf :: Pos -> Pos -> Bool
rightOf :: Pos -> Pos -> Bool
rightOf Pos
p Pos
q = Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
p') Bool -> Bool -> Bool
&& Bool -> Bool
not (Pos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Pos
q') Bool -> Bool -> Bool
&& Pos -> Int
forall a. HasCallStack => [a] -> a
head Pos
p' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Pos -> Int
forall a. HasCallStack => [a] -> a
head Pos
q' where
    (Pos
p', Pos
q') = Pos -> Pos -> (Pos, Pos)
forall a. Ord a => [a] -> [a] -> ([a], [a])
dropCommonPrefix Pos
p Pos
q

-- reference implementations
parallelToRef :: Pos -> Pos -> Bool
parallelToRef :: Pos -> Pos -> Bool
parallelToRef Pos
p Pos
q = Bool -> Bool
not (Pos
p Pos -> Pos -> Bool
`above` Pos
q) Bool -> Bool -> Bool
&& Bool -> Bool
not (Pos
p Pos -> Pos -> Bool
`below` Pos
q)