* 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.
* 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.
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.
* 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.
* 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.
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!
* 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.
* 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
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)
Andrea Asperti [Tue, 16 Apr 2002 09:00:50 +0000 (09:00 +0000)]
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
projects / helm.git / log