More profiling code.

CicUtil.profile ==> HExtlib.profile

CicUtil.profile ==> HExtlib.profile

...

bugfix: evaluation of object commands is now atomic wrt status (including CicEnvironment, metadata, and the heck ...), either it succeed returning a new status or raises an exception leaving the status unchanged

"verbose" argument of remove is now optional (default false)

Less feedback during removal of objects.

...

Too many OPTIMIZE TABLES (because of a very stupid bug).

save_object_to_disk profiler fixed

Profiling code removed.

several "INSERT VALUE" ==> "INSERT VALUES" (more efficient)

Profiling code removed.

avoid generating useless parens in mathml contextes that do not require them (e.g. exponent, fractions, ...)

removed a line of dead code

Dead code removed again!!!

avoid pattern matching on attributed terms since this loses attributes

fix

universes are saved to disk

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.

added universes list handling

added universes

added parsing of Type:N

a wrong exception was raised

bugfix for uminus notation, prints parens where needed

added support for universes uri ".univ"

The disambiguation now returns the aliases diff. It used to return the
new aliases and a slow diff operation was performed later on.

log.ma renamed into ord.ma

The new_aliases argument of the functions alias_diff and set_proof_aliases
used to be a whole environment. It is now just the diff! Much more efficient!

A few changes to factorization and gcd.

Environment replaced by lists of domain and codomain items.

More notation here and there.

More notation here and there: \sup, \divides, \ndivides, !

* Added divides and ndivides
* Removed sub and sup

'!' is no longer a decorator (to allow a reasonable notation for factorial).

More notation here and there.

Profiling messages grepped out.

...

Dead code removed

More profiling code.

This commit removes the slowest identity function ever implemented!

We do not longer generate inner-types and inner-sorts for XML files generated
by matitac. We will have to implement a -export flag to matitac to generate
them. This represents yet another important speed-up.

We do not longer generate inner-types and inner-sorts for XML files generated
by matitac. We will have to implement a -export flag to matitac to generate
them. This represents yet another important speed-up.

ported to the new parser interface (Ulexing.lexbuf instead of char Stream.t)

uses ligatures (as a sample)

added ligatures support

rebuilt

clean_and_fill optimization

...

bugfix on proof construction

All the debug_print are now lazy.

More debug_print made lazy.

1. profiling code added
2. debug_print made lazy to avoid computation of the argument when profiling
   is disabled. This really speeds up disambiguation!

Profiling did not profile functions that raise an exception!
Fixed.

...

More profiling code added.

More profiling code inserted.

added non-builtin notation for exists
actually, the parsing rules is built-in, while the pretty priting one is not

changed ast representation of exists

pretty printing of literals is now subject to the debug setting

changed ast representation of exists, now an 'exists simble with a lambda child is used

bugfix in default magic handling: consider as having option type only names
which appear in the some branch and in the none one (previously all names
appearing in the some branch where considered optional)

- bugfix: eta abstractions ignores attributed node while counting lambdas
- permit pattern matching on attributed asts (since attributes are transparent to pattern matching)
- wrapped with assert false some unsafe function invocations (e.g. List.map2)
- removed reset_href (no longer needed)

more refere to bindings in env type definition

fixed matitadep: now it should consider ALL depndencies

added a minimal parser to extract informations relevant to dependencies calculation

...

all initialization code is now in the new matitaInit.ml module.

matitadep now parses notation.

development windows now avoids doing an anction selecting no developments

* Obsolete debugging comments removed
* Debugging comments by Andrea marked with "Andrea:"

Notation for "ex" introduced. It is the same as the notation for forall,
but it uses \exists.

NOTE: there is a bug now in cic_notation. The notation for ex is parsed, but
it is not pretty-printed correctly!

...

More profiling code.

Great speed-up in alias_diff (about 3x).
NOTE: alias_diff is still quite slow (e.g. 2.4s in the processing of
factorization.ma). This function really deserves to be got rid of.
(Moreover, this is possible and not that difficult)

A bit of profiling functions added here and there.

Spurious interpretation removed.

Profiling disabled.

...

This commit (partially) removes a big source of inefficiency (at least for
the select function and the rewrite tactic): CicUnification.UnificationFailure
exceptions were enriched producing (in a very expensive way) a nice error
message. However, the expensive error message is useful only when it must be
shown to the user. Very often this is not the case. Thus I am now postponing
the production of the error message, changing the type of the exception.
NOTE: this kind of improvement can be applied everywhere in the code!
At least it should be applied to functions that can normally fail (e.g.
unification, refinement, convertibility, type checking, etc.)

added list.ma

- avoid catching top level exceptions when the relevant setting in the registry is set
- removed some ancient debugging prints

splitted command line arguments among debugging and non-debugging so that when BuildTimeConf.debug is false the -debug flag is not available

- added support for -debug, which avoid catching top level exceptions (still useless until we find a way to let the program die on uncaught exceptions raised by gtk callbacks)
- enable whelp syntax on command line
- uses Arg for command line parsing

- bugfix: when backtracking restore the appropriate matched terms instead of keeping the current ones
- changed column order while matching constructors, this should speed up the matching since often application head discriminate if a row can be applied or not

Removed final question marks from {apply|elim|rewrite}s.
(This used to change the goals order, but it has now been fixed by Gares)

Some code that used to avoid a fixed bug removed.

...

.ma inclusions corrected/minimized

Profiling code commented out.

CicUtil.profile made even more polymorphic.

added a function to reorder the metasenv.

...

...

added notation for: nleq, ngeq, nless, and ngtr

added notation for nleq, nlgt, ...

added entites/overrides for leq, geq, nleq, ngeq, to

re-generated

uses Hashtbl.replace instead of Hashtbl.add so that:
1) extra-entities.xml could be used to override undesired bindings
2) only used mapping are kept in memory at run-time

Yet another implementation of the single aliases / multi aliases idea.
The new implementation is much simpler: single aliases are used everywhere
in the disambiguation phase; however, when a term needs to be looked for in
the library, it can be looked in a user-provided multi aliases environment instead.

NOTE: the new implementation fixes a bug of the previous implementation: the
most recent alias in the multi-alias set was printed last in the .moo files,
changing the performances of the system.