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!
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.
1. profiling code added
2. debug_print made lazy to avoid computation of the argument when profiling
is disabled. This really speeds up disambiguation!
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)
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
projects / helm.git / log