{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ImplicitParams #-}

module Language.REST.Core where

import Prelude hiding (GT, EQ)

import           Debug.Trace                    ( trace )
import qualified Data.List                     as L
import qualified Data.HashSet                      as S

import           Language.REST.OCAlgebra
import           Language.REST.Types
import qualified Language.REST.MetaTerm as MT
import           Language.REST.Internal.Rewrite
import           Language.REST.RuntimeTerm as RT
import           Language.REST.RewriteRule

type MetaTerm = MT.MetaTerm


contains :: RuntimeTerm -> RuntimeTerm -> Bool
contains :: RuntimeTerm -> RuntimeTerm -> Bool
contains RuntimeTerm
t1 RuntimeTerm
t2 | RuntimeTerm
t1 RuntimeTerm -> RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm
t2 = Bool
True
contains (App Op
_ [RuntimeTerm]
ts) RuntimeTerm
t     = (RuntimeTerm -> Bool) -> [RuntimeTerm] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (RuntimeTerm -> RuntimeTerm -> Bool
contains RuntimeTerm
t) [RuntimeTerm]
ts


orient' :: Show oc => (?impl :: OCAlgebra oc RuntimeTerm m) => oc -> [RuntimeTerm] -> oc
orient' :: oc -> [RuntimeTerm] -> oc
orient' oc
oc0 [RuntimeTerm]
ts0 = oc -> [(RuntimeTerm, RuntimeTerm)] -> oc
forall t a (m :: * -> *).
(?impl::OCAlgebra t a m) =>
t -> [(a, a)] -> t
go oc
oc0 ([RuntimeTerm] -> [RuntimeTerm] -> [(RuntimeTerm, RuntimeTerm)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RuntimeTerm]
ts0 ([RuntimeTerm] -> [RuntimeTerm]
forall a. [a] -> [a]
tail [RuntimeTerm]
ts0))
  where
    go :: t -> [(a, a)] -> t
go t
oc []            = t
oc
    go t
oc ((a
t0, a
t1):[(a, a)]
ts) = t -> [(a, a)] -> t
go (OCAlgebra t a m -> t -> a -> a -> t
forall c a (m :: * -> *). OCAlgebra c a m -> c -> a -> a -> c
refine ?impl::OCAlgebra t a m
OCAlgebra t a m
?impl t
oc a
t0 a
t1) [(a, a)]
ts

orient :: Show oc =>  OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
orient :: OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
orient OCAlgebra oc RuntimeTerm m
impl = oc -> [RuntimeTerm] -> oc
forall oc (m :: * -> *).
(Show oc, ?impl::OCAlgebra oc RuntimeTerm m) =>
oc -> [RuntimeTerm] -> oc
orient' (OCAlgebra oc RuntimeTerm m -> oc
forall c a (m :: * -> *). OCAlgebra c a m -> c
top OCAlgebra oc RuntimeTerm m
impl)
   where
     ?impl = impl

canOrient :: forall oc m . Show oc
  => (?impl :: OCAlgebra oc RuntimeTerm m) => [RuntimeTerm] -> m Bool
canOrient :: [RuntimeTerm] -> m Bool
canOrient [RuntimeTerm]
terms = String -> m Bool -> m Bool
forall a. String -> a -> a
trace (String
"Try to orient " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [RuntimeTerm] -> String
termPathStr [RuntimeTerm]
terms) (m Bool -> m Bool) -> m Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ OCAlgebra oc RuntimeTerm m -> oc -> m Bool
forall c a (m :: * -> *). OCAlgebra c a m -> c -> m Bool
isSat ?impl::OCAlgebra oc RuntimeTerm m
OCAlgebra oc RuntimeTerm m
?impl (OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
forall oc (m :: * -> *).
Show oc =>
OCAlgebra oc RuntimeTerm m -> [RuntimeTerm] -> oc
orient ?impl::OCAlgebra oc RuntimeTerm m
OCAlgebra oc RuntimeTerm m
?impl [RuntimeTerm]
terms)

syms :: MetaTerm -> S.HashSet String
syms :: MetaTerm -> HashSet String
syms (MT.Var String
s)      = String -> HashSet String
forall a. Hashable a => a -> HashSet a
S.singleton String
s
syms (MT.RWApp Op
_ [MetaTerm]
xs) = [HashSet String] -> HashSet String
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions ((MetaTerm -> HashSet String) -> [MetaTerm] -> [HashSet String]
forall a b. (a -> b) -> [a] -> [b]
map MetaTerm -> HashSet String
syms [MetaTerm]
xs)

termPathStr :: [RuntimeTerm] -> String
termPathStr :: [RuntimeTerm] -> String
termPathStr [RuntimeTerm]
terms = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
" --> \n" ((RuntimeTerm -> String) -> [RuntimeTerm] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> String
pp [RuntimeTerm]
terms)
  where
    pp :: RuntimeTerm -> String
pp = PPArgs -> RuntimeTerm -> String
forall a. ToMetaTerm a => PPArgs -> a -> String
prettyPrint ([(Text, Text)]
-> [(Text, Text)] -> (MetaTerm -> Maybe Text) -> PPArgs
PPArgs [] [] (Maybe Text -> MetaTerm -> Maybe Text
forall a b. a -> b -> a
const Maybe Text
forall a. Maybe a
Nothing))

eval :: S.HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm
eval :: HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm
eval HashSet Rewrite
rws RuntimeTerm
t0 =
  do
    [HashSet RuntimeTerm]
result <- (Rewrite -> IO (HashSet RuntimeTerm))
-> [Rewrite] -> IO [HashSet RuntimeTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (RuntimeTerm -> Rewrite -> IO (HashSet RuntimeTerm)
forall (m :: * -> *) rule term.
RewriteRule m rule term =>
term -> rule -> m (HashSet term)
apply RuntimeTerm
t0) (HashSet Rewrite -> [Rewrite]
forall a. HashSet a -> [a]
S.toList HashSet Rewrite
rws)
    case HashSet RuntimeTerm -> [RuntimeTerm]
forall a. HashSet a -> [a]
S.toList (HashSet RuntimeTerm -> [RuntimeTerm])
-> HashSet RuntimeTerm -> [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]
result of
      []      -> RuntimeTerm -> IO RuntimeTerm
forall (m :: * -> *) a. Monad m => a -> m a
return RuntimeTerm
t0
      (RuntimeTerm
t : [RuntimeTerm]
_) -> HashSet Rewrite -> RuntimeTerm -> IO RuntimeTerm
eval HashSet Rewrite
rws RuntimeTerm
t