]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

12 years agoProgress.
Wilmer Ricciotti [Thu, 10 May 2012 15:49:45 +0000 (15:49 +0000)]
Progress.

12 years agoPatch to improve the pretty-printing of error messages.
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).

12 years agoadditions to basic_2
Ferruccio Guidi [Thu, 10 May 2012 11:06:02 +0000 (11:06 +0000)]
additions to basic_2

12 years ago- lib: some additions
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

12 years agoSys.Break no longer captured in two places.
Claudio Sacerdoti Coen [Thu, 10 May 2012 08:11:13 +0000 (08:11 +0000)]
Sys.Break no longer captured in two places.

12 years agoaxiomatization of acc_if
Andrea Asperti [Thu, 10 May 2012 07:38:44 +0000 (07:38 +0000)]
axiomatization of acc_if

12 years agoProgress.
Wilmer Ricciotti [Wed, 9 May 2012 16:49:50 +0000 (16:49 +0000)]
Progress.

12 years agoProgress in compare.ma (some machines have been moved to tests.ma and marks.ma)
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)

12 years agoprogress in turing/universal/compare.ma
Wilmer Ricciotti [Tue, 8 May 2012 16:09:32 +0000 (16:09 +0000)]
progress in turing/universal/compare.ma

12 years agoAdded compare auxiliary machine for universal turing machine.
Wilmer Ricciotti [Tue, 8 May 2012 09:56:46 +0000 (09:56 +0000)]
Added compare auxiliary machine for universal turing machine.

12 years agoprogress
Wilmer Ricciotti [Mon, 7 May 2012 15:34:16 +0000 (15:34 +0000)]
progress

12 years agoProve di terminazione
Andrea Asperti [Mon, 7 May 2012 13:13:32 +0000 (13:13 +0000)]
Prove di terminazione

12 years agoMore examples
Andrea Asperti [Mon, 7 May 2012 06:28:47 +0000 (06:28 +0000)]
More examples

12 years agostarl
Andrea Asperti [Mon, 7 May 2012 06:26:54 +0000 (06:26 +0000)]
starl

12 years agoForgotten in previous commit: move_char machines.
Wilmer Ricciotti [Fri, 4 May 2012 16:58:11 +0000 (16:58 +0000)]
Forgotten in previous commit: move_char machines.

12 years ago(no commit message)
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:16:39 +0000 (15:16 +0000)]

12 years ago(no commit message)
Claudio Sacerdoti Coen [Fri, 4 May 2012 15:14:44 +0000 (15:14 +0000)]

12 years agoAdded a turing/universal directory for the universal turing machine (and
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.

12 years agoprogress
Wilmer Ricciotti [Fri, 4 May 2012 12:04:18 +0000 (12:04 +0000)]
progress

12 years agoSpeed up: moved a #ppterm inside the lazy it belongs to.
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.

12 years agoprogress in while test machine
Wilmer Ricciotti [Thu, 3 May 2012 16:13:27 +0000 (16:13 +0000)]
progress in while test machine

12 years agoadditions in basic_2
Ferruccio Guidi [Thu, 3 May 2012 15:29:23 +0000 (15:29 +0000)]
additions in basic_2

12 years ago- more properties on lifting, slicing, delifting and thinning
Ferruccio Guidi [Thu, 3 May 2012 15:27:32 +0000 (15:27 +0000)]
- more properties on lifting, slicing, delifting and thinning

12 years agoprod fin set
Andrea Asperti [Thu, 3 May 2012 09:30:27 +0000 (09:30 +0000)]
prod fin set
-

12 years agobool and segments of natural numbers
Andrea Asperti [Thu, 3 May 2012 08:08:19 +0000 (08:08 +0000)]
bool and segments of natural numbers

12 years agoWhile semantics.
Wilmer Ricciotti [Wed, 2 May 2012 15:45:10 +0000 (15:45 +0000)]
While semantics.

12 years agosplit e merge
Andrea Asperti [Wed, 2 May 2012 13:10:30 +0000 (13:10 +0000)]
split e merge

12 years agoprogress
Andrea Asperti [Wed, 2 May 2012 12:00:00 +0000 (12:00 +0000)]
progress
-

12 years agowhile machine
Andrea Asperti [Wed, 2 May 2012 10:33:34 +0000 (10:33 +0000)]
while machine

12 years agoAdded weak realizability.
Wilmer Ricciotti [Wed, 2 May 2012 10:33:18 +0000 (10:33 +0000)]
Added weak realizability.

12 years agoAdded wmono.
Andrea Asperti [Wed, 2 May 2012 09:15:19 +0000 (09:15 +0000)]
Added wmono.

12 years agoMore proofs in if-then-else machine.
Wilmer Ricciotti [Mon, 30 Apr 2012 15:12:42 +0000 (15:12 +0000)]
More proofs in if-then-else machine.

12 years agoLe configurazioni sono definite non su macchine ma su stati.
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.

12 years agoDefinition of accRealize
Andrea Asperti [Mon, 30 Apr 2012 09:29:09 +0000 (09:29 +0000)]
Definition of accRealize

12 years agoIf machine
Andrea Asperti [Mon, 30 Apr 2012 08:44:34 +0000 (08:44 +0000)]
If machine

12 years agoMonotape turing machines update.
Wilmer Ricciotti [Mon, 30 Apr 2012 07:16:17 +0000 (07:16 +0000)]
Monotape turing machines update.

12 years agomore loop proofs
Wilmer Ricciotti [Fri, 27 Apr 2012 16:42:29 +0000 (16:42 +0000)]
more loop proofs

12 years agoloop functions
Wilmer Ricciotti [Fri, 27 Apr 2012 15:20:22 +0000 (15:20 +0000)]
loop functions

12 years agoloop functions
Andrea Asperti [Fri, 27 Apr 2012 15:19:23 +0000 (15:19 +0000)]
loop functions

12 years agoMono tape turing machines
Andrea Asperti [Fri, 27 Apr 2012 11:47:09 +0000 (11:47 +0000)]
Mono tape turing machines

12 years agoExtensions to finset (sum) and auxiliary lemmas.
Andrea Asperti [Fri, 27 Apr 2012 11:46:07 +0000 (11:46 +0000)]
Extensions to finset (sum) and auxiliary lemmas.

12 years ago- notation (possibly affecting all .ma files):
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)