patch

This commit was manufactured by cvs2svn to create branch
'unlabeled-1.2.2'.

...

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.

 Modified Files:
1) mmlctop2_0.xsl: added comments

First very-very-very-very-alfa release of a MathQL Interpreter implemented
on top of RDF-Suite.

Erroniously included (is a debian build process temp file)

Release 0.1.0-1 of the deb package.

Experimental commit: definitions are now allowed in contexts. As a consequence,
CicReduction.whd now requires a context.

Experimental commit: we can now have definitions in contexts. As a
consequence the context is now required by CicReduction.whd

Modified Files:
1) mmlnotation.xsl: added parenthesis to some operators because apply-imports
   doesn't support with-param

Added Files:
1) backward.dtd forward.dtd: dtd for forward and backward metadata files

* Slides can now also be in XHTML format
* Nijmegen's slides for the kick-off added
* Rendering of the management information improved (table border)

New data from DFKI about work-package leaders and PCC members.

New data.

basic MathQL support

Modified Files:
1) grammar.txt query.xml xmathql.dtd: Pattern structure added in the dtd
and some other changes

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

* Error handling improved
* Check does not move any more the input to the "old input" area.

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.

Bug fixed: the unwinding was not recursively performed. (a "t" should have been
a "t'")

META parsing was completely broken. Fixed.

gdome_xslt ==> gdome2-xslt

...

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

Old and dead code from the previous implementation removed.

First (very bugged) version of cic_unification committed.

Bug fixed in type_of_aux (Cast case).

Grammar factorized to avoid shift/reduced conflicts that were handled in
the wrong way. No more conflicts left.

'-' no more allowed in identifiers

* New implementation of Apply and Elim based on the latest implementation
  of the unification (not yet commited)

Modified Files:
1) grammar.txt: changes
Added Files:
1) query.xml: query example
2) xmathql.dtd: dtd for mathql

Modified Files:
1) grammar.txt: added new entries.

* The interface of CicTypeChecker now allows the usage of definitions in
  contexts.
* Let...In tactic implemented (but not tested!)

* env renamed to context everywhere in cicTypeChecker.ml
* Definitions should be allowed in the contexts as well as Declarations.
  This is the very first step: the notion of context is introduced in cic.ml
  and the interface of cicTypeChecker.mli reflects that. (Of course, also the
  interface of cicReduction should do the same!)
  The new implementation just raises an exception when a definition is found
  in the context.

Added Files:
1) grammar.txt: grammar of the Mathematical Query Language

Bug fixed: reduction in the scratch window now works even if there is no
proof in progress.

Reduction tactics in the scratch window implemented.
NOTE: if you select an hypothesis and you apply a reduction tactic, nothing
 will happen and no error message will be reported!

Debugging stuff removed.

Scratch window is now also raised (= hide + show ;-| when updated.

* Error reporting improved
* Check now also works when no current goal and/or no current proof is
  available.

* Scratch window added
* Check command implemented

Modified Files:
1) arith.xsl: ci -> cn for O

* Many improvements
* The interface now gives the user the possibility of (re-)opening an existing
  constant.
* Tactic Elim no more exposed in the user interface. Replaced by ElimIntros.
* Selection of subterms in the hypothesis of the goal is now "sound".
* Reduction tactics (Whd, Reduce, Simpl) now work also on the hypothesis.
  New bug/feature: their changes are lost when moving to another goal
  and coming back afterwards.

Module Logger added.

type_of_aux' (to get the type of a term in a given environment and context)
exported

pp exported

Ooops. Comments in .mly must be delimited by /* and */

* identifiers can now also have digits in them
* arrow notation for non-dependent Pi-abstraction introduced.
  It seems to be bugged w.r.t. application (a problem of priority?)
* CicTextualParserContext provides an highly not-reentrant implementation
  of parsing in a given environment

* Many improvements
* Added the possibility to select parts of the goal of a sequent and retrieve
  the corresponding CIC term.
* New tactics implemented: Cut, Whd, Reduce, Simpl, Change

Added the possibility to select parts of the goal of a sequent and retrieve
the corresponding CIC term.

Removed the patch to avoid a bug of gmetadom.

...

proofEngineReduction.ml added
It holds functions to perform reduction and simplification of terms.
They are used in the implementation of the reduction/conversion tactics.

* Bug fixed: applications of MutCase that are not iota-redexes were reduced
  just to their head.
* More debugging enabled (to be removed when code becomes stable)

Invariant enforced: no Appl of another Appl.

1. CicReduction moved into CicReductionNaif
2. CicReductionMachine is the new implementation based on an
   "environment machine".
You must make a sumbolic link from one implementation (.ml) to
cicReduction.ml

Replaced with a symbolic link to the actual implementation.
The symbolic link must be created after check-out.

type_of_aux' exported.

Meta implemented.

Modified Files:
1) mmlnotation.xsl xslt_index.txt: MathML default presentation now is
   generated by mmlctop.xsl
Added Files:
1) mmlctop.xsl mmlctop2_0.xsl: link and new Igor stylesheet for MathML default
   presentation

* New slides from Saarbrucken
* DTD changed

added debian stuff and a makefile with "dist" target

changed name to gdome2-xslt