CASL2SubCFOL.inline.hs revision 18a4d5cb6828f080db9c5f9551785c5151027271
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederModule : $Header$
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederCopyright : (c) Zicheng Wang, C.Maeder Uni Bremen 2002-2005
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederMaintainer : maeder@tzi.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederCoding out partiality (SubPCFOL= -> SubCFOL=),
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport qualified Common.Lib.Map as Map
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport qualified Common.Lib.Set as Set
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport qualified Common.Lib.Rel as Rel
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport CASL.Sublogic hiding(bottom)
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettich-- | The identity of the comorphism
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichdata CASL2SubCFOL = CASL2SubCFOL deriving (Show)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederinstance Language CASL2SubCFOL -- default definition is okay
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederinstance Comorphism CASL2SubCFOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder CASL CASL_Sublogics
ac0bbbcb2774629bb87986e69cf53d3402c5f575Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
2e2094a642e3775b0d76b890556407941d3a53b6Christian Maeder Symbol RawSymbol ()
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder CASL CASL_Sublogics
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Symbol RawSymbol () where
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder sourceLogic CASL2SubCFOL = CASL
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder sourceSublogic CASL2SubCFOL = CASL_SL
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich { has_sub = True,
e62d49c0dc2893da75faad896bd135e2e9a7087bKlaus Luettich has_part = True,
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich has_cons = True,
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich has_eq = True,
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder has_pred = True,
caa7f6cdf9f7d08300b4b17f1eaca30fdc6c94e1Christian Maeder which_logic = FOL
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich targetLogic CASL2SubCFOL = CASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder targetSublogic CASL2SubCFOL = CASL_SL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder { has_sub = True,
55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder has_part = False, -- partiality is coded out
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder has_cons = True,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder has_eq = True,
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder has_pred = True,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder which_logic = FOL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder map_theory CASL2SubCFOL = mkTheoryMapping ( \ sig ->
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder let e = encodeSig sig in return (e, generateAxioms sig))
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder (map_sentence CASL2SubCFOL)
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder map_morphism CASL2SubCFOL mor = return
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder (mor { msource = encodeSig $ msource mor,
cdd280437686b1e2e25e3761d4adf3d4a0a2d11cKlaus Luettich mtarget = encodeSig $ mtarget mor })
96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maeder -- other components need not to be adapted!
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder map_sentence CASL2SubCFOL sig = return . codeFormula (sortSet sig)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder map_symbol CASL2SubCFOL = Set.singleton . id
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowski-- | Add projections to the signature
c55a0f77be7e88d3620b419ec8961f4379a586e3Klaus LuettichencodeSig :: Sign f e -> Sign f e
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus LuettichencodeSig sig = sig { opMap = projOpMap, predMap = newpredMap }
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder newTotalMap = Map.map (Set.map $ makeTotal Total) $ opMap sig
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder botType x = OpType {opKind = Total, opArgs=[], opRes=x }
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder bsorts = sortSet sig -- all sorts must be considered for as and in forms
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder botTypes = Set.map botType bsorts
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder botOpMap = Map.insert bottom botTypes newTotalMap
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder defType x = PredType{predArgs=[x]}
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder defTypes = Set.map defType bsorts
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder newpredMap = Map.insert defPred defTypes $ predMap sig
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder rel = Rel.irreflex $ sortRel sig
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder total (s, s') = OpType{opKind = Total, opArgs = [s], opRes = s'}
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder setprojOptype = Set.map total $ Rel.toSet rel
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder projOpMap = Map.insert projName setprojOptype $ botOpMap
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergenerateAxioms :: Eq f => Sign f e -> [Named (FORMULA f)]
9e748851c150e1022fb952bab3315e869aaf0214Christian MaedergenerateAxioms sig = map (mapNamed $ rmDefs bsorts id) $
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder [inlineAxioms CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder " sort s < s' \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ op pr : s'->s \
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maeder \ forall x,y:s'. d(pr(x)) /\\ d(pr(y)) => pr(x)=pr(y)=>x=y \
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder \ %(ga_projection_injectivity)% "
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder ++ inlineAxioms CASL
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder " sort s < s' \
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder \ op pr : s'->s \
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ forall x:s . d(x) => d(pr(x)) /\\ pr(x)=x %(ga_projection)% "
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder | s <- sorts, let y = mkSimpleId "y",
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder s' <- minSupers s] ++
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [inlineAxioms CASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ . exists x:s.d(x) %(ga_nonEmpty)%" ++
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder inlineAxioms CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ op bottom:s \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ forall x:s . not d(x) <=> x=bottom %(ga_notDefBottom)%"
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder | s <- sortList ] ++
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder [inlineAxioms CASL
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ sorts s_i \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ sorts s_k \
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder \ op f:s_i->t \
ad4889ebb40efae8595b0969dd6ba1162d52bac3Christian Maeder \ var y_k:s_k \
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder \ forall y_i:s_i . def f(y_i) <=> def y_k /\\ def y_k %(ga_totality)%"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder | (f,typ) <- opList, opKind typ == Total,
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder [inlineAxioms CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ sorts s_i \
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder \ sorts s_k \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ op f:s_i->t \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ var y_k:s_k \
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder \ forall y_i:s_i . def f(y_i) => def y_k /\\ def y_k %(ga_strictness)%"
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder | (f,typ) <- opList, opKind typ == Partial,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let s=opArgs typ; t=opRes typ; y= mkVars (length s) ] ++
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder [inlineAxioms CASL
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder " sorts s_i \
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder \ sorts s_k \
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ pred p:s_i \
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ var y_k:s_k \
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder \ forall y_i:s_i . p(y_i) => def y_k /\\ def y_k \
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder \ %(ga_predicate_strictness)%"
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder | (p,typ) <- predList, let s=predArgs typ; y=mkVars (length s) ] )
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder x = mkSimpleId "x"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder pr = projName
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder minSupers so = keepMinimals sig2 id $ Set.toList $ Set.delete so
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder $ supersortsOf so sig2
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sorts = Set.toList $ sortSet sig
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder sig2 = sig { sortRel = Rel.irreflex $ sortRel sig }
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich bsorts = sortSet sig
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder sortList = Set.toList bsorts
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder opList = [(f,t) | (f,types) <- Map.assocs $ opMap sig,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder predList = [(p,t) | (p,types) <- Map.assocs $ predMap sig,
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder mkVars n = [mkSimpleId ("x_"++show i) | i<-[1..n]]
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedercodeRecord :: Set.Set SORT -> (f -> f) -> Record f (FORMULA f) (TERM f)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian MaedercodeRecord bsrts mf = (mapRecord mf)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder { foldQuantification = \ _ q vs qf ps ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Quantification q vs (Implication (defVards bsrts vs) qf False ps) ps
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder , foldDefinedness = \ _ t ps -> defined bsrts t (term_sort t) ps
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , foldExistl_equation = \ _ t1 t2 ps ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Conjunction[Strong_equation t1 t2 ps,
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder defined bsrts t1 (term_sort t1) ps] ps
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , foldMembership = \ _ t s ps -> defined bsrts (project ps t s) s ps
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , foldSort_gen_ax = \ _ cs b -> Sort_gen_ax (map totalizeConstraint cs) b
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder , foldApplication = \ _ o args ps -> Application (totalizeOpSymb o) args ps
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder , foldCast = \ _ t s ps -> project ps t s
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedercodeFormula :: Set.Set SORT -> FORMULA () -> FORMULA ()
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaedercodeFormula bsorts = foldFormula (codeRecord bsorts $ error "CASL2SubCFol")