]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years agoFixed a bug in the unification, which prevented some reduction steps from being
Wilmer Ricciotti [Mon, 1 Mar 2010 18:07:54 +0000 (18:07 +0000)]
Fixed a bug in the unification, which prevented some reduction steps from being
performed in the case "match vs. match", when the types of the matching term
were not the same. The procedure used to always raise an Uncertain exception,
while in many cases the good choice would be to raise KeepReducing. This caused
the nnormalize tactic to fail with an error in some cases.

14 years ago-bugfix in the "profile" entry
Ferruccio Guidi [Thu, 25 Feb 2010 21:19:29 +0000 (21:19 +0000)]
-bugfix in the "profile" entry

14 years ago- pipeline support for generated entities in text mode completed
Ferruccio Guidi [Thu, 25 Feb 2010 19:42:00 +0000 (19:42 +0000)]
- pipeline support for generated entities in text mode completed

14 years agoMinimal example in Z showing a problem in the nnormalize tactic.
Wilmer Ricciotti [Thu, 25 Feb 2010 12:42:56 +0000 (12:42 +0000)]
Minimal example in Z showing a problem in the nnormalize tactic.

14 years ago- a couple of new entities
Ferruccio Guidi [Wed, 24 Feb 2010 20:04:39 +0000 (20:04 +0000)]
- a couple of new entities

14 years ago- the text model now supports invocations of the entity generator (to
Ferruccio Guidi [Tue, 23 Feb 2010 12:00:26 +0000 (12:00 +0000)]
- the text model now supports invocations of the entity generator (to
be implemented)
- the XML objects can be exported to a specified directory (via the -x
command line option)

14 years ago- we completed the text parser fixing the syntactic shortcuts
Ferruccio Guidi [Mon, 22 Feb 2010 18:53:10 +0000 (18:53 +0000)]
- we completed the text parser fixing the syntactic shortcuts
- we can now parse several files without loosing the status
- some imperative variables refactored

14 years ago- we added some syntactic sugar in the text parser
Ferruccio Guidi [Sun, 21 Feb 2010 19:09:07 +0000 (19:09 +0000)]
- we added some syntactic sugar in the text parser

14 years ago- we implemented the hierarchy and sort names declaration in text parser
Ferruccio Guidi [Sat, 20 Feb 2010 22:18:47 +0000 (22:18 +0000)]
- we implemented the hierarchy and sort names declaration in text parser
- we implemented a basic taxonomy for the entities in the text parser
- we fixed the visibility rules in the text-to-crg transformation
- we corrected a bug in the text-to-crg transformation (a continuation was not called)
- we removed the hierarchy parameter from the type checker status
- we created an directory with the examples we can typecheck
- we changed the semantics of the -r command-line option

14 years agoOpen goals fixed (it also returned closed goals).
Andrea Asperti [Fri, 19 Feb 2010 17:15:41 +0000 (17:15 +0000)]
Open goals fixed (it also returned closed goals).

14 years ago- we added a parser for lambda-delta textual syntax (file extension .hln)
Ferruccio Guidi [Fri, 19 Feb 2010 16:27:17 +0000 (16:27 +0000)]
- we added a parser for lambda-delta textual syntax (file extension .hln)
- we now parse the input files with a straming policy
- we added a Meta attribute for explanatory metalinguistic comments
- brg: missing type casts were not inserted (fixed)

14 years agoRemoved debug printings.
Andrea Asperti [Fri, 19 Feb 2010 07:45:40 +0000 (07:45 +0000)]
Removed debug printings.

14 years agoadded lazy
Andrea Asperti [Fri, 19 Feb 2010 07:38:54 +0000 (07:38 +0000)]
added lazy

14 years agoNuova versione di auto.
Andrea Asperti [Fri, 19 Feb 2010 07:36:11 +0000 (07:36 +0000)]
Nuova versione di auto.

14 years agoNew proofs.
Andrea Asperti [Fri, 19 Feb 2010 07:30:16 +0000 (07:30 +0000)]
New proofs.

14 years agoWilmer's stuff for destruct.
Andrea Asperti [Fri, 19 Feb 2010 07:27:31 +0000 (07:27 +0000)]
Wilmer's stuff for destruct.

14 years ago(no commit message)
Andrea Asperti [Fri, 19 Feb 2010 07:25:04 +0000 (07:25 +0000)]

14 years agoAdded an implicit parameter to branch_tac to allow branching on a
Andrea Asperti [Fri, 19 Feb 2010 07:19:01 +0000 (07:19 +0000)]
Added an implicit parameter to branch_tac to allow branching on a
single goal.

14 years agoMore theorems
Andrea Asperti [Tue, 16 Feb 2010 09:21:04 +0000 (09:21 +0000)]
More theorems

14 years agoMinor fixings.
Andrea Asperti [Tue, 16 Feb 2010 07:34:33 +0000 (07:34 +0000)]
Minor fixings.

14 years agoThe height of fixpoint applications was not computed correctly.
Claudio Sacerdoti Coen [Mon, 15 Feb 2010 12:41:44 +0000 (12:41 +0000)]
The height of fixpoint applications was not computed correctly.

14 years ago cerco documentation
Cosimo Oliboni [Fri, 12 Feb 2010 21:06:50 +0000 (21:06 +0000)]
 cerco documentation

14 years agominimal sequent height set to 1
Enrico Tassi [Thu, 11 Feb 2010 10:34:32 +0000 (10:34 +0000)]
minimal sequent height set to 1

14 years agosome experiment filtering with height
Enrico Tassi [Thu, 11 Feb 2010 09:49:47 +0000 (09:49 +0000)]
some experiment filtering with height

14 years agoaddenda
Andrea Asperti [Wed, 10 Feb 2010 09:23:29 +0000 (09:23 +0000)]
addenda

14 years agoAdded a count_occurrences function.
Andrea Asperti [Tue, 9 Feb 2010 07:20:55 +0000 (07:20 +0000)]
Added a count_occurrences function.

14 years agoBug fixing.
Andrea Asperti [Mon, 8 Feb 2010 07:26:18 +0000 (07:26 +0000)]
Bug fixing.

14 years agoRemoved debug printings.
Andrea Asperti [Mon, 8 Feb 2010 07:25:32 +0000 (07:25 +0000)]
Removed debug printings.

14 years agoSome changes towards integration of setoid-rewriting.
Andrea Asperti [Mon, 8 Feb 2010 07:24:34 +0000 (07:24 +0000)]
Some changes towards integration of setoid-rewriting.

14 years ago freescale porting
Cosimo Oliboni [Sat, 6 Feb 2010 13:13:17 +0000 (13:13 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 6 Feb 2010 10:30:51 +0000 (10:30 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Fri, 5 Feb 2010 07:43:09 +0000 (07:43 +0000)]
 freescale porting

14 years ago...
Claudio Sacerdoti Coen [Thu, 4 Feb 2010 13:31:41 +0000 (13:31 +0000)]
...

14 years agoAdded count_occurrences.
Andrea Asperti [Thu, 4 Feb 2010 11:23:52 +0000 (11:23 +0000)]
Added count_occurrences.
Type of does_not_occur corrected.

14 years agoBug fixed: goto_top used to reset the status to the first one and then
Andrea Asperti [Thu, 4 Feb 2010 10:32:30 +0000 (10:32 +0000)]
Bug fixed: goto_top used to reset the status to the first one and then
reset_buffer (re-implemented yesterday) used to do the time travel
again. Fixed by getting rid of goto_top.

Note: the old implementation was slightly more efficient since the
initial notation of Matita was not re-loaded every time you go back to
top. In practice, this does not seem to matter.

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 07:54:26 +0000 (07:54 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 03:42:47 +0000 (03:42 +0000)]
 freescale porting

14 years ago...
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:14:47 +0000 (23:14 +0000)]
...

14 years agoEnd of curryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:10:57 +0000 (23:10 +0000)]
End of curryfication of binary_morphisms.

14 years agoCurryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:58:49 +0000 (22:58 +0000)]
Curryfication of binary_morphisms.

14 years agoCurryfication of binary setoids.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:46:21 +0000 (22:46 +0000)]
Curryfication of binary setoids.

14 years agoCurryfication of binary morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:03:37 +0000 (22:03 +0000)]
Curryfication of binary morphisms.

14 years agoWork in Progress: Who needs binary_morphisms? Curryfication is your friend.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 20:03:57 +0000 (20:03 +0000)]
Work in Progress: Who needs binary_morphisms? Curryfication is your friend.

But...

 1) the hints are uglier
 2) you really need to apply mk_binary_morphism to prove a curryfied binary
    morphism if you want to remain sane...

Note: with non uniform coercions everywhere we should be able to finally get
a beautiful script. Yet to be done.

14 years agoDisabled debug prints in ndestruct tactic.
Wilmer Ricciotti [Wed, 3 Feb 2010 17:00:36 +0000 (17:00 +0000)]
Disabled debug prints in ndestruct tactic.

14 years agoDebug code commented out.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 17:00:11 +0000 (17:00 +0000)]
Debug code commented out.

14 years agoParts of the status were not re-initialized correctly during a reset.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 16:56:57 +0000 (16:56 +0000)]
Parts of the status were not re-initialized correctly during a reset.
Fixed (and bugs avoided).

14 years agoBad variable name fixed.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 16:00:33 +0000 (16:00 +0000)]
Bad variable name fixed.

14 years agoBug fixed: projection redexes obtained reducing other projection redexes were
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 15:41:02 +0000 (15:41 +0000)]
Bug fixed: projection redexes obtained reducing other projection redexes were
not reduced.

14 years agoNew version using Streicher's K axiom. Should be faster and also work with
Wilmer Ricciotti [Tue, 2 Feb 2010 18:52:12 +0000 (18:52 +0000)]
New version using Streicher's K axiom. Should be faster and also work with
indexed inductive types.

14 years agoAdded Streicher's K axiom.
Wilmer Ricciotti [Tue, 2 Feb 2010 18:50:29 +0000 (18:50 +0000)]
Added Streicher's K axiom.

14 years agoFixed a bug with indexed inductive types which sometimes prevented the
Wilmer Ricciotti [Tue, 2 Feb 2010 13:39:54 +0000 (13:39 +0000)]
Fixed a bug with indexed inductive types which sometimes prevented the
inversion principles from being defined.

14 years ago freescale porting
Cosimo Oliboni [Tue, 2 Feb 2010 08:38:57 +0000 (08:38 +0000)]
 freescale porting

14 years agolists
Andrea Asperti [Tue, 2 Feb 2010 08:33:37 +0000 (08:33 +0000)]
lists

14 years agoBooleans
Andrea Asperti [Tue, 2 Feb 2010 07:47:13 +0000 (07:47 +0000)]
Booleans

14 years agoboolean arithmetics
Andrea Asperti [Tue, 2 Feb 2010 07:46:03 +0000 (07:46 +0000)]
boolean arithmetics

14 years ago freescale porting
Cosimo Oliboni [Tue, 2 Feb 2010 05:08:53 +0000 (05:08 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Mon, 1 Feb 2010 12:40:32 +0000 (12:40 +0000)]

14 years agominus
Andrea Asperti [Mon, 1 Feb 2010 07:57:00 +0000 (07:57 +0000)]
minus

14 years agoOn the last goal at maxdepth we stop at the first solution.
Andrea Asperti [Mon, 1 Feb 2010 07:54:35 +0000 (07:54 +0000)]
On the last goal at maxdepth we stop at the first solution.

14 years ago freescale porting
Cosimo Oliboni [Sun, 31 Jan 2010 06:38:45 +0000 (06:38 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 09:45:32 +0000 (09:45 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 08:49:34 +0000 (08:49 +0000)]
 freescale porting

14 years agominus in nat.ma
Andrea Asperti [Fri, 29 Jan 2010 10:16:48 +0000 (10:16 +0000)]
minus in nat.ma

14 years agoNuova gestione della width.
Andrea Asperti [Fri, 29 Jan 2010 10:16:03 +0000 (10:16 +0000)]
Nuova gestione della width.

14 years ago freescale porting
Cosimo Oliboni [Fri, 29 Jan 2010 07:48:08 +0000 (07:48 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Thu, 28 Jan 2010 00:42:24 +0000 (00:42 +0000)]
 freescale porting

14 years agole_arith
Andrea Asperti [Wed, 27 Jan 2010 10:29:07 +0000 (10:29 +0000)]
le_arith

14 years agoUnfolded exact letins during proof reconstruction.
Andrea Asperti [Wed, 27 Jan 2010 09:04:31 +0000 (09:04 +0000)]
Unfolded exact letins during proof reconstruction.

14 years agoAdded a parameter no_implicit (default true) to choose between raising
Andrea Asperti [Wed, 27 Jan 2010 08:47:27 +0000 (08:47 +0000)]
Added a parameter no_implicit (default true) to choose between raising
assert false or returning the identity.

14 years ago freescale porting
Cosimo Oliboni [Wed, 27 Jan 2010 06:39:00 +0000 (06:39 +0000)]
 freescale porting

14 years agole_arith
Andrea Asperti [Tue, 26 Jan 2010 09:20:14 +0000 (09:20 +0000)]
le_arith

14 years ago freescale porting
Cosimo Oliboni [Mon, 25 Jan 2010 22:17:28 +0000 (22:17 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Mon, 25 Jan 2010 06:56:56 +0000 (06:56 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Sun, 24 Jan 2010 05:44:00 +0000 (05:44 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Sat, 23 Jan 2010 16:16:40 +0000 (16:16 +0000)]

14 years ago(no commit message)
Cosimo Oliboni [Sat, 23 Jan 2010 16:15:28 +0000 (16:15 +0000)]

14 years ago freescale porting
Cosimo Oliboni [Fri, 22 Jan 2010 23:15:47 +0000 (23:15 +0000)]
 freescale porting

14 years ago freescale porting
Cosimo Oliboni [Fri, 22 Jan 2010 01:30:42 +0000 (01:30 +0000)]
 freescale porting

14 years ago(no commit message)
Cosimo Oliboni [Thu, 21 Jan 2010 19:39:17 +0000 (19:39 +0000)]

14 years agoEsempio
Andrea Asperti [Thu, 21 Jan 2010 17:32:19 +0000 (17:32 +0000)]
Esempio

14 years ago(no commit message)
Cosimo Oliboni [Thu, 21 Jan 2010 11:49:45 +0000 (11:49 +0000)]

14 years ago freescale porting, work in progress
Cosimo Oliboni [Thu, 21 Jan 2010 02:16:45 +0000 (02:16 +0000)]
 freescale porting, work in progress

14 years agoWe can always use the "covered by emptyset" relation...
Claudio Sacerdoti Coen [Tue, 19 Jan 2010 12:52:53 +0000 (12:52 +0000)]
We can always use the "covered by emptyset" relation...
Closer and closer to Bove-Capretta, but more and more far away from IGFT...

14 years agoMore //.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:49:58 +0000 (12:49 +0000)]
More //.

14 years agoMore // everywhere.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:40:38 +0000 (12:40 +0000)]
More // everywhere.

14 years ago// used everywhere!
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:00:31 +0000 (12:00 +0000)]
// used everywhere!

14 years ago// in place of nauto everywhere
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 11:46:06 +0000 (11:46 +0000)]
// in place of nauto everywhere

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:39:40 +0000 (10:39 +0000)]
// is now more powerful

14 years ago// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:34:24 +0000 (10:34 +0000)]
// is now more powerful

14 years agoNew paramod tac.
Andrea Asperti [Mon, 18 Jan 2010 10:04:51 +0000 (10:04 +0000)]
New paramod tac.

14 years agoInvocation of paramod
Andrea Asperti [Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)]
Invocation of paramod

14 years agoparamod_tac exported
Andrea Asperti [Mon, 18 Jan 2010 09:57:43 +0000 (09:57 +0000)]
paramod_tac exported

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:57 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:09 +0000 (09:51 +0000)]
Number notation for NG

14 years agoNumber notation for NG.
Andrea Asperti [Mon, 18 Jan 2010 09:50:06 +0000 (09:50 +0000)]
Number notation for NG.

14 years agoKeeping Implicit for refinement (instead of transforming them to Metas:
Andrea Asperti [Mon, 18 Jan 2010 07:25:27 +0000 (07:25 +0000)]
Keeping Implicit for refinement (instead of transforming them to Metas:
context bug).

14 years agoUpdating.
Andrea Asperti [Mon, 18 Jan 2010 07:23:03 +0000 (07:23 +0000)]
Updating.

14 years agoA slightly more complicated example.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:10:07 +0000 (17:10 +0000)]
A slightly more complicated example.

14 years agoFinished!
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:06:45 +0000 (17:06 +0000)]
Finished!

14 years agoWe are still equivalent (even if the definition of ncover is obfuscated).
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 16:15:09 +0000 (16:15 +0000)]
We are still equivalent (even if the definition of ncover is obfuscated).