ConcreteOC.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}

module Language.REST.ConcreteOC where

import qualified Language.REST.OCAlgebra as AOC
import qualified Language.REST.Internal.WQO as WQO
import           Language.REST.RuntimeTerm
import           Language.REST.RPO
import           Language.REST.Internal.OpOrdering
import           Language.REST.MetaTerm

import Data.List as L
import Data.Hashable
import GHC.Generics (Generic)
import qualified Data.Set as S

data ConcreteOC = ConcreteOC [RuntimeTerm] (Maybe OpOrdering)
  deriving (Eq, Ord, Generic, Hashable)

instance Show ConcreteOC where
  show (ConcreteOC _ (Just oo)) = show oo
  show _                        = "impossible"

isSat :: ConcreteOC -> Bool
isSat (ConcreteOC _ (Just _)) = True
isSat _                       = False

getOrdering :: [RuntimeTerm] -> Maybe OpOrdering
getOrdering ts =
  let
    ops       = S.unions $ map termOps ts
    orderings = S.toList $ WQO.orderings ops
  in
    L.find (`orients` ts) orderings


orients :: OpOrdering -> [RuntimeTerm] -> Bool
orients ordering terms =
  let
    pairs = zip terms (tail terms)
  in
    all (uncurry $ synGTE ordering) pairs

concreteOC :: Monad m => AOC.OCAlgebra ConcreteOC RuntimeTerm m
concreteOC = AOC.OCAlgebra (return . isSat) refine (ConcreteOC [] (Just (WQO.empty))) constUnion notStrongerThan
  where
    constUnion t1 _ = t1
    notStrongerThan _ _ = return False
    refine :: ConcreteOC -> RuntimeTerm -> RuntimeTerm -> ConcreteOC
    refine (ConcreteOC ts (Just o)) _ u =
      let
        ts' = ts ++ [u]
      in
        ConcreteOC ts' $
          if o `orients` ts'
          then Just o
          else getOrdering ts'
    refine (ConcreteOC ts Nothing) _ u = ConcreteOC (ts ++ [u]) Nothing