License	GPLv2 or higher, see LICENSE.txt
Maintainer	nevrenato@gmail.com
Stability	experimental
Portability	portable
Safe Haskell	None

TopHybrid.AS_TopHybrid

Description

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

Documentation

data TH_BSPEC s Source #

Constructors

Bspec
Fields bitems :: [TH_BASIC_ITEM] und :: s

Instances

Instances details

Data s => Data (TH_BSPEC s) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TH_BSPEC s -> c (TH_BSPEC s) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TH_BSPEC s) toConstr :: TH_BSPEC s -> Constr dataTypeOf :: TH_BSPEC s -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TH_BSPEC s)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TH_BSPEC s)) gmapT :: (forall b. Data b => b -> b) -> TH_BSPEC s -> TH_BSPEC s gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TH_BSPEC s -> r gmapQ :: (forall d. Data d => d -> u) -> TH_BSPEC s -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BSPEC s -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BSPEC s -> m (TH_BSPEC s)
Show s => Show (TH_BSPEC s) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> TH_BSPEC s -> ShowS show :: TH_BSPEC s -> String showList :: [TH_BSPEC s] -> ShowS
Generic (TH_BSPEC s)
Instance details Defined in TopHybrid.ATC_TopHybrid Associated Types type Rep (TH_BSPEC s) :: Type -> Type Methods from :: TH_BSPEC s -> Rep (TH_BSPEC s) x to :: Rep (TH_BSPEC s) x -> TH_BSPEC s
GetRange s => GetRange (TH_BSPEC s) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: TH_BSPEC s -> Range Source # rangeSpan :: TH_BSPEC s -> [Pos] Source #
FromJSON s => FromJSON (TH_BSPEC s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods parseJSON :: Value -> Parser (TH_BSPEC s) parseJSONList :: Value -> Parser [TH_BSPEC s]
ToJSON s => ToJSON (TH_BSPEC s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toJSON :: TH_BSPEC s -> Value toEncoding :: TH_BSPEC s -> Encoding toJSONList :: [TH_BSPEC s] -> Value toEncodingList :: [TH_BSPEC s] -> Encoding
ShATermConvertible s => ShATermConvertible (TH_BSPEC s)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toShATermAux :: ATermTable -> TH_BSPEC s -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TH_BSPEC s] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_BSPEC s) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH_BSPEC s])
Pretty b => Pretty (TH_BSPEC b) Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: TH_BSPEC b -> Doc Source # pretties :: [TH_BSPEC b] -> Doc Source #
type Rep (TH_BSPEC s)
Instance details Defined in TopHybrid.ATC_TopHybrid type Rep (TH_BSPEC s) = D1 ('MetaData "TH_BSPEC" "TopHybrid.AS_TopHybrid" "main" 'False) (C1 ('MetaCons "Bspec" 'PrefixI 'True) (S1 ('MetaSel ('Just "bitems") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TH_BASIC_ITEM]) :*: S1 ('MetaSel ('Just "und") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 s)))

data TH_BASIC_ITEM Source #

Constructors

Simple_mod_decl [MODALITY]
Simple_nom_decl [NOMINAL]

Instances

Instances details

Data TH_BASIC_ITEM Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TH_BASIC_ITEM -> c TH_BASIC_ITEM gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TH_BASIC_ITEM toConstr :: TH_BASIC_ITEM -> Constr dataTypeOf :: TH_BASIC_ITEM -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TH_BASIC_ITEM) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TH_BASIC_ITEM) gmapT :: (forall b. Data b => b -> b) -> TH_BASIC_ITEM -> TH_BASIC_ITEM gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TH_BASIC_ITEM -> r gmapQ :: (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_BASIC_ITEM -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_BASIC_ITEM -> m TH_BASIC_ITEM
Show TH_BASIC_ITEM Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> TH_BASIC_ITEM -> ShowS show :: TH_BASIC_ITEM -> String showList :: [TH_BASIC_ITEM] -> ShowS
Generic TH_BASIC_ITEM
Instance details Defined in TopHybrid.ATC_TopHybrid Associated Types type Rep TH_BASIC_ITEM :: Type -> Type Methods from :: TH_BASIC_ITEM -> Rep TH_BASIC_ITEM x to :: Rep TH_BASIC_ITEM x -> TH_BASIC_ITEM
GetRange TH_BASIC_ITEM Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: TH_BASIC_ITEM -> Range Source # rangeSpan :: TH_BASIC_ITEM -> [Pos] Source #
FromJSON TH_BASIC_ITEM
Instance details Defined in TopHybrid.ATC_TopHybrid Methods parseJSON :: Value -> Parser TH_BASIC_ITEM parseJSONList :: Value -> Parser [TH_BASIC_ITEM]
ToJSON TH_BASIC_ITEM
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toJSON :: TH_BASIC_ITEM -> Value toEncoding :: TH_BASIC_ITEM -> Encoding toJSONList :: [TH_BASIC_ITEM] -> Value toEncodingList :: [TH_BASIC_ITEM] -> Encoding
ShATermConvertible TH_BASIC_ITEM
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toShATermAux :: ATermTable -> TH_BASIC_ITEM -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TH_BASIC_ITEM] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_BASIC_ITEM) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH_BASIC_ITEM])
Pretty TH_BASIC_ITEM Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: TH_BASIC_ITEM -> Doc Source # pretties :: [TH_BASIC_ITEM] -> Doc Source #
type Rep TH_BASIC_ITEM
Instance details Defined in TopHybrid.ATC_TopHybrid type Rep TH_BASIC_ITEM = D1 ('MetaData "TH_BASIC_ITEM" "TopHybrid.AS_TopHybrid" "main" 'False) (C1 ('MetaCons "Simple_mod_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [MODALITY])) :+: C1 ('MetaCons "Simple_nom_decl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [NOMINAL])))

type MODALITY = SIMPLE_ID Source #

type NOMINAL = SIMPLE_ID Source #

data TH_FORMULA f Source #

Constructors

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

Instances

Instances details

Eq f => Eq (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods (==) :: TH_FORMULA f -> TH_FORMULA f -> Bool (/=) :: TH_FORMULA f -> TH_FORMULA f -> Bool
Data f => Data (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TH_FORMULA f -> c (TH_FORMULA f) gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TH_FORMULA f) toConstr :: TH_FORMULA f -> Constr dataTypeOf :: TH_FORMULA f -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TH_FORMULA f)) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TH_FORMULA f)) gmapT :: (forall b. Data b => b -> b) -> TH_FORMULA f -> TH_FORMULA f gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TH_FORMULA f -> r gmapQ :: (forall d. Data d => d -> u) -> TH_FORMULA f -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> TH_FORMULA f -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f) gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f) gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TH_FORMULA f -> m (TH_FORMULA f)
Ord f => Ord (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods compare :: TH_FORMULA f -> TH_FORMULA f -> Ordering (<) :: TH_FORMULA f -> TH_FORMULA f -> Bool (<=) :: TH_FORMULA f -> TH_FORMULA f -> Bool (>) :: TH_FORMULA f -> TH_FORMULA f -> Bool (>=) :: TH_FORMULA f -> TH_FORMULA f -> Bool max :: TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f min :: TH_FORMULA f -> TH_FORMULA f -> TH_FORMULA f
Show f => Show (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> TH_FORMULA f -> ShowS show :: TH_FORMULA f -> String showList :: [TH_FORMULA f] -> ShowS
Generic (TH_FORMULA f)
Instance details Defined in TopHybrid.ATC_TopHybrid Associated Types type Rep (TH_FORMULA f) :: Type -> Type Methods from :: TH_FORMULA f -> Rep (TH_FORMULA f) x to :: Rep (TH_FORMULA f) x -> TH_FORMULA f
GetRange f => GetRange (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: TH_FORMULA f -> Range Source # rangeSpan :: TH_FORMULA f -> [Pos] Source #
FromJSON f => FromJSON (TH_FORMULA f)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods parseJSON :: Value -> Parser (TH_FORMULA f) parseJSONList :: Value -> Parser [TH_FORMULA f]
ToJSON f => ToJSON (TH_FORMULA f)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toJSON :: TH_FORMULA f -> Value toEncoding :: TH_FORMULA f -> Encoding toJSONList :: [TH_FORMULA f] -> Value toEncodingList :: [TH_FORMULA f] -> Encoding
ShATermConvertible f => ShATermConvertible (TH_FORMULA f)
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toShATermAux :: ATermTable -> TH_FORMULA f -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [TH_FORMULA f] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, TH_FORMULA f) fromShATermList' :: Int -> ATermTable -> (ATermTable, [TH_FORMULA f])
Pretty f => Pretty (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: TH_FORMULA f -> Doc Source # pretties :: [TH_FORMULA f] -> Doc Source #
ToXml f => ToXml (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods asXml :: TH_FORMULA f -> Element Source #
ToJson f => ToJson (TH_FORMULA f) Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods asJson :: TH_FORMULA f -> Json Source #
type Rep (TH_FORMULA f)
Instance details Defined in TopHybrid.ATC_TopHybrid type Rep (TH_FORMULA f) = D1 ('MetaData "TH_FORMULA" "TopHybrid.AS_TopHybrid" "main" 'False) (((C1 ('MetaCons "At" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: (C1 ('MetaCons "Uni" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: C1 ('MetaCons "Exist" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))))) :+: ((C1 ('MetaCons "Box" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: C1 ('MetaCons "Dia" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MODALITY) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)))) :+: (C1 ('MetaCons "UnderLogic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 f)) :+: C1 ('MetaCons "Conjunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)))))) :+: (((C1 ('MetaCons "Disjunction" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: C1 ('MetaCons "Implication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)))) :+: (C1 ('MetaCons "BiImplication" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: C1 ('MetaCons "Here" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NOMINAL)))) :+: ((C1 ('MetaCons "Neg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f))) :+: C1 ('MetaCons "Par" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TH_FORMULA f)))) :+: (C1 ('MetaCons "TrueA" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FalseA" 'PrefixI 'False) (U1 :: Type -> Type)))))

data Frm_Wrap Source #

Constructors

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)

Instances

Instances details

Eq Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods (==) :: Frm_Wrap -> Frm_Wrap -> Bool (/=) :: Frm_Wrap -> Frm_Wrap -> Bool
Ord Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods compare :: Frm_Wrap -> Frm_Wrap -> Ordering (<) :: Frm_Wrap -> Frm_Wrap -> Bool (<=) :: Frm_Wrap -> Frm_Wrap -> Bool (>) :: Frm_Wrap -> Frm_Wrap -> Bool (>=) :: Frm_Wrap -> Frm_Wrap -> Bool max :: Frm_Wrap -> Frm_Wrap -> Frm_Wrap min :: Frm_Wrap -> Frm_Wrap -> Frm_Wrap
Show Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> Frm_Wrap -> ShowS show :: Frm_Wrap -> String showList :: [Frm_Wrap] -> ShowS
GetRange Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: Frm_Wrap -> Range Source # rangeSpan :: Frm_Wrap -> [Pos] Source #
FromJSON Frm_Wrap
Instance details Defined in TopHybrid.StatAna Methods parseJSON :: Value -> Parser Frm_Wrap parseJSONList :: Value -> Parser [Frm_Wrap]
ToJSON Frm_Wrap
Instance details Defined in TopHybrid.StatAna Methods toJSON :: Frm_Wrap -> Value toEncoding :: Frm_Wrap -> Encoding toJSONList :: [Frm_Wrap] -> Value toEncodingList :: [Frm_Wrap] -> Encoding
ShATermConvertible Frm_Wrap
Instance details Defined in TopHybrid.StatAna Methods toShATermAux :: ATermTable -> Frm_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Frm_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Frm_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Frm_Wrap])
Pretty Frm_Wrap Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: Frm_Wrap -> Doc Source # pretties :: [Frm_Wrap] -> Doc Source #
ToXml Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods asXml :: Frm_Wrap -> Element Source #
ToJson Frm_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods asJson :: Frm_Wrap -> Json Source #
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods map_sen :: Hybridize -> Mor -> Frm_Wrap -> Result Frm_Wrap Source # simplify_sen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> Frm_Wrap Source # negation :: Hybridize -> Frm_Wrap -> Maybe Frm_Wrap Source # print_sign :: Hybridize -> Sgn_Wrap -> Doc Source # print_named :: Hybridize -> Named Frm_Wrap -> Doc Source # sym_of :: Hybridize -> Sgn_Wrap -> [Set Symbol] Source # mostSymsOf :: Hybridize -> Sgn_Wrap -> [Symbol] Source # symmap_of :: Hybridize -> Mor -> EndoMap Symbol Source # sym_name :: Hybridize -> Symbol -> Id Source # sym_label :: Hybridize -> Symbol -> Maybe String Source # fullSymName :: Hybridize -> Symbol -> String Source # symKind :: Hybridize -> Symbol -> String Source # symsOfSen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> [Symbol] Source # pair_symbols :: Hybridize -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source # sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source # extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source # stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source # ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source # qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source # symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source # id_to_raw :: Hybridize -> Id -> RawSymbol Source # matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybridize -> Sgn_Wrap Source # add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source # signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source # is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source # subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source # generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source # induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source # is_transportable :: Hybridize -> Mor -> Bool Source # is_injective :: Hybridize -> Mor -> Bool Source # theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source # corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #
Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source # stability :: Hybridize -> Stability Source # data_logic :: Hybridize -> Maybe AnyLogic Source # top_sublogic :: Hybridize -> () Source # all_sublogics :: Hybridize -> [()] Source # bottomSublogic :: Hybridize -> Maybe () Source # sublogicDimensions :: Hybridize -> [[()]] Source # parseSublogic :: Hybridize -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source # provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source # default_prover :: Hybridize -> String Source # cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source # conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source # empty_proof_tree :: Hybridize -> () Source # syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybridize -> Maybe OMCD Source # export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source # omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source # addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # sublogicOfTheo :: Hybridize -> (Sgn_Wrap, [Frm_Wrap]) -> () Source #

data Spc_Wrap Source #

Constructors

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]

Instances

Instances details

Eq Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods (==) :: Spc_Wrap -> Spc_Wrap -> Bool (/=) :: Spc_Wrap -> Spc_Wrap -> Bool
Ord Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods compare :: Spc_Wrap -> Spc_Wrap -> Ordering (<) :: Spc_Wrap -> Spc_Wrap -> Bool (<=) :: Spc_Wrap -> Spc_Wrap -> Bool (>) :: Spc_Wrap -> Spc_Wrap -> Bool (>=) :: Spc_Wrap -> Spc_Wrap -> Bool max :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap min :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap
Show Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> Spc_Wrap -> ShowS show :: Spc_Wrap -> String showList :: [Spc_Wrap] -> ShowS
Semigroup Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods (<>) :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap # sconcat :: NonEmpty Spc_Wrap -> Spc_Wrap stimes :: Integral b => b -> Spc_Wrap -> Spc_Wrap
Monoid Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods mempty :: Spc_Wrap mappend :: Spc_Wrap -> Spc_Wrap -> Spc_Wrap mconcat :: [Spc_Wrap] -> Spc_Wrap
GetRange Spc_Wrap Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: Spc_Wrap -> Range Source # rangeSpan :: Spc_Wrap -> [Pos] Source #
FromJSON Spc_Wrap
Instance details Defined in TopHybrid.StatAna Methods parseJSON :: Value -> Parser Spc_Wrap parseJSONList :: Value -> Parser [Spc_Wrap]
ToJSON Spc_Wrap
Instance details Defined in TopHybrid.StatAna Methods toJSON :: Spc_Wrap -> Value toEncoding :: Spc_Wrap -> Encoding toJSONList :: [Spc_Wrap] -> Value toEncodingList :: [Spc_Wrap] -> Encoding
ShATermConvertible Spc_Wrap
Instance details Defined in TopHybrid.StatAna Methods toShATermAux :: ATermTable -> Spc_Wrap -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Spc_Wrap] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Spc_Wrap) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Spc_Wrap])
Pretty Spc_Wrap Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: Spc_Wrap -> Doc Source # pretties :: [Spc_Wrap] -> Doc Source #
Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods parsersAndPrinters :: Hybridize -> Map String (PrefixMap -> AParser st Spc_Wrap, Spc_Wrap -> Doc) Source # parse_basic_spec :: Hybridize -> Maybe (PrefixMap -> AParser st Spc_Wrap) Source # parseSingleSymbItem :: Hybridize -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_items :: Hybridize -> Maybe (PrefixMap -> AParser st SYMB_ITEMS) Source # parse_symb_map_items :: Hybridize -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS) Source # toItem :: Hybridize -> Spc_Wrap -> Item Source # symb_items_name :: Hybridize -> SYMB_ITEMS -> [String] Source #
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source # sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source # extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source # stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source # ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source # qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source # symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source # id_to_raw :: Hybridize -> Id -> RawSymbol Source # matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybridize -> Sgn_Wrap Source # add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source # signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source # is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source # subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source # generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source # induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source # is_transportable :: Hybridize -> Mor -> Bool Source # is_injective :: Hybridize -> Mor -> Bool Source # theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source # corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #
Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source # stability :: Hybridize -> Stability Source # data_logic :: Hybridize -> Maybe AnyLogic Source # top_sublogic :: Hybridize -> () Source # all_sublogics :: Hybridize -> [()] Source # bottomSublogic :: Hybridize -> Maybe () Source # sublogicDimensions :: Hybridize -> [[()]] Source # parseSublogic :: Hybridize -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source # provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source # default_prover :: Hybridize -> String Source # cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source # conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source # empty_proof_tree :: Hybridize -> () Source # syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybridize -> Maybe OMCD Source # export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source # omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source # addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # sublogicOfTheo :: Hybridize -> (Sgn_Wrap, [Frm_Wrap]) -> () Source #

data Mor Source #

Constructors

Mor

Instances

Instances details

Eq Mor Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods (==) :: Mor -> Mor -> Bool (/=) :: Mor -> Mor -> Bool
Data Mor Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Mor -> c Mor gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Mor toConstr :: Mor -> Constr dataTypeOf :: Mor -> DataType dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Mor) dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Mor) gmapT :: (forall b. Data b => b -> b) -> Mor -> Mor gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Mor -> r gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Mor -> r gmapQ :: (forall d. Data d => d -> u) -> Mor -> [u] gmapQi :: Int -> (forall d. Data d => d -> u) -> Mor -> u gmapM :: Monad m => (forall d. Data d => d -> m d) -> Mor -> m Mor gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Mor -> m Mor gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Mor -> m Mor
Ord Mor Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods compare :: Mor -> Mor -> Ordering (<) :: Mor -> Mor -> Bool (<=) :: Mor -> Mor -> Bool (>) :: Mor -> Mor -> Bool (>=) :: Mor -> Mor -> Bool max :: Mor -> Mor -> Mor min :: Mor -> Mor -> Mor
Show Mor Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods showsPrec :: Int -> Mor -> ShowS show :: Mor -> String showList :: [Mor] -> ShowS
Generic Mor
Instance details Defined in TopHybrid.ATC_TopHybrid Associated Types type Rep Mor :: Type -> Type Methods from :: Mor -> Rep Mor x to :: Rep Mor x -> Mor
GetRange Mor Source #
Instance details Defined in TopHybrid.AS_TopHybrid Methods getRange :: Mor -> Range Source # rangeSpan :: Mor -> [Pos] Source #
FromJSON Mor
Instance details Defined in TopHybrid.ATC_TopHybrid Methods parseJSON :: Value -> Parser Mor parseJSONList :: Value -> Parser [Mor]
ToJSON Mor
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toJSON :: Mor -> Value toEncoding :: Mor -> Encoding toJSONList :: [Mor] -> Value toEncodingList :: [Mor] -> Encoding
ShATermConvertible Mor
Instance details Defined in TopHybrid.ATC_TopHybrid Methods toShATermAux :: ATermTable -> Mor -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [Mor] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, Mor) fromShATermList' :: Int -> ATermTable -> (ATermTable, [Mor])
Pretty Mor Source #
Instance details Defined in TopHybrid.Print_AS Methods pretty :: Mor -> Doc Source # pretties :: [Mor] -> Doc Source #
Category Sgn_Wrap Mor Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods ide :: Sgn_Wrap -> Mor Source # composeMorphisms :: Mor -> Mor -> Result Mor Source # dom :: Mor -> Sgn_Wrap Source # cod :: Mor -> Sgn_Wrap Source # inverse :: Mor -> Result Mor Source # isInclusion :: Mor -> Bool Source # legal_mor :: Mor -> Result () Source #
Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods map_sen :: Hybridize -> Mor -> Frm_Wrap -> Result Frm_Wrap Source # simplify_sen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> Frm_Wrap Source # negation :: Hybridize -> Frm_Wrap -> Maybe Frm_Wrap Source # print_sign :: Hybridize -> Sgn_Wrap -> Doc Source # print_named :: Hybridize -> Named Frm_Wrap -> Doc Source # sym_of :: Hybridize -> Sgn_Wrap -> [Set Symbol] Source # mostSymsOf :: Hybridize -> Sgn_Wrap -> [Symbol] Source # symmap_of :: Hybridize -> Mor -> EndoMap Symbol Source # sym_name :: Hybridize -> Symbol -> Id Source # sym_label :: Hybridize -> Symbol -> Maybe String Source # fullSymName :: Hybridize -> Symbol -> String Source # symKind :: Hybridize -> Symbol -> String Source # symsOfSen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> [Symbol] Source # pair_symbols :: Hybridize -> Symbol -> Symbol -> Result Symbol Source #
StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods basic_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, GlobalAnnos) -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])) Source # sen_analysis :: Hybridize -> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap) Source # extBasicAnalysis :: Hybridize -> IRI -> LibName -> Spc_Wrap -> Sgn_Wrap -> GlobalAnnos -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]) Source # stat_symb_map_items :: Hybridize -> Sgn_Wrap -> Maybe Sgn_Wrap -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol) Source # stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol] Source # convertTheory :: Hybridize -> Maybe ((Sgn_Wrap, [Named Frm_Wrap]) -> Spc_Wrap) Source # ensures_amalgamability :: Hybridize -> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)], Gr String String) -> Result Amalgamates Source # quotient_term_algebra :: Hybridize -> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # signature_colimit :: Hybridize -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor) Source # qualify :: Hybridize -> SIMPLE_ID -> LibName -> Mor -> Sgn_Wrap -> Result (Mor, [Named Frm_Wrap]) Source # symbol_to_raw :: Hybridize -> Symbol -> RawSymbol Source # id_to_raw :: Hybridize -> Id -> RawSymbol Source # matches :: Hybridize -> Symbol -> RawSymbol -> Bool Source # empty_signature :: Hybridize -> Sgn_Wrap Source # add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap Source # signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap Source # morphism_union :: Hybridize -> Mor -> Mor -> Result Mor Source # is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool Source # subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor Source # generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor Source # induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor Source # induced_from_to_morphism :: Hybridize -> EndoMap RawSymbol -> ExtSign Sgn_Wrap Symbol -> ExtSign Sgn_Wrap Symbol -> Result Mor Source # is_transportable :: Hybridize -> Mor -> Bool Source # is_injective :: Hybridize -> Mor -> Bool Source # theory_to_taxonomy :: Hybridize -> TaxoGraphKind -> MMiSSOntology -> Sgn_Wrap -> [Named Frm_Wrap] -> Result MMiSSOntology Source # corresp2th :: Hybridize -> String -> Bool -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sgn_Wrap, [Named Frm_Wrap], Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # equiv2cospan :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> [SYMB_ITEMS] -> [SYMB_ITEMS] -> Result (Sgn_Wrap, Sgn_Wrap, Sgn_Wrap, EndoMap Symbol, EndoMap Symbol) Source # extract_module :: Hybridize -> [IRI] -> (Sgn_Wrap, [Named Frm_Wrap]) -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source #
Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS Sgn_Wrap Mor Symbol RawSymbol () Source #
Instance details Defined in TopHybrid.Logic_TopHybrid Methods parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap) Source # stability :: Hybridize -> Stability Source # data_logic :: Hybridize -> Maybe AnyLogic Source # top_sublogic :: Hybridize -> () Source # all_sublogics :: Hybridize -> [()] Source # bottomSublogic :: Hybridize -> Maybe () Source # sublogicDimensions :: Hybridize -> [[()]] Source # parseSublogic :: Hybridize -> String -> Maybe () Source # proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor Source # provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()] Source # default_prover :: Hybridize -> String Source # cons_checkers :: Hybridize -> [ConsChecker Sgn_Wrap Frm_Wrap () Mor ()] Source # conservativityCheck :: Hybridize -> [ConservativityChecker Sgn_Wrap Frm_Wrap Mor] Source # empty_proof_tree :: Hybridize -> () Source # syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable Source # omdoc_metatheory :: Hybridize -> Maybe OMCD Source # export_symToOmdoc :: Hybridize -> NameMap Symbol -> Symbol -> String -> Result TCElement Source # export_senToOmdoc :: Hybridize -> NameMap Symbol -> Frm_Wrap -> Result TCorOMElement Source # export_theoryToOmdoc :: Hybridize -> SigMap Symbol -> Sgn_Wrap -> [Named Frm_Wrap] -> Result [TCElement] Source # omdocToSym :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source # omdocToSen :: Hybridize -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Frm_Wrap)) Source # addOMadtToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [[OmdADT]] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # addOmdocToTheory :: Hybridize -> SigMapI Symbol -> (Sgn_Wrap, [Named Frm_Wrap]) -> [TCElement] -> Result (Sgn_Wrap, [Named Frm_Wrap]) Source # sublogicOfTheo :: Hybridize -> (Sgn_Wrap, [Frm_Wrap]) -> () Source #
type Rep Mor
Instance details Defined in TopHybrid.ATC_TopHybrid type Rep Mor = D1 ('MetaData "Mor" "TopHybrid.AS_TopHybrid" "main" 'False) (C1 ('MetaCons "Mor" 'PrefixI 'False) (U1 :: Type -> Type))