a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-|

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiModule : $Header$

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Till Mossakowski, Uni Bremen 2002-2004

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : hets@tzi.de

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : non-portable (via Logic)

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder Provides data structures for institution comorphisms.

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett These are just collections of

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach functions between (some of) the types of logics.

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- References: see Logic.hs

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

c4b2418421546a337f83332fe0db04742dcd735dAndy Gimblett Todo:

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett Weak amalgamability, also for comorphisms

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach comorphism modifications

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach comorphisms out of sublogic relationships

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder restrictions of comorphisms to sublogics

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder morphisms and other translations via spans

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettmodule Logic.Comorphism where

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettimport Logic.Logic

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettimport Common.Lib.Set

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiimport Common.Result

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Data.Maybe

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettimport Data.Dynamic

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettimport Common.DynamicUtils

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettimport Common.AS_Annotation

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblett

929190acb9f2b2f5857dce841c5a389710895515Andy Gimblettclass (Language cid,

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Logic lid1 sublogics1

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach basic_spec1 sentence1 symb_items1 symb_map_items1

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1,

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett Logic lid2 sublogics2

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett basic_spec2 sentence2 symb_items2 symb_map_items2

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach sign2 morphism2 symbol2 raw_symbol2 proof_tree2) =>

e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski Comorphism cid

da955132262baab309a50fdffe228c9efe68251dCui Jian lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett sign1 morphism1 symbol1 raw_symbol1 proof_tree1

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski sign2 morphism2 symbol2 raw_symbol2 proof_tree2

e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski | cid -> lid1, cid -> lid2

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder

da955132262baab309a50fdffe228c9efe68251dCui Jian where

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett -- source and target logic and sublogic

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett -- the source sublogic is the maximal one for which the comorphism works

eca4db63ed0bdbd93b62678feea6e3eb80aa47bbChristian Maeder -- the target sublogic is the resulting one

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sourceLogic :: cid -> lid1

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski sourceSublogic :: cid -> sublogics1

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski targetLogic :: cid -> lid2

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski targetSublogic :: cid -> sublogics2

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- finer information of target sublogics corresponding to source sublogics

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapSublogic :: cid -> sublogics1 -> sublogics2

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- default implementation

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapSublogic cid _ = targetSublogic cid

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski -- the translation functions are partial

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach -- because the target may be a sublanguage

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski -- map_basic_spec :: cid -> basic_spec1 -> Result basic_spec2

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- cover theoroidal comorphisms as well

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder map_theory :: cid -> (sign1,[Named sentence1])

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Result (sign2,[Named sentence2])

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder map_morphism :: cid -> morphism1 -> Result morphism2

1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski map_sentence :: cid -> sign1 -> sentence1 -> Result sentence2

b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski -- also covers semi-comorphisms

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder -- with no sentence translation

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder -- - but these are spans!

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder map_symbol :: cid -> symbol1 -> Set symbol2

fbb2d28086a1860850f661fbf4af531322bac405Christian Maeder constituents :: cid -> [String]

-- default implementation

constituents cid = [language_name cid]

map_sign :: Comorphism cid

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2

=> cid -> sign1 -> Result (sign2,[Named sentence2])

map_sign cid sign = map_theory cid (sign,[])

simpleTheoryMapping :: (sign1 -> sign2) -> (sentence1 -> sentence2)

-> (sign1, [Named sentence1])

-> (sign2, [Named sentence2])

simpleTheoryMapping mapSig mapSen (sign,sens) =

(mapSig sign, map (mapNamed mapSen) sens)

mkTheoryMapping :: (Monad m) => (sign1 -> m (sign2, [Named sentence2]))

-> (sign1 -> sentence1 -> m sentence2)

-> (sign1, [Named sentence1])

-> m (sign2, [Named sentence2])

mkTheoryMapping mapSig mapSen (sign,sens) = do

(sign',sens') <- mapSig sign

sens'' <- mapM (mapNamedM $ mapSen sign) sens

return (sign',sens'++sens'')

data IdComorphism lid sublogics =

IdComorphism lid sublogics

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Show (IdComorphism lid sublogics)

where

show = language_name

idComorphismTc :: TyCon

idComorphismTc = mkTyCon "Logic.Comorphism.IdComorphism"

instance Typeable (IdComorphism lid sub) where

typeOf _ = mkTyConApp idComorphismTc []

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Language (IdComorphism lid sublogics) where

language_name (IdComorphism lid sub) =

case sublogic_names lid sub of

[] -> error "language_name IdComorphism"

h : _ -> "id_" ++ language_name lid ++ "." ++ h

instance Logic lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree =>

Comorphism (IdComorphism lid sublogics)

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

lid sublogics

basic_spec sentence symb_items symb_map_items

sign morphism symbol raw_symbol proof_tree

where

sourceLogic (IdComorphism lid _sub) = lid

targetLogic (IdComorphism lid _sub) = lid

sourceSublogic (IdComorphism _lid sub) = sub

targetSublogic (IdComorphism _lid sub) = sub

mapSublogic _ = id

map_theory _ = return

map_morphism _ = return

map_sentence _ = \_ -> return

map_symbol _ = single

constituents _ = []

data CompComorphism cid1 cid2 = CompComorphism cid1 cid2 deriving Show

tyconCompComorphism :: TyCon

tyconCompComorphism = mkTyCon "Logic.Comorphism.CompComorphism"

instance Typeable (CompComorphism cid1 cid2) where

typeOf _ = mkTyConApp tyconCompComorphism []

instance (Comorphism cid1

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

Comorphism cid2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

=> Language (CompComorphism cid1 cid2) where

language_name (CompComorphism cid1 cid2) =

language_name cid1++";"

++language_name cid2

instance (Comorphism cid1

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2

sign2 morphism2 symbol2 raw_symbol2 proof_tree2,

Comorphism cid2

lid4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4

sign4 morphism4 symbol4 raw_symbol4 proof_tree4

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3)

=> Comorphism (CompComorphism cid1 cid2)

lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1

sign1 morphism1 symbol1 raw_symbol1 proof_tree1

lid3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3

sign3 morphism3 symbol3 raw_symbol3 proof_tree3 where

sourceLogic (CompComorphism cid1 _) =

sourceLogic cid1

targetLogic (CompComorphism _ cid2) =

targetLogic cid2

sourceSublogic (CompComorphism cid1 _) =

sourceSublogic cid1

targetSublogic (CompComorphism cid1 cid2) =

mapSublogic cid2

(idcoerce (targetLogic cid1) (sourceLogic cid2)

(targetSublogic cid1))

mapSublogic (CompComorphism cid1 cid2) =

mapSublogic cid2

. idcoerce (targetLogic cid1) (sourceLogic cid2)

. mapSublogic cid1

map_sentence (CompComorphism cid1 cid2) =

\si1 se1 ->

do (si2,_) <- map_sign cid1 si1

se2 <- map_sentence cid1 si1 se1

(si2', se2') <- mcoerce (targetLogic cid1) (sourceLogic cid2)

"Mapping sentence along comorphism" (si2, se2)

map_sentence cid2 si2' se2'

map_theory (CompComorphism cid1 cid2) =

\ti1 ->

do ti2 <- map_theory cid1 ti1

ti2' <- mcoerce (targetLogic cid1) (sourceLogic cid2)

"Mapping theory along comorphism" ti2

map_theory cid2 ti2'

map_morphism (CompComorphism cid1 cid2) = \ m1 ->

do m2 <- map_morphism cid1 m1

m3 <- mcoerce (targetLogic cid1) (sourceLogic cid2)

"Mapping signature morphism along comorphism"m2

map_morphism cid2 m3

map_symbol (CompComorphism cid1 cid2) = \ s1 ->

let mycast = fromJust . mcoerce (targetLogic cid1) (sourceLogic cid2)

"Mapping symbol along comorphism"

in unions

(map (map_symbol cid2 . mycast)

(toList (map_symbol cid1 s1)))

constituents (CompComorphism cid1 cid2) =

constituents cid1 ++ constituents cid2