Bug fixed (hopefully without introducing new ones): when the user clicked in
AutoWin on a theorem that does not generate new goals, the hint was never
found and auto "immediately" failed.
log.ma is now created. But it does not contain the exact sequence of things
proved by auto.
width=2 does not seem to hurt!
the graph is now really acyclic (I swear).
Ferruccio Guidi [Sun, 20 May 2007 10:41:12 +0000 (10:41 +0000)]
applyTransformation: added debugging information
makefiles: %.mo.opt now working
developments.txt: added Base-2 devel
acic_procedural: some improvements
new optimization: atomic let-ins are now expanded
Ferruccio Guidi [Fri, 18 May 2007 15:55:49 +0000 (15:55 +0000)]
- new devel contribs/LAMBDA-TYPES/Base-2 with the automatically generated
procedural representation of the proofs in contribs/LAMBDA-TYPES/Base-1
- template_makefile_devel.in: %.mo.opt now works
- acic_procedural: some improvements
- PrimitiveTactics: a part of the elim tactic was factorixed for use by the
procedural reconstruction
In some cases (e.g. JM equality) the inversion principle is not generated
because CicRefine cannot infer a dependetly enough type. Now a warning is
raised and compilation is not stopped.
Enrico Tassi [Thu, 17 May 2007 15:45:59 +0000 (15:45 +0000)]
auto rewritten with only one tail recursive function.
this allows to have a GUI to drive the procedure.
a new measure size has been added, and width changed its meaning.
a bunch of unfold lt added to library_auto.
Ferruccio Guidi [Mon, 14 May 2007 16:37:18 +0000 (16:37 +0000)]
CSC: terrific bug fixed. Enrico commented the application of eta_fix to the body
of a constant, without replacing it with Unshare.unshare (that is done inside
eta_fix). To avoid the bug to happear again, I have renamed eta_fix in
eta_fix_and_unshare.
Andrea Asperti [Mon, 30 Apr 2007 10:51:14 +0000 (10:51 +0000)]
Even if we are at depth 0, we first check in the cache for a solution,
before failing. In the other case the assert false at line 76 of
autocache may fail.
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.