]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years agoExtraction is now integrated with the usual machinery for serialization of
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:08:54 +0000 (12:08 +0000)]
Extraction is now integrated with the usual machinery for serialization of
commands.

12 years agoTop used also for fixes.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 08:44:25 +0000 (08:44 +0000)]
Top used also for fixes.

12 years agoMatch in types handled using top.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 08:21:28 +0000 (08:21 +0000)]
Match in types handled using top.

12 years agoMatch in types handled using Top.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 08:21:18 +0000 (08:21 +0000)]
Match in types handled using Top.

12 years agoDead code removed.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 16:13:44 +0000 (16:13 +0000)]
Dead code removed.

12 years agoMatch in classification of non-terms taken in account.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 16:11:37 +0000 (16:11 +0000)]
Match in classification of non-terms taken in account.
We take the sup of the classification of all branches according to the
order

`Proposition < `PropKind < `Type < `Kind < `KindOrType

12 years agoKnown bug fixed: the rhs of a match over a small singleton inductive type
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 15:16:10 +0000 (15:16 +0000)]
Known bug fixed: the rhs of a match over a small singleton inductive type
needed delifting to take it out its lhs.

12 years agoprogress in uni_step
Wilmer Ricciotti [Tue, 28 Aug 2012 14:47:44 +0000 (14:47 +0000)]
progress in uni_step

12 years agoBasics/logic.ma no longer raises exception.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 14:35:46 +0000 (14:35 +0000)]
Basics/logic.ma no longer raises exception.
Many workaround introduced to feed arguments to polymorphically kinded functions.

12 years agoBug fixed: when extracting pattern matching on singleton types it is possible
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 13:27:25 +0000 (13:27 +0000)]
Bug fixed: when extracting pattern matching on singleton types it is possible
that a type is faced during the computation of the type of its constructor.
Ad-hoc patch added.

12 years ago...
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 13:25:55 +0000 (13:25 +0000)]
...

12 years agoFixed pretty-printing of types of variables bound in patterns.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 09:48:25 +0000 (09:48 +0000)]
Fixed pretty-printing of types of variables bound in patterns.

12 years agoPatterns are now computed according to the extracted constructor type.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 09:39:53 +0000 (09:39 +0000)]
Patterns are now computed according to the extracted constructor type.

12 years agopattern arguments where printed in reverse order
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 08:55:32 +0000 (08:55 +0000)]
pattern arguments where printed in reverse order

12 years agoBug fixed: rhs in match were printed in wrong context.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 08:46:19 +0000 (08:46 +0000)]
Bug fixed: rhs in match were printed in wrong context.

12 years ago...
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 16:28:29 +0000 (16:28 +0000)]
...

12 years ago...
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 16:26:23 +0000 (16:26 +0000)]
...

12 years agoCode for computing patterns the way Haskell likes them (lhs + rhs).
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 16:26:15 +0000 (16:26 +0000)]
Code for computing patterns the way Haskell likes them (lhs + rhs).
Currently bugged:
 - some DeBrujin problems in the rhs
 - ignores the extracted type of the constructor (uses the CiC type)
 - does not perform eta-expansion when needed

12 years agoFixed pretty-printing of mutual recursive stuff and improved machinery to
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 15:11:26 +0000 (15:11 +0000)]
Fixed pretty-printing of mutual recursive stuff and improved machinery to
pretty print references.

12 years ago...
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 14:25:45 +0000 (14:25 +0000)]
...

12 years ago1. fixed pretty-printing of constructors, type variables, etc.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 14:25:35 +0000 (14:25 +0000)]
1. fixed pretty-printing of constructors, type variables, etc.
2. added UnsafeCoerce to pattern matching in an over-approximating way

12 years agoSelf contained now.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 13:32:31 +0000 (13:32 +0000)]
Self contained now.

12 years ago1. added Skip to terms to maintain consistency between Rels and context
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 13:20:14 +0000 (13:20 +0000)]
1. added Skip to terms to maintain consistency between Rels and context
   (required for pretty printing)

12 years agoFixed left/right context distinction in inductive types.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:59:08 +0000 (12:59 +0000)]
Fixed left/right context distinction in inductive types.

12 years agoPretty printing of context (variable refreshing) fixed.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:16:12 +0000 (12:16 +0000)]
Pretty printing of context (variable refreshing) fixed.

12 years agosize_of_type fixed and simplified
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:05:30 +0000 (12:05 +0000)]
size_of_type fixed and simplified

12 years agoNo pattern matching over empty types in Haskell
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:02:53 +0000 (12:02 +0000)]
No pattern matching over empty types in Haskell

12 years agoInfos stored for inductive types.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:00:52 +0000 (12:00 +0000)]
Infos stored for inductive types.

12 years agoPreliminary extraction of constructors.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 10:20:26 +0000 (10:20 +0000)]
Preliminary extraction of constructors.

BUG: ghc only allows forall quantifications at the beginning of the
 type! Needs re-ordering.

12 years agoAdded kind signatures to data declaration.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 09:08:42 +0000 (09:08 +0000)]
Added kind signatures to data declaration.

12 years ago1. Dominic:
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 08:58:57 +0000 (08:58 +0000)]
1. Dominic:
 - kinds signature in explicit for-all (if not simple kinds)
 - Haskell names of Matita names (still bugged)
 - improved pretty-printing (only necessary brackets)
2. CC types are now extracted to F_omega types even when NotInFOmega
   (exception removed altogether)

12 years agoEnd of copy.ma
Wilmer Ricciotti [Mon, 27 Aug 2012 08:43:30 +0000 (08:43 +0000)]
End of copy.ma

12 years agoupdate of logo completed!
Ferruccio Guidi [Sat, 25 Aug 2012 20:23:42 +0000 (20:23 +0000)]
update of logo completed!

12 years agostill updating ...
Ferruccio Guidi [Sat, 25 Aug 2012 20:15:31 +0000 (20:15 +0000)]
still updating ...

12 years agowe are updating the logo of lambda_delta ...
Ferruccio Guidi [Sat, 25 Aug 2012 19:27:01 +0000 (19:27 +0000)]
we are updating the logo of lambda_delta ...

12 years agosample table for character classes
Ferruccio Guidi [Fri, 24 Aug 2012 17:26:41 +0000 (17:26 +0000)]
sample table for character classes

12 years ago- Makefile update
Ferruccio Guidi [Fri, 24 Aug 2012 17:23:13 +0000 (17:23 +0000)]
- Makefile update
- for now the page related to BTM is committed here ...

12 years ago- renaming complete
Ferruccio Guidi [Fri, 24 Aug 2012 15:24:14 +0000 (15:24 +0000)]
- renaming complete
- noe file was missing

12 years agosome renaming ...
Ferruccio Guidi [Fri, 24 Aug 2012 14:45:02 +0000 (14:45 +0000)]
some renaming ...

12 years agowe updated the contribution porting it to the new matita ...
Ferruccio Guidi [Thu, 23 Aug 2012 17:15:24 +0000 (17:15 +0000)]
we updated the contribution porting it to the new matita ...

12 years agoPreliminary work on (co)inductive types.
Claudio Sacerdoti Coen [Wed, 22 Aug 2012 16:57:38 +0000 (16:57 +0000)]
Preliminary work on (co)inductive types.

12 years agoprogress
Wilmer Ricciotti [Wed, 15 Aug 2012 17:33:55 +0000 (17:33 +0000)]
progress

12 years agoWork in progress.
Wilmer Ricciotti [Thu, 9 Aug 2012 12:03:09 +0000 (12:03 +0000)]
Work in progress.

12 years agoAdding GRealize to uni_step.
Wilmer Ricciotti [Wed, 8 Aug 2012 12:09:51 +0000 (12:09 +0000)]
Adding GRealize to uni_step.

12 years agoporting to termination
Andrea Asperti [Wed, 8 Aug 2012 09:22:58 +0000 (09:22 +0000)]
porting to termination

12 years agoguarded realizability
Andrea Asperti [Tue, 7 Aug 2012 09:07:22 +0000 (09:07 +0000)]
guarded realizability

12 years agodependences update
Ferruccio Guidi [Mon, 6 Aug 2012 14:55:28 +0000 (14:55 +0000)]
dependences update

12 years agoA compiling version (not complete).
Andrea Asperti [Fri, 3 Aug 2012 13:02:40 +0000 (13:02 +0000)]
A compiling version (not complete).

12 years agoBug fixed: the context generated by l.h.s. binders was appended in wrong order.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 20:05:10 +0000 (20:05 +0000)]
Bug fixed: the context generated by l.h.s. binders was appended in wrong order.

12 years ago...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 20:03:52 +0000 (20:03 +0000)]
...

12 years ago...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 18:16:44 +0000 (18:16 +0000)]
...

12 years agoPretty printing of patterns done almost correctly.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 18:16:39 +0000 (18:16 +0000)]
Pretty printing of patterns done almost correctly.

12 years agoTentative code for Fixpoint. Still to be completed.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 16:38:01 +0000 (16:38 +0000)]
Tentative code for Fixpoint. Still to be completed.

12 years ago...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 16:37:41 +0000 (16:37 +0000)]
...

12 years agoPath fixed.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:56:00 +0000 (15:56 +0000)]
Path fixed.

12 years agoCode extraction branched.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:44:16 +0000 (15:44 +0000)]
Code extraction branched.

12 years agoTemporary stuff to test code extraction. Running make produces
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:42:20 +0000 (15:42 +0000)]
Temporary stuff to test code extraction. Running make produces
extraction.hs which is checked by "ghci extraction.hs"

12 years ago1. Implemented type inference for Fomega to extract term application correctly.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:41:46 +0000 (15:41 +0000)]
1. Implemented type inference for Fomega to extract term application correctly.
2. Fixed the Decl classification.

12 years agoBugs fixed:
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 09:34:00 +0000 (09:34 +0000)]
Bugs fixed:
1. the context was processed in reverse order
2. the classification of types was wrong

12 years agoBugs related to pretty printing of names fixed (capitalization, name
Claudio Sacerdoti Coen [Wed, 1 Aug 2012 16:37:09 +0000 (16:37 +0000)]
Bugs related to pretty printing of names fixed (capitalization, name
clashes, etc.). In particular removed binders (propositionals) were sometimes
still counted.

12 years agoTests for code extraction; to be moved elsewhere.
Claudio Sacerdoti Coen [Wed, 1 Aug 2012 15:24:45 +0000 (15:24 +0000)]
Tests for code extraction; to be moved elsewhere.

12 years agoBug fixed: Haskell forces capitalisation.
Claudio Sacerdoti Coen [Wed, 1 Aug 2012 15:23:59 +0000 (15:23 +0000)]
Bug fixed: Haskell forces capitalisation.
But still open: name clashes due to capitalisation.

12 years agoBegin of porting of code extraction to the new Matita.
Claudio Sacerdoti Coen [Wed, 1 Aug 2012 12:25:54 +0000 (12:25 +0000)]
Begin of porting of code extraction to the new Matita.
The file does not belong to the kernel: it will be moved away soon.
The extraction code is not branched yet and it does not need to be compiled.

12 years agowork in progress
Andrea Asperti [Tue, 31 Jul 2012 13:44:02 +0000 (13:44 +0000)]
work in progress

12 years agoTermination!
Andrea Asperti [Tue, 31 Jul 2012 09:18:34 +0000 (09:18 +0000)]
Termination!

12 years agoWip
Wilmer Ricciotti [Mon, 30 Jul 2012 14:08:36 +0000 (14:08 +0000)]
Wip

12 years agowork in progress
Andrea Asperti [Mon, 30 Jul 2012 13:47:37 +0000 (13:47 +0000)]
work in progress

12 years agoupdate in basic_2
Ferruccio Guidi [Sun, 29 Jul 2012 17:44:50 +0000 (17:44 +0000)]
update in basic_2

12 years ago- context free computation for terms and local environments
Ferruccio Guidi [Sun, 29 Jul 2012 17:41:46 +0000 (17:41 +0000)]
- context free computation for terms and local environments

12 years agoadditions and corrections to basic_2
Ferruccio Guidi [Fri, 27 Jul 2012 19:02:27 +0000 (19:02 +0000)]
additions and corrections to basic_2

12 years ago- support for pointwise extensions of a term relation started ...
Ferruccio Guidi [Fri, 27 Jul 2012 19:00:53 +0000 (19:00 +0000)]
- support for pointwise extensions of a term relation started ...
- we now support abstract liftable relations

12 years agowork in progress
Wilmer Ricciotti [Fri, 27 Jul 2012 16:03:28 +0000 (16:03 +0000)]
work in progress

12 years agowork in progress
Andrea Asperti [Fri, 27 Jul 2012 14:59:12 +0000 (14:59 +0000)]
work in progress

12 years agopolarized binders introduced in basic_2
Ferruccio Guidi [Thu, 26 Jul 2012 15:01:09 +0000 (15:01 +0000)]
polarized binders introduced in basic_2

12 years ago- matita: reset_font_size () added after matita.conf.xml is read to set
Ferruccio Guidi [Thu, 26 Jul 2012 14:53:37 +0000 (14:53 +0000)]
- matita: reset_font_size () added after matita.conf.xml is read to set
the font size specified by the user
- lambda_delta: equivalence between normal forms irreducible terms
proved (context-sensitive version)

12 years agoone file was missing ...
Ferruccio Guidi [Tue, 24 Jul 2012 08:10:59 +0000 (08:10 +0000)]
one file was missing ...

12 years ago- lambda_delta: we updated some notation
Ferruccio Guidi [Mon, 23 Jul 2012 20:32:03 +0000 (20:32 +0000)]
- lambda_delta: we updated some notation
                we are switching from context-free to context-sensitive reducible terms
- basics/star:  star constructor refl renamed to srefl to avoid name clash with id constructor refl

12 years ago- we polarized binders to control zeta reduction
Ferruccio Guidi [Sun, 22 Jul 2012 12:38:39 +0000 (12:38 +0000)]
- we polarized binders to control zeta reduction
- confluence and strong normalization proved

12 years agoAn executable version of the tutorial.
Andrea Asperti [Sat, 21 Jul 2012 14:07:48 +0000 (14:07 +0000)]
An executable version of the tutorial.

12 years agoprogress in termination of marks.ma
Wilmer Ricciotti [Fri, 20 Jul 2012 01:33:26 +0000 (01:33 +0000)]
progress in termination of marks.ma

12 years agoOne less warning.
Claudio Sacerdoti Coen [Thu, 19 Jul 2012 22:59:13 +0000 (22:59 +0000)]
One less warning.

12 years agoSome debugging times exposed.
Claudio Sacerdoti Coen [Thu, 19 Jul 2012 22:58:14 +0000 (22:58 +0000)]
Some debugging times exposed.

12 years agoMajor speed up improvement after every tactic application.
Claudio Sacerdoti Coen [Thu, 19 Jul 2012 22:11:00 +0000 (22:11 +0000)]
Major speed up improvement after every tactic application.
Exponential algorithm (in the size of the sequent) turned into linear.
It only shows for very large sequents though.

12 years agoFew changes
Andrea Asperti [Thu, 19 Jul 2012 14:43:48 +0000 (14:43 +0000)]
Few changes

12 years ago- intermediate commit to allow debugging of auto tactic in xprs.ma
Ferruccio Guidi [Thu, 19 Jul 2012 13:52:06 +0000 (13:52 +0000)]
- intermediate commit to allow debugging of auto tactic in xprs.ma
- extended computation is now defined (its De Vrijer's reduction rt)
- stratified native validity is now defined (it's supposed to be
easier to deal with than native type assignment)

12 years agoadding tutorial
Andrea Asperti [Thu, 19 Jul 2012 09:19:39 +0000 (09:19 +0000)]
adding tutorial

12 years agoporting to termination
Andrea Asperti [Tue, 17 Jul 2012 14:11:24 +0000 (14:11 +0000)]
porting to termination

12 years ago- we added a time specification in the generated web pages
Ferruccio Guidi [Fri, 13 Jul 2012 19:08:47 +0000 (19:08 +0000)]
- we added a time specification in the generated web pages
- update in basic_2

12 years agomore symbols added for lambda_delta
Ferruccio Guidi [Fri, 13 Jul 2012 16:30:19 +0000 (16:30 +0000)]
more symbols added for lambda_delta

12 years ago- dynamic type assignment dismissed for now
Ferruccio Guidi [Fri, 13 Jul 2012 16:28:23 +0000 (16:28 +0000)]
- dynamic type assignment dismissed for now
- stratified static type assignment and unwind defined

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 14:33:06 +0000 (14:33 +0000)]
commit by user mkmluser

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 08:55:11 +0000 (08:55 +0000)]
commit by user mkmluser

12 years agocommit by user mkmluser
matitaweb [Tue, 10 Jul 2012 08:54:01 +0000 (08:54 +0000)]
commit by user mkmluser

12 years agomanual commit
matitaweb [Mon, 9 Jul 2012 12:44:27 +0000 (12:44 +0000)]
manual commit

12 years agobug fixes
matitaweb [Sun, 8 Jul 2012 07:19:18 +0000 (07:19 +0000)]
bug fixes

12 years agoreverted to previous version (plus anchors)
matitaweb [Fri, 6 Jul 2012 14:02:50 +0000 (14:02 +0000)]
reverted to previous version (plus anchors)

12 years agoadded tick.png
Wilmer Ricciotti [Fri, 6 Jul 2012 13:27:08 +0000 (13:27 +0000)]
added tick.png

12 years agoAdded NotationPt.name_of_obj.
Wilmer Ricciotti [Fri, 6 Jul 2012 12:39:18 +0000 (12:39 +0000)]
Added NotationPt.name_of_obj.

12 years agoCosmetic changes.
Wilmer Ricciotti [Fri, 6 Jul 2012 12:35:32 +0000 (12:35 +0000)]
Cosmetic changes.

12 years agoBug fixing + cosmetic changes
Wilmer Ricciotti [Fri, 6 Jul 2012 12:32:08 +0000 (12:32 +0000)]
Bug fixing + cosmetic changes