Ferruccio Guidi [Sat, 18 Oct 2008 19:04:17 +0000 (19:04 +0000)]
Acic2Procedural:
now we accept an optional string argument "info" intended as a comment for the rendered proof (appears afer qed)
ProceduralOptimizer:
- we generate some comments for acic2Procedural.ml info (see above)
- optimize_term is now available
ApplyTransformation:
we fixed a bug in the procedural rendering of auto proofs:
the proof term must be optimized before rendering!
(it is written on the paper about the procedural rendering for PLMMS 2007)
Fixed a performance problem with unif_machines and small_delta_step.
Previously, small_delta_step would occasionally return two machines in
normal form, with a false "are_normal" flag: this in turn caused
unif_machines to perform more steps than necessary. Now the flag returned
by small_delta_step is true iff it could not perform any reduction step;
therefore unif_machines won't try a recursive call on the new machines
(which are equal to the old ones).
Enrico Tassi [Mon, 6 Oct 2008 15:02:12 +0000 (15:02 +0000)]
3 nasty bugs fixed:
- mk_restricted_irl has been duplicated
- mk_restricted_irl generates an irl
- mk_perforated_irl generates a restricted local context suitable for a new meta
- a wrong optimization in psubst was lifting of a bad amount
- force_does_not_occurr was not delifting rels to hypotheses to be cancelled
Enrico Tassi [Fri, 3 Oct 2008 11:04:07 +0000 (11:04 +0000)]
- NCicPp.ppterm applies the substitution
- NCicReduction.are_convertible does not take in input the get_relevance
function any longer, there is a ref set by the typechecker module
- fixes to the convert-machines and small-delta-step logic
- setters for data structures now support "commuting conversion"-like
operations w.r.t. getters
- several axioms have now been proved
- new file env_to_flatenv1 showing an alternative representation of the
environment
more push/pop to avoid confusion with imperative data structures employed by
notation. the patch is not well tested, but already improves the situation
make the library compile again. I commit it so that on monday we will have
again the livecd and the .dsb package that are required by the sysadmins to
install matita on the cs cluster
include statement better implemented:
- push/pop operation for both Lexicon and Grafite stuff, instead of reset
- this (if properly working) opens the doors to a completely functional
matita status
- code size reduced, looking for unifiables or generalizations is
almost the same and do not internally work with the query term,
but its path representation that is now decorated with arieties to
recover the tree structure when needed (jump to the sibling...)
- works with partial instantiation (no more global ariety list, but
local to application heads). Stupid example:
since the 2nd arg is ? we skip the query subterm rooted in plus,
but if plus is considered of ariety 2, we fail unifiing the following
terms (we skip [] and 0 reaching the second 0 that is unified with
[] and fails).
- term -> path string function fixed to clen up the input term, no more
"FIXME: the trie received invalid term". Here there is room for improvements
especially on beta redexes and terms beginning with an abstraction, but we
need the substitutions operation, we should move the file elsewhere
- Big change:
- if the query term is a meta, then the whole content of the tree is returned
- in paramodulation this is dangerous, thus we added a small check in
the paramodulation code (eq_indexing) instead of making the discrimination
tree behave in a nasty way
- the new implementation returns the same set of candidates on all test
TPTP/Veloci and library/ (except for the aforementioned corner case).
projects / helm.git / log