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

16 years agologger added
Enrico Tassi [Fri, 4 Apr 2008 10:20:23 +0000 (10:20 +0000)]
logger added

16 years agoadded get_obj in nCicEnvironment that returns an object and a boolean stating
Enrico Tassi [Fri, 4 Apr 2008 10:12:25 +0000 (10:12 +0000)]
added get_obj in nCicEnvironment that returns an object and a boolean stating
if the object is checked or not (to be used by the typechecker, function
type_of_constant

16 years agoindentation fixed
Enrico Tassi [Fri, 4 Apr 2008 10:07:22 +0000 (10:07 +0000)]
indentation fixed

16 years agoreturns_a_counductive implemented
Enrico Tassi [Fri, 4 Apr 2008 10:04:06 +0000 (10:04 +0000)]
returns_a_counductive implemented

16 years agotype_of_branch ported and optimized to not lift the outty every Prod, keep the
Enrico Tassi [Fri, 4 Apr 2008 09:57:58 +0000 (09:57 +0000)]
type_of_branch ported and optimized to not lift the outty every Prod, keep the
number of passes binders and lift it just once

16 years agois_really_smaller ported, still to understand the case in which
Enrico Tassi [Fri, 4 Apr 2008 09:40:10 +0000 (09:40 +0000)]
is_really_smaller ported, still to understand the case in which
whe find a Fix or and applied Fix (still there after a whd)

16 years agodebujin implemented with the map recursor
Enrico Tassi [Thu, 3 Apr 2008 16:55:10 +0000 (16:55 +0000)]
debujin implemented with the map recursor

16 years agobug found rewriting the kernel backported: n instead of m when pulling a def from...
Enrico Tassi [Thu, 3 Apr 2008 16:26:19 +0000 (16:26 +0000)]
bug found rewriting the kernel backported: n instead of m when pulling a def from the context, previously a meaningless index was used

16 years agonon debruijned constructor may be useless elswere, for the moment we do not bind it
Enrico Tassi [Thu, 3 Apr 2008 16:23:04 +0000 (16:23 +0000)]
non debruijned constructor may be useless elswere, for the moment we do not bind it

16 years agoguarded_by_destructor ported, many auxiliary functions still to be done
Enrico Tassi [Thu, 3 Apr 2008 16:16:59 +0000 (16:16 +0000)]
guarded_by_destructor ported, many auxiliary functions still to be done

16 years agoremoved FSF banner
Enrico Tassi [Thu, 3 Apr 2008 16:15:51 +0000 (16:15 +0000)]
removed FSF banner

16 years agoadded ugly test showing many many bugs in the current kernel
Enrico Tassi [Thu, 3 Apr 2008 15:42:10 +0000 (15:42 +0000)]
added ugly test showing many many bugs in the current kernel

16 years agoadded slim version of does_not_occur
Enrico Tassi [Wed, 2 Apr 2008 13:15:27 +0000 (13:15 +0000)]
added slim version of does_not_occur

16 years agoadded translation of Set to Type0 (avoid warning)
Enrico Tassi [Wed, 2 Apr 2008 13:14:45 +0000 (13:14 +0000)]
added translation of Set to Type0 (avoid warning)

16 years agofixes backported from the new kernel
Enrico Tassi [Wed, 2 Apr 2008 12:56:27 +0000 (12:56 +0000)]
fixes backported from the new kernel