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

16 years agoremoved dummy rewrite
Enrico Tassi [Wed, 2 Apr 2008 09:39:23 +0000 (09:39 +0000)]
removed dummy rewrite

16 years agoremoved dummy rewrite
Enrico Tassi [Wed, 2 Apr 2008 09:30:32 +0000 (09:30 +0000)]
removed dummy rewrite

16 years agoremoved dummy rewrites
Enrico Tassi [Wed, 2 Apr 2008 09:23:30 +0000 (09:23 +0000)]
removed dummy rewrites

16 years agofixed according to the new rewrite semantics (fails if no progress)
Enrico Tassi [Wed, 2 Apr 2008 09:22:14 +0000 (09:22 +0000)]
fixed according to the new rewrite semantics (fails if no progress)

16 years agofixed depends after the removal of Fsub
Enrico Tassi [Wed, 2 Apr 2008 09:18:08 +0000 (09:18 +0000)]
fixed depends after the removal of Fsub

16 years agobetter check for progress
Enrico Tassi [Tue, 1 Apr 2008 19:07:11 +0000 (19:07 +0000)]
better check for progress

16 years agotypeof_obj0 implemented
Claudio Sacerdoti Coen [Tue, 1 Apr 2008 17:51:14 +0000 (17:51 +0000)]
typeof_obj0 implemented

16 years ago1) added get_checked_indtys that returns the whole block of inductive types
Claudio Sacerdoti Coen [Tue, 1 Apr 2008 17:01:45 +0000 (17:01 +0000)]
1) added get_checked_indtys that returns the whole block of inductive types
2) type checking of Match almost finished

16 years agoprogress made better, still not perfect
Enrico Tassi [Tue, 1 Apr 2008 14:08:11 +0000 (14:08 +0000)]
progress made better, still not perfect

16 years agoadded to rewrite a check to effectively do something, and fail if nothing has been...
Enrico Tassi [Tue, 1 Apr 2008 12:40:50 +0000 (12:40 +0000)]
added to rewrite a check to effectively do something, and fail if nothing has been rewritten.

16 years agoadded some comments, but the samentics of many functions is still unclear to me
Enrico Tassi [Tue, 1 Apr 2008 08:59:02 +0000 (08:59 +0000)]
added some comments, but the samentics of many functions is still unclear to me

16 years agoadded set_ppterm
Enrico Tassi [Tue, 1 Apr 2008 08:20:29 +0000 (08:20 +0000)]
added set_ppterm

16 years agoAutomatic generation of elimination and inversion principles for co-inductive
Claudio Sacerdoti Coen [Mon, 31 Mar 2008 17:56:14 +0000 (17:56 +0000)]
Automatic generation of elimination and inversion principles for co-inductive
types disabled (since it does not make sense!)

16 years agoLarge amount of duplicated code (still in comments) factorized.
Claudio Sacerdoti Coen [Mon, 31 Mar 2008 17:45:01 +0000 (17:45 +0000)]
Large amount of duplicated code (still in comments) factorized.

16 years ago1) Impredicative sort "Set" removed everywhere.
Claudio Sacerdoti Coen [Mon, 31 Mar 2008 17:02:48 +0000 (17:02 +0000)]
1) Impredicative sort "Set" removed everywhere.
2) Sort "CProp" is now predicative.
3) Optimized case IRL in check_metasenv_consistency.

16 years ago1) more sharing everywhere in NCicSubstitution
Claudio Sacerdoti Coen [Mon, 31 Mar 2008 14:10:21 +0000 (14:10 +0000)]
1) more sharing everywhere in NCicSubstitution
2) type of iterators in nCicUtils changed to take a NCic.hypothesis when
   crossing binders

16 years agomore cases of the type checker honoured, still missing Match and Const.
Enrico Tassi [Thu, 27 Mar 2008 15:07:09 +0000 (15:07 +0000)]
more cases of the type checker honoured, still missing Match and Const.
lookup_meta added

16 years agoadded is_closed to nCicUtils.
Enrico Tassi [Thu, 27 Mar 2008 13:45:29 +0000 (13:45 +0000)]
added is_closed to nCicUtils.
partial implementation of the typeof main function.
dummy nCicPp waiting for a proper replacement

16 years agomoved psubst and list to the new iterators, result not very impressing
Enrico Tassi [Thu, 27 Mar 2008 10:51:12 +0000 (10:51 +0000)]
moved psubst and list to the new iterators, result not very impressing
from the #lines point of view

16 years agoadded iterators over NCic terms
Enrico Tassi [Thu, 27 Mar 2008 10:50:09 +0000 (10:50 +0000)]
added iterators over NCic terms

16 years agoremoved FSF header
Enrico Tassi [Thu, 27 Mar 2008 10:49:40 +0000 (10:49 +0000)]
removed FSF header

16 years agoUpdated depedencies.
Wilmer Ricciotti [Thu, 27 Mar 2008 10:22:56 +0000 (10:22 +0000)]
Updated depedencies.

16 years agoinsert comments of old tpechecker
Enrico Tassi [Thu, 27 Mar 2008 09:58:08 +0000 (09:58 +0000)]
insert comments of old tpechecker

16 years agoReorganization of list library (step 1)
Wilmer Ricciotti [Wed, 26 Mar 2008 17:59:11 +0000 (17:59 +0000)]
Reorganization of list library (step 1)

16 years agonew are_convertible and head_beta_reduce
Enrico Tassi [Tue, 25 Mar 2008 17:56:20 +0000 (17:56 +0000)]
new are_convertible and head_beta_reduce

16 years agocontext for fixpoint body created in the hopefully right order
Enrico Tassi [Tue, 25 Mar 2008 15:59:51 +0000 (15:59 +0000)]
context for fixpoint body created in the hopefully right order

16 years agoported to the Cic LetIn with explicit type
Enrico Tassi [Tue, 25 Mar 2008 15:51:59 +0000 (15:51 +0000)]
ported to the Cic LetIn with explicit type

16 years agothis patch is a shit, the part that fixes the heuristic about Obj.magic should be...
Enrico Tassi [Tue, 25 Mar 2008 15:37:01 +0000 (15:37 +0000)]
this patch is a shit, the part that fixes the heuristic about Obj.magic should be really adopted, the rest is metaocaml specific

16 years agofix with m (to be optimized) are rewritten such that m is abtracted outside the fix
Enrico Tassi [Tue, 25 Mar 2008 15:35:45 +0000 (15:35 +0000)]
fix with m (to be optimized) are rewritten such that m is abtracted outside the fix

16 years agovery very interesting hack
Enrico Tassi [Tue, 25 Mar 2008 15:34:32 +0000 (15:34 +0000)]
very very interesting hack

16 years agosmall update
Wilmer Ricciotti [Tue, 25 Mar 2008 13:52:29 +0000 (13:52 +0000)]
small update

16 years agoargument of type mcu_type always abstracted first
Enrico Tassi [Tue, 25 Mar 2008 13:23:33 +0000 (13:23 +0000)]
argument of type mcu_type always abstracted first

16 years agoXXX this is the beginning of the metaocaml work XXX
Enrico Tassi [Tue, 25 Mar 2008 12:21:24 +0000 (12:21 +0000)]
XXX this is the beginning of the metaocaml work XXX

16 years agoFsub moved in contribs
Enrico Tassi [Sun, 23 Mar 2008 18:55:49 +0000 (18:55 +0000)]
Fsub moved in contribs

16 years agocicNotationPp: fixed letin syntax (now typeless)
Ferruccio Guidi [Sun, 23 Mar 2008 18:39:34 +0000 (18:39 +0000)]
cicNotationPp: fixed letin syntax (now typeless)
LambdaTypes: typeles letin syntax, some notational changes, Makefile fixed

16 years agosince many stuff is under contrib, we need to ignore less directories
Enrico Tassi [Sat, 22 Mar 2008 11:21:10 +0000 (11:21 +0000)]
since many stuff is under contrib, we need to ignore less directories

16 years agolibrary_auto moved inside contrib, still not ported to the relatively-new
Enrico Tassi [Sat, 22 Mar 2008 11:19:05 +0000 (11:19 +0000)]
library_auto moved inside contrib, still not ported to the relatively-new
build system

16 years agomoved dama/ and dama_didactic/ in contribs/dama/
Enrico Tassi [Sat, 22 Mar 2008 11:17:17 +0000 (11:17 +0000)]
moved dama/ and dama_didactic/ in contribs/dama/
the tests output should not change and history is preserved

16 years agofreescale moved under contribs. contribs made relocatable
Enrico Tassi [Sat, 22 Mar 2008 11:01:57 +0000 (11:01 +0000)]
freescale moved under contribs. contribs made relocatable
since all internal Makefile include a Makefile.defs defining
where to find matita*
tests should not be affected since the output of the compilation is
the same and the URIs are the same

16 years agoNew syntax for auto-related tactics and conclude/obtain.
Claudio Sacerdoti Coen [Thu, 20 Mar 2008 21:08:08 +0000 (21:08 +0000)]
New syntax for auto-related tactics and conclude/obtain.

16 years agoScript fixed (it did not compile due to a mistake before committing).
Claudio Sacerdoti Coen [Thu, 20 Mar 2008 20:39:28 +0000 (20:39 +0000)]
Script fixed (it did not compile due to a mistake before committing).

16 years agoBase-2 is not compiling properly and is excluded for now
Ferruccio Guidi [Thu, 20 Mar 2008 18:26:49 +0000 (18:26 +0000)]
Base-2 is not compiling properly and is excluded for now

16 years agochanged auto_tac params type and all derivate tactics like applyS and
Enrico Tassi [Thu, 20 Mar 2008 17:42:42 +0000 (17:42 +0000)]
changed auto_tac params type and all derivate tactics like applyS and
demodulate honors the same syntax.

new syntax for auto parameters:
  auto string-params by only_terms_to_use
new syntax for declarative eq chains:
  [(conclude|obtain H) t1] = t2 (auto-params|exact t|using t|proof)
  exact t : apply t
  using t : 1 demodulation step using t
  auto-params : first [ auto ; auto paramodulation ]
  proof : id_tac
manual still to be updated

16 years agonew semantics for 'by t'
Enrico Tassi [Thu, 20 Mar 2008 13:07:09 +0000 (13:07 +0000)]
new semantics for 'by t'

16 years agoremoved pointless test
Enrico Tassi [Thu, 20 Mar 2008 13:02:05 +0000 (13:02 +0000)]
removed pointless test

16 years agoI believe that auto paramodulation does not try to
Enrico Tassi [Thu, 20 Mar 2008 12:59:03 +0000 (12:59 +0000)]
I believe that auto paramodulation does not try to
saturate guarded equations and solve hypothesis with auto...

16 years agoadded library option to auto
Enrico Tassi [Thu, 20 Mar 2008 12:56:05 +0000 (12:56 +0000)]
added library option to auto

16 years agoletins are no more unfolded, we do that by hand
Enrico Tassi [Thu, 20 Mar 2008 12:42:45 +0000 (12:42 +0000)]
letins are no more unfolded, we do that by hand

16 years agoletin are no longer unfolded thus coercions not propagated deeply.
Enrico Tassi [Thu, 20 Mar 2008 12:40:49 +0000 (12:40 +0000)]
letin are no longer unfolded thus coercions not propagated deeply.
workaround not using letins

16 years agoEnd of patch for computation of LetIn types. Now types of mutually (co)recursive
Claudio Sacerdoti Coen [Thu, 20 Mar 2008 09:23:30 +0000 (09:23 +0000)]
End of patch for computation of LetIn types. Now types of mutually (co)recursive
function are added to the environment _after_ Implicit have been resolved.

16 years agoBug: types and terms pushed into the context must be Implicit free.
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 19:25:25 +0000 (19:25 +0000)]
Bug: types and terms pushed into the context must be Implicit free.
Partial fix committed (types of Fix and CoFix not patched yet).

16 years ago-debug improved
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 19:03:22 +0000 (19:03 +0000)]
-debug improved

16 years ago...
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 18:57:40 +0000 (18:57 +0000)]
...

16 years agoprerr_endline => debug_print
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:52:07 +0000 (17:52 +0000)]
prerr_endline => debug_print

16 years agoprerr_endline => debug_print
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:44:49 +0000 (17:44 +0000)]
prerr_endline => debug_print

16 years agoNumber notation for Coq is back again, waiting for the ultimate solution.
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:37:02 +0000 (17:37 +0000)]
Number notation for Coq is back again, waiting for the ultimate solution.
Idea: raise the right exception when the Uri is not found.

16 years agoFiles committed by Enrico (a mistake, I suppose) removed.
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:23:13 +0000 (17:23 +0000)]
Files committed by Enrico (a mistake, I suppose) removed.

16 years agoProcedural : added some missing cases
Ferruccio Guidi [Wed, 19 Mar 2008 15:35:15 +0000 (15:35 +0000)]
Procedural  : added some missing cases
LAMBDA-TYPES: improved preambles

16 years agoLAMBDA-TYPES: level 2 dependences are now correct, at least :)
Ferruccio Guidi [Tue, 18 Mar 2008 19:22:41 +0000 (19:22 +0000)]
LAMBDA-TYPES: level 2 dependences are now correct, at least :)

16 years agoProcedural : tentative update to the new letin cic construction
Ferruccio Guidi [Tue, 18 Mar 2008 19:12:57 +0000 (19:12 +0000)]
Procedural  : tentative update to the new letin cic construction
LAMBDA-TYPES: level 1 is stand alone instead of coq dependent
              level 2 is untested so will not compile for now :)
legacy      : unpublished

16 years agoTests enabled again.
Claudio Sacerdoti Coen [Fri, 14 Mar 2008 12:00:54 +0000 (12:00 +0000)]
Tests enabled again.

16 years ago:-(
Claudio Sacerdoti Coen [Thu, 13 Mar 2008 18:48:26 +0000 (18:48 +0000)]
:-(
This commit introduces an hack in deannotate.ml to compute on-the-fly the types
for the body in a LetIn parsed from an XML file. This happens when parsing Coq
files. We should re-export everything from Coq sooner or later.

16 years agoNew version of freescale:
Claudio Sacerdoti Coen [Thu, 13 Mar 2008 14:01:52 +0000 (14:01 +0000)]
New version of freescale:
 a) bug fixed for SBC, JUMP e JSR
 b) medium_tests theorems ported to new pattern syntax
 c) new test for a perfect number generator
 d) "lambda-delifting" of let rec reverted (waiting for a better
    implementation of simplify or for the new generation kernel)

16 years agoProblem solved (was: apply needed an argument to avoid a great slow down due to
Claudio Sacerdoti Coen [Wed, 12 Mar 2008 18:55:42 +0000 (18:55 +0000)]
Problem solved (was: apply needed an argument to avoid a great slow down due to
conversion of a meta-open and a meta-closed term).

16 years agoAlmost always correct optimization: during unification, a meta-closed term and
Claudio Sacerdoti Coen [Wed, 12 Mar 2008 18:52:54 +0000 (18:52 +0000)]
Almost always correct optimization: during unification, a meta-closed term and
a term that is not meta closed are not tried for convertibility. This greatly
speeds up, for instance, some examples in Bertrand.

16 years agofixed implicit
Enrico Tassi [Wed, 12 Mar 2008 12:44:59 +0000 (12:44 +0000)]
fixed implicit

16 years agoNuova dimostrazione riflessiva di le_to_Bertrand.
Andrea Asperti [Wed, 12 Mar 2008 12:02:02 +0000 (12:02 +0000)]
Nuova dimostrazione riflessiva di le_to_Bertrand.

16 years agoif -debug is specified do not catch all exceptions
Enrico Tassi [Wed, 12 Mar 2008 10:37:10 +0000 (10:37 +0000)]
if -debug is specified do not catch all exceptions

16 years agoVery experimental commit: the type of the source is now required in LetIns
Claudio Sacerdoti Coen [Tue, 11 Mar 2008 22:02:58 +0000 (22:02 +0000)]
Very experimental commit: the type of the source is now required in LetIns
and Defs. This is a back-porting from the new generation kernel.

TODO:
a) debug some failing examples (paramodulation)
b) port the code by Ferruccio
c) do something for Coq files (that are now rejected)

16 years agofixed wrong dependencies in debian package reported by oliboni
Enrico Tassi [Mon, 10 Mar 2008 15:56:52 +0000 (15:56 +0000)]
fixed wrong dependencies in debian package reported by oliboni

16 years agoBad hack to avoid failure of conversion (unfolding) in "unfold t in H" where
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 15:51:07 +0000 (15:51 +0000)]
Bad hack to avoid failure of conversion (unfolding) in "unfold t in H" where
H is a definition. In this case it is perfectly normal that t may not occur
in the type or in the body of H.

16 years ago...
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 15:49:51 +0000 (15:49 +0000)]
...

16 years agoScripts fixed because of:
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 13:37:23 +0000 (13:37 +0000)]
Scripts fixed because of:
a) reduce got rid of
b) different behaviour of reduction w.r.t. zeta-reduction

16 years agoTactic reduce got rid of. Use normalize, instead.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 13:27:00 +0000 (13:27 +0000)]
Tactic reduce got rid of. Use normalize, instead.
Rationale: the two tactics did the very same thing, but normalizes exploits
reduction machines and so it is really faster in many cases.

16 years agowhd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 13:25:42 +0000 (13:25 +0000)]
whd: ~delta=false now controls also zeta-reduction. This greatly speed-ups
some operations when definitions are in the context.
Moreover, the semantics seems more reasonable (????).

16 years agoAn unimplemented case of clearbody is now implemented.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 11:06:26 +0000 (11:06 +0000)]
An unimplemented case of clearbody is now implemented.

16 years agocheck_metasenv_consistency:
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 10:39:45 +0000 (10:39 +0000)]
check_metasenv_consistency:
big ad-hoc performance improvement propagated from CicTypeChecker to CicRefine.
This really cuts down the total refinement time in some situations (freescale).

16 years agoExample query fixed.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 10:23:40 +0000 (10:23 +0000)]
Example query fixed.

16 years agoDebugging print removed.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 10:02:57 +0000 (10:02 +0000)]
Debugging print removed.

16 years agoAdded ad-hoc optimization for check_metasenv_consistency, case Rel to Let-in
Claudio Sacerdoti Coen [Sun, 9 Mar 2008 18:28:05 +0000 (18:28 +0000)]
Added ad-hoc optimization for check_metasenv_consistency, case Rel to Let-in
vs Def. Rationale: this is the case of an IRL when the metavariable is
created in a context with definitions. Without this optimization, a (possibly
expensive) reduction is always triggered.

Note: this should be better handled using a reduction strategy based on
heights.

16 years agoPerformance improvement: let-ins should always be pushed to the context with
Claudio Sacerdoti Coen [Sun, 9 Mar 2008 17:45:49 +0000 (17:45 +0000)]
Performance improvement: let-ins should always be pushed to the context with
their type (to avoid multiple re-typing).

16 years agoScripts fixed. They were broken since the change to the behaviour of CicMetaSubst...
Claudio Sacerdoti Coen [Sun, 9 Mar 2008 17:20:51 +0000 (17:20 +0000)]
Scripts fixed. They were broken since the change to the behaviour of CicMetaSubst.delift w.r.t. definitions in the context.

16 years agoLAMBDA-TYPES: some more generation lemmas and some proofs improved
Ferruccio Guidi [Sun, 9 Mar 2008 16:59:41 +0000 (16:59 +0000)]
LAMBDA-TYPES: some more generation lemmas and some proofs improved

16 years agoPotentially (and, at least sometimes, actually) big performance improvement:
Claudio Sacerdoti Coen [Sun, 9 Mar 2008 16:53:38 +0000 (16:53 +0000)]
Potentially (and, at least sometimes, actually) big performance improvement:
let-in were always zeta-expanded during delifting. As a result, implicit,
in a context with definitions, were always refined with a type that was well
typed, but only up to (potentially expensive) reduction!