AMBDA-TYPES: some improvements. subst now fully exploited
developments.txt: added library_auto
RELATIONAL: some improvements. subst now fully exploited
cic_procedural: a List.rev was missing :-p
substTactic: tacticals are now exploited properly
The declarative rewriting step now tries auto timeout=3 before
auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.
Much ado about nothing:
1) repeat tac end ==> repeat tac
2) do n tac end ==> do n tac
3) "goal n" finally dropped (deprecated, semantics no longer clear)
4) the AST (in grafiteAst) has been changed to better reflect the
distinction between tactics (including h.o. tactics, i.e. tacticals),
punctuational tinycals and non punctuation tinycals (i.e. skip, focus,
unfocus)
5) all tacticals are now running properly in every condition;
but tacticals argument (i.e. tactics occurring in tacticals) are
disambiguated eagerly and not lazily (to be changed)
WARNING: the code in proceduralTypes.ml has been commented out since I am
not able to figure out how to fix it properly
Interface of the argument to Continuationals.Make greately simplified. The
following functions have been removed:
- id_tactic
- get_status
- get_proof
- set_goals
Tacticals invoked from the top-level but the ones implemented on top
of tinycals where not working properly because of several bugs.
The current commit changes the code in quite a few places:
1) there is no longer a function Tacticals.Make since tacticals implemented
on top of tinycals always instantiated the functor with
Tacticals.ProofEngineStatus, and the toplevel can avoid any instantiation
at all since it can invoke tinycals directly on the low-level machine
(implemented by the functor Continuationals.Make)
2) when GrafiteEngine now meets a punctuation tacticals, it directly invokes
an instantiation of Continuationals.Make, without going througw Tacticals.
Instead, when it meets a real tactical, it directly invokes Tacticals
(where Continuationals.Make is applied to Tacticals.ProofEngineStatus
and not to the module defined in GrafiteEngine and used for punctuation
tacticals)
3) most of the tacticals not implemented on top of tinycals were bugged
(and unused). E.g.: solve always diverged unless it was applied to the
empty list. All these bugs have been fixed.
The commit is incomplete since:
1) all tacticals not implemented on top of tactics now accept only a single
tactic as argument (if they require a list, the list must be a singleton).
This limitation is going to disappear again, but we must change GrafiteAst
so that an atomic tactical becomes a recursive tactic.
2) Seq and Then are not branched (for the same reasons as 1 and a bit of
lazyness)
3) several auxiliary functions in the argument of Continuaniolas.Make can now
be removed since they were introduced for wrong reasons.
alpha equivalence fixed: in the case "meta against meta" we did not recur on theexplicit substitutions. The case "Type against Type" and "Implicit against Implicit" need to be checked. Are we really sure that structural equality is enough?
(when we compare universes and implict annotations)
Serious bug fixed: a variable was captured during unfolding of Fix, resulting
in the context of the return type of mutually recursive definitions being
lifted for each function but the first one!
Several instances of the same bug fixed at once: when processing a Fix,
before adding the types to the context (to process the bodies), the types
must be lifted. The simplify tactic is still not working propertly.
Ferruccio Guidi [Fri, 16 Mar 2007 18:39:27 +0000 (18:39 +0000)]
elim tactic: it needs two arguments, a term as well as a pattern
CicReduction: head_beta_reduce now can take the number of beta-redexes to reduce
Procedural: refactoring
Ferruccio Guidi [Tue, 13 Mar 2007 13:21:56 +0000 (13:21 +0000)]
elim tactic: now takes a pattern instead of just a term
works as before for now. the pattern wil be activated soon
Procedural: cleaning up
ProofEngineReduction: new subst_inv function exactly inverts subst
Ferruccio Guidi [Thu, 1 Mar 2007 19:00:14 +0000 (19:00 +0000)]
Procedural: some improvements
rewrite tactic: bug fix in hyps searching
TermContentPres: one space added in let-in rendering
prova.ma: new procedural proof of ty3_gen_cast
Ferruccio Guidi [Wed, 21 Feb 2007 14:15:55 +0000 (14:15 +0000)]
procedural : some improvements.
decompose tactic: user provided premise and types removed.
The decomposable types are now the non-recursive inductive
types without right parameters and are auto-detected
projects / helm.git / log