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

module Language.REST.Internal.Rewrite where

import GHC.Generics (Generic)

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


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
/= :: Rewrite -> Rewrite -> Bool
$c/= :: Rewrite -> Rewrite -> Bool
== :: Rewrite -> Rewrite -> Bool
$c== :: 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
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
$cp1Ord :: Eq 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
$cto :: forall x. Rep Rewrite x -> Rewrite
$cfrom :: forall x. Rewrite -> Rep Rewrite x
Generic, Int -> Rewrite -> Int
Rewrite -> Int
(Int -> Rewrite -> Int) -> (Rewrite -> Int) -> Hashable Rewrite
forall 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 -> ShowS
[Rewrite] -> ShowS
Rewrite -> String
(Int -> Rewrite -> ShowS)
-> (Rewrite -> String) -> ([Rewrite] -> ShowS) -> Show Rewrite
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rewrite] -> ShowS
$cshowList :: [Rewrite] -> ShowS
show :: Rewrite -> String
$cshow :: Rewrite -> String
showsPrec :: Int -> Rewrite -> ShowS
$cshowsPrec :: Int -> Rewrite -> ShowS
Show)

type Subst = M.HashMap String RuntimeTerm

getName :: Rewrite -> Maybe String
getName :: Rewrite -> Maybe String
getName (Rewrite MetaTerm
_t MetaTerm
_u Maybe String
n) = Maybe String
n

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 :: 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 -> ShowS
forall r. PrintfType r => String -> r
printf String
"No value for metavar %s during subst %s" (ShowS
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 :: 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 | 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
== Maybe RuntimeTerm
forall a. Maybe a
Nothing
  = 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 (t :: * -> *) a. Foldable t => t a -> Int
length [MetaTerm]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [RuntimeTerm] -> 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 (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, Hashable 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)
_        | Bool
otherwise                        = HashSet a
forall a. HashSet a
S.empty