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

22 years agogetallrdfuris implemented
Claudio Sacerdoti Coen [Wed, 22 May 2002 09:37:48 +0000 (09:37 +0000)]
getallrdfuris implemented

22 years agoMQRefs fixed
Ferruccio Guidi [Tue, 21 May 2002 15:24:24 +0000 (15:24 +0000)]
MQRefs fixed

22 years agoTwo Meta occurrences where a parameter is accessible only in one of them
Claudio Sacerdoti Coen [Tue, 21 May 2002 15:24:22 +0000 (15:24 +0000)]
Two Meta occurrences where a parameter is accessible only in one of them
can now be considered convertible.

22 years ago*** empty log message ***
Ferruccio Guidi [Tue, 21 May 2002 15:22:26 +0000 (15:22 +0000)]
*** empty log message ***

22 years agoExperimental commit that implements the getalluris method, that gives back in
Claudio Sacerdoti Coen [Tue, 21 May 2002 08:52:37 +0000 (08:52 +0000)]
Experimental commit that implements the getalluris method, that gives back in
XML all the known uris whose prefix is cic and whose suffix is not .types.
Useful to implement the locate query with galax.

22 years agoUpdated semantic notes on <pattern>
Ferruccio Guidi [Mon, 20 May 2002 16:17:03 +0000 (16:17 +0000)]
Updated semantic notes on <pattern>

22 years agoModified Files:
Irene Schena [Mon, 20 May 2002 15:11:49 +0000 (15:11 +0000)]
Modified Files:
1) query.xml xmathql.dtd: PATTERN changed

22 years agodded semantic notes on <pattern>
Ferruccio Guidi [Mon, 20 May 2002 15:09:22 +0000 (15:09 +0000)]
dded semantic notes on <pattern>

22 years agomathql.ml is now part of ocaml/mathql_interpreter
Claudio Sacerdoti Coen [Mon, 20 May 2002 13:51:31 +0000 (13:51 +0000)]
mathql.ml is now part of ocaml/mathql_interpreter

22 years agomquery.ml now really call the execution of the query.
Claudio Sacerdoti Coen [Mon, 20 May 2002 10:48:31 +0000 (10:48 +0000)]
mquery.ml now really call the execution of the query.
Locate and backward now really work!!!

22 years agoMetavariables representation changed. Explicit substitutions introduced.
Claudio Sacerdoti Coen [Mon, 20 May 2002 09:21:57 +0000 (09:21 +0000)]
Metavariables representation changed. Explicit substitutions introduced.

22 years agoNext commit undone: I committed the version used only for our proof-assistant.
Claudio Sacerdoti Coen [Mon, 20 May 2002 09:20:00 +0000 (09:20 +0000)]
Next commit undone: I committed the version used only for our proof-assistant.

22 years agoExplicit substitutions for metavariables introduced and DTD changed.
Claudio Sacerdoti Coen [Mon, 20 May 2002 09:18:52 +0000 (09:18 +0000)]
Explicit substitutions for metavariables introduced and DTD changed.

22 years agoMany many improvements:
Claudio Sacerdoti Coen [Mon, 20 May 2002 09:17:54 +0000 (09:17 +0000)]
Many many improvements:
1) First version after the introduction of explicit substitutions and
   the change in the DTD and in the stylesheets.
2) ElimIntros (that didn't work) have been replace by ElimIntrosSimpl
   that now does what the name tells you.
3) Buttons to move to the next and previous open goal introduced.
4) Serious bug in reduce and in simpl fixed: they didn't handle the environment
   properly.
5) replace is now an hygher order function, parametrized w.r.t. the equality
   to use. In some cases the right equality is physical equality. This closes
   some residual bugs.

22 years agocicReductionNaif.ml was left out from the commit that introduced explicit
Claudio Sacerdoti Coen [Mon, 20 May 2002 09:14:13 +0000 (09:14 +0000)]
cicReductionNaif.ml was left out from the commit that introduced explicit
substitutions. Then I also destroyed it. This is a new implementation that
considers explicit substitutions and has not been tested. I hope that it
works...

22 years agoNew experimental commit: metavariables representation is changed again,
Claudio Sacerdoti Coen [Mon, 20 May 2002 08:39:06 +0000 (08:39 +0000)]
New experimental commit: metavariables representation is changed again,
together with the DTD (still uncommitted). The new representation implements
explicit substitutions, allowing the correct reduction behaviour.
The most part of the modules have been changed to reflect the new
representation. Unification has been rewritten.

22 years ago Modified Files:
Irene Schena [Thu, 16 May 2002 14:35:45 +0000 (14:35 +0000)]
 Modified Files:
1) mmlctop2_0.xsl: added comments

22 years agoFirst very-very-very-very-alfa release of a MathQL Interpreter implemented
Claudio Sacerdoti Coen [Tue, 14 May 2002 17:26:44 +0000 (17:26 +0000)]
First very-very-very-very-alfa release of a MathQL Interpreter implemented
on top of RDF-Suite.

22 years agoErroniously included (is a debian build process temp file)
Stefano Zacchiroli [Tue, 14 May 2002 11:20:18 +0000 (11:20 +0000)]
Erroniously included (is a debian build process temp file)

22 years agoRelease 0.1.0-1 of the deb package.
Stefano Zacchiroli [Tue, 14 May 2002 11:19:29 +0000 (11:19 +0000)]
Release 0.1.0-1 of the deb package.

22 years agoExperimental commit: definitions are now allowed in contexts. As a consequence,
Claudio Sacerdoti Coen [Wed, 8 May 2002 09:17:24 +0000 (09:17 +0000)]
Experimental commit: definitions are now allowed in contexts. As a consequence,
CicReduction.whd now requires a context.

22 years agoExperimental commit: we can now have definitions in contexts. As a
Claudio Sacerdoti Coen [Wed, 8 May 2002 09:15:42 +0000 (09:15 +0000)]
Experimental commit: we can now have definitions in contexts. As a
consequence the context is now required by CicReduction.whd

22 years agoModified Files:
Irene Schena [Tue, 7 May 2002 11:01:23 +0000 (11:01 +0000)]
Modified Files:
1) mmlnotation.xsl: added parenthesis to some operators because apply-imports
   doesn't support with-param

22 years agoAdded Files:
Irene Schena [Mon, 6 May 2002 14:41:45 +0000 (14:41 +0000)]
Added Files:
1) backward.dtd forward.dtd: dtd for forward and backward metadata files

22 years ago* Slides can now also be in XHTML format
Claudio Sacerdoti Coen [Thu, 2 May 2002 12:52:48 +0000 (12:52 +0000)]
* Slides can now also be in XHTML format
* Nijmegen's slides for the kick-off added
* Rendering of the management information improved (table border)

22 years agoNew data from DFKI about work-package leaders and PCC members.
Claudio Sacerdoti Coen [Thu, 2 May 2002 12:51:39 +0000 (12:51 +0000)]
New data from DFKI about work-package leaders and PCC members.

22 years agoNew data.
Claudio Sacerdoti Coen [Thu, 2 May 2002 12:50:58 +0000 (12:50 +0000)]
New data.

22 years agobasic MathQL support
Ferruccio Guidi [Tue, 30 Apr 2002 16:52:08 +0000 (16:52 +0000)]
basic MathQL support

22 years agoModified Files:
Irene Schena [Mon, 29 Apr 2002 14:27:49 +0000 (14:27 +0000)]
Modified Files:
1) grammar.txt query.xml xmathql.dtd: Pattern structure added in the dtd
and some other changes

22 years ago* Bug fixed: Elim did not work for principles whose conclusion was just
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:53:51 +0000 (10:53 +0000)]
* Bug fixed: Elim did not work for principles whose conclusion was just
  a META and not an application.
* The old implementation of ElimIntros was misleading: It applied Intros only
  to the first goal. Removed.
* A new implementation of ElimIntros (and of ApplyIntros) is partially provided,
  but unused. It requires the forthcoming new META definition and unification
  algorithm.

22 years ago* Error handling improved
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:23:17 +0000 (10:23 +0000)]
* Error handling improved
* Check does not move any more the input to the "old input" area.

22 years agoComputed inner-types are now also put in whd normal form.
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:22:09 +0000 (10:22 +0000)]
Computed inner-types are now also put in whd normal form.
This is at the same type too strong (e.g. it performs delta-reductions)
and too weak (it is not full-reduction).
We can consider this just a patch waiting for Coscoy's double-inference
algorithm implementation.

22 years agoBug fixed: the unwinding was not recursively performed. (a "t" should have been
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:07:47 +0000 (10:07 +0000)]
Bug fixed: the unwinding was not recursively performed. (a "t" should have been
a "t'")

22 years agoMETA parsing was completely broken. Fixed.
Claudio Sacerdoti Coen [Mon, 29 Apr 2002 10:06:06 +0000 (10:06 +0000)]
META parsing was completely broken. Fixed.

22 years agogdome_xslt ==> gdome2-xslt
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 13:54:49 +0000 (13:54 +0000)]
gdome_xslt ==> gdome2-xslt

22 years ago...
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 12:03:12 +0000 (12:03 +0000)]
...

22 years ago* Many improvements (expecially in exceptions handling)
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:37:40 +0000 (10:37 +0000)]
* Many improvements (expecially in exceptions handling)
* The cases in which existential variables are now handled "correctly"
  have been increased. Neverthless, existential variables are still implemented
  in a completely wrong way.
* First commit after the commit of cic_unification.

22 years agoOld and dead code from the previous implementation removed.
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:34:57 +0000 (10:34 +0000)]
Old and dead code from the previous implementation removed.

22 years agoFirst (very bugged) version of cic_unification committed.
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:33:28 +0000 (10:33 +0000)]
First (very bugged) version of cic_unification committed.

22 years agoBug fixed in type_of_aux (Cast case).
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:31:06 +0000 (10:31 +0000)]
Bug fixed in type_of_aux (Cast case).

22 years agoGrammar factorized to avoid shift/reduced conflicts that were handled in
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:29:51 +0000 (10:29 +0000)]
Grammar factorized to avoid shift/reduced conflicts that were handled in
the wrong way. No more conflicts left.

22 years ago'-' no more allowed in identifiers
Claudio Sacerdoti Coen [Fri, 26 Apr 2002 10:28:49 +0000 (10:28 +0000)]
'-' no more allowed in identifiers

22 years ago* New implementation of Apply and Elim based on the latest implementation
Claudio Sacerdoti Coen [Wed, 24 Apr 2002 17:07:57 +0000 (17:07 +0000)]
* New implementation of Apply and Elim based on the latest implementation
  of the unification (not yet commited)

22 years agoModified Files:
Irene Schena [Wed, 24 Apr 2002 16:50:29 +0000 (16:50 +0000)]
Modified Files:
1) grammar.txt: changes
Added Files:
1) query.xml: query example
2) xmathql.dtd: dtd for mathql

22 years agoModified Files:
Irene Schena [Tue, 23 Apr 2002 14:58:22 +0000 (14:58 +0000)]
Modified Files:
1) grammar.txt: added new entries.