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)
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 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
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.
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.
- changed command line interface of cicbrowser so that everything which could be written in the "URL" bar can be provided on the cmdline as well (even without double-quoting)
- ported to new ppmetasenv (swapped arguments)
bugfixes:
1) ask for saving/mooing only when the user has choosen a file to load
2) opening a file doesn't call goto_top (removing all xml, even if the moo has
been generated). This fix should enforce the invariant that a moo exists only
if the corrsponding xml objects do.
3) the switch_page callback is inhibited before removing pages in
sequentViewers#reset
Bug fixed: when several instances are tried during disambiguation, do not add
aliases unless they are absolutely necessary. Even in this case they should
be one-shot aliases (not implemented yet).
- changed moo representation in MatitaTypes.status, no longer a string list, but a command (in AST format) list
- fixed redundancy in moo: aliases, interpretation, and default commands are always present only once in a single moo
- added MatitaTypes.add_moo_content: from now on it must be then only function used to add content to moo objects
Two bugs fixed in the apply tactic:
1. an application of a term of type t where t reduces to a product does not
fail any longer: t is unfolded as required to produce enough products.
E.g. apply (t: ~A) when the goal is False
2. the apply tactic does not fail any longer when the goal is a product.
When the head of the type of the term is flexible, the type is a product
and the goal is a product (e.g. t: A -> ? vs A' -> B) the less instantiated
term (i.e. t) is tried first; in case of failure (e.g. A not unifiable with
A') t is instantiated adding one metavariable after another.
Added support for multiple disambiguation passes.
Actually, passes can differ in:
- whether they use library as fallback for unbound domain items or not
- whether they use multi-aliases or not
- whether they use coercions or not.
The current policy is to postpone the use of coercions as much as possible and to fallback to library only as a last resort.
Passes can be configured from matitaDisambiguator.ml.
Filled pre-generated notation levels with productions on dummy tokens (never generated by the lexer). This hack works around a bug in camlp4 which on delete_rule remove an entire precedence level if it gets empty after the delete_rule invocation.
projects / helm.git / log