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

- boxPp: added missing spaces
- core_notation: bug fix in the input notation for congruent: we added term 90 after \sub
- library/nat/permutation.ma: added input notation for transpose and fixed term precedence in its output notation
- library/Makefile: compilation of single files re-enabled.
The syntax for compiling file.ma is is "make file.mo" and "make file.mo.opt"

now nat/congruence.ma and nat/permutation.ma are fully reconstructed :)

Update, using induction/inversion.

functorial abstraction over term blobs

not_to_not

New test for NG notation.

Huge commit with several changes:

1) CicNotationPres.render: type changed to make it more general (no
   dependency on the Hashtbl) and URI/REFERENCE agnostic.
   A compatibility function CicNotationPres.lookup_uri is provided to
   easily map the (old) Hashtbl to the (new) lookup function.
2) user interface partially changed to render NG objects in the CicBrowser
   and to follow NG hyperlinks
3) New CicNotationPt entries NRef (similar to Uri) and NRefPattern
   (similar to UriPattern) to avoid hijacking the old Uris (actually,
   uris + xpointers) to also hold new references.
   This allows to properly implement notation (for NG) and to properly
   handle hyperlinks.
4) all remaining Warnings for unused variables fixed (in some way or
   another, hopefully the correct one)
5) GrafiteEngine, NQed: the height of an object is now recomputed just
   before putting it in the environment. This fixes all the bugs related
   to reduction.
6) GrafiteParser/LexiconEngine: both old URIs and new references are now
   allowed in NG terms and in notations
7) ng_cic_content: rendering functions now return an "id |-> reference" table
   to correctly implement MathML hrefs
8) NReference: new compare function
9) NCicUntrusted: new height_of_obj_kind function (to be used in GrafiteEngine)
10) OCic2NCic: new reference_of_oxuri function to map old uris + xpointers
   into new references
11) bug fixed: after the commit by Enrico that starts using the extensible
   PTS, the old-to-new objects translations used to map Type into "Type" which
   was not declared. Type is now mapped into Type[0] and Type (as a "notation")
   is now a synonim of Type[0] (only during parsing for now)
12) bug fixed: after the commit by Enrico that cleans up terms for
    alpha-conversion and dummy products, the test in NCicTypeChecker that
    verifies the consistency of left parameters in constructor --- that used
    to do that NOT up to alpha-conversion --- used to fail when dummy products
    were found. The test is now relaxed to include alpha-conversion.
13) bug fixed: NCicTypeChecker did not verify that a .dec reference pointed to
    an axiom and that a .def reference did not point to an axiom. Fixed.

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.