]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agoSome results on relations. Moved things around.
Andrea Asperti [Tue, 5 Jun 2012 11:29:18 +0000 (11:29 +0000)]
Some results on relations. Moved things around.

12 years agoCompleted all proofs in if_machine
Andrea Asperti [Tue, 5 Jun 2012 08:22:40 +0000 (08:22 +0000)]
Completed all proofs in if_machine

12 years agoan addition to basic_2
Ferruccio Guidi [Mon, 4 Jun 2012 20:39:26 +0000 (20:39 +0000)]
an addition to basic_2

12 years ago- lambda_delta: subject reduction for nativa type assignment begins ...
Ferruccio Guidi [Mon, 4 Jun 2012 20:34:11 +0000 (20:34 +0000)]
- 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)

12 years agosemantics of the if-machine.
Andrea Asperti [Mon, 4 Jun 2012 14:16:05 +0000 (14:16 +0000)]
semantics of the if-machine.
Moved some lemmas to their proper places.

12 years agonotation
Andrea Asperti [Mon, 4 Jun 2012 08:31:30 +0000 (08:31 +0000)]
notation

12 years agocomments
Andrea Asperti [Mon, 4 Jun 2012 06:35:09 +0000 (06:35 +0000)]
comments

12 years agoadditions to basic_2
Ferruccio Guidi [Sat, 2 Jun 2012 18:46:34 +0000 (18:46 +0000)]
additions to basic_2

12 years ago- predefined_virtuals: an addition
Ferruccio Guidi [Sat, 2 Jun 2012 18:37:03 +0000 (18:37 +0000)]
- predefined_virtuals: an addition
- lambda_delta: lenv ref for native type assignment completed
                levn ref for substitution correctly oriented

12 years agoFinalized copy sub-machine of the universal turing machine. Some new results
Wilmer Ricciotti [Fri, 1 Jun 2012 14:40:49 +0000 (14:40 +0000)]
Finalized copy sub-machine of the universal turing machine. Some new results
on lists.

12 years agoCi siamo quasi
Andrea Asperti [Fri, 1 Jun 2012 12:53:28 +0000 (12:53 +0000)]
Ci siamo quasi

12 years agoupdate in basic_2
Ferruccio Guidi [Fri, 1 Jun 2012 12:36:29 +0000 (12:36 +0000)]
update in basic_2

12 years ago- predefined_virtuals: some additions
Ferruccio Guidi [Fri, 1 Jun 2012 12:34:16 +0000 (12:34 +0000)]
- predefined_virtuals: some additions
- lambda_delta: first results on lenv. ref. for native typing
                some notational changes

12 years agoThanks to Guarrigue, code for Serializer functor simplified using
Claudio Sacerdoti Coen [Thu, 31 May 2012 13:52:13 +0000 (13:52 +0000)]
Thanks to Guarrigue, code for Serializer functor simplified using
private types. The type system of OCaml is more and more misterious...

12 years agoProgress.
Wilmer Ricciotti [Thu, 31 May 2012 10:51:18 +0000 (10:51 +0000)]
Progress.

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 30 May 2012 21:12:25 +0000 (21:12 +0000)]
update in basic_2

12 years ago- nDestructTac: Sys.break handled in two places
Ferruccio Guidi [Wed, 30 May 2012 21:10:44 +0000 (21:10 +0000)]
- 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

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 14:20:28 +0000 (14:20 +0000)]
Progress.

12 years agosome progress
Andrea Asperti [Wed, 30 May 2012 11:56:33 +0000 (11:56 +0000)]
some progress

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 09:11:08 +0000 (09:11 +0000)]
Progress.

12 years agoProgress.
Wilmer Ricciotti [Wed, 30 May 2012 08:35:51 +0000 (08:35 +0000)]
Progress.

12 years agoThe universal machine!!!
Andrea Asperti [Tue, 29 May 2012 14:01:20 +0000 (14:01 +0000)]
The universal machine!!!

12 years agotrans_step.ma
Andrea Asperti [Mon, 28 May 2012 16:42:25 +0000 (16:42 +0000)]
trans_step.ma

12 years agoporting move_tape.ma
Andrea Asperti [Mon, 28 May 2012 14:02:42 +0000 (14:02 +0000)]
porting move_tape.ma

12 years agoporting move_char_l.ma
Andrea Asperti [Mon, 28 May 2012 13:47:38 +0000 (13:47 +0000)]
porting move_char_l.ma

12 years agoporting of move_char_c
Andrea Asperti [Mon, 28 May 2012 13:33:45 +0000 (13:33 +0000)]
porting of move_char_c

12 years agomore typos
Andrea Asperti [Mon, 28 May 2012 12:13:49 +0000 (12:13 +0000)]
more typos

12 years agotypos
Andrea Asperti [Mon, 28 May 2012 12:11:59 +0000 (12:11 +0000)]
typos

12 years agograph of a function
Andrea Asperti [Mon, 28 May 2012 11:42:02 +0000 (11:42 +0000)]
graph of a function

12 years agoFinOpt
Andrea Asperti [Mon, 28 May 2012 11:25:09 +0000 (11:25 +0000)]
FinOpt

12 years agomem, split
Andrea Asperti [Mon, 28 May 2012 06:21:26 +0000 (06:21 +0000)]
mem, split

12 years agoProgress.
Wilmer Ricciotti [Mon, 28 May 2012 06:19:50 +0000 (06:19 +0000)]
Progress.

12 years agotentative specification of Conway's construction for surreal numbers
Ferruccio Guidi [Sat, 26 May 2012 12:47:48 +0000 (12:47 +0000)]
tentative specification of Conway's construction for surreal numbers
matita.opt game.ma crashes after 4 lines of code :((

12 years agoupdate in basic_2
Ferruccio Guidi [Fri, 25 May 2012 17:16:04 +0000 (17:16 +0000)]
update in basic_2

12 years ago- substitution lemma for native type assignmenr proved!
Ferruccio Guidi [Fri, 25 May 2012 17:10:54 +0000 (17:10 +0000)]
- substitution lemma for native type assignmenr proved!
- notation change in the support for abstract c.r.'s
- some minor additions

12 years agoProgress
Wilmer Ricciotti [Fri, 25 May 2012 16:15:31 +0000 (16:15 +0000)]
Progress

12 years agoPorting to the new defintion of finset
Andrea Asperti [Fri, 25 May 2012 08:59:21 +0000 (08:59 +0000)]
Porting to the new defintion of finset

12 years agoNew definition of finset.
Andrea Asperti [Fri, 25 May 2012 08:58:36 +0000 (08:58 +0000)]
New definition of finset.

12 years agoa bit faster
Andrea Asperti [Fri, 25 May 2012 07:12:54 +0000 (07:12 +0000)]
a bit faster

12 years agoProgress
Wilmer Ricciotti [Thu, 24 May 2012 15:15:14 +0000 (15:15 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Thu, 24 May 2012 09:52:31 +0000 (09:52 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Wed, 23 May 2012 14:32:15 +0000 (14:32 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Wed, 23 May 2012 09:52:17 +0000 (09:52 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 16:07:23 +0000 (16:07 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 14:27:50 +0000 (14:27 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Tue, 22 May 2012 09:50:14 +0000 (09:50 +0000)]
Progress

12 years agoProgress.
Wilmer Ricciotti [Mon, 21 May 2012 16:57:38 +0000 (16:57 +0000)]
Progress.

12 years agoAdded move_tape.ma
Wilmer Ricciotti [Mon, 21 May 2012 11:57:26 +0000 (11:57 +0000)]
Added move_tape.ma

12 years agoProgress
Wilmer Ricciotti [Mon, 21 May 2012 11:57:00 +0000 (11:57 +0000)]
Progress

12 years agoNew version of init copy
Andrea Asperti [Mon, 21 May 2012 09:12:57 +0000 (09:12 +0000)]
New version of init copy

12 years agoProgress
Wilmer Ricciotti [Fri, 18 May 2012 16:30:03 +0000 (16:30 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Fri, 18 May 2012 15:43:37 +0000 (15:43 +0000)]
Progress

12 years agoinit_copy init_match
Andrea Asperti [Fri, 18 May 2012 11:24:56 +0000 (11:24 +0000)]
init_copy init_match

12 years agoProgress in semantics of the copy machine.
Wilmer Ricciotti [Fri, 18 May 2012 10:31:48 +0000 (10:31 +0000)]
Progress in semantics of the copy machine.

12 years agodepenences fixup
Ferruccio Guidi [Thu, 17 May 2012 20:11:06 +0000 (20:11 +0000)]
depenences fixup

12 years agoinit_match
Andrea Asperti [Thu, 17 May 2012 16:34:03 +0000 (16:34 +0000)]
init_match

12 years agoProgress
Wilmer Ricciotti [Thu, 17 May 2012 16:33:59 +0000 (16:33 +0000)]
Progress

12 years agoProgress
Wilmer Ricciotti [Thu, 17 May 2012 14:18:36 +0000 (14:18 +0000)]
Progress

12 years agoAdded step machine for universal machine.
Wilmer Ricciotti [Thu, 17 May 2012 14:12:45 +0000 (14:12 +0000)]
Added step machine for universal machine.

12 years ago...
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:40:37 +0000 (11:40 +0000)]
...

12 years ago...
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:37:49 +0000 (11:37 +0000)]
...

12 years agoEfficient hashing used.
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:33:34 +0000 (11:33 +0000)]
Efficient hashing used.

12 years agohash function exported
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:32:52 +0000 (11:32 +0000)]
hash function exported

12 years agoThe lpo cache is now implemented as an hastbl for more performance
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:26:24 +0000 (11:26 +0000)]
The lpo cache is now implemented as an hastbl for more performance
improvement. Probably it would be better with an ad-hoc hash-function.

12 years agomove tape right
Wilmer Ricciotti [Thu, 17 May 2012 09:28:06 +0000 (09:28 +0000)]
move tape right

12 years agofiltering on a list without repetitions
Andrea Asperti [Thu, 17 May 2012 07:20:23 +0000 (07:20 +0000)]
filtering on a list without repetitions

12 years agoAdded null character.
Wilmer Ricciotti [Thu, 17 May 2012 07:04:54 +0000 (07:04 +0000)]
Added null character.

12 years agoAdded cache to lpo implementation.
Claudio Sacerdoti Coen [Wed, 16 May 2012 23:32:12 +0000 (23:32 +0000)]
Added cache to lpo implementation.
The current cache is based on imperative lists.
Can it be improved with smarter data structures (e.g. HashTables?)

12 years agoOrientation of equalities is now displayed.
Claudio Sacerdoti Coen [Wed, 16 May 2012 22:25:03 +0000 (22:25 +0000)]
Orientation of equalities is now displayed.

12 years agoOrientation of equalities is now displayed.
Claudio Sacerdoti Coen [Wed, 16 May 2012 22:24:08 +0000 (22:24 +0000)]
Orientation of equalities is now displayed.

12 years agoRemoved duplicated notation and interaction with the user.
Claudio Sacerdoti Coen [Wed, 16 May 2012 20:33:41 +0000 (20:33 +0000)]
Removed duplicated notation and interaction with the user.

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 16 May 2012 20:30:28 +0000 (20:30 +0000)]
update in basic_2

12 years ago- a caracterization of the top elements of the local evironment
Ferruccio Guidi [Wed, 16 May 2012 20:28:10 +0000 (20:28 +0000)]
- 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

12 years agoCompare was not compatible with eq!
Claudio Sacerdoti Coen [Wed, 16 May 2012 20:21:59 +0000 (20:21 +0000)]
Compare was not compatible with eq!
The first used alpha_eq, the second did not.
Now both do.

12 years agoNew, faster implementation of lpo checked against old one.
Claudio Sacerdoti Coen [Wed, 16 May 2012 19:28:27 +0000 (19:28 +0000)]
New, faster implementation of lpo checked against old one.
Old code removed.

12 years agoAdded alias instance=1 to avoid interaction with the user.
Claudio Sacerdoti Coen [Wed, 16 May 2012 19:06:53 +0000 (19:06 +0000)]
Added alias instance=1 to avoid interaction with the user.

12 years agoNew implementation of lpo (the previous one was sometimes expnential)
Andrea Asperti [Wed, 16 May 2012 13:26:58 +0000 (13:26 +0000)]
New implementation of lpo (the previous one was sometimes expnential)

12 years agoa bit more
Andrea Asperti [Wed, 16 May 2012 07:53:04 +0000 (07:53 +0000)]
a bit more

12 years agoPruning generalized from Vars to applied Vars.
Claudio Sacerdoti Coen [Tue, 15 May 2012 23:20:33 +0000 (23:20 +0000)]
Pruning generalized from Vars to applied Vars.
Assert false since it can happen (???) that an equation
is oriented as ? M -> N   :-(

12 years agoBug fixed in does_not_occur when a LetIn was found in the context.
Claudio Sacerdoti Coen [Tue, 15 May 2012 20:47:27 +0000 (20:47 +0000)]
Bug fixed in does_not_occur when a LetIn was found in the context.

12 years agoprint => debug
Claudio Sacerdoti Coen [Tue, 15 May 2012 19:34:23 +0000 (19:34 +0000)]
print => debug

12 years agoPatch by Ferruccio that enables \top/\bot for False/True undone.
Claudio Sacerdoti Coen [Tue, 15 May 2012 19:26:03 +0000 (19:26 +0000)]
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.

12 years agoProgress
Wilmer Ricciotti [Tue, 15 May 2012 17:01:42 +0000 (17:01 +0000)]
Progress

12 years agowe added the standard notation for True and False (logical constants)
Ferruccio Guidi [Tue, 15 May 2012 16:11:07 +0000 (16:11 +0000)]
we added the standard notation for True and False (logical constants)

12 years agoDivergence during indexing fixed: (? t = t') was not recognized as too flexible.
Claudio Sacerdoti Coen [Tue, 15 May 2012 13:14:17 +0000 (13:14 +0000)]
Divergence during indexing fixed: (? t = t') was not recognized as too flexible.

12 years agoSys.Break no longer caught during indexing
Claudio Sacerdoti Coen [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
Sys.Break no longer caught during indexing

12 years agosempre li
Andrea Asperti [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
sempre li

12 years agoAdded universal machine (mockup)
Wilmer Ricciotti [Tue, 15 May 2012 09:56:18 +0000 (09:56 +0000)]
Added universal machine (mockup)

12 years agoAdded copy machine (mockup)
Wilmer Ricciotti [Mon, 14 May 2012 16:41:07 +0000 (16:41 +0000)]
Added copy machine (mockup)

12 years agoprogresprogresss
Andrea Asperti [Mon, 14 May 2012 16:37:56 +0000 (16:37 +0000)]
progresprogresss
-

12 years agoalmost there
Andrea Asperti [Mon, 14 May 2012 15:26:56 +0000 (15:26 +0000)]
almost there

12 years agoprogress
Andrea Asperti [Mon, 14 May 2012 11:55:54 +0000 (11:55 +0000)]
progress

12 years agoDefinition of the structure of the transition table of a
Wilmer Ricciotti [Fri, 11 May 2012 17:03:27 +0000 (17:03 +0000)]
Definition of the structure of the transition table of a
simulated Turing Machine.

12 years agopoca roba
Andrea Asperti [Fri, 11 May 2012 11:59:16 +0000 (11:59 +0000)]
poca roba

12 years agorestructuring
Andrea Asperti [Fri, 11 May 2012 11:23:40 +0000 (11:23 +0000)]
restructuring

12 years agoFinished wsem_compare proof.
Wilmer Ricciotti [Fri, 11 May 2012 10:29:56 +0000 (10:29 +0000)]
Finished wsem_compare proof.

12 years agoprogress
Andrea Asperti [Fri, 11 May 2012 09:02:25 +0000 (09:02 +0000)]
progress

12 years agoProgress.
Wilmer Ricciotti [Thu, 10 May 2012 16:55:35 +0000 (16:55 +0000)]
Progress.

12 years ago- notation changes in basic_2
Ferruccio Guidi [Thu, 10 May 2012 16:02:55 +0000 (16:02 +0000)]
- notation changes in basic_2

12 years ago- predefined_virtuals: an addition
Ferruccio Guidi [Thu, 10 May 2012 15:57:36 +0000 (15:57 +0000)]
- predefined_virtuals: an addition
- lambda_delta: some notation changes