use universe rank instead of Type0

Type related failures fixed

better pp of objects

Extracted code. The main executable is medium_tests that runs the emulator on
a few assembly programs with inputs of different sizes:
  * string reverse
  * counting sort
  * perfect numbers

removed useless file

fixed modules order

more fix removed from types

more fix removed from types in proofs

when we build the elimination principle we fresh universes to not
generate tems with different

added a parameter to unshare universes

Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.

context of types built in the reverse order

added a simplify to prevent the generation of an ugly fix

implemented inductive and less parentheses

The cache of objects is now used also for cofixpoints.

New: cache of translated fixpoints (to avoid the generative fix restriction and
to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)

does_not_occur exported to be used in oCic2NCic

Bug fixed: references to CoFix are CoFix, not Fix.

print unnamed variables as __n

switch off profilers

pp with parenthesis only when necessary and with some more boxes

...

Fixed serious bug that occurred only in the following situation:

\lambda x.
Fix f {
\lambda y: P x.
Fix g {

The two fixes must be translated as

Fix f { \lambda x. \lambda y: P x. ...}
Fix g { \lambda x. \lambda f. \lambda y: P x. ... }

In the first case, the x that occurs in the type of y must be a Rel 1.
In the second case, the x that occurs in the type of y must be a Rel 2.
The previous code translated both of them to Rel 1.

better pp in Appl

better pp

pretty printer on steroids

Added some "\n" here and there to the pretty-printing of Match.

Grave bug fixed: Ce that point to definitions were handled as those that point
to declarations. So Fix-constants were too much abstracted, too much applied,
etc.

added profiling on/off

invalidate fixed

allow to switch profiling on and off on the fly

removed two useless calls to the environment, one still to be optimized out

...

Variables are no longer experted (cooking is now implemented).
Better reporting with indentation.

Swapped arguments in error message.

Variables having a body can occur in cooked terms and must be delta-expanded
during translation to the new CIC format.

Fix over the previous one: Var-LetIn abstractions should be ignored and not
transformed into applications at all.

Error message improved.

Cooking w.r.t. variables with bodies is now implemented as delta-expansion.

Fix name capture in cofix.

To test the translation.

Name capture fixed.

Improved error messages in place of "sort elimination not allowed".

Seed reset before each convert_obj.

Use seed to avoid further name clashes.

...

Incredible, but true! Our name mangling clashed with one identifier in the
library of Coq, generating two functions that mutually called each other,
making the type-checker diverge!!!!

Cooked objects are no longer well typed in the uncooked old environment.
Thus we need to fix_outtype before cooking.

Improved eat_prods error message (at the cost of passing the 6th argument!)

The old kernel does not accept ens whose order is different from the one
declared for the object whose reference it is applied to. Fixed.

Bad alpha-conversion by Enrico fixed.

Bug fixed: the ens need not be ordered w.r.t. the declared variables.
The latter order is the right one for abstraction.

j off by one in error message

fix_outty partially fixed: missing lifts in args and ens

fix_outty fixed in order to perform eta-expansion when the term is not
a sequence of lambdas.

added simplify to avoid ugly proofterm

Tentative (and bad!) fix of outtypes in non-dependent eliminations.
The fix does not work since there is no guarantee in Coq that the outtype
is made of a sequence of Lambdas (and indeed it is not for automatically
generated elimiantion principles). Thus I need to perform recursion on the
type of the outtype and I also need to perform some eta-expansion to insert
the additional lambda in the right position :-(

Cooking discriminated into cooking in types (using Prods) and cooking in bodies
(using Lambdas).

Pretty-printing of definitions fixed.

Cooking implemented (not tested yet).

Reports improved.

Debugging code fixed.

added invalidate to clear the cache and ease the comparison with the new kernel

commented out uris of objs that do not compile properly

added comparison with old kernel

fixed error message for eat prods

invalidate

uris relative to axioms are translated in the right way

added invalidate

added preliminary checks for indtys
typecheck the explicit type of letins

call get_obj instead of get_cooked_obj ~trust:false

added case of const and axiom

added # to comment

better printings

the explicit type in a LetIn must be typecheckd before convertibility is checked

opt compilation enabled, removed some pps, check has -alluris to regenerate
the uri list, alluri sorted such that the last fpart of the file fails (but not the former).
all nat/ compiles!

lefts_ad_tys properly sorted, added some metasenv here and there,
recursive args defined in case of appl

lefts_and_tys was tys@lefts, CSC claims it was working since that context is only used
by whd and it did not contain any definitions by contructions, thus the length was the only important bit

added a list of uris to ease debugging

print the excpetion and raise it again, seems to produce a reasonable backtrace

new constants have depth = max_int insted of 0 so that reducing to 0 expands them

off by one in calling count_from

fixed bug in translating Fix, recno was not properly computed

added a pretty printing of the new object and use argv[1] as uri

context, metasenv and subst made mandatory in CicPp

guarded by has a nice error message

reference type made private, added mk_constructor to be used
to create the i-th constructor of an inductive type (used in match typechecking).

fixed name capture in oCic2nCic when typing fixpoint types

some debug printings

added to the cache a boolean to state if the object is
already checked or not (a frozen list is really needed)

fix

today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_args since k starts from 1

added ppobj

type_of_constant was retunrning the type of the wrong constructor (-1 missing)
fixpoints were not properly debruijnated before being checked
better error message for match branches

fixed list.nth and added some paretheses

added some printings and catched more exceptions

removed useless printing

iterator map was mapping Lambdas to Prods!!!

debugging started

type of constant ported

added add_obj to store objects in the environment, implementation still
shaky since no frozen list is there