As with modules, all commands at the Full Maude level should be entered enclosed in parentheses. In this way the system can distinguish between commands at the Core Maude level--that in this context are "system programming" commands in the module FULL-MAUDE--and commands to be handled by Full Maude.
The reduce and rewrite commands have the same effect in Full Maude specifications as their homonymous commands in Core Maude.
The syntax for the reduce commands is given by the following declarations. Notice that, as in Core Maude, red is used as an abbreviation for reduce. However, the command to reduce a term in a given module has a somewhat different syntax than the one used in Core Maude32.
op red_. : Bubble -> PreCommand .
op red-in_:_. : ModExp Bubble -> PreCommand .
Similarly, the following are the declarations defining the syntax of the rewrite commands.
op rew_. : Bubble -> PreCommand .
op rew[_]_. : Token Bubble -> PreCommand .
op rew-in_:_. : ModExp Bubble -> PreCommand .
op rew-in[_]_:_. : Token ModExp Bubble -> PreCommand .
Full Maude maintains a database with all the modules that have been introduced since the begining of the session. Notice that a Full Maude session does not start automatically when we start the system. The Maude specification of Full Maude has to be loaded first, and the loop has to be initialized. Apart from the built-in modules, Core Maude and Full Maude keep independent module stores.
As in Core Maude, when a module is not explicitly specified the system uses a module by default, that in general is the last module introduced, although one can select another module from the database with the select command.
op select_. : ModExp -> PreCommand .
There are also several show commands as in Core Maude. There are commands to show a module or theory33 as introduced by the user, to show the flattened version of any module in the database, and to show some of the components in a module in the same way as the commands for Core Maude, as explained in Section A. For any of these commands the name of a module can be given. If no name is specified, the default current module is used. The syntax of these commands is as follows.
op show module . : -> PreCommand .
op show module_. : ModExp -> PreCommand .
op show all . : -> PreCommand .
op show all_. : ModExp -> PreCommand .
op show sorts . : -> PreCommand .
op show sorts_. : ModExp -> PreCommand .
op show ops . : -> PreCommand .
op show ops_. : ModExp -> PreCommand .
op show vars . : -> PreCommand .
op show vars_. : ModExp -> PreCommand .
op show mbs . : -> PreCommand .
op show mbs_. : ModExp -> PreCommand .
op show eqns . : -> PreCommand .
op show eqns_. : ModExp -> PreCommand .
op show rls . : -> PreCommand .
op show rls_. : ModExp -> PreCommand .
The show view_ command prints the view34 with the specified name.
op show view_. : ViewExp -> PreCommand .
The show modules and show views commands print, respectively, the list of the names of all modules, and the list of the names of all views, present in the database.
op show modules . : -> PreCommand .
op show views . : -> PreCommand .