{-# 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c== :: Rewrite -> Rewrite -> Bool
Eq, Eq 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
min :: Rewrite -> Rewrite -> Rewrite
$cmin :: Rewrite -> Rewrite -> Rewrite
max :: Rewrite -> Rewrite -> Rewrite
$cmax :: Rewrite -> Rewrite -> Rewrite
>= :: Rewrite -> Rewrite -> Bool
$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
compare :: Rewrite -> Rewrite -> Ordering
$ccompare :: Rewrite -> Rewrite -> Ordering
Ord, 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
$cto :: forall x. Rep Rewrite x -> Rewrite
$cfrom :: forall x. Rewrite -> Rep Rewrite x
Generic, Eq Rewrite
Int -> Rewrite -> Int
Rewrite -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Rewrite -> Int
$chash :: Rewrite -> Int
hashWithSalt :: Int -> Rewrite -> Int
$chashWithSalt :: Int -> Rewrite -> Int
Hashable, Int -> Rewrite -> String -> String
[Rewrite] -> String -> String
Rewrite -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Rewrite] -> String -> String
$cshowList :: [Rewrite] -> String -> String
show :: Rewrite -> String
$cshow :: Rewrite -> String
showsPrec :: Int -> Rewrite -> String -> String
$cshowsPrec :: Int -> 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 (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 <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
v Subst
s = RuntimeTerm
t
                    | Bool
otherwise
                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => String -> r
printf String
"No value for metavar %s during subst %s" (forall a. Show a => a -> String
show String
v) (forall a. Show a => a -> String
show Subst
s)
subst Subst
s (MT.RWApp Op
op [MetaTerm]
xs) = Op -> [RuntimeTerm] -> RuntimeTerm
App Op
op (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 [] = 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
  = 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 | forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
s Subst
su forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just RuntimeTerm
term
  = forall a. a -> Maybe a
Just Subst
su
unify (MT.Var String
s) RuntimeTerm
term Subst
su | forall a. Maybe a -> Bool
isNothing (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
s Subst
su)
  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== Op
o2 Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [MetaTerm]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [RuntimeTerm]
ys =
  Subst -> [(MetaTerm, RuntimeTerm)] -> Maybe Subst
unifyAll Subst
su (forall a b. [a] -> [b] -> [(a, b)]
zip [MetaTerm]
xs [RuntimeTerm]
ys)
unify MetaTerm
_ RuntimeTerm
_ 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
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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' forall k v. HashMap k v
M.empty = forall a. Hashable a => a -> HashSet a
S.singleton (RuntimeTerm -> a
tf forall a b. (a -> b) -> a -> b
$ Subst -> MetaTerm -> RuntimeTerm
subst Subst
su MetaTerm
right)
      go (RuntimeTerm, RuntimeTerm -> a)
_                                = forall a. HashSet a
S.empty