freescale porting, work in progress

 freescale porting, work in progress

fix to speedup reduction making intermediate conversion problems smaller

fixed eliminator name

some work

CIC has no eta-reduction/expansion

do not fail if the inductive type is mutual, just do not generate the eliminator

decent error on interpretation declaration

fix double app in Ast

better print of ILLEGAL applications

lint target improved

basic_rg: bugfix in AST to allow attributes in global entries
xml: the exported XML data now comply a DTD
icons: crux icon for the browser's address line
Makefile: "lint" entry added for XML validation

catch wrapped exception

alias bug revealed

...

initial and incomplete port of the old demo about inductively generated formal
topologies. we try to make slightly different choices...

exponentiation should output with \sup not with ^, that is meant to be an
input only notation.

added "already defined"

ncoindutive now generates a co-inductive type, not an inductive one

Meta case not handled, the iterator was complaining.

Nicer proof "finished" (up to arithmetical facts).

- alpha convertibility test disabled for now (it needs better implementation)
- some icons related to lambda-delta are now available

Towards a simplified proof.

...

Injectivity proved! What a mess...

...

- Bug fixed in definition of big_op.
- ltb now goes to booleans
- the meaning of big_x n is to sum from 0 to (pred n);
  in particular big_x O is the neutral element.
  Thus the isomorphism is broken.

...

- sort inclusion must be restricted to term backbone in order to avoid
validity of non-normalizing terms (see the omega.aut example)
- command-line options -a and -p rearranged

One half done.

...

...

...

...

- alpha conversion check added to the brg kernel (succeeds 1/4 of the times)

- performance data added for reference
- interface of the Hierarchy module improved
- library for managining abstract layer representation files added
- toplevel improved: the analysis of the automath source is now optional

- proper KAM with closures implemented for the brg kernel

- kernel parameters indication added to exported objects (xml)
- some refactoring

...

...

Since the introduction of saturation, an assert false is now possible
(i.e. locked meta vs non flexible term since some saturations have not been
fully performed yet)

 freescale porting, work in progress

- xml exportation activated for the brg kernel
- improved Makefiles

(nat,plus) is an abelian, unital magma

Some quick patch to fix elimination that used to look for
nat_rect_max{CProp0,Type0}

fix_sorts (cfr. previous commit) used to break too many things.
This commit is a more conservative extension...

Assert false do not allow to debug...

Let's refresh the universe to avoid assert failure.
However, the effect of this is still unclear to me.

 freescale porting, work in progress

A very little bit of arithmetic.

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

basic_rg: improved interface, unwind removed from applicability check
basic_ag: improved interface
common: kernel code sharing started

 freescale porting, work in progress

The first omomorphism theorem for whole sets (i.e. setoids + morphisms, not
sets + morphisms).

Hmmm: I don't see much gain here.

Metas must be handled when using iterators.

Setoid rewriting as unification hinting. Does not work recursively yet.
(Why??)

 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

 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