]> matita.cs.unibo.it Git - helm.git/log
helm.git
22 years agosome small improvements: command line sintax changed, -MB added
Ferruccio Guidi [Thu, 5 Sep 2002 13:39:08 +0000 (13:39 +0000)]
some small improvements: command line sintax changed, -MB added

22 years agoModified Files:
Irene Schena [Thu, 5 Sep 2002 09:41:09 +0000 (09:41 +0000)]
Modified Files:
xmathql.dtd: syntax error

22 years agoThe parser (the lexer indeed) now use the locate query to locate an object
Claudio Sacerdoti Coen [Wed, 4 Sep 2002 17:53:22 +0000 (17:53 +0000)]
The parser (the lexer indeed) now use the locate query to locate an object
whose identifier is unknown. In ambigous cases, no choice is given to the
user and the usual exception (identifier not found) is raised. It works
only for constants and for the first inductive type of a mutual inductive
type block.

22 years agoraw HTML markap generator
Ferruccio Guidi [Wed, 4 Sep 2002 17:05:21 +0000 (17:05 +0000)]
raw HTML markap generator

22 years agotextual parser fixed
Ferruccio Guidi [Wed, 4 Sep 2002 17:00:54 +0000 (17:00 +0000)]
textual parser fixed

22 years agoFourier tactic
Enrico Tassi [Wed, 4 Sep 2002 15:34:28 +0000 (15:34 +0000)]
Fourier tactic

22 years agoAdded Files:
Irene Schena [Tue, 3 Sep 2002 14:55:02 +0000 (14:55 +0000)]
Added Files:
1)result.xml xmqlresult.dtd: example and dtd for MathQL query results

22 years agouser name added to tmp file name
Ferruccio Guidi [Fri, 30 Aug 2002 17:02:37 +0000 (17:02 +0000)]
user name added to tmp file name

22 years agoModified Files:
Irene Schena [Thu, 29 Aug 2002 14:41:02 +0000 (14:41 +0000)]
Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new grammar

22 years agoType expression simplified.
Michele Galatà [Thu, 29 Aug 2002 13:19:02 +0000 (13:19 +0000)]
Type expression simplified.

22 years agoComment typo fixed.
Michele Galatà [Thu, 29 Aug 2002 13:18:34 +0000 (13:18 +0000)]
Comment typo fixed.

22 years agoModified Files:
Irene Schena [Wed, 28 Aug 2002 14:57:52 +0000 (14:57 +0000)]
Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new version
----------------------------------------------------------------------

22 years agodebian release -3
Stefano Zacchiroli [Wed, 28 Aug 2002 13:57:45 +0000 (13:57 +0000)]
debian release -3

22 years agodebian version "-8"
Stefano Zacchiroli [Wed, 28 Aug 2002 13:41:26 +0000 (13:41 +0000)]
debian version "-8"

22 years agoforward compatibility changes for ocaml 3.06
Stefano Zacchiroli [Wed, 28 Aug 2002 13:37:38 +0000 (13:37 +0000)]
forward compatibility changes for ocaml 3.06

22 years agoInterface file created. Missing from previous commit.
Claudio Sacerdoti Coen [Tue, 27 Aug 2002 14:18:31 +0000 (14:18 +0000)]
Interface file created. Missing from previous commit.

22 years agoUpdated to use the new parser that creates (stacks of) existential variables
Claudio Sacerdoti Coen [Mon, 29 Jul 2002 15:55:31 +0000 (15:55 +0000)]
Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

22 years agoUpdated to use the new parser that creates (stacks of) existential variables
Claudio Sacerdoti Coen [Mon, 29 Jul 2002 15:50:29 +0000 (15:50 +0000)]
Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

22 years agoMany improvements in tactics (and tactical) representation:
Claudio Sacerdoti Coen [Mon, 22 Jul 2002 17:50:49 +0000 (17:50 +0000)]
Many improvements in tactics (and tactical) representation:
1) tactics are no more functions from state to state, but functions from
   proof * goal to proof * goal list where the goal list is the list of
   new goals generated
2) proof and goal are no more optional
3) all the tactics have been slightly changed so that their type is now
   param1 -> ... -> paramn -> ProofEngineTypes.tactic
4) the tactical thens has been implemented

Other changes:
1) more .mli committed
2) comments and copyright notices added where missing

22 years agoFirst version of hxsp (new version of UWOBO implemented in Perl by
Claudio Sacerdoti Coen [Mon, 22 Jul 2002 17:34:34 +0000 (17:34 +0000)]
First version of hxsp (new version of UWOBO implemented in Perl by
Alessandro Barzanti using the bindings to libxml and libxslt).

22 years agoAdded examples.
Stefano Zacchiroli [Tue, 2 Jul 2002 09:26:09 +0000 (09:26 +0000)]
Added examples.

22 years agoconverted to unix textfile (fromdos)
Stefano Zacchiroli [Tue, 2 Jul 2002 08:06:44 +0000 (08:06 +0000)]
converted to unix textfile (fromdos)

22 years agobugfix: Ring will work again with varmaps :-)
Stefano Zacchiroli [Tue, 2 Jul 2002 08:05:52 +0000 (08:05 +0000)]
bugfix: Ring will work again with varmaps :-)

22 years ago- added Ring tactic on reals
Stefano Zacchiroli [Mon, 1 Jul 2002 20:22:39 +0000 (20:22 +0000)]
- added Ring tactic on reals
- module splitting
- proofEngine is now almost functional

22 years agobugfix that inhibit the removal of certain hypotheses
Stefano Zacchiroli [Mon, 1 Jul 2002 20:12:54 +0000 (20:12 +0000)]
bugfix that inhibit the removal of certain hypotheses

22 years agobug fix: handled LetIn case in simpl
Stefano Zacchiroli [Mon, 1 Jul 2002 20:10:54 +0000 (20:10 +0000)]
bug fix: handled LetIn case in simpl

22 years agomathQL modified, stderr corrected to stdout im mathql_interpreter,
Ferruccio Guidi [Mon, 1 Jul 2002 11:34:24 +0000 (11:34 +0000)]
mathQL modified, stderr corrected to stdout im mathql_interpreter,
new lavel assignment procedure in mQueryGenerator (uses degrees),
textual interface for mQueryGenerator added

22 years agoInvariant description added.
Claudio Sacerdoti Coen [Mon, 1 Jul 2002 09:15:14 +0000 (09:15 +0000)]
Invariant description added.

22 years agoBug fixed: there is an invariant that every attributed uri list must be
Claudio Sacerdoti Coen [Mon, 1 Jul 2002 09:13:36 +0000 (09:13 +0000)]
Bug fixed: there is an invariant that every attributed uri list must be
ordered on the uri that was not enforced for the new Reference.

22 years agoWrong xpointers generated. Fixed.
Claudio Sacerdoti Coen [Tue, 25 Jun 2002 08:52:21 +0000 (08:52 +0000)]
Wrong xpointers generated. Fixed.

22 years agoLocate query changed again. There is a mismatch between Domenico's
Claudio Sacerdoti Coen [Tue, 25 Jun 2002 08:51:42 +0000 (08:51 +0000)]
Locate query changed again. There is a mismatch between Domenico's
implementation and Ferruccio's semantics. The code now conforms to
Domenico's implementation and seems to work.

22 years agoclass parameter added to the getallrdfuris method.
Claudio Sacerdoti Coen [Mon, 24 Jun 2002 17:11:49 +0000 (17:11 +0000)]
class parameter added to the getallrdfuris method.
Values may be forward or backward.

22 years agoBug fixed: empty elements did not ask for the size of their first following siblings...
Claudio Sacerdoti Coen [Mon, 24 Jun 2002 15:17:48 +0000 (15:17 +0000)]
Bug fixed: empty elements did not ask for the size of their first following siblings in the
charcount mode.

22 years agoadded comment about 0 and 1 based indexes
Stefano Zacchiroli [Mon, 24 Jun 2002 09:34:44 +0000 (09:34 +0000)]
added comment about 0 and 1 based indexes

22 years agomathQL and mqint updated
Ferruccio Guidi [Sat, 22 Jun 2002 17:17:03 +0000 (17:17 +0000)]
mathQL and mqint updated
multiple MQReference and MQPattern added (untested)

22 years agoted version of mQueryGenerator (was mquery part 2)
Ferruccio Guidi [Sat, 22 Jun 2002 17:03:34 +0000 (17:03 +0000)]
ted version of mQueryGenerator (was mquery part 2)

22 years agountested version of mQueryGenerator (was mquery part 2)
Ferruccio Guidi [Sat, 22 Jun 2002 17:01:41 +0000 (17:01 +0000)]
untested version of mQueryGenerator (was mquery part 2)

22 years agobug fix: wrapped some possible List.{hd,tl} failures raising an
Stefano Zacchiroli [Sat, 22 Jun 2002 16:52:57 +0000 (16:52 +0000)]
bug fix: wrapped some possible List.{hd,tl} failures raising an
IllFormedUri exception

22 years agodatabase connection parameters updated
lordi [Wed, 19 Jun 2002 13:22:03 +0000 (13:22 +0000)]
database connection parameters updated

22 years agolet in scope corrected and new database format support
lordi [Wed, 19 Jun 2002 12:53:55 +0000 (12:53 +0000)]
let in scope corrected and new database format support

22 years agopiecewise ==> m:piecewise
Claudio Sacerdoti Coen [Wed, 19 Jun 2002 12:38:44 +0000 (12:38 +0000)]
piecewise ==> m:piecewise
piece     ==> m:piece

22 years ago*** empty log message ***
Claudio Sacerdoti Coen [Wed, 19 Jun 2002 10:45:28 +0000 (10:45 +0000)]
*** empty log message ***

22 years agoBug fixed: a sort not in normal form can now also be a LetIn.
Claudio Sacerdoti Coen [Wed, 19 Jun 2002 10:44:15 +0000 (10:44 +0000)]
Bug fixed: a sort not in normal form can now also be a LetIn.

22 years agoCoscoy double inner types now available also for Meta arguments.
Claudio Sacerdoti Coen [Wed, 19 Jun 2002 10:43:42 +0000 (10:43 +0000)]
Coscoy double inner types now available also for Meta arguments.

22 years agoupdated for the new version of mathQL.ml
Ferruccio Guidi [Tue, 18 Jun 2002 17:42:23 +0000 (17:42 +0000)]
updated for the new version of mathQL.ml

22 years agomathQL.ml updated
Ferruccio Guidi [Tue, 18 Jun 2002 17:39:14 +0000 (17:39 +0000)]
mathQL.ml updated

22 years agoInner-types a la Coscoy now correctly generated even for atoms.
Claudio Sacerdoti Coen [Tue, 18 Jun 2002 17:11:28 +0000 (17:11 +0000)]
Inner-types a la Coscoy now correctly generated even for atoms.

22 years agoConversion rules are now correctly handled also for atoms.
Claudio Sacerdoti Coen [Tue, 18 Jun 2002 17:10:28 +0000 (17:10 +0000)]
Conversion rules are now correctly handled also for atoms.
The only residual problem is that some proofs + side-proofs
where the proof is an atom with different inner-types are
rendered as a proof with two sub-proofs which is innatural.

22 years agoBenchmarcking informations output.
Claudio Sacerdoti Coen [Tue, 18 Jun 2002 13:04:53 +0000 (13:04 +0000)]
Benchmarcking informations output.

22 years agoNew query implementation using LetIn.
Claudio Sacerdoti Coen [Tue, 18 Jun 2002 13:00:43 +0000 (13:00 +0000)]
New query implementation using LetIn.
Some benchmarks:

Query: 2*n <= 2*m

Results:

  No-LetIn     LetIn  Output
 1: 23s   >>>>  3s    9uri        uri/s: 3
 0: 276s  >>>> 14s   48uri        uri/s: 3.42

Open BUGs:
 the implementation of the LetIn scope is surely not correct. The whole
 semantics is wrong in case of repeated names.

22 years agoModified Files:
Irene Schena [Fri, 14 Jun 2002 14:48:32 +0000 (14:48 +0000)]
Modified Files:
1) grammar.txt xmathql.dtd: modified EXISTS, added SORTEDBY and MINIMIZE
Added Files:
1) core_grammar.txt: implemented grammar

22 years agoadded type for list variables
lordi [Fri, 14 Jun 2002 08:03:01 +0000 (08:03 +0000)]
added type for list variables

22 years agolet in updated with the grammar
lordi [Fri, 14 Jun 2002 08:01:10 +0000 (08:01 +0000)]
let in updated with the grammar

22 years agoNames of some constructors changed.
Claudio Sacerdoti Coen [Thu, 13 Jun 2002 17:56:47 +0000 (17:56 +0000)]
Names of some constructors changed.

22 years agochanged settings to access database
lordi [Thu, 13 Jun 2002 17:25:31 +0000 (17:25 +0000)]
changed settings to access database

22 years agolet in implemented
lordi [Thu, 13 Jun 2002 17:18:40 +0000 (17:18 +0000)]
let in implemented

22 years agoadded support for let in
lordi [Thu, 13 Jun 2002 17:13:05 +0000 (17:13 +0000)]
added support for let in

22 years agoMQueryUtil updated
Ferruccio Guidi [Thu, 13 Jun 2002 17:04:53 +0000 (17:04 +0000)]
MQueryUtil updated

22 years ago* syntax error fixed
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 16:12:34 +0000 (16:12 +0000)]
* syntax error fixed
* IT DOESN'T COMPILE!!!
  It must still be ported to the new Meta. I don't do it yet because
  this module should disappear when the new exportation module will be
  available.

22 years ago* Abst removed from the DTD
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 16:09:31 +0000 (16:09 +0000)]
* Abst removed from the DTD
* Metas completely changed in the DTD

22 years ago* Abst removed from the DTD
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 16:07:05 +0000 (16:07 +0000)]
* Abst removed from the DTD

22 years ago* double inner types (in the sense of Coscoy) handled correctly
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 16:04:05 +0000 (16:04 +0000)]
* double inner types (in the sense of Coscoy) handled correctly
  (but only in HTML)

22 years ago* Abst removed from the DTD
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 16:03:09 +0000 (16:03 +0000)]
* Abst removed from the DTD
* real double-type-inference algorithm implemented
* performance improved again (25s for limit_mul). Why???
* Bug left: the double-type annotation is not generated in the case
  of a lambda inside another lambda. To be fixed soon.

22 years agoAbst removed from the DTD.
Claudio Sacerdoti Coen [Wed, 12 Jun 2002 15:53:43 +0000 (15:53 +0000)]
Abst removed from the DTD.
Warning!!!! This breaks the most part of the code of HELM.

22 years agoNew: expected types (in the sense of Yann Coscoy) now availables for
Claudio Sacerdoti Coen [Tue, 11 Jun 2002 10:19:54 +0000 (10:19 +0000)]
New: expected types (in the sense of Yann Coscoy) now availables for
MathML Content and MathML Presentation. HTML support is still missing
(and bugs may have been introduced when expected types are present)

22 years agoNew: expected types (in the sense of Yann Coscoy) are now available
Claudio Sacerdoti Coen [Tue, 11 Jun 2002 10:13:26 +0000 (10:13 +0000)]
New: expected types (in the sense of Yann Coscoy) are now available

22 years ago* doubleTypeInference.ml* added. For now, it just computes the synthesized type.
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 17:39:19 +0000 (17:39 +0000)]
* doubleTypeInference.ml* added. For now, it just computes the synthesized type.
  The expected type is expected soon ;-)
* great performance improvement. For example, the rendering of limit_plus
  is now "only" 30s (was 50s)

22 years agopgocaml ==> postgres
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 17:35:07 +0000 (17:35 +0000)]
pgocaml ==> postgres
Note: a debian package is now available on Zack debian repository
In case you don't use the debian package and postgres is not found, just
make a symbol link from postgres to pgocaml.

22 years agoModified Files:
Irene Schena [Mon, 10 Jun 2002 15:40:36 +0000 (15:40 +0000)]
Modified Files:
1) grammar.txt query.xml xmathql.dtd: aligned versions (added LETIN
   REFERENCE SETEQUAL SUBSET LVAR)

22 years agoModified Files:
Irene Schena [Mon, 10 Jun 2002 14:46:24 +0000 (14:46 +0000)]
Modified Files:
1) mmlctop.xsl: a copy of mmlctop2_0.xsl

22 years agoXSLT Version 0.1 ==> 1.0
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 14:33:48 +0000 (14:33 +0000)]
XSLT Version 0.1 ==> 1.0

22 years agoXSL Version 0.1 ==> 1.0
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 14:32:19 +0000 (14:32 +0000)]
XSL Version 0.1 ==> 1.0

22 years agoXSL version 0.1 ==> 1.0
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 14:27:49 +0000 (14:27 +0000)]
XSL version 0.1 ==> 1.0

22 years agoSyntax error.
Claudio Sacerdoti Coen [Mon, 10 Jun 2002 10:51:12 +0000 (10:51 +0000)]
Syntax error.

22 years agoThe GET request of the method "RemoveAllPredefined" had a separator at the end.
Claudio Sacerdoti Coen [Thu, 6 Jun 2002 11:04:39 +0000 (11:04 +0000)]
The GET request of the method "RemoveAllPredefined" had a separator at the end.
Fixed.

22 years agodummy=0 was inserted in the GET part of the HTTP request of the "Load All
Claudio Sacerdoti Coen [Thu, 6 Jun 2002 11:02:01 +0000 (11:02 +0000)]
dummy=0 was inserted in the GET part of the HTTP request of the "Load All
Predefined" method. Fixed.

22 years agodiff and sortedby implemented
lordi [Fri, 31 May 2002 16:48:07 +0000 (16:48 +0000)]
diff and sortedby implemented

22 years agoNew module helm-mathql.
Claudio Sacerdoti Coen [Wed, 29 May 2002 15:07:52 +0000 (15:07 +0000)]
New module helm-mathql.

22 years ago...
Claudio Sacerdoti Coen [Tue, 28 May 2002 17:56:23 +0000 (17:56 +0000)]
...

22 years agonew MathQL syntax
Ferruccio Guidi [Tue, 28 May 2002 17:48:08 +0000 (17:48 +0000)]
new MathQL syntax

22 years ago* Bug fixed: syntactic equality for CIC term (which was used in the Fold tactic)
Claudio Sacerdoti Coen [Tue, 28 May 2002 17:37:10 +0000 (17:37 +0000)]
* Bug fixed: syntactic equality for CIC term (which was used in the Fold tactic)
  is not the structural equality of Ocaml (i.e. '=') because of cooking
  numbers that can differ denoting the very same term. So a new function
  syntactic_equality has been added to proofEngineReduction.ml and it is now
  used for Fold.

22 years agoModified Files:
Irene Schena [Tue, 28 May 2002 16:05:50 +0000 (16:05 +0000)]
Modified Files:
1) grammar.txt: added SUBSET, SETEQUAL, REFERENCE and rvar in <list>

22 years ago* The "backward" query has been refined considering head position as a different
Claudio Sacerdoti Coen [Tue, 28 May 2002 15:59:01 +0000 (15:59 +0000)]
* The "backward" query has been refined considering head position as a different
  level w.r.t. non-head positions.
* The "backward" query has been refined using the new Subset construct.

22 years ago* New operators (Subset, SetEqual and RVarOccurrence) added to MathQL
Claudio Sacerdoti Coen [Tue, 28 May 2002 15:55:36 +0000 (15:55 +0000)]
* New operators (Subset, SetEqual and RVarOccurrence) added to MathQL
* New implementation of all the operations. We will have to choose if this
  new implementation is better or worst than the previous one.
* Diff and SortBy not implemented yet.

22 years agoFold must use replace with the = equality and not the physical == equality.
Claudio Sacerdoti Coen [Tue, 28 May 2002 15:48:48 +0000 (15:48 +0000)]
Fold must use replace with the = equality and not the physical == equality.

22 years agofaster database format implemented
lordi [Fri, 24 May 2002 17:27:09 +0000 (17:27 +0000)]
faster database format implemented

22 years agoModified Files:
Irene Schena [Fri, 24 May 2002 16:30:12 +0000 (16:30 +0000)]
Modified Files:
1) grammar.txt: added in where clause EQUAL between lists

22 years ago* Clear and ClearBody implemented, but they are bugged because they do not
Claudio Sacerdoti Coen [Fri, 24 May 2002 13:59:59 +0000 (13:59 +0000)]
* Clear and ClearBody implemented, but they are bugged because they do not
  restrict the metavariables that used the cleared hypothesis.
* Reduction tactics in the hypotheses were bugged. This version is still
  bugged, but it works a bit better.

22 years agointersect improved in speed
lordi [Thu, 23 May 2002 16:12:52 +0000 (16:12 +0000)]
intersect improved in speed

22 years agoModified Files:
Irene Schena [Thu, 23 May 2002 13:30:10 +0000 (13:30 +0000)]
Modified Files:
1) grammar.txt xmathql.dtd: moved sortby in grammar comments

22 years agoresult format changed
lordi [Wed, 22 May 2002 17:51:53 +0000 (17:51 +0000)]
result format changed

22 years ago.cvsignore improved
lordi [Wed, 22 May 2002 17:46:08 +0000 (17:46 +0000)]
.cvsignore improved

22 years agosortedby implemented and new uri result format
lordi [Wed, 22 May 2002 17:45:31 +0000 (17:45 +0000)]
sortedby implemented and new uri result format

22 years agoconstant string quoting was fixed
Ferruccio Guidi [Wed, 22 May 2002 17:07:58 +0000 (17:07 +0000)]
constant string quoting was fixed

22 years agomathql package started
Ferruccio Guidi [Wed, 22 May 2002 16:57:18 +0000 (16:57 +0000)]
mathql package started

22 years agotextual parser and other utilities for mathql
Ferruccio Guidi [Wed, 22 May 2002 16:54:11 +0000 (16:54 +0000)]
textual parser and other utilities for mathql

22 years agoConjectures and Hypotheses inside every conjecture and in the sequents now
Claudio Sacerdoti Coen [Wed, 22 May 2002 10:13:34 +0000 (10:13 +0000)]
Conjectures and Hypotheses inside every conjecture and in the sequents now
have an id and thus can be selected.

22 years agocic2acic.mli added
Claudio Sacerdoti Coen [Wed, 22 May 2002 10:10:54 +0000 (10:10 +0000)]
cic2acic.mli added

22 years agodelift moved from cicSubstitution to cicUnification
Claudio Sacerdoti Coen [Wed, 22 May 2002 10:09:21 +0000 (10:09 +0000)]
delift moved from cicSubstitution to cicUnification

22 years agoModified Files:
Irene Schena [Wed, 22 May 2002 10:02:08 +0000 (10:02 +0000)]
Modified Files:
1) query.xml xmathql.dtd: pattern changed