mathQL modified, stderr corrected to stdout im mathql_interpreter,
new lavel assignment procedure in mQueryGenerator (uses degrees),
textual interface for mQueryGenerator added
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.
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.
* 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
* 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.
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)
* 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.
* 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.
* 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.
* 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.
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.
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.
projects / helm.git / log