]> matita.cs.unibo.it Git - helm.git/log
helm.git
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

16 years agocicEnvironment refactoring with sound view of Coq`s univ-less terms
Enrico Tassi [Fri, 18 Apr 2008 15:30:40 +0000 (15:30 +0000)]
cicEnvironment refactoring with sound view of Coq`s univ-less terms

16 years agoassertion was wrong, an object can contain a named univers if its uri is the one...
Enrico Tassi [Fri, 18 Apr 2008 15:27:39 +0000 (15:27 +0000)]
assertion was wrong, an object can contain a named univers if its uri is the one of the object itself

16 years agograph generation phase fixed
Enrico Tassi [Fri, 18 Apr 2008 15:26:11 +0000 (15:26 +0000)]
graph generation phase fixed

16 years agoAppl case in is_really_smaller fixed as in the old kernel
Enrico Tassi [Fri, 18 Apr 2008 13:59:17 +0000 (13:59 +0000)]
Appl case in is_really_smaller fixed as in the old kernel

16 years agoexample:
Enrico Tassi [Thu, 17 Apr 2008 16:55:36 +0000 (16:55 +0000)]
example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)

16 years agoadded a missing whd
Enrico Tassi [Thu, 17 Apr 2008 16:34:44 +0000 (16:34 +0000)]
added a missing whd

16 years agonew calculation of recursive parameters in guarded by destructors:
Enrico Tassi [Thu, 17 Apr 2008 16:12:12 +0000 (16:12 +0000)]
new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).

16 years agoTwo similar cases packed together
Enrico Tassi [Thu, 17 Apr 2008 14:39:30 +0000 (14:39 +0000)]
Two similar cases packed together

16 years agosome fixes for guardness conditions
Enrico Tassi [Thu, 17 Apr 2008 14:30:56 +0000 (14:30 +0000)]
some fixes for guardness conditions

16 years agois_really_smaller in sync with old kernel, impossible cases removed
Enrico Tassi [Thu, 17 Apr 2008 14:26:23 +0000 (14:26 +0000)]
is_really_smaller in sync with old kernel, impossible cases removed

16 years agocheck_is_really_smaller simplified to consider that it is called only on terms
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 20:52:43 +0000 (20:52 +0000)]
check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.

16 years ago1. bug fixed: the context must be type-checked before using it in type_of_aux'.
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 20:10:44 +0000 (20:10 +0000)]
1. bug fixed: the context must be type-checked before using it in type_of_aux'.
   Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
   argument is found in the body of another fix, the body of the inner fix
   is check adding the recusrive formal parameter as an additional safe
   argument.

16 years agoget_checked_fix -> get_checked_fixes
Enrico Tassi [Tue, 15 Apr 2008 13:44:16 +0000 (13:44 +0000)]
get_checked_fix -> get_checked_fixes

16 years agoadded comment
Enrico Tassi [Tue, 15 Apr 2008 13:42:39 +0000 (13:42 +0000)]
added comment

16 years agoadded sample of guarded by in which coq is stronger
Claudio Sacerdoti Coen [Tue, 15 Apr 2008 10:47:29 +0000 (10:47 +0000)]
added sample of guarded by in which coq is stronger

16 years agopositivity check fixed, a MutInd not applied (but with an exp-named-subst)
Enrico Tassi [Tue, 15 Apr 2008 08:53:01 +0000 (08:53 +0000)]
positivity check fixed, a MutInd not applied (but with an exp-named-subst)
was considere non strictly positive always

16 years agodo not use an implicit but a sort as a neutral term for positivity check
Enrico Tassi [Tue, 15 Apr 2008 08:20:24 +0000 (08:20 +0000)]
do not use an implicit but a sort as a neutral term for positivity check

16 years agoobjects are typechecked to ensure there is a graph before doing all the stuff......
Enrico Tassi [Mon, 14 Apr 2008 14:59:12 +0000 (14:59 +0000)]
objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required

16 years agoleftno should be increased of the expnamedsubst, but counting only the uris of vars...
Enrico Tassi [Mon, 14 Apr 2008 14:48:14 +0000 (14:48 +0000)]
leftno should be increased of the expnamedsubst, but counting only the uris of vars without a body

16 years agobetter error message
Enrico Tassi [Mon, 14 Apr 2008 14:47:15 +0000 (14:47 +0000)]
better error message

16 years agosame_obj made more precise, fixed the order of the context for fixpoints body,
Enrico Tassi [Mon, 14 Apr 2008 13:21:15 +0000 (13:21 +0000)]
same_obj made more precise, fixed the order of the context for fixpoints body,
cache of fix extended to the mutual case (properly)

16 years agoficed fixpoint cache usage for mutual fix
Enrico Tassi [Mon, 14 Apr 2008 10:22:14 +0000 (10:22 +0000)]
ficed fixpoint cache usage for mutual fix

16 years agofixed positivity conditions
Enrico Tassi [Mon, 14 Apr 2008 10:21:33 +0000 (10:21 +0000)]
fixed positivity conditions

16 years agoadded mk_fix i j r that given an r of a fix generated another fix on i and j
Enrico Tassi [Mon, 14 Apr 2008 10:20:39 +0000 (10:20 +0000)]
added mk_fix i j r that given an r of a fix generated another fix on i and j

16 years agopositivity condition was relying on the name declared in abstractions, and
Enrico Tassi [Mon, 14 Apr 2008 09:58:24 +0000 (09:58 +0000)]
positivity condition was relying on the name declared in abstractions, and
was checking for a dependent product calling does not occurr with a wrong
index

16 years agoadded little optimization to not add twice the same arc
Enrico Tassi [Mon, 14 Apr 2008 09:00:52 +0000 (09:00 +0000)]
added little optimization to not add twice the same arc

16 years agoquinck and untested implementation of positivity conditions check
Enrico Tassi [Fri, 11 Apr 2008 16:45:29 +0000 (16:45 +0000)]
quinck and untested implementation of positivity conditions check

16 years ago...
Enrico Tassi [Fri, 11 Apr 2008 15:25:15 +0000 (15:25 +0000)]
...

16 years agoadded depndency of new kernel to metadata to allow to use the DB to calculate the...
Enrico Tassi [Fri, 11 Apr 2008 15:20:27 +0000 (15:20 +0000)]
added depndency of new kernel to metadata to allow to use the DB to calculate the minimum set of graphs to load

16 years agoFIXED bug, added assertion in case a universe inside a term T living at URI u
Enrico Tassi [Fri, 11 Apr 2008 15:19:31 +0000 (15:19 +0000)]
FIXED bug, added assertion in case a universe inside a term T living at URI u
was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.

16 years agoadded function to fresh types
Enrico Tassi [Fri, 11 Apr 2008 15:16:33 +0000 (15:16 +0000)]
added function to fresh types

16 years agocall Unshare.fresh_types
Enrico Tassi [Fri, 11 Apr 2008 15:15:46 +0000 (15:15 +0000)]
call Unshare.fresh_types

16 years agoload the graph of objects that depend on the ones requested,
Enrico Tassi [Fri, 11 Apr 2008 15:15:21 +0000 (15:15 +0000)]
load the graph of objects that depend on the ones requested,
rank universes and use them in the transformation to obtain terms
with TypeK and not always Type0

16 years agouse universe rank instead of Type0
Enrico Tassi [Fri, 11 Apr 2008 15:13:47 +0000 (15:13 +0000)]
use universe rank instead of Type0

16 years agoType related failures fixed
Enrico Tassi [Fri, 11 Apr 2008 15:13:09 +0000 (15:13 +0000)]
Type related failures fixed

16 years agobetter pp of objects
Enrico Tassi [Fri, 11 Apr 2008 15:12:30 +0000 (15:12 +0000)]
better pp of objects

16 years agoExtracted code. The main executable is medium_tests that runs the emulator on
Claudio Sacerdoti Coen [Fri, 11 Apr 2008 13:09:02 +0000 (13:09 +0000)]
Extracted code. The main executable is medium_tests that runs the emulator on
a few assembly programs with inputs of different sizes:
  * string reverse
  * counting sort
  * perfect numbers

16 years agoremoved useless file
Enrico Tassi [Fri, 11 Apr 2008 13:07:54 +0000 (13:07 +0000)]
removed useless file

16 years agofixed modules order
Enrico Tassi [Fri, 11 Apr 2008 11:40:49 +0000 (11:40 +0000)]
fixed modules order

16 years agomore fix removed from types
Enrico Tassi [Fri, 11 Apr 2008 11:10:12 +0000 (11:10 +0000)]
more fix removed from types

16 years agomore fix removed from types in proofs
Enrico Tassi [Fri, 11 Apr 2008 11:01:53 +0000 (11:01 +0000)]
more fix removed from types in proofs

16 years agowhen we build the elimination principle we fresh universes to not
Enrico Tassi [Fri, 11 Apr 2008 10:33:49 +0000 (10:33 +0000)]
when we build the elimination principle we fresh universes to not
generate tems with different

16 years agoadded a parameter to unshare universes
Enrico Tassi [Fri, 11 Apr 2008 10:21:45 +0000 (10:21 +0000)]
added a parameter to unshare universes

16 years agoConversion of 2 lambdas was not requiring equality on universes of the source type...
Enrico Tassi [Fri, 11 Apr 2008 10:20:34 +0000 (10:20 +0000)]
Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.

16 years agocontext of types built in the reverse order
Enrico Tassi [Fri, 11 Apr 2008 10:16:56 +0000 (10:16 +0000)]
context of types built in the reverse order

16 years agoadded a simplify to prevent the generation of an ugly fix
Enrico Tassi [Fri, 11 Apr 2008 10:16:00 +0000 (10:16 +0000)]
added a simplify to prevent the generation of an ugly fix

16 years agoimplemented inductive and less parentheses
Enrico Tassi [Fri, 11 Apr 2008 08:16:23 +0000 (08:16 +0000)]
implemented inductive and less parentheses

16 years agoThe cache of objects is now used also for cofixpoints.
Claudio Sacerdoti Coen [Thu, 10 Apr 2008 18:19:16 +0000 (18:19 +0000)]
The cache of objects is now used also for cofixpoints.

16 years agoNew: cache of translated fixpoints (to avoid the generative fix restriction and
Claudio Sacerdoti Coen [Thu, 10 Apr 2008 18:14:47 +0000 (18:14 +0000)]
New: cache of translated fixpoints (to avoid the generative fix restriction and
to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)

16 years agodoes_not_occur exported to be used in oCic2NCic
Claudio Sacerdoti Coen [Thu, 10 Apr 2008 18:09:01 +0000 (18:09 +0000)]
does_not_occur exported to be used in oCic2NCic

16 years agoBug fixed: references to CoFix are CoFix, not Fix.
Claudio Sacerdoti Coen [Wed, 9 Apr 2008 15:59:57 +0000 (15:59 +0000)]
Bug fixed: references to CoFix are CoFix, not Fix.

16 years agoprint unnamed variables as __n
Enrico Tassi [Wed, 9 Apr 2008 15:24:54 +0000 (15:24 +0000)]
print unnamed variables as __n

16 years agoswitch off profilers
Enrico Tassi [Wed, 9 Apr 2008 15:22:03 +0000 (15:22 +0000)]
switch off profilers

16 years agopp with parenthesis only when necessary and with some more boxes
Enrico Tassi [Wed, 9 Apr 2008 15:13:59 +0000 (15:13 +0000)]
pp with parenthesis only when necessary and with some more boxes

16 years ago...
Claudio Sacerdoti Coen [Wed, 9 Apr 2008 14:58:35 +0000 (14:58 +0000)]
...

16 years agoFixed serious bug that occurred only in the following situation:
Claudio Sacerdoti Coen [Wed, 9 Apr 2008 14:57:34 +0000 (14:57 +0000)]
Fixed serious bug that occurred only in the following situation:

\lambda x.
Fix f {
\lambda y: P x.
Fix g {

The two fixes must be translated as

Fix f { \lambda x. \lambda y: P x. ...}
Fix g { \lambda x. \lambda f. \lambda y: P x. ... }

In the first case, the x that occurs in the type of y must be a Rel 1.
In the second case, the x that occurs in the type of y must be a Rel 2.
The previous code translated both of them to Rel 1.

16 years agobetter pp in Appl
Enrico Tassi [Wed, 9 Apr 2008 14:57:13 +0000 (14:57 +0000)]
better pp in Appl

16 years agobetter pp
Enrico Tassi [Wed, 9 Apr 2008 14:55:30 +0000 (14:55 +0000)]
better pp

16 years agopretty printer on steroids
Enrico Tassi [Wed, 9 Apr 2008 14:37:56 +0000 (14:37 +0000)]
pretty printer on steroids

16 years agoAdded some "\n" here and there to the pretty-printing of Match.
Claudio Sacerdoti Coen [Wed, 9 Apr 2008 12:20:22 +0000 (12:20 +0000)]
Added some "\n" here and there to the pretty-printing of Match.

16 years agoGrave bug fixed: Ce that point to definitions were handled as those that point
Claudio Sacerdoti Coen [Wed, 9 Apr 2008 12:19:06 +0000 (12:19 +0000)]
Grave bug fixed: Ce that point to definitions were handled as those that point
to declarations. So Fix-constants were too much abstracted, too much applied,
etc.

16 years agoadded profiling on/off
Enrico Tassi [Wed, 9 Apr 2008 12:04:09 +0000 (12:04 +0000)]
added profiling on/off

16 years agoinvalidate fixed
Enrico Tassi [Wed, 9 Apr 2008 12:03:34 +0000 (12:03 +0000)]
invalidate fixed

16 years agoallow to switch profiling on and off on the fly
Enrico Tassi [Wed, 9 Apr 2008 11:59:49 +0000 (11:59 +0000)]
allow to switch profiling on and off on the fly

16 years agoremoved two useless calls to the environment, one still to be optimized out
Enrico Tassi [Wed, 9 Apr 2008 11:58:33 +0000 (11:58 +0000)]
removed two useless calls to the environment, one still to be optimized out

16 years ago...
Enrico Tassi [Wed, 9 Apr 2008 08:47:07 +0000 (08:47 +0000)]
...

16 years agoVariables are no longer experted (cooking is now implemented).
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 22:00:51 +0000 (22:00 +0000)]
Variables are no longer experted (cooking is now implemented).
Better reporting with indentation.

16 years agoSwapped arguments in error message.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 21:49:50 +0000 (21:49 +0000)]
Swapped arguments in error message.

16 years agoVariables having a body can occur in cooked terms and must be delta-expanded
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 21:31:13 +0000 (21:31 +0000)]
Variables having a body can occur in cooked terms and must be delta-expanded
during translation to the new CIC format.

16 years agoFix over the previous one: Var-LetIn abstractions should be ignored and not
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 21:18:03 +0000 (21:18 +0000)]
Fix over the previous one: Var-LetIn abstractions should be ignored and not
transformed into applications at all.

16 years agoError message improved.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 21:13:18 +0000 (21:13 +0000)]
Error message improved.

16 years agoCooking w.r.t. variables with bodies is now implemented as delta-expansion.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 20:57:30 +0000 (20:57 +0000)]
Cooking w.r.t. variables with bodies is now implemented as delta-expansion.

16 years agoFix name capture in cofix.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:51:10 +0000 (17:51 +0000)]
Fix name capture in cofix.

16 years agoTo test the translation.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:50:32 +0000 (17:50 +0000)]
To test the translation.

16 years agoName capture fixed.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:27:41 +0000 (17:27 +0000)]
Name capture fixed.

16 years agoImproved error messages in place of "sort elimination not allowed".
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:22:19 +0000 (17:22 +0000)]
Improved error messages in place of "sort elimination not allowed".

16 years agoSeed reset before each convert_obj.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:03:35 +0000 (17:03 +0000)]
Seed reset before each convert_obj.

16 years agoUse seed to avoid further name clashes.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 17:02:04 +0000 (17:02 +0000)]
Use seed to avoid further name clashes.

16 years ago...
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 16:59:26 +0000 (16:59 +0000)]
...

16 years agoIncredible, but true! Our name mangling clashed with one identifier in the
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 16:45:16 +0000 (16:45 +0000)]
Incredible, but true! Our name mangling clashed with one identifier in the
library of Coq, generating two functions that mutually called each other,
making the type-checker diverge!!!!

16 years agoCooked objects are no longer well typed in the uncooked old environment.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 16:37:16 +0000 (16:37 +0000)]
Cooked objects are no longer well typed in the uncooked old environment.
Thus we need to fix_outtype before cooking.