Commit Graph

7787 Commits

Author SHA1 Message Date
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
Paul Chiusano
e6f432ead4 added lookupType 2013-12-03 11:29:25 -05:00
Paul Chiusano
bce030ad13 finished with check function 2013-12-02 19:32:04 -05:00
Paul Chiusano
8d7eca2ca1 more progress on check function 2013-12-02 18:57:24 -05:00
Paul Chiusano
1afb99f260 added literal checking 2013-11-25 23:51:20 -05:00
Paul Chiusano
07e9491517 added literals to types 2013-11-25 23:39:41 -05:00
Paul Chiusano
32a382a1cd renamed literal type param to 2013-11-25 23:22:25 -05:00
Paul Chiusano
8a816d93e2 tweak to term representation - no longer bakes in Var, for consistency with Element and Type ADTs 2013-11-25 23:16:26 -05:00
Paul Chiusano
062dc65325 parameterized term over literals type 2013-11-25 23:01:13 -05:00
Paul Chiusano
f7b4b90846 added check signature 2013-11-25 22:33:44 -05:00
Paul Chiusano
7d46efecaa finished with instantiateL/R 2013-11-21 13:15:46 -05:00
Paul Chiusano
ce73bab33d subtype function now compiling, removed use of DataKinds 2013-09-27 16:29:01 -04:00
Paul Chiusano
581a9b3aa7 added extra param to Forall actor, just need to get Context compiling 2013-09-27 00:24:51 -04:00
Paul Chiusano
a88fa4a621 working on subtyping operation 2013-09-26 19:56:13 -04:00
Paul Chiusano
365617774a Added fresh variable supply to context, minor notes 2013-09-22 12:34:32 -04:00
Paul Chiusano
c568357355 Context substitution 2013-09-22 00:13:40 -04:00
Paul Chiusano
e86a528d7f wellformed context check 2013-09-21 23:08:26 -04:00
Paul Chiusano
b4486ac6ce Algorithmic context well formedness 2013-09-21 22:15:49 -04:00
Paul Chiusano
1de38e9f2e Context elements, and some refactoring of variable references 2013-09-21 14:43:17 -04:00
Paul Chiusano
1ce1a0f6e3 Type syntax 2013-09-20 23:37:34 -04:00
Paul Chiusano
17cd797c66 Added helper function for creating single argument Lam and Examples module 2013-09-20 20:16:14 -04:00
Paul Chiusano
c5b9c4b5c3 Added project structure and Syntax.Term 2013-09-20 19:31:34 -04:00
pchiusano
2cb2e73962 Initial commit 2013-09-19 13:44:05 -07:00