Sentence.hs revision fecce42517d20490f893c4a9dee29b000e1653ea
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederModule : $Header$
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederDescription : Sentences for Maude
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederMaintainer : mkhl@informatik.uni-bremen.de
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederStability : experimental
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederPortability : portable
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederDefinition of sentences for Maude.
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Sentence(..),
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder fromStatements,
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederimport Data.Maybe (mapMaybe, fromJust)
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederimport Common.Id (mkSimpleId)
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederimport Common.DocUtils (Pretty(..))
96de7ec4008f75574077816c4c71a22e6afe1e01Christian Maederdata Sentence = Membership Membership
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder | Equation Equation
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder deriving (Show, Read, Ord, Eq)
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance Pretty Sentence where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder pretty sent = case sent of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> pretty mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> pretty eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> pretty rl
162a689da386fc8ddbbe47bcae83eaca4fc8dbc0Christian Maeder pretties = vcat . map pretty
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance HasSorts Sentence where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder getSorts sen = case sen of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> getSorts mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> getSorts eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> getSorts rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder mapSorts mp sen = case sen of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> Membership $ mapSorts mp mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> Equation $ mapSorts mp eq
ce59e0cc5c7221245ed323290bfccbda4ee32dd9Christian Maeder Rule rl -> Rule $ mapSorts mp rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance HasOps Sentence where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder getOps sen = case sen of
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder Membership mb -> getOps mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> getOps eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> getOps rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder mapOps mp sen = case sen of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> Membership $ mapOps mp mb
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder Equation eq -> Equation $ mapOps mp eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> Rule $ mapOps mp rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maederinstance HasLabels Sentence where
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder getLabels sen = case sen of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> getLabels mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> getLabels eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> getLabels rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder mapLabels mp sen = case sen of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Membership mb -> Membership $ mapLabels mp mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Equation eq -> Equation $ mapLabels mp eq
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder Rule rl -> Rule $ mapLabels mp rl
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder-- | Extract the |Sentence|s of a |Module|
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromSpec :: Module -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromSpec (Module _ _ stmts) = fromStatements stmts
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder-- | Extract the |Sentence|s from the |Statement|s
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromStatements :: [Statement] -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromStatements stmts = let
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder convert stmt = case stmt of
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder SubsortStmnt sbsrt -> Just [fromSubsort sbsrt]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder OpStmnt op -> Just $ fromOperator op
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder MbStmnt mb -> Just [Membership mb]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder EqStmnt eq -> Just [Equation eq]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder RlStmnt rl -> Just [Rule rl]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder in concat $ mapMaybe convert stmts
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder-- | Check whether a |Sentence| is a |Rule|
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederisRule :: Sentence -> Bool
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederisRule sent = case sent of
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder Rule _ -> True
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromSubsort :: SubsortDecl -> Sentence
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromSubsort (Subsort s1 s2) = Membership mb
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v = Var (mkSimpleId "V") (TypeSort s1)
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder cond = MbCond v s1
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder mb = Mb v s2 [cond] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromOperator :: Operator -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederfromOperator (Op op_id ar co ats) = concat [comm_sens, assoc_sens, idem_sens,
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder id_sens, leftId_sens, rightId_sens]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where assoc_sens = if any assoc ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then assocEq (getName op_id) (head ar) (head $ tail ar) co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder comm_sens = if any comm ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then commEq (getName op_id) (head ar) (head $ tail ar) co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder idem_sens = if any idem ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then idemEq (getName op_id) (head ar) co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder id_sens = if any idtty ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then identityEq (getName op_id) (head ar) (fromJust $ getIdentity ats) co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder leftId_sens = if any leftId ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then leftIdEq (getName op_id) (head ar) (fromJust $ getIdentity ats) co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder rightId_sens = if any rightId ats
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder then rightIdEq (getName op_id) (head ar) (fromJust $ getIdentity ats) co
af1cb109bce240bcafe3823df022d6088cbfc438Christian MaederassocEq :: Qid -> Type -> Type -> Type -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederassocEq op ar1 ar2 co = [Equation $ Eq t1 t2 [] []]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v1 = Var (mkSimpleId "v1") ar1
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder v2 = Var (mkSimpleId "v2") ar2
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t1 = Apply op [v1, v2] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t2 = Apply op [v2, v1] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaedercommEq :: Qid -> Type -> Type -> Type -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaedercommEq op ar1 ar2 co = [eq1, eq2]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v1 = Var (mkSimpleId "v1") ar1
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder v2 = Var (mkSimpleId "v2") ar2
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder v3 = Var (mkSimpleId "v3") ar2
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t1 = Apply op [v1, v2] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t2 = Apply op [t1, v3] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t3 = Apply op [v2, v3] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t4 = Apply op [v1, t3] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq1 = Equation $ Eq t2 t4 [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq2 = Equation $ Eq t4 t2 [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederidemEq :: Qid -> Type -> Type -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederidemEq op ar co = [Equation $ Eq t v [] []]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v = Apply (mkSimpleId "v") [] ar
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t = Apply op [v, v] co
31c6978fd9066c9d2c3c98c950f7abbe89112522Christian MaederidentityEq :: Qid -> Type -> Term -> Type -> [Sentence]
31c6978fd9066c9d2c3c98c950f7abbe89112522Christian MaederidentityEq op ar1 idt co = [eq1, eq2, eq3, eq4]
31c6978fd9066c9d2c3c98c950f7abbe89112522Christian Maeder where v = Var (mkSimpleId "v") ar1
31c6978fd9066c9d2c3c98c950f7abbe89112522Christian Maeder t1 = Apply op [v, idt] co
31c6978fd9066c9d2c3c98c950f7abbe89112522Christian Maeder t2 = Apply op [idt, v] co
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder eq1 = Equation $ Eq t1 v [] []
af1cb109bce240bcafe3823df022d6088cbfc438Christian Maeder eq2 = Equation $ Eq t2 v [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq3 = Equation $ Eq v t1 [] []
162a689da386fc8ddbbe47bcae83eaca4fc8dbc0Christian Maeder eq4 = Equation $ Eq v t2 [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederleftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederleftIdEq op ar1 idt co = [eq1, eq2]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v = Var (mkSimpleId "v") ar1
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t = Apply op [idt, v] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq1 = Equation $ Eq t v [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq2 = Equation $ Eq v t [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederrightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian MaederrightIdEq op ar1 idt co = [eq1, eq2]
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder where v = Var (mkSimpleId "v") ar1
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder t = Apply op [v, idt] co
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq1 = Equation $ Eq t v [] []
bd8ff5b5f66be563e5be9d3a0c069e32d06f331cChristian Maeder eq2 = Equation $ Eq v t [] []