AS_Maude.hs revision b92e4eba198fcbffab302375b6c3527a8492bc66
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceDescription : abstract maude syntax
81ec673ac5ab1493568d9ef7798b752ab8ee0e61Felix Gabriel ManceCopyright : (c) DFKI GmbH 2009
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : ariesco@fdi.ucm.es
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : experimental
5d801400993c9671010d244646936d8fd435638cChristian MaederPortability : portable
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel ManceThe abstract syntax of maude. Basic specs are a list of statements excluding
aa0ca44e856c87db27e61687cbb630f270976da1Felix Gabriel Manceimports. Sentences are equations, membership axioms, and rules. Sort, subsort
5d801400993c9671010d244646936d8fd435638cChristian Maederand operations should be converted to signature.
5d801400993c9671010d244646936d8fd435638cChristian MaederBecause maude parses and typechecks an input string in one go, basic specs for
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancethe logic instance are just a wrapped string that is created by a simple
18ff56829e5e99383ee6106584d55bcbd8ed45e7Felix Gabriel Mancetype Qid = Token
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian Maederdata Spec = Spec ModId [Parameter] [Statement]
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Read, Ord, Eq)
863fa65ac095659c6da1cde7fe7b839f1e7f60f9Felix Gabriel Mancedata Theory = Theory ModId [Statement]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Parameter = Parameter Sort ModExp
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance deriving (Show, Read, Ord, Eq)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancedata ModExp = ModExp ModId
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | ParenthesesModExp ModExp
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | SummationModExp ModExp ModExp
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | RenamingModExp ModExp [Renaming]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Renaming = SortRenaming Sort Sort
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | LabelRenaming LabelId LabelId
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance | OpRenaming1 OpId ToPartRenaming
0ec1551231bc5dfdcb3f2bd68fec7457fade7bfdFelix Gabriel Mance | OpRenaming2 OpId [Type] Type ToPartRenaming
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
1a38107941725211e7c3f051f7a8f5e12199f03acmaedernewtype MaudeText = MaudeText String deriving (Show)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Manceinstance Pretty MaudeText where
6033265e7b4ae660eff78e944213286863304903Mihai Codescu pretty (MaudeText s) = specBraces $ text s
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mancedata Statement = ImportStmnt Import
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | SortStmnt Sort
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | SubsortStmnt SubsortDecl
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | OpStmnt Operator
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | MbStmnt Membership
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder | EqStmnt Equation
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder | RlStmnt Rule
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder deriving (Show, Read, Ord, Eq)
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederdata Import = Including ModExp
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder | Extending ModExp
68de80eb2800338cbd16512106fcadab79325d8bChristian Maeder | Protecting ModExp
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder deriving (Show, Read, Ord, Eq)
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederdata SubsortDecl = Subsort Sort Sort
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder deriving (Show, Read, Ord, Eq)
68de80eb2800338cbd16512106fcadab79325d8bChristian Maederdata Operator = Op OpId [Type] Type [Attr]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Equation = Eq Term Term [Condition] [StmntAttr]
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder deriving (Show, Read, Ord, Eq)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mancedata Membership = Mb Term Sort [Condition] [StmntAttr]
c4ca03cce9571a309b1c173e9d5d27fdb8843abdChristian Maeder deriving (Show, Read, Ord, Eq)
407f3d9049715c5d96f014a5a1776410e034db83Christian Maederdata Rule = Rl Term Term [Condition] [StmntAttr]
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancedata Condition = EqCond Term Term
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | MbCond Term Sort
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance | MatchCond Term Term
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance | RwCond Term Term
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mance deriving (Show, Read, Ord, Eq)
544989bc1f6ed4bc0813334ffd934db0fb0010eaFelix Gabriel Mancedata ToPartRenaming = To OpId [Attr]
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder deriving (Show, Read, Ord, Eq)
6856a07e36551ed6fadd7c01e7152a3a28878a6fChristian Maederdata Attr = Assoc
f8c3d045dda224e92bf6bcb6288e1ee75ab54d1eChristian Maeder | LeftId Term
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | RightId Term
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder | Gather [Qid]
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder | Format [Qid]
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance | Frozen [Int]
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mancedata StmntAttr = Label Qid
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance | Metadata String
5a3ae0a9224276de25e709ef8788c1b9716cd206Christian Maeder deriving (Show, Read, Ord, Eq)
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mancedata Term = Const Qid Type
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance | Var Qid Type
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance | Apply Qid [Term]
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mancedata Type = TypeSort Sort
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance | TypeKind Kind
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance deriving (Show, Read, Ord, Eq)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mancenewtype Sort = SortId Qid
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance deriving (Show, Read, Ord, Eq)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mancenewtype Kind = KindId Qid
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mancenewtype ParamId = ParamId Qid
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mancenewtype ModId = ModId Qid
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mance deriving (Show, Read, Ord, Eq)
8af00c8930672188ae80c8829428859160d329d0Felix Gabriel Mancenewtype LabelId = LabelId Qid
9cb6af1a7632f12b60f592ce5eb2ac51e6bd33bbFelix Gabriel Mance deriving (Show, Read, Ord, Eq)
c77c0efe19dc6556ac872828bfb4cfc5fbca5ac5Felix Gabriel Mancenewtype OpId = OpId Qid
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Read, Ord, Eq)