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!

...

added TODO list

huge commit regarding the grafite_status:
- in the ng_status component it embeds the lexicon status
- the lexicon status is not passed around alone anymore
- coercions/hints for the ng system are no longer imperative
  (are in the e (for external) status of the tac_status
- ng_refiner does not take in input a look_for_coercions function
  but an aggregate type "rdb" comprising hints and coercions
  (and empty one is passed to disable hints/coercions)
functionalities losses:
- old (generated) hint are no longer translated on the fly
- old coercions are translated in a best effort way
  (no universes calculation)

part of last commit

tacticals are really tactics now, they have an AST at the same level of
tactics. Parser/engine fixed accordingly. This allowed a better TPTP
exportation

we removed some coercion detours and we added some coercions we really would like to see

Implemented keep_simplified.
If a candidate for forward inference is discarded, another is selected

ocaml sucks...

...

-ng implemented

Added a new keep_simplified function

Renamed forward_simplify into simplify and backward_simplify
into simplify_goal

Active goals are now demodulated after selecting a positive clause.
Implemented OrderedSet for passive clauses.
Selection is now based on weight (fairness condition to be added).

- applyTransformation: bugfix in the rendering of records

now algebra/monoids.ma is fully reconstructed :)

content2pres for the new cic fixed

- some depend files fixed
- matitacLib: we peform a garbage collection after compiling every file instead of just .mma (let's see the times)
- transcript: support for "cr" inline param completed
- procedural: now record are supported

the records of logic/cprop_coonectives.ma are now reconstructed :)

logic higher_order_defs list nat Z Q are now fully reconstructed :))

- library/list/list.ma: unused code commented
- proceduralClassify type argument are no longer critical: let's see how it goes
- acic2Procedural: the inline parameter Debug now works
- procedural2: we remove the conversions before first order relexivities (exp. to avoid conversion to []=[] in list/list.ma [does not work because []=[] in an open term since the equality type is unspecified]). so we we strengthen reflexivity (see below)
- setoids: now reflexivity is retried after whd if it fails in the first place.
- grafiteAst: detection of convertible rewrites is now optional and activated with the inline parameter "cr". nat/factorial2 is very slow without rewrites
transcript: we now avoid the generation of dupplicated inlines (mistakely generated by the grafite parser [this can not be avoided without a better syntax for .ma scripts])

now list/list.ma is fully reconstructed :)

nat/factorial2.ma takes long to be produced 22m31. Some conversion is slowing the process. nat/bertrand.ma also: we are waiting for it now :(

1) added simplification of actives w.r.t. selected
2) added simple main loop (look at the comment for a possible optimization)

right inference step completed

new function filter_map_acc

Extended the equality case to non ground terms

- Procedural: more support for the Debug inline option (does not work yet)
- transcript: now we can process a given subset so the source files
- termContentPres: bugfix in the syntax of letrec, a space was missing :(

now nat/generic_iter_p.ma is fully reconstructed :) (thx Claudio)

Debugging code removed.

Temporary (and partially broken) patch for Ferruccio: I duplicate
\Pi abstractions in let ... rec definitions in order to make the system
infer the same names. However, it could be infer a -> in place of a \forall.

almost complete superposition right step

snapshot

see the previous commit

termAcicContent is logic independent (despite its name) thus it
needs also term_of_nref

Optimized weigths comparison, removed normalization

snaphost: supright almost done

...

...

Implemented substitution application and concatenation

...

fixed metas

fixed building

...

a skeleton of supright

some more functors and a nice higher-order all_positions iterator

added META for ng_paramodulation

Previous commit reverted, as explained in that log.

This commit restores the ids_to_father_ids table.
However, after the implementation, I sort of realized that maybe this table
is useless, after all.
Thus I am gonna do my commit and immediately revert it (just to keep the
code in SVN in case of need).

some renaming to make ocamlopt happy

bugfix in Include syntax: it was changed and committed by mistake :(

- Procedural convertible rewrites in the conclusion are now detected and replaced by change
- grafiteAst: semantics of the Include flag changed: now true means normal include, New Inline flags Coercions, Comments (activated) Debug (not yet)
- library: eq_plus_Zplus moved from Z/times to Z/plus

now Z/plus.ma Z/times.ma are fully reconstructed :)

First tests for paramodulation (pretty printer, unification)

- replaced part1a/defn with the version based on induction/inversion and deleted
older version
- more minor improvements

Fix : wrong exception was catch in apply_subst

1) the home button of CicBrowser now works also for NG
2) implemented simple (i.e. no natural language) rendering of NG constants.
   Inductive types and (co)recursive definitions are still missing.

The kernel _must_ check the correctness of the height since the reduction
machine never tries to reduce terms whose height is 0. Thus, if the
declared height is 0, the height is no longer an optimization!

syntax error fixed :(

- doubleTypeInference: we check for unreferenced letins in the inferred type also after beta-reduction because beta-reduction can cause unreferenced letins
- procedural: bugfix in the use of inner types, the expected type was sometimes used in place of the inferred type; context cleaning is now disabled because the clear tactics are not generated; debugging mode is now activated

nat/ord.ma is now fully reconstructed :)

First pretty printing functions

minor changes here and there. We extend fo-unification with
(X ...) =?= (f ...) --> X := f

comments

better type for comparison and implementation of KBO orderings

more functors