AS_Maude.hs revision fecce42517d20490f893c4a9dee29b000e1653ea
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherModule : $Header$
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherDescription : abstract maude syntax
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherCopyright : (c) DFKI GmbH 2009
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherMaintainer : ariesco@fdi.ucm.es
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherStability : experimental
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherPortability : portable
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherThe abstract syntax of maude. Basic specs are a list of statements excluding
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherimports. Sentences are equations, membership axioms, and rules. Sort, subsort
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherand operations should be converted to signature.
3dfa09a826e5f63b4948462c2452937fc329834dJakub HrozekBecause maude parses and typechecks an input string in one go, basic specs for
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekthe logic instance are just a wrapped string that is created by a simple
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekimport Common.Doc (specBraces, text)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekimport Common.DocUtils (Pretty(..))
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozektype Qid = Token
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata Spec = SpecMod Module
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | SpecTh Module
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | SpecView View
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata Module = Module ModId [Parameter] [Statement]
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata View = View ModId ModExp ModExp [Renaming]
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata Parameter = Parameter Sort ModExp
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata ModExp = ModExp ModId
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | SummationModExp ModExp ModExp
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | RenamingModExp ModExp [Renaming]
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | InstantiationModExp ModExp [ViewId]
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata Renaming = SortRenaming Sort Sort
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | LabelRenaming LabelId LabelId
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | OpRenaming1 OpId ToPartRenaming
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | OpRenaming2 OpId [Type] Type ToPartRenaming
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek | TermMap Term Term
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozekdata ToPartRenaming = To OpId [Attr]
3dfa09a826e5f63b4948462c2452937fc329834dJakub Hrozek deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype MaudeText = MaudeText String deriving (Show)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherinstance Pretty MaudeText where
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher pretty (MaudeText s) = specBraces $ text s
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Statement = ImportStmnt Import
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | SortStmnt Sort
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | SubsortStmnt SubsortDecl
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | OpStmnt Operator
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | EqStmnt Equation
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | MbStmnt Membership
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | RlStmnt Rule
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Import = Including ModExp
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Extending ModExp
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Protecting ModExp
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata SubsortDecl = Subsort Sort Sort
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Operator = Op OpId [Type] Type [Attr]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Membership = Mb Term Sort [Condition] [StmntAttr]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Equation = Eq Term Term [Condition] [StmntAttr]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Rule = Rl Term Term [Condition] [StmntAttr]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Condition = EqCond Term Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | MbCond Term Sort
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | MatchCond Term Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | RwCond Term Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Attr = Assoc
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | RightId Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Gather [Qid]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Format [Qid]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Frozen [Int]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Special [Hook]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata StmntAttr = Label Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Metadata String
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Hook = IdHook Qid [Qid]
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | OpHook Qid Qid [Qid] Qid
724426603e727bdbf08fe3fb2637f6f5d7d0881eOndrej Kos | TermHook Qid Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Term = Const Qid Type
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher | Var Qid Type
724426603e727bdbf08fe3fb2637f6f5d7d0881eOndrej Kos | Apply Qid [Term] Type
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherdata Type = TypeSort Sort
ceb40cb8846ff755f841466908954087f927eae7Jakub Hrozek | TypeKind Kind
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype Sort = SortId Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype Kind = KindId Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype ParamId = ParamId Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype ViewId = ViewId Qid
724426603e727bdbf08fe3fb2637f6f5d7d0881eOndrej Kos deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype ModId = ModId Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
724426603e727bdbf08fe3fb2637f6f5d7d0881eOndrej Kosnewtype LabelId = LabelId Qid
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghernewtype OpId = OpId Qid
67ca9e7c006d8619f446c018eabf29eab1368ba5Ondrej Kos deriving (Show, Read, Ord, Eq)
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | Auxiliary functions to traverse the attributes
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | check if a list of attributes contains the assoc attribute
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherassoc :: Attr -> Bool
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherassoc a = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | check if a list of attributes contains the comm attribute
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghercomm :: Attr -> Bool
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallaghercomm a = case a of
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichl Comm -> True
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichl-- | check if a list of attributes contains the idem attribute
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichlidem :: Attr -> Bool
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichlidem a = case a of
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichl Idem -> True
d9de4b26f44a344025bbfa23104b7b67935fae35Pavel Reichl-- | check if a list of attributes contains the identity attribute
d9de4b26f44a344025bbfa23104b7b67935fae35Pavel Reichlidtty :: Attr -> Bool
d9de4b26f44a344025bbfa23104b7b67935fae35Pavel Reichlidtty a = case a of
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichl Id _ -> True
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel Reichl-- | check if a list of attributes contains the left identity attribute
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel ReichlleftId :: Attr -> Bool
13aea9c2b9c48dd614095b4551021868812ba2f0Pavel ReichlleftId a = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher LeftId _ -> True
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | check if a list of attributes contains the right identity attribute
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherrightId :: Attr -> Bool
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallagherrightId a = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher RightId _ -> True
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | check if a list of attributes contains the right identity attribute
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherctor :: Attr -> Bool
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherctor a = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | check if a list of attributes contains the owise attribute
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherowise :: StmntAttr -> Bool
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagherowise a = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher-- | returns the identity term from the attribute set
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallaghergetIdentity :: [Attr] -> Maybe Term
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallaghergetIdentity [] = Nothing
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen GallaghergetIdentity (a : as) = case a of
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher Id t -> Just t
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher RightId t -> Just t
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher LeftId t -> Just t
a23919ed39d212f9f5694d9b103c84641fdb7680Stephen Gallagher _ -> getIdentity as