d29201dd5328b88140ce050100693c501852657dChristian Maeder{-# LANGUAGE MultiParamTypeClasses #-}
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederDescription : coding out subtyping
cf7e0d6750e408ddb47545d6b8349a70cf0b47afChristian MaederCopyright : (c) C.Maeder Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.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.
f876a858a3644fa16b793afb4692cf353fa13762Christian 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
bc994dca195712fe9143e074ed479077f9bab75dChristian Maeder (\ sig -> return (encodeSig sig, monos 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
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder in if Rel.nullKeys $ 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
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder { foldTypedTerm = \ o ntrm q ty ps ->
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder let origTerm = TypedTerm ntrm q ty ps
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder TypedTerm trm _ _ _ = o
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder in case getTypeOf trm of
c72f409b411e817f42a1c18f49cf9b8190d51ea3Christian Maeder Nothing -> origTerm -- assume this to be the exact type
e9490701e16d1e8abd995ef876d6f937da93b412Christian Maeder Just sty -> if eqStrippedType ty sty
c72f409b411e817f42a1c18f49cf9b8190d51ea3Christian Maeder then if q == InType then unitTerm trueId ps else
c72f409b411e817f42a1c18f49cf9b8190d51ea3Christian Maeder if q == OfType then origTerm else ntrm
24b61080d4414cdc68c92ecd4d0f93996c73a1a8Christian Maeder prTrm = mkTermInst
24b61080d4414cdc68c92ecd4d0f93996c73a1a8Christian Maeder (if q == InType then UserGiven else Infer)
24b61080d4414cdc68c92ecd4d0f93996c73a1a8Christian Maeder projName (mkInjOrProjType PFunArr) [sty, ty] ps ntrm
a608d5645ae434cdb7a1555057007301072f447eChristian Maeder InType -> mkTerm defId defType [ty] ps prTrm
03db3efebb43c12041915cb7ffcc172b191208f9Christian Maeder AsType -> TypedTerm prTrm Inferred ty ps
2b470a98ae13b1a87d53f64c3188c8ea77600d99Christian Maeder rty = case getTypeAppl ty of
2b470a98ae13b1a87d53f64c3188c8ea77600d99Christian Maeder (TypeName l _ _, [lt]) | l == lazyTypeId -> lt
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder {- do not create injections into lazy types
f876a858a3644fa16b793afb4692cf353fa13762Christian Maeder (via strippedType all function arrows became partial) -}
94b9f4ce450f9508dcb30b129529d635234c52c3Christian Maeder rtrm = mkTerm injName (mkInjOrProjType FunArr) [sty, rty] ps ntrm
03db3efebb43c12041915cb7ffcc172b191208f9Christian Maeder in TypedTerm rtrm q ty ps }