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)

Composite coercions are here!

- brgOutput: the nodes count is now implemented
- brgReduction: the type annotation in the beta-reductum is useless
- brgType: a never-occurring condition marked with assert false

initial implementation of coercion composition

more work on coercions composition

 +root +depends

Removed unused parameter of unification procedure (vars)

more profilers

Coercions used here and there.

Bug fixed (missing ctx) + comment added.

...

new ng freescale, no external dependencies

Let's live with new ocaml type system limitations...

initial implementation of `ncoercion name : type := body on name : pat to pat`

claudio, please have a look at this

new nrepeat (and block '('...')' ) tactical

...

New functorialization: paramod is abstracted over a Orderings.Blob, that is like Terms.Blob but adds the compare_terms function.
This allows an easy instantiation of the main loop with differend orderings

Fixed check for condition iv p.33 (Riazzanov)

More updates to Fsub.

profile most operations, do not return a filtered varlist in unif (useless and expensive)

1 process for now

two cases should be assert false at least in TPTP

micro optimizations to unification

Cleaned a bit

...

activate kbo, not lpo

...

Bug fixed (non-captured variable).

eq moved to CProp
In Prop a unification problem was not solved, but I suspect that that was
a bug...

...

repeat_tac