-- |

module Language.REST where

import Control.Monad.Identity
import Data.Hashable
import Data.Maybe
import qualified Data.HashSet as S

import Language.REST.OCAlgebra (OCAlgebra)
import Language.REST.OCToAbstract
import Language.REST.WQOConstraints
import Language.REST.WQOConstraints.ADT (ConstraintsADT, adtOC)
import Language.REST.RPO
import Language.REST.RuntimeTerm
import Language.REST.Op
import Language.REST.Internal.OpOrdering
import qualified Language.REST.Internal.WQO as WQO
import System.IO (Handle)


adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
adtRPO :: (Handle, Handle) -> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
adtRPO (Handle, Handle)
z3 = WQOConstraints ConstraintsADT IO
-> ConstraintGen ConstraintsADT Op RuntimeTerm Identity
-> OCAlgebra (ConstraintsADT Op) RuntimeTerm IO
forall (impl :: * -> *) base lifted (m :: * -> *).
(ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted,
 Show base, Show (impl base)) =>
WQOConstraints impl m
-> ConstraintGen impl base lifted Identity
-> OCAlgebra (impl base) lifted m
lift ((Handle, Handle) -> WQOConstraints ConstraintsADT IO
adtOC (Handle, Handle)
z3) forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
ConstraintGen ConstraintsADT Op RuntimeTerm Identity
rpo
-- lazyRPO = lift lazyOC rpo
-- strictRPO = lift strictOC rpo

-- Assume vars are arity 0, which is usually correct
getVars :: RuntimeTerm -> S.HashSet Op
getVars :: RuntimeTerm -> HashSet Op
getVars (App Op
op []) = Op -> HashSet Op
forall a. Hashable a => a -> HashSet a
S.singleton Op
op
getVars (App Op
_op [RuntimeTerm]
xs) = [HashSet Op] -> HashSet Op
forall a. (Eq a, Hashable a) => [HashSet a] -> HashSet a
S.unions ((RuntimeTerm -> HashSet Op) -> [RuntimeTerm] -> [HashSet Op]
forall a b. (a -> b) -> [a] -> [b]
map RuntimeTerm -> HashSet Op
getVars [RuntimeTerm]
xs)


varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO.WQO Op
varsEQ :: RuntimeTerm -> RuntimeTerm -> WQO Op
varsEQ RuntimeTerm
t1 RuntimeTerm
t2 =
  let
    vars :: HashSet Op
vars = RuntimeTerm -> HashSet Op
getVars RuntimeTerm
t1 HashSet Op -> HashSet Op -> HashSet Op
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
`S.union` RuntimeTerm -> HashSet Op
getVars RuntimeTerm
t2
  in
    Maybe (WQO Op) -> WQO Op
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (WQO Op) -> WQO Op) -> Maybe (WQO Op) -> WQO Op
forall a b. (a -> b) -> a -> b
$ [WQO Op] -> Maybe (WQO Op)
forall a.
(Show a, Ord a, Eq a, Hashable a) =>
[WQO a] -> Maybe (WQO a)
WQO.mergeAll (((Op, Op) -> WQO Op) -> [(Op, Op)] -> [WQO Op]
forall a b. (a -> b) -> [a] -> [b]
map ((Op -> Op -> WQO Op) -> (Op, Op) -> WQO Op
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Op -> Op -> WQO Op
(=.)) ([Op] -> [(Op, Op)]
forall b. [b] -> [(b, b)]
pairs (HashSet Op -> [Op]
forall a. HashSet a -> [a]
S.toList HashSet Op
vars)))
  where
    pairs :: [b] -> [(b, b)]
pairs [b]
xs | [b] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 = []
    pairs [b]
xs | Bool
otherwise = [b] -> [b] -> [(b, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [b]
xs ([b] -> [b]
forall a. [a] -> [a]
tail [b]
xs)

cgen :: (Show (oc Op), Eq (oc Op), Hashable (oc Op)) => ConstraintGen oc Op RuntimeTerm Identity
cgen :: ConstraintGen oc Op RuntimeTerm Identity
cgen WQOConstraints oc m'
impl Relation
r oc Op
oc RuntimeTerm
t1 RuntimeTerm
t2 =
  let
    Identity oc Op
rpoc = WQOConstraints oc m'
-> Relation
-> oc Op
-> RuntimeTerm
-> RuntimeTerm
-> Identity (oc Op)
forall (oc :: * -> *).
(Show (oc Op), Eq (oc Op), Hashable (oc Op)) =>
ConstraintGen oc Op RuntimeTerm Identity
rpo WQOConstraints oc m'
impl Relation
r oc Op
oc RuntimeTerm
t1 RuntimeTerm
t2
  in
    oc Op -> Identity (oc Op)
forall (m :: * -> *) a. Monad m => a -> m a
return (oc Op -> Identity (oc Op)) -> oc Op -> Identity (oc Op)
forall a b. (a -> b) -> a -> b
$ WQOConstraints oc m' -> WQO Op -> oc Op -> oc Op
forall (impl :: * -> *) (m :: * -> *).
WQOConstraints impl m
-> forall a. (Eq a, Ord a, Hashable a) => WQO a -> impl a -> impl a
addConstraint WQOConstraints oc m'
impl (RuntimeTerm -> RuntimeTerm -> WQO Op
varsEQ RuntimeTerm
t1 RuntimeTerm
t2) oc Op
rpoc