55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederDescription : Coding a description language into CASL
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederCopyright : (c) Stef Joosten, Christian Maeder DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederMaintainer : Christian.Maeder@dfki.de
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederStability : experimental
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederPortability : non-portable (imports Logic.Logic)
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederThe translating comorphism from Adl to CASL.
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder ( Adl2CASL (..)
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maederimport qualified Common.Lib.Rel as Rel
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maederimport qualified Data.Set as Set
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder-- | lid of the morphism
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maederdata Adl2CASL = Adl2CASL deriving Show
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maederinstance Language Adl2CASL -- default is ok
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maederinstance Comorphism Adl2CASL
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder CASL_Sublogics
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder CASLBasicSpec
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder SYMB_MAP_ITEMS
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder sourceLogic Adl2CASL = Adl
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder sourceSublogic Adl2CASL = ()
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder targetLogic Adl2CASL = CASL
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder mapSublogic Adl2CASL _ = Just $ caslTop
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder { has_part = False
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder , sub_features = LocFilSub
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder , cons_features = NoSortGen }
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder map_theory Adl2CASL = mapTheory
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder map_sentence Adl2CASL s = return . mapSen (mapSign s)
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder map_morphism Adl2CASL = mapMor
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder map_symbol Adl2CASL _ = Set.singleton . mapSym
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder is_model_transportable Adl2CASL = True
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder has_model_expansion Adl2CASL = True
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder is_weakly_amalgamable Adl2CASL = True
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder isInclusionComorphism Adl2CASL = True
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapTheory :: (A.Sign, [Named Sen]) -> Result (CASLSign, [Named CASLFORMULA])
ac4003061d04445bce1fad507f5caf50f8903685Christian MaedermapTheory (s, ns) = let cs = mapSign s in
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder return (cs, map (mapNamed $ mapSen cs) ns)
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederrelTypeToPred :: RelType -> PredType
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaederrelTypeToPred (RelType c1 c2) = PredType [conceptToId c1, conceptToId c2]
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapSign :: A.Sign -> CASLSign
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapSign s = (C.emptySign ())
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder (Rel.fromKeysSet $ Set.fold (\ sy -> case sy of
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder $ Rel.map conceptToId $ isas s
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder . map (\ (i, l) -> (transRelId $ idToSimpleId i, l))
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder . MapSet.toList . MapSet.map relTypeToPred . MapSet.fromMap $ rels s
e2330d7f462d9e15378c8408f825f23aac37100aChristian MaedertransRelId :: Token -> Id
e2330d7f462d9e15378c8408f825f23aac37100aChristian MaedertransRelId t@(Token s p) = simpleIdToId $
e2330d7f462d9e15378c8408f825f23aac37100aChristian Maeder if elem s casl_reserved_fwords then Token ("P_" ++ s) p else t
ac4003061d04445bce1fad507f5caf50f8903685Christian MaedermapSen :: CASLSign -> Sen -> CASLFORMULA
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian MaedermapSen sig s = case s of
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder DeclProp r p -> getRelProp sig r p
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder Assertion _ r ->
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder let ((v1, s1), (v2, s2), f) = evalState (transRule sig r) 1 in
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder mkForall [mkVarDecl v1 s1, mkVarDecl v2 s2] f
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder-- | Translation of morphisms
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapMor :: A.Morphism -> Result CASLMor
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapMor mor = return $ embedMorphism ()
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian Maeder (mapSign $ domOfDefaultMorphism mor) $ mapSign $ codOfDefaultMorphism mor
51dc4ec3c58b834d0ef0eb3d5a8d9379983377bfChristian MaedermapSym s = case s of
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder A.Con c -> idToSortSymbol $ conceptToId c
e2330d7f462d9e15378c8408f825f23aac37100aChristian Maeder Rel (Sgn n t) -> idToPredSymbol (transRelId n) $ relTypeToPred t
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maedernext :: State Int Int
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetRelPred :: CASLSign -> A.Relation -> PRED_SYMB
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian MaedergetRelPred sig m@(Sgn t (RelType c1 c2)) = let
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder ty1 = conceptToId c1
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder ty2 = conceptToId c2
e2330d7f462d9e15378c8408f825f23aac37100aChristian Maeder i = transRelId t
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder cs = filter (\ pt -> case predArgs pt of
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder [fr, to] -> leqSort sig ty1 fr && leqSort sig ty2 to
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder $ Set.toList $ MapSet.lookup i $ predMap sig
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder in case cs of
e2330d7f462d9e15378c8408f825f23aac37100aChristian Maeder Qual_pred_name i (toPRED_TYPE ty) $ tokPos t
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder _ -> error $ "getRelPred " ++ showDoc m ""
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedergetRelProp :: CASLSign -> A.Relation -> RangedProp -> CASLFORMULA
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian MaedergetRelProp sig r p =
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig r
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder q = propRange p
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder q1 = Var_decl [mkSimpleId "a"] fr q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder q2 = Var_decl [mkSimpleId "b"] to q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder q3 = Var_decl [mkSimpleId "c"] fr q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder t1 = toQualVar q1
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder t2 = toQualVar q2
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder t3 = toQualVar q3
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder pAppl = Predication qp [t1, t2] q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder eqs = fr == to
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder in case propProp p of
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Uni -> mkForallRange [q1, q2, q3]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (conjunctRange
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder [pAppl, Predication qp [t3, t2] q] q)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Implication (Equation t1 Strong t3 q)
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Tot -> mkForallRange [q1] (Quantification Existential [q2] pAppl q) q
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Sur -> mkForallRange [q2] (Quantification Existential [q1] pAppl q) q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder q4 = Var_decl [mkSimpleId "c"] to q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder t4 = toQualVar q4
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder in mkForallRange [q1, q2, q4]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (conjunctRange
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder [pAppl, Predication qp [t1, t4] q] q)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Implication (Equation t2 Strong t4 q)
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Sym | eqs -> mkForallRange [q1, q2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (Relation pAppl Equivalence (Predication qp [t2, t1] q) q) q
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Asy | eqs -> mkForallRange [q1, q2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (Relation pAppl Implication
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (Negation (Predication qp [t2, t1] q) q) q) q
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Trn | eqs -> mkForallRange [q1, q2, q3]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (conjunctRange [pAppl, Predication qp [t2, t3] q] q)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Implication (Predication qp [t1, t3] q)
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder Rfx | eqs -> mkForallRange [q1] (Predication qp [t1, t1] q) q
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder pr -> error $ "getRelProp " ++ showDoc pr ""
ac4003061d04445bce1fad507f5caf50f8903685Christian MaedertransRule :: CASLSign -> Rule
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder -> State Int ((VAR, SORT), (VAR, SORT), CASLFORMULA)
ac4003061d04445bce1fad507f5caf50f8903685Christian MaedertransRule sig rule =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder let myMin v@(ta, sa) (_, sb)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | leqSort sig sa sb = v
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | leqSort sig sb sa = (ta, sb)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder | otherwise = error $
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder "transRule.myMin " ++ showDoc (sa, sb) "\n " ++ showDoc rule ""
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder myVarDecl = uncurry mkVarDecl
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder in case rule of
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder Tm m@(Sgn (Token s p) (RelType c1 c2)) -> do
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder let v1 = mkNumVar "a" i
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder v2 = mkNumVar "b" j
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder isI = s == "I"
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder ty1' = conceptToId c1
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder ty2' = conceptToId c2
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder ty1 = if isI && leqSort sig ty2 ty1 then ty2' else ty1'
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder ty2 = if isI && leqSort sig ty1 ty2 then ty1' else ty2'
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder q1 = Qual_var v1 ty1 p
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder q2 = Qual_var v2 ty2 p
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder return ((v1, ty1), (v2, ty2),
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder if s == "V" then Atom True p else
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder if ty1 == ty2 then Equation q1 Strong q2 p else
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder error $ "transRule.I " ++ showDoc rule ""
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder let qp@(Qual_pred_name _ (Pred_type [fr, to] _) _) = getRelPred sig m
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder in Predication qp
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder [ if ty1 == fr then q1 else Sorted_term q1 fr p
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder , if ty2 == to then q2 else Sorted_term q2 to p] p)
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder UnExp o e -> do
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder (v1, v2@(t2, _), f) <- transRule sig e
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Co -> return (v2, v1, f)
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Cp -> return (v1, v2, negateForm f nullRange)
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder let v@(_, s) = myMin v1 v2
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder nf = renameVar sig v1 v $ renameVar sig v2 w f
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder z = (mkNumVar "c" k, s)
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder cf = mkExist [myVarDecl z]
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder $ conjunct [renameVar sig v z nf, renameVar sig w z nf]
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder -- this is (and always will be) incomplete wrt to compositions
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder return (v, w, disjunct
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder $ [ mkStEq (toQualVar $ myVarDecl v) $ toQualVar $ myVarDecl w
08eabcc70456fa8e6d34521ba20946630d5e16b2Christian Maeder | o == K0] ++ [nf, cf])
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder MulExp o es -> case es of
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder [] -> error "transRule2"
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder r : t -> if null t then transRule sig r else do
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder (v1, v2, f1) <- transRule sig r
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder (v3, v4, f2) <- transRule sig $ MulExp o t
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder if elem o [Fc, Fd] then return (v1, v4,
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder let v23 = myMin v2 v3
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder f3 = renameVar sig v2 v23 f1
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder f4 = renameVar sig v3 v23 f2
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder vs = [myVarDecl v23]
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder cs = [f3, f4]
ea9c85afaa9e7cc986b1bf81ad3abaa05b8af463Christian Maeder in if o == Fc then mkExist vs $ conjunct cs
3a2de7e5a3c5da0a96c9563617ab332685a41cedChristian Maeder else mkForall vs $ disjunct cs)
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder let v13 = myMin v1 v3
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder v24 = myMin v2 v4
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder f3 = renameVar sig v1 v13 $ renameVar sig v2 v24 f1
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder f4 = renameVar sig v3 v13 $ renameVar sig v4 v24 f2
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder return (v13, v24, case o of
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Fi -> conjunct [f3, f4]
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Fu -> disjunct [f3, f4]
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Ri -> mkImpl f3 f4
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder Rr -> Relation f4 RevImpl f3 nullRange
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder Re -> mkEqv f3 f4
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder _ -> error "transRule,MulExp")
ac4003061d04445bce1fad507f5caf50f8903685Christian MaederrenameVarRecord :: CASLSign -> (VAR, SORT) -> (VAR, SORT)
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder -> Record () CASLFORMULA (TERM ())
ac4003061d04445bce1fad507f5caf50f8903685Christian MaederrenameVarRecord sig from to = (mapRecord id)
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder { foldQual_var = \ _ v ty p ->
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder let (nv, nty) = if (v, ty) == from then to else (v, ty)
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder qv = Qual_var nv nty p
534d2a17ea35f30d0d462fa539d633b6ba389da6Christian Maeder in if nty == ty then qv else
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder if leqSort sig nty ty then Sorted_term qv ty p else
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder error "renameVar"
ac4003061d04445bce1fad507f5caf50f8903685Christian MaederrenameVar :: CASLSign -> (VAR, SORT) -> (VAR, SORT) -> CASLFORMULA
ac4003061d04445bce1fad507f5caf50f8903685Christian Maeder -> CASLFORMULA
ac4003061d04445bce1fad507f5caf50f8903685Christian MaederrenameVar sig v = foldFormula . renameVarRecord sig v