-- 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.Ops (
    apply,
    compose,
    ofTerm,
) where

import Control.Monad
import Data.Rewriting.Pos
import Data.Rewriting.Term.Type
import Data.Rewriting.Context.Type

-- | Apply a context to a term (i.e., replace the hole in the context by the
-- term).
apply :: Ctxt f v -> Term f v -> Term f v
apply :: forall f v. Ctxt f v -> Term f v -> Term f v
apply Ctxt f v
Hole Term f v
t = Term f v
t
apply (Ctxt f
f [Term f v]
ts1 Ctxt f v
ctxt [Term f v]
ts2) Term f v
t = f -> [Term f v] -> Term f v
forall f v. f -> [Term f v] -> Term f v
Fun f
f ([Term f v]
ts1 [Term f v] -> [Term f v] -> [Term f v]
forall a. [a] -> [a] -> [a]
++ Ctxt f v -> Term f v -> Term f v
forall f v. Ctxt f v -> Term f v -> Term f v
apply Ctxt f v
ctxt Term f v
t Term f v -> [Term f v] -> [Term f v]
forall a. a -> [a] -> [a]
: [Term f v]
ts2)

-- | Compose two contexts (i.e., replace the hole in the left context by the
-- right context).
compose :: Ctxt f v -> Ctxt f v -> Ctxt f v
compose :: forall f v. Ctxt f v -> Ctxt f v -> Ctxt f v
compose Ctxt f v
Hole Ctxt f v
c2 = Ctxt f v
c2
compose (Ctxt f
f [Term f v]
ts1 Ctxt f v
c1 [Term f v]
ts2) Ctxt f v
c2 = f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
forall f v. f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
Ctxt f
f [Term f v]
ts1 (Ctxt f v
c1 Ctxt f v -> Ctxt f v -> Ctxt f v
forall f v. Ctxt f v -> Ctxt f v -> Ctxt f v
`compose` Ctxt f v
c2) [Term f v]
ts2

-- | Create a context from a term by placing the hole at a specific position.
ofTerm :: Term f v -> Pos -> Maybe (Ctxt f v)
ofTerm :: forall f v. Term f v -> Pos -> Maybe (Ctxt f v)
ofTerm Term f v
_ [] = Ctxt f v -> Maybe (Ctxt f v)
forall a. a -> Maybe a
Just Ctxt f v
forall f v. Ctxt f v
Hole
ofTerm (Fun f
f [Term f v]
ts) (Int
i:Pos
p) = do
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Term f v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term f v]
ts)
    let ([Term f v]
ts1, Term f v
t:[Term f v]
ts2) = Int -> [Term f v] -> ([Term f v], [Term f v])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
i [Term f v]
ts
    Ctxt f v
ctxt <- Term f v -> Pos -> Maybe (Ctxt f v)
forall f v. Term f v -> Pos -> Maybe (Ctxt f v)
ofTerm Term f v
t Pos
p
    Ctxt f v -> Maybe (Ctxt f v)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
forall f v. f -> [Term f v] -> Ctxt f v -> [Term f v] -> Ctxt f v
Ctxt f
f [Term f v]
ts1 Ctxt f v
ctxt [Term f v]
ts2)
ofTerm Term f v
_ Pos
_ = Maybe (Ctxt f v)
forall a. Maybe a
Nothing