{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
{- |
Module      :  ./TopHybrid/TopHybridSign.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  nevrenato@gmail.com
Stability   :  experimental
Portability :  portable

Description  :
Signature for an hybridized logic. Its constituted by
the declaration of nominals and modalities, and the signature
of the logic below
-}

module TopHybrid.TopHybridSign where

import TopHybrid.AS_TopHybrid
import Logic.Logic
import Common.Result
import Common.Id
import Data.Data
import Data.Set
import Unsafe.Coerce
import Control.Monad (liftM)

{- Prototype; a datatype that wraps the signature and the base logic
so that we can know which is the underlying logic, by only looking
to the signature
We have a total different constructor to represent the empty signagture;
we can't compute the an empty signature, without knowing the logic below,
hence we use the different constructor for that, which doesn't have the lid. -}
data Sgn_Wrap = forall l sub bs f s sm sign mo sy rw pf .
                        (Logic l sub bs f s sm sign mo sy rw pf) =>
                        Sgn_Wrap l (THybridSign sign)
                | EmptySign
  deriving Typeable

instance Show Sgn_Wrap where
  show :: Sgn_Wrap -> String
show c :: Sgn_Wrap
c = case Sgn_Wrap
c of
    Sgn_Wrap l :: l
l s :: THybridSign sign
s -> "Sgn_Wrap " String -> ShowS
forall a. [a] -> [a] -> [a]
++ l -> String
forall a. Show a => a -> String
show l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ THybridSign sign -> String
forall a. Show a => a -> String
show THybridSign sign
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
    EmptySign -> "EmptySign"

data THybridSign s = THybridSign
  {
    THybridSign s -> Set MODALITY
modies :: Set MODALITY
  , THybridSign s -> Set MODALITY
nomies :: Set NOMINAL
  , THybridSign s -> s
extended :: s
  } deriving (Int -> THybridSign s -> ShowS
[THybridSign s] -> ShowS
THybridSign s -> String
(Int -> THybridSign s -> ShowS)
-> (THybridSign s -> String)
-> ([THybridSign s] -> ShowS)
-> Show (THybridSign s)
forall s. Show s => Int -> THybridSign s -> ShowS
forall s. Show s => [THybridSign s] -> ShowS
forall s. Show s => THybridSign s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [THybridSign s] -> ShowS
$cshowList :: forall s. Show s => [THybridSign s] -> ShowS
show :: THybridSign s -> String
$cshow :: forall s. Show s => THybridSign s -> String
showsPrec :: Int -> THybridSign s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> THybridSign s -> ShowS
Show, THybridSign s -> THybridSign s -> Bool
(THybridSign s -> THybridSign s -> Bool)
-> (THybridSign s -> THybridSign s -> Bool) -> Eq (THybridSign s)
forall s. Eq s => THybridSign s -> THybridSign s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: THybridSign s -> THybridSign s -> Bool
$c/= :: forall s. Eq s => THybridSign s -> THybridSign s -> Bool
== :: THybridSign s -> THybridSign s -> Bool
$c== :: forall s. Eq s => THybridSign s -> THybridSign s -> Bool
Eq, Eq (THybridSign s)
Eq (THybridSign s) =>
(THybridSign s -> THybridSign s -> Ordering)
-> (THybridSign s -> THybridSign s -> Bool)
-> (THybridSign s -> THybridSign s -> Bool)
-> (THybridSign s -> THybridSign s -> Bool)
-> (THybridSign s -> THybridSign s -> Bool)
-> (THybridSign s -> THybridSign s -> THybridSign s)
-> (THybridSign s -> THybridSign s -> THybridSign s)
-> Ord (THybridSign s)
THybridSign s -> THybridSign s -> Bool
THybridSign s -> THybridSign s -> Ordering
THybridSign s -> THybridSign s -> THybridSign s
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
forall s. Ord s => Eq (THybridSign s)
forall s. Ord s => THybridSign s -> THybridSign s -> Bool
forall s. Ord s => THybridSign s -> THybridSign s -> Ordering
forall s. Ord s => THybridSign s -> THybridSign s -> THybridSign s
min :: THybridSign s -> THybridSign s -> THybridSign s
$cmin :: forall s. Ord s => THybridSign s -> THybridSign s -> THybridSign s
max :: THybridSign s -> THybridSign s -> THybridSign s
$cmax :: forall s. Ord s => THybridSign s -> THybridSign s -> THybridSign s
>= :: THybridSign s -> THybridSign s -> Bool
$c>= :: forall s. Ord s => THybridSign s -> THybridSign s -> Bool
> :: THybridSign s -> THybridSign s -> Bool
$c> :: forall s. Ord s => THybridSign s -> THybridSign s -> Bool
<= :: THybridSign s -> THybridSign s -> Bool
$c<= :: forall s. Ord s => THybridSign s -> THybridSign s -> Bool
< :: THybridSign s -> THybridSign s -> Bool
$c< :: forall s. Ord s => THybridSign s -> THybridSign s -> Bool
compare :: THybridSign s -> THybridSign s -> Ordering
$ccompare :: forall s. Ord s => THybridSign s -> THybridSign s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (THybridSign s)
Ord, Typeable, Typeable (THybridSign s)
Constr
DataType
Typeable (THybridSign s) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (THybridSign s))
-> (THybridSign s -> Constr)
-> (THybridSign s -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (THybridSign s)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (THybridSign s)))
-> ((forall b. Data b => b -> b) -> THybridSign s -> THybridSign s)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> THybridSign s -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> THybridSign s -> r)
-> (forall u. (forall d. Data d => d -> u) -> THybridSign s -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> THybridSign s -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> THybridSign s -> m (THybridSign s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> THybridSign s -> m (THybridSign s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> THybridSign s -> m (THybridSign s))
-> Data (THybridSign s)
THybridSign s -> Constr
THybridSign s -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (THybridSign s))
(forall b. Data b => b -> b) -> THybridSign s -> THybridSign s
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (THybridSign s)
forall s. Data s => Typeable (THybridSign s)
forall s. Data s => THybridSign s -> Constr
forall s. Data s => THybridSign s -> DataType
forall s.
Data s =>
(forall b. Data b => b -> b) -> THybridSign s -> THybridSign s
forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> THybridSign s -> u
forall s u.
Data s =>
(forall d. Data d => d -> u) -> THybridSign s -> [u]
forall s r r'.
Data s =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
forall s r r'.
Data s =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (THybridSign s)
forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s)
forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (THybridSign s))
forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (THybridSign s))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> THybridSign s -> u
forall u. (forall d. Data d => d -> u) -> THybridSign s -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (THybridSign s)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (THybridSign s))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (THybridSign s))
$cTHybridSign :: Constr
$tTHybridSign :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
$cgmapMo :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
gmapMp :: (forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
$cgmapMp :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
gmapM :: (forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
$cgmapM :: forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d)
-> THybridSign s -> m (THybridSign s)
gmapQi :: Int -> (forall d. Data d => d -> u) -> THybridSign s -> u
$cgmapQi :: forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> THybridSign s -> u
gmapQ :: (forall d. Data d => d -> u) -> THybridSign s -> [u]
$cgmapQ :: forall s u.
Data s =>
(forall d. Data d => d -> u) -> THybridSign s -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
$cgmapQr :: forall s r r'.
Data s =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
$cgmapQl :: forall s r r'.
Data s =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> THybridSign s -> r
gmapT :: (forall b. Data b => b -> b) -> THybridSign s -> THybridSign s
$cgmapT :: forall s.
Data s =>
(forall b. Data b => b -> b) -> THybridSign s -> THybridSign s
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (THybridSign s))
$cdataCast2 :: forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (THybridSign s))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (THybridSign s))
$cdataCast1 :: forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (THybridSign s))
dataTypeOf :: THybridSign s -> DataType
$cdataTypeOf :: forall s. Data s => THybridSign s -> DataType
toConstr :: THybridSign s -> Constr
$ctoConstr :: forall s. Data s => THybridSign s -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (THybridSign s)
$cgunfold :: forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (THybridSign s)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s)
$cgfoldl :: forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> THybridSign s -> c (THybridSign s)
$cp1Data :: forall s. Data s => Typeable (THybridSign s)
Data)

emptyHybridSign :: Sgn_Wrap
emptyHybridSign :: Sgn_Wrap
emptyHybridSign = Sgn_Wrap
EmptySign

{- Unfortunately, the typechecker can't know that if (l == l') then
the extended signatures are the same. Thus, we will have to use unsafe
functions here. Also unfortunately the datatype Lids can't be directly compared
so we have to use their string representation, which is bijective, hence we can
compare in this way. -}
isSubTHybSgn :: Sgn_Wrap -> Sgn_Wrap -> Bool
isSubTHybSgn :: Sgn_Wrap -> Sgn_Wrap -> Bool
isSubTHybSgn (Sgn_Wrap l :: l
l s :: THybridSign sign
s) (Sgn_Wrap l' :: l
l' s' :: THybridSign sign
s') = Bool
final
               where
               resExt :: Bool
resExt = (l -> String
forall a. Show a => a -> String
show l
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== l -> String
forall a. Show a => a -> String
show l
l') Bool -> Bool -> Bool
&&
                        l -> sign -> sign -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Bool
is_subsig l
l (THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s) (sign -> sign
forall a b. a -> b
unsafeCoerce (sign -> sign) -> sign -> sign
forall a b. (a -> b) -> a -> b
$ THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s')
               final :: Bool
final = Set MODALITY -> Set MODALITY -> Bool
forall a. Ord a => Set a -> Set a -> Bool
isSubsetOf (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s) (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s') Bool -> Bool -> Bool
&&
                       Set MODALITY -> Set MODALITY -> Bool
forall a. Ord a => Set a -> Set a -> Bool
isSubsetOf (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s) (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s') Bool -> Bool -> Bool
&&
                       Bool
resExt
-- An empty set is always contained in any other set
isSubTHybSgn EmptySign _ = Bool
True
-- A non empty set is never contained in an empty set
isSubTHybSgn _ EmptySign = Bool
False

{- Computes the difference between two signatures. If they belong to
different logics then throw an error -}
sgnDiff :: Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
-- The difference between an emptySign and any other Sig results in an emptySig
sgnDiff :: Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
sgnDiff EmptySign _ = Sgn_Wrap -> Result Sgn_Wrap
forall (m :: * -> *) a. Monad m => a -> m a
return Sgn_Wrap
EmptySign
-- The difference between any sig and a empty sig results in the original sig
sgnDiff s :: Sgn_Wrap
s EmptySign = Sgn_Wrap -> Result Sgn_Wrap
forall (m :: * -> *) a. Monad m => a -> m a
return Sgn_Wrap
s

sgnDiff (Sgn_Wrap l :: l
l s :: THybridSign sign
s) (Sgn_Wrap l' :: l
l' s' :: THybridSign sign
s') =
                if l -> String
forall a. Show a => a -> String
show l
l String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= l -> String
forall a. Show a => a -> String
show l
l'
                then [Diagnosis] -> Maybe Sgn_Wrap -> Result Sgn_Wrap
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error "signatures belong to different logics"
                              Range
nullRange] Maybe Sgn_Wrap
forall a. Maybe a
Nothing
                else (THybridSign sign -> Sgn_Wrap)
-> Result (THybridSign sign) -> Result Sgn_Wrap
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (l -> THybridSign sign -> Sgn_Wrap
forall l sub bs f s sm sign mo sy rw pf.
Logic l sub bs f s sm sign mo sy rw pf =>
l -> THybridSign sign -> Sgn_Wrap
Sgn_Wrap l
l) Result (THybridSign sign)
ds
                where
                        dn :: Set MODALITY
dn = Set MODALITY -> Set MODALITY -> Set MODALITY
forall a. Ord a => Set a -> Set a -> Set a
difference (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s) (Set MODALITY -> Set MODALITY) -> Set MODALITY -> Set MODALITY
forall a b. (a -> b) -> a -> b
$ THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
nomies THybridSign sign
s'
                        dm :: Set MODALITY
dm = Set MODALITY -> Set MODALITY -> Set MODALITY
forall a. Ord a => Set a -> Set a -> Set a
difference (THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s) (Set MODALITY -> Set MODALITY) -> Set MODALITY -> Set MODALITY
forall a b. (a -> b) -> a -> b
$ THybridSign sign -> Set MODALITY
forall s. THybridSign s -> Set MODALITY
modies THybridSign sign
s'
                        ds :: Result (THybridSign sign)
ds = (sign -> THybridSign sign)
-> Result sign -> Result (THybridSign sign)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Set MODALITY -> Set MODALITY -> sign -> THybridSign sign
forall s. Set MODALITY -> Set MODALITY -> s -> THybridSign s
THybridSign Set MODALITY
dm Set MODALITY
dn) (Result sign -> Result (THybridSign sign))
-> Result sign -> Result (THybridSign sign)
forall a b. (a -> b) -> a -> b
$ l -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signatureDiff l
l
                              (THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s) (sign -> sign
forall a b. a -> b
unsafeCoerce (sign -> sign) -> sign -> sign
forall a b. (a -> b) -> a -> b
$ THybridSign sign -> sign
forall s. THybridSign s -> s
extended THybridSign sign
s')

-- --- instances needed

instance Eq Sgn_Wrap where
        == :: Sgn_Wrap -> Sgn_Wrap -> Bool
(==) a :: Sgn_Wrap
a b :: Sgn_Wrap
b = Sgn_Wrap -> Sgn_Wrap -> Bool
isSubTHybSgn Sgn_Wrap
a Sgn_Wrap
b Bool -> Bool -> Bool
&& Sgn_Wrap -> Sgn_Wrap -> Bool
isSubTHybSgn Sgn_Wrap
b Sgn_Wrap
a
instance Ord Sgn_Wrap where
        compare :: Sgn_Wrap -> Sgn_Wrap -> Ordering
compare a :: Sgn_Wrap
a b :: Sgn_Wrap
b = if Sgn_Wrap
a Sgn_Wrap -> Sgn_Wrap -> Bool
forall a. Eq a => a -> a -> Bool
== Sgn_Wrap
b then Ordering
EQ else Ordering
GT