{-# OPTIONS -fno-warn-missing-methods #-}

{- HetCATS/CASL/Logic_CASL.hs

$Id$

Authors: Klaus L�ttich

Year: 2002

Here is the place where the class Logic is instantiated for CASL.

Also the instances for Syntax an Category.

todo:

- writing real functions

-}

module Logic_CASL where

import AS_Basic_CASL

import Print_AS_Basic

import Parse_AS_Basic

import SymbolParser

import ParsecInterface

import AnnoState(emptyAnnos)

import Sign

import Logic

import qualified Sublogics

import qualified Static

-- a dummy datatype for the LogicGraph and for identifying the right

-- instances

data CASL = CASL deriving (Show)

instance Language CASL where -- default definition is okay

instance Category CASL Sign Morphism

where

-- ide :: id -> object -> morphism

ide CASL sigma = Morphism { msource = sigma,

mtarget = sigma

}

-- o :: id -> morphism -> morphism -> Maybe morphism

comp CASL sigma1 sigma2 = Just sigma1 -- ???

-- dom, cod :: id -> morphism -> object

dom CASL _ = emptySign

cod CASL _ = emptySign

-- legal_obj :: id -> object -> Bool

legal_obj CASL _ = fun_err "legall_obj"

-- legal_mor :: id -> morphism -> Bool

legal_mor CASL _ = fun_err "legal_mor"

-- abstract syntax, parsing (and printing)

instance Syntax CASL BASIC_SPEC

SYMB_ITEMS SYMB_MAP_ITEMS

where

parse_basic_spec CASL = Just(toParseFun basicSpec emptyAnnos)

parse_symb_items CASL = Just(toParseFun symbItems ())

parse_symb_map_items CASL = Just(toParseFun symbMapItems ())

-- lattices (for sublogics)

instance LatticeWithTop Sublogics.CASL_Sublogics where

-- meet, join :: l -> l -> l

meet = Sublogics.sublogics_min

join = Sublogics.sublogics_max

-- top :: l

top = Sublogics.top

-- CASL logic

instance Sentences CASL Sentence () Sign Morphism Symbol where

-- missing

instance StaticAnalysis CASL BASIC_SPEC Sentence ()

SYMB_ITEMS SYMB_MAP_ITEMS

Sign

Morphism

Symbol RawSymbol where

basic_analysis CASL = Just Static.basicAnalysis

stat_symb_map_items CASL = Static.statSymbMapItems

stat_symb_items CASL = Static.statSymbItems

-- ensures_amalgamability :: id

-- -> (Diagram Sign Morphism, Node, Sign, LEdge Morphism, Morphism)

-- -> Result (Diagram Sign Morphism)

sign_to_basic_spec CASL sigma sens = Basic_spec []

symbol_to_raw CASL = Static.symbolToRaw

id_to_raw CASL = Static.idToRaw

sym_of CASL = Static.symOf

symmap_of CASL = Static.symmapOf

matches CASL = Static.matches

sym_name CASL = Static.symName

-- add_sign :: id -> Sign -> Sign -> Sign

empty_signature CASL = emptySign

signature_union CASL sigma1 sigma2 = return sigma1 -- ??? incorrect

morphism_union CASL mor1 mor2 = return mor1 -- ??? incorrect

-- final_union :: id -> Sign -> Sign -> Result Sign

is_subsig CASL = Static.isSubSig

cogenerated_sign CASL rsys sigma = return (ide CASL sigma)

generated_sign CASL rsys sigma = return (ide CASL sigma)

-- generated_sign, cogenerated_sign :: id -> [RawSymbol]

-- -> Sign -> Result Morphism

induced_from_morphism CASL rmap sigma = return (ide CASL sigma) -- ???

induced_from_to_morphism CASL rmap sigmaS sigmaT =

return (ide CASL sigmaS) -- ???

--induced_from_to_morphism :: id -> EndoMap RawSymbol

-- -> Sign -> Sign -> Result Morphism

-- extend_morphism :: id -> Sign -> Morphism -> Sign -> Sign

-- -> Result Morphism

instance Logic CASL Sublogics.CASL_Sublogics

BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS

Sign

Morphism

Symbol RawSymbol () where

sublogic_names CASL = Sublogics.sublogics_name

all_sublogics CASL = Sublogics.sublogics_all

is_in_basic_spec CASL = Sublogics.in_basic_spec

is_in_sentence CASL = Sublogics.in_sentence

is_in_symb_items CASL = Sublogics.in_symb_items

is_in_symb_map_items CASL = Sublogics.in_symb_map_items

is_in_sign CASL = Sublogics.in_sign

is_in_morphism CASL = Sublogics.in_morphism

is_in_symbol CASL = Sublogics.in_symbol

min_sublogic_basic_spec CASL = Sublogics.sl_basic_spec

min_sublogic_sentence CASL = Sublogics.sl_sentence

min_sublogic_symb_items CASL = Sublogics.sl_symb_items

min_sublogic_symb_map_items CASL = Sublogics.sl_symb_map_items

min_sublogic_sign CASL = Sublogics.sl_sign

min_sublogic_morphism CASL = Sublogics.sl_morphism

min_sublogic_symbol CASL = Sublogics.sl_symbol

proj_sublogic_basic_spec CASL = Sublogics.pr_basic_spec

proj_sublogic_symb_items CASL = Sublogics.pr_symb_items

proj_sublogic_symb_map_items CASL = Sublogics.pr_symb_map_items

proj_sublogic_sign CASL = Sublogics.pr_sign

proj_sublogic_morphism CASL = Sublogics.pr_morphism

proj_sublogic_epsilon CASL = Sublogics.pr_epsilon

proj_sublogic_symbol CASL = Sublogics.pr_symbol

---- helpers ---------------------------------

fun_err :: String -> a

fun_err fname =

error ("*** Function \"" ++ fname ++ "\" is not yet implemented!")

----------------------------------------------