metaSearch

The operation metaSearch takes as arguments the metarepresentation of a module, the metarepresentation of the starting term for search, the metarepresentation of the pattern to search for, the metarepresentation of a condition to be satisfied, the metarepresentation of the kind of search to carry on, a Bound value, and a natural number.

  op metaSearch : 
       Module Term Term Condition Qid Bound Nat ~> ResultTriple?
       [special (...)] .

The searching strategy used by metaSearch coincides with that of the object-level search command in Maude (see Sections 5.4 and 16.4). The Qid values that are allowed as arguments are: '* for a search involving zero or more rewrites (corresponding to =>* in the search command), '+ for a search consisting in one or more rewrites (=>+), and '! for a search that only matches canonical forms (=>!). The Bound argument indicates the maximum depth of the search, and the Nat argument is the solution number. To indicate a search consisting in exactly one rewrite, we set the maximum depth of the search to $1$.

Using metaSearch we can redo at the metalevel the last example in Section 5.4. The results give us the answer to the question: if I have already inserted one dollar and three quarters in the vending machine, can I get two cakes and an apple? The answer is yes; in fact, there are several ways.

  Maude> reduce in META-LEVEL :
           metaSearch(upModule('VENDING-MACHINE, false),
             '__['$.Coin, 'q.Coin, 'q.Coin,'q.Coin],
             '__['c.Item, 'a.Item, 'c.Item, 'M:Marking],
             nil, '+, unbounded, 0) .
  result ResultTriple:
    {'__['q.Coin,'q.Coin,'q.Coin,'q.Coin,'a.Item,'c.Item,'c.Item],
     'Marking,
     'M:Marking <- '__['q.Coin, 'q.Coin, 'q.Coin, 'q.Coin]}

  Maude> reduce in META-LEVEL :
           metaSearch(upModule('VENDING-MACHINE, false),
             '__['$.Coin, 'q.Coin, 'q.Coin, 'q.Coin],
             '__['c.Item, 'a.Item, 'c.Item, 'M:Marking],
             nil, '+, unbounded, 1) .
  result ResultTriple:
    {'__['a.Item, 'c.Item, 'c.Item], 
     'Marking, 
     'M:Marking <- 'null.Marking}