First implementation of unification on foterms

First functions on substitutions for unification

added a snapshot of comparison

This works for me

we rewrite the paramodulation code!

POPLmark part 1a using the de Bruijn encoding.

- cicNotationParser: added extra space to TeX control sequences accordind to previous commit of cicNotationLexer
- core_notation: bugfix in the notation for exp
- library/nat/congruence.ma: notation for "congruent" moved to core_notation

now nat/exp.ma is fully reconstructed :)

Procedural: higher-order unification needs a lot of hints !!

files fully reconstructed today:
nat/lt_arith.ma nat/div_and_mod.ma Z/plus.ma Z/orders.ma

- cicInspect: relevant nodes count updated: letin nodes are not relevant
- Procedural: reflexivity is now supported
- grafiteAst: boolean flag for include to tag inclusion of a source file. This command is relevant for .ma generation only. [ the source file of a .mma is not included in the generated .ma ]
- cicNotationLexer: unexpanded TeX macro symbols are now encoded with an extra space at the end. This is consistent with the concept of TeX sequence and fixes a bug in the renering of these symbols. The space is needed for reparsing!

Procedural: bugfix in the generation of intros for letin: the bodies and types of the actual letin and of the inferred letin must be equal upto alpha

now nat/minus.ma and nat/minimization.ma are fully reconstructed :)

- Procedural: we specify more unifiers for apply to help higher-order unification
- cicNotationPp: bugfix in the notation for Meta and ImplicitPattern
- transcript: grafite lexer/parser updated

Basic support for interpretations for NG:
 1) only interpretations for old objects are used
    (i.e. no way yet to declare a new interpretation on a new object)
 2) only interpretations for constants (no inductive definitions/constructors)
    since we have no faithful embedding of new references into old URIs
 3) no support for backtracking (I think)

Avoiding to filter the application of congruence equations
due to a couple of cases in "didactics" where auto is used
instead of reflexivity.

...

...

removed a call to autobatch.

nasty change in the lexer/parser:
- identifiers can begin with _
- interpretations use ? for implicits instead of _

possible problems:
- _foo is not anymore: SYMBOL(_) IDENT(foo)
  put a space to obtain the old token stream

bugfix in the output notation for eq

Pruning candidates in the applicative case for equalities.

Procedural: we use the expected type rather than the inferred type when we perform a cut to keep the goal in sync with the expected type.
we try to beta-reduce the elimination pattern when it does not match the goal/expected type

now nat/compare.ma and Z/z.ma are fully reconstructed :)

- cicUtil: is_sober now detects non-positive rels.
- PropceduralOptimizer: bug fix in critical step detection

now decidable_kit/streicher.ma is fully reconstructed :)

autobatch -> autobatch by

we catch the refiner errors in the critical step and fall back to the non-criticall version (this is just for debugging)
bug-fix in elimination recognition euristics

now nat/orders.ma and nat/times.ma are fully reconstructed :)

Removed a silly type check

...

NotEq is now considered as a negative Eq atom

regenerated

fixed generation of horn clauses, negated atoms are hypotheses

some horn+equality problems

removed byte queries

removed useless function

in the new kernel you can type Type[i] to mean Type_i, and Type is interpreted as
Type[0]. The same holds for CProp.

tests/ng_pts.ma defines some sorts, you may want to include it

nothing special

1) GrafiteAst.NEval => GrafiteAst.NReduce
2) new tactic "nnormalize" implemented
3) "ngeneralize" now uses "wanted" when no term is selected
   (so that it is possible to use ngeneralize to move an
   hypothesis down)
4) new syntax for non punctuational tinycals was missing

1) new tactic normalize (low-level function implemented in
   nCicTacReduction)
2) the select tactic used to generate fresh metavariables by unifying the
   "wanted" part of the pattern in a root where "wanted" did not occur.
   Those metavariables are now removed in that case

1) order of processing of case branches reverted (to generate metas in
   left-to-right order)
2) metas generated by eat_prods are now re-ordered so that they occur
   in left-to-right order

maxmeta implemented

maxmeta function to return the heighest meta used so far

alpha_eq exported

alpha_eq defined and exported

efficiency improvement (buffers are now used everywhere)

...

byte tests disabled

added patch to not unify any term containing the in_scope tag with
an entry in the local context

Patch to add a debugging string to HExtlib.split_nth reverted
(we cannot add a string to every function that raises an exception).

To know where the problem is, it is sufficient to look at the backtrace.
However:
 1) it works for matitac -debug
 2) ocaml is so dumb that it says "compile with -g" when it cannot find
    the executable in the current working directory. Since Matita chdir
    to the directory where the .ma file is, you need to put a copy of
    matitac (or make a symbolic link) where the .ma file is.

Cosmetic.

- hExtlib: added debugging information for split_nth

nat/plus.ma reconstructed :)

- libraryObjects: new default "natural numbers" with the uri of nat.
alias num "natural number" uses this one instead of the hardcoded uri (removed)
also destroy_nat (moved to termAcicContent) looks at this default

interpretations placed right after the corresponding definitions (in this way the script is reconstructed correctly)

logic/equality and datatypes/bool reconstructed :)

- matitaEngine: some commands like "coercion" must not be executed when mma's are dumped. This hack will be removed when mma's will be executed while dumped
- primitiveTactics: bugxix in the generation of the predicate for elim: we leave to the refiner the task of instantiating the types of the pattern variables.
Note: the head beta-reductions after the elimination must be performed following the instantiated predicate because (\lambda x:?.t v) does not beta-reduce (bug or feature?)

The singature of the "by" universe is added to the goal signature
(so univ is never filtered)

Via un'altra linea...

Sempre piu' breve

Signature is computed on the initial goal, once and for all.
Ripristined the filtering on candidates also for non-smart applications
(was too slow on some examples, e.g. in Fsub *

Do we really want to generate eliminators for nested data types? :-)

All weakly positive types but imbricated ones are now accepted
(e.g. ordinals).

- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal starts with an abbreviation. Clearbody before change in reactivated (to change the inferred type of the abbreviations of sort Prop)
- RELATIONAL: notation fixup
- character: autobatch fixup
- ng_tactics: dependences were not committed correctly

We only filter the smart candidates w.r.t the signature

Some experiments in generation of elimination principles.

ppsubst commented out in ppobj

Bug fixed: the relevance list can be shorted then leftno args.

Missing spaces inserted here and there.

- non_punctuational_tacticals ported to NG
- experimental generation of elimination principles passing through ASTs

Buffers are now used everywhere for speed-up.
However, the ppsubst is deadly slow even for not-that-large substitutions.

New function list_iter_sep.

A few lemmas about inclusion.

More automation

- critical bug fixed in NCicSubstitution.lift:
  (0,Irl 0) was lifted to (1,Irl 0)
  but later on NCicTypechecker.check_metasenv_consistency assumes the
  invariant that the currenct context has length (m+n) if the metavariable
  is (m,Irl n). But this invariant is false in the case (m, Irl 0) when m > 0.
- in NCicRefiner there was one line to normalize (m,Irl 0) and (m,Ctx []) to
  (0,...). Is it still required after the first patch to the kernel? I suspect
  no, thus I put an assert false to check.

Stupid typing error fixed.

...

...

Bug fixed: left parameters of constructors were unified before refining them.
Fixed, but the new code typechecks the constructors twice (in order to
re-compute) the sort without the inductive types. Is a more efficient
implementation worth the effort?

Bug fixed: refinement of mutual recursive definitions used to invert the
definitions.

Improved tests (for left parameters and mutual recursive definitions).

Bug fixed in refinement of inductive types: left parameters were forgot
during reconstruction of refined object.

1) better implementation of NObj that now calls recursively NQed
   to avoid code duplication
2) NQed now calls the kernel to check the object, since add_obj is too
   low level for that (this makes a huge difference with the previous
   architecture, but will probably break when dealing with undo)

The relevance list can be shorter than leftno (when the default is used).

Bug fixed in interpretation of records (the type was unbound in the fields).

Constructors are closed with thier types when computing the signatur

versione automatizzata

symmetry of inequality sym_neq

documentation for the inline command

- dependenciesParser: updated to new inline syntax

LAMBDA-TYPES: mma's recommitted because inline syntax changed

- cicUtil: is_sober now detects folded applications
- Procedural: bugfix in pattern generation for elim/rewrite, better debug output, applications are flattened before alpha-conversion to hide a bug of the double type inference :( (it generates folded applications)
- applyTransformation: coercions are shown when rendering a tactic because Procedural is not aware of coercions :(

apply and auto.equational_case call saturation.solve_narrowing
that performs goal inference and demodulation

updated comment

- Procedural: new flag "level=n" to control the reconstruction level (defaults to maximum level available). Level 1 reconstruction activated.

- hExtlib: new function "list_assoc_all"
- procedural: new flag "nodefaults" to turn off "default" based tactics. The `Variant flavour is now activated
- grafiteAst: now inline accepts a list of flags that can be easily extended
current flags are: procedural, nodefaults, depth=n, prefix="string" (untested),
theorem, definition, etc.
- transcript: support for explicitly provided inline flags

- pretty printer made robust in face of list_nth
- bugfixed in generation of aliases in nCicLibrary:
  contructor index are 1-based
- refinement of indtypes fixed:
  - missing undebujinate added
  - index for current indty was in the wrong order
- apply_subst moved to nCicUntrusted
- new iterator for obj_kind

more tests

Nuova gestione di "by" per auto.

autobatch by

- librarian: 3 bugs fixed in the building system:
1) external dependences must be built using the path relative to their baseuri
2) the path of a non-existent .ma generated by a .mma was wrong
3) the compilation status of external dependences must be cached as for the other files in order to avoid looping.

Repetition of failed compilation remains for dependences of external dependences because the the external compilation caches are lost in the building process

When a devel is entered or leaved, its baseuei is printed for reference. This helps to disambiguate the files with the same name (eg original and reconstructed)
We hope that this will not bother the tests collection mechanism.

- core_notation: notation for non-functional exists had the wrong precedence

- procedural/library/Makefile: -onepass was added by mistake: datatypes/bool.ma fails with -onepass because of the ambiguity of the /\ notation

run check_if_goal_is_solved on all goals (active+passive)

Added an option --enable-annot to the configure to compile with -dtypes

Minor changes pro-automation

Added a passive table

Calling paramodulation instead of demod_all

Refinement of inductive type implemented.
Some functions have been exported from the kernel :-( to avoid code
duplication.

Note: the code seem to be bugged (wrong context), but the operations are taken
verbatim from the kernel. Have we really tested it on inductive types?