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.

Patch to improve the pretty-printing of error messages.
Moreover, when a delift creates an ill-typed term, a more
informative error message is printed (even if later
backtracking makes it irrelevant).

additions to basic_2

- lib: some additions
- lambda_delta: more properties on native type assignment
                change of notation for consand append

Sys.Break no longer captured in two places.

axiomatization of acc_if

Progress.

Progress in compare.ma (some machines have been moved to tests.ma and marks.ma)

progress in turing/universal/compare.ma

Added compare auxiliary machine for universal turing machine.

progress

Prove di terminazione

More examples

starl

Forgotten in previous commit: move_char machines.

Added a turing/universal directory for the universal turing machine (and
auxiliary definitions).
Added the definition of machine move_char (variant c) to be used in the
universal machine.
Small library refactoring.

progress

Speed up: moved a #ppterm inside the lazy it belongs to.

progress in while test machine

additions in basic_2

- more properties on lifting, slicing, delifting and thinning

prod fin set
-

bool and segments of natural numbers

While semantics.

split e merge

progress
-

while machine

Added weak realizability.

Added wmono.

More proofs in if-then-else machine.

Le configurazioni sono definite non su macchine ma su stati.
Idem per alcune funzioni di lift.

Definition of accRealize

If machine

Monotape turing machines update.

more loop proofs

loop functions

loop functions

Mono tape turing machines

Extensions to finset (sum) and auxiliary lemmas.

- notation (possibly affecting all .ma files):
  we shifted the precedence levels from 50 to 60 up by 5
  and moved level 65 to 66. By so doing, we cleared level 50 for
  use in the specification of the formal system lambda_delta,
  where we use it for weakly binding constructors
- lambda_delta:
  notation fixup (a couple of bugs were corrected)

additions in basic_2

- lambda_delta: bug fix in static type assignment
                some theorems on delift and thin
- nat: eliminator for nat with "+1" rather than "S"

Update to universal turing machine (preliminaries).

More turing machines (still not compiling)

Started converting informal definition of the machines to matita code
(currently not compiling).

Added universal turing machines (only comments for now).

additions to basic_2

- lambda_delta: static type assignment is defined
- predefined_virtuals: some additions
- nat: we added a lemma

- update in basic_2

- firs theorems on native type assignment
- we removed iterated unfold on local environments
  since transitivity of this unfold is not needed so far