CASL2PCFOL.hs revision afaa83a4ca9cab6b8db80a7d07b8e9823d1d04ab
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederDescripzion : coding out subsorting
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederCopyright : (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2005
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCoding out subsorting (SubPCFOL= -> PCFOL=),
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder following Chap. III:3.1 of the CASL Reference Manual
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport qualified Data.Set as Set
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maederimport qualified Common.Lib.Rel as Rel
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport CASL.Sublogic as Sublogic
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | The identity of the comorphism
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata CASL2PCFOL = CASL2PCFOL deriving (Show)
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichinstance Language CASL2PCFOL -- default definition is okay
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Comorphism CASL2PCFOL
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder CASL CASL_Sublogics
4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Symbol RawSymbol ProofTree
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder CASL CASL_Sublogics
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder Symbol RawSymbol ProofTree where
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder sourceLogic CASL2PCFOL = CASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sourceSublogic CASL2PCFOL = Sublogic.caslTop
e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder targetLogic CASL2PCFOL = CASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder mapSublogic CASL2PCFOL sl = Just $
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder if has_sub sl then -- subsorting is coded out
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder sl { sub_features = NoSub
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , has_part = True
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder , which_logic = max Horn
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder $ which_logic sl
f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder , has_eq = True}
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder map_theory CASL2PCFOL = mkTheoryMapping ( \ sig ->
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder let e = encodeSig sig in
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder return (e, map (mapNamed $ injFormula id) (monotonicities sig)
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder ++ generateAxioms sig))
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder (map_sentence CASL2PCFOL)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder map_morphism CASL2PCFOL mor = return
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder (mor { msource = encodeSig $ msource mor,
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder mtarget = encodeSig $ mtarget mor })
d0279930f87bf39843e0bd2992a4789322662144Christian Maeder -- other components need not to be adapted!
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder map_sentence CASL2PCFOL _ = return . f2Formula
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder map_symbol CASL2PCFOL _ = Set.singleton . id
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder has_model_expansion CASL2PCFOL = True
09d6f5d326545acfea43d3ffe1493c2176366475Christian Maeder is_weakly_amalgamable CASL2PCFOL = True
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder-- | Add injection, projection and membership symbols to a signature
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian MaederencodeSig :: Sign f e -> Sign f e
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder = if Rel.null rel then sig else
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder sig{sortRel = Rel.empty, opMap = projOpMap}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder rel = sortRel sig
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder total (s, s') = OpType{opKind = Total, opArgs = [s], opRes = s'}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder partial (s, s') = OpType{opKind = if Rel.member s' s rel
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder else Partial, opArgs = [s'], opRes = s}
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder setinjOptype = Set.map total $ Rel.toSet rel
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder setprojOptype = Set.map partial $ Rel.toSet rel
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder injOpMap = Set.fold (\ t -> addOpTo (uniqueInjName $ toOP_TYPE t) t)
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder (opMap sig) setinjOptype
b9b331bded61b8860edacac91df16ee19e465b42Christian Maeder projOpMap = Set.fold (\ t -> addOpTo (uniqueProjName $ toOP_TYPE t) t)
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder injOpMap setprojOptype
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder -- membership predicates are coded out
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich-- | Make the name for the embedding or projecton injectivity axiom
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichmkInjectivityName :: String -> SORT -> SORT -> String
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus LuettichmkInjectivityName str s s' =
f8e1a1eca871a26a535a4ee7d51902ba94b1db1eChristian Maeder "ga_" ++ str ++ "_injectivity_" ++ show s ++ "_to_" ++ show s'
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- | Make the name for the embedding injectivity axiom
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian MaedermkEmbInjName :: SORT -> SORT -> String
363939beade943a02b31004cea09dec34fa8a6d9Christian MaedermkEmbInjName = mkInjectivityName "embedding"
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich-- | Make the name for the projection injectivity axiom
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedermkProjInjName :: SORT -> SORT -> String
797ccd67cb8ae127be097cd43448801b673e3b69Christian MaedermkProjInjName s s' = mkInjectivityName "projection" s' s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermkInjectivity :: (TERM () -> TERM ()) -> VAR_DECL -> VAR_DECL -> FORMULA ()
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian MaedermkInjectivity f vx vy = mkForall [vx, vy]
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder (mkInjImpl f (toQualVar vx) $ toQualVar vy) nullRange
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedermkInjImpl :: (TERM () -> TERM ()) -> TERM () -> TERM () -> FORMULA ()
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedermkInjImpl f x y = mkImpl (mkExEq (f x) (f y)) (mkExEq x y)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- | Make the named sentence for the embedding injectivity axiom from s to s'
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder-- i.e., forall x,y:s . inj(x)=e=inj(y) => x=e=y
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermkEmbInjAxiom:: SORT -> SORT -> Named (FORMULA ())
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermkEmbInjAxiom s s' = let appInj q = injectUnique nullRange q s' in
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jiang makeNamed (mkEmbInjName s s')
64d532f676706149814b58c97cd064ca5993cccfChristian Maeder $ mkInjectivity appInj (mkVarDeclStr "x" s) $ mkVarDeclStr "y" s
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder-- | Make the named sentence for the projection injectivity axiom from s' to s
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder-- i.e., forall x,y:s . pr(x)=e=pr(y) => x=e=y
498aa48bdb931ab50990d3b74318a5db2312186cChristian MaedermkProjInjAxiom:: SORT -> SORT -> Named (FORMULA ())
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedermkProjInjAxiom s s' = let appProj q = projectUnique Partial nullRange q s in
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder makeNamed (mkProjInjName s s')
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder $ mkInjectivity appProj (mkVarDeclStr "x" s') $ mkVarDeclStr "y" s'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Make the name for the projection axiom
61fa0ac06ede811c7aad54ec4c4202346727368eChristian MaedermkProjName :: SORT -> SORT -> String
c0c2380bced8159ff0297ece14eba948bd236471Christian MaedermkProjName s s' =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "ga_projection_" ++ show s ++ "_to_" ++ show s' ++ "_to_" ++ show s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Make the named sentence for the projection axiom from s' to s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- i.e., forall x:s . pr(inj(x))=e=x
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermkProjAxiom:: SORT -> SORT -> Named (FORMULA ())
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedermkProjAxiom s s' =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder makeNamed (mkProjName s s')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder $ (mkForall [vx]
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian Maeder (appProj $ injectUnique nullRange qualX s')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder where appProj x = projectUnique Partial nullRange x s
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder vx = mkVarDeclStr "x" s
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder qualX = toQualVar vx
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder-- | Make the name for the transitivity axiom from s to s' to s''
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian MaedermkTransAxiomName :: SORT -> SORT -> SORT -> String
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaedermkTransAxiomName s s' s'' =
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder "ga_transitivity_" ++ show s ++ "_to_" ++ show s' ++ "_to_" ++ show s''
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder-- | Make the named sentence for the transitivity axiom from s to s' to s''
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder-- i.e., forall x:s . inj(inj(x))=e=inj(x)
2d130d212db7208777ca896a7ecad619a8944971Christian MaedermkTransAxiom:: SORT -> SORT -> SORT -> Named (FORMULA ())
2d130d212db7208777ca896a7ecad619a8944971Christian MaedermkTransAxiom s s' s'' =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder makeNamed name
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder (mkForall [vx]
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (injectUnique nullRange (injectUnique nullRange qualX s') s'')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (injectUnique nullRange qualX s'')
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder where name = mkTransAxiomName s s' s''
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder vx = mkVarDeclStr "x" s
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder qualX = toQualVar vx
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder-- | Make the name for the identity axiom from s to s'
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaedermkIdAxiomName :: SORT -> SORT -> String
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian MaedermkIdAxiomName s s' =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder "ga_identity_" ++ show s ++ "_to_" ++ show s' ++ "_to_" ++ show s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-- | Make the named sentence for the identity axiom from s to s'
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder-- i.e., forall x:s . inj(inj(x))=e=x
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermkIdAxiom:: SORT -> SORT -> Named (FORMULA ())
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaedermkIdAxiom s s' =
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder makeNamed name
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (mkForall [vx]
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder (injectUnique nullRange (injectUnique nullRange qualX s') s)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder where name = mkIdAxiomName s s'
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder vx = mkVarDeclStr "x" s
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder qualX = toQualVar vx
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergenerateAxioms :: Sign f e -> [Named (FORMULA ())]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedergenerateAxioms sig = map (mapNamed $ renameFormula id) $ concat $
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder [[mkEmbInjAxiom s s'] ++ [mkProjInjAxiom s s'] ++ [mkProjAxiom s s']
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder | s <- sorts,
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder s' <- realSupers s]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ++ [[mkTransAxiom s s' s'']
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder | s <- sorts,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder s' <- realSupers s,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder s'' <- realSupers s',
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder ++ [[mkIdAxiom s s']
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder | s <- sorts,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder s' <- realSupers s,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder Set.member s $ supersortsOf s' sig]
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder realSupers so = Set.toList $ supersortsOf so sig
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder sorts = Set.toList $ sortSet sig
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maederf2Formula :: FORMULA f -> FORMULA f
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maederf2Formula = projFormula Partial id . injFormula id
363939beade943a02b31004cea09dec34fa8a6d9Christian Maedert2Term :: TERM f -> TERM f
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maedert2Term = projTerm Partial id . injTerm id