]>
matita.cs.unibo.it Git - helm.git/log
Ferruccio Guidi [Fri, 9 Nov 2012 18:56:55 +0000 (18:56 +0000)]
- mac (ma count)
small program to count the number of characters (not bytes) in a .ma
file excluding (possibly nested) comments, repeated spaces, and escape
characters in strings
- lambda_delta:
Makefile updated to use mac
Andrea Asperti [Fri, 9 Nov 2012 17:57:33 +0000 (17:57 +0000)]
if_multi.ma
Andrea Asperti [Fri, 9 Nov 2012 15:09:23 +0000 (15:09 +0000)]
done
Ferruccio Guidi [Wed, 7 Nov 2012 17:48:14 +0000 (17:48 +0000)]
- commit completed!!
The static type of <W>.T is now the static type of T.
This allows to prove that each valid term has a static type as
expected!
Andrea Asperti [Wed, 7 Nov 2012 16:59:25 +0000 (16:59 +0000)]
New multi tapes machines
Ferruccio Guidi [Wed, 7 Nov 2012 16:46:54 +0000 (16:46 +0000)]
- commit of the component: static
- notation updates missing in former commit
Ferruccio Guidi [Wed, 7 Nov 2012 16:18:41 +0000 (16:18 +0000)]
- predefined_virtuals: nwe characters
- lib: some additions
- lambda_delta: commit of the components gramma, substitution, unfold
- we parked the support for the "bt-reduction"
- some renaming ...
Ferruccio Guidi [Mon, 29 Oct 2012 18:28:47 +0000 (18:28 +0000)]
- we set up the support for the "bt-reduction" of Automath literature
- we now use the STIX GENERAL fonts for a better rendering of U+2B43
Ferruccio Guidi [Sun, 28 Oct 2012 14:39:27 +0000 (14:39 +0000)]
an addition ...
Ferruccio Guidi [Sat, 27 Oct 2012 13:34:28 +0000 (13:34 +0000)]
- some additions and corrections
Claudio Sacerdoti Coen [Fri, 19 Oct 2012 10:59:51 +0000 (10:59 +0000)]
One useless Obj.magic removed.
Ferruccio Guidi [Thu, 18 Oct 2012 15:01:55 +0000 (15:01 +0000)]
- additions in basic_2
- substitution of downloadable logo is now complete!
Ferruccio Guidi [Thu, 18 Oct 2012 14:57:26 +0000 (14:57 +0000)]
- some confluence results for focalized reduction and computation
- more notation to be used later on ....
Ferruccio Guidi [Tue, 16 Oct 2012 18:15:13 +0000 (18:15 +0000)]
- milestone update in basic_2
- the new logo for the Crux is now linked to the site
- version update for xhtbl
Ferruccio Guidi [Tue, 16 Oct 2012 18:11:21 +0000 (18:11 +0000)]
context-free parallel reduction on closures is confluent!
Ferruccio Guidi [Mon, 15 Oct 2012 15:26:26 +0000 (15:26 +0000)]
- xhtbl: we added the construction + to place several keys in one cell
- basic_2_src: corrected and updated to use the operator +
Ferruccio Guidi [Sat, 13 Oct 2012 21:37:29 +0000 (21:37 +0000)]
updates in basic_2 ...
Ferruccio Guidi [Sat, 13 Oct 2012 21:35:45 +0000 (21:35 +0000)]
- parallel reduction for local environments: we proved the equivalence
between the old context-sensitive version and the focalized version
- as a result, the context-sensitive version disappears with its derivatives
Wilmer Ricciotti [Mon, 8 Oct 2012 14:33:46 +0000 (14:33 +0000)]
Downgrades buggy destruct patch.
Wilmer Ricciotti [Fri, 5 Oct 2012 12:25:35 +0000 (12:25 +0000)]
Removes debug prints that were left from last commit.
Wilmer Ricciotti [Fri, 5 Oct 2012 10:08:05 +0000 (10:08 +0000)]
This patch allows generation of minimally dependent discrimination principles
for inductive types, in the case where Leibniz equality is used.
Ferruccio Guidi [Sat, 29 Sep 2012 21:51:19 +0000 (21:51 +0000)]
bugfix in Makefiles
Ferruccio Guidi [Sat, 29 Sep 2012 17:33:22 +0000 (17:33 +0000)]
- updates in basic_2
Ferruccio Guidi [Sat, 29 Sep 2012 17:28:48 +0000 (17:28 +0000)]
- full commit for the transtive closure of ltpss!
Ferruccio Guidi [Fri, 28 Sep 2012 20:48:41 +0000 (20:48 +0000)]
additions to basic_2
Ferruccio Guidi [Fri, 28 Sep 2012 20:45:20 +0000 (20:45 +0000)]
- partial commit (static component only)
- results on the transitive closure of ltpss
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.