Paul Chiusano
a9359fd5dc
added eta reduction Action and eliminated usage of lam1M
2014-06-25 11:13:13 -04:00
Paul Chiusano
d54dd1bade
now using Noted monad transformer in more places to greatly reduce plumbing code
2014-06-25 10:49:00 -04:00
Paul Chiusano
af91eded80
cleanup, using Noted monad for less plumbing code
2014-06-24 18:22:56 -04:00
Paul Chiusano
889ea04b1c
Added Noted monad
2014-06-24 17:38:04 -04:00
Paul Chiusano
9cf566560d
stubbed out edit function
2014-06-24 16:54:01 -04:00
Paul Chiusano
847a3b185d
fixed all compile errors and updated cabal file following change to handling of naming in term binders
2014-06-23 17:10:01 -04:00
Paul Chiusano
75cbc241fa
using Axelsson-Claesson naming for binders in Term
2014-06-23 13:39:24 -04:00
Paul Chiusano
efae244700
fixed bug in retract where annotated types in context weren’t being retracted
2014-06-20 16:56:37 -04:00
Paul Chiusano
a03dbc9ab5
fixed typechecker bugs
2014-06-20 15:20:36 -04:00
Paul Chiusano
d368116fb9
Added pretty printing of terms/types
2014-06-20 14:00:20 -04:00
Paul Chiusano
05a58e4c6e
remove dead code
2014-06-19 14:02:29 -04:00
Paul Chiusano
54d1c981d1
Adding more examples
2014-06-19 13:57:51 -04:00
Paul Chiusano
9388409d88
Removed warning
2014-06-19 13:57:40 -04:00
Paul Chiusano
87e9718ad3
More progress on Node
2014-06-19 13:57:06 -04:00
Paul Chiusano
8404ce5e3f
Implemented several Node functions
2014-06-18 13:12:34 -04:00
Paul Chiusano
0103864689
Got rid of Layout, this type will be pure Unison, rather than being imported from Haskell
2014-06-18 11:51:56 -04:00
Paul Chiusano
64026b272e
Cleaned up interface to type checker
2014-06-18 10:46:55 -04:00
Paul Chiusano
7cb8c7bd2e
Moved Note to top level Unison package, as it’s being used for error reporting throughout
2014-06-18 09:58:44 -04:00
Paul Chiusano
a4f84194ec
Term literals can contain layouts, also added Read instances for Term / Type
2014-06-18 09:12:53 -04:00
Paul Chiusano
b5b26698c3
Generalized node creation slightly
2014-06-17 22:18:48 -04:00
Paul Chiusano
c2fb5d9575
fixed case in check
2014-06-17 19:40:49 -04:00
Paul Chiusano
5a8d22c6bc
Terms may now contain references to other terms by hash, which are expanded when type checking.
...
Terms are thus dynamically linked to other terms (important for code sizes), but we support incremental type checking. The node permanently caches a type for each term hash. When typechecking a term, we simply lookup the already computed types of any hashes it references, rather than redoing their typechecking problem.
2014-06-17 18:03:56 -04:00
Paul Chiusano
cc85d3dcf6
Starting on implementation of Node
2014-06-16 17:12:55 -04:00
Paul Chiusano
e44938ee14
Term and type are now monomorphic, polymorphism over literals and constraints wasn’t buying much
2014-06-16 14:47:59 -04:00
Paul Chiusano
83e6548633
updated Term
2014-06-16 13:04:10 -04:00
Paul Chiusano
605282accf
Unison.Language package, which commits to particular choices of term and type literals
2014-06-16 12:50:38 -04:00
Paul Chiusano
01deebc32f
Moving Layout to Unison.Language package
2014-06-16 11:13:05 -04:00
Paul Chiusano
ffbaf28a89
Node API reasonably complete
2014-06-13 17:54:28 -04:00
Paul Chiusano
f9428720e5
Start of node API
2014-06-13 16:38:19 -04:00
Paul Chiusano
c3759de14c
signatures for hashing types and terms
2014-06-11 18:08:42 -04:00
Paul Chiusano
f656cde69d
cabal file cleanup
2014-06-10 18:57:18 -04:00
Paul Chiusano
f963c249e7
Eval module
2014-06-10 18:20:06 -04:00
Paul Chiusano
ebe5652324
cabal file edits
2014-06-10 18:19:47 -04:00
Paul Chiusano
3c11cf84a5
hardcoding font choice for header
2014-03-28 14:59:58 -04:00
Paul Chiusano
07c21e26b0
minor site formatting tweaks
2014-03-28 14:51:08 -04:00
Paul Chiusano
8bca969385
static hakyll site
2014-03-28 14:32:07 -04:00
Paul Chiusano
2b4ddb27cb
more progress on implementing edit actions
2014-01-16 23:29:40 -05:00
Paul Chiusano
dc432c46d9
abstract operation is now type preserving
2014-01-14 18:52:10 -05:00
Paul Chiusano
1e33941c90
editing combinators progress
2014-01-14 18:48:22 -05:00
Paul Chiusano
5eef578a28
Added better diagnostics in event of type error
2013-12-15 02:44:36 -05:00
Paul Chiusano
af40c4a85f
fixed typing issues caused by accidentally reversing the context in breakAt
, now successfully inferring type of identity function
2013-12-15 02:15:20 -05:00
Paul Chiusano
c98d22f33c
some debugging of camas milner rule, which isn't generalizing properly
2013-12-14 23:36:12 -05:00
Paul Chiusano
889d9ea4c9
Code compiling and fixed a few substitution bugs
2013-12-14 22:54:03 -05:00
Paul Chiusano
0ecb0d2e03
Finished simplification of Term/Type/Context representation
2013-12-13 21:08:04 -05:00
Paul Chiusano
30fb17317f
Progress simplifying type repr
2013-12-10 23:27:11 -05:00
Paul Chiusano
b690c3f191
finished with synthesizeApp, which completes draft of typechecking algorithm
2013-12-10 10:12:00 -05:00
Paul Chiusano
5a5fd5f054
docs for synthesize case
2013-12-08 00:29:41 -05:00
Paul Chiusano
5ee535dbfd
finished with synthesize function
2013-12-08 00:26:04 -05:00
Paul Chiusano
a34fc319b6
stub for synthesizeApp
2013-12-05 08:57:55 -05:00
Paul Chiusano
14559b8b3d
more progress on type synthesis function
2013-12-05 08:40:29 -05:00