- content/interpretations.ml and ng_cic_content/nTermCicContent.ml where
mutually recursive and part of the status was kept imperatively;
the two files have been merged together into ng_cic_content/interpretations.ml
Andrea Asperti [Thu, 4 Nov 2010 13:36:47 +0000 (13:36 +0000)]
- Print/Set commands removed
- stupid bug fixed in interpretations: we did not add the new id to the
id list, so that only the first interpretation was considered
- added a new field to the interpretations status to record the recently
added aliases that need to be made explicit in the script; much better
than what we did before (alias diffing)
Ferruccio Guidi [Wed, 3 Nov 2010 21:02:44 +0000 (21:02 +0000)]
last commit for helena 0.8.1
- xsl : we can render the levels of the abstractions
- ccs : we output three kinds of constraints
- Makefiles: we automatized the relising process
- brgCrg : all abstractions have infinite level for now
Ferruccio Guidi [Tue, 2 Nov 2010 22:06:52 +0000 (22:06 +0000)]
- the connections between the intermediate language and the "bag"
kernel were missing
- the connections between the intermediate language and the "bag"
kernel are now tail recursive
- the dtd now declares the "level" attribute
- some "assert false" removed in crg
- xml exportation of the data processed by the "bag" kernel is now
available
- the "bag" kernel now uses Entity names rather than identifiers
Andrea Asperti [Fri, 29 Oct 2010 11:27:11 +0000 (11:27 +0000)]
- grammar of // changed to move the justification inside;
reason: that brain damaged piece of software that is CAMLP5 does a
lookahead and then it forgets to rollback the token (why??? is it
a bug). As a consequence matita used to work (since it parses a
statement at a time), but not matitac (since the lookahead destroyed
the next command)
- core_notation.moo: \frac used to be at level 90, but this is incorrect
during parsing and incompatible with the new syntax; \frac is now
used only in output
- minor dead code removal here and there
Enrico Tassi [Tue, 19 Oct 2010 13:25:32 +0000 (13:25 +0000)]
camlp5 probably changed some internal data structures and now they cannot be compared with pervasives.comapre, thus we avoid it. Was breaking the natural deduction stuff
Enrico Tassi [Sun, 17 Oct 2010 09:08:05 +0000 (09:08 +0000)]
new case for higher order unification:
(? ?) =?= (f x)
is not handled by delift, since flexible arguments in the local context
are skipped by delift, resulting in the instantiation of the head meta to
a constant function, even if the rhs is structurally the same.
Andrea Asperti [Fri, 8 Oct 2010 10:30:47 +0000 (10:30 +0000)]
- hmysql removed (RIP)
- library simplified to handle only new files, moo and lexicon
- BROKEN FEATURES: recursive decompilation of library files is currently
broken since, without the db, there is currently no way to compute the
reverse dependencies
1)
===========
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example
Hint: And A B === fun_of_morph And_morphism A B
If the problem
And A B =?= fun_of_morph ? A B
is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve
And =?= fun_of_morph ?
While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.
2)
===========
The fo_unif function does some clever higher order unification in the
case
(? x1 ... xn) =?= (t y1 ... ym)
but in the very similar case
K (? x1 ... xn) _ =?= (t y1 ... ym)
it does not.
K has to be reduced away, and afterwards the KAM configuration
has ? and t as heads, xs and ys on the stack. Assume m-n=l, the
unification problems generated by the check_stack function are
? =?= t y1 .. yl
xi =?= yl+i for i in 1 .. n
That is clearly suboptimal, since xn and ym could differ, but a clever
instantiation of the flexible head could drop or move around xm.
Moreover one expects the two unification problems to be solved in the
same way by the system, but it does not, and in my case the second one
actually fails. The KAM code should just be a speedup over a naive
unfolding of constants, beta-iota-zeta reduction and fo_unif, but in
this (unfortunate) case it is weaker.
3)
============
The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.
1)
===========
It is an old and know issue. The check_stack calls fo_unif_w_hints only
on a prefix of applications, leaving some arguments on the stack. This
prevents hints to be found. Example
Hint: And A B === fun_of_morph And_morphism A B
If the problem
And A B =?= fun_of_morph ? A B
is found immediately (before entering the KAM) the it is solved, but if
it shows up inside the KAM, A and B are left on the stack and a
fo_unif_w_hints has to solve
And =?= fun_of_morph ?
While one could declare hints multiple times, varying the number of
actual arguments, I believe that the right solution is to make the
KAM code pass more information to fo_unif_w_hints, like the remaining
arguments. Nevertheless, the new fo_unif_w_hints is hard to factor with
the old one (that is used elsewere) so I wrote a new one called
fo_unif_heads_and_cont_or_unwind_and_hints. It first tries fo_unif on
the heads, and if successfull call a continuation (that will unify
all stack arguments pairwise) or unwinds the machine and looks for hints
on the complete terms, not just a prefix.
2)
===========
The fo_unif function does some clever higher order unification in the
case
(? x1 ... xn) =?= (t y1 ... ym)
but in the very similar case
K (? x1 ... xn) _ =?= (t y1 ... ym)
it does not.
K has to be reduced away, and afterwards the KAM configuration
has ? and t as heads, xs and ys on the stack. Assume m-n=l, the
unification problems generated by the check_stack function are
? =?= t y1 .. yl
xi =?= yl+i for i in 1 .. n
That is clearly suboptimal, since xn and ym could differ, but a clever
instantiation of the flexible head could drop or move around xm.
Moreover one expects the two unification problems to be solved in the
same way by the system, but it does not, and in my case the second one
actually fails. The KAM code should just be a speedup over a naive
unfolding of constants, beta-iota-zeta reduction and fo_unif, but in
this (unfortunate) case it is weaker.
3)
============
The delift function does a lot of work even if the metavariable is being
instantiated with a closed term. This is very often the case when the
term is suggested by hints. Hints may suggest constants in partially
unfolded form (see paper submitted to Type09), that can thus be very
big. This simple patch speeds up delift in this case.
projects / helm.git / log