Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

Updated to use the new parser that creates (stacks of) existential variables
when an implicit arguments is found.

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

First version of hxsp (new version of UWOBO implemented in Perl by
Alessandro Barzanti using the bindings to libxml and libxslt).

Added examples.

converted to unix textfile (fromdos)

bugfix: Ring will work again with varmaps :-)

- added Ring tactic on reals
- module splitting
- proofEngine is now almost functional

bugfix that inhibit the removal of certain hypotheses

bug fix: handled LetIn case in simpl

mathQL modified, stderr corrected to stdout im mathql_interpreter,
new lavel assignment procedure in mQueryGenerator (uses degrees),
textual interface for mQueryGenerator added

Invariant description added.

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.

Wrong xpointers generated. Fixed.

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.

class parameter added to the getallrdfuris method.
Values may be forward or backward.

Bug fixed: empty elements did not ask for the size of their first following siblings in the
charcount mode.

added comment about 0 and 1 based indexes

mathQL and mqint updated
multiple MQReference and MQPattern added (untested)

ted version of mQueryGenerator (was mquery part 2)

untested version of mQueryGenerator (was mquery part 2)

bug fix: wrapped some possible List.{hd,tl} failures raising an
IllFormedUri exception

database connection parameters updated

let in scope corrected and new database format support

piecewise ==> m:piecewise
piece     ==> m:piece

*** empty log message ***

Bug fixed: a sort not in normal form can now also be a LetIn.

Coscoy double inner types now available also for Meta arguments.

updated for the new version of mathQL.ml

mathQL.ml updated

Inner-types a la Coscoy now correctly generated even for atoms.

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.

Benchmarcking informations output.

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.

Modified Files:
1) grammar.txt xmathql.dtd: modified EXISTS, added SORTEDBY and MINIMIZE
Added Files:
1) core_grammar.txt: implemented grammar

added type for list variables

let in updated with the grammar

Names of some constructors changed.

changed settings to access database

let in implemented

added support for let in

MQueryUtil updated

* 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.

* Abst removed from the DTD
* Metas completely changed in the DTD

* Abst removed from the DTD

* double inner types (in the sense of Coscoy) handled correctly
  (but only in HTML)

* 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.

Abst removed from the DTD.
Warning!!!! This breaks the most part of the code of HELM.

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)

New: expected types (in the sense of Yann Coscoy) are now available

* 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)

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.

Modified Files:
1) grammar.txt query.xml xmathql.dtd: aligned versions (added LETIN
   REFERENCE SETEQUAL SUBSET LVAR)

Modified Files:
1) mmlctop.xsl: a copy of mmlctop2_0.xsl

XSLT Version 0.1 ==> 1.0

XSL Version 0.1 ==> 1.0

XSL version 0.1 ==> 1.0

Syntax error.

The GET request of the method "RemoveAllPredefined" had a separator at the end.
Fixed.

dummy=0 was inserted in the GET part of the HTTP request of the "Load All
Predefined" method. Fixed.

diff and sortedby implemented

New module helm-mathql.

...

new MathQL syntax

* 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.

Modified Files:
1) grammar.txt: added SUBSET, SETEQUAL, REFERENCE and rvar in <list>

* 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.

* 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.

Fold must use replace with the = equality and not the physical == equality.

faster database format implemented

Modified Files:
1) grammar.txt: added in where clause EQUAL between lists

* 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.

intersect improved in speed

Modified Files:
1) grammar.txt xmathql.dtd: moved sortby in grammar comments

result format changed

.cvsignore improved

sortedby implemented and new uri result format

constant string quoting was fixed

mathql package started

textual parser and other utilities for mathql

Conjectures and Hypotheses inside every conjecture and in the sequents now
have an id and thus can be selected.

cic2acic.mli added

delift moved from cicSubstitution to cicUnification

Modified Files:
1) query.xml xmathql.dtd: pattern changed

getallrdfuris implemented

MQRefs fixed

Two Meta occurrences where a parameter is accessible only in one of them
can now be considered convertible.

*** empty log message ***

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.

Updated semantic notes on <pattern>

Modified Files:
1) query.xml xmathql.dtd: PATTERN changed

dded semantic notes on <pattern>

mathql.ml is now part of ocaml/mathql_interpreter

mquery.ml now really call the execution of the query.
Locate and backward now really work!!!

Metavariables representation changed. Explicit substitutions introduced.

Next commit undone: I committed the version used only for our proof-assistant.

Explicit substitutions for metavariables introduced and DTD changed.

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.

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...

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.