mark local state variables (#710)

* counter for Meson inferences is local state

* meson vardb is local state

* meson cdb is local state

* slice and units are local data of a mlibSolver.solver

* contrapos_cache is a local variable

* mark caches in mlibModel.model as local (to METIS_TAC)

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

avoid confusion: depth is global and memory is local

Uref.uref -> Uref.new

introduce Uref for both polyml and mosml

more systematic use of "open Unsynchronized"

make heavily allocated variables explicit as local program variables

Fix mesonLib to make more references local

Also remove unused bump_hol_thm

mesonLib: delete unused fol_of_form function

Make meson's contrapos_cache local to each invocation

This stops problems if order of evaluation is different from
expected (or if things are happening concurrently). There are a
number of refs being used by meson, so further commits will be
necessary here.

(Work towards #575.)

Remove eqtype declaration for term type

By eta-expanding, make ASM_MESON_TAC pay attention to changes in the
reference variable max_depth.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

ListPair.all isn't false if the lists are of different lengths. Sheesh.
I think the new version of the Basis library has such a function, but
I'll need to roll my own for the moment.

The cstore or "constant store" variable can contain abstractions as well
as constants and variables. It's therefore inappropriate to be using
term equality on it.

More term comparisons with equality; naughty.

Changed the semantics back to the way they were.

Make the "no useful instantiations" message only happen if the session
is interactive.

Sacrilege!

+ I abolished the Meson: ... spots!
+ Ditto for <<inventing new type names>> and <<overloading>> messages
+ save_thm now prints the name of the theorem it is saving.

Actually, all of the above only happens when Globals.interactive is
false, i.e., when Holmaking/building the system.

Hope you like the new look!

Fix for MJCG's performance bug. The problem was in Canon_Port.PRENEX_CONV,
when dealing with deeply nested quantifiers.

Minor inconsequential cosmetic changes made in the course of tracking
down various bugs.

The interface to the various trace functions has changed slightly.

Minor dull changes.

Kananaskis compatibility changes.

Added simple fix to ASM_MESON_TAC so that it actually tracks the
value of mesonLib.max_depth. Before the fix, changes to max_depth
were not visible to ASM_MESON_TAC (and therefore MESON_TAC).

Register the chatting variable with the global register of trace variables.

Fixes in order to remove library file dependencies on global grammars.

Added a max_depth variable initialised to 30 to stand in for what had been
an unconfigurable value in the definitions of ASM_MESON_TAC (and hence
MESON_TAC). This reference value is now tweakable from the outside
world.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision