HasCASL2PCoClTyConsHOL.hs revision 03db3efebb43c12041915cb7ffcc172b191208f9
0f99afe251428a5600a8919dd42b26bdf8359172nd{- |
0f99afe251428a5600a8919dd42b26bdf8359172ndModule : $Header$
0f99afe251428a5600a8919dd42b26bdf8359172ndDescription : coding out subtyping
a1d62218cdb0efd0f02da1b54fd3eda91a681d98ndCopyright : (c) C.Maeder Uni Bremen 2007
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdnd
031b91a62d25106ae69d4693475c79618dd5e884fieldingMaintainer : Christian.Maeder@dfki.de
031b91a62d25106ae69d4693475c79618dd5e884fieldingStability : provisional
031b91a62d25106ae69d4693475c79618dd5e884fieldingPortability : portable
031b91a62d25106ae69d4693475c79618dd5e884fielding
031b91a62d25106ae69d4693475c79618dd5e884fieldingCoding out subtyping in analogy to (SubPCFOL= -> PCFOL=),
031b91a62d25106ae69d4693475c79618dd5e884fielding following Chap. III:3.1 of the CASL Reference Manual
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdnd
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndThe higher kinded builtin function arrow subtypes must be ignored.
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdnd-}
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdnd
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndmodule Comorphisms.HasCASL2PCoClTyConsHOL (HasCASL2PCoClTyConsHOL(..)) where
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdnd
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport Logic.Logic
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport Logic.Comorphism
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Data.Map as Map
d5d794fc2f4cc9ca6d6da17cfa2cdcd8d244bacdndimport qualified Data.Set as Set
0f99afe251428a5600a8919dd42b26bdf8359172ndimport qualified Common.Lib.Rel as Rel
0f99afe251428a5600a8919dd42b26bdf8359172ndimport Common.Id
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.Logic_HasCASL
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.Sublogic
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.TypeRel
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.As
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.AsUtils
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.Le
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.FoldTerm
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.Builtin
0f99afe251428a5600a8919dd42b26bdf8359172ndimport HasCASL.Unify (getTypeOf)
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172nd-- | The identity of the comorphism
0f99afe251428a5600a8919dd42b26bdf8359172nddata HasCASL2PCoClTyConsHOL = HasCASL2PCoClTyConsHOL deriving Show
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fndinstance Language HasCASL2PCoClTyConsHOL where
0f99afe251428a5600a8919dd42b26bdf8359172nd language_name HasCASL2PCoClTyConsHOL = "HasCASL2HasCASLNoSubtypes"
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172ndinstance Comorphism HasCASL2PCoClTyConsHOL
0f99afe251428a5600a8919dd42b26bdf8359172nd HasCASL Sublogic
0f99afe251428a5600a8919dd42b26bdf8359172nd BasicSpec Sentence SymbItems SymbMapItems
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd Env Morphism Symbol RawSymbol ()
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd HasCASL Sublogic
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd BasicSpec Sentence SymbItems SymbMapItems
0f99afe251428a5600a8919dd42b26bdf8359172nd Env Morphism Symbol RawSymbol () where
0f99afe251428a5600a8919dd42b26bdf8359172nd sourceLogic HasCASL2PCoClTyConsHOL = HasCASL
0f99afe251428a5600a8919dd42b26bdf8359172nd sourceSublogic HasCASL2PCoClTyConsHOL = top
0f99afe251428a5600a8919dd42b26bdf8359172nd targetLogic HasCASL2PCoClTyConsHOL = HasCASL
0f99afe251428a5600a8919dd42b26bdf8359172nd mapSublogic HasCASL2PCoClTyConsHOL sl = Just $ if has_sub sl then sl
0f99afe251428a5600a8919dd42b26bdf8359172nd { has_sub = False
0f99afe251428a5600a8919dd42b26bdf8359172nd , has_part = True
0f99afe251428a5600a8919dd42b26bdf8359172nd , has_polymorphism = True
0f99afe251428a5600a8919dd42b26bdf8359172nd , which_logic = max Horn $ which_logic sl
0f99afe251428a5600a8919dd42b26bdf8359172nd , has_eq = True } else sl
0f99afe251428a5600a8919dd42b26bdf8359172nd map_theory HasCASL2PCoClTyConsHOL = mkTheoryMapping
0f99afe251428a5600a8919dd42b26bdf8359172nd (\ sig -> return (encodeSig sig, subtAxioms $ typeMap sig))
0f99afe251428a5600a8919dd42b26bdf8359172nd (map_sentence HasCASL2PCoClTyConsHOL)
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd map_morphism HasCASL2PCoClTyConsHOL mor = return mor
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd { msource = encodeSig $ msource mor
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd , mtarget = encodeSig $ mtarget mor }
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd -- other components need not to be adapted!
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd map_sentence HasCASL2PCoClTyConsHOL _ = return . f2Formula
5718d2b6ea423b4eb2d45f64bbc4c8eb61e0400fnd map_symbol HasCASL2PCoClTyConsHOL _ = Set.singleton . id
0f99afe251428a5600a8919dd42b26bdf8359172nd has_model_expansion HasCASL2PCoClTyConsHOL = True
0f99afe251428a5600a8919dd42b26bdf8359172nd is_weakly_amalgamable HasCASL2PCoClTyConsHOL = True
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172nd-- | Add injection and projection symbols to a signature, remove supersorts
0f99afe251428a5600a8919dd42b26bdf8359172ndencodeSig :: Env -> Env
0f99afe251428a5600a8919dd42b26bdf8359172ndencodeSig sig = let
0f99afe251428a5600a8919dd42b26bdf8359172nd tm1 = typeMap sig
0f99afe251428a5600a8919dd42b26bdf8359172nd injMap = Map.insert injName (mkInjOrProj FunArr) $ assumps sig
0f99afe251428a5600a8919dd42b26bdf8359172nd projMap = Map.insert projName (mkInjOrProj PFunArr) injMap
0f99afe251428a5600a8919dd42b26bdf8359172nd subtRelMap = Map.insert subtRelName subtRel projMap
0f99afe251428a5600a8919dd42b26bdf8359172nd in if Rel.null $ typeRel tm1 then sig else sig
0f99afe251428a5600a8919dd42b26bdf8359172nd { assumps = subtRelMap
0f99afe251428a5600a8919dd42b26bdf8359172nd , typeMap = Map.map ( \ ti -> ti { superTypes = Set.empty } ) tm1 }
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172ndf2Formula :: Sentence -> Sentence
0f99afe251428a5600a8919dd42b26bdf8359172ndf2Formula s = case s of
0f99afe251428a5600a8919dd42b26bdf8359172nd Formula trm -> Formula $ t2term trm
0f99afe251428a5600a8919dd42b26bdf8359172nd _ -> s
0f99afe251428a5600a8919dd42b26bdf8359172nd
0f99afe251428a5600a8919dd42b26bdf8359172ndt2term :: Term -> Term
0f99afe251428a5600a8919dd42b26bdf8359172ndt2term = foldTerm mapRec
0f99afe251428a5600a8919dd42b26bdf8359172nd { foldTypedTerm = \ (TypedTerm trm _ _ _) ntrm q ty ps ->
0f99afe251428a5600a8919dd42b26bdf8359172nd case getTypeOf trm of
0f99afe251428a5600a8919dd42b26bdf8359172nd Nothing -> TypedTerm ntrm q ty ps -- assume this to be the exact type
0f99afe251428a5600a8919dd42b26bdf8359172nd Just sty -> if eqStrippedType ty sty
0f99afe251428a5600a8919dd42b26bdf8359172nd then if q == InType then unitTerm trueId ps else ntrm
0f99afe251428a5600a8919dd42b26bdf8359172nd else let
0f99afe251428a5600a8919dd42b26bdf8359172nd prTrm = mkTerm projName (mkInjOrProjType PFunArr) [sty, ty] ps ntrm
0f99afe251428a5600a8919dd42b26bdf8359172nd in case q of
0f99afe251428a5600a8919dd42b26bdf8359172nd InType -> mkTerm defId defType [ty] ps prTrm
0f99afe251428a5600a8919dd42b26bdf8359172nd AsType -> TypedTerm prTrm Inferred ty ps
0f99afe251428a5600a8919dd42b26bdf8359172nd _ -> let
0f99afe251428a5600a8919dd42b26bdf8359172nd rty = strippedType ty
0f99afe251428a5600a8919dd42b26bdf8359172nd rtrm = mkTerm injName (mkInjOrProjType FunArr) [sty, rty] ps ntrm
0f99afe251428a5600a8919dd42b26bdf8359172nd in TypedTerm rtrm q ty ps }
0f99afe251428a5600a8919dd42b26bdf8359172nd