]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years ago- some additions to basic_2
Ferruccio Guidi [Fri, 28 Sep 2012 17:14:12 +0000 (17:14 +0000)]
- some additions to basic_2
- new logo for lambda_delta

12 years ago- partial commit (unfold component only)
Ferruccio Guidi [Fri, 28 Sep 2012 17:07:46 +0000 (17:07 +0000)]
- partial commit (unfold component only)
  we introduced the transitive closure of ltpss,
  which we now use in the definition of thin

12 years agoMore work on inserting UnsafeCoerce in argument applications only when needed.
Claudio Sacerdoti Coen [Wed, 19 Sep 2012 16:42:51 +0000 (16:42 +0000)]
More work on inserting UnsafeCoerce in argument applications only when needed.

12 years agoGHC.Prim.Any fixed
Claudio Sacerdoti Coen [Wed, 19 Sep 2012 16:42:27 +0000 (16:42 +0000)]
GHC.Prim.Any fixed

12 years agothe partial commit continues ...
Ferruccio Guidi [Wed, 5 Sep 2012 16:09:37 +0000 (16:09 +0000)]
the partial commit continues ...

12 years ago1. deriving (Show) no longer used because it fails on empty types
Claudio Sacerdoti Coen [Tue, 4 Sep 2012 07:55:26 +0000 (07:55 +0000)]
1. deriving (Show) no longer used because it fails on empty types
2. pretty-printing of types fixed: application arguments never had
   parentheses
3. Top replaced with GHC.Prim.Any

12 years agopartial update in basic_2 ...
Ferruccio Guidi [Mon, 3 Sep 2012 14:32:06 +0000 (14:32 +0000)]
partial update in basic_2 ...

12 years agolambda_delta: partial commit ...
Ferruccio Guidi [Mon, 3 Sep 2012 14:30:24 +0000 (14:30 +0000)]
lambda_delta: partial commit ...

12 years agoComposite coercions are now extracted too.
Claudio Sacerdoti Coen [Thu, 30 Aug 2012 08:22:05 +0000 (08:22 +0000)]
Composite coercions are now extracted too.

12 years agoName mangling until separate extraction is implemented.
Claudio Sacerdoti Coen [Thu, 30 Aug 2012 08:02:28 +0000 (08:02 +0000)]
Name mangling until separate extraction is implemented.

12 years agoCode to make all global names in a file fresh.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 16:11:06 +0000 (16:11 +0000)]
Code to make all global names in a file fresh.

12 years agoCapitalization of variables bound in patterns fixed.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 13:00:29 +0000 (13:00 +0000)]
Capitalization of variables bound in patterns fixed.

12 years ago...
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:54:15 +0000 (12:54 +0000)]
...

12 years agoFixed indentation, which is semantic in Haskell.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:32:52 +0000 (12:32 +0000)]
Fixed indentation, which is semantic in Haskell.

12 years ago(Part of previous two commits)
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:10:02 +0000 (12:10 +0000)]
(Part of previous two commits)

12 years ago(Part of previous commit)
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:09:20 +0000 (12:09 +0000)]
(Part of previous commit)

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