]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years ago...
Claudio Sacerdoti Coen [Sun, 18 May 2008 21:29:29 +0000 (21:29 +0000)]
...

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 21:00:31 +0000 (21:00 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agorun fsub during night
Enrico Tassi [Sun, 18 May 2008 20:51:26 +0000 (20:51 +0000)]
run fsub during night

16 years agoBug fixed: when computing the left arguments, I was not doing the right thing.
Claudio Sacerdoti Coen [Sun, 18 May 2008 20:51:15 +0000 (20:51 +0000)]
Bug fixed: when computing the left arguments, I was not doing the right thing.

New check implemented: references should cache data correctly.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 20:06:29 +0000 (20:06 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:56:38 +0000 (19:56 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:30:44 +0000 (19:30 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agonames fixed accoding to the new ones generated after arity of
Enrico Tassi [Sun, 18 May 2008 19:29:56 +0000 (19:29 +0000)]
names fixed accoding to the new ones generated after arity of
indtypes is not cleaned for dummy names

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:22:55 +0000 (19:22 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:14:34 +0000 (19:14 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 19:04:18 +0000 (19:04 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agorevert last commit, context' -> context (added comment)
Enrico Tassi [Sun, 18 May 2008 19:03:13 +0000 (19:03 +0000)]
revert last commit, context' -> context (added comment)

16 years agousing the right names in the context to check match patterns(better error report...
Enrico Tassi [Sun, 18 May 2008 18:37:28 +0000 (18:37 +0000)]
using the right names in the context to check match patterns(better error report) and use the refined matched term to compute the type

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:31:45 +0000 (18:31 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:22:24 +0000 (18:22 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 18:19:39 +0000 (18:19 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:55:16 +0000 (17:55 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoNew missing check implemented: the left parameters of each constructor and
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:49:57 +0000 (17:49 +0000)]
New missing check implemented: the left parameters of each constructor and
inductive types should be convertible and should have the very same name.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:46:38 +0000 (17:46 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent types are no longer cleaned in inductive type arities.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:44:51 +0000 (17:44 +0000)]
Dummy dependent types are no longer cleaned in inductive type arities.

16 years agoDummy dependent products in inductive types arities are no longer cleaned.
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:38:47 +0000 (17:38 +0000)]
Dummy dependent products in inductive types arities are no longer cleaned.

16 years agoThis commit avoids cleaning dummy dependent types in the arities of inductive
Claudio Sacerdoti Coen [Sun, 18 May 2008 17:31:41 +0000 (17:31 +0000)]
This commit avoids cleaning dummy dependent types in the arities of inductive
types. This is an overkilling solution to the problem of avoiding cleaning
dummy dependent types in the left products in the arities of inductive types.
The left products should be _syntactically_ the same as those of the
constructors. Otherwise, error reporting is incorrect.

16 years agoImplemented translation of inductive types from the new to the old format.
Claudio Sacerdoti Coen [Sun, 18 May 2008 08:16:55 +0000 (08:16 +0000)]
Implemented translation of inductive types from the new to the old format.

16 years agoSerious bug fixed: the max of two universes was computed using the polymorphic
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:52:55 +0000 (07:52 +0000)]
Serious bug fixed: the max of two universes was computed using the polymorphic
max function of OCaml instead of append!!!

16 years agoSynch with the paper.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:49:20 +0000 (07:49 +0000)]
Synch with the paper.

16 years ago...
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:42:05 +0000 (07:42 +0000)]
...

16 years agoError message improved.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:30:14 +0000 (07:30 +0000)]
Error message improved.

16 years agoMore effective optimization: avoid introducing already implied arcs.
Claudio Sacerdoti Coen [Sun, 18 May 2008 07:25:38 +0000 (07:25 +0000)]
More effective optimization: avoid introducing already implied arcs.

16 years agoimpredicative Set is considered as Prop in the new check implemented by CSC
Enrico Tassi [Sat, 17 May 2008 18:50:09 +0000 (18:50 +0000)]
impredicative Set is considered as Prop in the new check implemented by CSC

16 years agoNew check implemented: the sort of each constructor should be constrained by
Claudio Sacerdoti Coen [Sat, 17 May 2008 18:02:51 +0000 (18:02 +0000)]
New check implemented: the sort of each constructor should be constrained by
the sort of its inductive type.

Note: I just realized that nobody implements the check that the left
abstractions of each constructors/inductive type must be exactly the same.
To be implemented.

16 years agoMissing check implemented: the sort of each constructors should be constrained
Claudio Sacerdoti Coen [Sat, 17 May 2008 17:57:58 +0000 (17:57 +0000)]
Missing check implemented: the sort of each constructors should be constrained
by the sort of its inductive type.

16 years agoThe file bug_universi.ma shows a strage case where the ranked universe
Claudio Sacerdoti Coen [Sat, 17 May 2008 15:26:44 +0000 (15:26 +0000)]
The file bug_universi.ma shows a strage case where the ranked universe
graph does not contain any universe for one object that does contain a
user-provided universe. In turns, this make check.ml fail (since no constraint
is defined between Type0, which occurs in the object, and Type1).

16 years agoMissing whd.
Claudio Sacerdoti Coen [Sat, 17 May 2008 15:05:41 +0000 (15:05 +0000)]
Missing whd.

16 years agoBug fixed: since circular <= graphs are allowed, added an avoid list to
Claudio Sacerdoti Coen [Sat, 17 May 2008 13:21:45 +0000 (13:21 +0000)]
Bug fixed: since circular <= graphs are allowed, added an avoid list to
avoid looping.
Even more code semplification.
Little optimization: adding x <= x does nothing

16 years agoBug fixed: only Type < Type1 was declared.
Claudio Sacerdoti Coen [Sat, 17 May 2008 13:19:22 +0000 (13:19 +0000)]
Bug fixed: only Type < Type1 was declared.

16 years agoBug fixed and further code semplification in management of universes.
Claudio Sacerdoti Coen [Sat, 17 May 2008 12:59:39 +0000 (12:59 +0000)]
Bug fixed and further code semplification in management of universes.

16 years agoThe code for universes was not correct in many borderline cases.
Claudio Sacerdoti Coen [Sat, 17 May 2008 11:14:46 +0000 (11:14 +0000)]
The code for universes was not correct in many borderline cases.
The new code should be correct. For sure, it is much simpler, shorter,
characterized by better invariants and its interface has less functions.

16 years agoranking reports the lest of univs
Enrico Tassi [Fri, 16 May 2008 17:07:06 +0000 (17:07 +0000)]
ranking reports the lest of univs

16 years agoadded new implementation of universes
Enrico Tassi [Fri, 16 May 2008 17:06:29 +0000 (17:06 +0000)]
added new implementation of universes

16 years agoadded name_of_uri
Enrico Tassi [Fri, 16 May 2008 16:03:01 +0000 (16:03 +0000)]
added name_of_uri

16 years agometa VS meta in alpha_eq honors substitution
Enrico Tassi [Fri, 16 May 2008 13:23:50 +0000 (13:23 +0000)]
meta VS meta in alpha_eq honors substitution

16 years agoused ind/coind information in references
Enrico Tassi [Fri, 16 May 2008 11:52:59 +0000 (11:52 +0000)]
used ind/coind information in references

16 years agotypes where compared without lookig at test_eq_only
Enrico Tassi [Fri, 16 May 2008 11:34:37 +0000 (11:34 +0000)]
types where compared without lookig at test_eq_only

16 years agoTimings
Claudio Sacerdoti Coen [Thu, 15 May 2008 21:40:45 +0000 (21:40 +0000)]
Timings

16 years ago(Approximated) inference of relevance implemented: an argument X of t is irrelevant
Enrico Tassi [Thu, 15 May 2008 17:04:07 +0000 (17:04 +0000)]
(Approximated) inference of relevance implemented: an argument X of t is irrelevant
if it has sort Prop and the sort of t is not Prop.

16 years agoFirst implementation of irrelevance in conversion.
Enrico Tassi [Thu, 15 May 2008 16:09:43 +0000 (16:09 +0000)]
First implementation of irrelevance in conversion.

16 years agoNew function get_relevance and new (not exported) function get_checked_decl.
Enrico Tassi [Thu, 15 May 2008 16:09:17 +0000 (16:09 +0000)]
New function get_relevance and new (not exported) function get_checked_decl.

16 years agoNew function list_forall_default3. 3 euros to the first one that reuses this function
Enrico Tassi [Thu, 15 May 2008 15:47:57 +0000 (15:47 +0000)]
New function list_forall_default3. 3 euros to the first one that reuses this function
(not artificially)

16 years agoBug fixed in computation of heights: a constant must have height greater than its...
Enrico Tassi [Thu, 15 May 2008 15:08:57 +0000 (15:08 +0000)]
Bug fixed in computation of heights: a constant must have height greater than its constant__s

16 years agoImplementation of calculation of heights.
Enrico Tassi [Thu, 15 May 2008 14:12:21 +0000 (14:12 +0000)]
Implementation of calculation of heights.

16 years agoTypo fixed.
Enrico Tassi [Thu, 15 May 2008 12:45:30 +0000 (12:45 +0000)]
Typo fixed.

16 years agoMajor code semplification and bugs removed (thanks to a better invariant):
Enrico Tassi [Thu, 15 May 2008 12:39:00 +0000 (12:39 +0000)]
Major code semplification and bugs removed (thanks to a better invariant):
small_delta_step always put the terms in WHNF, even if it can do that with delta > 0.
Terms in WHNF, delta=0 that are not head-alpha convertible and tail-machine convertible
are not convertible.

16 years agoRemoved two args from psubst.
Andrea Asperti [Thu, 15 May 2008 10:08:00 +0000 (10:08 +0000)]
Removed two args from psubst.

16 years agoheight of constants properly handled
Enrico Tassi [Thu, 15 May 2008 09:24:19 +0000 (09:24 +0000)]
height of constants properly handled

16 years agolist_iter2_default_value moved to HExtlib. 1 euro to the first one that will
Claudio Sacerdoti Coen [Wed, 14 May 2008 17:41:33 +0000 (17:41 +0000)]
list_iter2_default_value moved to HExtlib. 1 euro to the first one that will
re-use it (not artificially)

16 years agoeat_lambdas and eat_or_subst_lambdas taken out of the big recursion.
Claudio Sacerdoti Coen [Wed, 14 May 2008 17:16:07 +0000 (17:16 +0000)]
eat_lambdas and eat_or_subst_lambdas taken out of the big recursion.
In principle, we could move them to nCicUtils. Maybe this should be done.

16 years agodebruijn simplified. It could go in nCicUtils, but why should we do that?
Claudio Sacerdoti Coen [Wed, 14 May 2008 17:11:19 +0000 (17:11 +0000)]
debruijn simplified. It could go in nCicUtils, but why should we do that?

16 years agoBug fixed: types were check for conversion in the wrong context.
Claudio Sacerdoti Coen [Wed, 14 May 2008 16:49:25 +0000 (16:49 +0000)]
Bug fixed: types were check for conversion in the wrong context.

16 years agoWe forgot an important check: the declared and expected type in definitions in
Claudio Sacerdoti Coen [Wed, 14 May 2008 16:35:55 +0000 (16:35 +0000)]
We forgot an important check: the declared and expected type in definitions in
the context must be checked for convertibility.

16 years agopartial implementation of reduction up to a given height
Enrico Tassi [Wed, 14 May 2008 16:27:16 +0000 (16:27 +0000)]
partial implementation of reduction up to a given height

16 years agofixed error message
Enrico Tassi [Wed, 14 May 2008 16:26:41 +0000 (16:26 +0000)]
fixed error message

16 years agoNew checks for well-formedness of metasenvs and substs.
Claudio Sacerdoti Coen [Wed, 14 May 2008 16:06:45 +0000 (16:06 +0000)]
New checks for well-formedness of metasenvs and substs.

16 years agonuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved
Claudio Sacerdoti Coen [Wed, 14 May 2008 15:36:26 +0000 (15:36 +0000)]
nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved
to NCic2OCic or to OCic2NCic.\fThe kernel is now clean of conversion functions.

16 years agoNicer graph.
Claudio Sacerdoti Coen [Wed, 14 May 2008 15:07:54 +0000 (15:07 +0000)]
Nicer graph.

16 years agomap_hash moved to HExtlib
Claudio Sacerdoti Coen [Wed, 14 May 2008 15:01:31 +0000 (15:01 +0000)]
map_hash moved to HExtlib

16 years agoNew function map_hash.
Claudio Sacerdoti Coen [Wed, 14 May 2008 14:58:05 +0000 (14:58 +0000)]
New function map_hash.

16 years agoGeneration of dot file.
Claudio Sacerdoti Coen [Wed, 14 May 2008 14:55:57 +0000 (14:55 +0000)]
Generation of dot file.

16 years agoNew licence used uniformly everywhere.
Claudio Sacerdoti Coen [Wed, 14 May 2008 13:45:41 +0000 (13:45 +0000)]
New licence used uniformly everywhere.

16 years agowe added a link to lambda-delta home page in the hope that this page gets eventually...
Ferruccio Guidi [Tue, 13 May 2008 19:03:34 +0000 (19:03 +0000)]
we added a link to lambda-delta home page in the hope that this page gets eventually indexed by google :)

16 years agoOne more bug fixed: we tried to perform List.nth on negative indexes.
Claudio Sacerdoti Coen [Tue, 13 May 2008 17:32:34 +0000 (17:32 +0000)]
One more bug fixed: we tried to perform List.nth on negative indexes.

16 years agoMore exceptions captured.
Claudio Sacerdoti Coen [Tue, 13 May 2008 17:31:40 +0000 (17:31 +0000)]
More exceptions captured.

16 years agoBug fixed in pretty-printing of free Rels.
Claudio Sacerdoti Coen [Tue, 13 May 2008 17:27:08 +0000 (17:27 +0000)]
Bug fixed in pretty-printing of free Rels.

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