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

 Maintainer   :    
 Stability    :   experimental 
 Portability :   portable 

 Description : 
 Abstract syntax for an hybridized logic . Declaration 
 of the basic specification . Underlying Spec ; Declaration 
 of nominals and modalities , and axioms . 

Module      :  ./TopHybrid/AS_TopHybrid.der.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  
Stability   :  experimental
Portability :  portable

Description :
Abstract syntax for an hybridized logic. Declaration
of the basic specification. Underlying Spec; Declaration
of nominals and modalities, and axioms.
-}

module TopHybrid.AS_TopHybrid where

import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.ToXml

import Logic.Logic

import Unsafe.Coerce

import Data.Data
import Data.Monoid ()

import Text.XML.Light

-- DrIFT command
! global : GetRange !

{- Union of the the declaration of nominals/modalities and the
   spec correspondent to the underlying logic -}
data TH_BSPEC s = Bspec { bitems :: [TH_BASIC_ITEM], und :: s }
  deriving (Show, Typeable, Data)

-- Declaration of nominals/modalities
data TH_BASIC_ITEM = Simple_mod_decl [MODALITY]
                   | Simple_nom_decl [NOMINAL]
                     deriving (Show, Typeable, Data)

type MODALITY = SIMPLE_ID
type NOMINAL = SIMPLE_ID

  The strucuture of an hybridized sentence , where f  to the 
 underlying logic
underlying logic -}
data TH_FORMULA f = At NOMINAL (TH_FORMULA f)
                  | Uni NOMINAL (TH_FORMULA f)
                  | Exist NOMINAL (TH_FORMULA f)
                  | Box MODALITY (TH_FORMULA f)
                  | Dia MODALITY (TH_FORMULA f)
                  | UnderLogic f
                  | Conjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Disjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Implication (TH_FORMULA f) (TH_FORMULA f)
                  | BiImplication (TH_FORMULA f) (TH_FORMULA f)
                  | Here NOMINAL
                  | Neg (TH_FORMULA f)
                  | Par (TH_FORMULA f)
                  | TrueA
                  | FalseA
                    deriving (Show, Eq, Ord, Typeable, Data)

instance ToJson f => ToJson (TH_FORMULA f) where
  asJson _ = mkJObj []

instance ToXml f => ToXml (TH_FORMULA f) where
  asXml _ = unode "missing" ()

  Existential quantification is used , in the Sentences , Spec and Signature 
 because , we need to hide that these datatypes are polymorphic , or else , 
 haskell will complain that their types will vary with the same logic . Which 
 is forbidden in Logic class by using functional dependencies .
because, we need to hide that these datatypes are polymorphic, or else,
haskell will complain that their types will vary with the same logic. Which
is forbidden in Logic class by using functional dependencies. -}

{- An hybridized formula has the hybrid constructors; the constructors
of the hybridized logic and the logic identifier, so that we can
identify the underlying logic, by only looking to the sentence. -}
data Frm_Wrap = forall l sub bs f s sm si mo sy rw pf .
    (Logic l sub bs f s sm si mo sy rw pf)
    => Frm_Wrap l (TH_FORMULA f)
  deriving Typeable

instance Show Frm_Wrap where
  show (Frm_Wrap l f) = "Frm_Wrap " ++ show l ++ " (" ++ show f ++ ")"

instance ToJson Frm_Wrap where
  asJson (Frm_Wrap l f) = mkJObj [("Frm_Wrap:" ++ show l, asJson f)]

instance ToXml Frm_Wrap where
  asXml (Frm_Wrap l f) =
    add_attr (mkAttr "language" $ show l) $ unode "Frm_Wrap" $ asXml f

{- An hybridized specification has the basic specification; The declararation
of nominals and modalities, and the axioms; -}
data Spc_Wrap = forall l sub bs sen si smi sign mor symb raw pf .
    (Logic l sub bs sen si smi sign mor symb raw pf)
    => Spc_Wrap l (TH_BSPEC bs) [Annoted Frm_Wrap]
  deriving Typeable

instance Show Spc_Wrap where
  show (Spc_Wrap l b a) =
    "Spc_Wrap " ++ show l ++ " (" ++ show b ++ ") " ++ show a

instance Semigroup Spc_Wrap where
  _ <> _ = error "Not implemented!"

instance Monoid Spc_Wrap where
 mempty = error "Not implemented!"

-- --- instances
data Mor = Mor deriving (Show, Eq, Ord, Typeable, Data)

-- Why do we need to compare specifications ?
instance Ord Spc_Wrap where
        compare _ _ = GT

instance Eq Spc_Wrap where
       (==) _ _ = False
-- --------------

-- Who do we need to order formulas ?
instance Ord Frm_Wrap where
        compare a b = if a == b then EQ else GT

{- Need to use unsafe coerce here, as the typechecker as no way to know
that if l == l' then type f == type f'. However, we know. -}
instance Eq Frm_Wrap where
       (==) (Frm_Wrap l f) (Frm_Wrap l' f') =
               (show l == show l') && (unsafeCoerce f == f')

-- Why do we need range ?
instance GetRange Frm_Wrap where
        getRange (Frm_Wrap _ f) = getRange f
        rangeSpan (Frm_Wrap _ f) = rangeSpan f

instance GetRange Spc_Wrap where
        getRange (Spc_Wrap _ s _) = getRange s
        rangeSpan (Spc_Wrap _ s _) = rangeSpan s

# LANGUAGE DeriveDataTypeable #
 DrIFT command
 Union of the the declaration of nominals/modalities and the
   spec correspondent to the underlying logic 
 Declaration of nominals/modalities
 An hybridized formula has the hybrid constructors; the constructors
of the hybridized logic and the logic identifier, so that we can
identify the underlying logic, by only looking to the sentence. 
 An hybridized specification has the basic specification; The declararation
of nominals and modalities, and the axioms; 
 --- instances
 Why do we need to compare specifications ?
 --------------
 Who do we need to order formulas ?
 Need to use unsafe coerce here, as the typechecker as no way to know
that if l == l' then type f == type f'. However, we know. 
 Why do we need range ?
# LANGUAGE ExistentialQuantification #
# LANGUAGE MonoLocalBinds #
  | 
 Module       :   ./TopHybrid / AS_TopHybrid.der.hs 
 License      :   GPLv2 or higher , see LICENSE.txt 

 Maintainer   :    
 Stability    :   experimental 
 Portability :   portable 

 Description : 
 Abstract syntax for an hybridized logic . Declaration 
 of the basic specification . Underlying Spec ; Declaration 
 of nominals and modalities , and axioms . 

Module      :  ./TopHybrid/AS_TopHybrid.der.hs
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  
Stability   :  experimental
Portability :  portable

Description :
Abstract syntax for an hybridized logic. Declaration
of the basic specification. Underlying Spec; Declaration
of nominals and modalities, and axioms.
-}

module TopHybrid.AS_TopHybrid where

import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.ToXml

import Logic.Logic

import Unsafe.Coerce

import Data.Data
import Data.Monoid ()

import Text.XML.Light

! global : GetRange !

data TH_BSPEC s = Bspec { bitems :: [TH_BASIC_ITEM], und :: s }
  deriving (Show, Typeable, Data)

data TH_BASIC_ITEM = Simple_mod_decl [MODALITY]
                   | Simple_nom_decl [NOMINAL]
                     deriving (Show, Typeable, Data)

type MODALITY = SIMPLE_ID
type NOMINAL = SIMPLE_ID

  The strucuture of an hybridized sentence , where f  to the 
 underlying logic
underlying logic -}
data TH_FORMULA f = At NOMINAL (TH_FORMULA f)
                  | Uni NOMINAL (TH_FORMULA f)
                  | Exist NOMINAL (TH_FORMULA f)
                  | Box MODALITY (TH_FORMULA f)
                  | Dia MODALITY (TH_FORMULA f)
                  | UnderLogic f
                  | Conjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Disjunction (TH_FORMULA f) (TH_FORMULA f)
                  | Implication (TH_FORMULA f) (TH_FORMULA f)
                  | BiImplication (TH_FORMULA f) (TH_FORMULA f)
                  | Here NOMINAL
                  | Neg (TH_FORMULA f)
                  | Par (TH_FORMULA f)
                  | TrueA
                  | FalseA
                    deriving (Show, Eq, Ord, Typeable, Data)

instance ToJson f => ToJson (TH_FORMULA f) where
  asJson _ = mkJObj []

instance ToXml f => ToXml (TH_FORMULA f) where
  asXml _ = unode "missing" ()

  Existential quantification is used , in the Sentences , Spec and Signature 
 because , we need to hide that these datatypes are polymorphic , or else , 
 haskell will complain that their types will vary with the same logic . Which 
 is forbidden in Logic class by using functional dependencies .
because, we need to hide that these datatypes are polymorphic, or else,
haskell will complain that their types will vary with the same logic. Which
is forbidden in Logic class by using functional dependencies. -}

data Frm_Wrap = forall l sub bs f s sm si mo sy rw pf .
    (Logic l sub bs f s sm si mo sy rw pf)
    => Frm_Wrap l (TH_FORMULA f)
  deriving Typeable

instance Show Frm_Wrap where
  show (Frm_Wrap l f) = "Frm_Wrap " ++ show l ++ " (" ++ show f ++ ")"

instance ToJson Frm_Wrap where
  asJson (Frm_Wrap l f) = mkJObj [("Frm_Wrap:" ++ show l, asJson f)]

instance ToXml Frm_Wrap where
  asXml (Frm_Wrap l f) =
    add_attr (mkAttr "language" $ show l) $ unode "Frm_Wrap" $ asXml f

data Spc_Wrap = forall l sub bs sen si smi sign mor symb raw pf .
    (Logic l sub bs sen si smi sign mor symb raw pf)
    => Spc_Wrap l (TH_BSPEC bs) [Annoted Frm_Wrap]
  deriving Typeable

instance Show Spc_Wrap where
  show (Spc_Wrap l b a) =
    "Spc_Wrap " ++ show l ++ " (" ++ show b ++ ") " ++ show a

instance Semigroup Spc_Wrap where
  _ <> _ = error "Not implemented!"

instance Monoid Spc_Wrap where
 mempty = error "Not implemented!"

data Mor = Mor deriving (Show, Eq, Ord, Typeable, Data)

instance Ord Spc_Wrap where
        compare _ _ = GT

instance Eq Spc_Wrap where
       (==) _ _ = False

instance Ord Frm_Wrap where
        compare a b = if a == b then EQ else GT

instance Eq Frm_Wrap where
       (==) (Frm_Wrap l f) (Frm_Wrap l' f') =
               (show l == show l') && (unsafeCoerce f == f')

instance GetRange Frm_Wrap where
        getRange (Frm_Wrap _ f) = getRange f
        rangeSpan (Frm_Wrap _ f) = rangeSpan f

instance GetRange Spc_Wrap where
        getRange (Spc_Wrap _ s _) = getRange s
        rangeSpan (Spc_Wrap _ s _) = rangeSpan s
