-- 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

module Data.Rewriting.Context.Type (
    Ctxt (..),
) where

import Data.Rewriting.Term (Term(..))

data Ctxt f v
    = Hole                                    -- ^ Hole
    | Ctxt f [Term f v] (Ctxt f v) [Term f v] -- ^ Non-empty context

    -- CS: would it make sense to reverse the left term list?
    deriving (Int -> Ctxt f v -> ShowS
[Ctxt f v] -> ShowS
Ctxt f v -> String
(Int -> Ctxt f v -> ShowS)
-> (Ctxt f v -> String) -> ([Ctxt f v] -> ShowS) -> Show (Ctxt f v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f v. (Show f, Show v) => Int -> Ctxt f v -> ShowS
forall f v. (Show f, Show v) => [Ctxt f v] -> ShowS
forall f v. (Show f, Show v) => Ctxt f v -> String
$cshowsPrec :: forall f v. (Show f, Show v) => Int -> Ctxt f v -> ShowS
showsPrec :: Int -> Ctxt f v -> ShowS
$cshow :: forall f v. (Show f, Show v) => Ctxt f v -> String
show :: Ctxt f v -> String
$cshowList :: forall f v. (Show f, Show v) => [Ctxt f v] -> ShowS
showList :: [Ctxt f v] -> ShowS
Show, Ctxt f v -> Ctxt f v -> Bool
(Ctxt f v -> Ctxt f v -> Bool)
-> (Ctxt f v -> Ctxt f v -> Bool) -> Eq (Ctxt f v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f v. (Eq f, Eq v) => Ctxt f v -> Ctxt f v -> Bool
$c== :: forall f v. (Eq f, Eq v) => Ctxt f v -> Ctxt f v -> Bool
== :: Ctxt f v -> Ctxt f v -> Bool
$c/= :: forall f v. (Eq f, Eq v) => Ctxt f v -> Ctxt f v -> Bool
/= :: Ctxt f v -> Ctxt f v -> Bool
Eq, Eq (Ctxt f v)
Eq (Ctxt f v) =>
(Ctxt f v -> Ctxt f v -> Ordering)
-> (Ctxt f v -> Ctxt f v -> Bool)
-> (Ctxt f v -> Ctxt f v -> Bool)
-> (Ctxt f v -> Ctxt f v -> Bool)
-> (Ctxt f v -> Ctxt f v -> Bool)
-> (Ctxt f v -> Ctxt f v -> Ctxt f v)
-> (Ctxt f v -> Ctxt f v -> Ctxt f v)
-> Ord (Ctxt f v)
Ctxt f v -> Ctxt f v -> Bool
Ctxt f v -> Ctxt f v -> Ordering
Ctxt f v -> Ctxt f v -> Ctxt f v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f v. (Ord f, Ord v) => Eq (Ctxt f v)
forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Bool
forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Ordering
forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Ctxt f v
$ccompare :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Ordering
compare :: Ctxt f v -> Ctxt f v -> Ordering
$c< :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Bool
< :: Ctxt f v -> Ctxt f v -> Bool
$c<= :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Bool
<= :: Ctxt f v -> Ctxt f v -> Bool
$c> :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Bool
> :: Ctxt f v -> Ctxt f v -> Bool
$c>= :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Bool
>= :: Ctxt f v -> Ctxt f v -> Bool
$cmax :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Ctxt f v
max :: Ctxt f v -> Ctxt f v -> Ctxt f v
$cmin :: forall f v. (Ord f, Ord v) => Ctxt f v -> Ctxt f v -> Ctxt f v
min :: Ctxt f v -> Ctxt f v -> Ctxt f v
Ord)