{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Language.REST.Internal.Rewrite
  ( Rewrite(..)
  , Subst
  , named
  , subst
  , unify
  ) where

import GHC.Generics (Generic)

import           Data.Maybe (isNothing)
import           Data.Hashable
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import           Text.Printf

import Language.REST.RewriteRule
import Language.REST.MetaTerm as MT
import Language.REST.RuntimeTerm


-- | @Rewrite t u s@ defines a rewrite rule \( t \rightarrow u \), with
--   an optional name @s@.
data Rewrite = Rewrite MetaTerm MetaTerm (Maybe String)
  deriving (Rewrite -> Rewrite -> Bool
(Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool) -> Eq Rewrite
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
/= :: Rewrite -> Rewrite -> Bool
Eq, Eq Rewrite
Eq Rewrite =>
(Rewrite -> Rewrite -> Ordering)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Bool)
-> (Rewrite -> Rewrite -> Rewrite)
-> (Rewrite -> Rewrite -> Rewrite)
-> Ord Rewrite
Rewrite -> Rewrite -> Bool
Rewrite -> Rewrite -> Ordering
Rewrite -> Rewrite -> Rewrite
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
$ccompare :: Rewrite -> Rewrite -> Ordering
compare :: Rewrite -> Rewrite -> Ordering
$c< :: Rewrite -> Rewrite -> Bool
< :: Rewrite -> Rewrite -> Bool
$c<= :: Rewrite -> Rewrite -> Bool
<= :: Rewrite -> Rewrite -> Bool
$c> :: Rewrite -> Rewrite -> Bool
> :: Rewrite -> Rewrite -> Bool
$c>= :: Rewrite -> Rewrite -> Bool
>= :: Rewrite -> Rewrite -> Bool
$cmax :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
min :: Rewrite -> Rewrite -> Rewrite
Ord, (forall x. Rewrite -> Rep Rewrite x)
-> (forall x. Rep Rewrite x -> Rewrite) -> Generic Rewrite
forall x. Rep Rewrite x -> Rewrite
forall x. Rewrite -> Rep Rewrite x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Rewrite -> Rep Rewrite x
from :: forall x. Rewrite -> Rep Rewrite x
$cto :: forall x. Rep Rewrite x -> Rewrite
to :: forall x. Rep Rewrite x -> Rewrite
Generic, Eq Rewrite
Eq Rewrite =>
(Int -> Rewrite -> Int) -> (Rewrite -> Int) -> Hashable Rewrite
Int -> Rewrite -> Int
Rewrite -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Rewrite -> Int
hashWithSalt :: Int -> Rewrite -> Int
$chash :: Rewrite -> Int
hash :: Rewrite -> Int
Hashable, Int -> Rewrite -> String -> String
[Rewrite] -> String -> String
Rewrite -> String
(Int -> Rewrite -> String -> String)
-> (Rewrite -> String)
-> ([Rewrite] -> String -> String)
-> Show Rewrite
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> Rewrite -> String -> String
showsPrec :: Int -> Rewrite -> String -> String
$cshow :: Rewrite -> String
show :: Rewrite -> String
$cshowList :: [Rewrite] -> String -> String
showList :: [Rewrite] -> String -> String
Show)

-- | 'Subst' is a mapping from variable names to 'RuntimeTerm's.
--   Normally this would be generated by unifying the left-hand-side of
--   a 'Rewrite' with a term.
type Subst = M.HashMap String RuntimeTerm

-- | @named r n@ assigns the name @n@ to rule @r@, replacing any
--   existing name
named :: Rewrite -> String -> Rewrite
named :: Rewrite -> String -> Rewrite
named (Rewrite MetaTerm
t MetaTerm
u Maybe String
_) String
n = MetaTerm -> MetaTerm -> Maybe String -> Rewrite
Rewrite MetaTerm
t MetaTerm
u (String -> Maybe String
forall a. a -> Maybe a
Just String
n)

-- | @subst s m@ replaces the variables in the 'MetaTerm' @m@ with 'RuntimeTerm's
--   in the substitution 's'. This function returns an error if any variables in 'm'
--   do not have a substituion
subst :: Subst -> MetaTerm -> RuntimeTerm
subst :: Subst -> MetaTerm -> RuntimeTerm
subst Subst
s (MT.Var String
v)  | Just RuntimeTerm
t <- String -> Subst -> Maybe RuntimeTerm
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
v Subst
s = RuntimeTerm
t
                    | Bool
otherwise
                    = String -> RuntimeTerm
forall a. HasCallStack => String -> a
error (String -> RuntimeTerm) -> String -> RuntimeTerm
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"No value for metavar %s during subst %s" (String -> String
forall a. Show a => a -> String
show String
v) (Subst -> String
forall a. Show a => a -> String
show Subst
s)
subst Subst
s (MT.RWApp Op
op [MetaTerm]
xs) = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
op ((MetaTerm -> RuntimeTerm) -> [MetaTerm] -> [RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> MetaTerm -> RuntimeTerm
subst Subst
s) [MetaTerm]
xs)

unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst
unifyAll :: Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst
unifyAll Subst
su [] = Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
su
unifyAll Subst
su ((MetaTerm
x, RuntimeTerm
y) : [(MetaTerm, RuntimeTerm)]
ts)
  | Just Subst
s <- MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
unify MetaTerm
x RuntimeTerm
y Subst
su
  = Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst
unifyAll Subst
s [(MetaTerm, RuntimeTerm)]
ts
  | Bool
otherwise
  = Maybe Subst
forall a. Maybe a
Nothing

-- | @unify m r su@ extends the substitution @su@ to generate a new
--   substitution that unifies @m@ and @r@. Returns 'Nothing' if su
--   cannot be extended to unify the terms.
unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
unify :: MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
unify (MT.Var String
s) RuntimeTerm
term Subst
su | String -> Subst -> Maybe RuntimeTerm
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
s Subst
su Maybe RuntimeTerm -> Maybe RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm -> Maybe RuntimeTerm
forall a. a -> Maybe a
Just RuntimeTerm
term
  = Subst -> Maybe Subst
forall a. a -> Maybe a
Just Subst
su
unify (MT.Var String
s) RuntimeTerm
term Subst
su | Maybe RuntimeTerm -> Bool
forall a. Maybe a -> Bool
isNothing (String -> Subst -> Maybe RuntimeTerm
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
s Subst
su)
  = Subst -> Maybe Subst
forall a. a -> Maybe a
Just (Subst -> Maybe Subst) -> Subst -> Maybe Subst
forall a b. (a -> b) -> a -> b
$ String -> RuntimeTerm -> Subst -> Subst
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert String
s RuntimeTerm
term Subst
su
unify (MT.RWApp Op
o1 [MetaTerm]
xs) (App Op
o2 [RuntimeTerm]
ys) Subst
su | Op
o1 Op -> Op -> Bool
forall a. Eq a => a -> a -> Bool
== Op
o2 Bool -> Bool -> Bool
&& [MetaTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [MetaTerm]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RuntimeTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
ys =
  Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst
unifyAll Subst
su ([MetaTerm] -> [RuntimeTerm] -> [(MetaTerm, RuntimeTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [MetaTerm]
xs [RuntimeTerm]
ys)
unify MetaTerm
_ RuntimeTerm
_ Subst
_ = Maybe Subst
forall a. Maybe a
Nothing

instance Monad m => RewriteRule m Rewrite RuntimeTerm where
  apply :: RuntimeTerm -> Rewrite -> m (HashSet RuntimeTerm)
apply RuntimeTerm
t (Rewrite MetaTerm
left MetaTerm
right Maybe String
_) = HashSet RuntimeTerm -> m (HashSet RuntimeTerm)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (HashSet RuntimeTerm -> m (HashSet RuntimeTerm))
-> HashSet RuntimeTerm -> m (HashSet RuntimeTerm)
forall a b. (a -> b) -> a -> b
$ [HashSet RuntimeTerm] -> HashSet RuntimeTerm
forall a. Eq a => [HashSet a] -> HashSet a
S.unions ([HashSet RuntimeTerm] -> HashSet RuntimeTerm)
-> [HashSet RuntimeTerm] -> HashSet RuntimeTerm
forall a b. (a -> b) -> a -> b
$ ((RuntimeTerm, RuntimeTerm -> RuntimeTerm) -> HashSet RuntimeTerm)
-> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
-> [HashSet RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map (RuntimeTerm, RuntimeTerm -> RuntimeTerm) -> HashSet RuntimeTerm
forall {a}.
Hashable a =>
(RuntimeTerm, RuntimeTerm -> a) -> HashSet a
go (RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
subTerms RuntimeTerm
t)
    where
      go :: (RuntimeTerm, RuntimeTerm -> a) -> HashSet a
go (RuntimeTerm
t', RuntimeTerm -> a
tf) | Just Subst
su <- MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
unify MetaTerm
left RuntimeTerm
t' Subst
forall k v. HashMap k v
M.empty = a -> HashSet a
forall a. Hashable a => a -> HashSet a
S.singleton (RuntimeTerm -> a
tf (RuntimeTerm -> a) -> RuntimeTerm -> a
forall a b. (a -> b) -> a -> b
$ Subst -> MetaTerm -> RuntimeTerm
subst Subst
su MetaTerm
right)
      go (RuntimeTerm, RuntimeTerm -> a)
_                                = HashSet a
forall a. HashSet a
S.empty