Logo Search packages:      
Sourcecode: maude version File versions  Download package

Classes | Public Member Functions | Private Types | Private Member Functions | Static Private Member Functions | Private Attributes

MetaLevel Class Reference

Collaboration diagram for MetaLevel:
Collaboration graph
[legend]

List of all members.

Classes

struct  AttributeInfo
struct  StatementAttributeInfo

Public Member Functions

bool bind (const char *name, Symbol *symbol)
bool bind (const char *name, Term *term)
bool downAssignment (DagNode *metaAssignment, MixfixModule *m, Vector< Term * > &variables, Vector< Term * > &values)
bool downBool (DagNode *metaBool, bool &value)
bool downBound (DagNode *metaBound, int &bound) const
bool downBound64 (DagNode *metaBound, Int64 &bound) const
bool downComponent (DagNode *metaComponent, MixfixModule *m, ConnectedComponent *&component)
bool downCondition (DagNode *metaCondition, MixfixModule *m, Vector< ConditionFragment * > &condition)
MetaModuledownModule (DagNode *metaModule, bool cacheMetaModule=true, Interpreter *owner=0)
bool downOpName (DagNode *metaQid, int &id)
bool downPrintOptionSet (DagNode *metaPrintOptionSet, int &printFlags) const
bool downQid (DagNode *metaQid, int &id)
bool downQidList (DagNode *metaQidList, Vector< int > &ids)
bool downSaturate (DagNode *metaBound, int &bound) const
bool downSaturate64 (DagNode *metaBound, Int64 &bound) const
bool downSimpleSort (DagNode *metaSort, MixfixModule *m, Sort *&sort)
bool downSubstitution (DagNode *metaSubstitution, MixfixModule *m, Vector< Term * > &variables, Vector< Term * > &values)
TermdownTerm (DagNode *metaTerm, MixfixModule *m)
bool downTermAndSort (DagNode *metaTerm, DagNode *metaSort, Term *&term, Sort *&sort, MixfixModule *m)
bool downTermPair (DagNode *metaTerm1, DagNode *metaTerm2, Term *&term1, Term *&term2, MixfixModule *m, bool makeDisjoint=false)
bool downType (DagNode *metaType, MixfixModule *m, Sort *&type)
bool downTypeList (DagNode *metaTypeList, MixfixModule *m, Vector< Sort * > &typeList)
bool downUnificandPair (DagNode *metaUnificandPair, Term *&lhs, Term *&rhs, MixfixModule *m, bool makeDisjoint)
bool downUnificationProblem (DagNode *metaUnificationProblem, Vector< Term * > &leftHandSides, Vector< Term * > &rightHandSides, MixfixModule *m, bool makeDisjoint)
const mpz_class & getNat (const DagNode *dagNode) const
void getSymbolAttachments (Vector< const char * > &purposes, Vector< Symbol * > &symbols)
void getTermAttachments (Vector< const char * > &purposes, Vector< Term * > &terms)
bool isNat (const DagNode *dagNode) const
 MetaLevel (const MetaLevel *original, SymbolMap *map)
void postInterSymbolPass ()
void reset ()
void startVariableMapping (int varCounter, FreshVariableGenerator *varGenerator)
void stopVariableMapping ()
DagNodeupAmbiguity (Term *parse1, Term *parse2, MixfixModule *m)
DagNodeupBool (bool value)
DagNodeupContext (DagNode *dagNode, MixfixModule *m, DagNode *hole, PointerMap &qidMap, PointerMap &dagNodeMap)
DagNodeupDagNode (DagNode *dagNode, MixfixModule *m, PointerMap &qidMap, PointerMap &dagNodeMap)
void upDisjointSubstitutions (const Substitution &substitution, const VariableInfo &variableInfo, MixfixModule *m, PointerMap &qidMap, PointerMap &dagNodeMap, DagNode *&left, DagNode *&right)
DagNodeupEqs (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupFailure4Tuple ()
DagNodeupFailurePair ()
DagNodeupFailureTrace ()
DagNodeupFailureTriple ()
DagNodeupImports (PreModule *pm, PointerMap &qidMap)
DagNodeupKindSet (const Vector< ConnectedComponent * > &kinds)
DagNodeupMatchPair (const Substitution &substitution, const VariableInfo &variableInfo, DagNode *dagNode, DagNode *hole, MixfixModule *m)
DagNodeupMbs (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupModule (bool flat, PreModule *pm, PointerMap &qidMap)
DagNodeupNat (const mpz_class &nat)
DagNodeupNoMatchPair ()
DagNodeupNoMatchSubst ()
DagNodeupNoParse (int badTokenIndex)
DagNodeupNoUnifierContext4Tuple ()
DagNodeupNoUnifierContextTriple ()
DagNodeupNoUnifierPair ()
DagNodeupNoUnifierTriple ()
DagNodeupOpDecls (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupQidList (const Vector< int > &ids)
DagNodeupResult4Tuple (DagNode *dagNode, const Substitution &substitution, const VariableInfo &variableInfo, DagNode *metaContext, MixfixModule *m)
DagNodeupResultPair (Term *term, MixfixModule *m)
DagNodeupResultPair (DagNode *dagNode, MixfixModule *m)
DagNodeupResultTriple (DagNode *dagNode, const Substitution &substitution, const VariableInfo &variableInfo, MixfixModule *m)
DagNodeupRls (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupSorts (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupSortSet (const Vector< Sort * > &sorts)
DagNodeupSubsortDecls (bool flat, ImportModule *m, PointerMap &qidMap)
DagNodeupSubstitution (const Substitution &substitution, const VariableInfo &variableInfo, MixfixModule *m, PointerMap &qidMap, PointerMap &dagNodeMap)
DagNodeupTrace (const RewriteSequenceSearch &state, MixfixModule *m)
DagNodeupType (Sort *sort, PointerMap &qidMap)
DagNodeupTypeListSet (const Vector< OpDeclaration > &opDecls, const NatSet &chosenDecls, PointerMap &qidMap)
DagNodeupUnificationContext4Tuple (const Substitution &substitution, const VariableInfo &variableInfo, DagNode *dagNode, DagNode *hole, const mpz_class &variableIndex, MixfixModule *m)
DagNodeupUnificationContextTriple (const Substitution &substitution, const VariableInfo &variableInfo, DagNode *dagNode, DagNode *hole, const mpz_class &variableIndex, MixfixModule *m)
DagNodeupUnificationPair (const Substitution &substitution, const VariableInfo &variableInfo, const mpz_class &variableIndex, MixfixModule *m)
DagNodeupUnificationTriple (const Substitution &substitution, const VariableInfo &variableInfo, const mpz_class &variableIndex, MixfixModule *m)
DagNodeupView (View *view, PointerMap &qidMap)

Private Types

enum  ComplexSymbolType { REGULAR_SYMBOL, POLYMORPH, BUBBLE }
enum  Flags { NONEXEC = 1, OWISE = 2, PRINT = 4 }
enum  Implementation { nrPreallocatedArgs = 3 }

Private Member Functions

void checkHook (DagNode *metaIdHook, SymbolType &symbolType)
void checkHookList (DagNode *metaHookList, SymbolType &symbolType)
bool downAssignment (DagNode *metaAssignment, MixfixModule *m, Vector< Symbol * > &variables, Vector< Term * > &values)
bool downAttr (DagNode *metaAttr, AttributeInfo &ai)
bool downAttrSet (DagNode *metaAttrSet, AttributeInfo &ai)
bool downBubbleSpec (DagNode *metaBubbleSpec, MetaModule *m, Symbol *topSymbol, int &bubbleSpecIndex)
bool downConditionFragment (DagNode *metaConditionFragment, MixfixModule *m, ConditionFragment *&fragment)
bool downEquation (DagNode *metaEquation, MixfixModule *m)
bool downEquations (DagNode *metaEquations, MixfixModule *m)
bool downFixUps (MetaModule *m)
bool downHeader (DagNode *metaHeader, int &id, DagNode *&metaParameterDeclList)
bool downHook (DagNode *metaHook, MetaModule *m, Symbol *symbol, const Vector< Sort * > &domainAndRange)
bool downHook (DagNode *metaHook, MetaModule *m, int index)
bool downImport (DagNode *metaImport, MetaModule *m)
bool downImports (DagNode *metaImports, MetaModule *m)
bool downInstantiationArguments (DagNode *metaArguments, Vector< int > &arguments)
bool downMembAx (DagNode *metaMembAx, MixfixModule *m)
bool downMembAxs (DagNode *metaMembAxs, MixfixModule *m)
bool downModuleExpression (DagNode *metaExpr, ImportModule *enclosingModule, ImportModule *&m)
bool downNatList (DagNode *metaNatList, Vector< int > &intList)
bool downOpDecl (DagNode *metaOpDecl, MetaModule *m)
bool downOpDecls (DagNode *metaOpDecls, MetaModule *m)
bool downOpHook (DagNode *metaOpHook, MetaModule *m, int &purpose, Symbol *&op)
bool downParameterDecl (DagNode *metaParameterDecl, ImportModule *m)
bool downParameterDeclList (DagNode *metaParameterDeclList, ImportModule *m)
bool downPolymorphTypeList (DagNode *metaTypeList, MixfixModule *m, const NatSet &polyArgs, Vector< Sort * > &typeList)
bool downPrintList (DagNode *metaPrintList, MixfixModule *m, StatementAttributeInfo &ai)
bool downPrintListItem (DagNode *metaPrintListItem, MixfixModule *m, StatementAttributeInfo &ai)
bool downPrintOption (DagNode *metaPrintOption, int &printFlags) const
bool downRenaming (DagNode *metaRenaming, Renaming *renaming)
bool downRenamingAttribute (DagNode *metaRenamingAttribute, Renaming *renaming)
bool downRenamingAttributes (DagNode *metaRenamingAttributes, Renaming *renaming)
bool downRenamings (DagNode *metaRenamings, Renaming *renaming)
bool downRenamingType (DagNode *metaType, Renaming *renaming)
bool downRenamingTypes (DagNode *metaTypes, Renaming *renaming)
bool downRule (DagNode *metaRule, MixfixModule *m)
bool downRules (DagNode *metaRules, MixfixModule *m)
bool downSimpleSortList (DagNode *metaSortList, MixfixModule *m, Vector< Sort * > &sortList)
bool downSort (DagNode *metaSort, MixfixModule *m)
bool downSorts (DagNode *metaSorts, MixfixModule *m)
bool downStatementAttr (DagNode *metaAttr, MixfixModule *m, StatementAttributeInfo &ai)
bool downStatementAttrSet (DagNode *metaAttrSet, MixfixModule *m, StatementAttributeInfo &ai)
bool downSubsort (DagNode *metaSubsort, MixfixModule *m)
bool downSubsorts (DagNode *metaSubsorts, MixfixModule *m)
bool downTermList (DagNode *metaTermList, MixfixModule *m, Vector< Term * > &termList)
bool downType2 (int id, MixfixModule *m, Sort *&type)
bool downVariable (DagNode *metaVariable, MixfixModule *m, Symbol *&vs)
bool fixUpBubble (DagNode *metaHookList, MetaModule *m, int polymorphIndex)
bool handleIdentity (DagNode *metaIdentity, MetaModule *m, int index, const Vector< Sort * > &domainAndRange)
bool handleIdentity (DagNode *metaIdentity, MetaModule *m, BinarySymbol *s)
bool handleSpecial (DagNode *metaHookList, MetaModule *m, Symbol *symbol, const Vector< Sort * > &domainAndRange)
bool handleSpecial (DagNode *metaHookList, MetaModule *m, int polymorphIndex)
 NO_COPYING (MetaLevel)
DagNodeupArguments (const Vector< Token > &arguments, PointerMap &qidMap)
DagNodeupAssignment (const Term *variable, DagNode *value, MixfixModule *m, PointerMap &qidMap, PointerMap &dagNodeMap)
DagNodeupAttributeSet (SymbolType st, Vector< DagNode * > &args)
DagNodeupCondition (const Vector< ConditionFragment * > &condition, MixfixModule *m, PointerMap &qidMap)
DagNodeupConditionFragment (const ConditionFragment *fragment, MixfixModule *m, PointerMap &qidMap)
DagNodeupConstant (int id, DagNode *d, PointerMap &qidMap)
DagNodeupConstant (int id, Sort *sort, PointerMap &qidMap)
DagNodeupEq (const Equation *equation, MixfixModule *m, PointerMap &qidMap)
DagNodeupFrozen (const NatSet &frozen)
DagNodeupGather (const Vector< int > &gather, PointerMap &qidMap)
DagNodeupHeader (bool flat, PreModule *pm, PointerMap &qidMap)
DagNodeupIdentity (MixfixModule *m, SymbolType st, Term *identity, PointerMap &qidMap)
DagNodeupIdHook (int purpose, const Vector< int > &items, PointerMap &qidMap)
DagNodeupJoin (int id, Sort *sort, char sep, PointerMap &qidMap)
DagNodeupLabel (const Label &label, PointerMap &qidMap)
DagNodeupMb (const SortConstraint *mb, MixfixModule *m, PointerMap &qidMap)
DagNodeupModuleExpression (const ModuleExpression *e, PointerMap &qidMap)
DagNodeupOpDecl (ImportModule *m, int symbolNr, int declNr, PointerMap &qidMap)
DagNodeupOpHook (int purpose, Symbol *op, PointerMap &qidMap)
DagNodeupOpMappings (View *view, PointerMap &qidMap)
DagNodeupParameterDecl (PreModule *pm, int index, PointerMap &qidMap)
DagNodeupParameterDecls (PreModule *pm, PointerMap &qidMap)
DagNodeupPolymorphDecl (ImportModule *m, int index, PointerMap &qidMap)
DagNodeupPolymorphSpecial (int index, MixfixModule *m, PointerMap &qidMap)
DagNodeupQid (int id, PointerMap &qidMap)
DagNodeupQidList (const Vector< int > &ids, PointerMap &qidMap)
DagNodeupRenaming (const Renaming *r, PointerMap &qidMap)
DagNodeupRenamingAttributeSet (const Renaming *r, int index, PointerMap &qidMap)
DagNodeupRl (const Rule *rule, MixfixModule *m, PointerMap &qidMap)
DagNodeupSortMappings (View *view, PointerMap &qidMap)
DagNodeupSortSet (const Vector< Sort * > &sorts, int begin, int nrSorts, PointerMap &qidMap)
DagNodeupSpecial (Symbol *symbol, const OpDeclaration &decl, MixfixModule *m, PointerMap &qidMap)
DagNodeupStatementAttributes (MixfixModule *m, MixfixModule::ItemType type, const PreEquation *pe, PointerMap &qidMap)
DagNodeupStrat (const Vector< int > &strategy)
DagNodeupTerm (const Term *term, MixfixModule *m, PointerMap &qidMap)
DagNodeupTermHook (int purpose, Term *term, MixfixModule *m, PointerMap &qidMap)
DagNodeupTraceStep (const RewriteSequenceSearch &state, int stateNr, MixfixModule *m, PointerMap &qidMap, PointerMap &dagNodeMap)
DagNodeupTypeList (const Vector< Sort * > &types, bool omitLast, PointerMap &qidMap)
DagNodeupTypeSorts (const set< int > &sorts, PointerMap &qidMap)
DagNodeupVariable (int id, Sort *sort, PointerMap &qidMap)

Static Private Member Functions

static void convertToTokens (const Vector< int > &ids, Vector< Token > &tokens)
static int iterToken (DagNode *dagNode)
static DagNodeupGroup (const Vector< DagNode * > &args, Symbol *emptyCase, Symbol *multipleCase)

Private Attributes

MetaModuleCache cache
CachedDag falseTerm
bool flagVariables
CachedDag trueTerm
int variableBase
FreshVariableGeneratorvariableGenerator

Detailed Description

Definition at line 31 of file metaLevel.hh.


The documentation for this class was generated from the following files:

Generated by  Doxygen 1.6.0   Back to index