]> matita.cs.unibo.it Git - helm.git/log
helm.git
12 years ago- mac (ma count)
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

12 years agoif_multi.ma
Andrea Asperti [Fri, 9 Nov 2012 17:57:33 +0000 (17:57 +0000)]
if_multi.ma

12 years agodone
Andrea Asperti [Fri, 9 Nov 2012 15:09:23 +0000 (15:09 +0000)]
done

12 years ago- commit completed!!
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!

12 years agoNew multi tapes machines
Andrea Asperti [Wed, 7 Nov 2012 16:59:25 +0000 (16:59 +0000)]
New multi tapes machines

12 years ago- commit of the component: static
Ferruccio Guidi [Wed, 7 Nov 2012 16:46:54 +0000 (16:46 +0000)]
- commit of the component: static
- notation updates missing in former commit

12 years ago- predefined_virtuals: nwe characters
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 ...

12 years ago- we set up the support for the "bt-reduction" of Automath literature
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

12 years agoan addition ...
Ferruccio Guidi [Sun, 28 Oct 2012 14:39:27 +0000 (14:39 +0000)]
an addition ...

12 years ago- some additions and corrections
Ferruccio Guidi [Sat, 27 Oct 2012 13:34:28 +0000 (13:34 +0000)]
- some additions and corrections

12 years agoOne useless Obj.magic removed.
Claudio Sacerdoti Coen [Fri, 19 Oct 2012 10:59:51 +0000 (10:59 +0000)]
One useless Obj.magic removed.

12 years ago- additions in basic_2
Ferruccio Guidi [Thu, 18 Oct 2012 15:01:55 +0000 (15:01 +0000)]
- additions in basic_2
- substitution of downloadable logo is now complete!

12 years ago- some confluence results for focalized reduction and computation
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 ....

12 years ago- milestone update in basic_2
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

12 years agocontext-free parallel reduction on closures is confluent!
Ferruccio Guidi [Tue, 16 Oct 2012 18:11:21 +0000 (18:11 +0000)]
context-free parallel reduction on closures is confluent!

12 years ago- xhtbl: we added the construction + to place several keys in one cell
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 +

12 years agoupdates in basic_2 ...
Ferruccio Guidi [Sat, 13 Oct 2012 21:37:29 +0000 (21:37 +0000)]
updates in basic_2 ...

12 years ago- parallel reduction for local environments: we proved the equivalence
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

12 years agoDowngrades buggy destruct patch.
Wilmer Ricciotti [Mon, 8 Oct 2012 14:33:46 +0000 (14:33 +0000)]
Downgrades buggy destruct patch.

12 years agoRemoves debug prints that were left from last commit.
Wilmer Ricciotti [Fri, 5 Oct 2012 12:25:35 +0000 (12:25 +0000)]
Removes debug prints that were left from last commit.

12 years agoThis patch allows generation of minimally dependent discrimination principles
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.

12 years agobugfix in Makefiles
Ferruccio Guidi [Sat, 29 Sep 2012 21:51:19 +0000 (21:51 +0000)]
bugfix in Makefiles

12 years ago- updates in basic_2
Ferruccio Guidi [Sat, 29 Sep 2012 17:33:22 +0000 (17:33 +0000)]
- updates in basic_2

12 years ago- full commit for the transtive closure of ltpss!
Ferruccio Guidi [Sat, 29 Sep 2012 17:28:48 +0000 (17:28 +0000)]
- full commit for the transtive closure of ltpss!

12 years agoadditions to basic_2
Ferruccio Guidi [Fri, 28 Sep 2012 20:48:41 +0000 (20:48 +0000)]
additions to basic_2

12 years ago- partial commit (static component only)
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

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.