cicEnvironment refactoring with sound view of Coq`s univ-less terms

assertion was wrong, an object can contain a named univers if its uri is the one of the object itself

graph generation phase fixed

Appl case in is_really_smaller fixed as in the old kernel

example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)

added a missing whd

new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).

Two similar cases packed together

some fixes for guardness conditions

is_really_smaller in sync with old kernel, impossible cases removed

check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.

1. bug fixed: the context must be type-checked before using it in type_of_aux'.
   Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
   argument is found in the body of another fix, the body of the inner fix
   is check adding the recusrive formal parameter as an additional safe
   argument.

get_checked_fix -> get_checked_fixes

added comment

added sample of guarded by in which coq is stronger

positivity check fixed, a MutInd not applied (but with an exp-named-subst)
was considere non strictly positive always

do not use an implicit but a sort as a neutral term for positivity check

objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required

leftno should be increased of the expnamedsubst, but counting only the uris of vars without a body

better error message

same_obj made more precise, fixed the order of the context for fixpoints body,
cache of fix extended to the mutual case (properly)

ficed fixpoint cache usage for mutual fix

fixed positivity conditions

added mk_fix i j r that given an r of a fix generated another fix on i and j

positivity condition was relying on the name declared in abstractions, and
was checking for a dependent product calling does not occurr with a wrong
index

added little optimization to not add twice the same arc

quinck and untested implementation of positivity conditions check

...

added depndency of new kernel to metadata to allow to use the DB to calculate the minimum set of graphs to load

FIXED bug, added assertion in case a universe inside a term T living at URI u
was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.

added function to fresh types

call Unshare.fresh_types

load the graph of objects that depend on the ones requested,
rank universes and use them in the transformation to obtain terms
with TypeK and not always Type0

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