]> matita.cs.unibo.it Git - helm.git/log
helm.git
14 years agonow we take the NUri module from the helm-ng_kernel packeage
Ferruccio Guidi [Fri, 6 Aug 2010 11:27:18 +0000 (11:27 +0000)]
now we take the NUri module from the helm-ng_kernel packeage

14 years agothe refactoring continues
Ferruccio Guidi [Fri, 6 Aug 2010 10:57:42 +0000 (10:57 +0000)]
the refactoring continues

14 years agorefactoring: helena sources are now in a dedicated directory
Ferruccio Guidi [Fri, 6 Aug 2010 10:52:43 +0000 (10:52 +0000)]
refactoring: helena sources are now in a dedicated directory

14 years agotxtLexer: bug fix in parsing the string tokens
Ferruccio Guidi [Fri, 6 Aug 2010 10:21:49 +0000 (10:21 +0000)]
txtLexer: bug fix in parsing the string tokens
library: we now export the "meta" attribute
crgXml: crg exportation factorized and alpha conversion now works
crgBrg: we now mark the abstraction and the reverse translation works
ld.dtd: updated to export crg contents

14 years ago- we simplified the parser return values
Ferruccio Guidi [Tue, 3 Aug 2010 20:54:58 +0000 (20:54 +0000)]
- we simplified the parser return values
- now the display of parser and lexer debug information is controlled
from the command line (with the options -P and -L)
complete_rg: now the empty binders are not treated especially
top: we isolated a fragment of slow code (process_streaming) to be
investigated. It can be enabled with the -1 command line option)
Makefile: we now create the etc directory when it is missing

14 years agoBug fixed: nodes were copied.
Claudio Sacerdoti Coen [Thu, 29 Jul 2010 15:27:13 +0000 (15:27 +0000)]
Bug fixed: nodes were copied.

14 years agointerpret non ambiguous symbols ASAP
Enrico Tassi [Thu, 29 Jul 2010 15:09:38 +0000 (15:09 +0000)]
interpret non ambiguous symbols ASAP

14 years ago...
Enrico Tassi [Wed, 28 Jul 2010 16:44:03 +0000 (16:44 +0000)]
...

14 years agoallows auto before eq is defined
Enrico Tassi [Wed, 28 Jul 2010 16:43:39 +0000 (16:43 +0000)]
allows auto before eq is defined

14 years ago...
Claudio Sacerdoti Coen [Wed, 28 Jul 2010 16:14:53 +0000 (16:14 +0000)]
...

14 years agoFixes unexpected behaviour of ncut when multiple goals are selected.
Wilmer Ricciotti [Wed, 28 Jul 2010 15:45:04 +0000 (15:45 +0000)]
Fixes unexpected behaviour of ncut when multiple goals are selected.

14 years agoExperimental enhancements to the ndestruct tactic. By using the syntax
Wilmer Ricciotti [Wed, 28 Jul 2010 15:44:09 +0000 (15:44 +0000)]
Experimental enhancements to the ndestruct tactic. By using the syntax

ndestruct (e1 ... em) skip (H1 ... Hn)

the user can tell the tactic that
- only equations e1 ... em should be considered
- rewriting should happen only in hypotheses H1 ... Hn and in the goal

both "(e1 ... em)" and "skip (H1 ... Hn)" are optional parameters.

14 years agoSome experiments on a co-inductive Heityng algebra.
Claudio Sacerdoti Coen [Fri, 23 Jul 2010 09:25:06 +0000 (09:25 +0000)]
Some experiments on a co-inductive Heityng algebra.

14 years ago...
Enrico Tassi [Thu, 22 Jul 2010 08:11:22 +0000 (08:11 +0000)]
...

14 years agosome work on \exists
Enrico Tassi [Thu, 22 Jul 2010 08:05:23 +0000 (08:05 +0000)]
some work on \exists

14 years agoeq -> eq0 renaming
Enrico Tassi [Thu, 22 Jul 2010 08:05:08 +0000 (08:05 +0000)]
eq -> eq0 renaming

14 years agouseless box removed
Enrico Tassi [Thu, 22 Jul 2010 08:04:43 +0000 (08:04 +0000)]
useless box removed

14 years agofixed precedence so that no () are needed around variable assignement
Enrico Tassi [Thu, 22 Jul 2010 08:04:19 +0000 (08:04 +0000)]
fixed precedence so that no () are needed around variable assignement

14 years agodo not apply hints if metaclosed
Enrico Tassi [Thu, 22 Jul 2010 08:03:45 +0000 (08:03 +0000)]
do not apply hints if metaclosed

14 years agoavoid assert false, just fail generating the coercion
Enrico Tassi [Thu, 22 Jul 2010 08:03:17 +0000 (08:03 +0000)]
avoid assert false, just fail generating the coercion

14 years ago...
Enrico Tassi [Wed, 21 Jul 2010 15:46:33 +0000 (15:46 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 21 Jul 2010 15:34:49 +0000 (15:34 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 21 Jul 2010 08:54:04 +0000 (08:54 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 21 Jul 2010 08:05:59 +0000 (08:05 +0000)]
...

14 years agonew icons for the lambda-delta web site
Ferruccio Guidi [Tue, 20 Jul 2010 16:15:22 +0000 (16:15 +0000)]
new icons for the lambda-delta web site

14 years agocompleted lemma 17
Enrico Tassi [Tue, 20 Jul 2010 12:43:19 +0000 (12:43 +0000)]
completed lemma 17

14 years ago...
Enrico Tassi [Mon, 19 Jul 2010 09:29:50 +0000 (09:29 +0000)]
...

14 years agore 16.4 almost done
Enrico Tassi [Thu, 15 Jul 2010 16:16:50 +0000 (16:16 +0000)]
re 16.4 almost done

14 years agobig mess of notation
Enrico Tassi [Sat, 10 Jul 2010 16:29:47 +0000 (16:29 +0000)]
big mess of notation

14 years agomore notation
Enrico Tassi [Fri, 9 Jul 2010 12:43:33 +0000 (12:43 +0000)]
more notation

14 years agomoved formal_topology into library"
Enrico Tassi [Wed, 7 Jul 2010 16:08:18 +0000 (16:08 +0000)]
moved formal_topology into library"

14 years agosome notation for map_arrows2
Enrico Tassi [Tue, 6 Jul 2010 10:42:33 +0000 (10:42 +0000)]
some notation for map_arrows2

14 years ago...
Claudio Sacerdoti Coen [Sun, 4 Jul 2010 18:48:10 +0000 (18:48 +0000)]
...

14 years agoSome important proofs/definitions were (and are still) commented out and
Claudio Sacerdoti Coen [Sun, 4 Jul 2010 11:24:14 +0000 (11:24 +0000)]
Some important proofs/definitions were (and are still) commented out and
do not compile.

Added the notion of functor1 to state the main theorem.

14 years agoProof simplified.
Claudio Sacerdoti Coen [Thu, 1 Jul 2010 22:01:36 +0000 (22:01 +0000)]
Proof simplified.

14 years agoProof simplified (??).
Claudio Sacerdoti Coen [Thu, 1 Jul 2010 21:38:32 +0000 (21:38 +0000)]
Proof simplified (??).

14 years ago...
Enrico Tassi [Thu, 1 Jul 2010 16:52:00 +0000 (16:52 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 30 Jun 2010 20:33:43 +0000 (20:33 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 30 Jun 2010 14:10:39 +0000 (14:10 +0000)]
...

14 years ago...
Enrico Tassi [Wed, 30 Jun 2010 13:29:50 +0000 (13:29 +0000)]
...

14 years ago....
Enrico Tassi [Wed, 30 Jun 2010 09:44:22 +0000 (09:44 +0000)]
....

14 years ago...
Enrico Tassi [Tue, 29 Jun 2010 14:03:40 +0000 (14:03 +0000)]
...

14 years agonotation made half decent
Enrico Tassi [Tue, 29 Jun 2010 12:07:37 +0000 (12:07 +0000)]
notation made half decent

14 years agobetter notation for oalgebra
Enrico Tassi [Mon, 28 Jun 2010 20:15:28 +0000 (20:15 +0000)]
better notation for oalgebra

14 years ago....
Enrico Tassi [Fri, 18 Jun 2010 11:11:43 +0000 (11:11 +0000)]
....

14 years agooff by one fixed
Enrico Tassi [Thu, 17 Jun 2010 21:41:00 +0000 (21:41 +0000)]
off by one fixed

14 years agoFix for inversion principles of types with a single constructor.
Wilmer Ricciotti [Thu, 10 Jun 2010 18:23:59 +0000 (18:23 +0000)]
Fix for inversion principles of types with a single constructor.

14 years agoFixed a bug in the undebruijnate function which caused the refiner to produce
Wilmer Ricciotti [Tue, 8 Jun 2010 16:15:14 +0000 (16:15 +0000)]
Fixed a bug in the undebruijnate function which caused the refiner to produce
a wrong object when refining mutually recursive functions (the references to
recursive calls would contain the wrong index to the recursive argument).

14 years agosome stuff on re
Enrico Tassi [Mon, 7 Jun 2010 22:56:03 +0000 (22:56 +0000)]
some stuff on re

14 years agounify left args of inductive types with left argus of constructors. this allows
Enrico Tassi [Mon, 7 Jun 2010 22:55:47 +0000 (22:55 +0000)]
unify left args of inductive types with left argus of constructors. this allows
to put ? in every left arg of every constructor of an inductive type.

14 years agoLibrary support files for John Major equality and Russell.
Wilmer Ricciotti [Wed, 12 May 2010 18:41:47 +0000 (18:41 +0000)]
Library support files for John Major equality and Russell.

14 years agoExperimental support for Russell (coercions moving inside lambda & pattern
Wilmer Ricciotti [Wed, 12 May 2010 18:39:05 +0000 (18:39 +0000)]
Experimental support for Russell (coercions moving inside lambda & pattern
matching etc.) added to the refiner.

14 years agominimization.ma
Andrea Asperti [Tue, 11 May 2010 08:50:33 +0000 (08:50 +0000)]
minimization.ma

14 years agolittle workaround for multiple screens, gdk support not bound by lablgtk2
Enrico Tassi [Tue, 11 May 2010 07:21:34 +0000 (07:21 +0000)]
little workaround for multiple screens, gdk support not bound by lablgtk2

14 years agonew intro:
Enrico Tassi [Mon, 10 May 2010 09:48:33 +0000 (09:48 +0000)]
new intro:
- #; -- introduces into the context every possible assumption giving
        to it an unusable name
- #h1 .. h2; -- multi intros
- intros; -- macro che espande a #h1...hn.

14 years agotrace generation with "// by _;"
Enrico Tassi [Fri, 7 May 2010 21:21:01 +0000 (21:21 +0000)]
trace generation with "// by _;"

14 years agonotation
Enrico Tassi [Fri, 7 May 2010 21:20:58 +0000 (21:20 +0000)]
notation

14 years agoremarks and applyS
Andrea Asperti [Fri, 7 May 2010 10:04:00 +0000 (10:04 +0000)]
remarks and applyS

14 years agoBug fixed: nstatus => status (to undo the changes).
Claudio Sacerdoti Coen [Thu, 6 May 2010 22:35:02 +0000 (22:35 +0000)]
Bug fixed: nstatus => status (to undo the changes).

Worring warnings commented out.

14 years ago...
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:52:38 +0000 (15:52 +0000)]
...

14 years agoFixing naming scheme for composite coercions.
Wilmer Ricciotti [Thu, 6 May 2010 15:50:07 +0000 (15:50 +0000)]
Fixing naming scheme for composite coercions.

14 years agoassert false could happen
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:45:35 +0000 (15:45 +0000)]
assert false could happen

14 years agoBug fixed:
Claudio Sacerdoti Coen [Thu, 6 May 2010 15:15:46 +0000 (15:15 +0000)]
Bug fixed:

 During unification of E1 with E2, E1 and E2 where not always reduced.
 In particular, reduction was not performed in the cases:
   LetIn vs LetIn, Match vs Match
 and maybe also in some cases Appl Meta vs Appl Meta (who knows?)

14 years agocoinduction is between us
Claudio Sacerdoti Coen [Wed, 5 May 2010 15:13:41 +0000 (15:13 +0000)]
coinduction is between us

14 years agoFirst tests.
Claudio Sacerdoti Coen [Wed, 5 May 2010 14:29:57 +0000 (14:29 +0000)]
First tests.

14 years ago* Fixed a couple of glitches in ndestruct
Wilmer Ricciotti [Tue, 4 May 2010 16:49:59 +0000 (16:49 +0000)]
* Fixed a couple of glitches in ndestruct
  - blob equations were not always handled properly
  - tactic used to fail due to not optimal behaviour of the refiner
* Added (experimental) support for JM equality to ndestruct

14 years agoRegular expressions.
Claudio Sacerdoti Coen [Tue, 4 May 2010 16:40:26 +0000 (16:40 +0000)]
Regular expressions.

14 years agonew dependences
Ferruccio Guidi [Wed, 21 Apr 2010 09:00:04 +0000 (09:00 +0000)]
new dependences

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoElimination of recursive inductive types leads to looping.
Andrea Asperti [Mon, 19 Apr 2010 09:47:02 +0000 (09:47 +0000)]
Elimination of recursive inductive types leads to looping.
ELimnation of singleton types gives problems with negation.

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoalpha_eq instead of pervasives.compare
Andrea Asperti [Mon, 19 Apr 2010 09:44:21 +0000 (09:44 +0000)]
alpha_eq instead of pervasives.compare

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agobool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
Enrico Tassi [Thu, 15 Apr 2010 14:02:02 +0000 (14:02 +0000)]
bool_ext on 'o' not on 'Prop' (they are convertible, but discrimination
trees do not compare up to conversion)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 15:47:51 +0000 (15:47 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 14:06:35 +0000 (14:06 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFormal points.
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:42:14 +0000 (13:42 +0000)]
Formal points.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoSome dualization clean-up.
Claudio Sacerdoti Coen [Wed, 14 Apr 2010 13:28:53 +0000 (13:28 +0000)]
Some dualization clean-up.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed makefile
Enrico Tassi [Tue, 13 Apr 2010 19:56:18 +0000 (19:56 +0000)]
fixed makefile

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoauto destructs while introducing in the context
Enrico Tassi [Tue, 13 Apr 2010 19:55:18 +0000 (19:55 +0000)]
auto destructs while introducing in the context

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoprint nobjects (hack with Obj.magic)
Enrico Tassi [Tue, 13 Apr 2010 19:54:23 +0000 (19:54 +0000)]
print nobjects (hack with Obj.magic)

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agocatch the right exception, avoid uncaught Subst_not_found
Enrico Tassi [Tue, 13 Apr 2010 19:53:31 +0000 (19:53 +0000)]
catch the right exception, avoid uncaught Subst_not_found

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosame heads different arity -> INCOMPARABLE
Enrico Tassi [Tue, 13 Apr 2010 19:52:58 +0000 (19:52 +0000)]
same heads different arity -> INCOMPARABLE

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosome fixes to THF parser
Enrico Tassi [Tue, 13 Apr 2010 19:52:26 +0000 (19:52 +0000)]
some fixes to THF parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed support file for TPTP
Enrico Tassi [Tue, 13 Apr 2010 19:51:39 +0000 (19:51 +0000)]
fixed support file for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothe edges must be quoted as well (not only the nodes)
Ferruccio Guidi [Sun, 11 Apr 2010 17:13:56 +0000 (17:13 +0000)]
the edges must be quoted as well (not only the nodes)

From: fguidi <fguidi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoapply_subst_context on statuses
Andrea Asperti [Fri, 9 Apr 2010 14:04:08 +0000 (14:04 +0000)]
apply_subst_context on statuses

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Enrico Tassi [Thu, 8 Apr 2010 17:49:30 +0000 (17:49 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agosupport axioms
Enrico Tassi [Thu, 8 Apr 2010 17:44:46 +0000 (17:44 +0000)]
support axioms

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Enrico Tassi [Thu, 8 Apr 2010 17:33:28 +0000 (17:33 +0000)]
...

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agothf problems list for tptp 4.0.1
Enrico Tassi [Thu, 8 Apr 2010 17:31:03 +0000 (17:31 +0000)]
thf problems list for tptp 4.0.1

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agofixed compiltion order of lexer/parser
Enrico Tassi [Thu, 8 Apr 2010 17:28:13 +0000 (17:28 +0000)]
fixed compiltion order of lexer/parser

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew code (unbranched) to compute all keys by all possible ways of reducing the term.
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:38:53 +0000 (16:38 +0000)]
New code (unbranched) to compute all keys by all possible ways of reducing the term.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNew sets of.
Claudio Sacerdoti Coen [Thu, 8 Apr 2010 16:37:26 +0000 (16:37 +0000)]
New sets of.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser received some care
Enrico Tassi [Thu, 8 Apr 2010 14:43:43 +0000 (14:43 +0000)]
THF parser received some care

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoFixing indexing (commit parziale di Claudio?)
Andrea Asperti [Thu, 8 Apr 2010 13:02:05 +0000 (13:02 +0000)]
Fixing indexing (commit parziale di Claudio?)

From: asperti <asperti@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoTHF parser for TPTP
Enrico Tassi [Wed, 7 Apr 2010 13:34:29 +0000 (13:34 +0000)]
THF parser for TPTP

From: tassi <tassi@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoNot is now inductive.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 16:27:56 +0000 (16:27 +0000)]
Not is now inductive.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoUse the inversion!
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:53:12 +0000 (14:53 +0000)]
Use the inversion!

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoBug fixed: the current equation is not always the last hyp.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:41:09 +0000 (14:41 +0000)]
Bug fixed: the current equation is not always the last hyp.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago...
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 14:40:34 +0000 (14:40 +0000)]
...

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years ago- inversion principles are now generated also for co-inductive types
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:49:43 +0000 (13:49 +0000)]
- inversion principles are now generated also for co-inductive types
- we use uniformly the cases_tac/elim_tac in the inversion principle

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>

14 years agoMore debugging info from print_tac.
Claudio Sacerdoti Coen [Wed, 31 Mar 2010 13:35:12 +0000 (13:35 +0000)]
More debugging info from print_tac.

From: sacerdot <sacerdot@c2b2084f-9a08-0410-b176-e24b037a169a>