{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Hybrid/Logic_Hybrid.hs
Description :  Instance of class Logic for Hybrid CASL


Instance of class Logic for hybrid logic.
-}

module Hybrid.Logic_Hybrid where

import Logic.Logic
import Hybrid.AS_Hybrid
import Hybrid.HybridSign
import Hybrid.ATC_Hybrid ()
import Hybrid.Parse_AS
import Hybrid.Print_AS
import Hybrid.StatAna
import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.MapSentence
import CASL.SimplifySen
import CASL.SymbolParser
import CASL.Taxonomy
import CASL.ToDoc
import CASL.Logic_CASL ()

data Hybrid = Hybrid deriving Int -> Hybrid -> ShowS
[Hybrid] -> ShowS
Hybrid -> String
(Int -> Hybrid -> ShowS)
-> (Hybrid -> String) -> ([Hybrid] -> ShowS) -> Show Hybrid
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Hybrid] -> ShowS
$cshowList :: [Hybrid] -> ShowS
show :: Hybrid -> String
$cshow :: Hybrid -> String
showsPrec :: Int -> Hybrid -> ShowS
$cshowsPrec :: Int -> Hybrid -> ShowS
Show

instance Language Hybrid where
 description :: Hybrid -> String
description _ = "Hybrid CASL\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                 "Extends an abitrary logic with at/modal operators."


type HSign = Sign H_FORMULA HybridSign
type HybridMor = Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
type HybridFORMULA = FORMULA H_FORMULA

instance SignExtension HybridSign where
  isSubSignExtension :: HybridSign -> HybridSign -> Bool
isSubSignExtension = HybridSign -> HybridSign -> Bool
isSubHybridSign

instance Syntax Hybrid H_BASIC_SPEC Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
    parse_basic_spec :: Hybrid -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC)
parse_basic_spec Hybrid = (PrefixMap -> AParser st H_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st H_BASIC_SPEC)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st H_BASIC_SPEC)
 -> Maybe (PrefixMap -> AParser st H_BASIC_SPEC))
-> (PrefixMap -> AParser st H_BASIC_SPEC)
-> Maybe (PrefixMap -> AParser st H_BASIC_SPEC)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st H_BASIC_SPEC
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
hybrid_reserved_words
    parse_symb_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Hybrid = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
hybrid_reserved_words
    parse_symb_map_items :: Hybrid -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Hybrid = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
hybrid_reserved_words

-- Hybrid logic
map_H_FORMULA :: MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA :: MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA mor :: Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor (BoxOrDiamond b :: Bool
b m :: MODALITY
m f :: FORMULA H_FORMULA
f ps :: Range
ps) =
   let newM :: MODALITY
newM = case MODALITY
m of
                   Simple_mod _ -> MODALITY
m
                   Term_mod t :: TERM H_FORMULA
t -> let newT :: TERM H_FORMULA
newT = MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> TERM H_FORMULA
-> TERM H_FORMULA
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor TERM H_FORMULA
t
                                 in TERM H_FORMULA -> MODALITY
Term_mod TERM H_FORMULA
newT
       newF :: FORMULA H_FORMULA
newF = MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor FORMULA H_FORMULA
f
   in Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
b MODALITY
newM FORMULA H_FORMULA
newF Range
ps
map_H_FORMULA mor :: Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor (At n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
n (MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor FORMULA H_FORMULA
f) Range
ps
map_H_FORMULA mor :: Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor (Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
n (MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor FORMULA H_FORMULA
f) Range
ps
map_H_FORMULA mor :: Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor (Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) = NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
n (MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
mor FORMULA H_FORMULA
f) Range
ps
map_H_FORMULA _ (Here n :: NOMINAL
n ps :: Range
ps) = NOMINAL -> Range -> H_FORMULA
Here NOMINAL
n Range
ps

instance Sentences Hybrid HybridFORMULA HSign HybridMor Symbol where
      map_sen :: Hybrid
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
map_sen Hybrid h :: Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
h = FORMULA H_FORMULA -> Result (FORMULA H_FORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (FORMULA H_FORMULA -> Result (FORMULA H_FORMULA))
-> (FORMULA H_FORMULA -> FORMULA H_FORMULA)
-> FORMULA H_FORMULA
-> Result (FORMULA H_FORMULA)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen H_FORMULA HybridSign (DefMorExt HybridSign)
map_H_FORMULA Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
h
      sym_of :: Hybrid -> HSign -> [Set Symbol]
sym_of Hybrid = HSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symmap_of :: Hybrid
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> EndoMap Symbol
symmap_of Hybrid = Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: Hybrid -> Symbol -> Id
sym_name Hybrid = Symbol -> Id
symName
      simplify_sen :: Hybrid -> HSign -> FORMULA H_FORMULA -> FORMULA H_FORMULA
simplify_sen Hybrid = Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid
      print_sign :: Hybrid -> HSign -> Doc
print_sign Hybrid sig :: HSign
sig = (HybridSign -> Doc) -> HSign -> Doc
forall e f. (e -> Doc) -> Sign f e -> Doc
printSign
          ((FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
printHybridSign ((FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc)
-> (FORMULA H_FORMULA -> FORMULA H_FORMULA) -> HybridSign -> Doc
forall a b. (a -> b) -> a -> b
$ Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sig) HSign
sig
      print_named :: Hybrid -> Named (FORMULA H_FORMULA) -> Doc
print_named Hybrid = Named (FORMULA H_FORMULA) -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula

-- simplifySen for ExtFORMULA
simHybrid :: Sign H_FORMULA HybridSign -> H_FORMULA -> H_FORMULA
simHybrid :: HSign -> H_FORMULA -> H_FORMULA
simHybrid sign :: HSign
sign (BoxOrDiamond b :: Bool
b md :: MODALITY
md form :: FORMULA H_FORMULA
form pos :: Range
pos) =
        let mod' :: MODALITY
mod' = case MODALITY
md of
                Term_mod term :: TERM H_FORMULA
term -> TERM H_FORMULA -> MODALITY
Term_mod (TERM H_FORMULA -> MODALITY) -> TERM H_FORMULA -> MODALITY
forall a b. (a -> b) -> a -> b
$ Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> TERM H_FORMULA
-> TERM H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> (Sign f e -> f -> f) -> Sign f e -> TERM f -> TERM f
rmTypesT Min H_FORMULA HybridSign
minExpForm
                                             HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sign TERM H_FORMULA
term
                t :: MODALITY
t -> MODALITY
t
        in Bool -> MODALITY -> FORMULA H_FORMULA -> Range -> H_FORMULA
BoxOrDiamond Bool
b MODALITY
mod' (Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sign FORMULA H_FORMULA
form) Range
pos
simHybrid sign :: HSign
sign (At n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) =
        NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
At NOMINAL
n (Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sign FORMULA H_FORMULA
f) Range
ps
simHybrid sign :: HSign
sign (Univ n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) =
        NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Univ NOMINAL
n (Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sign FORMULA H_FORMULA
f) Range
ps
simHybrid sign :: HSign
sign (Exist n :: NOMINAL
n f :: FORMULA H_FORMULA
f ps :: Range
ps) =
        NOMINAL -> FORMULA H_FORMULA -> Range -> H_FORMULA
Exist NOMINAL
n (Min H_FORMULA HybridSign
-> (HSign -> H_FORMULA -> H_FORMULA)
-> HSign
-> FORMULA H_FORMULA
-> FORMULA H_FORMULA
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min H_FORMULA HybridSign
minExpForm HSign -> H_FORMULA -> H_FORMULA
simHybrid HSign
sign FORMULA H_FORMULA
f) Range
ps

simHybrid _ (Here n :: NOMINAL
n ps :: Range
ps) = NOMINAL -> Range -> H_FORMULA
Here NOMINAL
n Range
ps

rmTypesExt :: a -> b -> b
rmTypesExt :: a -> b -> b
rmTypesExt _ f :: b
f = b
f

instance StaticAnalysis Hybrid H_BASIC_SPEC HybridFORMULA
        SYMB_ITEMS SYMB_MAP_ITEMS
        HSign
        HybridMor
        Symbol RawSymbol where
                basic_analysis :: Hybrid
-> Maybe
     ((H_BASIC_SPEC, HSign, GlobalAnnos)
      -> Result
           (H_BASIC_SPEC, ExtSign HSign Symbol, [Named (FORMULA H_FORMULA)]))
basic_analysis Hybrid = ((H_BASIC_SPEC, HSign, GlobalAnnos)
 -> Result
      (H_BASIC_SPEC, ExtSign HSign Symbol, [Named (FORMULA H_FORMULA)]))
-> Maybe
     ((H_BASIC_SPEC, HSign, GlobalAnnos)
      -> Result
           (H_BASIC_SPEC, ExtSign HSign Symbol, [Named (FORMULA H_FORMULA)]))
forall a. a -> Maybe a
Just (H_BASIC_SPEC, HSign, GlobalAnnos)
-> Result
     (H_BASIC_SPEC, ExtSign HSign Symbol, [Named (FORMULA H_FORMULA)])
basicHybridAnalysis
                stat_symb_map_items :: Hybrid
-> HSign
-> Maybe HSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items Hybrid = HSign
-> Maybe HSign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
                stat_symb_items :: Hybrid -> HSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items Hybrid = HSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems
                symbol_to_raw :: Hybrid -> Symbol -> RawSymbol
symbol_to_raw Hybrid = Symbol -> RawSymbol
symbolToRaw
                id_to_raw :: Hybrid -> Id -> RawSymbol
id_to_raw Hybrid = Id -> RawSymbol
idToRaw
                matches :: Hybrid -> Symbol -> RawSymbol -> Bool
matches Hybrid = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches
                empty_signature :: Hybrid -> HSign
empty_signature Hybrid = HybridSign -> HSign
forall e f. e -> Sign f e
emptySign HybridSign
emptyHybridSign
                signature_union :: Hybrid -> HSign -> HSign -> Result HSign
signature_union Hybrid s :: HSign
s = HSign -> Result HSign
forall (m :: * -> *) a. Monad m => a -> m a
return (HSign -> Result HSign)
-> (HSign -> HSign) -> HSign -> Result HSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HybridSign -> HybridSign -> HybridSign) -> HSign -> HSign -> HSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig HybridSign -> HybridSign -> HybridSign
addHybridSign HSign
s
                intersection :: Hybrid -> HSign -> HSign -> Result HSign
intersection Hybrid s :: HSign
s = HSign -> Result HSign
forall (m :: * -> *) a. Monad m => a -> m a
return (HSign -> Result HSign)
-> (HSign -> HSign) -> HSign -> Result HSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (HybridSign -> HybridSign -> HybridSign) -> HSign -> HSign -> HSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig HybridSign -> HybridSign -> HybridSign
interHybridSign HSign
s
                morphism_union :: Hybrid
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
morphism_union Hybrid = (HybridSign -> HybridSign -> HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> Morphism H_FORMULA HybridSign (DefMorExt HybridSign)
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion HybridSign -> HybridSign -> HybridSign
addHybridSign
                final_union :: Hybrid -> HSign -> HSign -> Result HSign
final_union Hybrid = (HybridSign -> HybridSign -> HybridSign)
-> HSign -> HSign -> Result HSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion HybridSign -> HybridSign -> HybridSign
addHybridSign
                is_subsig :: Hybrid -> HSign -> HSign -> Bool
is_subsig Hybrid = (HybridSign -> HybridSign -> Bool) -> HSign -> HSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig HybridSign -> HybridSign -> Bool
isSubHybridSign
                subsig_inclusion :: Hybrid
-> HSign
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
subsig_inclusion Hybrid = DefMorExt HybridSign
-> HSign
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt
                cogenerated_sign :: Hybrid
-> Set Symbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
cogenerated_sign Hybrid = DefMorExt HybridSign
-> Set Symbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt
                generated_sign :: Hybrid
-> Set Symbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
generated_sign Hybrid = DefMorExt HybridSign
-> Set Symbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt
                induced_from_morphism :: Hybrid
-> EndoMap RawSymbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
induced_from_morphism Hybrid = DefMorExt HybridSign
-> EndoMap RawSymbol
-> HSign
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt
                induced_from_to_morphism :: Hybrid
-> EndoMap RawSymbol
-> ExtSign HSign Symbol
-> ExtSign HSign Symbol
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
induced_from_to_morphism Hybrid = DefMorExt HybridSign
-> (HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> HybridSign)
-> EndoMap RawSymbol
-> ExtSign HSign Symbol
-> ExtSign HSign Symbol
-> Result (Morphism H_FORMULA HybridSign (DefMorExt HybridSign))
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism
                 DefMorExt HybridSign
forall e. DefMorExt e
emptyMorExt HybridSign -> HybridSign -> Bool
isSubHybridSign HybridSign -> HybridSign -> HybridSign
diffHybridSign
                theory_to_taxonomy :: Hybrid
-> TaxoGraphKind
-> MMiSSOntology
-> HSign
-> [Named (FORMULA H_FORMULA)]
-> Result MMiSSOntology
theory_to_taxonomy Hybrid = TaxoGraphKind
-> MMiSSOntology
-> HSign
-> [Named (FORMULA H_FORMULA)]
-> Result MMiSSOntology
forall f e.
TaxoGraphKind
-> MMiSSOntology
-> Sign f e
-> [Named (FORMULA f)]
-> Result MMiSSOntology
convTaxo

instance Logic Hybrid ()
        H_BASIC_SPEC HybridFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
        HSign
        HybridMor
        Symbol RawSymbol () where
                stability :: Hybrid -> Stability
stability _ = Stability
Experimental
                empty_proof_tree :: Hybrid -> ()
empty_proof_tree _ = ()