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