]>
matita.cs.unibo.it Git - helm.git/log
Wilmer Ricciotti [Wed, 23 May 2012 09:52:17 +0000 (09:52 +0000)]
Progress
Wilmer Ricciotti [Tue, 22 May 2012 16:07:23 +0000 (16:07 +0000)]
Progress
Wilmer Ricciotti [Tue, 22 May 2012 14:27:50 +0000 (14:27 +0000)]
Progress
Wilmer Ricciotti [Tue, 22 May 2012 09:50:14 +0000 (09:50 +0000)]
Progress
Wilmer Ricciotti [Mon, 21 May 2012 16:57:38 +0000 (16:57 +0000)]
Progress.
Wilmer Ricciotti [Mon, 21 May 2012 11:57:26 +0000 (11:57 +0000)]
Added move_tape.ma
Wilmer Ricciotti [Mon, 21 May 2012 11:57:00 +0000 (11:57 +0000)]
Progress
Andrea Asperti [Mon, 21 May 2012 09:12:57 +0000 (09:12 +0000)]
New version of init copy
Wilmer Ricciotti [Fri, 18 May 2012 16:30:03 +0000 (16:30 +0000)]
Progress
Wilmer Ricciotti [Fri, 18 May 2012 15:43:37 +0000 (15:43 +0000)]
Progress
Andrea Asperti [Fri, 18 May 2012 11:24:56 +0000 (11:24 +0000)]
init_copy init_match
Wilmer Ricciotti [Fri, 18 May 2012 10:31:48 +0000 (10:31 +0000)]
Progress in semantics of the copy machine.
Ferruccio Guidi [Thu, 17 May 2012 20:11:06 +0000 (20:11 +0000)]
depenences fixup
Andrea Asperti [Thu, 17 May 2012 16:34:03 +0000 (16:34 +0000)]
init_match
Wilmer Ricciotti [Thu, 17 May 2012 16:33:59 +0000 (16:33 +0000)]
Progress
Wilmer Ricciotti [Thu, 17 May 2012 14:18:36 +0000 (14:18 +0000)]
Progress
Wilmer Ricciotti [Thu, 17 May 2012 14:12:45 +0000 (14:12 +0000)]
Added step machine for universal machine.
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:40:37 +0000 (11:40 +0000)]
...
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:37:49 +0000 (11:37 +0000)]
...
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:33:34 +0000 (11:33 +0000)]
Efficient hashing used.
Claudio Sacerdoti Coen [Thu, 17 May 2012 11:32:52 +0000 (11:32 +0000)]
hash function exported
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.
Wilmer Ricciotti [Thu, 17 May 2012 09:28:06 +0000 (09:28 +0000)]
move tape right
Andrea Asperti [Thu, 17 May 2012 07:20:23 +0000 (07:20 +0000)]
filtering on a list without repetitions
Wilmer Ricciotti [Thu, 17 May 2012 07:04:54 +0000 (07:04 +0000)]
Added null character.
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?)
Claudio Sacerdoti Coen [Wed, 16 May 2012 22:25:03 +0000 (22:25 +0000)]
Orientation 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.
Claudio Sacerdoti Coen [Wed, 16 May 2012 20:33:41 +0000 (20:33 +0000)]
Removed duplicated notation and interaction with the user.
Ferruccio Guidi [Wed, 16 May 2012 20:30:28 +0000 (20:30 +0000)]
update in basic_2
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
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.
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.
Claudio Sacerdoti Coen [Wed, 16 May 2012 19:06:53 +0000 (19:06 +0000)]
Added alias instance=1 to avoid interaction with the user.
Andrea Asperti [Wed, 16 May 2012 13:26:58 +0000 (13:26 +0000)]
New implementation of lpo (the previous one was sometimes expnential)
Andrea Asperti [Wed, 16 May 2012 07:53:04 +0000 (07:53 +0000)]
a bit more
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 :-(
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.
Claudio Sacerdoti Coen [Tue, 15 May 2012 19:34:23 +0000 (19:34 +0000)]
print => debug
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.
Wilmer Ricciotti [Tue, 15 May 2012 17:01:42 +0000 (17:01 +0000)]
Progress
Ferruccio Guidi [Tue, 15 May 2012 16:11:07 +0000 (16:11 +0000)]
we added the standard notation for True and False (logical constants)
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.
Claudio Sacerdoti Coen [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
Sys.Break no longer caught during indexing
Andrea Asperti [Tue, 15 May 2012 13:12:43 +0000 (13:12 +0000)]
sempre li
Wilmer Ricciotti [Tue, 15 May 2012 09:56:18 +0000 (09:56 +0000)]
Added universal machine (mockup)
Wilmer Ricciotti [Mon, 14 May 2012 16:41:07 +0000 (16:41 +0000)]
Added copy machine (mockup)
Andrea Asperti [Mon, 14 May 2012 16:37:56 +0000 (16:37 +0000)]
progresprogresss
-
Andrea Asperti [Mon, 14 May 2012 15:26:56 +0000 (15:26 +0000)]
almost there
Andrea Asperti [Mon, 14 May 2012 11:55:54 +0000 (11:55 +0000)]
progress
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.
Andrea Asperti [Fri, 11 May 2012 11:59:16 +0000 (11:59 +0000)]
poca roba
Andrea Asperti [Fri, 11 May 2012 11:23:40 +0000 (11:23 +0000)]
restructuring
Wilmer Ricciotti [Fri, 11 May 2012 10:29:56 +0000 (10:29 +0000)]
Finished wsem_compare proof.
Andrea Asperti [Fri, 11 May 2012 09:02:25 +0000 (09:02 +0000)]
progress
Wilmer Ricciotti [Thu, 10 May 2012 16:55:35 +0000 (16:55 +0000)]
Progress.
Ferruccio Guidi [Thu, 10 May 2012 16:02:55 +0000 (16:02 +0000)]
- notation changes in basic_2
Ferruccio Guidi [Thu, 10 May 2012 15:57:36 +0000 (15:57 +0000)]
- predefined_virtuals: an addition
- lambda_delta: some notation changes
Wilmer Ricciotti [Thu, 10 May 2012 15:49:45 +0000 (15:49 +0000)]
Progress.
Claudio Sacerdoti Coen [Thu, 10 May 2012 14:18:17 +0000 (14:18 +0000)]
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).
Ferruccio Guidi [Thu, 10 May 2012 11:06:02 +0000 (11:06 +0000)]
additions to basic_2
Ferruccio Guidi [Thu, 10 May 2012 10:58:45 +0000 (10:58 +0000)]
- lib: some additions
- lambda_delta: more properties on native type assignment
change of notation for consand append
Claudio Sacerdoti Coen [Thu, 10 May 2012 08:11:13 +0000 (08:11 +0000)]
Sys.Break no longer captured in two places.
Andrea Asperti [Thu, 10 May 2012 07:38:44 +0000 (07:38 +0000)]
axiomatization of acc_if
Wilmer Ricciotti [Wed, 9 May 2012 16:49:50 +0000 (16:49 +0000)]
Progress.
Wilmer Ricciotti [Wed, 9 May 2012 15:32:25 +0000 (15:32 +0000)]
Progress in compare.ma (some machines have been moved to tests.ma and marks.ma)
Wilmer Ricciotti [Tue, 8 May 2012 16:09:32 +0000 (16:09 +0000)]
progress in turing/universal/compare.ma
Wilmer Ricciotti [Tue, 8 May 2012 09:56:46 +0000 (09:56 +0000)]
Added compare auxiliary machine for universal turing machine.
Wilmer Ricciotti [Mon, 7 May 2012 15:34:16 +0000 (15:34 +0000)]
progress
Andrea Asperti [Mon, 7 May 2012 13:13:32 +0000 (13:13 +0000)]
Prove di terminazione
Andrea Asperti [Mon, 7 May 2012 06:28:47 +0000 (06:28 +0000)]
More examples
Andrea Asperti [Mon, 7 May 2012 06:26:54 +0000 (06:26 +0000)]
starl
Wilmer Ricciotti [Fri, 4 May 2012 16:58:11 +0000 (16:58 +0000)]
Forgotten in previous commit: move_char machines.
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:16:39 +0000 (15:16 +0000)]
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:14:44 +0000 (15:14 +0000)]
Wilmer Ricciotti [Fri, 4 May 2012 15:09:54 +0000 (15:09 +0000)]
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.
Wilmer Ricciotti [Fri, 4 May 2012 12:04:18 +0000 (12:04 +0000)]
progress
Claudio Sacerdoti Coen [Thu, 3 May 2012 19:26:39 +0000 (19:26 +0000)]
Speed up: moved a #ppterm inside the lazy it belongs to.
Wilmer Ricciotti [Thu, 3 May 2012 16:13:27 +0000 (16:13 +0000)]
progress in while test machine
Ferruccio Guidi [Thu, 3 May 2012 15:29:23 +0000 (15:29 +0000)]
additions in basic_2
Ferruccio Guidi [Thu, 3 May 2012 15:27:32 +0000 (15:27 +0000)]
- more properties on lifting, slicing, delifting and thinning
Andrea Asperti [Thu, 3 May 2012 09:30:27 +0000 (09:30 +0000)]
prod fin set
-
Andrea Asperti [Thu, 3 May 2012 08:08:19 +0000 (08:08 +0000)]
bool and segments of natural numbers
Wilmer Ricciotti [Wed, 2 May 2012 15:45:10 +0000 (15:45 +0000)]
While semantics.
Andrea Asperti [Wed, 2 May 2012 13:10:30 +0000 (13:10 +0000)]
split e merge
Andrea Asperti [Wed, 2 May 2012 12:00:00 +0000 (12:00 +0000)]
progress
-
Andrea Asperti [Wed, 2 May 2012 10:33:34 +0000 (10:33 +0000)]
while machine
Wilmer Ricciotti [Wed, 2 May 2012 10:33:18 +0000 (10:33 +0000)]
Added weak realizability.
Andrea Asperti [Wed, 2 May 2012 09:15:19 +0000 (09:15 +0000)]
Added wmono.
Wilmer Ricciotti [Mon, 30 Apr 2012 15:12:42 +0000 (15:12 +0000)]
More proofs in if-then-else machine.
Andrea Asperti [Mon, 30 Apr 2012 10:44:36 +0000 (10:44 +0000)]
Le configurazioni sono definite non su macchine ma su stati.
Idem per alcune funzioni di lift.
Andrea Asperti [Mon, 30 Apr 2012 09:29:09 +0000 (09:29 +0000)]
Definition of accRealize
Andrea Asperti [Mon, 30 Apr 2012 08:44:34 +0000 (08:44 +0000)]
If machine
Wilmer Ricciotti [Mon, 30 Apr 2012 07:16:17 +0000 (07:16 +0000)]
Monotape turing machines update.
Wilmer Ricciotti [Fri, 27 Apr 2012 16:42:29 +0000 (16:42 +0000)]
more loop proofs
Wilmer Ricciotti [Fri, 27 Apr 2012 15:20:22 +0000 (15:20 +0000)]
loop functions
Andrea Asperti [Fri, 27 Apr 2012 15:19:23 +0000 (15:19 +0000)]
loop functions
Andrea Asperti [Fri, 27 Apr 2012 11:47:09 +0000 (11:47 +0000)]
Mono tape turing machines
Andrea Asperti [Fri, 27 Apr 2012 11:46:07 +0000 (11:46 +0000)]
Extensions to finset (sum) and auxiliary lemmas.
Ferruccio Guidi [Thu, 26 Apr 2012 15:28:13 +0000 (15:28 +0000)]
- 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)