New style debugging/profiling for NCicMetaSubst.

Sometimes it is useful to be able to print the subst without applying it.

auto snapshot

- dual_rg: renamed to complete_rg [as suggested in the ToCL documentation]
- Makefile: "lddl" entry generates lddl.tar.bz2

refactoring ...

new xml exportation procedure for basic_rg (10 times faster than previous). the static html pages were changed accordingly. Old exportation procedure removed

Better error message.

For some obscure reason, more universes are now needed (but not used in
scripts). To be better understood.

instantiate/sortfy/kindfy etc. reimplemented with less and more correct code

New function.

Let's use already existent functions.

- lambda-delta: some fixes: now the grundlagen type-checkes through dual_rg
- matita/Makefile: we removed LAMBDA-TYPES from the nightly tests (too slow ???)

Works again

Ad-hoc management of ? vs out_scope in instantiate. The library passes again,
but there seems to be still more work to do in instantiate.

Bug fixed: the `IsTerm attribute is now added by mk_meta and it was not
preserved. The current code should be more stable.

1) new-style debugging/profiling code for old reduction
2) aliases are now dumped to stderr

Commented out code to optimize the case t1 vs t2 when t1 and t2 are both
meta closed. Why is it necessary, anyway?

One-shot aliases were no longer generated because of a bug (i.e. all aliases
retrieved from the universe used to have instance=0). Fixed by parameterizing
once again all the functions with a ~fix_instance function to fix the instance.

Different aliases, better equality inferred.

instances

instance fixed

better indentation

better indentation

better comments and indentation

use prop_only to filter instead of repeting the same function body

better logging

better logging and immediate pruning of new goals when
- length(goals) > maxwidth
- depth = maxdepth and goals <> []

auto navigates a real tree, not a flattened one

labels in group_by_tac

new data structures for auto

do not put " around node name, otherwise names like foo:f1 are not
accepted

export group_by_tac

drg->brg translation contibued (still bugged though)

qed => nqed.

Now the time required to eval a command is printed.

added code to print the tree

CSC proof made by paramod

more functions

Alias required now ??

new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_assembly/compiler/environment.ma

the trie indexes terms up to 10 nested applications and skips applications with more then 50 arguments

more auto

Non general recursion implemented via recursion over unary (?) inductive
generated formal topologies.

first bits for the zipper

...

...

more printings

auto is smarter :-)

nauto:
- fixed indexing (now always dome in the same way)
- depth=x means: tray at depth=2 ... try at depth=x
- run auto on set of goals that are linked by occurring in each others types,
  simply distribute if there is no dependency

...

fixed pictures

preserve sharing if map_term_fold_a

add XXX where I found a catch all statement

new sharing-preserving map with accumulator

apply the subst to the metasenv and to p

- Bug fixed: some assert failure were just failures (when processing terms
  that do not satisfy the IRS condition).
- New test ng_bove.ma added to test the Bove-Capretta method (in CProp)

...

Smarter implementation of instantiate to avoid re-checking twice the same term.

...

batch pdf generation

...

some more work

...

...

debug idem for auto added

new lambda instros and better logging

better indexing for auto

some work for auto

some work for auto

removed optimization potentially unsound

...

Profiling code integrated.

 freescale porting, work in progress

Debugging improved.

Benchmarking integrated in folding/unfolding.

 freescale porting, work in progress

cantor...

...

hints were not used by reduction machines on heads

...

ncheck is not erased

...

...

...

...

minor fix

tons of typo fixed

Error message fixed (dereferencing must be done eagerly, not when the error is
actually printed!)

Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!

CProp uri fixed

...

...

...

...

...

...

Experimental scripts for nth-order rewriting principles.

relocate is hopefully fixed once and for-all!

better screenshot

 freescale porting, work in progress