Hets - the Heterogeneous Tool Set

Copyright(c) DFKI GmbH 2009
LicenseGPLv2 or higher, see LICENSE.txt
Maintainerariesco@fdi.ucm.es
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

Maude.AS_Maude

Contents

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.

Synopsis

Types

newtype MaudeText Source #

Constructors

MaudeText String 

Instances

Show MaudeText Source # 

Methods

showsPrec :: Int -> MaudeText -> ShowS

show :: MaudeText -> String

showList :: [MaudeText] -> ShowS

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

Methods

basic_analysis :: Maude -> Maybe ((MaudeText, Sign, GlobalAnnos) -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence])) Source #

sen_analysis :: Maude -> Maybe ((MaudeText, Sign, Sentence) -> Result Sentence) Source #

extBasicAnalysis :: Maude -> IRI -> LibName -> MaudeText -> Sign -> GlobalAnnos -> Result (MaudeText, ExtSign Sign Symbol, [Named Sentence]) Source #

stat_symb_map_items :: Maude -> Sign -> Maybe Sign -> [()] -> Result (EndoMap Symbol) Source #

stat_symb_items :: Maude -> Sign -> [()] -> Result [Symbol] Source #

convertTheory :: Maude -> Maybe ((Sign, [Named Sentence]) -> MaudeText) Source #

ensures_amalgamability :: Maude -> ([CASLAmalgOpt], Gr Sign (Int, Morphism), [(Int, Morphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: Maude -> Morphism -> [Named Sentence] -> Result (Sign, [Named Sentence]) Source #

signature_colimit :: Maude -> Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism) Source #

qualify :: Maude -> SIMPLE_ID -> LibName -> Morphism -> Sign -> Result (Morphism, [Named Sentence]) Source #

symbol_to_raw :: Maude -> Symbol -> Symbol Source #

id_to_raw :: Maude -> Id -> Symbol Source #

matches :: Maude -> Symbol -> Symbol -> Bool Source #

empty_signature :: Maude -> Sign Source #

add_symb_to_sign :: Maude -> Sign -> Symbol -> Result Sign Source #

signature_union :: Maude -> Sign -> Sign -> Result Sign Source #

signatureDiff :: Maude -> Sign -> Sign -> Result Sign Source #

intersection :: Maude -> Sign -> Sign -> Result Sign Source #

final_union :: Maude -> Sign -> Sign -> Result Sign Source #

morphism_union :: Maude -> Morphism -> Morphism -> Result Morphism Source #

is_subsig :: Maude -> Sign -> Sign -> Bool Source #

subsig_inclusion :: Maude -> Sign -> Sign -> Result Morphism Source #

generated_sign :: Maude -> Set Symbol -> Sign -> Result Morphism Source #

cogenerated_sign :: Maude -> Set Symbol -> Sign -> Result Morphism Source #

induced_from_morphism :: Maude -> EndoMap Symbol -> Sign -> Result Morphism Source #

induced_from_to_morphism :: Maude -> EndoMap Symbol -> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism Source #

is_transportable :: Maude -> Morphism -> Bool Source #

is_injective :: Maude -> Morphism -> Bool Source #

theory_to_taxonomy :: Maude -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named Sentence] -> Result MMiSSOntology Source #

corresp2th :: Maude -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap Symbol -> EndoMap Symbol -> REL_REF -> Result (Sign, [Named Sentence], Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

equiv2cospan :: Maude -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap Symbol, EndoMap Symbol) Source #

extract_module :: Maude -> [IRI] -> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence]) Source #

LogicalFramework Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source # 

Methods

base_sig :: Maude -> Sign Source #

write_logic :: Maude -> String -> String Source #

write_syntax :: Maude -> String -> Morphism -> String Source #

write_proof :: Maude -> String -> Morphism -> String Source #

write_model :: Maude -> String -> Morphism -> String Source #

read_morphism :: Maude -> FilePath -> Morphism Source #

write_comorphism :: Maude -> String -> String -> String -> Morphism -> Morphism -> Morphism -> String Source #

Logic Maude () MaudeText Sentence () () Sign Morphism Symbol Symbol () Source #

Instance of Logic for Maude

Methods

parse_basic_sen :: Maude -> Maybe (MaudeText -> AParser st Sentence) Source #

stability :: Maude -> Stability Source #

data_logic :: Maude -> Maybe AnyLogic Source #

top_sublogic :: Maude -> () Source #

all_sublogics :: Maude -> [()] Source #

bottomSublogic :: Maude -> Maybe () Source #

sublogicDimensions :: Maude -> [[()]] Source #

parseSublogic :: Maude -> String -> Maybe () Source #

proj_sublogic_epsilon :: Maude -> () -> Sign -> Morphism Source #

provers :: Maude -> [Prover Sign Sentence Morphism () ()] Source #

default_prover :: Maude -> String Source #

cons_checkers :: Maude -> [ConsChecker Sign Sentence () Morphism ()] Source #

conservativityCheck :: Maude -> [ConservativityChecker Sign Sentence Morphism] Source #

empty_proof_tree :: Maude -> () Source #

syntaxTable :: Maude -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: Maude -> Maybe OMCD Source #

export_symToOmdoc :: Maude -> NameMap Symbol -> Symbol -> String -> Result TCElement Source #

export_senToOmdoc :: Maude -> NameMap Symbol -> Sentence -> Result TCorOMElement Source #

export_theoryToOmdoc :: Maude -> SigMap Symbol -> Sign -> [Named Sentence] -> Result [TCElement] Source #

omdocToSym :: Maude -> SigMapI Symbol -> TCElement -> String -> Result Symbol Source #

omdocToSen :: Maude -> SigMapI Symbol -> TCElement -> String -> Result (Maybe (Named Sentence)) Source #

addOMadtToTheory :: Maude -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [[OmdADT]] -> Result (Sign, [Named Sentence]) Source #

addOmdocToTheory :: Maude -> SigMapI Symbol -> (Sign, [Named Sentence]) -> [TCElement] -> Result (Sign, [Named Sentence]) Source #

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 # 

type Qid = Token Source #

data Spec Source #

Instances

Eq Spec Source # 

Methods

(==) :: Spec -> Spec -> Bool

(/=) :: Spec -> Spec -> Bool

Data Spec Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Spec -> c Spec

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Spec

toConstr :: Spec -> Constr

dataTypeOf :: Spec -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Spec)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Spec)

gmapT :: (forall b. Data b => b -> b) -> Spec -> Spec

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Spec -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Spec -> r

gmapQ :: (forall d. Data d => d -> u) -> Spec -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Spec -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Spec -> m Spec

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Spec -> m Spec

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Spec -> m Spec

Ord Spec Source # 

Methods

compare :: Spec -> Spec -> Ordering

(<) :: Spec -> Spec -> Bool

(<=) :: Spec -> Spec -> Bool

(>) :: Spec -> Spec -> Bool

(>=) :: Spec -> Spec -> Bool

max :: Spec -> Spec -> Spec

min :: Spec -> Spec -> Spec

Read Spec Source # 

Methods

readsPrec :: Int -> ReadS Spec

readList :: ReadS [Spec]

readPrec :: ReadPrec Spec

readListPrec :: ReadPrec [Spec]

Show Spec Source # 

Methods

showsPrec :: Int -> Spec -> ShowS

show :: Spec -> String

showList :: [Spec] -> ShowS

HasName Spec Source # 

Methods

getName :: Spec -> Qid Source #

mapName :: (Qid -> Qid) -> Spec -> Spec Source #

data Module Source #

Constructors

Module ModId [Parameter] [Statement] 

Instances

Eq Module Source # 

Methods

(==) :: Module -> Module -> Bool

(/=) :: Module -> Module -> Bool

Data Module Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Module -> c Module

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Module

toConstr :: Module -> Constr

dataTypeOf :: Module -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Module)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Module)

gmapT :: (forall b. Data b => b -> b) -> Module -> Module

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Module -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Module -> r

gmapQ :: (forall d. Data d => d -> u) -> Module -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Module -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Module -> m Module

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Module -> m Module

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Module -> m Module

Ord Module Source # 

Methods

compare :: Module -> Module -> Ordering

(<) :: Module -> Module -> Bool

(<=) :: Module -> Module -> Bool

(>) :: Module -> Module -> Bool

(>=) :: Module -> Module -> Bool

max :: Module -> Module -> Module

min :: Module -> Module -> Module

Read Module Source # 

Methods

readsPrec :: Int -> ReadS Module

readList :: ReadS [Module]

readPrec :: ReadPrec Module

readListPrec :: ReadPrec [Module]

Show Module Source # 

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

HasName Module Source # 

Methods

getName :: Module -> Qid Source #

mapName :: (Qid -> Qid) -> Module -> Module Source #

data View Source #

Constructors

View ModId ModExp ModExp [Renaming] 

Instances

Eq View Source # 

Methods

(==) :: View -> View -> Bool

(/=) :: View -> View -> Bool

Data View Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> View -> c View

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c View

toConstr :: View -> Constr

dataTypeOf :: View -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c View)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c View)

gmapT :: (forall b. Data b => b -> b) -> View -> View

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> View -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> View -> r

gmapQ :: (forall d. Data d => d -> u) -> View -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> View -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> View -> m View

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> View -> m View

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> View -> m View

Ord View Source # 

Methods

compare :: View -> View -> Ordering

(<) :: View -> View -> Bool

(<=) :: View -> View -> Bool

(>) :: View -> View -> Bool

(>=) :: View -> View -> Bool

max :: View -> View -> View

min :: View -> View -> View

Read View Source # 

Methods

readsPrec :: Int -> ReadS View

readList :: ReadS [View]

readPrec :: ReadPrec View

readListPrec :: ReadPrec [View]

Show View Source # 

Methods

showsPrec :: Int -> View -> ShowS

show :: View -> String

showList :: [View] -> ShowS

HasName View Source # 

Methods

getName :: View -> Qid Source #

mapName :: (Qid -> Qid) -> View -> View Source #

data Parameter Source #

Constructors

Parameter Sort ModExp 

Instances

Eq Parameter Source # 

Methods

(==) :: Parameter -> Parameter -> Bool

(/=) :: Parameter -> Parameter -> Bool

Data Parameter Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Parameter -> c Parameter

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Parameter

toConstr :: Parameter -> Constr

dataTypeOf :: Parameter -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Parameter)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Parameter)

gmapT :: (forall b. Data b => b -> b) -> Parameter -> Parameter

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Parameter -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Parameter -> r

gmapQ :: (forall d. Data d => d -> u) -> Parameter -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Parameter -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Parameter -> m Parameter

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Parameter -> m Parameter

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Parameter -> m Parameter

Ord Parameter Source # 

Methods

compare :: Parameter -> Parameter -> Ordering

(<) :: Parameter -> Parameter -> Bool

(<=) :: Parameter -> Parameter -> Bool

(>) :: Parameter -> Parameter -> Bool

(>=) :: Parameter -> Parameter -> Bool

max :: Parameter -> Parameter -> Parameter

min :: Parameter -> Parameter -> Parameter

Read Parameter Source # 

Methods

readsPrec :: Int -> ReadS Parameter

readList :: ReadS [Parameter]

readPrec :: ReadPrec Parameter

readListPrec :: ReadPrec [Parameter]

Show Parameter Source # 

Methods

showsPrec :: Int -> Parameter -> ShowS

show :: Parameter -> String

showList :: [Parameter] -> ShowS

data ModExp Source #

Instances

Eq ModExp Source # 

Methods

(==) :: ModExp -> ModExp -> Bool

(/=) :: ModExp -> ModExp -> Bool

Data ModExp Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModExp -> c ModExp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModExp

toConstr :: ModExp -> Constr

dataTypeOf :: ModExp -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ModExp)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModExp)

gmapT :: (forall b. Data b => b -> b) -> ModExp -> ModExp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModExp -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModExp -> r

gmapQ :: (forall d. Data d => d -> u) -> ModExp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModExp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModExp -> m ModExp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModExp -> m ModExp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModExp -> m ModExp

Ord ModExp Source # 

Methods

compare :: ModExp -> ModExp -> Ordering

(<) :: ModExp -> ModExp -> Bool

(<=) :: ModExp -> ModExp -> Bool

(>) :: ModExp -> ModExp -> Bool

(>=) :: ModExp -> ModExp -> Bool

max :: ModExp -> ModExp -> ModExp

min :: ModExp -> ModExp -> ModExp

Read ModExp Source # 

Methods

readsPrec :: Int -> ReadS ModExp

readList :: ReadS [ModExp]

readPrec :: ReadPrec ModExp

readListPrec :: ReadPrec [ModExp]

Show ModExp Source # 

Methods

showsPrec :: Int -> ModExp -> ShowS

show :: ModExp -> String

showList :: [ModExp] -> ShowS

data Renaming Source #

Instances

Eq Renaming Source # 

Methods

(==) :: Renaming -> Renaming -> Bool

(/=) :: Renaming -> Renaming -> Bool

Data Renaming Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Renaming -> c Renaming

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Renaming

toConstr :: Renaming -> Constr

dataTypeOf :: Renaming -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Renaming)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Renaming)

gmapT :: (forall b. Data b => b -> b) -> Renaming -> Renaming

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Renaming -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Renaming -> r

gmapQ :: (forall d. Data d => d -> u) -> Renaming -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Renaming -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Renaming -> m Renaming

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming -> m Renaming

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Renaming -> m Renaming

Ord Renaming Source # 

Methods

compare :: Renaming -> Renaming -> Ordering

(<) :: Renaming -> Renaming -> Bool

(<=) :: Renaming -> Renaming -> Bool

(>) :: Renaming -> Renaming -> Bool

(>=) :: Renaming -> Renaming -> Bool

max :: Renaming -> Renaming -> Renaming

min :: Renaming -> Renaming -> Renaming

Read Renaming Source # 

Methods

readsPrec :: Int -> ReadS Renaming

readList :: ReadS [Renaming]

readPrec :: ReadPrec Renaming

readListPrec :: ReadPrec [Renaming]

Show Renaming Source # 

Methods

showsPrec :: Int -> Renaming -> ShowS

show :: Renaming -> String

showList :: [Renaming] -> ShowS

data ToPartRenaming Source #

Constructors

To OpId [Attr] 

Instances

Eq ToPartRenaming Source # 
Data ToPartRenaming Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ToPartRenaming -> c ToPartRenaming

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ToPartRenaming

toConstr :: ToPartRenaming -> Constr

dataTypeOf :: ToPartRenaming -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ToPartRenaming)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ToPartRenaming)

gmapT :: (forall b. Data b => b -> b) -> ToPartRenaming -> ToPartRenaming

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ToPartRenaming -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ToPartRenaming -> r

gmapQ :: (forall d. Data d => d -> u) -> ToPartRenaming -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ToPartRenaming -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ToPartRenaming -> m ToPartRenaming

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ToPartRenaming -> m ToPartRenaming

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ToPartRenaming -> m ToPartRenaming

Ord ToPartRenaming Source # 
Read ToPartRenaming Source # 

Methods

readsPrec :: Int -> ReadS ToPartRenaming

readList :: ReadS [ToPartRenaming]

readPrec :: ReadPrec ToPartRenaming

readListPrec :: ReadPrec [ToPartRenaming]

Show ToPartRenaming Source # 

Methods

showsPrec :: Int -> ToPartRenaming -> ShowS

show :: ToPartRenaming -> String

showList :: [ToPartRenaming] -> ShowS

data Statement Source #

Instances

Eq Statement Source # 

Methods

(==) :: Statement -> Statement -> Bool

(/=) :: Statement -> Statement -> Bool

Data Statement Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Statement -> c Statement

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Statement

toConstr :: Statement -> Constr

dataTypeOf :: Statement -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Statement)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Statement)

gmapT :: (forall b. Data b => b -> b) -> Statement -> Statement

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Statement -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Statement -> r

gmapQ :: (forall d. Data d => d -> u) -> Statement -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Statement -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Statement -> m Statement

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Statement -> m Statement

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Statement -> m Statement

Ord Statement Source # 

Methods

compare :: Statement -> Statement -> Ordering

(<) :: Statement -> Statement -> Bool

(<=) :: Statement -> Statement -> Bool

(>) :: Statement -> Statement -> Bool

(>=) :: Statement -> Statement -> Bool

max :: Statement -> Statement -> Statement

min :: Statement -> Statement -> Statement

Read Statement Source # 

Methods

readsPrec :: Int -> ReadS Statement

readList :: ReadS [Statement]

readPrec :: ReadPrec Statement

readListPrec :: ReadPrec [Statement]

Show Statement Source # 

Methods

showsPrec :: Int -> Statement -> ShowS

show :: Statement -> String

showList :: [Statement] -> ShowS

data Import Source #

Instances

Eq Import Source # 

Methods

(==) :: Import -> Import -> Bool

(/=) :: Import -> Import -> Bool

Data Import Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Import -> c Import

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Import

toConstr :: Import -> Constr

dataTypeOf :: Import -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Import)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Import)

gmapT :: (forall b. Data b => b -> b) -> Import -> Import

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Import -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Import -> r

gmapQ :: (forall d. Data d => d -> u) -> Import -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Import -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Import -> m Import

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Import -> m Import

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Import -> m Import

Ord Import Source # 

Methods

compare :: Import -> Import -> Ordering

(<) :: Import -> Import -> Bool

(<=) :: Import -> Import -> Bool

(>) :: Import -> Import -> Bool

(>=) :: Import -> Import -> Bool

max :: Import -> Import -> Import

min :: Import -> Import -> Import

Read Import Source # 

Methods

readsPrec :: Int -> ReadS Import

readList :: ReadS [Import]

readPrec :: ReadPrec Import

readListPrec :: ReadPrec [Import]

Show Import Source # 

Methods

showsPrec :: Int -> Import -> ShowS

show :: Import -> String

showList :: [Import] -> ShowS

data SubsortDecl Source #

Constructors

Subsort Sort Sort 

Instances

Eq SubsortDecl Source # 

Methods

(==) :: SubsortDecl -> SubsortDecl -> Bool

(/=) :: SubsortDecl -> SubsortDecl -> Bool

Data SubsortDecl Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SubsortDecl -> c SubsortDecl

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SubsortDecl

toConstr :: SubsortDecl -> Constr

dataTypeOf :: SubsortDecl -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c SubsortDecl)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SubsortDecl)

gmapT :: (forall b. Data b => b -> b) -> SubsortDecl -> SubsortDecl

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SubsortDecl -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SubsortDecl -> r

gmapQ :: (forall d. Data d => d -> u) -> SubsortDecl -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> SubsortDecl -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SubsortDecl -> m SubsortDecl

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SubsortDecl -> m SubsortDecl

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SubsortDecl -> m SubsortDecl

Ord SubsortDecl Source # 
Read SubsortDecl Source # 

Methods

readsPrec :: Int -> ReadS SubsortDecl

readList :: ReadS [SubsortDecl]

readPrec :: ReadPrec SubsortDecl

readListPrec :: ReadPrec [SubsortDecl]

Show SubsortDecl Source # 

Methods

showsPrec :: Int -> SubsortDecl -> ShowS

show :: SubsortDecl -> String

showList :: [SubsortDecl] -> ShowS

data Operator Source #

Constructors

Op OpId [Type] Type [Attr] 

Instances

Eq Operator Source # 

Methods

(==) :: Operator -> Operator -> Bool

(/=) :: Operator -> Operator -> Bool

Data Operator Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Operator -> c Operator

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Operator

toConstr :: Operator -> Constr

dataTypeOf :: Operator -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Operator)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Operator)

gmapT :: (forall b. Data b => b -> b) -> Operator -> Operator

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Operator -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Operator -> r

gmapQ :: (forall d. Data d => d -> u) -> Operator -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Operator -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Operator -> m Operator

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Operator -> m Operator

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Operator -> m Operator

Ord Operator Source # 

Methods

compare :: Operator -> Operator -> Ordering

(<) :: Operator -> Operator -> Bool

(<=) :: Operator -> Operator -> Bool

(>) :: Operator -> Operator -> Bool

(>=) :: Operator -> Operator -> Bool

max :: Operator -> Operator -> Operator

min :: Operator -> Operator -> Operator

Read Operator Source # 

Methods

readsPrec :: Int -> ReadS Operator

readList :: ReadS [Operator]

readPrec :: ReadPrec Operator

readListPrec :: ReadPrec [Operator]

Show Operator Source # 

Methods

showsPrec :: Int -> Operator -> ShowS

show :: Operator -> String

showList :: [Operator] -> ShowS

HasName Operator Source # 
AsSymbol Operator Source # 
HasOps Operator Source # 
HasSorts Operator Source # 

data Membership Source #

Constructors

Mb Term Sort [Condition] [StmntAttr] 

Instances

Eq Membership Source # 

Methods

(==) :: Membership -> Membership -> Bool

(/=) :: Membership -> Membership -> Bool

Data Membership Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Membership -> c Membership

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Membership

toConstr :: Membership -> Constr

dataTypeOf :: Membership -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Membership)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Membership)

gmapT :: (forall b. Data b => b -> b) -> Membership -> Membership

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Membership -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Membership -> r

gmapQ :: (forall d. Data d => d -> u) -> Membership -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Membership -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Membership -> m Membership

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Membership -> m Membership

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Membership -> m Membership

Ord Membership Source # 
Read Membership Source # 

Methods

readsPrec :: Int -> ReadS Membership

readList :: ReadS [Membership]

readPrec :: ReadPrec Membership

readListPrec :: ReadPrec [Membership]

Show Membership Source # 

Methods

showsPrec :: Int -> Membership -> ShowS

show :: Membership -> String

showList :: [Membership] -> ShowS

HasLabels Membership Source # 
HasOps Membership Source # 
HasSorts Membership Source # 

data Equation Source #

Constructors

Eq Term Term [Condition] [StmntAttr] 

Instances

Eq Equation Source # 

Methods

(==) :: Equation -> Equation -> Bool

(/=) :: Equation -> Equation -> Bool

Data Equation Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Equation -> c Equation

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Equation

toConstr :: Equation -> Constr

dataTypeOf :: Equation -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Equation)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Equation)

gmapT :: (forall b. Data b => b -> b) -> Equation -> Equation

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Equation -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Equation -> r

gmapQ :: (forall d. Data d => d -> u) -> Equation -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Equation -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Equation -> m Equation

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Equation -> m Equation

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Equation -> m Equation

Ord Equation Source # 

Methods

compare :: Equation -> Equation -> Ordering

(<) :: Equation -> Equation -> Bool

(<=) :: Equation -> Equation -> Bool

(>) :: Equation -> Equation -> Bool

(>=) :: Equation -> Equation -> Bool

max :: Equation -> Equation -> Equation

min :: Equation -> Equation -> Equation

Read Equation Source # 

Methods

readsPrec :: Int -> ReadS Equation

readList :: ReadS [Equation]

readPrec :: ReadPrec Equation

readListPrec :: ReadPrec [Equation]

Show Equation Source # 

Methods

showsPrec :: Int -> Equation -> ShowS

show :: Equation -> String

showList :: [Equation] -> ShowS

HasLabels Equation Source # 
HasOps Equation Source # 
HasSorts Equation Source # 

data Rule Source #

Constructors

Rl Term Term [Condition] [StmntAttr] 

Instances

Eq Rule Source # 

Methods

(==) :: Rule -> Rule -> Bool

(/=) :: Rule -> Rule -> Bool

Data Rule Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Rule -> c Rule

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Rule

toConstr :: Rule -> Constr

dataTypeOf :: Rule -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Rule)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Rule)

gmapT :: (forall b. Data b => b -> b) -> Rule -> Rule

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Rule -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Rule -> r

gmapQ :: (forall d. Data d => d -> u) -> Rule -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Rule -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Rule -> m Rule

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Rule -> m Rule

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Rule -> m Rule

Ord Rule Source # 

Methods

compare :: Rule -> Rule -> Ordering

(<) :: Rule -> Rule -> Bool

(<=) :: Rule -> Rule -> Bool

(>) :: Rule -> Rule -> Bool

(>=) :: Rule -> Rule -> Bool

max :: Rule -> Rule -> Rule

min :: Rule -> Rule -> Rule

Read Rule Source # 

Methods

readsPrec :: Int -> ReadS Rule

readList :: ReadS [Rule]

readPrec :: ReadPrec Rule

readListPrec :: ReadPrec [Rule]

Show Rule Source # 

Methods

showsPrec :: Int -> Rule -> ShowS

show :: Rule -> String

showList :: [Rule] -> ShowS

HasLabels Rule Source # 
HasOps Rule Source # 
HasSorts Rule Source # 

data Condition Source #

Instances

Eq Condition Source # 

Methods

(==) :: Condition -> Condition -> Bool

(/=) :: Condition -> Condition -> Bool

Data Condition Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Condition -> c Condition

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Condition

toConstr :: Condition -> Constr

dataTypeOf :: Condition -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Condition)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Condition)

gmapT :: (forall b. Data b => b -> b) -> Condition -> Condition

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Condition -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Condition -> r

gmapQ :: (forall d. Data d => d -> u) -> Condition -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Condition -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Condition -> m Condition

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Condition -> m Condition

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Condition -> m Condition

Ord Condition Source # 

Methods

compare :: Condition -> Condition -> Ordering

(<) :: Condition -> Condition -> Bool

(<=) :: Condition -> Condition -> Bool

(>) :: Condition -> Condition -> Bool

(>=) :: Condition -> Condition -> Bool

max :: Condition -> Condition -> Condition

min :: Condition -> Condition -> Condition

Read Condition Source # 

Methods

readsPrec :: Int -> ReadS Condition

readList :: ReadS [Condition]

readPrec :: ReadPrec Condition

readListPrec :: ReadPrec [Condition]

Show Condition Source # 

Methods

showsPrec :: Int -> Condition -> ShowS

show :: Condition -> String

showList :: [Condition] -> ShowS

HasOps Condition Source # 
HasSorts Condition Source # 

data Attr Source #

Constructors

Assoc 
Comm 
Idem 
Iter 
Id Term 
LeftId Term 
RightId Term 
Strat [Int] 
Memo 
Prec Int 
Gather [Qid] 
Format [Qid] 
Ctor 
Config 
Object 
Msg 
Frozen [Int] 
Poly [Int] 
Special [Hook] 

Instances

Eq Attr Source # 

Methods

(==) :: Attr -> Attr -> Bool

(/=) :: Attr -> Attr -> Bool

Data Attr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Attr -> c Attr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Attr

toConstr :: Attr -> Constr

dataTypeOf :: Attr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Attr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Attr)

gmapT :: (forall b. Data b => b -> b) -> Attr -> Attr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Attr -> r

gmapQ :: (forall d. Data d => d -> u) -> Attr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Attr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Attr -> m Attr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Attr -> m Attr

Ord Attr Source # 

Methods

compare :: Attr -> Attr -> Ordering

(<) :: Attr -> Attr -> Bool

(<=) :: Attr -> Attr -> Bool

(>) :: Attr -> Attr -> Bool

(>=) :: Attr -> Attr -> Bool

max :: Attr -> Attr -> Attr

min :: Attr -> Attr -> Attr

Read Attr Source # 

Methods

readsPrec :: Int -> ReadS Attr

readList :: ReadS [Attr]

readPrec :: ReadPrec Attr

readListPrec :: ReadPrec [Attr]

Show Attr Source # 

Methods

showsPrec :: Int -> Attr -> ShowS

show :: Attr -> String

showList :: [Attr] -> ShowS

HasOps Attr Source # 
HasSorts Attr Source # 

data StmntAttr Source #

Constructors

Label Qid 
Metadata String 
Owise 
Nonexec 
Print [Qid] 

Instances

Eq StmntAttr Source # 

Methods

(==) :: StmntAttr -> StmntAttr -> Bool

(/=) :: StmntAttr -> StmntAttr -> Bool

Data StmntAttr Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> StmntAttr -> c StmntAttr

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c StmntAttr

toConstr :: StmntAttr -> Constr

dataTypeOf :: StmntAttr -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c StmntAttr)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c StmntAttr)

gmapT :: (forall b. Data b => b -> b) -> StmntAttr -> StmntAttr

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> StmntAttr -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> StmntAttr -> r

gmapQ :: (forall d. Data d => d -> u) -> StmntAttr -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> StmntAttr -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> StmntAttr -> m StmntAttr

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> StmntAttr -> m StmntAttr

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> StmntAttr -> m StmntAttr

Ord StmntAttr Source # 

Methods

compare :: StmntAttr -> StmntAttr -> Ordering

(<) :: StmntAttr -> StmntAttr -> Bool

(<=) :: StmntAttr -> StmntAttr -> Bool

(>) :: StmntAttr -> StmntAttr -> Bool

(>=) :: StmntAttr -> StmntAttr -> Bool

max :: StmntAttr -> StmntAttr -> StmntAttr

min :: StmntAttr -> StmntAttr -> StmntAttr

Read StmntAttr Source # 

Methods

readsPrec :: Int -> ReadS StmntAttr

readList :: ReadS [StmntAttr]

readPrec :: ReadPrec StmntAttr

readListPrec :: ReadPrec [StmntAttr]

Show StmntAttr Source # 

Methods

showsPrec :: Int -> StmntAttr -> ShowS

show :: StmntAttr -> String

showList :: [StmntAttr] -> ShowS

AsSymbol StmntAttr Source # 
HasLabels StmntAttr Source # 

data Hook Source #

Constructors

IdHook Qid [Qid] 
OpHook Qid Qid [Qid] Qid 
TermHook Qid Term 

Instances

Eq Hook Source # 

Methods

(==) :: Hook -> Hook -> Bool

(/=) :: Hook -> Hook -> Bool

Data Hook Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Hook -> c Hook

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Hook

toConstr :: Hook -> Constr

dataTypeOf :: Hook -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Hook)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Hook)

gmapT :: (forall b. Data b => b -> b) -> Hook -> Hook

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Hook -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Hook -> r

gmapQ :: (forall d. Data d => d -> u) -> Hook -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Hook -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Hook -> m Hook

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Hook -> m Hook

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Hook -> m Hook

Ord Hook Source # 

Methods

compare :: Hook -> Hook -> Ordering

(<) :: Hook -> Hook -> Bool

(<=) :: Hook -> Hook -> Bool

(>) :: Hook -> Hook -> Bool

(>=) :: Hook -> Hook -> Bool

max :: Hook -> Hook -> Hook

min :: Hook -> Hook -> Hook

Read Hook Source # 

Methods

readsPrec :: Int -> ReadS Hook

readList :: ReadS [Hook]

readPrec :: ReadPrec Hook

readListPrec :: ReadPrec [Hook]

Show Hook Source # 

Methods

showsPrec :: Int -> Hook -> ShowS

show :: Hook -> String

showList :: [Hook] -> ShowS

data Term Source #

Constructors

Const Qid Type 
Var Qid Type 
Apply Qid [Term] Type 

Instances

Eq Term Source # 

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Data Term Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term -> c Term

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Term

toConstr :: Term -> Constr

dataTypeOf :: Term -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Term)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Term)

gmapT :: (forall b. Data b => b -> b) -> Term -> Term

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term -> r

gmapQ :: (forall d. Data d => d -> u) -> Term -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term -> m Term

Ord Term Source # 

Methods

compare :: Term -> Term -> Ordering

(<) :: Term -> Term -> Bool

(<=) :: Term -> Term -> Bool

(>) :: Term -> Term -> Bool

(>=) :: Term -> Term -> Bool

max :: Term -> Term -> Term

min :: Term -> Term -> Term

Read Term Source # 

Methods

readsPrec :: Int -> ReadS Term

readList :: ReadS [Term]

readPrec :: ReadPrec Term

readListPrec :: ReadPrec [Term]

Show Term Source # 

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

AsSymbol Term Source # 
HasOps Term Source # 
HasSorts Term Source # 

data Type Source #

Constructors

TypeSort Sort 
TypeKind Kind 

Instances

Eq Type Source # 

Methods

(==) :: Type -> Type -> Bool

(/=) :: Type -> Type -> Bool

Data Type Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Type -> c Type

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Type

toConstr :: Type -> Constr

dataTypeOf :: Type -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Type)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Type)

gmapT :: (forall b. Data b => b -> b) -> Type -> Type

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Type -> r

gmapQ :: (forall d. Data d => d -> u) -> Type -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Type -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Type -> m Type

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Type -> m Type

Ord Type Source # 

Methods

compare :: Type -> Type -> Ordering

(<) :: Type -> Type -> Bool

(<=) :: Type -> Type -> Bool

(>) :: Type -> Type -> Bool

(>=) :: Type -> Type -> Bool

max :: Type -> Type -> Type

min :: Type -> Type -> Type

Read Type Source # 

Methods

readsPrec :: Int -> ReadS Type

readList :: ReadS [Type]

readPrec :: ReadPrec Type

readListPrec :: ReadPrec [Type]

Show Type Source # 

Methods

showsPrec :: Int -> Type -> ShowS

show :: Type -> String

showList :: [Type] -> ShowS

HasName Type Source # 

Methods

getName :: Type -> Qid Source #

mapName :: (Qid -> Qid) -> Type -> Type Source #

AsSymbol Type Source # 
HasSorts Type Source # 

newtype Sort Source #

Constructors

SortId Qid 

Instances

Eq Sort Source # 

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Data Sort Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sort -> c Sort

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sort

toConstr :: Sort -> Constr

dataTypeOf :: Sort -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Sort)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sort)

gmapT :: (forall b. Data b => b -> b) -> Sort -> Sort

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sort -> r

gmapQ :: (forall d. Data d => d -> u) -> Sort -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sort -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sort -> m Sort

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sort -> m Sort

Ord Sort Source # 

Methods

compare :: Sort -> Sort -> Ordering

(<) :: Sort -> Sort -> Bool

(<=) :: Sort -> Sort -> Bool

(>) :: Sort -> Sort -> Bool

(>=) :: Sort -> Sort -> Bool

max :: Sort -> Sort -> Sort

min :: Sort -> Sort -> Sort

Read Sort Source # 

Methods

readsPrec :: Int -> ReadS Sort

readList :: ReadS [Sort]

readPrec :: ReadPrec Sort

readListPrec :: ReadPrec [Sort]

Show Sort Source # 

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

HasName Sort Source # 

Methods

getName :: Sort -> Qid Source #

mapName :: (Qid -> Qid) -> Sort -> Sort Source #

AsSymbol Sort Source # 
HasSorts Sort Source # 

newtype Kind Source #

Constructors

KindId Qid 

Instances

Eq Kind Source # 

Methods

(==) :: Kind -> Kind -> Bool

(/=) :: Kind -> Kind -> Bool

Data Kind Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Kind -> c Kind

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Kind

toConstr :: Kind -> Constr

dataTypeOf :: Kind -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Kind)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Kind)

gmapT :: (forall b. Data b => b -> b) -> Kind -> Kind

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Kind -> r

gmapQ :: (forall d. Data d => d -> u) -> Kind -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Kind -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Kind -> m Kind

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Kind -> m Kind

Ord Kind Source # 

Methods

compare :: Kind -> Kind -> Ordering

(<) :: Kind -> Kind -> Bool

(<=) :: Kind -> Kind -> Bool

(>) :: Kind -> Kind -> Bool

(>=) :: Kind -> Kind -> Bool

max :: Kind -> Kind -> Kind

min :: Kind -> Kind -> Kind

Read Kind Source # 

Methods

readsPrec :: Int -> ReadS Kind

readList :: ReadS [Kind]

readPrec :: ReadPrec Kind

readListPrec :: ReadPrec [Kind]

Show Kind Source # 

Methods

showsPrec :: Int -> Kind -> ShowS

show :: Kind -> String

showList :: [Kind] -> ShowS

HasName Kind Source # 

Methods

getName :: Kind -> Qid Source #

mapName :: (Qid -> Qid) -> Kind -> Kind Source #

AsSymbol Kind Source # 
HasSorts Kind Source # 

newtype ParamId Source #

Constructors

ParamId Qid 

Instances

Eq ParamId Source # 

Methods

(==) :: ParamId -> ParamId -> Bool

(/=) :: ParamId -> ParamId -> Bool

Data ParamId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParamId -> c ParamId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ParamId

toConstr :: ParamId -> Constr

dataTypeOf :: ParamId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ParamId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ParamId)

gmapT :: (forall b. Data b => b -> b) -> ParamId -> ParamId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParamId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParamId -> r

gmapQ :: (forall d. Data d => d -> u) -> ParamId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ParamId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParamId -> m ParamId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParamId -> m ParamId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParamId -> m ParamId

Ord ParamId Source # 

Methods

compare :: ParamId -> ParamId -> Ordering

(<) :: ParamId -> ParamId -> Bool

(<=) :: ParamId -> ParamId -> Bool

(>) :: ParamId -> ParamId -> Bool

(>=) :: ParamId -> ParamId -> Bool

max :: ParamId -> ParamId -> ParamId

min :: ParamId -> ParamId -> ParamId

Read ParamId Source # 

Methods

readsPrec :: Int -> ReadS ParamId

readList :: ReadS [ParamId]

readPrec :: ReadPrec ParamId

readListPrec :: ReadPrec [ParamId]

Show ParamId Source # 

Methods

showsPrec :: Int -> ParamId -> ShowS

show :: ParamId -> String

showList :: [ParamId] -> ShowS

HasName ParamId Source # 

newtype ViewId Source #

Constructors

ViewId Qid 

Instances

Eq ViewId Source # 

Methods

(==) :: ViewId -> ViewId -> Bool

(/=) :: ViewId -> ViewId -> Bool

Data ViewId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ViewId -> c ViewId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ViewId

toConstr :: ViewId -> Constr

dataTypeOf :: ViewId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ViewId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ViewId)

gmapT :: (forall b. Data b => b -> b) -> ViewId -> ViewId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ViewId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ViewId -> r

gmapQ :: (forall d. Data d => d -> u) -> ViewId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ViewId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ViewId -> m ViewId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ViewId -> m ViewId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ViewId -> m ViewId

Ord ViewId Source # 

Methods

compare :: ViewId -> ViewId -> Ordering

(<) :: ViewId -> ViewId -> Bool

(<=) :: ViewId -> ViewId -> Bool

(>) :: ViewId -> ViewId -> Bool

(>=) :: ViewId -> ViewId -> Bool

max :: ViewId -> ViewId -> ViewId

min :: ViewId -> ViewId -> ViewId

Read ViewId Source # 

Methods

readsPrec :: Int -> ReadS ViewId

readList :: ReadS [ViewId]

readPrec :: ReadPrec ViewId

readListPrec :: ReadPrec [ViewId]

Show ViewId Source # 

Methods

showsPrec :: Int -> ViewId -> ShowS

show :: ViewId -> String

showList :: [ViewId] -> ShowS

HasName ViewId Source # 

Methods

getName :: ViewId -> Qid Source #

mapName :: (Qid -> Qid) -> ViewId -> ViewId Source #

newtype ModId Source #

Constructors

ModId Qid 

Instances

Eq ModId Source # 

Methods

(==) :: ModId -> ModId -> Bool

(/=) :: ModId -> ModId -> Bool

Data ModId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ModId -> c ModId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ModId

toConstr :: ModId -> Constr

dataTypeOf :: ModId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ModId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ModId)

gmapT :: (forall b. Data b => b -> b) -> ModId -> ModId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ModId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ModId -> r

gmapQ :: (forall d. Data d => d -> u) -> ModId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ModId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ModId -> m ModId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ModId -> m ModId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ModId -> m ModId

Ord ModId Source # 

Methods

compare :: ModId -> ModId -> Ordering

(<) :: ModId -> ModId -> Bool

(<=) :: ModId -> ModId -> Bool

(>) :: ModId -> ModId -> Bool

(>=) :: ModId -> ModId -> Bool

max :: ModId -> ModId -> ModId

min :: ModId -> ModId -> ModId

Read ModId Source # 

Methods

readsPrec :: Int -> ReadS ModId

readList :: ReadS [ModId]

readPrec :: ReadPrec ModId

readListPrec :: ReadPrec [ModId]

Show ModId Source # 

Methods

showsPrec :: Int -> ModId -> ShowS

show :: ModId -> String

showList :: [ModId] -> ShowS

HasName ModId Source # 

Methods

getName :: ModId -> Qid Source #

mapName :: (Qid -> Qid) -> ModId -> ModId Source #

newtype LabelId Source #

Constructors

LabelId Qid 

Instances

Eq LabelId Source # 

Methods

(==) :: LabelId -> LabelId -> Bool

(/=) :: LabelId -> LabelId -> Bool

Data LabelId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LabelId -> c LabelId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LabelId

toConstr :: LabelId -> Constr

dataTypeOf :: LabelId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c LabelId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LabelId)

gmapT :: (forall b. Data b => b -> b) -> LabelId -> LabelId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LabelId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LabelId -> r

gmapQ :: (forall d. Data d => d -> u) -> LabelId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LabelId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LabelId -> m LabelId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LabelId -> m LabelId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LabelId -> m LabelId

Ord LabelId Source # 

Methods

compare :: LabelId -> LabelId -> Ordering

(<) :: LabelId -> LabelId -> Bool

(<=) :: LabelId -> LabelId -> Bool

(>) :: LabelId -> LabelId -> Bool

(>=) :: LabelId -> LabelId -> Bool

max :: LabelId -> LabelId -> LabelId

min :: LabelId -> LabelId -> LabelId

Read LabelId Source # 

Methods

readsPrec :: Int -> ReadS LabelId

readList :: ReadS [LabelId]

readPrec :: ReadPrec LabelId

readListPrec :: ReadPrec [LabelId]

Show LabelId Source # 

Methods

showsPrec :: Int -> LabelId -> ShowS

show :: LabelId -> String

showList :: [LabelId] -> ShowS

HasName LabelId Source # 
AsSymbol LabelId Source # 

newtype OpId Source #

Constructors

OpId Qid 

Instances

Eq OpId Source # 

Methods

(==) :: OpId -> OpId -> Bool

(/=) :: OpId -> OpId -> Bool

Data OpId Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> OpId -> c OpId

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c OpId

toConstr :: OpId -> Constr

dataTypeOf :: OpId -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c OpId)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c OpId)

gmapT :: (forall b. Data b => b -> b) -> OpId -> OpId

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> OpId -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> OpId -> r

gmapQ :: (forall d. Data d => d -> u) -> OpId -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> OpId -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> OpId -> m OpId

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> OpId -> m OpId

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> OpId -> m OpId

Ord OpId Source # 

Methods

compare :: OpId -> OpId -> Ordering

(<) :: OpId -> OpId -> Bool

(<=) :: OpId -> OpId -> Bool

(>) :: OpId -> OpId -> Bool

(>=) :: OpId -> OpId -> Bool

max :: OpId -> OpId -> OpId

min :: OpId -> OpId -> OpId

Read OpId Source # 

Methods

readsPrec :: Int -> ReadS OpId

readList :: ReadS [OpId]

readPrec :: ReadPrec OpId

readListPrec :: ReadPrec [OpId]

Show OpId Source # 

Methods

showsPrec :: Int -> OpId -> ShowS

show :: OpId -> String

showList :: [OpId] -> ShowS

HasName OpId Source # 

Methods

getName :: OpId -> Qid Source #

mapName :: (Qid -> Qid) -> OpId -> OpId Source #

AsSymbol OpId Source # 

Construction

mkVar :: String -> Type -> Term Source #

Create a Var Term from the given arguments.

Information Extraction

getTermType :: Term -> Type Source #

Extract the Type from the given Term.

Attribute Classification

assoc :: Attr -> Bool Source #

True iff the argument is the assoc attribute.

comm :: Attr -> Bool Source #

True iff the argument is the comm attribute.

idem :: Attr -> Bool Source #

True iff the argument is the idem attribute.

idtty :: Attr -> Bool Source #

True iff the argument is the identity attribute.

leftId :: Attr -> Bool Source #

True iff the argument is the left identity attribute.

rightId :: Attr -> Bool Source #

True iff the argument is the right identity attribute.

ctor :: Attr -> Bool Source #

True iff the argument is the ctor attribute.

owise :: StmntAttr -> Bool Source #

True iff the argument is the owise attribute.