]>
Git — Sourcephile - haskell/symantic.git/log
Julien Moutinho [Tue, 27 Jun 2017 06:27:09 +0000 (08:27 +0200)]
Rename source -> withSource, and g_*.
Julien Moutinho [Sat, 24 Jun 2017 21:45:42 +0000 (23:45 +0200)]
Polish comments.
Julien Moutinho [Sat, 24 Jun 2017 21:16:26 +0000 (23:16 +0200)]
Remove Proxy in Sym instances.
Julien Moutinho [Fri, 23 Jun 2017 14:09:06 +0000 (16:09 +0200)]
Polish for publication.
Julien Moutinho [Fri, 23 Jun 2017 14:04:22 +0000 (16:04 +0200)]
Add make target %/fast.
Julien Moutinho [Fri, 23 Jun 2017 13:31:25 +0000 (15:31 +0200)]
Add display exception for the list type [].
Julien Moutinho [Fri, 23 Jun 2017 11:20:54 +0000 (13:20 +0200)]
Fix Dim.
Julien Moutinho [Fri, 23 Jun 2017 00:11:11 +0000 (02:11 +0200)]
Use symantic-document to write docType.
Julien Moutinho [Thu, 22 Jun 2017 22:12:58 +0000 (00:12 +0200)]
Add replicate.
Julien Moutinho [Thu, 22 Jun 2017 21:06:42 +0000 (23:06 +0200)]
Fix handling of Fixity in showType.
Julien Moutinho [Thu, 22 Jun 2017 20:40:40 +0000 (22:40 +0200)]
Add Config_showType.
Julien Moutinho [Thu, 22 Jun 2017 16:13:27 +0000 (18:13 +0200)]
Use AllowAmbiguousTypes to avoid Proxy uses.
Julien Moutinho [Thu, 22 Jun 2017 15:48:44 +0000 (17:48 +0200)]
Change Term to be a GADT, to avoid type applications and allow TypeOf Term.
Julien Moutinho [Thu, 22 Jun 2017 14:32:25 +0000 (16:32 +0200)]
Fix symantic-lib tests.
Julien Moutinho [Thu, 22 Jun 2017 14:28:03 +0000 (16:28 +0200)]
Fix symantic-grammar test.
Julien Moutinho [Thu, 22 Jun 2017 14:08:45 +0000 (16:08 +0200)]
Put symantic-document before symantic and symantic-lib.
Julien Moutinho [Thu, 22 Jun 2017 14:07:23 +0000 (16:07 +0200)]
Remove debugging entry map_f.
Julien Moutinho [Wed, 21 Jun 2017 22:01:37 +0000 (00:01 +0200)]
Fix description.
Julien Moutinho [Wed, 21 Jun 2017 19:57:43 +0000 (21:57 +0200)]
Bump versions.
Julien Moutinho [Wed, 21 Jun 2017 19:57:00 +0000 (21:57 +0200)]
Add symantic-document.
Julien Moutinho [Sun, 18 Jun 2017 22:52:03 +0000 (00:52 +0200)]
Add some Eq and Show instances.
Julien Moutinho [Sun, 18 Jun 2017 20:25:33 +0000 (22:25 +0200)]
Improve dynamic insertion of terms (via CtxTy or Modules).
Julien Moutinho [Fri, 16 Jun 2017 10:22:03 +0000 (12:22 +0200)]
Clarification : Megaparsec integration.
Julien Moutinho [Thu, 15 Jun 2017 23:59:51 +0000 (01:59 +0200)]
Clarification : eqKi -> eqKind.
Julien Moutinho [Thu, 15 Jun 2017 23:49:30 +0000 (01:49 +0200)]
Improve the module system.
Julien Moutinho [Tue, 13 Jun 2017 14:57:26 +0000 (16:57 +0200)]
Improve handling of metadata in grammars.
Julien Moutinho [Sun, 11 Jun 2017 19:06:35 +0000 (21:06 +0200)]
Support directories as targets in GNUmakefile.
Julien Moutinho [Sun, 11 Jun 2017 19:05:51 +0000 (21:05 +0200)]
Massive rewrite to better support rank-1 polymorphic types.
Julien Moutinho [Thu, 11 May 2017 14:34:29 +0000 (16:34 +0200)]
Try the new Type and Term design against the actual needs.
Julien Moutinho [Mon, 1 May 2017 23:02:35 +0000 (01:02 +0200)]
Improve Show of Type.
Julien Moutinho [Sun, 30 Apr 2017 21:53:57 +0000 (23:53 +0200)]
Archive old attempt to remove proto tokens without polymorphic types.
Julien Moutinho [Sun, 30 Apr 2017 21:32:35 +0000 (23:32 +0200)]
Cleanup dead-end attempts.
Julien Moutinho [Sun, 30 Apr 2017 20:51:07 +0000 (22:51 +0200)]
Complexify the type system to support rank-1 polymorphic types and terms.
With polymorphic types now expressible,
the proto token workaround should be removable,
since every token should now be able to directly have a Type/Term,
thus no longer needing to be applied to a few others before having it.
As a consequence of merging Type and Term,
the symantic machinery will have to be moved to TeSym,
and thus also carried by Type. WIP.
Julien Moutinho [Sat, 22 Apr 2017 01:28:48 +0000 (03:28 +0200)]
Try to implement polymorphic types.
Julien Moutinho [Wed, 19 Apr 2017 10:08:37 +0000 (12:08 +0200)]
Fix prefix/postfix operators wrt. term application.
Julien Moutinho [Sat, 8 Apr 2017 17:37:33 +0000 (19:37 +0200)]
Add compileWithTyCtx.
Julien Moutinho [Sat, 1 Apr 2017 22:34:49 +0000 (00:34 +0200)]
Add support for (>=>).
Julien Moutinho [Sat, 1 Apr 2017 15:19:47 +0000 (17:19 +0200)]
Add GNUmakefile rule : tag.
Julien Moutinho [Sat, 1 Apr 2017 14:49:13 +0000 (16:49 +0200)]
Fix Mono{Foldable,Functor} and {Semi,Is}Sequence constraints.
Cleaner to support the constraints
in the various data types' Proj_TyConC
instead of the constraints'.
For instance, this avoids to require the IO TyConst
when using MonoFunctor.
Julien Moutinho [Fri, 31 Mar 2017 13:00:40 +0000 (15:00 +0200)]
Add withContext.
Julien Moutinho [Fri, 24 Mar 2017 00:31:44 +0000 (01:31 +0100)]
Fix stack clean.
Julien Moutinho [Fri, 24 Mar 2017 00:15:22 +0000 (01:15 +0100)]
Rename grammar rules, prefixing them with g_.
Julien Moutinho [Thu, 23 Mar 2017 23:36:34 +0000 (00:36 +0100)]
Rename Term_Name -> TeName
Julien Moutinho [Thu, 23 Mar 2017 23:30:31 +0000 (00:30 +0100)]
Add IsString instances.
Julien Moutinho [Tue, 14 Mar 2017 14:48:21 +0000 (15:48 +0100)]
Fix time&space explosion of GHC's typechecker.
Julien Moutinho [Mon, 13 Mar 2017 09:14:51 +0000 (10:14 +0100)]
Add Lib.{Bounded,Enum,Ratio,Rational,Real,Semigroup}.
Julien Moutinho [Sat, 11 Mar 2017 02:59:27 +0000 (03:59 +0100)]
Fix comment typo.
Julien Moutinho [Fri, 10 Mar 2017 00:27:57 +0000 (01:27 +0100)]
Fix lexeme to progress over indented lines.
Julien Moutinho [Fri, 10 Mar 2017 00:25:50 +0000 (01:25 +0100)]
Renaming Constants -> TyConsts.
Julien Moutinho [Fri, 10 Mar 2017 00:20:04 +0000 (01:20 +0100)]
Cosmetic cleanup of GHC flags.
Julien Moutinho [Wed, 8 Mar 2017 06:21:32 +0000 (07:21 +0100)]
Add GNUmakefile.
Julien Moutinho [Wed, 8 Mar 2017 06:15:53 +0000 (07:15 +0100)]
Cosmetic cleanup.
Julien Moutinho [Wed, 8 Mar 2017 04:23:17 +0000 (05:23 +0100)]
Fix Inj_ConstP -> Inj_TyConstP.
Julien Moutinho [Tue, 7 Mar 2017 02:57:26 +0000 (03:57 +0100)]
Use AllowAmbiguousTypes to avoid using Proxy.
Julien Moutinho [Mon, 6 Mar 2017 22:32:24 +0000 (23:32 +0100)]
Cosmetic cleanup.
Julien Moutinho [Mon, 6 Mar 2017 22:31:37 +0000 (23:31 +0100)]
Fix empty and eoi.
Julien Moutinho [Mon, 6 Mar 2017 22:30:09 +0000 (23:30 +0100)]
Backtrack (try) the grammar only when necessary to get better error messages.
Julien Moutinho [Sun, 5 Mar 2017 19:12:39 +0000 (20:12 +0100)]
Gather type declarations and infix declarations.
Julien Moutinho [Sun, 5 Mar 2017 02:29:20 +0000 (03:29 +0100)]
Reduce compile time of tests with -O0 -fmax-simplifier-iterations=0.
Julien Moutinho [Fri, 10 Feb 2017 10:39:14 +0000 (11:39 +0100)]
Split into symantic{,-grammar,-lib}.
Julien Moutinho [Wed, 8 Feb 2017 19:18:08 +0000 (20:18 +0100)]
Bump version.
Julien Moutinho [Wed, 8 Feb 2017 19:01:57 +0000 (20:01 +0100)]
Renames.
Julien Moutinho [Wed, 8 Feb 2017 16:05:07 +0000 (17:05 +0100)]
Polish doc.
Julien Moutinho [Wed, 8 Feb 2017 16:04:33 +0000 (17:04 +0100)]
Add optional.
Julien Moutinho [Mon, 6 Feb 2017 15:16:31 +0000 (16:16 +0100)]
Add stack.yaml.
Julien Moutinho [Mon, 6 Feb 2017 11:30:50 +0000 (12:30 +0100)]
Update doc.
Julien Moutinho [Sat, 4 Feb 2017 07:10:18 +0000 (08:10 +0100)]
Fix Lib.Ord : Ordering.
Julien Moutinho [Sat, 4 Feb 2017 05:29:48 +0000 (06:29 +0100)]
Fix module including.
Julien Moutinho [Fri, 3 Feb 2017 06:25:40 +0000 (07:25 +0100)]
Use more TypeApplications.
Julien Moutinho [Fri, 3 Feb 2017 06:18:28 +0000 (07:18 +0100)]
Remove Alternative uses in grammars.
Julien Moutinho [Fri, 3 Feb 2017 03:34:56 +0000 (04:34 +0100)]
Fix Lib.Text.
Julien Moutinho [Thu, 2 Feb 2017 03:14:08 +0000 (04:14 +0100)]
Move libraries in Lib.
Julien Moutinho [Mon, 23 Jan 2017 13:31:20 +0000 (14:31 +0100)]
Add Gram_Term.
Julien Moutinho [Wed, 11 Jan 2017 01:18:47 +0000 (02:18 +0100)]
Add Parsing.Grammar.
Julien Moutinho [Fri, 6 Jan 2017 18:48:29 +0000 (19:48 +0100)]
Fix comment typo.
Julien Moutinho [Thu, 5 Jan 2017 19:49:19 +0000 (20:49 +0100)]
Add Compiling.Alternative.
Julien Moutinho [Thu, 5 Jan 2017 19:48:43 +0000 (20:48 +0100)]
Renaming textI_app* to textI*.
Julien Moutinho [Thu, 5 Jan 2017 05:13:22 +0000 (06:13 +0100)]
Clarify names, and add commentaries (bis).
Julien Moutinho [Wed, 4 Jan 2017 02:58:31 +0000 (03:58 +0100)]
Clarify names, and add commentaries.
Julien Moutinho [Tue, 3 Jan 2017 20:39:52 +0000 (21:39 +0100)]
Add Compiling.Show.
Julien Moutinho [Fri, 30 Dec 2016 21:29:12 +0000 (22:29 +0100)]
Add Parsing.Token.
Julien Moutinho [Sat, 10 Dec 2016 19:32:29 +0000 (20:32 +0100)]
Add Compiling.Sequences.
Julien Moutinho [Sat, 10 Dec 2016 04:37:29 +0000 (05:37 +0100)]
Add Compiling.NonNull.
Julien Moutinho [Sat, 10 Dec 2016 02:51:00 +0000 (03:51 +0100)]
Add Compiling.MonoFoldable.
Julien Moutinho [Fri, 9 Dec 2016 04:28:04 +0000 (05:28 +0100)]
Add Typing.Family and Compiling.MonoFunctor.
Julien Moutinho [Thu, 8 Dec 2016 01:50:22 +0000 (02:50 +0100)]
Add tests for Compiling.
Julien Moutinho [Wed, 7 Dec 2016 21:22:08 +0000 (22:22 +0100)]
Fix lambda application.
Julien Moutinho [Wed, 7 Dec 2016 03:26:22 +0000 (04:26 +0100)]
Use GHC-8.0.1's TypeInType to handle kinds better, and migrate Compiling.
Julien Moutinho [Sun, 4 Dec 2016 00:59:07 +0000 (01:59 +0100)]
Add Compiling, Interpreting and Transforming.
Julien Moutinho [Thu, 24 Nov 2016 19:04:08 +0000 (20:04 +0100)]
Simplify the Constraint projection
Julien Moutinho [Thu, 24 Nov 2016 04:47:58 +0000 (05:47 +0100)]
Revamp the type system.
This is definitively much more correct, simple and powerful this way:
kinds are now properly handled,
type constraints capture is now quite neat,
and usable type variables should be possible.
Though the current code may seem obvious and natural
for the task at hand, it required
first to know that this was indeed this task that has to be done…
Indeed I was previously much more focused on the symantics part,
but this happened when I decided to put a day or two
to check if type inferencing would indeed be possible with the previous type system,
I rapidly convinced myself that I couldn't handle type variables as required,
so I then put aside the previous type system to work anew
from the main (mono)type of Top,
which also appears in Write You a Haskell:
data Type
= TVar TVar
| TCon String
| TArr Type Type
As in the previous type system,
I first tried to have Type indexing an Haskell type (h)
by using the usual GADTs way,
which was surprisingly possible for every kind:
once I realized this could be done through Proxy
(this definitively is a very important type
to compute with GHC's type system),
and found that the type application could be handled
with a type family, which could effectively let me build types
from an AST, the type family's result just stays abstract,
and GADTs put constraints in scope with it in them.
The Index GADT of GLambda was my inspiration to handle type constants
through a type list of them, and thus drop the previous approach
which was indexing types (and not type constants)
and required much more code.
I then tried to have Type always well-formed through GADTs,
my first attempt was (stupidly) to only check the arity,
then I realized it was not enough and introduced a Kind type.
At this point I was able to kindcheck an AST of a type,
but failed to replicate the previous approach to capture a Constraint,
hopefully I then tried (without much hope it would work)
to do the "obvious thing" (since this is what GHC does),
that is to add a type constraint kind into Kind,
which proved itself quite rewarding.
Surprisingly I've quickly found that introducing UnProxy
enables to capture Constraints which need to work on abstract types,
like (Eq a) to prove (Eq (Maybe a)).
Work ahead is to try to update the previous approach
to build expressions with symantics.
Then later to try again type inferencing.
Cheers :-)
Julien Moutinho [Sat, 19 Nov 2016 13:39:02 +0000 (14:39 +0100)]
factorizing Type1_From ast Type0
Julien Moutinho [Fri, 18 Nov 2016 22:27:00 +0000 (23:27 +0100)]
polish code
Julien Moutinho [Fri, 18 Nov 2016 22:10:03 +0000 (23:10 +0100)]
fix Num requiring Integer
Julien Moutinho [Fri, 18 Nov 2016 21:46:44 +0000 (22:46 +0100)]
Type1_From instances
Julien Moutinho [Fri, 18 Nov 2016 21:16:36 +0000 (22:16 +0100)]
polish code, Foldable
Julien Moutinho [Thu, 17 Nov 2016 01:32:14 +0000 (02:32 +0100)]
Repr_Dup helpers
Julien Moutinho [Wed, 16 Nov 2016 11:38:26 +0000 (12:38 +0100)]
Foldable, Num
Julien Moutinho [Wed, 16 Nov 2016 06:05:05 +0000 (07:05 +0100)]
explore parsing of partially applied functions
Julien Moutinho [Mon, 14 Nov 2016 22:17:12 +0000 (23:17 +0100)]
polish names