HasCASL2PCoClTyConsHOL.hs revision 03db3efebb43c12041915cb7ffcc172b191208f9
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 Data.Map as Map
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederimport qualified Data.Set as Set
70e83495a9753d2a104a9869ac2a997ac30d05c1Christian Maederimport qualified Common.Lib.Rel as Rel
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maederimport HasCASL.Unify (getTypeOf)
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder-- | The identity of the comorphism
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederdata HasCASL2PCoClTyConsHOL = HasCASL2PCoClTyConsHOL deriving Show
616b72452ce5a75ade1a11ccc2c9671b3444558eChristian Maederinstance Language HasCASL2PCoClTyConsHOL where
616b72452ce5a75ade1a11ccc2c9671b3444558eChristian Maeder language_name HasCASL2PCoClTyConsHOL = "HasCASL2HasCASLNoSubtypes"
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
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder , has_polymorphism = True
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , which_logic = max Horn $ which_logic sl
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maeder , has_eq = True } else sl
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder map_theory HasCASL2PCoClTyConsHOL = mkTheoryMapping
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder (\ sig -> return (encodeSig sig, subtAxioms $ typeMap sig))
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder (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
83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu 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
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder injMap = Map.insert injName (mkInjOrProj FunArr) $ assumps sig
21b18016469e574bd145ad07c7b0f02839677cc3Christian Maeder projMap = Map.insert projName (mkInjOrProj PFunArr) injMap
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder subtRelMap = Map.insert subtRelName subtRel projMap
70e83495a9753d2a104a9869ac2a997ac30d05c1Christian Maeder in if Rel.null $ typeRel tm1 then sig else sig
722e8a91f69209ba0e99bf799c4989801d78cf16Christian Maeder { assumps = subtRelMap
7862e8fb34d79382e93b45ce894acdd928da8a51Christian Maeder , typeMap = Map.map ( \ ti -> ti { superTypes = Set.empty } ) tm1 }
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian Maederf2Formula :: Sentence -> Sentence
62d8627183cce49c052386186ad69c95b1aa3953Christian Maederf2Formula s = case s of
62d8627183cce49c052386186ad69c95b1aa3953Christian Maeder Formula trm -> Formula $ t2term trm
62d8627183cce49c052386186ad69c95b1aa3953Christian Maedert2term :: Term -> Term
62d8627183cce49c052386186ad69c95b1aa3953Christian Maedert2term = foldTerm mapRec
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder { foldTypedTerm = \ (TypedTerm trm _ _ _) ntrm q ty ps ->
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder case getTypeOf trm of
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder Nothing -> TypedTerm ntrm q ty ps -- assume this to be the exact type
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder Just sty -> if eqStrippedType ty sty
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder then if q == InType then unitTerm trueId ps else ntrm
a608d5645ae434cdb7a1555057007301072f447eChristian Maeder prTrm = mkTerm projName (mkInjOrProjType PFunArr) [sty, ty] ps ntrm
a608d5645ae434cdb7a1555057007301072f447eChristian Maeder InType -> mkTerm defId defType [ty] ps prTrm
03db3efebb43c12041915cb7ffcc172b191208f9Christian Maeder AsType -> TypedTerm prTrm Inferred ty ps
94b9f4ce450f9508dcb30b129529d635234c52c3Christian Maeder rty = strippedType ty
94b9f4ce450f9508dcb30b129529d635234c52c3Christian Maeder rtrm = mkTerm injName (mkInjOrProjType FunArr) [sty, rty] ps ntrm
03db3efebb43c12041915cb7ffcc172b191208f9Christian Maeder in TypedTerm rtrm q ty ps }