Copyright | (c) DFKI GmbH 2009 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | ariesco@fdi.ucm.es |
Stability | experimental |
Portability | portable |
Safe Haskell | Safe |
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
Constructors
MaudeText String |
Instances
Show MaudeText Source # | |
GetRange MaudeText Source # | |
Pretty MaudeText Source # | |
Syntax Maude MaudeText Symbol () () Source # | Instance of Syntax for Maude |
StaticAnalysis Maude MaudeText Sentence () () Sign Morphism Symbol Symbol Source # | Instance of StaticAnalysis for Maude |
LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # | |
Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # | 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 Source # | |
Constructors
ModExp ModId | |
SummationModExp ModExp ModExp | |
RenamingModExp ModExp [Renaming] | |
InstantiationModExp ModExp [ViewId] |
data ToPartRenaming Source #
Instances
Eq ToPartRenaming Source # | |
Data ToPartRenaming Source # | |
Ord ToPartRenaming Source # | |
Read ToPartRenaming Source # | |
Show ToPartRenaming Source # | |
data SubsortDecl Source #
Instances
Eq SubsortDecl Source # | |
Data SubsortDecl Source # | |
Ord SubsortDecl Source # | |
Read SubsortDecl Source # | |
Show SubsortDecl Source # | |
data Membership Source #
Instances
Eq Membership Source # | |
Data Membership Source # | |
Ord Membership Source # | |
Read Membership Source # | |
Show Membership Source # | |
HasLabels Membership Source # | |
HasOps Membership Source # | |
HasSorts Membership Source # | |