Don't reinvent the wheel.

Added benchmarks

 freescale porting, work in progress

New demodulation (innermost, optimized to avoid reducing already normalized
subterms).

Changed the ordering of rels, and the introduction of hypothesis to get
a version closer to the standalone prover.

Lazy strings
-This line, and those below, will be ignored--

    paramod.ml

Added the benchmark with the new demodulation function.

"..." -> "\ldots" for implicit vectors

1) Some more work for vector implicits.
2) Vector implicits can be used only in argument position.

Introduction of vectors of implicit (only for NG).
Proposed concrete syntax: "..."

New reference benchmark with CPU Time

Removed meaningless time information

Removed internal default timeout
Added TreeLimitedRun (CASC) script to run_on_a_list

Stupid bug fixed: the test to detect Uncertain cases was simply reverted.

Removed old logs

Useless "let module" removed.

Since I guess the divergence bug is fixed, I activate the test again.

Serious bug fixed: because of lazy evaluation of !require1, the function could
diverge.

setoids.ma split into setoids.ma + setoids1.ma

topology/igt.ma (???) |-> sets/setoids.ma

...

Moved benchmarks to new folder

It works better now.

...

No more hand-made coercions.

Debugging code removed.

Record fields declared as coercions as now really declared as coercions.

Beta-expansion was avoided as soon as one argument was flexible.
This lead to a different behaviour in the following two unification problems:

   (\lambda_.?) ? =?= T         vs               ? ? =?= T
     or, equivalently
        ?[?] =?= T

The fix is very easy: we always perform beta-expansion and delifting will
take care of ignoring the flexible "arguments", both during beta-expansion
and during the unification that follows.

...

Function to map NCic.term to CicNotationPt.term finished.
Note: it is almost identical to ncic_of_ast0, but it uses a different data
type for contexts that allow to perform "substitution" in a single operation.
Moreover, the terms that are substituted are CicNotationPt.terms and not
NCic.terms. The two codes really ought to be unified.

Bug (found during code review) fixed (but not tested and bug never re-produced):
wrong context passed around.

...

 freescale porting, work in progress

 freescale porting, work in progress

Elimination principles are now processed in O(1) again

Major speed-up: meta-chains are now expanded during restriction to avoid
creating longer ones and to avoid restricting twice the same conjecture.

Fixed test for invertibility

...

1) PTS simplified
2) several eliminiation principles and projections are now automatically generated

Now using lazy strings for debug printings

...

nelim fixed

leftno was List.length rights :-)

Almost ready to implement coercion declaration for record fields. But how?

 freescale porting, work in progress

1) record projections are now automatically generated
2) incomplete code commented out

Debugging code removed.

Record projections are now automatically generated for NG.

Note: I have implemented a partial function from NCic.term to
CicNotationPt.term. Is there already a similar function? Where should it be
moved?

Implemented handling of Invertible equalities
Fixed nasty bug in inferences for Incomparable equalities

sorted modules

Debugging printf removed

nrewrite now uses the appropriate principle when going from right to left

nrewrite now working

...

Removed status printing by processes

Fixed multiple printing

Final version, submitted to CASC-22.

added a flag for age selection

Very serious bug fixed in unification, but the fix is very ugly.

Explanation: we have reduced the case ? x1 .. xn to the case
?[x1,...,xn] by mean of lambda-abstractions. However, these need to be
typed. The way we used to type them was with non-dependent types. Thus they
failed in almost all dependent cases (like rewrite).

This fix seems to work and uses a few lines of code, but it requires a call
to the unifier which is VEEERY bad.

Debugging prints still to be removed.

1) The NG kernel now accepts only usage of declared universes
2) Bug (badly) fixed in NCicElim: it used to generate undeclared universe
   names.

One-side indexing for commutativity

No demod call on functionnal symbols

1) ppmetasenv and ppcontext to reduce the amount of printed information during
   debugging
2) BUG FIXED: boxes (in particular out_scope ones) could happear in the
   substitution after unification. In particular, this happened when the goal
   had the form   H: False |- C  and we tried to "nelim H". After the
   unification, some meta ?1 was instantiated with ?os where ?os := C. This
   triggered a unification C =?= ?1 before the end of the tactic (hence
   before the apply_subst). As a result, the ad-hoc unification case for
   in_scope/out_scope was triggered on inputs of the bad shape and an assert
   false was raised.

 freescale porting, work in progress

...

nelim now uses the appropriate _rect_XXX elimination principle

1) the user is notified when a new object is defined
2) (very ugly) "detection" of elimination principles that cannot be defined

More info to refine empty types elimination.

Old code commented out.

Generation of principles is now atomic.

Debugging code commented out.

add comment

Non reproducible.

Some bugs already fixed.

Bugs (mostly from Oliboni)

Bug fixed: singleton application.

New suffixes for elimination principles:

_ind (towards Prop)
_rect_UNIVERSENAME (towards Type)

1) added a function to retrieve all the universes currently in use
2) INCONSISTENCY BUG FIXED: it was possible to _redefine_ an already defined
   constant. Thus it was very easy to prove False!

 freescale porting, work in progress

Generation of inductive principle for Type[0].

The way the code has been branched is very messy: we generate an AST and
from it a new command NObj that is recursively processed in GrafiteEngine.
However, disambiguation needs the alias. Thus the aliases for the inductive
principle are immediately generated and added while the others are delayed.

 freescale porting, work in progress

Sorted version of eligible problems list

Disabled age selection and ad hoc goal weight computation

ncopy partially implemented and fixed (a ?) chain to print elimintaors

Fixed dependency function, which was lacking the code for recursive calls.

...

match_coercion gives back the saturations, not the arity:
`f ??????? x ???? y z` has to be rendered as `x y z`
   <----->   <-->
    cpos     stat

 freescale porting, work in progress

Fixed Option type error (OCaml bug)

.

.

 freescale porting to ng, work in progress

better spacing

statistics are used, when possible, to sort
constants

Added statistics printings

Added statistics module

First proof finished (some tactics still not working).

matitaprover is now flexible enough to allow the computation of statistics on
the clauses and then choose an ordering to be used for the proof search

Coercion hiding implemented. Notes:

1) hiding of coercions whose return type is a product is not done correctly,
   since the "sats" information seem to have changed semantics. Enrico, is it
   a bug or just a new semantics?
2) coercion matching has been implemented trivially (O(n)) in NCicCoercion.
   Here I need a special version of a discrimination tree. Enrico, do we have
   one already or is there a way to simulate it?

 freescale translation (work in progress)