]> matita.cs.unibo.it Git - helm.git/log
helm.git
16 years agoadded a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now...
Enrico Tassi [Fri, 30 May 2008 09:12:51 +0000 (09:12 +0000)]
added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now is full whd

16 years agorelevance check partially implemented but bugged since cic:/matita/nat/compare/eqb...
Enrico Tassi [Thu, 29 May 2008 16:38:51 +0000 (16:38 +0000)]
relevance check partially implemented but bugged since cic:/matita/nat/compare/eqb.con is not ok!

16 years agocase not unfilding fixed
Enrico Tassi [Thu, 29 May 2008 16:34:08 +0000 (16:34 +0000)]
case not unfilding fixed

16 years agoCProp, since it was defined in CoRN as a Type, is predicative.
Enrico Tassi [Thu, 29 May 2008 16:27:26 +0000 (16:27 +0000)]
CProp, since it was defined in CoRN as a Type, is predicative.
However, it is not Type0, but a moving Type as usual, for example

  inductive and (A,B:CProp) : CProp := ...

  inductive exists (A:Type) (P:A->CProp) : CProp :=
   | ext : \forall x:A. \forall p : P x. exists A P.

does not pass since the sort of x is Type not included in CProp. Putting
exists in Type does not work either, if you want to make a conjuction
involving an existential.

solution, to be implemented:

  CProp of CicUniv.universe

where CProp n is meant to be Type (n + 0.5).

16 years ago0.5.1 released
Enrico Tassi [Thu, 29 May 2008 14:15:25 +0000 (14:15 +0000)]
0.5.1 released

16 years agounused variables removed
Enrico Tassi [Thu, 29 May 2008 12:28:32 +0000 (12:28 +0000)]
unused variables removed

16 years agoref sync check fixed controlling fix/cofix coherence
Enrico Tassi [Thu, 29 May 2008 11:51:14 +0000 (11:51 +0000)]
ref sync check fixed controlling fix/cofix coherence

16 years ago...
Enrico Tassi [Thu, 29 May 2008 11:38:44 +0000 (11:38 +0000)]
...

16 years agofirst page of the new dama proof
Enrico Tassi [Thu, 29 May 2008 09:51:22 +0000 (09:51 +0000)]
first page of the new dama proof

16 years ago...
Enrico Tassi [Thu, 29 May 2008 09:45:35 +0000 (09:45 +0000)]
...

16 years agothe type of the match was obtained reducing the outtype
Enrico Tassi [Thu, 29 May 2008 09:43:47 +0000 (09:43 +0000)]
the type of the match was obtained reducing the outtype
applied to right + matched with whd ~delta:true that
is not what you want. replaced with head_beta_reduce.

16 years ago...
Enrico Tassi [Wed, 28 May 2008 12:48:43 +0000 (12:48 +0000)]
...

16 years agodama restarted
Enrico Tassi [Wed, 28 May 2008 11:00:26 +0000 (11:00 +0000)]
dama restarted

16 years agocleanup
Enrico Tassi [Wed, 28 May 2008 10:40:54 +0000 (10:40 +0000)]
cleanup

16 years agothe attempt of completing dama using duality frozen
Enrico Tassi [Wed, 28 May 2008 10:39:13 +0000 (10:39 +0000)]
the attempt of completing dama using duality frozen

16 years ago0.5.1
Enrico Tassi [Wed, 28 May 2008 10:11:11 +0000 (10:11 +0000)]
0.5.1

16 years ago...
Enrico Tassi [Tue, 27 May 2008 15:47:54 +0000 (15:47 +0000)]
...

16 years agosmarter lexer needed by lambda-delta that is splitting "let rec" statements
Enrico Tassi [Tue, 27 May 2008 15:42:03 +0000 (15:42 +0000)]
smarter lexer needed by lambda-delta that is splitting "let rec" statements
on multiple lines

16 years ago...
Enrico Tassi [Tue, 27 May 2008 10:56:02 +0000 (10:56 +0000)]
...

16 years agoCoRN moved in contribs
Enrico Tassi [Tue, 27 May 2008 08:51:59 +0000 (08:51 +0000)]
CoRN moved in contribs

16 years agofrst step to move away the CoRN stuff
Enrico Tassi [Tue, 27 May 2008 08:47:27 +0000 (08:47 +0000)]
frst step to move away the CoRN stuff

16 years agofrst step to move away the CoRN stuff
Enrico Tassi [Tue, 27 May 2008 08:46:56 +0000 (08:46 +0000)]
frst step to move away the CoRN stuff

16 years agoauto calls cleanup\
Enrico Tassi [Tue, 27 May 2008 08:36:21 +0000 (08:36 +0000)]
auto calls cleanup\

16 years agobetter description of declarative tactics
Enrico Tassi [Mon, 26 May 2008 16:33:07 +0000 (16:33 +0000)]
better description of declarative tactics

16 years agonew, more rigid syntax, for auto_params affecting the declarative language.
Enrico Tassi [Mon, 26 May 2008 14:01:04 +0000 (14:01 +0000)]
new, more rigid syntax, for auto_params affecting the declarative language.

many multi-word constructs (like 'we proved') are now a single token.
all declarative tactics now use auto_params.
syntax of declarative tactics changed.
many camlp5 refactoring to avoid many rule conflics.

16 years agoUniverse.key was not used to index terms, but was used to retrieve them
Enrico Tassi [Mon, 26 May 2008 13:58:13 +0000 (13:58 +0000)]
Universe.key was not used to index terms, but was used to retrieve them

16 years agobetter presentation of lambda-delta
Ferruccio Guidi [Mon, 26 May 2008 13:43:02 +0000 (13:43 +0000)]
better presentation of lambda-delta

16 years ago- some bugs fixed in the domain-based preorders on environments
Ferruccio Guidi [Mon, 26 May 2008 12:30:21 +0000 (12:30 +0000)]
- some bugs fixed in the domain-based preorders on environments
- some missing lemmas added

16 years agoadded comment for zack
Enrico Tassi [Mon, 26 May 2008 10:43:31 +0000 (10:43 +0000)]
added comment for zack

16 years ago...
Enrico Tassi [Mon, 26 May 2008 09:47:12 +0000 (09:47 +0000)]
...

16 years agoauto syntax updated
Enrico Tassi [Mon, 26 May 2008 09:46:16 +0000 (09:46 +0000)]
auto syntax updated

16 years ago...
Enrico Tassi [Mon, 26 May 2008 09:13:07 +0000 (09:13 +0000)]
...

16 years ago...
Enrico Tassi [Sat, 24 May 2008 13:16:12 +0000 (13:16 +0000)]
...

16 years agoorder of goals changes, open ones are preferred to closed ones as in the paper
Enrico Tassi [Sat, 24 May 2008 10:32:53 +0000 (10:32 +0000)]
order of goals changes, open ones are preferred to closed ones as in the paper

16 years agominimal implementation of left parameters display
Enrico Tassi [Wed, 21 May 2008 12:23:53 +0000 (12:23 +0000)]
minimal implementation of left parameters display

16 years ago0.5.1 should be realased soon, the bug that was affecting fixpoints
Enrico Tassi [Wed, 21 May 2008 10:40:56 +0000 (10:40 +0000)]
0.5.1 should be realased soon, the bug that was affecting fixpoints
disambiguation is nasty

16 years agoHere is where we should add relevance checks.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:42:25 +0000 (23:42 +0000)]
Here is where we should add relevance checks.

16 years agoBug fixed in computation of leftnos: variables were not considered.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:31:44 +0000 (23:31 +0000)]
Bug fixed in computation of leftnos: variables were not considered.

16 years agoCode simplification.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:31:21 +0000 (23:31 +0000)]
Code simplification.

16 years agoAdded cprop <= type constraint.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:06:08 +0000 (23:06 +0000)]
Added cprop <= type constraint.

16 years agoWe do not need to give cprop a special status yet.
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:01:48 +0000 (23:01 +0000)]
We do not need to give cprop a special status yet.

16 years ago...
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:01:32 +0000 (23:01 +0000)]
...

16 years agoCProp dropped in favour of a cprop universe exported from NCicEnvironment,
Claudio Sacerdoti Coen [Mon, 19 May 2008 23:00:11 +0000 (23:00 +0000)]
CProp dropped in favour of a cprop universe exported from NCicEnvironment,
which is just an URI recognized by the pretty printer.

16 years agoadded leftno to references f inductive types and constructors, more unifor names...
Enrico Tassi [Mon, 19 May 2008 20:58:36 +0000 (20:58 +0000)]
added leftno to references f inductive types and constructors, more unifor names of modules, NCic -> C and NReference Ref everywhere

16 years agoadded aps generation
Enrico Tassi [Mon, 19 May 2008 14:36:16 +0000 (14:36 +0000)]
added aps generation

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

16 years ago...
Enrico Tassi [Mon, 19 May 2008 11:41:46 +0000 (11:41 +0000)]
...

16 years agorenamed add_le_constraint to add_constraint since it adds both le and lt constraints
Enrico Tassi [Mon, 19 May 2008 11:41:21 +0000 (11:41 +0000)]
renamed add_le_constraint to add_constraint since it adds both le and lt constraints

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.