freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

More Gonthierism. Are they the right solution?

...

Hmmm, quite broken now.

 freescale porting, work in progress

 freescle porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

Smaller formulae.

 freescale porting, work in progress

 freescale porting, work in progress

Setoids, setoids1, sets, and the like. The mess begins.

Note: the (partially) interesting part of the development is that canonical
structures (provided by unification hints) allow to perform setoid rewriting
by hieroglyphs without having to use "rich operators". On the other hand, after
the application what you get is always an enriched structure and thus either
it is normalized away or the theory becomes a mix of rich/unrich. The latter
phenomena happens anyway because, in algebraic structures, you need to put
things in rich structures to have all the properties you need.

algebra/magmas does not work because refinement of projection is too weak

Bad patch reverted (in error message).

Bug fixed: one case of too many arguments was not detected and used to diverge.

Serious bug fixed: uris were not refreshed when loading coercions.

Record projections are now defined as fixpoints in order to block
delta-expansion when the argument is not a constructor.

\ldots are now used in nelim and ncases

Pp fixed in order to obtain read-back.

1) \ldots here and there
   Where they are not used, it means they do not work!
2) napply/etc. now add \ldots at the end by default

More napply \ldots => napply

napply now automatically inserts \ldots at the end

More \ldots.

\ldots used here and there. Cool!

First implementation of \ldots.

Note: the implementation is now inefficient since implicits are generated and
mapped to metavariables again and again and again. It would be better to handle
\ldots as a coercion from \forall x:A.B(x) to B(?).

...

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.