| 0082ea4 | mkolosick | 02 July 2019, 22:43:33 UTC | Updated constraint generation to match paper. Note: abz.hs currently hangs and all implicit examples are broken | 02 July 2019, 22:43:33 UTC |
| 876cfae | mkolosick | 02 July 2019, 22:41:45 UTC | Updated pretty-print to include cubifying | 02 July 2019, 22:41:45 UTC |
| 09b6bd6 | mkolosick | 02 July 2019, 22:41:29 UTC | Pseudo mist linear examples | 02 July 2019, 22:41:29 UTC |
| 7833fdc | mkolosick | 28 June 2019, 18:13:09 UTC | pseudo-mist revoke, tick, and linear access | 02 July 2019, 16:00:47 UTC |
| a2b22e3 | mkolosick | 28 June 2019, 18:12:20 UTC | renaming split on accident | 28 June 2019, 18:12:20 UTC |
| 829fca4 | mkolosick | 28 June 2019, 18:11:40 UTC | removed debugging info | 28 June 2019, 18:11:40 UTC |
| d5df0e5 | mkolosick | 05 June 2019, 21:18:44 UTC | Updated todo testing framework | 05 June 2019, 21:18:44 UTC |
| fe707ec | Anish Tondwalkar | 05 June 2019, 18:21:10 UTC | oops; added todo tests back | 05 June 2019, 18:21:10 UTC |
| 8f3cf15 | Anish Tondwalkar | 01 June 2019, 21:50:02 UTC | fix tests/todo | 01 June 2019, 21:52:01 UTC |
| 6ef4dfd | Anish Tondwalkar | 30 May 2019, 21:18:11 UTC | Merge pull request #13 from ucsd-progsys/bidi bidirectional constraint generation | 30 May 2019, 21:18:11 UTC |
| 7290276 | Anish Tondwalkar | 30 May 2019, 21:17:05 UTC | make fixpoint a submodule | 30 May 2019, 21:17:05 UTC |
| cfb38bd | anish | 29 May 2019, 23:00:40 UTC | incrState actually increments | 29 May 2019, 23:00:40 UTC |
| 6aa997c | mkolosick | 29 May 2019, 22:01:11 UTC | Fixed more substitutions | 29 May 2019, 22:01:11 UTC |
| b2c12f7 | mkolosick | 29 May 2019, 21:49:24 UTC | Added pretty print script | 29 May 2019, 21:54:27 UTC |
| 59775fb | mkolosick | 29 May 2019, 21:49:24 UTC | Added pretty print script | 29 May 2019, 21:49:24 UTC |
| 7027c40 | mkolosick | 24 May 2019, 21:38:53 UTC | Removing subst1 forms | 29 May 2019, 21:47:38 UTC |
| 88ae0a1 | mkolosick | 24 May 2019, 21:35:59 UTC | Added constraint kinds simplification to CGen | 24 May 2019, 21:35:59 UTC |
| 92878ee | mkolosick | 21 May 2019, 21:41:49 UTC | Split incrState and incrState poly examples | 21 May 2019, 21:42:00 UTC |
| fd138ab | anish | 08 May 2019, 15:16:25 UTC | bump ghc using stack lts-12.15 gives us ghc-8.4.4, which is what sid is currently at (stack doesn't have aarch64 ghc installs) | 20 May 2019, 21:37:24 UTC |
| 3c35899 | anish | 08 May 2019, 15:16:25 UTC | bump ghc using stack lts-12.15 gives us ghc-8.4.4, which is what sid is currently at (stack doesn't have aarch64 ghc installs) | 08 May 2019, 15:16:25 UTC |
| a13171f | mkolosick | 07 May 2019, 16:18:53 UTC | Fixed pprint for RApp | 07 May 2019, 16:18:53 UTC |
| d3755a8 | Anish Tondwalkar | 03 May 2019, 17:33:09 UTC | Make example work: get >> get | 03 May 2019, 17:33:09 UTC |
| 39dc9b7 | Anish Tondwalkar | 30 April 2019, 17:16:17 UTC | Write CGen as bidirectional. Some caveats. This implementation works for non-implicits, but when you have implicit paramters, polymorphism, and ANF, the bidirectional approach doesn't quite work. You end up with something like ```haskell let anf0 :: SST Int Int Int = (>>) @Int @Int @Int in get >> get ``` The problem is that the implicit information simply travels up, not down! Seems the solution is to either not use bidi, or make fresh and <: allocate implicit paramters and solve for them. | 30 April 2019, 17:16:17 UTC |
| e491261 | Anish Tondwalkar | 30 April 2019, 08:23:04 UTC | Merge pull request #12 from ucsd-progsys/tycon Type Constructors | 30 April 2019, 08:23:04 UTC |
| 62681dd | Anish Tondwalkar | 30 April 2019, 08:01:52 UTC | bump fp | 30 April 2019, 08:01:52 UTC |
| a610328 | Anish Tondwalkar | 29 April 2019, 20:52:55 UTC | start: make cgen bidirectional again | 29 April 2019, 20:52:55 UTC |
| 40de375 | Anish Tondwalkar | 29 April 2019, 20:41:01 UTC | WIP : fix CGen to flatten RApp TODO: I don't think this is quite right... in general you may want to refine a type constructor. | 29 April 2019, 20:41:01 UTC |
| 97d88ca | Anish Tondwalkar | 28 April 2019, 00:31:11 UTC | fix crash, incrState:foTypes should mirror foBinds | 28 April 2019, 00:31:11 UTC |
| 309931f | Anish Tondwalkar | 26 April 2019, 17:43:22 UTC | add semantic whitespace to parser | 26 April 2019, 17:45:23 UTC |
| 34b1fa6 | Anish Tondwalkar | 24 April 2019, 14:26:48 UTC | Subtyping should respect variance | 26 April 2019, 17:45:23 UTC |
| 4d368ea | mkolosick | 25 April 2019, 21:40:32 UTC | Whitespace and new test | 25 April 2019, 21:40:32 UTC |
| 7b41627 | mkolosick | 23 April 2019, 20:32:59 UTC | Fixed incrState syntax | 23 April 2019, 20:32:59 UTC |
| da4119b | Anish Tondwalkar | 23 April 2019, 20:23:03 UTC | oops commited the wrong file | 23 April 2019, 20:23:03 UTC |
| 4460a0b | Anish Tondwalkar | 23 April 2019, 20:19:19 UTC | Cgen RApp <: RApp case | 23 April 2019, 20:19:19 UTC |
| 0411239 | Anish Tondwalkar | 23 April 2019, 20:16:49 UTC | Fixed error by squashing higher-order kvar params | 23 April 2019, 20:16:49 UTC |
| 8d56902 | Anish Tondwalkar | 23 April 2019, 19:42:02 UTC | Make grammar less strange We don't need to surround all applications in parentheses, just ones at the end of an expresssion (so that we can tell where an expression ends) | 23 April 2019, 20:06:01 UTC |
| 6eb06a3 | mkolosick | 23 April 2019, 20:01:00 UTC | Fixed annotation in synthesizeSpine | 23 April 2019, 20:01:00 UTC |
| d32554a | mkolosick | 23 April 2019, 20:00:19 UTC | Improved printing of type application | 23 April 2019, 20:00:19 UTC |
| 72b4dc7 | mkolosick | 23 April 2019, 20:00:07 UTC | Partially corrected temporary cgen error printing | 23 April 2019, 20:00:07 UTC |
| 41444b0 | Anish Tondwalkar | 23 April 2019, 16:07:29 UTC | Update testcases - pair now tests polymorphic function application (and fails in checker) - incrState no longer uses 0-ary get | 23 April 2019, 16:07:29 UTC |
| b35700f | Anish Tondwalkar | 15 April 2019, 18:17:30 UTC | fresh RType on CTor | 15 April 2019, 18:17:30 UTC |
| c470669 | Anish Tondwalkar | 15 April 2019, 06:12:15 UTC | Type's Ctor now keeps track of variances TODO: This commit also fucks the Ctor ToFixpoint, but I don't think that ever really worked right. We had a hack there involving TMap, but now we're just making them all TInt | 15 April 2019, 06:12:15 UTC |
| 4237f49 | Anish Tondwalkar | 12 April 2019, 16:12:03 UTC | Parser: Refactored RFun and RIFun into one parser | 12 April 2019, 16:12:03 UTC |
| c7b763d | Anish Tondwalkar | 12 April 2019, 04:12:30 UTC | Progress Towards Typechecking incrState | 12 April 2019, 04:12:30 UTC |
| ebcd665 | mkolosick | 10 April 2019, 21:38:23 UTC | Fixed incr00 test syntax | 10 April 2019, 21:38:23 UTC |
| c0a5ea6 | mkolosick | 10 April 2019, 21:25:33 UTC | Changed printing of errors in runMist | 10 April 2019, 21:38:03 UTC |
| 6c3602d | mkolosick | 10 April 2019, 20:58:43 UTC | Added single equal as other equality operator | 10 April 2019, 20:58:43 UTC |
| 195dd5b | mkolosick | 10 April 2019, 20:57:07 UTC | Fixed parse error | 10 April 2019, 20:57:07 UTC |
| adbba40 | Anish Tondwalkar | 10 April 2019, 20:24:07 UTC | Added tycon tests | 10 April 2019, 20:24:07 UTC |
| 9d3d6c6 | Anish Tondwalkar | 04 April 2019, 23:46:44 UTC | more parser tweaks | 04 April 2019, 23:46:44 UTC |
| 0070386 | Anish Tondwalkar | 04 April 2019, 23:11:54 UTC | Tweaked Expression Parser | 04 April 2019, 23:11:54 UTC |
| c11f653 | Anish Tondwalkar | 03 April 2019, 20:33:35 UTC | propogate assumes | 03 April 2019, 21:09:16 UTC |
| 4cd10cd | Anish Tondwalkar | 01 April 2019, 23:35:42 UTC | parse Ctor with variance | 01 April 2019, 23:35:42 UTC |
| d764f6e | Anish Tondwalkar | 01 April 2019, 23:19:13 UTC | Added RApp to RType This allows us to construct refinement types by applying a type constructor to arguments. | 01 April 2019, 23:19:13 UTC |
| 58a436c | Anish Tondwalkar | 28 March 2019, 22:42:05 UTC | Merge pull request #11 from ucsd-progsys/typed-anf Adding annotation points to every AST node | 28 March 2019, 22:42:05 UTC |
| f72ed27 | Anish Tondwalkar | 28 March 2019, 22:41:39 UTC | bump lf | 28 March 2019, 22:41:39 UTC |
| 2c6463f | mkolosick | 26 March 2019, 19:50:08 UTC | Annotating each node before ANF | 26 March 2019, 19:50:08 UTC |
| c565421 | mkolosick | 26 March 2019, 19:48:02 UTC | Moving to annotated expression forms | 26 March 2019, 19:49:13 UTC |
| 0546d63 | mkolosick | 22 March 2019, 01:01:19 UTC | Added type annotations to App and TApp | 22 March 2019, 01:01:19 UTC |
| 6ff8ddf | mkolosick | 21 March 2019, 23:27:37 UTC | Compiles with new Expr annotated forms | 21 March 2019, 23:27:37 UTC |
| e8eb56c | mkolosick | 15 March 2019, 20:57:43 UTC | Switched Prim2 to Prim apart from ANF | 18 March 2019, 18:30:01 UTC |
| 9ee6750 | mkolosick | 14 March 2019, 20:56:25 UTC | Correctly substituting for existentials in annotations | 14 March 2019, 20:56:25 UTC |
| 0c0da4d | Matthew Kolosick | 12 March 2019, 17:39:25 UTC | Merge pull request #10 from ucsd-progsys/implicits Implicits | 12 March 2019, 17:39:25 UTC |
| 385d693 | Matthew Kolosick | 12 March 2019, 17:39:13 UTC | Merge pull request #9 from ucsd-progsys/liquid-cgen Liquid cgen | 12 March 2019, 17:39:13 UTC |
| 20b2c74 | Anish Tondwalkar | 24 February 2019, 23:54:29 UTC | implement implicits | 08 March 2019, 19:25:34 UTC |
| 80d7162 | Anish Tondwalkar | 24 February 2019, 09:44:41 UTC | added testcase that breaks checker | 24 February 2019, 09:44:41 UTC |
| 1157f0d | Anish Tondwalkar | 24 February 2019, 09:42:24 UTC | tests pass | 24 February 2019, 09:42:24 UTC |
| bfa9b26 | Anish Tondwalkar | 22 February 2019, 20:48:41 UTC | cgen: fresh (Gamma) and subst bug | 22 February 2019, 20:50:27 UTC |
| efd594f | mkolosick | 22 February 2019, 07:00:21 UTC | Added initial unit test for CGen | 22 February 2019, 07:00:21 UTC |
| 1aebb7e | mkolosick | 22 February 2019, 02:10:34 UTC | Left todo for normalizer | 22 February 2019, 02:10:34 UTC |
| 7073357 | mkolosick | 21 February 2019, 19:08:02 UTC | Testing new cgen for lets | 21 February 2019, 19:08:02 UTC |
| 1543ace | mkolosick | 21 February 2019, 18:57:30 UTC | Fixed bug in collecting kvars | 21 February 2019, 18:57:30 UTC |
| 83aafe7 | mkolosick | 20 February 2019, 18:56:58 UTC | Surfacing solver result in mist runner | 20 February 2019, 18:56:58 UTC |
| 69f4a4a | mkolosick | 20 February 2019, 00:03:41 UTC | Adding refinement checker failing test | 20 February 2019, 00:03:41 UTC |
| 4a1013f | mkolosick | 20 February 2019, 00:00:43 UTC | All fixpoint tests not relying on If pass | 20 February 2019, 00:00:43 UTC |
| 144445d | mkolosick | 19 February 2019, 23:36:22 UTC | Collected kvars | 19 February 2019, 23:36:22 UTC |
| 4a0a6b4 | mkolosick | 19 February 2019, 23:00:19 UTC | Fixed and integrated uniquify | 19 February 2019, 23:00:19 UTC |
| d4fea5e | mkolosick | 19 February 2019, 22:12:38 UTC | WIP on CGen | 19 February 2019, 22:22:10 UTC |
| 539139b | mkolosick | 31 January 2019, 20:10:57 UTC | Work in progress (failing tests) | 09 February 2019, 01:01:15 UTC |
| 5faaa2d | Anish Tondwalkar | 29 January 2019, 08:44:31 UTC | Run the whole pipeline bit of gore, but tests pass! | 29 January 2019, 08:44:31 UTC |
| e38a637 | Anish Tondwalkar | 29 January 2019, 08:27:49 UTC | insert KVars | 29 January 2019, 08:27:49 UTC |
| e76f4e1 | Anish Tondwalkar | 29 January 2019, 02:33:11 UTC | start rewrite of CGen | 29 January 2019, 02:39:55 UTC |
| 3e97fc9 | Anish Tondwalkar | 29 January 2019, 02:34:52 UTC | Merge pull request #8 from ucsd-progsys/elaboration Elaboration | 29 January 2019, 02:34:52 UTC |
| 58e8e5f | mkolosick | 26 January 2019, 03:54:44 UTC | Added todo for RUnrefined cases | 26 January 2019, 03:54:44 UTC |
| 608a273 | mkolosick | 26 January 2019, 03:47:27 UTC | Hooked elaboration into the running of Mist | 26 January 2019, 03:52:40 UTC |
| 28aaacd | mkolosick | 26 January 2019, 03:46:53 UTC | Fixed bug in mkArrow | 26 January 2019, 03:52:40 UTC |
| e382a04 | Anish Tondwalkar | 25 January 2019, 09:21:35 UTC | edits to documentation for RUnrefined | 26 January 2019, 03:52:40 UTC |
| 0375ea3 | mkolosick | 24 January 2019, 20:11:35 UTC | Added test of let generalization of non recursive lambda | 26 January 2019, 03:52:40 UTC |
| dbe6509 | mkolosick | 24 January 2019, 19:50:03 UTC | Added test to ensure correct ordering of multiple type applications | 26 January 2019, 03:52:40 UTC |
| a2ec697 | mkolosick | 24 January 2019, 19:40:00 UTC | Fixed bug with splitEnv and added type instantiation | 26 January 2019, 03:52:40 UTC |
| 0cb78fa | mkolosick | 24 January 2019, 19:38:33 UTC | Added type checker debugging scaffolding | 26 January 2019, 03:52:40 UTC |
| 84cbb77 | mkolosick | 26 January 2019, 03:52:40 UTC | Added RUnrefined | 26 January 2019, 03:52:40 UTC |
| 505df6f | mkolosick | 19 January 2019, 00:43:09 UTC | Initial tests hitting failing elaboration and need to insert kvars. | 26 January 2019, 03:52:09 UTC |
| 6e5942f | mkolosick | 17 January 2019, 20:35:11 UTC | Initial type checker tests and fixed a bug with lambdas | 26 January 2019, 03:52:09 UTC |
| e888165 | mkolosick | 26 January 2019, 03:52:09 UTC | Initial implementation of elaboration | 26 January 2019, 03:52:09 UTC |
| 6068299 | Anish Tondwalkar | 25 January 2019, 08:52:18 UTC | clean up interface to ToFixpoint | 25 January 2019, 08:52:18 UTC |
| d4bbb71 | Anish Tondwalkar | 24 January 2019, 02:08:03 UTC | Translate subC to FP Horn | 24 January 2019, 02:11:27 UTC |
| 0c5cf19 | Matthew Kolosick | 15 January 2019, 21:15:01 UTC | Merge pull request #7 from ucsd-progsys/currify Merge type schemes into types and currify functions and type abstractions | 15 January 2019, 21:15:01 UTC |
| 04fe8a9 | Ranjit Jhala | 11 January 2019, 22:29:42 UTC | testS | 11 January 2019, 22:29:42 UTC |
| b8f15d2 | Anish Tondwalkar | 09 January 2019, 08:32:07 UTC | checked in doctests for CGen.synth | 09 January 2019, 08:32:07 UTC |
