HasCASL2PCoClTyConsHOL.hs revision 7862e8fb34d79382e93b45ce894acdd928da8a51
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederModule : $Header$
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederDescription : coding out subtyping
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederCopyright : (c) C.Maeder Uni Bremen 2007
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederMaintainer : Christian.Maeder@dfki.de
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederStability : provisional
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederPortability : portable
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederCoding out subtyping in analogy to (SubPCFOL= -> PCFOL=),
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder following Chap. III:3.1 of the CASL Reference Manual
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederThe higher kinded builtin function arrow subtypes must be ignored.
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maedermodule Comorphisms.HasCASL2PCoClTyConsHOL (HasCASL2PCoClTyConsHOL(..)) where
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport qualified Common.Lib.Rel as Rel
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maederimport qualified Data.Map as Map
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport qualified Data.Set as Set
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder-- | The identity of the comorphism
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederdata HasCASL2PCoClTyConsHOL = HasCASL2PCoClTyConsHOL deriving Show
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederinstance Language HasCASL2PCoClTyConsHOL
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederinstance Comorphism HasCASL2PCoClTyConsHOL
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder HasCASL Sublogic
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder BasicSpec Sentence SymbItems SymbMapItems
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder Env Morphism Symbol RawSymbol ()
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder HasCASL Sublogic
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder BasicSpec Sentence SymbItems SymbMapItems
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder Env Morphism Symbol RawSymbol () where
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder sourceLogic HasCASL2PCoClTyConsHOL = HasCASL
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder sourceSublogic HasCASL2PCoClTyConsHOL = top
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder targetLogic HasCASL2PCoClTyConsHOL = HasCASL
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder mapSublogic HasCASL2PCoClTyConsHOL sl = Just $ if has_sub sl then sl
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder { has_sub = False
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , has_part = True
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , which_logic = max Horn $ which_logic sl
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , has_eq = True } else sl
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder map_theory HasCASL2PCoClTyConsHOL = mkTheoryMapping ( \ sig ->
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder let e = encodeSig sig in
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder return (e, [])) (map_sentence HasCASL2PCoClTyConsHOL)
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder map_morphism HasCASL2PCoClTyConsHOL mor = return mor
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder { msource = encodeSig $ msource mor
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , mtarget = encodeSig $ mtarget mor }
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder -- other components need not to be adapted!
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder map_sentence HasCASL2PCoClTyConsHOL _ = return . f2Formula
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder map_symbol HasCASL2PCoClTyConsHOL = Set.singleton . id
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder has_model_expansion HasCASL2PCoClTyConsHOL = True
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder is_weakly_amalgamable HasCASL2PCoClTyConsHOL = True
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder-- | Add injection and projection symbols to a signature, remove supersorts
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederencodeSig :: Env -> Env
bb4d3b6e93db1495f02de46aff5076862e30517bChristian MaederencodeSig sig = let
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder tm1 = typeMap sig
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder tr = Rel.toSet $ typeRel tm1
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder tm = addUnit (classMap sig) tm1
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder injs = Set.map (mkInjOrProj True tm) tr
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder projs = Set.map (mkInjOrProj False tm) tr
bb4d3b6e93db1495f02de46aff5076862e30517bChristian Maeder in sig { assumps = Map.insert injName injs
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder $ Map.insert projName projs $ assumps sig
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder , typeMap = Map.map ( \ ti -> ti { superTypes = Set.empty } ) tm1 }
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederf2Formula :: Sentence -> Sentence
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederf2Formula = id