{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances,
             UndecidableInstances, ExistentialQuantification #-}
{- |
Module      :  ./TopHybrid/Logic_TopHybrid.hs
License     :  GPLv2 or higher, see LICENSE.txt

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

Description :
Instance of class Logic for hybridized logics
with an arbitrary logic under.
-}
module TopHybrid.Logic_TopHybrid where

import qualified Data.Map as M
import Logic.Logic
import TopHybrid.AS_TopHybrid
import TopHybrid.TopHybridSign
import TopHybrid.Parse_AS
import TopHybrid.Print_AS
import TopHybrid.StatAna
import TopHybrid.Utilities
import CASL.Morphism
import CASL.AS_Basic_CASL
import CASL.Sign

-- Import of logics
import CASL.Logic_CASL
import Propositional.Logic_Propositional
import CoCASL.Logic_CoCASL
-- End of import of logics

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

instance Language Hybridize where
 description :: Hybridize -> String
description _ = "Hybridization of an arbitrary logic"

instance Category Sgn_Wrap Mor where
 ide :: Sgn_Wrap -> Mor
ide = Sgn_Wrap -> Mor
forall a. HasCallStack => a
undefined
 inverse :: Mor -> Result Mor
inverse = Mor -> Result Mor
forall a. HasCallStack => a
undefined
 composeMorphisms :: Mor -> Mor -> Result Mor
composeMorphisms = Mor -> Mor -> Result Mor
forall a. HasCallStack => a
undefined
 dom :: Mor -> Sgn_Wrap
dom = Mor -> Sgn_Wrap
forall a. HasCallStack => a
undefined
 cod :: Mor -> Sgn_Wrap
cod = Mor -> Sgn_Wrap
forall a. HasCallStack => a
undefined
 isInclusion :: Mor -> Bool
isInclusion = Mor -> Bool
forall a. HasCallStack => a
undefined
 legal_mor :: Mor -> Result ()
legal_mor = Mor -> Result ()
forall a. HasCallStack => a
undefined

instance Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
        parse_basic_spec :: Hybridize -> Maybe (PrefixMap -> AParser st Spc_Wrap)
parse_basic_spec Hybridize = (PrefixMap -> AParser st Spc_Wrap)
-> Maybe (PrefixMap -> AParser st Spc_Wrap)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st Spc_Wrap)
 -> Maybe (PrefixMap -> AParser st Spc_Wrap))
-> (PrefixMap -> AParser st Spc_Wrap)
-> Maybe (PrefixMap -> AParser st Spc_Wrap)
forall a b. (a -> b) -> a -> b
$ \ _ -> (String -> AnyLogic) -> AParser st Spc_Wrap
forall st. (String -> AnyLogic) -> AParser st Spc_Wrap
thBasic String -> AnyLogic
getLogic
        parse_symb_items :: Hybridize -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items Hybridize = (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 a. HasCallStack => String -> a
error "parse_symb_items !"
        parse_symb_map_items :: Hybridize -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items Hybridize = (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 a. HasCallStack => String -> a
error "parse_symb_map_items !"
        toItem :: Hybridize -> Spc_Wrap -> Item
toItem Hybridize = String -> Spc_Wrap -> Item
forall a. HasCallStack => String -> a
error "toItem !"

instance Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol where
        map_sen :: Hybridize -> Mor -> Frm_Wrap -> Result Frm_Wrap
map_sen Hybridize = String -> Mor -> Frm_Wrap -> Result Frm_Wrap
forall a. HasCallStack => String -> a
error "map_sen !"
        negation :: Hybridize -> Frm_Wrap -> Maybe Frm_Wrap
negation Hybridize = String -> Frm_Wrap -> Maybe Frm_Wrap
forall a. HasCallStack => String -> a
error "negation !"
        sym_of :: Hybridize -> Sgn_Wrap -> [Set Symbol]
sym_of Hybridize = String -> Sgn_Wrap -> [Set Symbol]
forall a. HasCallStack => String -> a
error "sym_of !"
        mostSymsOf :: Hybridize -> Sgn_Wrap -> [Symbol]
mostSymsOf Hybridize = String -> Sgn_Wrap -> [Symbol]
forall a. HasCallStack => String -> a
error "mostSymsOf !"
        symmap_of :: Hybridize -> Mor -> EndoMap Symbol
symmap_of Hybridize = String -> Mor -> EndoMap Symbol
forall a. HasCallStack => String -> a
error "symmap_of !"
        sym_name :: Hybridize -> Symbol -> Id
sym_name Hybridize = String -> Symbol -> Id
forall a. HasCallStack => String -> a
error "sym_name !"
        symKind :: Hybridize -> Symbol -> String
symKind Hybridize = String -> Symbol -> String
forall a. HasCallStack => String -> a
error "symKind !"
        symsOfSen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> [Symbol]
symsOfSen Hybridize = String -> Sgn_Wrap -> Frm_Wrap -> [Symbol]
forall a. HasCallStack => String -> a
error "symsOfSen !"
        simplify_sen :: Hybridize -> Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
simplify_sen Hybridize = Sgn_Wrap -> Frm_Wrap -> Frm_Wrap
simSen
        print_named :: Hybridize -> Named Frm_Wrap -> Doc
print_named Hybridize = Named Frm_Wrap -> Doc
printNamedFormula

instance StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS
          Sgn_Wrap Mor Symbol RawSymbol where
                basic_analysis :: Hybridize
-> Maybe
     ((Spc_Wrap, Sgn_Wrap, GlobalAnnos)
      -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]))
basic_analysis Hybridize = ((Spc_Wrap, Sgn_Wrap, GlobalAnnos)
 -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]))
-> Maybe
     ((Spc_Wrap, Sgn_Wrap, GlobalAnnos)
      -> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap]))
forall a. a -> Maybe a
Just (Spc_Wrap, Sgn_Wrap, GlobalAnnos)
-> Result (Spc_Wrap, ExtSign Sgn_Wrap Symbol, [Named Frm_Wrap])
thAna
                empty_signature :: Hybridize -> Sgn_Wrap
empty_signature Hybridize = Sgn_Wrap
emptyHybridSign
                sen_analysis :: Hybridize
-> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap)
sen_analysis Hybridize = ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap)
-> Maybe ((Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap)
forall a. a -> Maybe a
Just (Spc_Wrap, Sgn_Wrap, Frm_Wrap) -> Result Frm_Wrap
anaForm'
                stat_symb_map_items :: Hybridize
-> Sgn_Wrap
-> Maybe Sgn_Wrap
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items Hybridize = String
-> Sgn_Wrap
-> Maybe Sgn_Wrap
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
forall a. HasCallStack => String -> a
error "stat_symb_map_items !"
                stat_symb_items :: Hybridize -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items Hybridize = String -> Sgn_Wrap -> [SYMB_ITEMS] -> Result [RawSymbol]
forall a. HasCallStack => String -> a
error "stat_symb_items !"
                signature_colimit :: Hybridize
-> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor)
signature_colimit Hybridize = String -> Gr Sgn_Wrap (Int, Mor) -> Result (Sgn_Wrap, Map Int Mor)
forall a. HasCallStack => String -> a
error "signature_colimit !"
                quotient_term_algebra :: Hybridize
-> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap])
quotient_term_algebra Hybridize =
                 String
-> Mor -> [Named Frm_Wrap] -> Result (Sgn_Wrap, [Named Frm_Wrap])
forall a. HasCallStack => String -> a
error "quotient_term_algebra !"
                ensures_amalgamability :: Hybridize
-> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)],
    Gr String String)
-> Result Amalgamates
ensures_amalgamability Hybridize =
                 String
-> ([CASLAmalgOpt], Gr Sgn_Wrap (Int, Mor), [(Int, Mor)],
    Gr String String)
-> Result Amalgamates
forall a. HasCallStack => String -> a
error "ensures_amalgamability !"
                qualify :: Hybridize
-> SIMPLE_ID
-> LibName
-> Mor
-> Sgn_Wrap
-> Result (Mor, [Named Frm_Wrap])
qualify Hybridize = String
-> SIMPLE_ID
-> LibName
-> Mor
-> Sgn_Wrap
-> Result (Mor, [Named Frm_Wrap])
forall a. HasCallStack => String -> a
error "qualify !"
                symbol_to_raw :: Hybridize -> Symbol -> RawSymbol
symbol_to_raw Hybridize = String -> Symbol -> RawSymbol
forall a. HasCallStack => String -> a
error "symbol_to_raw !"
                matches :: Hybridize -> Symbol -> RawSymbol -> Bool
matches Hybridize = String -> Symbol -> RawSymbol -> Bool
forall a. HasCallStack => String -> a
error "matches !"
                is_transportable :: Hybridize -> Mor -> Bool
is_transportable Hybridize = String -> Mor -> Bool
forall a. HasCallStack => String -> a
error "is_transportable !"
                is_injective :: Hybridize -> Mor -> Bool
is_injective Hybridize = String -> Mor -> Bool
forall a. HasCallStack => String -> a
error "is_injective !"
                add_symb_to_sign :: Hybridize -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap
add_symb_to_sign Hybridize = String -> Sgn_Wrap -> Symbol -> Result Sgn_Wrap
forall a. HasCallStack => String -> a
error "add_symb_to_sign !"
                signature_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
signature_union Hybridize = String -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
forall a. HasCallStack => String -> a
error "signature_union !"
                signatureDiff :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
signatureDiff Hybridize = Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
sgnDiff
                intersection :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
intersection Hybridize = String -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
forall a. HasCallStack => String -> a
error "intersection !"
                morphism_union :: Hybridize -> Mor -> Mor -> Result Mor
morphism_union Hybridize = String -> Mor -> Mor -> Result Mor
forall a. HasCallStack => String -> a
error "morphism_union !"
                final_union :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
final_union Hybridize = String -> Sgn_Wrap -> Sgn_Wrap -> Result Sgn_Wrap
forall a. HasCallStack => String -> a
error "final_union !"
                is_subsig :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Bool
is_subsig Hybridize = Sgn_Wrap -> Sgn_Wrap -> Bool
isSubTHybSgn
                subsig_inclusion :: Hybridize -> Sgn_Wrap -> Sgn_Wrap -> Result Mor
subsig_inclusion Hybridize = String -> Sgn_Wrap -> Sgn_Wrap -> Result Mor
forall a. HasCallStack => String -> a
error "sub_sig_inclusion !"
                cogenerated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor
cogenerated_sign Hybridize = String -> Set Symbol -> Sgn_Wrap -> Result Mor
forall a. HasCallStack => String -> a
error "cogenerated_sign !"
                generated_sign :: Hybridize -> Set Symbol -> Sgn_Wrap -> Result Mor
generated_sign Hybridize = String -> Set Symbol -> Sgn_Wrap -> Result Mor
forall a. HasCallStack => String -> a
error "generated_sign !"
                induced_from_morphism :: Hybridize -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor
induced_from_morphism Hybridize =
                 String -> EndoMap RawSymbol -> Sgn_Wrap -> Result Mor
forall a. HasCallStack => String -> a
error "induced_from_morphism !"
                induced_from_to_morphism :: Hybridize
-> EndoMap RawSymbol
-> ExtSign Sgn_Wrap Symbol
-> ExtSign Sgn_Wrap Symbol
-> Result Mor
induced_from_to_morphism Hybridize =
                 String
-> EndoMap RawSymbol
-> ExtSign Sgn_Wrap Symbol
-> ExtSign Sgn_Wrap Symbol
-> Result Mor
forall a. HasCallStack => String -> a
error "induced_from_to_morphism !"
                theory_to_taxonomy :: Hybridize
-> TaxoGraphKind
-> MMiSSOntology
-> Sgn_Wrap
-> [Named Frm_Wrap]
-> Result MMiSSOntology
theory_to_taxonomy Hybridize = String
-> TaxoGraphKind
-> MMiSSOntology
-> Sgn_Wrap
-> [Named Frm_Wrap]
-> Result MMiSSOntology
forall a. HasCallStack => String -> a
error "theory_to_taxonomy !"

instance Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS
               Sgn_Wrap Mor Symbol RawSymbol () where
                stability :: Hybridize -> Stability
stability Hybridize = Stability
Experimental
                parse_basic_sen :: Hybridize -> Maybe (Spc_Wrap -> AParser st Frm_Wrap)
parse_basic_sen Hybridize = (Spc_Wrap -> AParser st Frm_Wrap)
-> Maybe (Spc_Wrap -> AParser st Frm_Wrap)
forall a. a -> Maybe a
Just Spc_Wrap -> AParser st Frm_Wrap
forall st. Spc_Wrap -> AParser st Frm_Wrap
formParser'
                proj_sublogic_epsilon :: Hybridize -> () -> Sgn_Wrap -> Mor
proj_sublogic_epsilon Hybridize =
                 String -> () -> Sgn_Wrap -> Mor
forall a. HasCallStack => String -> a
error "proj_sublogic_epsilon !"
                empty_proof_tree :: Hybridize -> ()
empty_proof_tree Hybridize = String -> ()
forall a. HasCallStack => String -> a
error "empty_proof_tree !"
                addOMadtToTheory :: Hybridize
-> SigMapI Symbol
-> (Sgn_Wrap, [Named Frm_Wrap])
-> [[OmdADT]]
-> Result (Sgn_Wrap, [Named Frm_Wrap])
addOMadtToTheory Hybridize = String
-> SigMapI Symbol
-> (Sgn_Wrap, [Named Frm_Wrap])
-> [[OmdADT]]
-> Result (Sgn_Wrap, [Named Frm_Wrap])
forall a. HasCallStack => String -> a
error "addOMadtToTheory !"
                addOmdocToTheory :: Hybridize
-> SigMapI Symbol
-> (Sgn_Wrap, [Named Frm_Wrap])
-> [TCElement]
-> Result (Sgn_Wrap, [Named Frm_Wrap])
addOmdocToTheory Hybridize = String
-> SigMapI Symbol
-> (Sgn_Wrap, [Named Frm_Wrap])
-> [TCElement]
-> Result (Sgn_Wrap, [Named Frm_Wrap])
forall a. HasCallStack => String -> a
error "addOmdocToTheory !"
                syntaxTable :: Hybridize -> Sgn_Wrap -> Maybe SyntaxTable
syntaxTable Hybridize = String -> Sgn_Wrap -> Maybe SyntaxTable
forall a. HasCallStack => String -> a
error "syntaxTable !"
                provers :: Hybridize -> [Prover Sgn_Wrap Frm_Wrap Mor () ()]
provers Hybridize = []
{- --- The logics supported section ----
Logics supported -}
underlogicList :: [(String, AnyLogic)]
underlogicList :: [(String, AnyLogic)]
underlogicList = [
                   (CASL -> String
forall a. Show a => a -> String
show CASL
CASL, CASL -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic CASL
CASL),
                   (Propositional -> String
forall a. Show a => a -> String
show Propositional
Propositional, Propositional -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Propositional
Propositional),
                   (CoCASL -> String
forall a. Show a => a -> String
show CoCASL
CoCASL, CoCASL -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic CoCASL
CoCASL),
                   (Hybridize -> String
forall a. Show a => a -> String
show Hybridize
Hybridize, Hybridize -> AnyLogic
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> AnyLogic
Logic Hybridize
Hybridize)
                 ]

-- Construction of the underlogics map using a list
underlogics :: M.Map String AnyLogic
underlogics :: Map String AnyLogic
underlogics = [(String, AnyLogic)] -> Map String AnyLogic
forall a b. Ord a => [(a, b)] -> Map a b
buildMapFromList [(String, AnyLogic)]
underlogicList

{- Tries to get a logic, if it fails, then
gives an error saying that the logic in question doesn't exist -}
getLogic :: String -> AnyLogic
getLogic :: String -> AnyLogic
getLogic s :: String
s = Int -> Maybe AnyLogic -> AnyLogic
forall a. Int -> Maybe a -> a
maybeE 3 (Maybe AnyLogic -> AnyLogic) -> Maybe AnyLogic -> AnyLogic
forall a b. (a -> b) -> a -> b
$ String -> Map String AnyLogic -> Maybe AnyLogic
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup String
s Map String AnyLogic
underlogics