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

16 years agoRedundant check (because of an invariant) removed.
Claudio Sacerdoti Coen [Sun, 9 Mar 2008 16:51:36 +0000 (16:51 +0000)]
Redundant check (because of an invariant) removed.
The check was added by Tassi when adding universe constraints.
However, it is now believed to be useless.

16 years ago* please let the library in shape *
Enrico Tassi [Thu, 6 Mar 2008 16:34:15 +0000 (16:34 +0000)]
* please let the library in shape *

16 years agofixed
Enrico Tassi [Thu, 6 Mar 2008 16:21:16 +0000 (16:21 +0000)]
fixed

16 years agoskipped freescale and dama_didactic
Enrico Tassi [Thu, 6 Mar 2008 15:42:16 +0000 (15:42 +0000)]
skipped freescale and dama_didactic

16 years agofixed deps
Enrico Tassi [Thu, 6 Mar 2008 15:39:26 +0000 (15:39 +0000)]
fixed deps

16 years agoreworked freescale stuff to put \m as a left parameter
Enrico Tassi [Thu, 6 Mar 2008 15:37:52 +0000 (15:37 +0000)]
reworked freescale stuff to put \m as a left parameter

16 years agono more assembly/ to skip
Enrico Tassi [Thu, 6 Mar 2008 15:32:47 +0000 (15:32 +0000)]
no more assembly/ to skip

16 years agofix typo
Enrico Tassi [Thu, 6 Mar 2008 15:13:52 +0000 (15:13 +0000)]
fix typo

16 years agoadded mkdir
Enrico Tassi [Thu, 6 Mar 2008 15:09:47 +0000 (15:09 +0000)]
added mkdir

16 years ago...
Enrico Tassi [Thu, 6 Mar 2008 11:11:10 +0000 (11:11 +0000)]
...

16 years agosome corrections and additions
Ferruccio Guidi [Wed, 5 Mar 2008 18:26:38 +0000 (18:26 +0000)]
some corrections and additions

16 years agofrom now on, export MATITA_EXTRACT=true to extract
Enrico Tassi [Wed, 5 Mar 2008 11:08:21 +0000 (11:08 +0000)]
from now on, export MATITA_EXTRACT=true to extract

16 years agoverbosity increased in case of error
Enrico Tassi [Wed, 5 Mar 2008 10:18:51 +0000 (10:18 +0000)]
verbosity increased in case of error

16 years agocomponents/library: dotdothack removed
Ferruccio Guidi [Tue, 4 Mar 2008 19:10:48 +0000 (19:10 +0000)]
components/library: dotdothack removed
legacy & LAMBDA-TYPES support $(MATITAUSEROPTIONS) (= -system for fguidi)
LAMBDA-TYPES: two missing generation lemmas added

16 years agoNew syntax for patterns.
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 16:42:17 +0000 (16:42 +0000)]
New syntax for patterns.

16 years agoprodT ==> prod
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 16:12:25 +0000 (16:12 +0000)]
prodT ==> prod

16 years agoA) New version.
Claudio Sacerdoti Coen [Tue, 4 Mar 2008 15:44:36 +0000 (15:44 +0000)]
A) New version.
B) set "baseuri" removed
C) minor clean-up

16 years agowe added the classic substitution function
Ferruccio Guidi [Fri, 29 Feb 2008 18:13:10 +0000 (18:13 +0000)]
we added the classic substitution function

16 years agofirs attempt to compile with ocamlbuild
Enrico Tassi [Thu, 28 Feb 2008 08:42:37 +0000 (08:42 +0000)]
firs attempt to compile with ocamlbuild

16 years agothe proof of bertrand's conjecture is now complete
Wilmer Ricciotti [Wed, 27 Feb 2008 17:03:01 +0000 (17:03 +0000)]
the proof of bertrand's conjecture is now complete

16 years agoI added some debugging information
Ferruccio Guidi [Tue, 26 Feb 2008 17:23:37 +0000 (17:23 +0000)]
I added some debugging information

16 years agoadded MATITAOPTIONS -onepass as for LAMBDA-TYPES
Ferruccio Guidi [Tue, 26 Feb 2008 17:20:47 +0000 (17:20 +0000)]
added MATITAOPTIONS -onepass as for LAMBDA-TYPES