The pretty printers in CicPp now have an optional ~metasenv argument to
show the globally restricted arguments of a metavariable local context as
locally restricted. The pretty printers in CicMetaSubst have the same argument,
but the argument is mandatory.
Enrico Zoli [Fri, 10 Nov 2006 18:06:13 +0000 (18:06 +0000)]
Dama: up to L-spaces and the proof (completed up to properties of the
absolute value) that every complete integration riesz space is an L-space.
Now the plan is to prove the Lebesgue dominated convergence theorem for
L-spaces as Fremlin does and to build a model of them later on as suggested
by Spitters. Note: the proof of the theorem by Spitters is almost trivial
because it really exploits the fact the L0 is the (Cauchy) completion of L1.
The proof by Fremlin is much more general since it does not assume anything
more on L-spaces.
Note: we could also prove that every L-space is archimedean.
Enrico Zoli [Mon, 6 Nov 2006 18:43:24 +0000 (18:43 +0000)]
More work on groups, real numbers and integration algebras.
Up to a thousand of unproved lemmas, we have the result that the
distance induced by the integral on an integration Riesz space is
a distance. The next step is to axiomatise an L-space (an integration
Riesz space complete w.r.t. the induced distance).
Bug fixed: the disambiguation domain for a record with left parameters was
not obtained with a pre-visit. The result was that often Failures were detected
later than possible with consequent waste of time.
Critical bug finally found after a long chasing!!!
When looking for a coercion over a non meta closed term, often the case was
not detected and a Failure was raised instead of Uncertain.
Enrico Zoli [Fri, 3 Nov 2006 16:58:51 +0000 (16:58 +0000)]
Integration f_algebras declassed.
We suppose to prove everything on integration_riesz_spaces.
However, the definition or weak order unit is complex because of the sup
on sequences.
Enrico Zoli [Tue, 31 Oct 2006 18:23:36 +0000 (18:23 +0000)]
We begin to play the real game: we have defined real numbers and
constructive connectives (only the disjunction for now) and we are
trying to define the max between two real numbers as the limit of a
particular cauchy sequence. Cool.
remove_obj is now much faster:
1. the code was utterly messy, trying to remove from the DB files and
to remove from disk #xpointer uris.
2. LIKE substituted by =
3. added QUICK and LOW_PRIORITY to the DELETE statement
4. removed unuseful and unused debugging code that used to slow down every
deletion
GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
applications of applications (that are forbidden and not handled properly).
1. is_meta_closed should be applied only to terms on which a substitution
has already been applied. Fixed here and there.
Note: it is not possible to add a subst parameter to is_meta_closed since
the function is declared in cic/CicUtil and it is used where the unification
is not available (e.g. in whelp and library)
2. known (but never verified before) bug fixed: delifting should fail
(instead of raising Uncertain) iff the local context is not meta_closed.
The test used to be "does not contain a Meta"
1. bug fixed: Unicode characters that are not mapped to TeX macros used to
be post-fixed with a blank
2. bug fixed: the textual pretty-printer does not implement the same
spacing politics of GtkMathView. Since that politics is very very complex
to implement, I try a different solution: we explicitly insert a space
where we want one. The widget does not seem to be disturbed by this.
This way the let ... rec and match ... with constructs are now printed
correctly and they can be read back.
3. syntax change: applicative patterns no longer require parentheses around
them
Our unification used to guess a very complex argument of an apply in
fermat_little_theorem. It does no longer, but the old behaviour seems to be
really lucky. Thus I change the .ma file.
Andrea Asperti [Fri, 20 Oct 2006 15:32:34 +0000 (15:32 +0000)]
a. uniform mangement for context and library
b. collapsing flexible terms (X args) into a single meta. Metas in
head position give arity problems with discrimination trees.
c. Even terms with a single meta as conlcusion (e.g. elimination
principles) get indexed.
Andrea Asperti [Fri, 20 Oct 2006 14:50:40 +0000 (14:50 +0000)]
This is only a temporary patch. The typecheker raises a
CicUniv.UniverseInconsistency that should be properly
captured and transformed into a tyepchecking error.
Potential performance improvement + better disambiguation error messages:
the delift functions used to raise Uncertain every time it failed; now it
raises Failure when the local context contains no Metas (that means that
for every future subst it will not contain new Rels).
Note: if we are working up to conversion (I do not think so), we should check
that the local context is Meta-closed, that is a weaker check.
Missing optimization implemented: before starting to analyze the disambiguation
domain we try first without interpreting any symbol. This way we can avoid
lot of refinements when the information in the uninterpreted term already
tells us that every instance will not be well typed.
- Disambiguation error exception enriched with more information
(the same returned in case of correct disambiguation)
- The disambiguation error interface now shows the complete environment
in which the error occurs. I am not sure if this is better or worst than
showing only the diffs.
Bug fixed: the diff component of the exception raised when the term cannot
be disambiguated used to lack the last choice in case of the look-ahead
optimization.
Enrico Tassi [Thu, 12 Oct 2006 13:34:32 +0000 (13:34 +0000)]
timeout if unspecfied should be set to infinity, not 0, since the timeout inside the flagfs structure is a time in the future, not a decreasing quantity.
every loop of auto the check gettimeofday() > timeout raise Fail
projects / helm.git / log