Sentence.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : Maude Sentences
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : mkhl@informatik.uni-bremen.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : experimental
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederDefinition of sentences for Maude.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- ** The Sentence type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Sentence(..),
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder -- * Contruction
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder fromStatements,
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederimport Common.Id (mkSimpleId, GetRange)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederimport Common.DocUtils (Pretty(..))
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini-- ** The Sentence type
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo Torrini-- | A 'Membership', 'Equation' or 'Rule'.
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederdata Sentence = Membership Membership
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder | Equation Equation
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder deriving (Show, Read, Ord, Eq)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- ** Sentence Instances
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederinstance GetRange Sentence
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederinstance Pretty Sentence where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder pretty sent = case sent of
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder Membership mb -> pretty mb
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder Equation eq -> pretty eq
603e326e7b189de8c1e4ea8c89470b3a61154019Christian Maeder Rule rl -> pretty rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder pretties = vcat . map pretty
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederinstance HasSorts Sentence where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder getSorts sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Membership mb -> getSorts mb
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Equation eq -> getSorts eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> getSorts rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder mapSorts mp sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Membership mb -> Membership $ mapSorts mp mb
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Equation eq -> Equation $ mapSorts mp eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> Rule $ mapSorts mp rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederinstance HasOps Sentence where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder getOps sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Membership mb -> getOps mb
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Equation eq -> getOps eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> getOps rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder mapOps mp sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Membership mb -> Membership $ mapOps mp mb
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Equation eq -> Equation $ mapOps mp eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> Rule $ mapOps mp rl
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maederinstance HasLabels Sentence where
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder getLabels sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Membership mb -> getLabels mb
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder Equation eq -> getLabels eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> getLabels rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder mapLabels mp sen = case sen of
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder Membership mb -> Membership $ mapLabels mp mb
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Equation eq -> Equation $ mapLabels mp eq
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Rule rl -> Rule $ mapLabels mp rl
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * Contruction
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | Extract the 'Sentence's from the given 'Module'.
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaederfromSpec :: Module -> [Sentence]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederfromSpec (Module _ _ stmts) = fromStatements stmts
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | Extract the 'Sentence's from the given 'Statement's.
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaederfromStatements :: [Statement] -> [Sentence]
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaederfromStatements stmts = let
2f65d931e866162d39d09c43021a55314040b377Christian Maeder convert stmt = case stmt of
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian Maeder -- SubsortStmnt sub -> [fromSubsort sub]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder OpStmnt op -> fromOperator op
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder MbStmnt mb -> [Membership mb]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder EqStmnt eq -> [Equation eq]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder RlStmnt rl -> [Rule rl]
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder in concatMap convert stmts
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederfromSubsort :: SubsortDecl -> Sentence
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederfromSubsort (Subsort s1 s2) = Membership mb
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder where var = mkVar "V" (TypeSort s1)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder cond = MbCond var s1
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder mb = Mb var s2 [cond] []
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfromOperator :: Operator -> [Sentence]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfromOperator (Op op dom cod attrs) = let
81eaac399d69af15425d06b054e5d0331dbc132bChristian Maeder name = getName op
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder first = head dom
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder second = head $ tail dom
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder convert attr = case attr of
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini Assoc -> assocEq name first second cod
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder Comm -> commEq name first second cod
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder Idem -> idemEq name first cod
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder Id term -> identityEq name first term cod
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maeder LeftId term -> leftIdEq name first term cod
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder RightId term -> rightIdEq name first term cod
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder in concatMap convert attrs
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercommEq :: Qid -> Type -> Type -> Type -> [Sentence]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercommEq op ar1 ar2 co = [Equation $ Eq t1 t2 [] []]
f1082bc15d1cbd06522cf49842929d73ba4214fcChristian Maeder where v1 = mkVar "v1" $ type2Kind ar1
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder v2 = mkVar "v2" $ type2Kind ar2
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder t1 = Apply op [v1, v2] $ type2Kind co
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder t2 = Apply op [v2, v1] $ type2Kind co
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederassocEq :: Qid -> Type -> Type -> Type -> [Sentence]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederassocEq op ar1 ar2 co = [eq]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder where v1 = mkVar "v1" $ type2Kind ar1
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder v2 = mkVar "v2" $ type2Kind ar2
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder v3 = mkVar "v3" $ type2Kind ar2
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder t1 = Apply op [v1, v2] $ type2Kind co
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder t2 = Apply op [t1, v3] $ type2Kind co
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder t3 = Apply op [v2, v3] $ type2Kind co
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder t4 = Apply op [v1, t3] $ type2Kind co
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder eq = Equation $ Eq t2 t4 [] []
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederidemEq :: Qid -> Type -> Type -> [Sentence]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederidemEq op ar co = [Equation $ Eq t v [] []]
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder where v = Apply (mkSimpleId "v") [] $ type2Kind ar
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo Torrini t = Apply op [v, v] $ type2Kind co
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorriniidentityEq :: Qid -> Type -> Term -> Type -> [Sentence]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederidentityEq op ar1 idt co = [eq1, eq2]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder where idt' = const2kind idt
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder v = mkVar "v" $ type2Kind ar1
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder t1 = Apply op [v, idt'] $ type2Kind co
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder t2 = Apply op [idt', v] $ type2Kind co
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder eq1 = Equation $ Eq t1 v [] []
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder eq2 = Equation $ Eq t2 v [] []
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederleftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederleftIdEq op ar1 idt co = [eq1, eq2]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder where idt' = const2kind idt
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder v = mkVar "v" $ type2Kind ar1
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder t = Apply op [idt', v] $ type2Kind co
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder eq1 = Equation $ Eq t v [] []
4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder eq2 = Equation $ Eq v t [] []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederrightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederrightIdEq op ar1 idt co = [eq1, eq2]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder where idt' = const2kind idt
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder v = mkVar "v" $ type2Kind ar1
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder t = Apply op [v, idt'] $ type2Kind co
8451d8feb0aa0e67f6585ed10669eec73ba1fba0Christian Maeder eq1 = Equation $ Eq t v [] []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder eq2 = Equation $ Eq v t [] []
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype2Kind :: Type -> Type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype2Kind (TypeSort (SortId s)) = TypeKind $ KindId s
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertype2Kind k = k
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconst2kind :: Term -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconst2kind (Const q ty) = Const q $ type2Kind ty
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconst2kind t = t
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | True iff the given 'Sentence' is a 'Rule'.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisRule :: Sentence -> Bool
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisRule sent = case sent of
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder Rule _ -> True