Debugging Sub and Meet

Updating contests and time misurations

the db connection parameters are now parametrized istead of hard-coded
we use Sys.time () instead of Unix.time ()
Let-in for vvars fixed

topLevel updated for the new mqint

Relation ok!

Db connection ok!

mqint updated

toplevel updated

Db connection initialization

Db exceptions update

Whithout List.hd error

Without warning

Const without duplicates

contest file

New files about Sub Meet

After add relation.ml relation.mli

After Union and Relation

binders list specified in MathQL.Ex constructors

binders list added to MathQL.Ex constructor

new semantics for relation and attribute

intersect.ml cleaned

Generator updated for the new semantics of Relation

Commit of updates in intersect.ml/mli, mqint.ml, Makefile

new query generator

new toplevel with -help option instead of the Readme

vvar context component added

This commit was manufactured by cvs2svn to create branch 'new_mathql'.

parser and pretty printer corrected and tested

let-in on vvars added to mathql

attr_list changed in vvar_list

parsing and pretty printing for textual notation

a small correction to mathQL.ml

new mathql semantics

This commit was manufactured by cvs2svn to create branch 'new_mathql'.

mQueryGenerator and topLevel patched

Modified Files:
1)dces dcq dctype: new versions
Removed Files:
1)eor

some small improvements: command line sintax changed, -MB added

Modified Files:
xmathql.dtd: syntax error

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.

raw HTML markap generator

textual parser fixed

Fourier tactic

Added Files:
1)result.xml xmqlresult.dtd: example and dtd for MathQL query results

user name added to tmp file name

Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new grammar

Type expression simplified.

Comment typo fixed.

Modified Files:
1)core_grammar.txt grammar.txt query.xml xmathql.dtd: new version
----------------------------------------------------------------------

debian release -3

debian version "-8"

forward compatibility changes for ocaml 3.06

Interface file created. Missing from previous commit.

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.