| Copyright | (c) DFKI GmbH 2009 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | ariesco@fdi.ucm.es |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe-Inferred |
Maude.AS_Maude
Description
The abstract syntax of maude. Basic specs are a list of statements excluding imports. Sentences are equations, membership axioms, and rules. Sort, subsort and operations should be converted to signature.
Because maude parses and typechecks an input string in one go, basic specs for the logic instance are just a wrapped string that is created by a simple parser.
- newtype MaudeText = MaudeText String
- type Qid = Token
- data Spec
- data Module = Module ModId [Parameter] [Statement]
- data View = View ModId ModExp ModExp [Renaming]
- data Parameter = Parameter Sort ModExp
- data ModExp
- data Renaming
- data ToPartRenaming = To OpId [Attr]
- data Statement
- data Import
- data SubsortDecl = Subsort Sort Sort
- data Operator = Op OpId [Type] Type [Attr]
- data Membership = Mb Term Sort [Condition] [StmntAttr]
- data Equation = Eq Term Term [Condition] [StmntAttr]
- data Rule = Rl Term Term [Condition] [StmntAttr]
- data Condition
- data Attr
- data StmntAttr
- data Hook
- data Term
- data Type
- newtype Sort = SortId Qid
- newtype Kind = KindId Qid
- newtype ParamId = ParamId Qid
- newtype ViewId = ViewId Qid
- newtype ModId = ModId Qid
- newtype LabelId = LabelId Qid
- newtype OpId = OpId Qid
- mkVar :: String -> Type -> Term
- getTermType :: Term -> Type
- assoc :: Attr -> Bool
- comm :: Attr -> Bool
- idem :: Attr -> Bool
- idtty :: Attr -> Bool
- leftId :: Attr -> Bool
- rightId :: Attr -> Bool
- ctor :: Attr -> Bool
- owise :: StmntAttr -> Bool
Types
newtype MaudeText
Instances
| Show MaudeText | |
| ShATermConvertible MaudeText | |
| Monoid MaudeText | |
| GetRange MaudeText | |
| Pretty MaudeText | |
| Typeable * MaudeText | |
| Syntax Maude MaudeText Symbol () () | Instance of Syntax for Maude |
| StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol | Instance of StaticAnalysis for Maude |
| LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () | |
| Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () | Instance of Logic for Maude |
| Comorphism Maude2CASL Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree |
data Spec
data Module
data View
data Parameter
data ModExp
Constructors
| ModExp ModId | |
| SummationModExp ModExp ModExp | |
| RenamingModExp ModExp [Renaming] | |
| InstantiationModExp ModExp [ViewId] |
data Renaming
data ToPartRenaming
data Statement
data Import
data SubsortDecl
data Operator
data Membership
data Equation
data Rule
data Condition
data Attr
data StmntAttr
data Hook
data Term
data Type
newtype Sort
newtype Kind
newtype ParamId
newtype ViewId
newtype ModId
newtype LabelId
newtype OpId
Construction
Information Extraction
getTermType :: Term -> Type