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

16 years agoImproved eat_prods error message (at the cost of passing the 6th argument!)
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 16:10:40 +0000 (16:10 +0000)]
Improved eat_prods error message (at the cost of passing the 6th argument!)

16 years agoThe old kernel does not accept ens whose order is different from the one
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 15:56:31 +0000 (15:56 +0000)]
The old kernel does not accept ens whose order is different from the one
declared for the object whose reference it is applied to. Fixed.

16 years agoBad alpha-conversion by Enrico fixed.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 15:25:46 +0000 (15:25 +0000)]
Bad alpha-conversion by Enrico fixed.

16 years agoBug fixed: the ens need not be ordered w.r.t. the declared variables.
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 15:18:33 +0000 (15:18 +0000)]
Bug fixed: the ens need not be ordered w.r.t. the declared variables.
The latter order is the right one for abstraction.

16 years agoj off by one in error message
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 14:54:14 +0000 (14:54 +0000)]
j off by one in error message

16 years agofix_outty partially fixed: missing lifts in args and ens
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 14:47:56 +0000 (14:47 +0000)]
fix_outty partially fixed: missing lifts in args and ens

16 years agofix_outty fixed in order to perform eta-expansion when the term is not
Claudio Sacerdoti Coen [Tue, 8 Apr 2008 14:38:48 +0000 (14:38 +0000)]
fix_outty fixed in order to perform eta-expansion when the term is not
a sequence of lambdas.

16 years agoadded simplify to avoid ugly proofterm
Enrico Tassi [Tue, 8 Apr 2008 09:11:33 +0000 (09:11 +0000)]
added simplify to avoid ugly proofterm

16 years agoTentative (and bad!) fix of outtypes in non-dependent eliminations.
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 23:16:36 +0000 (23:16 +0000)]
Tentative (and bad!) fix of outtypes in non-dependent eliminations.
The fix does not work since there is no guarantee in Coq that the outtype
is made of a sequence of Lambdas (and indeed it is not for automatically
generated elimiantion principles). Thus I need to perform recursion on the
type of the outtype and I also need to perform some eta-expansion to insert
the additional lambda in the right position :-(

16 years agoCooking discriminated into cooking in types (using Prods) and cooking in bodies
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 22:09:02 +0000 (22:09 +0000)]
Cooking discriminated into cooking in types (using Prods) and cooking in bodies
(using Lambdas).

16 years agoPretty-printing of definitions fixed.
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 22:04:17 +0000 (22:04 +0000)]
Pretty-printing of definitions fixed.

16 years agoCooking implemented (not tested yet).
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 22:00:51 +0000 (22:00 +0000)]
Cooking implemented (not tested yet).

16 years agoReports improved.
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 21:27:48 +0000 (21:27 +0000)]
Reports improved.

16 years agoDebugging code fixed.
Claudio Sacerdoti Coen [Mon, 7 Apr 2008 21:05:13 +0000 (21:05 +0000)]
Debugging code fixed.

16 years agoadded invalidate to clear the cache and ease the comparison with the new kernel
Enrico Tassi [Mon, 7 Apr 2008 16:30:11 +0000 (16:30 +0000)]
added invalidate to clear the cache and ease the comparison with the new kernel

16 years agocommented out uris of objs that do not compile properly
Enrico Tassi [Mon, 7 Apr 2008 16:19:11 +0000 (16:19 +0000)]
commented out uris of objs that do not compile properly

16 years agoadded comparison with old kernel
Enrico Tassi [Mon, 7 Apr 2008 16:18:52 +0000 (16:18 +0000)]
added comparison with old kernel

16 years agofixed error message for eat prods
Enrico Tassi [Mon, 7 Apr 2008 16:18:22 +0000 (16:18 +0000)]
fixed error message for eat prods

16 years agoinvalidate
Enrico Tassi [Mon, 7 Apr 2008 16:17:57 +0000 (16:17 +0000)]
invalidate

16 years agouris relative to axioms are translated in the right way
Enrico Tassi [Mon, 7 Apr 2008 16:17:16 +0000 (16:17 +0000)]
uris relative to axioms are translated in the right way

16 years agoadded invalidate
Enrico Tassi [Mon, 7 Apr 2008 16:16:19 +0000 (16:16 +0000)]
added invalidate

16 years agoadded preliminary checks for indtys
Enrico Tassi [Mon, 7 Apr 2008 15:01:32 +0000 (15:01 +0000)]
added preliminary checks for indtys
typecheck the explicit type of letins

16 years agocall get_obj instead of get_cooked_obj ~trust:false
Enrico Tassi [Mon, 7 Apr 2008 15:00:23 +0000 (15:00 +0000)]
call get_obj instead of get_cooked_obj ~trust:false

16 years agoadded case of const and axiom
Enrico Tassi [Mon, 7 Apr 2008 14:59:43 +0000 (14:59 +0000)]
added case of const and axiom

16 years agoadded # to comment
Enrico Tassi [Mon, 7 Apr 2008 14:59:04 +0000 (14:59 +0000)]
added # to comment

16 years agobetter printings
Enrico Tassi [Mon, 7 Apr 2008 14:58:39 +0000 (14:58 +0000)]
better printings

16 years agothe explicit type in a LetIn must be typecheckd before convertibility is checked
Enrico Tassi [Mon, 7 Apr 2008 14:31:03 +0000 (14:31 +0000)]
the explicit type in a LetIn must be typecheckd before convertibility is checked

16 years agoopt compilation enabled, removed some pps, check has -alluris to regenerate
Enrico Tassi [Mon, 7 Apr 2008 12:16:04 +0000 (12:16 +0000)]
opt compilation enabled, removed some pps, check has -alluris to regenerate
the uri list, alluri sorted such that the last fpart of the file fails (but not the former).
all nat/ compiles!

16 years agolefts_ad_tys properly sorted, added some metasenv here and there,
Enrico Tassi [Mon, 7 Apr 2008 11:57:33 +0000 (11:57 +0000)]
lefts_ad_tys properly sorted, added some metasenv here and there,
recursive args defined in case of appl

16 years agolefts_and_tys was tys@lefts, CSC claims it was working since that context is only...
Enrico Tassi [Mon, 7 Apr 2008 11:55:43 +0000 (11:55 +0000)]
lefts_and_tys was tys@lefts, CSC claims it was working since that context is only used
by whd and it did not contain any definitions by contructions, thus the length was the only important bit

16 years agoadded a list of uris to ease debugging
Enrico Tassi [Mon, 7 Apr 2008 11:26:54 +0000 (11:26 +0000)]
added a list of uris to ease debugging

16 years agoprint the excpetion and raise it again, seems to produce a reasonable backtrace
Enrico Tassi [Mon, 7 Apr 2008 11:07:11 +0000 (11:07 +0000)]
print the excpetion and raise it again, seems to produce a reasonable backtrace

16 years agonew constants have depth = max_int insted of 0 so that reducing to 0 expands them
Enrico Tassi [Mon, 7 Apr 2008 11:04:14 +0000 (11:04 +0000)]
new constants have depth = max_int insted of 0 so that reducing to 0 expands them

16 years agooff by one in calling count_from
Enrico Tassi [Mon, 7 Apr 2008 10:54:41 +0000 (10:54 +0000)]
off by one in calling count_from

16 years agofixed bug in translating Fix, recno was not properly computed
Enrico Tassi [Mon, 7 Apr 2008 10:54:11 +0000 (10:54 +0000)]
fixed bug in translating Fix, recno was not properly computed

16 years agoadded a pretty printing of the new object and use argv[1] as uri
Enrico Tassi [Mon, 7 Apr 2008 10:53:05 +0000 (10:53 +0000)]
added a pretty printing of the new object and use argv[1] as uri

16 years agocontext, metasenv and subst made mandatory in CicPp
Enrico Tassi [Mon, 7 Apr 2008 10:22:52 +0000 (10:22 +0000)]
context, metasenv and subst made mandatory in CicPp

16 years agoguarded by has a nice error message
Enrico Tassi [Mon, 7 Apr 2008 10:06:33 +0000 (10:06 +0000)]
guarded by has a nice error message

16 years agoreference type made private, added mk_constructor to be used
Enrico Tassi [Mon, 7 Apr 2008 09:57:46 +0000 (09:57 +0000)]
reference type made private, added mk_constructor to be used
to create the i-th constructor of an inductive type (used in match typechecking).

fixed name capture in oCic2nCic when typing fixpoint types

16 years agosome debug printings
Enrico Tassi [Fri, 4 Apr 2008 17:43:20 +0000 (17:43 +0000)]
some debug printings

16 years agoadded to the cache a boolean to state if the object is
Enrico Tassi [Fri, 4 Apr 2008 17:43:00 +0000 (17:43 +0000)]
added to the cache a boolean to state if the object is
already checked or not (a frozen list is really needed)

16 years agofix
Enrico Tassi [Fri, 4 Apr 2008 17:41:58 +0000 (17:41 +0000)]
fix

16 years agotoday it seems that the substituted should be lifted by k-1+lift_args and not k+lift_...
Enrico Tassi [Fri, 4 Apr 2008 17:41:33 +0000 (17:41 +0000)]
today it seems that the substituted should be lifted by k-1+lift_args and not k+lift_args since k starts from 1

16 years agoadded ppobj
Enrico Tassi [Fri, 4 Apr 2008 16:40:05 +0000 (16:40 +0000)]
added ppobj

16 years agotype_of_constant was retunrning the type of the wrong constructor (-1 missing)
Enrico Tassi [Fri, 4 Apr 2008 13:10:22 +0000 (13:10 +0000)]
type_of_constant was retunrning the type of the wrong constructor (-1 missing)
fixpoints were not properly debruijnated before being checked
better error message for match branches

16 years agofixed list.nth and added some paretheses
Enrico Tassi [Fri, 4 Apr 2008 13:08:32 +0000 (13:08 +0000)]
fixed list.nth and added some paretheses

16 years agoadded some printings and catched more exceptions
Enrico Tassi [Fri, 4 Apr 2008 13:07:36 +0000 (13:07 +0000)]
added some printings and catched more exceptions

16 years agoremoved useless printing
Enrico Tassi [Fri, 4 Apr 2008 13:06:46 +0000 (13:06 +0000)]
removed useless printing

16 years agoiterator map was mapping Lambdas to Prods!!!
Enrico Tassi [Fri, 4 Apr 2008 13:06:21 +0000 (13:06 +0000)]
iterator map was mapping Lambdas to Prods!!!

16 years agodebugging started
Enrico Tassi [Fri, 4 Apr 2008 11:46:57 +0000 (11:46 +0000)]
debugging started

16 years agotype of constant ported
Enrico Tassi [Fri, 4 Apr 2008 10:42:57 +0000 (10:42 +0000)]
type of constant ported

16 years agoadded add_obj to store objects in the environment, implementation still
Enrico Tassi [Fri, 4 Apr 2008 10:26:50 +0000 (10:26 +0000)]
added add_obj to store objects in the environment, implementation still
shaky since no frozen list is there