1. All the reduction tactics have been modified to reduce several (sub)terms
at once.
2. To reduce several (sub)terms at once you can use the new multiple
selection feature.
Optional callbacks have been added to tactics that need to introduce
new fresh names directly (i.e. without calling other tactics that need
fresh names). The default behaviour is _MUCH_ nicer than the previous
dummy one and is fully functional.
Corollary 1: all the code of tactics.cma is now reentrant.
Corollary 2: the user can be asked the fresh name if it is requested
by a top-level tactic.
New module Disambiguate to hold:
- a functor to disambiguate terms. The input module holds all the
callbacks to the user (that will be implemented differently in Gtk
and as Web forms).
- some utility functions working on CicTextualParser0.uri which should
be moved somewhere else.
Ambiguous parsing improved: refining is now used to prune-out not-well-typed
choices as soon as the term can not be refined. Unfortunately the whole
disambiguation is parsing-bound and not type-checking/refining bound.
Refine can now also raise Uncertain. The exception is raised every
time a metavariab le could be instantiated in such a way that the
term could become well-typed. Useful for ambiguous parsing.
Added a special charcount threatment to the 'append' csymbol (whose length
was estimated being 6 instead of 3). We should do the same for every csymbol
we provide special notation to.
Michele Galatà [Thu, 12 Dec 2002 09:08:38 +0000 (09:08 +0000)]
Rearranged tactics in VariousTactics into new modules EqualityTactics, EliminationTactics,
IntroductionTactics and NegationTactics.
Added new tactics: Rewrite <-, Replace.
positive.xsl is now included in headercontent.xsl and no more required in
arith.xml and list.xml. This is necessary to overload the standard rendering
of some operators (e.g. notation for real numbers).
* New button "Select only constants" to choose the URIs to try during the
disambiguation phase. Usually the number of constants is small and among
them there is the right URI.
* New ElimIntrosSimpl replaces the old ElimSimplIntros.
* mQueryLevel2.get_constraints now gives back only the "must" constraints.
* the "refine constraints" interface has been improved. It can now handle
also constraints on Sorts and constants.
The fresh_name generator has been moved to ProofEngineHelpers.
intros_tac now directly uses it ==> no more ~mkname arguments.
The generator has been "improved" so that it does not generate any
more two equal names. The drawback is that every identifier is
augmented with a nonce.
Bug fixed: when iota-expanding fixpoints the context was sometimes augmented
with the new types, even if the expansion already de-lifted the function body.
The user interface for the completeSearchPattern query has been improved.
It is now "easy" to query for induction principles, for example.
Much work still to do.
1. depth constraints for Rels and Sorts are now optional
2. "can" constraints renamed to "only" constraints
3. several bug fixes:
* the order of arguments for Sub in the second phase of the query was wrong
* some identifiers in the generated query were unbound
Bug fixed: the lhs part of an explicit name substitution was not generated
as an m:ci, but as simple text ===> no m:mi and no hyperlink were generated.
* mQueryLevels interface clean-up
* gui improvement: the precision level of the SearchPattern query is now
chosen by the user. Previously it was guessed.
* fold_tac has now a new parameter, which is the reduction to ``undo''
* The Fold button is replaced with Fold_whd and Fold_reduce
* Minor interfaces modifications
First working version of the possibility to introduce new inductive type
definitions. Many checks have not been implemented yet and the interface
allows you to progress to further stages even if the input is incorrect.
Nevertheless, if the input is correct it will be accepted by the kernel,
saved to disk and notified to the getter.
put_inductive_definition implemented and exposed.
It is a very UNSAFE solution to the problem of computing inner-types of
non-debrujined mutual inductive types (whose constructors referes to
the not-yet-defined inductive type block): you can use this function to
add the block to the environment; then you compute the inner-types; and
finally you save the object and register it to the getter.
typecheck_mutual_inductive_defs exposed.
It is used to type-check and inductive definition which has no URI associated
to it (i.e. it is not managed by the getter; e.g. when it is not saved yet
since we do not know if it is well-typed).
Michele Galatà [Tue, 3 Dec 2002 11:02:33 +0000 (11:02 +0000)]
Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work)
Moved ElimType from ring.ml to variousTactics.ml
Moved Contradiction from fourierR.ml to variousTactics.ml
First implementation of the new generalized SearchPattern on the whole
type (not only the conclusion). Despite the file name, no levels have
been implemented so far.
Brand new implementation based on functors taking a strategy in input.
Several different strategies have been implemented. Unfortunately many
of them are incomparable and there are critical examples where only some
of them terminate in reasonable time.
Removing the functor/module stuff does not bring any sensible performance
improvement even for simple strategies (where most of the functions are
just identity fuctions that can be inlined when not crossing functor
boundaries).
projects / helm.git / log