Sentence.hs revision 98890889ffb2e8f6f722b00e265a211f13b5a861
276e28f813ffef042d5a6e9f3373ef4e2ad37996Mark AndrewsModule : $Header$
a6a23642eaf383add7a0be045c01e7dd8278ccafAndreas GustafssonDescription : Maude Sentences
250ed9e230b3903b1b264dd1ed2f691fc7cd2f8fAndreas GustafssonCopyright : (c) Martin Kuehl, Uni Bremen 2008-2009
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserLicense : GPLv2 or higher, see LICENSE.txt
848dcebe28e032abfc66e7f10686e1b04a8516feMark AndrewsMaintainer : mkhl@informatik.uni-bremen.de
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserStability : experimental
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserPortability : portable
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserDefinition of sentences for Maude.
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User -- ** The Sentence type
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User Sentence(..),
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews -- * Contruction
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews fromStatements,
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsimport Common.Id (mkSimpleId, GetRange)
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsimport Common.DocUtils (Pretty(..))
a3ff24aaa545c45b8c581b2127d02d735aff8881Tinderbox User-- ** The Sentence type
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews-- | A 'Membership', 'Equation' or 'Rule'.
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsdata Sentence = Membership Membership
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews | Equation Equation
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews deriving (Show, Read, Ord, Eq)
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews-- ** Sentence Instances
09d72af3e9961c210d7baa6179165b6cd81e8dd0Tinderbox Userinstance GetRange Sentence
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsinstance Pretty Sentence where
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews pretty sent = case sent of
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Membership mb -> pretty mb
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt Equation eq -> pretty eq
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt Rule rl -> pretty rl
fc74b733bf679e1b3fb1599e32d445dffe325208Tinderbox User pretties = vcat . map pretty
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsinstance HasSorts Sentence where
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews getSorts sen = case sen of
09d72af3e9961c210d7baa6179165b6cd81e8dd0Tinderbox User Membership mb -> getSorts mb
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User Equation eq -> getSorts eq
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Rule rl -> getSorts rl
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User mapSorts mp sen = case sen of
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User Membership mb -> Membership $ mapSorts mp mb
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Equation eq -> Equation $ mapSorts mp eq
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User Rule rl -> Rule $ mapSorts mp rl
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox Userinstance HasOps Sentence where
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User getOps sen = case sen of
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Membership mb -> getOps mb
250ed9e230b3903b1b264dd1ed2f691fc7cd2f8fAndreas Gustafsson Equation eq -> getOps eq
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Rule rl -> getOps rl
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews mapOps mp sen = case sen of
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Membership mb -> Membership $ mapOps mp mb
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Equation eq -> Equation $ mapOps mp eq
82d13321f4dcc79a9aec992c7a1c4aaff8983adaAutomatic Updater Rule rl -> Rule $ mapOps mp rl
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsinstance HasLabels Sentence where
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews getLabels sen = case sen of
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Membership mb -> getLabels mb
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Equation eq -> getLabels eq
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Rule rl -> getLabels rl
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews mapLabels mp sen = case sen of
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Membership mb -> Membership $ mapLabels mp mb
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Equation eq -> Equation $ mapLabels mp eq
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews Rule rl -> Rule $ mapLabels mp rl
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt-- * Contruction
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt-- | Extract the 'Sentence's from the given 'Module'.
67adc03ef81fb610f8df093b17f55275ee816754Evan HuntfromSpec :: Module -> [Sentence]
67adc03ef81fb610f8df093b17f55275ee816754Evan HuntfromSpec (Module _ _ stmts) = fromStatements stmts
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt-- | Extract the 'Sentence's from the given 'Statement's.
0ddeab91cf922fd977f37318620b4c69dccf8364Automatic UpdaterfromStatements :: [Statement] -> [Sentence]
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark AndrewsfromStatements stmts = let
36da16fa31fa2a582afe67010ba449a57177fd2fAutomatic Updater convert stmt = case stmt of
f2016fcecf098726740507a5522dca04c49aeb82Tinderbox User -- SubsortStmnt sub -> [fromSubsort sub]
984c2e9f76e66e86f7d9aca99a774836ddf196eaAutomatic Updater OpStmnt op -> fromOperator op
984c2e9f76e66e86f7d9aca99a774836ddf196eaAutomatic Updater MbStmnt mb -> [Membership mb]
7a7a44400d49122d4cc207b43922a7b9c5afe443Automatic Updater EqStmnt eq -> [Equation eq]
22f0b13f28a7df3b348b18848d0ccd745ea88c3cAndreas Gustafsson RlStmnt rl -> [Rule rl]
260e8e04b0dc24cb884c789b5d9eb046457f264eTinderbox User in concatMap convert stmts
1e126d80e1b8a0dd541a733283907656424634dcTinderbox UserfromSubsort :: SubsortDecl -> Sentence
1e126d80e1b8a0dd541a733283907656424634dcTinderbox UserfromSubsort (Subsort s1 s2) = Membership mb
e2e4d321999340802f77adaacd19c797d04b4b95Automatic Updater where var = mkVar "V" (TypeSort s1)
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews cond = MbCond var s1
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews mb = Mb var s2 [cond] []
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserfromOperator :: Operator -> [Sentence]
848dcebe28e032abfc66e7f10686e1b04a8516feMark AndrewsfromOperator (Op op dom cod attrs) = let
7be2f6d5df28b207e3e385c555eb4f740150528dTinderbox User name = getName op
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews first = head dom
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrews second = head $ tail dom
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews convert attr = case attr of
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews Assoc -> assocEq name first second cod
1879ff49326b49a9e4eadaca193c631409bf8575Tinderbox User Comm -> commEq name first second cod
1879ff49326b49a9e4eadaca193c631409bf8575Tinderbox User Idem -> idemEq name first cod
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox User Id term -> identityEq name first term cod
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox User LeftId term -> leftIdEq name first term cod
22f0b13f28a7df3b348b18848d0ccd745ea88c3cAndreas Gustafsson RightId term -> rightIdEq name first term cod
afb33f777af856f8c3382604a7a8ffdfe2b512c5Automatic Updater in concatMap convert attrs
afb33f777af856f8c3382604a7a8ffdfe2b512c5Automatic UpdatercommEq :: Qid -> Type -> Type -> Type -> [Sentence]
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox UsercommEq op ar1 ar2 co = [Equation $ Eq t1 t2 [] []]
22f0b13f28a7df3b348b18848d0ccd745ea88c3cAndreas Gustafsson where v1 = mkVar "v1" $ type2Kind ar1
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User v2 = mkVar "v2" $ type2Kind ar2
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User t1 = Apply op [v1, v2] $ type2Kind co
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User t2 = Apply op [v2, v1] $ type2Kind co
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UserassocEq :: Qid -> Type -> Type -> Type -> [Sentence]
e334405421979688f2d838805ac67ee47bd62976Mark AndrewsassocEq op ar1 ar2 co = [eq]
e334405421979688f2d838805ac67ee47bd62976Mark Andrews where v1 = mkVar "v1" $ type2Kind ar1
e334405421979688f2d838805ac67ee47bd62976Mark Andrews v2 = mkVar "v2" $ type2Kind ar2
e334405421979688f2d838805ac67ee47bd62976Mark Andrews v3 = mkVar "v3" $ type2Kind ar2
e334405421979688f2d838805ac67ee47bd62976Mark Andrews t1 = Apply op [v1, v2] $ type2Kind co
e334405421979688f2d838805ac67ee47bd62976Mark Andrews t2 = Apply op [t1, v3] $ type2Kind co
e334405421979688f2d838805ac67ee47bd62976Mark Andrews t3 = Apply op [v2, v3] $ type2Kind co
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox User t4 = Apply op [v1, t3] $ type2Kind co
65ad89971ee9973074cd11c207af92bf5440df01Automatic Updater eq = Equation $ Eq t2 t4 [] []
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark AndrewsidemEq :: Qid -> Type -> Type -> [Sentence]
089c63b69cdf6803aa8901aae3f2fbae58969511Automatic UpdateridemEq op ar co = [Equation $ Eq t v [] []]
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews where v = Apply (mkSimpleId "v") [] $ type2Kind ar
db6353c9b89628e16f6e729ce57baabad3460c49Automatic Updater t = Apply op [v, v] $ type2Kind co
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UseridentityEq :: Qid -> Type -> Term -> Type -> [Sentence]
45571e73747cb97c4abcdc7be8cc0c484b1b0e42Tinderbox UseridentityEq op ar1 idt co = [eq1, eq2]
089c63b69cdf6803aa8901aae3f2fbae58969511Automatic Updater where idt' = const2kind idt
9ce6056d520aaf5241560fab6ab096c0d4e87b36Automatic Updater v = mkVar "v" $ type2Kind ar1
ebabe300b615154d08f5577822cfd8726d2643c8Automatic Updater t1 = Apply op [v, idt'] $ type2Kind co
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox User t2 = Apply op [idt', v] $ type2Kind co
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox User eq1 = Equation $ Eq t1 v [] []
10b865e9187fc77cae02f106ddcc9e03eecdfe06Tinderbox User eq2 = Equation $ Eq t2 v [] []
10b865e9187fc77cae02f106ddcc9e03eecdfe06Tinderbox UserleftIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
10b865e9187fc77cae02f106ddcc9e03eecdfe06Tinderbox UserleftIdEq op ar1 idt co = [eq1, eq2]
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt where idt' = const2kind idt
1f8dc520d4bbc5406d551724282df1e5f7626e19Automatic Updater v = mkVar "v" $ type2Kind ar1
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt t = Apply op [idt', v] $ type2Kind co
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt eq1 = Equation $ Eq t v [] []
67adc03ef81fb610f8df093b17f55275ee816754Evan Hunt eq2 = Equation $ Eq v t [] []
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark AndrewsrightIdEq :: Qid -> Type -> Term -> Type -> [Sentence]
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark AndrewsrightIdEq op ar1 idt co = [eq1, eq2]
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews where idt' = const2kind idt
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews v = mkVar "v" $ type2Kind ar1
22f0b13f28a7df3b348b18848d0ccd745ea88c3cAndreas Gustafsson t = Apply op [v, idt'] $ type2Kind co
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrews eq1 = Equation $ Eq t v [] []
c0cbdeedb5e119c640f098da1851cb1b9adcc739Tinderbox User eq2 = Equation $ Eq v t [] []
c0cbdeedb5e119c640f098da1851cb1b9adcc739Tinderbox Usertype2Kind :: Type -> Type
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox Usertype2Kind (TypeSort (SortId s)) = TypeKind $ KindId s
f33abec8a62ab6f2b867d7189dfffa72592c027bTinderbox Usertype2Kind k = k
f33abec8a62ab6f2b867d7189dfffa72592c027bTinderbox Userconst2kind :: Term -> Term
a3edcadfffbe617a419cdbe1bebb95f68a0eda1eMark Andrewsconst2kind (Const q ty) = Const q $ type2Kind ty
848dcebe28e032abfc66e7f10686e1b04a8516feMark Andrewsconst2kind t = t
281ed127e3ed6c7e07792c19c3bc4562f71cfa90Tinderbox User-- | True iff the given 'Sentence' is a 'Rule'.
281ed127e3ed6c7e07792c19c3bc4562f71cfa90Tinderbox UserisRule :: Sentence -> Bool
281ed127e3ed6c7e07792c19c3bc4562f71cfa90Tinderbox UserisRule sent = case sent of
ac946c1f16db64f14431ac53177904ec5f058f03Tinderbox User Rule _ -> True