| 7eaf80d | Anish Tondwalkar | 20 July 2019, 22:24:09 UTC | Fixed fixpoint scoping bug next: cryptic Checker error | 20 July 2019, 22:24:09 UTC |
| 47d4396 | Anish Tondwalkar | 19 July 2019, 23:03:18 UTC | added TODOs | 19 July 2019, 23:03:18 UTC |
| 0a83b72 | Anish Tondwalkar | 19 July 2019, 22:59:50 UTC | Parse nested RApp | 19 July 2019, 22:59:50 UTC |
| e395635 | Anish Tondwalkar | 19 July 2019, 22:53:06 UTC | Clean up type signatures | 19 July 2019, 22:53:06 UTC |
| 257b123 | Anish Tondwalkar | 19 July 2019, 22:42:30 UTC | fix mistake in shillset | 19 July 2019, 22:42:30 UTC |
| e964cb4 | Anish Tondwalkar | 19 July 2019, 22:34:24 UTC | Added subset prim next: parse nested RApp? | 19 July 2019, 22:40:17 UTC |
| 124be31 | Anish Tondwalkar | 19 July 2019, 21:36:32 UTC | add shillSet example Let's try and make the shill example from the BRTs paper work. I'm going to start with a set for each capability and see if we can get that to work before I add a map of sets to keep them together. After we get this example working, we should get RJ's state example working before we mapify everything. | 19 July 2019, 21:53:58 UTC |
| 6911d0e | Anish Tondwalkar | 19 July 2019, 21:30:50 UTC | renamed examples from the paper filenames should be more meaningful now | 19 July 2019, 21:30:50 UTC |
| 588b557 | Anish Tondwalkar | 19 July 2019, 00:53:01 UTC | Update revoke test | 19 July 2019, 00:53:01 UTC |
| 9891638 | Anish Tondwalkar | 18 July 2019, 23:21:41 UTC | deadline commit | 18 July 2019, 23:21:41 UTC |
| 84316f0 | Anish Tondwalkar | 10 July 2019, 21:22:00 UTC | Fixed typo in revoke example | 10 July 2019, 21:23:27 UTC |
| 3eb6028 | mkolosick | 10 July 2019, 20:31:40 UTC | Debugging changes | 10 July 2019, 20:31:40 UTC |
| e5ba0f4 | Anish Tondwalkar | 10 July 2019, 18:23:38 UTC | Fix CGen.<: for tick | 10 July 2019, 18:24:01 UTC |
| 7b4b829 | Anish Tondwalkar | 10 July 2019, 09:06:56 UTC | Fix RRTy in CGen; bump fp | 10 July 2019, 09:06:56 UTC |
| 9c14620 | mkolosick | 10 July 2019, 08:25:38 UTC | new tests | 10 July 2019, 08:25:38 UTC |
| d4c2c4d | mkolosick | 10 July 2019, 06:55:12 UTC | Fixing mkAll and mkExists | 10 July 2019, 06:55:12 UTC |
| a60d2f9 | mkolosick | 10 July 2019, 06:30:18 UTC | Fixing mkAll | 10 July 2019, 06:30:18 UTC |
| 7e87b34 | Anish Tondwalkar | 10 July 2019, 02:00:04 UTC | Fix more Sort problems with revoke now runs through, but returns unsafe | 10 July 2019, 02:00:04 UTC |
| 729c6f4 | Anish Tondwalkar | 10 July 2019, 00:21:43 UTC | Split quantifiers into rforall and forall rforall quantifies over an RType a la Cosman forall quantifies only over a base Type | 10 July 2019, 00:21:43 UTC |
| 78b795a | Anish Tondwalkar | 09 July 2019, 22:26:36 UTC | quantifers are now base if used at an implicit | 09 July 2019, 22:26:36 UTC |
| 5372728 | mkolosick | 09 July 2019, 21:50:13 UTC | No more refinement polymorphism | 09 July 2019, 22:15:23 UTC |
| ffbaca0 | mkolosick | 09 July 2019, 20:27:01 UTC | Updating tests | 09 July 2019, 20:27:01 UTC |
| 9f79c7b | mkolosick | 09 July 2019, 20:26:53 UTC | Pruning in pretty-printer | 09 July 2019, 20:26:53 UTC |
| 16967d0 | mkolosick | 09 July 2019, 18:06:01 UTC | Recursive and strengthening | 09 July 2019, 18:06:01 UTC |
| 5943edc | mkolosick | 09 July 2019, 18:03:15 UTC | Recursion without strengthening | 09 July 2019, 18:03:15 UTC |
| 5d46b87 | Anish Tondwalkar | 08 July 2019, 21:02:16 UTC | revoke now generates well-sorted constraints | 08 July 2019, 21:02:16 UTC |
| 485358c | Anish Tondwalkar | 08 July 2019, 18:09:08 UTC | Reduce the number of kvars generated | 08 July 2019, 18:09:08 UTC |
| f0d849d | Anish Tondwalkar | 08 July 2019, 04:45:49 UTC | Fixed sorts | 08 July 2019, 04:45:49 UTC |
| 19d4c14 | Anish Tondwalkar | 04 July 2019, 00:00:57 UTC | Added set prims and wrote revoke example in mist | 08 July 2019, 04:40:00 UTC |
| 6369b84 | Anish Tondwalkar | 06 July 2019, 08:25:08 UTC | added Set type for grant/revoke | 08 July 2019, 04:37:23 UTC |
| cb6719d | mkolosick | 07 July 2019, 06:27:55 UTC | Redid revoke and made linear types a full checker | 07 July 2019, 06:27:55 UTC |
| f5813c8 | mkolosick | 06 July 2019, 17:52:01 UTC | New tests | 06 July 2019, 17:52:01 UTC |
| bf7edfe | mkolosick | 06 July 2019, 00:40:25 UTC | Updating how RRTy and RApp are treated. RRTypes get flattened down as much as they can. RApp is parsed in similarly to parsing an unrefined base type, that is as an RRTy with refinement True of an RApp. | 06 July 2019, 07:05:04 UTC |
| d88274d | mkolosick | 05 July 2019, 22:08:48 UTC | Uninterpreted functions | 05 July 2019, 22:08:48 UTC |
| 150ed33 | Anish Tondwalkar | 04 July 2019, 22:24:45 UTC | remove flattenRType | 04 July 2019, 23:15:18 UTC |
| 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 |
