{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Language.REST.OCToAbstract where import Data.Hashable import Control.Monad.Identity import Language.REST.OCAlgebra import qualified Language.REST.WQOConstraints as OC import Language.REST.Types import Language.REST.SMT (ToSMTVar) showHash :: Show a => a -> String showHash :: a -> String showHash = Int -> String forall a. Show a => a -> String show (Int -> String) -> (a -> Int) -> a -> String forall b c a. (b -> c) -> (a -> b) -> a -> c . String -> Int forall a. Hashable a => a -> Int hash (String -> Int) -> (a -> String) -> a -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . a -> String forall a. Show a => a -> String show lift :: forall impl base lifted m . (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) => OC.WQOConstraints impl m -> OC.ConstraintGen impl base lifted Identity -> OCAlgebra (impl base) lifted m lift :: WQOConstraints impl m -> ConstraintGen impl base lifted Identity -> OCAlgebra (impl base) lifted m lift WQOConstraints impl m oc ConstraintGen impl base lifted Identity cgen = OCAlgebra :: forall c a (m :: * -> *). (c -> m Bool) -> (c -> a -> a -> c) -> c -> (c -> c -> c) -> (c -> c -> m Bool) -> OCAlgebra c a m OCAlgebra { isSat :: impl base -> m Bool isSat = impl base -> m Bool isSat' , top :: impl base top = impl base top' , refine :: impl base -> lifted -> lifted -> impl base refine = impl base -> lifted -> lifted -> impl base refine' , union :: impl base -> impl base -> impl base union = WQOConstraints impl m -> forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a forall (impl :: * -> *) (m :: * -> *). WQOConstraints impl m -> forall a. (Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a OC.union WQOConstraints impl m oc , notStrongerThan :: impl base -> impl base -> m Bool notStrongerThan = WQOConstraints impl m -> forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool forall (impl :: * -> *) (m :: * -> *). WQOConstraints impl m -> forall a. (ToSMTVar a Int, Eq a, Ord a, Hashable a) => impl a -> impl a -> m Bool OC.notStrongerThan WQOConstraints impl m oc } where isSat' :: impl base -> m Bool isSat' :: impl base -> m Bool isSat' impl base aoc = WQOConstraints impl m -> impl base -> m Bool forall (impl :: * -> *) (m :: * -> *). WQOConstraints impl m -> forall a. (ToSMTVar a Int, Show a, Eq a, Ord a, Hashable a) => impl a -> m Bool OC.isSatisfiable WQOConstraints impl m oc impl base aoc top' :: impl base top' :: impl base top' = WQOConstraints impl m -> forall a. (Eq a, Ord a, Hashable a) => impl a forall (impl :: * -> *) (m :: * -> *). WQOConstraints impl m -> forall a. (Eq a, Ord a, Hashable a) => impl a OC.noConstraints WQOConstraints impl m oc refine' :: impl base -> lifted -> lifted -> impl base refine' :: impl base -> lifted -> lifted -> impl base refine' impl base c lifted t lifted u = let pair :: impl base pair = Identity (impl base) -> impl base forall a. Identity a -> a runIdentity (Identity (impl base) -> impl base) -> Identity (impl base) -> impl base forall a b. (a -> b) -> a -> b $ WQOConstraints impl m -> Relation -> impl base -> lifted -> lifted -> Identity (impl base) ConstraintGen impl base lifted Identity cgen WQOConstraints impl m oc Relation GTE impl base top' lifted t lifted u result :: impl base result = WQOConstraints impl m -> impl base -> impl base -> impl base forall (impl :: * -> *) (m :: * -> *). WQOConstraints impl m -> forall a. (Show a, Eq a, Ord a, Hashable a) => impl a -> impl a -> impl a OC.intersect WQOConstraints impl m oc impl base c impl base pair in impl base result