lambda-delta:
- lib/output: infrastructrure for reduction reporting
  we found just one instance of "referene typing" in the "Grundlagen"
  rt.txt reports where it occurs
- lib/time: bugfix
- basic_rg: bugfix (some relocations were missing)
  the "Grundlagen" now typechecks :)

...

do not infer on closed goals

removed a maybe diverging test

...

First attempt for refined goal selection strategy

added (but not active) last chance idea

Implemented orphan murdering technique

new make test target

new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

attempt to run a last chance procedure after the timeout

the timeout is passed to test last chance

this case is not assert false since it can happen if occur_check
makes fail the unification

fixed parsing

convenient problem lists

an easy for loop

deep subsumption activated

test for deep subsumption added

Implemented orphan murder test (clauses are not discarded for now)
Re-enabled zero weight trick

...

better doc

timeouts are passed as arguments, so that tptpprover can
accept --timeout argument. Moreover it prints the proof
according to the SZS ontology

- some depend files :)

the prover is almost OK, types in fuctors a bit extended to
ease their instantiation

First version of deep_subsumption.

Various fixes

new function

...

matitaprover is almost there

...

initial import of standalone matitaprover binary

Now using age selection

code refactoring for paramodulation

new function list_mapi_acc

Fixed is_identity for facts

Fixed insertion of passive clauses

Code factorization

Removed debug printing

Now inserting hypothesis and goal with zero weight

Extended is_identity test
First step towards age selection

Implemented check for duplicates (in goals)

Removed old debugging assertion

- procedural: basic support for lapply (solves a problem in the reconstruction of algebra/groups.ma)
- lambda-delta: bugfix in line counts and nodes counts

Removed debug printing raising Failure

Removed debug printing

Rewrote the main loop for paramodulation

undo/serialization for universes implemented

Debugging prerr_endlines removed.

1) NCicTypechecker.typecheck_obj removed, since it did not add to the
   environment (and thus all objects were type-checked at least twice)
2) NCicEnvironment.check_and_add_obj that checks and add an object
3) added NCicEnvironment.invalidate_obj that invalidate all objects after a
   given one (that comprised)
4) NCicLibrary.add_obj now calls the NCicEnvironment.check_and_add_obj;
   NCicLibrary.time_travel now calls NCicEnvironment.invalidate_obj

Note: it could happen that an object is in the environment but not in the
      library and thus it could not be invalidated by time_travel.
      In practice, this is safe anyway and it will never happen.

Fixed nasty bug in maxvar updating

- Bug fixed: removed URIs were not removed from the dependencies DB.
- The assert failure has been removed since in some situations (????) an
  empty dir (no new objects) was not created and thus it was normal that it
  was not removed. TO BE BETTER UNDERSTOOD

removed problem not in UEQ

- nodes count is now working for aut and meta
- bugfix in autLexer
- comment fix in aut

Added more precise time information

Added problems from CASC 208

Regenerated problems with corrected tptp2grafite

Corrected proof visiting (topological sort)

Small debugging in tptp2grafite

Added injective compose

- cicNotationPp: bugfix in record syntax
- lambda-delta: version update

Some notation and additional lemmata.

Debugging

"matitaclean all" ported to NG

Invert dependencies between baseuris (files) are now stored in the db.
Hence decompilation is now fully correct (???).

Bug fixed: refreshing of uris for the db.

More improvements.

The global db is now updated during decompilation.

Persistent db (to lookup names in the library) inefficiently implemented as
an associative list which is:

 1) loaded from disk and stored in memory when matita starts
 2) updated every time a file is saved

Still to be implemented: decompilation.

NG decompilation is now activated. However, it is called from the old
decompilation that cannot detect when a NG-only file A is used by another
NG-only file B. As a consequence, decompiling A does not decompile B too.

Estatus finally merged into the global status using inheritance.
Major code simplification everywhere :-)

Useless GrafiteTypes.get_baseuri removed.

More statuses converted to objects.

Good:
1) all set_* methods are now polymorphic
2) no more :> coercions
3) no more technical class types

Bad:
1) some polymorphic set_* methods have explicit row types that are
   problematic when extending another class in another file. The
   row types should just be #classname, but ocaml rejects them that
   way.

debug pps removed

better exception handling

proof patching!

Objects are now used to represent also the tactic status.
Cool (but error messages can be bad).

Added ntry and nassumption tactics

callbacks were taking in input a status bu were not using them.
thanks to the new #type for statuses this was a problem, and Obj.magic
was required to fix them. Removed both the dummy parameter and the
unsafe cast

Fixed stupid path

Added script useful for running benchmarks

Changed parenthesis to optional around letin ident (and type)

Fixed wrong types in proof terms

Stricter type: the type now shows that disambiguation only alter the lexicon.
In this way we are forced to manually set the content of the object in place of
setting the whole object, that leads to information loss since in the meanwhile
new commands may have altered the rest of the state.

1) grafiteWalker removed
2) ncommands and commands are now two distinct syntactic entries
3) NEstatus.status and LexiconEngine.status are now objects

proof reconstruction almost OK

Initial implementation of statuses using objects in place of nested records.
So nicer!

The only major problem is that the NCicLibrary functor does not return a
function #status as 'status -> 'status, but a function status -> status.
Thus I have to painfully wrap NCicLibrary.Realizer(...).require in NRstatus.

TO REMEMBER:
- every function that works on a data type that used to be put in the status
  (e.g. a db) must now work on a functional class with just two members
  (db and set_db). Moreover, every function in the module must work on the
  open variants of the class type, i.e. #status

Added optionnal one pass simplification (instead of keep_simplified)
Fix for varlists (we traverse the term to collect occuring variables)

first proof reconstruction attempt, still bugged since it
does all steps in a forward fashion

1) unification hint now takes NG terms (as it should have been from the very
   beginning)
2) refresh_uris_in_term is now passed to the constructor of the
   existential/universal data type in NCicLibrary
3) URIs are now refreshed in unification hint data

1) NCicLibrary (which is untrusted) moved after NCicUntrusted.
   NCicLibrary registers get_obj to NCicEnvironemnt (and to NCicPp)
2) URIs are now refreshed when objects are included from disk

Observation: even NCicPp is untrusted. Thus its implementation should be put
at the end and some references set to one early module. Which one? Two
choices: NCic or NCicPp (two modules, one with the implementation follows).
Could the same be done for NCicLibrary too in order to bring back the explicit
dependency of NCicEnvironment over NCicLibrary? [ In that case, remember to
change back the exception caught by GrafiteDisambiguate ]

Implementation of existential type improved (more strict checking).

avoid fixing non-recursive terms

we fix recursive object reference with the correct height
just before adding it to the library

FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

Instead of serializing closures (of type status -> status), we now
serialize data. This is achieved by implementing an existential type

       NCicLibrary.Serializer(struct type status end).obj

whose semantics is "\exists 'a. 'a -> status -> status"
and by putting in the dump a list of these existential types.

The current implementation is the type-unsafe one based internally on Obj.magic.
However, the interface is (should be?) type-safe.
Other type-safe implementations could be derived by the ocaml m.l. thread on
existential types. In particular, I remember implementations via:
  - references
  - functors
  - exceptions
  - impredicative encoding via polymorphic methods

This fix allow to change the Matita code without invalidating the library.

(Critical) things still to be done:
 - decompilation
 - refreshment of URIs

we corrected some reduction bugs about renaming.

The grundlagen is now fully typechecked :)

we removed some old code and fixed a reduction bug: two instances fo the
same constant applied to a different number of arguments may be convertible

We now check grundlagen up to item 109 :) (with naive sort inclusion :( puah)

EXPERIMENTAL COMMIT (part B, by CSC :-):
 - objects are now individually serialized too
   (but never decompiled)

CRITICAL OBSERVATION:
 - closures in ocaml are pointers in the binary, hence the library
   must be decompiled at every single change in matita's code

EXPERIMENTAL COMMIT (by CSC,actuall :-)
This commit partially implements (in NCicLibrary) serialization for NG.
It creates several .matita/matita/.../foo.ng files that are ocaml dumps
of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied
to the current status.

The test tests/ng_includeB.ma shows how unification hints are preserved.

TODO:
 a) decompilation is implemented in NCicLibrary, but not called anywhere
 b) serialization of objects (and "query" db (and old to new cache??)) not
    implemented yet
 c) objects are removed from the library, but not from the environment!

...