Major module reorganization:
- new module TermViewer: holds widgets to render and interact with sequents
and proofs at the CIC level
- new module ApplyStylesheets: functions to apply stylesheets and map
terms and sequents to MathML Presentation
- new module InvokeTactics: it is a functor that gives back a module that
defines one callback function for every tactic
1. helmns and domImpl moved to the misc module ;-(
2. all the constants and functions relative to stylesheet applications have
been moved to the new module ApplyStylesheets, whose interface is really
minimal.
Minor code reorganization:
1. several functions unrelated do disambiguation moved from Disambiguate
do Misc.
2. TermEditor module added. It implements a widget for entering terms.
The widget is also responsible for the disambiguation.
3. TermEditor is now the only widget that uses the Disambiguate module.
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).
projects / helm.git / log