]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Fri, 28 Sep 2012 17:14:12 +0000 (17:14 +0000)]
- some additions to basic_2
- new logo for lambda_delta
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
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.
Claudio Sacerdoti Coen [Wed, 19 Sep 2012 16:42:27 +0000 (16:42 +0000)]
GHC.Prim.Any fixed
Ferruccio Guidi [Wed, 5 Sep 2012 16:09:37 +0000 (16:09 +0000)]
the partial commit continues ...
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
Ferruccio Guidi [Mon, 3 Sep 2012 14:32:06 +0000 (14:32 +0000)]
partial update in basic_2 ...
Ferruccio Guidi [Mon, 3 Sep 2012 14:30:24 +0000 (14:30 +0000)]
lambda_delta: partial commit ...
Claudio Sacerdoti Coen [Thu, 30 Aug 2012 08:22:05 +0000 (08:22 +0000)]
Composite coercions are now extracted too.
Claudio Sacerdoti Coen [Thu, 30 Aug 2012 08:02:28 +0000 (08:02 +0000)]
Name mangling until separate extraction is implemented.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 16:11:06 +0000 (16:11 +0000)]
Code to make all global names in a file fresh.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 13:00:29 +0000 (13:00 +0000)]
Capitalization of variables bound in patterns fixed.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:54:15 +0000 (12:54 +0000)]
...
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:32:52 +0000 (12:32 +0000)]
Fixed indentation, which is semantic in Haskell.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:10:02 +0000 (12:10 +0000)]
(Part of previous two commits)
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 12:09:20 +0000 (12:09 +0000)]
(Part of previous commit)
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.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 08:44:25 +0000 (08:44 +0000)]
Top used also for fixes.
Claudio Sacerdoti Coen [Wed, 29 Aug 2012 08:21:28 +0000 (08:21 +0000)]
Match 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.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 16:13:44 +0000 (16:13 +0000)]
Dead code removed.
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
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.
Wilmer Ricciotti [Tue, 28 Aug 2012 14:47:44 +0000 (14:47 +0000)]
progress in uni_step
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.
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.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 13:25:55 +0000 (13:25 +0000)]
...
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 09:48:25 +0000 (09:48 +0000)]
Fixed pretty-printing of types of variables bound in patterns.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 09:39:53 +0000 (09:39 +0000)]
Patterns are now computed according to the extracted constructor type.
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 08:55:32 +0000 (08:55 +0000)]
pattern arguments where printed in reverse order
Claudio Sacerdoti Coen [Tue, 28 Aug 2012 08:46:19 +0000 (08:46 +0000)]
Bug fixed: rhs in match were printed in wrong context.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 16:28:29 +0000 (16:28 +0000)]
...
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 16:26:23 +0000 (16:26 +0000)]
...
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
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.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 14:25:45 +0000 (14:25 +0000)]
...
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
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 13:32:31 +0000 (13:32 +0000)]
Self contained now.
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)
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:59:08 +0000 (12:59 +0000)]
Fixed left/right context distinction in inductive types.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:16:12 +0000 (12:16 +0000)]
Pretty printing of context (variable refreshing) fixed.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:05:30 +0000 (12:05 +0000)]
size_of_type fixed and simplified
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:02:53 +0000 (12:02 +0000)]
No pattern matching over empty types in Haskell
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 12:00:52 +0000 (12:00 +0000)]
Infos stored for inductive types.
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.
Claudio Sacerdoti Coen [Mon, 27 Aug 2012 09:08:42 +0000 (09:08 +0000)]
Added kind signatures to data declaration.
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)
Wilmer Ricciotti [Mon, 27 Aug 2012 08:43:30 +0000 (08:43 +0000)]
End of copy.ma
Ferruccio Guidi [Sat, 25 Aug 2012 20:23:42 +0000 (20:23 +0000)]
update of logo completed!
Ferruccio Guidi [Sat, 25 Aug 2012 20:15:31 +0000 (20:15 +0000)]
still updating ...
Ferruccio Guidi [Sat, 25 Aug 2012 19:27:01 +0000 (19:27 +0000)]
we are updating the logo of lambda_delta ...
Ferruccio Guidi [Fri, 24 Aug 2012 17:26:41 +0000 (17:26 +0000)]
sample table for character classes
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 ...
Ferruccio Guidi [Fri, 24 Aug 2012 15:24:14 +0000 (15:24 +0000)]
- renaming complete
- noe file was missing
Ferruccio Guidi [Fri, 24 Aug 2012 14:45:02 +0000 (14:45 +0000)]
some renaming ...
Ferruccio Guidi [Thu, 23 Aug 2012 17:15:24 +0000 (17:15 +0000)]
we updated the contribution porting it to the new matita ...
Claudio Sacerdoti Coen [Wed, 22 Aug 2012 16:57:38 +0000 (16:57 +0000)]
Preliminary work on (co)inductive types.
Wilmer Ricciotti [Wed, 15 Aug 2012 17:33:55 +0000 (17:33 +0000)]
progress
Wilmer Ricciotti [Thu, 9 Aug 2012 12:03:09 +0000 (12:03 +0000)]
Work in progress.
Wilmer Ricciotti [Wed, 8 Aug 2012 12:09:51 +0000 (12:09 +0000)]
Adding GRealize to uni_step.
Andrea Asperti [Wed, 8 Aug 2012 09:22:58 +0000 (09:22 +0000)]
porting to termination
Andrea Asperti [Tue, 7 Aug 2012 09:07:22 +0000 (09:07 +0000)]
guarded realizability
Ferruccio Guidi [Mon, 6 Aug 2012 14:55:28 +0000 (14:55 +0000)]
dependences update
Andrea Asperti [Fri, 3 Aug 2012 13:02:40 +0000 (13:02 +0000)]
A compiling version (not complete).
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.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 20:03:52 +0000 (20:03 +0000)]
...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 18:16:44 +0000 (18:16 +0000)]
...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 18:16:39 +0000 (18:16 +0000)]
Pretty printing of patterns done almost correctly.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 16:38:01 +0000 (16:38 +0000)]
Tentative code for Fixpoint. Still to be completed.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 16:37:41 +0000 (16:37 +0000)]
...
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:56:00 +0000 (15:56 +0000)]
Path fixed.
Claudio Sacerdoti Coen [Thu, 2 Aug 2012 15:44:16 +0000 (15:44 +0000)]
Code extraction branched.
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"
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.
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
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.
Claudio Sacerdoti Coen [Wed, 1 Aug 2012 15:24:45 +0000 (15:24 +0000)]
Tests for code extraction; to be moved elsewhere.
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.
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.
Andrea Asperti [Tue, 31 Jul 2012 13:44:02 +0000 (13:44 +0000)]
work in progress
Andrea Asperti [Tue, 31 Jul 2012 09:18:34 +0000 (09:18 +0000)]
Termination!
Wilmer Ricciotti [Mon, 30 Jul 2012 14:08:36 +0000 (14:08 +0000)]
Wip
Andrea Asperti [Mon, 30 Jul 2012 13:47:37 +0000 (13:47 +0000)]
work in progress
Ferruccio Guidi [Sun, 29 Jul 2012 17:44:50 +0000 (17:44 +0000)]
update in basic_2
Ferruccio Guidi [Sun, 29 Jul 2012 17:41:46 +0000 (17:41 +0000)]
- context free computation for terms and local environments
Ferruccio Guidi [Fri, 27 Jul 2012 19:02:27 +0000 (19:02 +0000)]
additions and corrections to basic_2
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
Wilmer Ricciotti [Fri, 27 Jul 2012 16:03:28 +0000 (16:03 +0000)]
work in progress
Andrea Asperti [Fri, 27 Jul 2012 14:59:12 +0000 (14:59 +0000)]
work in progress
Ferruccio Guidi [Thu, 26 Jul 2012 15:01:09 +0000 (15:01 +0000)]
polarized binders introduced in basic_2
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)
Ferruccio Guidi [Tue, 24 Jul 2012 08:10:59 +0000 (08:10 +0000)]
one file was missing ...
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
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
Andrea Asperti [Sat, 21 Jul 2012 14:07:48 +0000 (14:07 +0000)]
An executable version of the tutorial.
Wilmer Ricciotti [Fri, 20 Jul 2012 01:33:26 +0000 (01:33 +0000)]
progress in termination of marks.ma
Claudio Sacerdoti Coen [Thu, 19 Jul 2012 22:59:13 +0000 (22:59 +0000)]
One less warning.
Claudio Sacerdoti Coen [Thu, 19 Jul 2012 22:58:14 +0000 (22:58 +0000)]
Some debugging times exposed.
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.
Andrea Asperti [Thu, 19 Jul 2012 14:43:48 +0000 (14:43 +0000)]
Few changes