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).
librarian: improved error detection, bug fix in time comparison functions: now the object files are considered in the correct compilation order even if they mtime is the same :)
Procedural: improved error detection
1) as usual, I took the reverse notation for composition.
"fixed" according to the internatinal tradition
2) partial proof that basic_topologies form a category
cicDischarge, Procedural: we improved debugging and added some time stamps
librarian.ml: new algorithm for sorting sources according to compilation order
some work to make tries "printable", fixed comparison of constants in
paramodulation, added (but commented) a call to auto after every tactic
invocation to test it on the whole library.
cicDischarge: we still have some problems here. Some fixes
cicTypeChecker: added some debug prints (commented for now)
applyTransformation.ml: improved error detection
unification+pullback fix. It used to saturate a coercion (generating new metas)
but not do any unification steps on them nor using them to build a new term,
thus they were left in the metasenv with no chance to be closed by subsequent
calls to unification. The meets function has been specialized takin in input a
boolean for every direction (left/right) to state if the graph can grow in this
direction and it returns saturated coercions and augmented metasenv only for
the requested directions. Still unclear to me what does it mean to search a non
triangular pullback with a boolean set to false....
transcript: we improved the parser/lexer to read the scripts of the standard
library of coq. Coercion extraction is disabled for now.
contribs/procedural: new root for mma files generated by transcript.
We now have the mma files of the cic:/Coq/* objects
projects / helm.git / log