Completed all proofs in if_machine

an addition to basic_2

- lambda_delta: subject reduction for nativa type assignment begins ...
                dependecnes between source files improved
- matitadep: little application for optimizing dependences between .ma files
             (used by lambda_delta Makefile)

semantics of the if-machine.
Moved some lemmas to their proper places.

notation

comments

additions to basic_2

- predefined_virtuals: an addition
- lambda_delta: lenv ref for native type assignment completed
                levn ref for substitution correctly oriented

Finalized copy sub-machine of the universal turing machine. Some new results
on lists.

Ci siamo quasi

update in basic_2

- predefined_virtuals: some additions
- lambda_delta: first results on lenv. ref. for native typing
                some notational changes

Thanks to Guarrigue, code for Serializer functor simplified using
private types. The type system of OCaml is more and more misterious...

Progress.

update in basic_2

- nDestructTac: Sys.break handled in two places
- lambda_delta: a major property of native type assignment
                some properties of context sensitive equivalence
some notational changes
some annotations

Progress.

some progress

Progress.

Progress.

The universal machine!!!

trans_step.ma

porting move_tape.ma

porting move_char_l.ma

porting of move_char_c

more typos

typos

graph of a function

FinOpt

mem, split

Progress.

tentative specification of Conway's construction for surreal numbers
matita.opt game.ma crashes after 4 lines of code :((

update in basic_2

- substitution lemma for native type assignmenr proved!
- notation change in the support for abstract c.r.'s
- some minor additions

Progress

Porting to the new defintion of finset

New definition of finset.

a bit faster

Progress

Progress

Progress

Progress

Progress

Progress

Progress

Progress.

Added move_tape.ma

Progress

New version of init copy

Progress

Progress

init_copy init_match

Progress in semantics of the copy machine.

depenences fixup

init_match

Progress

Progress

Added step machine for universal machine.

...

...

Efficient hashing used.

hash function exported

The lpo cache is now implemented as an hastbl for more performance
improvement. Probably it would be better with an ad-hoc hash-function.

move tape right

filtering on a list without repetitions

Added null character.

Added cache to lpo implementation.
The current cache is based on imperative lists.
Can it be improved with smarter data structures (e.g. HashTables?)

Orientation of equalities is now displayed.

Orientation of equalities is now displayed.

Removed duplicated notation and interaction with the user.

update in basic_2

- a caracterization of the top elements of the local evironment
refinement for substitution
- notation update for subsstitution and unfold
- added notation for True and False

Compare was not compatible with eq!
The first used alpha_eq, the second did not.
Now both do.

New, faster implementation of lpo checked against old one.
Old code removed.

Added alias instance=1 to avoid interaction with the user.

New implementation of lpo (the previous one was sometimes expnential)

a bit more

Pruning generalized from Vars to applied Vars.
Assert false since it can happen (???) that an equation
is oriented as ? M -> N   :-(

Bug fixed in does_not_occur when a LetIn was found in the context.

print => debug

Patch by Ferruccio that enables \top/\bot for False/True undone.
This needs some rediscussion. In particular:
 1) \top/\bot are also used as the (only?) symbols for bottom/top
    in square lattices. Overloading is not a great idea in this case
    (type vs term).
 2) \bot is also traditionally used as the undefined value. For instance,
    we use it in CerCo for (match ?:\bot in False with []) so that
    you can use/apply \bot just to say that that case is undefined.
    Interpretation can't be used for this because "match"es can't be used
    in interpretations. Thus we use a notation which cannot be overloaded
    and conflicts with Ferruccio's. Is there any other commonly used
    symbol for undefined terms?
 3) True/False are rarely used in statements. Do they really deserve
    a symbol? (maybe they do)

The patch can be re-enabled by re-applying the inverse svn diff of this commit.

Progress

we added the standard notation for True and False (logical constants)

Divergence during indexing fixed: (? t = t') was not recognized as too flexible.

Sys.Break no longer caught during indexing

sempre li

Added universal machine (mockup)

Added copy machine (mockup)

progresprogresss
-

almost there

progress

Definition of the structure of the transition table of a
simulated Turing Machine.

poca roba

restructuring

Finished wsem_compare proof.

progress

Progress.

- notation changes in basic_2

- predefined_virtuals: an addition
- lambda_delta: some notation changes

Progress.