HasCASL2PCoClTyConsHOL.hs revision bb4d3b6e93db1495f02de46aff5076862e30517b
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesModule : $Header$
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesDescription : coding out subtyping
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCopyright : (c) C.Maeder Uni Bremen 2007
b819d97849e89dad276b0e079414a1012aa1ead4fuankgLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b819d97849e89dad276b0e079414a1012aa1ead4fuankgMaintainer : Christian.Maeder@dfki.de
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesStability : provisional
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesPortability : portable
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesCoding out subtyping in analogy to (SubPCFOL= -> PCFOL=),
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes following Chap. III:3.1 of the CASL Reference Manual
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesThe higher kinded builtin function arrow subtypes must be ignored.
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesmodule Comorphisms.HasCASL2PCoClTyConsHOL (HasCASL2PCoClTyConsHOL(..)) where
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesimport qualified Common.Lib.Rel as Rel
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesimport qualified Data.Map as Map
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesimport qualified Data.Set as Set
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes-- | The identity of the comorphism
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesdata HasCASL2PCoClTyConsHOL = HasCASL2PCoClTyConsHOL deriving Show
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesinstance Language HasCASL2PCoClTyConsHOL
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesinstance Comorphism HasCASL2PCoClTyConsHOL
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg HasCASL Sublogic
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg BasicSpec Sentence SymbItems SymbMapItems
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg Env Morphism Symbol RawSymbol ()
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes HasCASL Sublogic
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg BasicSpec Sentence SymbItems SymbMapItems
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg Env Morphism Symbol RawSymbol () where
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg sourceLogic HasCASL2PCoClTyConsHOL = HasCASL
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg sourceSublogic HasCASL2PCoClTyConsHOL = top
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg targetLogic HasCASL2PCoClTyConsHOL = HasCASL
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg mapSublogic HasCASL2PCoClTyConsHOL sl = Just $ if has_sub sl then sl
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg { has_sub = False
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg , has_part = True
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg , which_logic = max Horn $ which_logic sl
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg , has_eq = True } else sl
8492a2583e10c69f40de92f9d5da884b64d9f379fuankg map_theory HasCASL2PCoClTyConsHOL = mkTheoryMapping ( \ sig ->
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg let e = encodeSig sig in
3630dd34e2b231b30ab9b541f9e5445852e33e80fuankg return (e, monotonicities sig ++ generateAxioms sig))
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes (map_sentence HasCASL2PCoClTyConsHOL)
c78d5d52a36b67ddfabc4e2edb9d04ce022abe76bnicholes map_morphism HasCASL2PCoClTyConsHOL mor = return mor
c78d5d52a36b67ddfabc4e2edb9d04ce022abe76bnicholes { msource = encodeSig $ msource mor
c78d5d52a36b67ddfabc4e2edb9d04ce022abe76bnicholes , mtarget = encodeSig $ mtarget mor }
c78d5d52a36b67ddfabc4e2edb9d04ce022abe76bnicholes -- other components need not to be adapted!
c78d5d52a36b67ddfabc4e2edb9d04ce022abe76bnicholes map_sentence HasCASL2PCoClTyConsHOL _ = return . f2Formula
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes map_symbol HasCASL2PCoClTyConsHOL = Set.singleton . id
e097a47d2f32eaf74a6130e6fadfa3e24b8cb2effuankg has_model_expansion HasCASL2PCoClTyConsHOL = True
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes is_weakly_amalgamable HasCASL2PCoClTyConsHOL = True
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes-- | Add injection, projection and membership symbols to a signature
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesencodeSig :: Env -> Env
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesencodeSig sig = let
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes tm1 = typeMap sig
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes tr = Rel.toSet $ typeRel tm1
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes tm = addUnit (classMap sig) tm1
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes injs = Set.map (mkInjOrProj True tm) tr
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes projs = Set.map (mkInjOrProj False tm) tr
bb2b38cd44b032118359afbc743efbea12f48e61bnicholes in sig { assumps = Map.insert injName injs
ae2a7200f0b172b7caaeb39bdf9a4724517b6527fuankg $ Map.insert projName projs $ assumps sig }
ae2a7200f0b172b7caaeb39bdf9a4724517b6527fuankggenerateAxioms :: Env -> [Named Sentence]
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesgenerateAxioms _ = []
ae2a7200f0b172b7caaeb39bdf9a4724517b6527fuankgmonotonicities :: Env -> [Named Sentence]
ae2a7200f0b172b7caaeb39bdf9a4724517b6527fuankgmonotonicities _ = []
bb2b38cd44b032118359afbc743efbea12f48e61bnicholesf2Formula :: Sentence -> Sentence
ae2a7200f0b172b7caaeb39bdf9a4724517b6527fuankgf2Formula = id