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

12 years agoadditions in basic_2
Ferruccio Guidi [Wed, 25 Apr 2012 16:05:54 +0000 (16:05 +0000)]
additions in basic_2

12 years ago- lambda_delta: bug fix in static type assignment
Ferruccio Guidi [Wed, 25 Apr 2012 15:54:27 +0000 (15:54 +0000)]
- lambda_delta: bug fix in static type assignment
                some theorems on delift and thin
- nat: eliminator for nat with "+1" rather than "S"

12 years agoUpdate to universal turing machine (preliminaries).
Wilmer Ricciotti [Tue, 24 Apr 2012 16:12:01 +0000 (16:12 +0000)]
Update to universal turing machine (preliminaries).

12 years agoMore turing machines (still not compiling)
Wilmer Ricciotti [Tue, 24 Apr 2012 12:35:49 +0000 (12:35 +0000)]
More turing machines (still not compiling)

12 years agoStarted converting informal definition of the machines to matita code
Wilmer Ricciotti [Tue, 24 Apr 2012 10:52:41 +0000 (10:52 +0000)]
Started converting informal definition of the machines to matita code
(currently not compiling).

12 years agoAdded universal turing machines (only comments for now).
Wilmer Ricciotti [Mon, 23 Apr 2012 11:33:11 +0000 (11:33 +0000)]
Added universal turing machines (only comments for now).

12 years agoadditions to basic_2
Ferruccio Guidi [Sat, 21 Apr 2012 13:27:53 +0000 (13:27 +0000)]
additions to basic_2

12 years ago- lambda_delta: static type assignment is defined
Ferruccio Guidi [Sat, 21 Apr 2012 13:20:21 +0000 (13:20 +0000)]
- lambda_delta: static type assignment is defined
- predefined_virtuals: some additions
- nat: we added a lemma

12 years ago- update in basic_2
Ferruccio Guidi [Thu, 19 Apr 2012 13:16:47 +0000 (13:16 +0000)]
- update in basic_2

12 years ago- firs theorems on native type assignment
Ferruccio Guidi [Thu, 19 Apr 2012 13:06:00 +0000 (13:06 +0000)]
- firs theorems on native type assignment
- we removed iterated unfold on local environments
  since transitivity of this unfold is not needed so far

12 years agoFixed w.r.t. new yelp.
Claudio Sacerdoti Coen [Tue, 17 Apr 2012 14:07:27 +0000 (14:07 +0000)]
Fixed w.r.t. new yelp.

12 years ago- milestone update in basic_2
Ferruccio Guidi [Mon, 16 Apr 2012 15:08:39 +0000 (15:08 +0000)]
- milestone update in basic_2
- html bugfix in hand written web pages

12 years ago- subject equivalence for atomic arity assignment completed!
Ferruccio Guidi [Mon, 16 Apr 2012 14:45:39 +0000 (14:45 +0000)]
- subject equivalence for atomic arity assignment completed!
- bug fix in partial unfold for local environments (nowthis relation
is confluent)

12 years agoDefinition of complexity
Andrea Asperti [Fri, 13 Apr 2012 10:24:39 +0000 (10:24 +0000)]
Definition of complexity

12 years agocommit by user ricciott
matitaweb [Tue, 10 Apr 2012 17:15:10 +0000 (17:15 +0000)]
commit by user ricciott

12 years agocommit by user
matitaweb [Tue, 10 Apr 2012 17:15:08 +0000 (17:15 +0000)]
commit by user

12 years agourgent partial commit ... to be fixed later ...
Ferruccio Guidi [Tue, 10 Apr 2012 13:50:40 +0000 (13:50 +0000)]
urgent partial commit ... to be fixed later ...

12 years agourgent partial commit ... to be fixed later ...
Ferruccio Guidi [Tue, 10 Apr 2012 13:48:26 +0000 (13:48 +0000)]
urgent partial commit ... to be fixed later ...

12 years agoupdate in basic_2
Ferruccio Guidi [Wed, 4 Apr 2012 18:52:03 +0000 (18:52 +0000)]
update in basic_2

12 years ago- some work on context equivalence of atomic arity assignment
Ferruccio Guidi [Wed, 4 Apr 2012 18:47:28 +0000 (18:47 +0000)]
- some work on context equivalence of atomic arity assignment

12 years agoAdded in basics
Andrea Asperti [Wed, 4 Apr 2012 07:28:38 +0000 (07:28 +0000)]
Added in basics
- vectors.ma
- finset.ma

Added turing

minor ntegrations in list,ma and listb.ma

12 years agoMinor changes
Andrea Asperti [Tue, 3 Apr 2012 15:36:09 +0000 (15:36 +0000)]
Minor changes

12 years agoMore changes to the website (matitaweb).
Wilmer Ricciotti [Tue, 3 Apr 2012 13:33:04 +0000 (13:33 +0000)]
More changes to the website (matitaweb).

12 years agoVarious updates to the (obsolete) website.
Wilmer Ricciotti [Tue, 3 Apr 2012 11:31:03 +0000 (11:31 +0000)]
Various updates to the (obsolete) website.