AS_TopHybrid.der.hs revision fb379f6c0a7ae0d68ce7e9a2da13d2cece4d76d1
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable #-}
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiModule : $Header$
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachLicense : GPLv2 or higher, see LICENSE.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : nevrenato@gmail.com
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiStability : experimental
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederAbstract syntax for an hybridized logic. Declaration
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachof the basic specification. Underlying Spec; Declaration
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachof nominals and modalities, and axioms.
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- DrIFT command
fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly{-! global: GetRange !-}
bcd914850de931848b86d7728192a149f9c0108bChristian Maeder{- Union of the the declaration of nominals/modalities and the
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly spec correspondent to the underlying logic -}
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillydata TH_BSPEC s = Bspec { bitems :: [TH_BASIC_ITEM], und :: s } deriving Show
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- Declaration of nominals/modalities
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederdata TH_BASIC_ITEM = Simple_mod_decl [MODALITY]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder | Simple_nom_decl [NOMINAL]
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder deriving Show
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maedertype MODALITY = SIMPLE_ID
f284db6f4dffd7bf60b82319648efb7bcb9378c9Christian Maedertype NOMINAL = SIMPLE_ID
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett{- The strucuture of an hybridized sentence, where f correponds to the
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederunderlying logic -}
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederdata TH_FORMULA f = At NOMINAL (TH_FORMULA f)
d04c328b10f17ec78001a94d694f7188ebd8c03cAndy Gimblett | Uni NOMINAL (TH_FORMULA f)
2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly | Exist NOMINAL (TH_FORMULA f)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett | Box MODALITY (TH_FORMULA f)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | Dia MODALITY (TH_FORMULA f)
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder | UnderLogic f
2650e8a56cc2381719bd2390fdf82402e0c696d8Christian Maeder | Conjunction (TH_FORMULA f) (TH_FORMULA f)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder | Disjunction (TH_FORMULA f) (TH_FORMULA f)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | Implication (TH_FORMULA f) (TH_FORMULA f)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | BiImplication (TH_FORMULA f) (TH_FORMULA f)
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder | Here NOMINAL
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder | Neg (TH_FORMULA f)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly | Par (TH_FORMULA f)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder deriving (Show, Eq, Ord)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder{- Existential quantification is used, in the Sentences, Spec and Signature
4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maederbecause, we need to hide that these datatypes are polymorphic, or else,
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyhaskell will complain that their types will vary with the same logic. Which
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyis forbidden in Logic class by using functional dependencies. -}
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly{- An hybridized formula has the hybrid constructors; the constructors
842ae753ab848a8508c4832ab64296b929167a97Christian Maederof the hybridized logic and the logic identifier, so that we can
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyidentify the underlying logic, by only looking to the sentence. -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maederdata Frm_Wrap = forall l sub bs f s sm si mo sy rw pf .
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (Logic l sub bs f s sm si mo sy rw pf) =>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Frm_Wrap l (TH_FORMULA f)
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder deriving Typeable
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Show Frm_Wrap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (Frm_Wrap l f) = "Frm_Wrap " ++ show l ++ " (" ++ show f ++ ")"
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder{- An hybridized specification has the basic specification; The declararation
67e234eb781dd16dfd269486befd2b5781075079Christian Maederof nominals and modalities, and the axioms; -}
842ae753ab848a8508c4832ab64296b929167a97Christian Maederdata Spc_Wrap = forall l sub bs sen si smi sign mor symb raw pf .
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (Logic l sub bs sen si smi sign mor symb raw pf) =>
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Spc_Wrap l (TH_BSPEC bs) [Annoted Frm_Wrap]
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly deriving Typeable
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederinstance Show Spc_Wrap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly show (Spc_Wrap l b a) =
842ae753ab848a8508c4832ab64296b929167a97Christian Maeder "Spc_Wrap " ++ show l ++ " (" ++ show b ++ ") " ++ show a
842ae753ab848a8508c4832ab64296b929167a97Christian Maederinstance Monoid Spc_Wrap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly mempty = error "Not implemented!"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly mappend _ _ = error "Not implemented!"
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- --- instances
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettdata Mor = Mor deriving (Eq, Ord, Show)
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- Why do we need to compare specifications ?
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Ord Spc_Wrap where
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett compare _ _ = GT
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyinstance Eq Spc_Wrap where
9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (==) _ _ = False
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder-- --------------
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder-- Who do we need to order formulas ?
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Ord Frm_Wrap where
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly compare a b = if a == b then EQ else GT
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly{- Need to use unsafe coerce here, as the typechecker as no way to know
b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederthat if l == l' then type f == type f'. However, we know. -}
8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettinstance Eq Frm_Wrap where
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett (==) (Frm_Wrap l f) (Frm_Wrap l' f') =
e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett (show l == show l') && (unsafeCoerce f == f')
d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett-- Why do we need range ?
16e124196c6b204769042028c74f533509c9b5d3Christian Maederinstance GetRange Frm_Wrap where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach getRange (Frm_Wrap _ f) = getRange f
67e234eb781dd16dfd269486befd2b5781075079Christian Maeder rangeSpan (Frm_Wrap _ f) = rangeSpan f
67e234eb781dd16dfd269486befd2b5781075079Christian Maederinstance GetRange Spc_Wrap where
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder getRange (Spc_Wrap _ s _) = getRange s
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder rangeSpan (Spc_Wrap _ s _) = rangeSpan s