]>
matita.cs.unibo.it Git - helm.git/log
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
Enrico Tassi [Thu, 3 Apr 2008 16:16:59 +0000 (16:16 +0000)]
guarded_by_destructor ported, many auxiliary functions still to be done
Enrico Tassi [Thu, 3 Apr 2008 16:15:51 +0000 (16:15 +0000)]
removed FSF banner
Enrico Tassi [Thu, 3 Apr 2008 15:42:10 +0000 (15:42 +0000)]
added ugly test showing many many bugs in the current kernel
Enrico Tassi [Wed, 2 Apr 2008 13:15:27 +0000 (13:15 +0000)]
added slim version of does_not_occur
Enrico Tassi [Wed, 2 Apr 2008 13:14:45 +0000 (13:14 +0000)]
added translation of Set to Type0 (avoid warning)
Enrico Tassi [Wed, 2 Apr 2008 12:56:27 +0000 (12:56 +0000)]
fixes backported from the new kernel
Enrico Tassi [Wed, 2 Apr 2008 09:39:23 +0000 (09:39 +0000)]
removed dummy rewrite
Enrico Tassi [Wed, 2 Apr 2008 09:30:32 +0000 (09:30 +0000)]
removed dummy rewrite
Enrico Tassi [Wed, 2 Apr 2008 09:23:30 +0000 (09:23 +0000)]
removed dummy rewrites
Enrico Tassi [Wed, 2 Apr 2008 09:22:14 +0000 (09:22 +0000)]
fixed according to the new rewrite semantics (fails if no progress)
Enrico Tassi [Wed, 2 Apr 2008 09:18:08 +0000 (09:18 +0000)]
fixed depends after the removal of Fsub
Enrico Tassi [Tue, 1 Apr 2008 19:07:11 +0000 (19:07 +0000)]
better check for progress
Claudio Sacerdoti Coen [Tue, 1 Apr 2008 17:51:14 +0000 (17:51 +0000)]
typeof_obj0 implemented
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
Enrico Tassi [Tue, 1 Apr 2008 14:08:11 +0000 (14:08 +0000)]
progress made better, still not perfect
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.
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
Enrico Tassi [Tue, 1 Apr 2008 08:20:29 +0000 (08:20 +0000)]
added set_ppterm
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!)
Claudio Sacerdoti Coen [Mon, 31 Mar 2008 17:45:01 +0000 (17:45 +0000)]
Large amount of duplicated code (still in comments) factorized.
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.
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
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
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
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
Enrico Tassi [Thu, 27 Mar 2008 10:50:09 +0000 (10:50 +0000)]
added iterators over NCic terms
Enrico Tassi [Thu, 27 Mar 2008 10:49:40 +0000 (10:49 +0000)]
removed FSF header
Wilmer Ricciotti [Thu, 27 Mar 2008 10:22:56 +0000 (10:22 +0000)]
Updated depedencies.
Enrico Tassi [Thu, 27 Mar 2008 09:58:08 +0000 (09:58 +0000)]
insert comments of old tpechecker
Wilmer Ricciotti [Wed, 26 Mar 2008 17:59:11 +0000 (17:59 +0000)]
Reorganization of list library (step 1)
Enrico Tassi [Tue, 25 Mar 2008 17:56:20 +0000 (17:56 +0000)]
new are_convertible and head_beta_reduce
Enrico Tassi [Tue, 25 Mar 2008 15:59:51 +0000 (15:59 +0000)]
context for fixpoint body created in the hopefully right order
Enrico Tassi [Tue, 25 Mar 2008 15:51:59 +0000 (15:51 +0000)]
ported to the Cic LetIn with explicit type
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
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
Enrico Tassi [Tue, 25 Mar 2008 15:34:32 +0000 (15:34 +0000)]
very very interesting hack
Wilmer Ricciotti [Tue, 25 Mar 2008 13:52:29 +0000 (13:52 +0000)]
small update
Enrico Tassi [Tue, 25 Mar 2008 13:23:33 +0000 (13:23 +0000)]
argument of type mcu_type always abstracted first
Enrico Tassi [Tue, 25 Mar 2008 12:21:24 +0000 (12:21 +0000)]
XXX this is the beginning of the metaocaml work XXX
Enrico Tassi [Sun, 23 Mar 2008 18:55:49 +0000 (18:55 +0000)]
Fsub moved in contribs
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
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
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
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
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
Claudio Sacerdoti Coen [Thu, 20 Mar 2008 21:08:08 +0000 (21:08 +0000)]
New syntax for auto-related tactics and conclude/obtain.
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).
Ferruccio Guidi [Thu, 20 Mar 2008 18:26:49 +0000 (18:26 +0000)]
Base-2 is not compiling properly and is excluded for now
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
Enrico Tassi [Thu, 20 Mar 2008 13:07:09 +0000 (13:07 +0000)]
new semantics for 'by t'
Enrico Tassi [Thu, 20 Mar 2008 13:02:05 +0000 (13:02 +0000)]
removed pointless test
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...
Enrico Tassi [Thu, 20 Mar 2008 12:56:05 +0000 (12:56 +0000)]
added library option to auto
Enrico Tassi [Thu, 20 Mar 2008 12:42:45 +0000 (12:42 +0000)]
letins are no more unfolded, we do that by hand
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
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.
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).
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 19:03:22 +0000 (19:03 +0000)]
-debug improved
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 18:57:40 +0000 (18:57 +0000)]
...
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:52:07 +0000 (17:52 +0000)]
prerr_endline => debug_print
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:44:49 +0000 (17:44 +0000)]
prerr_endline => debug_print
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.
Claudio Sacerdoti Coen [Wed, 19 Mar 2008 17:23:13 +0000 (17:23 +0000)]
Files committed by Enrico (a mistake, I suppose) removed.
Ferruccio Guidi [Wed, 19 Mar 2008 15:35:15 +0000 (15:35 +0000)]
Procedural : added some missing cases
LAMBDA-TYPES: improved preambles
Ferruccio Guidi [Tue, 18 Mar 2008 19:22:41 +0000 (19:22 +0000)]
LAMBDA-TYPES: level 2 dependences are now correct, at least :)
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
Claudio Sacerdoti Coen [Fri, 14 Mar 2008 12:00:54 +0000 (12:00 +0000)]
Tests enabled again.
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.
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)
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).
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.
Enrico Tassi [Wed, 12 Mar 2008 12:44:59 +0000 (12:44 +0000)]
fixed implicit
Andrea Asperti [Wed, 12 Mar 2008 12:02:02 +0000 (12:02 +0000)]
Nuova dimostrazione riflessiva di le_to_Bertrand.
Enrico Tassi [Wed, 12 Mar 2008 10:37:10 +0000 (10:37 +0000)]
if -debug is specified do not catch all exceptions
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)
Enrico Tassi [Mon, 10 Mar 2008 15:56:52 +0000 (15:56 +0000)]
fixed wrong dependencies in debian package reported by oliboni
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.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 15:49:51 +0000 (15:49 +0000)]
...
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
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.
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 (????).
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 11:06:26 +0000 (11:06 +0000)]
An unimplemented case of clearbody is now implemented.
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).
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 10:23:40 +0000 (10:23 +0000)]
Example query fixed.
Claudio Sacerdoti Coen [Mon, 10 Mar 2008 10:02:57 +0000 (10:02 +0000)]
Debugging print removed.
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.
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).
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.
Ferruccio Guidi [Sun, 9 Mar 2008 16:59:41 +0000 (16:59 +0000)]
LAMBDA-TYPES: some more generation lemmas and some proofs improved
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!
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.
Enrico Tassi [Thu, 6 Mar 2008 16:34:15 +0000 (16:34 +0000)]
* please let the library in shape *
Enrico Tassi [Thu, 6 Mar 2008 16:21:16 +0000 (16:21 +0000)]
fixed
Enrico Tassi [Thu, 6 Mar 2008 15:42:16 +0000 (15:42 +0000)]
skipped freescale and dama_didactic
Enrico Tassi [Thu, 6 Mar 2008 15:39:26 +0000 (15:39 +0000)]
fixed deps
Enrico Tassi [Thu, 6 Mar 2008 15:37:52 +0000 (15:37 +0000)]
reworked freescale stuff to put \m as a left parameter
Enrico Tassi [Thu, 6 Mar 2008 15:32:47 +0000 (15:32 +0000)]
no more assembly/ to skip
Enrico Tassi [Thu, 6 Mar 2008 15:13:52 +0000 (15:13 +0000)]
fix typo
Enrico Tassi [Thu, 6 Mar 2008 15:09:47 +0000 (15:09 +0000)]
added mkdir