{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances,

UndecidableInstances, ExistentialQuantification #-}

{- |

Module : $Header$

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 Show

instance Language Hybridize where

description _ = "Hybridization of an arbitrary logic"

instance Category Sgn_Wrap Mor where

ide = undefined

inverse = undefined

composeMorphisms = undefined

dom = undefined

cod = undefined

isInclusion = undefined

legal_mor = undefined

instance Syntax Hybridize Spc_Wrap Symbol SYMB_ITEMS SYMB_MAP_ITEMS where

parse_basic_spec Hybridize = Just $ \ _ -> thBasic getLogic

parse_symb_items Hybridize = Just $ error "parse_symb_items !"

parse_symb_map_items Hybridize = Just $ error "parse_symb_map_items !"

toItem Hybridize = error "toItem !"

instance Sentences Hybridize Frm_Wrap Sgn_Wrap Mor Symbol where

map_sen Hybridize = error "map_sen !"

negation Hybridize = error "negation !"

sym_of Hybridize = error "sym_of !"

mostSymsOf Hybridize = error "mostSymsOf !"

symmap_of Hybridize = error "symmap_of !"

sym_name Hybridize = error "sym_name !"

symKind Hybridize = error "symKind !"

symsOfSen Hybridize = error "symsOfSen !"

simplify_sen Hybridize = simSen

print_named Hybridize = printNamedFormula

instance StaticAnalysis Hybridize Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS

Sgn_Wrap Mor Symbol RawSymbol where

basic_analysis Hybridize = Just thAna

empty_signature Hybridize = emptyHybridSign

sen_analysis Hybridize = Just anaForm'

stat_symb_map_items Hybridize = error "stat_symb_map_items !"

stat_symb_items Hybridize = error "stat_symb_items !"

signature_colimit Hybridize = error "signature_colimit !"

quotient_term_algebra Hybridize =

error "quotient_term_algebra !"

ensures_amalgamability Hybridize =

error "ensures_amalgamability !"

qualify Hybridize = error "qualify !"

symbol_to_raw Hybridize = error "symbol_to_raw !"

matches Hybridize = error "matches !"

is_transportable Hybridize = error "is_transportable !"

is_injective Hybridize = error "is_injective !"

add_symb_to_sign Hybridize = error "add_symb_to_sign !"

signature_union Hybridize = error "signature_union !"

signatureDiff Hybridize = sgnDiff

intersection Hybridize = error "intersection !"

morphism_union Hybridize = error "morphism_union !"

final_union Hybridize = error "final_union !"

is_subsig Hybridize = isSubTHybSgn

subsig_inclusion Hybridize = error "sub_sig_inclusion !"

cogenerated_sign Hybridize = error "cogenerated_sign !"

generated_sign Hybridize = error "generated_sign !"

induced_from_morphism Hybridize =

error "induced_from_morphism !"

induced_from_to_morphism Hybridize =

error "induced_from_to_morphism !"

theory_to_taxonomy Hybridize = error "theory_to_taxonomy !"

instance Logic Hybridize () Spc_Wrap Frm_Wrap SYMB_ITEMS SYMB_MAP_ITEMS

Sgn_Wrap Mor Symbol RawSymbol () where

stability Hybridize = Experimental

parse_basic_sen Hybridize = Just formParser'

proj_sublogic_epsilon Hybridize =

error "proj_sublogic_epsilon !"

all_sublogics Hybridize = error "all_sublogics !"

empty_proof_tree Hybridize = error "empty_proof_tree !"

addOMadtToTheory Hybridize = error "addOMadtToTheory !"

addOmdocToTheory Hybridize = error "addOmdocToTheory !"

syntaxTable Hybridize = error "syntaxTable !"

provers Hybridize = []

{- --- The logics supported section ----

Logics supported -}

underlogicList :: [(String, AnyLogic)]

underlogicList = [

(show CASL, Logic CASL),

(show Propositional, Logic Propositional),

(show CoCASL, Logic CoCASL),

(show Hybridize, Logic Hybridize)

]

-- Construction of the underlogics map using a list

underlogics :: M.Map String AnyLogic

underlogics = buildMapFromList 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 s = maybeE 3 $ M.lookup s underlogics