]>
matita.cs.unibo.it Git - helm.git/log
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.
Ferruccio Guidi [Thu, 25 Feb 2010 21:19:29 +0000 (21:19 +0000)]
-bugfix in the "profile" entry
Ferruccio Guidi [Thu, 25 Feb 2010 19:42:00 +0000 (19:42 +0000)]
- pipeline support for generated entities in text mode completed
Wilmer Ricciotti [Thu, 25 Feb 2010 12:42:56 +0000 (12:42 +0000)]
Minimal example in Z showing a problem in the nnormalize tactic.
Ferruccio Guidi [Wed, 24 Feb 2010 20:04:39 +0000 (20:04 +0000)]
- a couple of new entities
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)
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
Ferruccio Guidi [Sun, 21 Feb 2010 19:09:07 +0000 (19:09 +0000)]
- we added some syntactic sugar in the 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
Andrea Asperti [Fri, 19 Feb 2010 17:15:41 +0000 (17:15 +0000)]
Open goals fixed (it also returned closed goals).
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)
Andrea Asperti [Fri, 19 Feb 2010 07:45:40 +0000 (07:45 +0000)]
Removed debug printings.
Andrea Asperti [Fri, 19 Feb 2010 07:38:54 +0000 (07:38 +0000)]
added lazy
Andrea Asperti [Fri, 19 Feb 2010 07:36:11 +0000 (07:36 +0000)]
Nuova versione di auto.
Andrea Asperti [Fri, 19 Feb 2010 07:30:16 +0000 (07:30 +0000)]
New proofs.
Andrea Asperti [Fri, 19 Feb 2010 07:27:31 +0000 (07:27 +0000)]
Wilmer's stuff for destruct.
Andrea Asperti [Fri, 19 Feb 2010 07:25:04 +0000 (07:25 +0000)]
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.
Andrea Asperti [Tue, 16 Feb 2010 09:21:04 +0000 (09:21 +0000)]
More theorems
Andrea Asperti [Tue, 16 Feb 2010 07:34:33 +0000 (07:34 +0000)]
Minor fixings.
Claudio Sacerdoti Coen [Mon, 15 Feb 2010 12:41:44 +0000 (12:41 +0000)]
The height of fixpoint applications was not computed correctly.
Cosimo Oliboni [Fri, 12 Feb 2010 21:06:50 +0000 (21:06 +0000)]
cerco documentation
Enrico Tassi [Thu, 11 Feb 2010 10:34:32 +0000 (10:34 +0000)]
minimal sequent height set to 1
Enrico Tassi [Thu, 11 Feb 2010 09:49:47 +0000 (09:49 +0000)]
some experiment filtering with height
Andrea Asperti [Wed, 10 Feb 2010 09:23:29 +0000 (09:23 +0000)]
addenda
Andrea Asperti [Tue, 9 Feb 2010 07:20:55 +0000 (07:20 +0000)]
Added a count_occurrences function.
Andrea Asperti [Mon, 8 Feb 2010 07:26:18 +0000 (07:26 +0000)]
Bug fixing.
Andrea Asperti [Mon, 8 Feb 2010 07:25:32 +0000 (07:25 +0000)]
Removed debug printings.
Andrea Asperti [Mon, 8 Feb 2010 07:24:34 +0000 (07:24 +0000)]
Some changes towards integration of setoid-rewriting.
Cosimo Oliboni [Sat, 6 Feb 2010 13:13:17 +0000 (13:13 +0000)]
freescale porting
Cosimo Oliboni [Sat, 6 Feb 2010 10:30:51 +0000 (10:30 +0000)]
freescale porting
Cosimo Oliboni [Fri, 5 Feb 2010 07:43:09 +0000 (07:43 +0000)]
freescale porting
Claudio Sacerdoti Coen [Thu, 4 Feb 2010 13:31:41 +0000 (13:31 +0000)]
...
Andrea Asperti [Thu, 4 Feb 2010 11:23:52 +0000 (11:23 +0000)]
Added count_occurrences.
Type of does_not_occur corrected.
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.
Cosimo Oliboni [Thu, 4 Feb 2010 07:54:26 +0000 (07:54 +0000)]
freescale porting
Cosimo Oliboni [Thu, 4 Feb 2010 03:42:47 +0000 (03:42 +0000)]
freescale porting
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:14:47 +0000 (23:14 +0000)]
...
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 23:10:57 +0000 (23:10 +0000)]
End of curryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:58:49 +0000 (22:58 +0000)]
Curryfication of binary_morphisms.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:46:21 +0000 (22:46 +0000)]
Curryfication of binary setoids.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 22:03:37 +0000 (22:03 +0000)]
Curryfication of binary morphisms.
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.
Wilmer Ricciotti [Wed, 3 Feb 2010 17:00:36 +0000 (17:00 +0000)]
Disabled debug prints in ndestruct tactic.
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 17:00:11 +0000 (17:00 +0000)]
Debug code commented out.
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).
Claudio Sacerdoti Coen [Wed, 3 Feb 2010 16:00:33 +0000 (16:00 +0000)]
Bad variable name fixed.
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.
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.
Wilmer Ricciotti [Tue, 2 Feb 2010 18:50:29 +0000 (18:50 +0000)]
Added Streicher's K axiom.
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.
Cosimo Oliboni [Tue, 2 Feb 2010 08:38:57 +0000 (08:38 +0000)]
freescale porting
Andrea Asperti [Tue, 2 Feb 2010 08:33:37 +0000 (08:33 +0000)]
lists
Andrea Asperti [Tue, 2 Feb 2010 07:47:13 +0000 (07:47 +0000)]
Booleans
Andrea Asperti [Tue, 2 Feb 2010 07:46:03 +0000 (07:46 +0000)]
boolean arithmetics
Cosimo Oliboni [Tue, 2 Feb 2010 05:08:53 +0000 (05:08 +0000)]
freescale porting
Cosimo Oliboni [Mon, 1 Feb 2010 12:40:32 +0000 (12:40 +0000)]
Andrea Asperti [Mon, 1 Feb 2010 07:57:00 +0000 (07:57 +0000)]
minus
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.
Cosimo Oliboni [Sun, 31 Jan 2010 06:38:45 +0000 (06:38 +0000)]
freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 09:45:32 +0000 (09:45 +0000)]
freescale porting
Cosimo Oliboni [Sat, 30 Jan 2010 08:49:34 +0000 (08:49 +0000)]
freescale porting
Andrea Asperti [Fri, 29 Jan 2010 10:16:48 +0000 (10:16 +0000)]
minus in nat.ma
Andrea Asperti [Fri, 29 Jan 2010 10:16:03 +0000 (10:16 +0000)]
Nuova gestione della width.
Cosimo Oliboni [Fri, 29 Jan 2010 07:48:08 +0000 (07:48 +0000)]
freescale porting
Cosimo Oliboni [Thu, 28 Jan 2010 00:42:24 +0000 (00:42 +0000)]
freescale porting
Andrea Asperti [Wed, 27 Jan 2010 10:29:07 +0000 (10:29 +0000)]
le_arith
Andrea Asperti [Wed, 27 Jan 2010 09:04:31 +0000 (09:04 +0000)]
Unfolded exact letins during proof reconstruction.
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.
Cosimo Oliboni [Wed, 27 Jan 2010 06:39:00 +0000 (06:39 +0000)]
freescale porting
Andrea Asperti [Tue, 26 Jan 2010 09:20:14 +0000 (09:20 +0000)]
le_arith
Cosimo Oliboni [Mon, 25 Jan 2010 22:17:28 +0000 (22:17 +0000)]
freescale porting
Cosimo Oliboni [Mon, 25 Jan 2010 06:56:56 +0000 (06:56 +0000)]
freescale porting
Cosimo Oliboni [Sun, 24 Jan 2010 05:44:00 +0000 (05:44 +0000)]
freescale porting
Cosimo Oliboni [Sat, 23 Jan 2010 16:16:40 +0000 (16:16 +0000)]
Cosimo Oliboni [Sat, 23 Jan 2010 16:15:28 +0000 (16:15 +0000)]
Cosimo Oliboni [Fri, 22 Jan 2010 23:15:47 +0000 (23:15 +0000)]
freescale porting
Cosimo Oliboni [Fri, 22 Jan 2010 01:30:42 +0000 (01:30 +0000)]
freescale porting
Cosimo Oliboni [Thu, 21 Jan 2010 19:39:17 +0000 (19:39 +0000)]
Andrea Asperti [Thu, 21 Jan 2010 17:32:19 +0000 (17:32 +0000)]
Esempio
Cosimo Oliboni [Thu, 21 Jan 2010 11:49:45 +0000 (11:49 +0000)]
Cosimo Oliboni [Thu, 21 Jan 2010 02:16:45 +0000 (02:16 +0000)]
freescale porting, work in progress
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...
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:49:58 +0000 (12:49 +0000)]
More //.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:40:38 +0000 (12:40 +0000)]
More // everywhere.
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 12:00:31 +0000 (12:00 +0000)]
// used everywhere!
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 11:46:06 +0000 (11:46 +0000)]
// in place of nauto everywhere
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:39:40 +0000 (10:39 +0000)]
// is now more powerful
Claudio Sacerdoti Coen [Mon, 18 Jan 2010 10:34:24 +0000 (10:34 +0000)]
// is now more powerful
Andrea Asperti [Mon, 18 Jan 2010 10:04:51 +0000 (10:04 +0000)]
New paramod tac.
Andrea Asperti [Mon, 18 Jan 2010 09:59:04 +0000 (09:59 +0000)]
Invocation of paramod
Andrea Asperti [Mon, 18 Jan 2010 09:57:43 +0000 (09:57 +0000)]
paramod_tac exported
Andrea Asperti [Mon, 18 Jan 2010 09:51:57 +0000 (09:51 +0000)]
Number notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:51:09 +0000 (09:51 +0000)]
Number notation for NG
Andrea Asperti [Mon, 18 Jan 2010 09:50:06 +0000 (09:50 +0000)]
Number notation for NG.
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).
Andrea Asperti [Mon, 18 Jan 2010 07:23:03 +0000 (07:23 +0000)]
Updating.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:10:07 +0000 (17:10 +0000)]
A slightly more complicated example.
Claudio Sacerdoti Coen [Fri, 15 Jan 2010 17:06:45 +0000 (17:06 +0000)]
Finished!
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).