]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoNever commit before trying to compile... stupid typo fixed.
Claudio Sacerdoti Coen [Tue, 13 May 2008 17:07:07 +0000 (17:07 +0000)]
Never commit before trying to compile... stupid typo fixed.

16 years agoUsed old kernel exception in place of brand new one.
Claudio Sacerdoti Coen [Tue, 13 May 2008 17:05:08 +0000 (17:05 +0000)]
Used old kernel exception in place of brand new one.

16 years ago- is_closed removed from the kernel (it used to make a loose test, replaced
Claudio Sacerdoti Coen [Tue, 13 May 2008 16:53:33 +0000 (16:53 +0000)]
- is_closed removed from the kernel (it used to make a loose test, replaced
  with a tighter one)
- does_not_occur no longer calls lift (performance improvement)
- does_not_occur: bug fixed in management of Metas

16 years agoLibrary factorized out.
Claudio Sacerdoti Coen [Tue, 13 May 2008 16:51:14 +0000 (16:51 +0000)]
Library factorized out.

16 years agowrong test equality only fixed
Enrico Tassi [Tue, 13 May 2008 16:47:54 +0000 (16:47 +0000)]
wrong test equality only fixed

16 years agoType of conjecture and subst_entry made uniform.
Claudio Sacerdoti Coen [Tue, 13 May 2008 10:41:53 +0000 (10:41 +0000)]
Type of conjecture and subst_entry made uniform.

16 years agoconvertibility was taking a metasenv but not using it
Enrico Tassi [Tue, 13 May 2008 10:01:10 +0000 (10:01 +0000)]
convertibility was taking a metasenv but not using it

16 years agoAdded boolean "is_inductive" to NReference.Ind
Claudio Sacerdoti Coen [Tue, 13 May 2008 09:40:21 +0000 (09:40 +0000)]
Added boolean "is_inductive" to NReference.Ind

16 years agotrust is always false by default
Claudio Sacerdoti Coen [Mon, 12 May 2008 21:41:57 +0000 (21:41 +0000)]
trust is always false by default

16 years agotrust implemented, but in the nCicTypeChecker!
Claudio Sacerdoti Coen [Mon, 12 May 2008 21:41:02 +0000 (21:41 +0000)]
trust implemented, but in the nCicTypeChecker!

16 years agoNew implementation of CicEnvironment:
Claudio Sacerdoti Coen [Mon, 12 May 2008 21:24:11 +0000 (21:24 +0000)]
New implementation of CicEnvironment:
 a) I have splitted out nCicLibrary from nCicEnvironment
 b) Recursion changed: the nCicTypechecker now registers itself to the
    nCicEnvironment. Then it is the nCicEnvironment.get_obj that retrieves
    an object from the library before calling the registered typecheck_obj
 c) The logger is now called every time NCicTypechecker.get_obj is invoked,
    both by the nCicEnvironment and by another module

TODO: implement trustness

16 years agoheight is stored in the reference, no need to fetch the object from the environment
Enrico Tassi [Mon, 12 May 2008 15:11:14 +0000 (15:11 +0000)]
height is stored in the reference, no need to fetch the object from the environment

16 years agofixed english
Enrico Tassi [Sat, 10 May 2008 11:54:26 +0000 (11:54 +0000)]
fixed english

16 years agovalid xml
Enrico Tassi [Sat, 10 May 2008 11:53:00 +0000 (11:53 +0000)]
valid xml

16 years ago...
Enrico Tassi [Sat, 10 May 2008 10:49:58 +0000 (10:49 +0000)]
...

16 years ago...
Enrico Tassi [Sat, 10 May 2008 10:48:22 +0000 (10:48 +0000)]
...

16 years agoreleased 0.5.0
Enrico Tassi [Sat, 10 May 2008 10:39:29 +0000 (10:39 +0000)]
released 0.5.0

16 years ago...
Enrico Tassi [Sat, 10 May 2008 10:28:29 +0000 (10:28 +0000)]
...

16 years ago...
Enrico Tassi [Sat, 10 May 2008 10:27:59 +0000 (10:27 +0000)]
...

16 years agosome files orphaned
Enrico Tassi [Sat, 10 May 2008 10:14:42 +0000 (10:14 +0000)]
some files orphaned

16 years ago...
Enrico Tassi [Fri, 9 May 2008 16:45:03 +0000 (16:45 +0000)]
...

16 years agoa missing prime
Enrico Tassi [Fri, 9 May 2008 12:05:57 +0000 (12:05 +0000)]
a missing prime

16 years agoBug fixed: the domain of a LetRec was only made by the last function in the
Claudio Sacerdoti Coen [Fri, 9 May 2008 11:40:29 +0000 (11:40 +0000)]
Bug fixed: the domain of a LetRec was only made by the last function in the
mutual block.

16 years agoUpdate after some more bug fixing.
Claudio Sacerdoti Coen [Wed, 7 May 2008 22:43:37 +0000 (22:43 +0000)]
Update after some more bug fixing.

16 years agoPartially reverted bad merge by Enrico that re-introduced an un-conditioned
Claudio Sacerdoti Coen [Wed, 7 May 2008 22:01:04 +0000 (22:01 +0000)]
Partially reverted bad merge by Enrico that re-introduced an un-conditioned
whd in guarded_by_destructors.

16 years agoMore bugs fixed.
Claudio Sacerdoti Coen [Mon, 5 May 2008 21:01:37 +0000 (21:01 +0000)]
More bugs fixed.

16 years agoget_check_fix and cofix unified, bug regarding debruijnation of constructors types...
Enrico Tassi [Mon, 5 May 2008 17:02:26 +0000 (17:02 +0000)]
get_check_fix and cofix unified, bug regarding debruijnation of constructors types fixed everywhere.
the constructor typs are debruinated wrt some inductive type uri an not wrt
their own, thus a wrong context was created. guarded by constructors ported from the old kernel.

16 years agoget_checked_indtys can take a constructor reference
Enrico Tassi [Mon, 5 May 2008 16:43:04 +0000 (16:43 +0000)]
get_checked_indtys can take a constructor reference

16 years agoadded mk_cofix
Enrico Tassi [Mon, 5 May 2008 16:42:12 +0000 (16:42 +0000)]
added mk_cofix

16 years agolet corec
Enrico Tassi [Mon, 5 May 2008 16:41:52 +0000 (16:41 +0000)]
let corec

16 years agoCoFix cache implemented
Enrico Tassi [Mon, 5 May 2008 16:41:39 +0000 (16:41 +0000)]
CoFix cache implemented

16 years agofix_left_in_constr still broken, ask enrico
Enrico Tassi [Mon, 5 May 2008 13:40:34 +0000 (13:40 +0000)]
fix_left_in_constr still broken, ask enrico

16 years agoguarded_by_constructors implemented, some cleanup here and there.
Enrico Tassi [Mon, 5 May 2008 13:34:10 +0000 (13:34 +0000)]
guarded_by_constructors implemented, some cleanup here and there.
fix_lefts_in_constr fixed: the inductive type list was returned with
constructors instantiated and debruijned, but with types whose arity was
instantiated with lefts too. This is wrong since we want to use these types to
build a context, that is closed, and will be put at the end of the actual
context since debruijn will make uris point to those terms

16 years agoremoved dead code
Enrico Tassi [Mon, 5 May 2008 13:31:59 +0000 (13:31 +0000)]
removed dead code

16 years ago...
Enrico Tassi [Mon, 5 May 2008 11:40:57 +0000 (11:40 +0000)]
...

16 years agoBug fixed in handling of explicit named substitutions: it could happen that
Claudio Sacerdoti Coen [Sat, 3 May 2008 21:31:45 +0000 (21:31 +0000)]
Bug fixed in handling of explicit named substitutions: it could happen that
explicit named substitution are merged not in the expected order. This happens
comparing the case of an instantiation inside and outside a (nested) section.
Thus I have added back the re-ordering of the explicit named substitution in
CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have
added to CicTypechecker.type_of_aux' the check that verifies if an explicit
named substitution is ordered.

16 years agoBroken XML files either fixed or removed.
Claudio Sacerdoti Coen [Sat, 3 May 2008 14:52:17 +0000 (14:52 +0000)]
Broken XML files either fixed or removed.

16 years agoSome destruct tactics got broken after last update. Small axiomatization
Wilmer Ricciotti [Fri, 2 May 2008 13:40:56 +0000 (13:40 +0000)]
Some destruct tactics got broken after last update. Small axiomatization
still included.

16 years agoMore precise classification of failures.
Claudio Sacerdoti Coen [Thu, 1 May 2008 17:31:31 +0000 (17:31 +0000)]
More precise classification of failures.

16 years agoList of all URIS comprising:
Claudio Sacerdoti Coen [Thu, 1 May 2008 17:30:20 +0000 (17:30 +0000)]
List of all URIS comprising:
 - coq objects
 - matita standard library
 - all matita tests and matita contribs that compile today

16 years agoMore options can now be set at the beginning of the file.
Claudio Sacerdoti Coen [Thu, 1 May 2008 17:16:10 +0000 (17:16 +0000)]
More options can now be set at the beginning of the file.

16 years agoLast (???) bug about variables with bodies fixed: we do no longer create
Claudio Sacerdoti Coen [Thu, 1 May 2008 14:11:07 +0000 (14:11 +0000)]
Last (???) bug about variables with bodies fixed: we do no longer create
applications with less than 2 args.

16 years agoAnother case where the presence of variables with bodies resulted in the
Claudio Sacerdoti Coen [Thu, 1 May 2008 13:59:06 +0000 (13:59 +0000)]
Another case where the presence of variables with bodies resulted in the
creation of an application without arguments.

16 years agotagging 0.5.0-rc1
Enrico Tassi [Thu, 1 May 2008 12:44:26 +0000 (12:44 +0000)]
tagging 0.5.0-rc1

16 years agoBug fixed: application without arguments generated in case of an ens made only
Claudio Sacerdoti Coen [Thu, 1 May 2008 10:57:00 +0000 (10:57 +0000)]
Bug fixed: application without arguments generated in case of an ens made only
of variables with bodies.

16 years agoNew bug found.
Claudio Sacerdoti Coen [Thu, 1 May 2008 10:45:19 +0000 (10:45 +0000)]
New bug found.

16 years agoThings are getting better.
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 23:33:38 +0000 (23:33 +0000)]
Things are getting better.

16 years agoImplementation of guarded_by_destructor is now complete w.r.t. the old kernel:
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 23:12:21 +0000 (23:12 +0000)]
Implementation of guarded_by_destructor is now complete w.r.t. the old kernel:
 a) bug fixed in eat_lambdas_etc: we cannot apply the term to the residual
    arguments since these are not left arguments
 b) when the recursive argument of the nested "let rec" is safe, the formal
    argument can also be considered safe.

TODO:
This implementation of condition b) could be improved by re-writing eat_lambdas
in such a way that it uses a shift_k function to add the context item to the
"context".

16 years agoReducing an open term should not be an error (or should it be???) and it
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 22:51:05 +0000 (22:51 +0000)]
Reducing an open term should not be an error (or should it be???) and it
should not raise Failure (that's for sure!).

16 years agostupid error fixed
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 21:38:26 +0000 (21:38 +0000)]
stupid error fixed

16 years agofixed_args fixed to accept passing a partially applied fix to a fix that
Claudio Sacerdoti Coen [Wed, 30 Apr 2008 20:50:58 +0000 (20:50 +0000)]
fixed_args fixed to accept passing a partially applied fix to a fix that
passes itself partially applied to anothere fix

16 years agoadded check on all bodies, only the one we actually encountered is applied to all...
Enrico Tassi [Wed, 30 Apr 2008 19:42:34 +0000 (19:42 +0000)]
added check on all bodies, only the one we actually encountered is applied to all arguments, other boedies are applied only up to j

16 years agoadded fake uri when the univ is anon
Enrico Tassi [Wed, 30 Apr 2008 19:04:28 +0000 (19:04 +0000)]
added fake uri when the univ is anon

16 years agofixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies...
Enrico Tassi [Wed, 30 Apr 2008 17:02:00 +0000 (17:02 +0000)]
fixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies in parallel, not just the i-th

16 years agouniverses are written with the URI inside objects, this allows
Enrico Tassi [Wed, 30 Apr 2008 15:50:06 +0000 (15:50 +0000)]
universes are written with the URI inside objects, this allows
universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!

16 years agoxml strict!
Enrico Tassi [Wed, 30 Apr 2008 10:53:27 +0000 (10:53 +0000)]
xml strict!

16 years agomany pending modifications were there, now the website at least validates
Enrico Tassi [Wed, 30 Apr 2008 10:46:54 +0000 (10:46 +0000)]
many pending modifications were there, now the website at least validates

16 years agoguarded_by_destructors on steroids
Enrico Tassi [Wed, 30 Apr 2008 10:17:34 +0000 (10:17 +0000)]
guarded_by_destructors on steroids

  when Fix/i args and some args are not guarded
  1) fixed params in interval 0..i are checked for bewing just passed around
  2) the fix is unfolded, debruijned, fixed arguments substituted,
     not fixed arguments pushed and checked for guardednes
  3) a new function with relative fixed arguments (not to be checked again)
     is added to k
  4) the resulting term is applied to the remaining arguments

  testcase: cic:/Suresnes/MiniC/MiniC/State/sizeOfType.con

16 years agoadded list_mapi
Enrico Tassi [Wed, 30 Apr 2008 10:14:23 +0000 (10:14 +0000)]
added list_mapi

16 years agoTests status update.
Claudio Sacerdoti Coen [Tue, 29 Apr 2008 14:58:22 +0000 (14:58 +0000)]
Tests status update.

16 years agospeedup in fixing the graph closures
Enrico Tassi [Tue, 29 Apr 2008 10:18:56 +0000 (10:18 +0000)]
speedup in fixing the graph closures

16 years agoAvoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Claudio Sacerdoti Coen [Mon, 28 Apr 2008 17:52:04 +0000 (17:52 +0000)]
Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).

16 years agoIn guarded by destructors, avoid computing the (whd ~delta:true) unless the
Claudio Sacerdoti Coen [Mon, 28 Apr 2008 17:43:33 +0000 (17:43 +0000)]
In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con

16 years agoUpdate...
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 17:08:25 +0000 (17:08 +0000)]
Update...

16 years agoNo more bugs on guarded_by_constructors in the old kernel.
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 16:23:53 +0000 (16:23 +0000)]
No more bugs on guarded_by_constructors in the old kernel.

16 years agoWhen going under a binder, a term must be converted twice, as explained in the
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 16:22:17 +0000 (16:22 +0000)]
When going under a binder, a term must be converted twice, as explained in the
previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.

16 years agoProof of adequacy.
Wilmer Ricciotti [Thu, 24 Apr 2008 15:55:21 +0000 (15:55 +0000)]
Proof of adequacy.

16 years agoguarded_by_constructor completely rewritten, fixed missing lift when generating the...
Enrico Tassi [Thu, 24 Apr 2008 13:01:26 +0000 (13:01 +0000)]
guarded_by_constructor completely rewritten, fixed missing lift when generating the context of an inductive type in guarded_by_destructors.

16 years agoadded coinductive example
Enrico Tassi [Thu, 24 Apr 2008 13:00:21 +0000 (13:00 +0000)]
added coinductive example

16 years agoWorking and broken URIs.
Claudio Sacerdoti Coen [Thu, 24 Apr 2008 12:56:14 +0000 (12:56 +0000)]
Working and broken URIs.

16 years agoported the instantiate-left-params-to-calculate-rec-args patch from the old to the...
Enrico Tassi [Wed, 23 Apr 2008 16:41:37 +0000 (16:41 +0000)]
ported the instantiate-left-params-to-calculate-rec-args patch from the old to the new kernel,
to test the patch properly some steps of substitution inside a possibly blocked fix are performed,
this should be in general avoided without good checks (still to understand)

16 years agoAvoid other comparisons on universes using =.
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:17:26 +0000 (08:17 +0000)]
Avoid other comparisons on universes using =.

16 years agoAvoid code duplication.
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:09:39 +0000 (08:09 +0000)]
Avoid code duplication.

16 years agoDo NOT dare using Pervasives.compare on data structures containing URIs!
Claudio Sacerdoti Coen [Wed, 23 Apr 2008 08:04:53 +0000 (08:04 +0000)]
Do NOT dare using Pervasives.compare on data structures containing URIs!
Use UriManager.compare to get a 2x speed-up in type-checking setoids.

16 years agooblivion ugraph everywhere outside the kernel
Enrico Tassi [Tue, 22 Apr 2008 19:18:53 +0000 (19:18 +0000)]
oblivion ugraph everywhere outside the kernel

16 years agoslow_implementation and some dead code removed
Enrico Tassi [Tue, 22 Apr 2008 13:44:27 +0000 (13:44 +0000)]
slow_implementation and some dead code removed

16 years agomore strict check by CSC, I miss it
Enrico Tassi [Tue, 22 Apr 2008 13:28:10 +0000 (13:28 +0000)]
more strict check by CSC, I miss it

16 years agofix cache comparison relaxed to URI and not REFERENCE
Enrico Tassi [Tue, 22 Apr 2008 12:50:33 +0000 (12:50 +0000)]
fix cache comparison relaxed to URI and not REFERENCE

16 years agoadded a call to ppcontext in the case of appl, to ease the localization of the error
Enrico Tassi [Tue, 22 Apr 2008 12:48:10 +0000 (12:48 +0000)]
added a call to ppcontext in the case of appl, to ease the localization of the error

16 years agoadded ppcontext
Enrico Tassi [Tue, 22 Apr 2008 12:47:31 +0000 (12:47 +0000)]
added ppcontext

16 years agoTypes for LetIns computed during parsing for Coq objects may contain universes
Claudio Sacerdoti Coen [Tue, 22 Apr 2008 09:41:34 +0000 (09:41 +0000)]
Types for LetIns computed during parsing for Coq objects may contain universes
that must be made fresh.

16 years agodefn2.ma is to be used with part1a_inversion3
Claudio Sacerdoti Coen [Mon, 21 Apr 2008 17:20:43 +0000 (17:20 +0000)]
defn2.ma is to be used with part1a_inversion3
the induction/inversion lemma in part1a_inversion3 is more regular w.r.t.
 the meta-theory
automation pushed to its limits in part1a_inversion3.ma

16 years agofix universe handling, newly encountered objects are typed in an empty ugraph
Enrico Tassi [Mon, 21 Apr 2008 09:19:23 +0000 (09:19 +0000)]
fix universe handling, newly encountered objects are typed in an empty ugraph
that after the cleanup phase is committed into the cic_environement and merged
with the current one.

minor reformatting of sources and some more for_all

16 years agoAlternative prove using just one induction/inversion principle.
Claudio Sacerdoti Coen [Sun, 20 Apr 2008 21:32:11 +0000 (21:32 +0000)]
Alternative prove using just one induction/inversion principle.

16 years agobetter error message
Enrico Tassi [Sat, 19 Apr 2008 16:33:26 +0000 (16:33 +0000)]
better error message

16 years ago...
Enrico Tassi [Sat, 19 Apr 2008 16:32:53 +0000 (16:32 +0000)]
...

16 years agoimpredicative set work around
Enrico Tassi [Sat, 19 Apr 2008 16:32:36 +0000 (16:32 +0000)]
impredicative set work around

16 years agoimpredicative set work around
Enrico Tassi [Sat, 19 Apr 2008 16:32:22 +0000 (16:32 +0000)]
impredicative set work around

16 years agoassociativity of -> fixed
Enrico Tassi [Sat, 19 Apr 2008 16:30:53 +0000 (16:30 +0000)]
associativity of -> fixed

16 years agoancient graph regarding universes and trust=false, universes calculated for internal...
Enrico Tassi [Sat, 19 Apr 2008 16:30:21 +0000 (16:30 +0000)]
ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object

16 years agoextlib list_uniq instead of local copy
Enrico Tassi [Sat, 19 Apr 2008 16:27:57 +0000 (16:27 +0000)]
extlib list_uniq instead of local copy

16 years agoranking function fixed: when graphs are collapsed one step links are not updated...
Enrico Tassi [Sat, 19 Apr 2008 16:27:28 +0000 (16:27 +0000)]
ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk)
thus you can not rely on them, just use the closures!

16 years agoadded flag to change Set into Type on the fly, that helps on some coq objects using...
Enrico Tassi [Sat, 19 Apr 2008 16:26:21 +0000 (16:26 +0000)]
added flag to change Set into Type on the fly, that helps on some coq objects using impredicative set

16 years agooblivion_ugraph => empty_ugraph
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 11:13:05 +0000 (11:13 +0000)]
oblivion_ugraph => empty_ugraph

16 years agoAdded to flags to activate/disactivate pretty-printing and exception catching.
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 10:52:50 +0000 (10:52 +0000)]
Added to flags to activate/disactivate pretty-printing and exception catching.

16 years agoUris must be stripped of their xpointers.
Claudio Sacerdoti Coen [Sat, 19 Apr 2008 09:20:24 +0000 (09:20 +0000)]
Uris must be stripped of their xpointers.

16 years agoDead code removed.
Claudio Sacerdoti Coen [Fri, 18 Apr 2008 18:31:58 +0000 (18:31 +0000)]
Dead code removed.

16 years agoInversion lemma for Forall.
Claudio Sacerdoti Coen [Fri, 18 Apr 2008 18:27:43 +0000 (18:27 +0000)]
Inversion lemma for Forall.

16 years agoworkaround for Pi associativity
Enrico Tassi [Fri, 18 Apr 2008 16:58:38 +0000 (16:58 +0000)]
workaround for Pi associativity

16 years agoworkaround for some Set/Type problems
Enrico Tassi [Fri, 18 Apr 2008 16:50:10 +0000 (16:50 +0000)]
workaround for some Set/Type problems