| b39be83 | mkolosick | 13 November 2019, 19:53:32 UTC | Added RIFun to freshRType | 13 November 2019, 19:53:32 UTC |
| 4769704 | mkolosick | 11 November 2019, 17:54:16 UTC | Pagination with tokens | 11 November 2019, 17:54:16 UTC |
| cf8ef66 | mkolosick | 11 November 2019, 06:30:06 UTC | More interesting forSigma test | 11 November 2019, 06:30:06 UTC |
| b49f5df | mkolosick | 11 November 2019, 06:13:23 UTC | Added implicit sigma types. Test and usage are in pos/forSigma.hs | 11 November 2019, 06:13:23 UTC |
| e61ad1f | mkolosick | 09 November 2019, 04:42:49 UTC | Removed unneeded implicits | 09 November 2019, 04:42:49 UTC |
| 08d0b00 | mkolosick | 09 November 2019, 04:11:29 UTC | Fixed typo in forSigma | 09 November 2019, 04:11:29 UTC |
| 0d63594 | mkolosick | 09 November 2019, 01:27:07 UTC | WIP on forSigma | 09 November 2019, 01:27:07 UTC |
| 1b5d6ba | Anish Tondwalkar | 09 November 2019, 01:07:19 UTC | Support for Higher-Rank Types you need double parens (see hrts.hs) | 09 November 2019, 01:07:33 UTC |
| 739d4a2 | mkolosick | 09 November 2019, 00:04:13 UTC | Pagination tokens | 09 November 2019, 00:04:13 UTC |
| a48dc6a | mkolosick | 08 November 2019, 00:40:29 UTC | Removing ANF | 08 November 2019, 00:40:29 UTC |
| 5b56304 | mkolosick | 06 November 2019, 23:14:02 UTC | Commit before disabling ANF | 06 November 2019, 23:14:02 UTC |
| 0f1485f | mkolosick | 05 November 2019, 01:07:29 UTC | Removed strengthening | 05 November 2019, 01:07:29 UTC |
| b52fffe | mkolosick | 01 November 2019, 18:17:40 UTC | Updated pure in tests | 01 November 2019, 18:17:40 UTC |
| 883df18 | mkolosick | 29 October 2019, 22:35:08 UTC | CPS script | 29 October 2019, 22:35:08 UTC |
| 082f610 | mkolosick | 22 October 2019, 21:56:49 UTC | Refixed parser | 22 October 2019, 21:56:49 UTC |
| a90a8af | mkolosick | 21 October 2019, 18:24:24 UTC | More tests | 22 October 2019, 21:46:04 UTC |
| f59c0b0 | mkolosick | 21 October 2019, 18:23:13 UTC | Merge commit of some sort | 22 October 2019, 21:46:04 UTC |
| e7cedf6 | mkolosick | 21 October 2019, 17:47:01 UTC | shillSet experiments | 22 October 2019, 21:46:04 UTC |
| 5f94d69 | Anish Tondwalkar | 21 October 2019, 18:07:18 UTC | added TCP client example | 21 October 2019, 18:07:18 UTC |
| f9d43a2 | Anish Tondwalkar | 20 October 2019, 05:17:02 UTC | run tests with setVerbosity Quiet | 20 October 2019, 06:22:20 UTC |
| 23ef471 | Anish Tondwalkar | 18 October 2019, 19:01:34 UTC | Update to ticktock3 Add send/recv channels and prove that unreachable states are unreachable | 18 October 2019, 19:01:34 UTC |
| c56ef6c | Anish Tondwalkar | 17 October 2019, 21:33:07 UTC | Added twoPhaseCommit | 17 October 2019, 21:33:07 UTC |
| ce240b3 | Anish Tondwalkar | 17 October 2019, 02:31:05 UTC | added ticktock and pagination | 17 October 2019, 02:31:23 UTC |
| f1d86f3 | Anish Tondwalkar | 17 October 2019, 00:20:03 UTC | Read verbosity from command line instead of statically specifying it | 17 October 2019, 02:31:23 UTC |
| 3050d85 | mkolosick | 14 October 2019, 18:56:59 UTC | Added or and implication | 14 October 2019, 18:56:59 UTC |
| a139996 | Anish Tondwalkar | 11 October 2019, 00:38:30 UTC | idr_login finally works! | 11 October 2019, 00:38:30 UTC |
| 5570953 | Anish Tondwalkar | 20 September 2019, 20:16:26 UTC | edits to idr_login | 20 September 2019, 20:16:26 UTC |
| 6aae376 | mkolosick | 12 September 2019, 21:34:45 UTC | Added implicit lambda term former | 12 September 2019, 21:35:20 UTC |
| 8ca0371 | Anish Tondwalkar | 12 September 2019, 20:30:00 UTC | More work on idr examples - login example runs into strange bug in Checker articulation - intro example works, but need to make all types to Int to make FP happy | 12 September 2019, 20:30:00 UTC |
| 5c17971 | Anish Tondwalkar | 10 September 2019, 18:29:33 UTC | Added test for renamer bug implicit args are in scope in the body in cgen, which is correct, but not in the renamer | 10 September 2019, 18:29:33 UTC |
| 6787ad4 | Anish Tondwalkar | 10 September 2019, 06:58:30 UTC | First go at some real error messages Currently we print the bare refinement post-uniqify and freshening, but without the kvar sols having been applied, so that could definitely be improved upon | 10 September 2019, 06:58:30 UTC |
| cd20f0c | mkolosick | 09 September 2019, 21:24:19 UTC | Fixed for.hs todo test. Needed to pull loop invariant into constraint on implicit parameter of callback. | 09 September 2019, 21:24:19 UTC |
| 1a405c6 | Anish Tondwalkar | 09 September 2019, 20:12:25 UTC | Added todo/for case with refinement on iter index | 09 September 2019, 20:12:25 UTC |
| 9d7c337 | mkolosick | 29 August 2019, 18:36:54 UTC | - Fixed subtyping for constructors in Checker. - Made existential instantiation more robust. | 29 August 2019, 18:36:54 UTC |
| c9b4d70 | mkolosick | 26 August 2019, 22:42:02 UTC | Fixed set annotations in shillSet | 26 August 2019, 22:42:02 UTC |
| 5ea1864 | mkolosick | 26 August 2019, 20:40:22 UTC | Fixed parsing of annotated lets and added negative test | 26 August 2019, 20:40:22 UTC |
| ad522c2 | Anish Tondwalkar | 21 August 2019, 03:39:42 UTC | Annotated let binders | 21 August 2019, 03:43:02 UTC |
| 22dbb0e | Anish Tondwalkar | 21 August 2019, 01:06:17 UTC | correctly serialize type constructors to FP | 21 August 2019, 01:06:17 UTC |
| 579b1dc | Anish Tondwalkar | 19 August 2019, 09:38:42 UTC | Better parse errors | 19 August 2019, 09:38:42 UTC |
| a62e4b2 | Anish Tondwalkar | 19 August 2019, 08:45:23 UTC | Update to lts-14.0 includes megaparsec 6 -> 7 migration, which changes the API for error messages and source positions also update fixpoint to to be on same lts | 19 August 2019, 08:45:23 UTC |
| 71eb919 | mkolosick | 15 August 2019, 23:20:00 UTC | Better formatted error messages from solver failures | 15 August 2019, 23:20:00 UTC |
| b681213 | mkolosick | 15 August 2019, 23:08:18 UTC | Fixed printf format string | 15 August 2019, 23:08:18 UTC |
| c3df68d | mkolosick | 15 August 2019, 23:03:10 UTC | Fixed Set bug | 15 August 2019, 23:03:10 UTC |
| 68df304 | Anish Tondwalkar | 15 August 2019, 22:42:01 UTC | refactored SSParsedExpr | 15 August 2019, 22:46:36 UTC |
| 95861d2 | Anish Tondwalkar | 15 August 2019, 17:59:20 UTC | SSParsedExpr is now recursive This recursion should probably be done at the ParsedExpr level, but that's an involved refactoring | 15 August 2019, 22:45:56 UTC |
| 9d2a590 | mkolosick | 15 August 2019, 22:40:46 UTC | Fixed test framework to use new config object | 15 August 2019, 22:40:46 UTC |
| 065c068 | mkolosick | 15 August 2019, 22:33:50 UTC | Added read option to mist | 15 August 2019, 22:33:50 UTC |
| 7069a8e | Anish Tondwalkar | 07 August 2019, 18:51:37 UTC | start work on idris login example | 07 August 2019, 18:51:37 UTC |
| ea1aad5 | Anish Tondwalkar | 04 August 2019, 05:52:42 UTC | cleanup pointers example | 04 August 2019, 05:52:42 UTC |
| 97f6408 | Anish Tondwalkar | 04 August 2019, 05:31:33 UTC | fix bug with implicits after forall | 04 August 2019, 05:52:10 UTC |
| 0c3f096 | Anish Tondwalkar | 04 August 2019, 05:30:22 UTC | oops | 04 August 2019, 05:30:22 UTC |
| e2b69aa | Anish Tondwalkar | 02 August 2019, 18:44:06 UTC | unit in pointers_noalias.hs | 02 August 2019, 18:44:06 UTC |
| 4d122d5 | Anish Tondwalkar | 02 August 2019, 18:11:54 UTC | Make pattern matcher timeout go away in ToFixpoint | 02 August 2019, 18:11:54 UTC |
| ff589c2 | Anish Tondwalkar | 02 August 2019, 17:58:48 UTC | Add unit Type | 02 August 2019, 17:58:48 UTC |
| 088d2fc | Anish Tondwalkar | 02 August 2019, 17:49:19 UTC | Improve debugging output from CGen.hs | 02 August 2019, 17:49:19 UTC |
| 82249de | Anish Tondwalkar | 02 August 2019, 07:44:51 UTC | Fix equal primOp | 02 August 2019, 07:44:51 UTC |
| 72aa198 | Anish Tondwalkar | 01 August 2019, 07:53:00 UTC | isolated tabs/ifun bug and split into own test The problem is that when we have an ~> under an forall, at the term level we have a tabs, and that means we have to swtich from checking (at the type with the implicit parameter) to synthing (plus a subtyping check). But when we synth, this implicit parameter is simply not in scope: since it's not bound anywhere in the term, it can't be added to the context during synthesis. | 01 August 2019, 07:53:00 UTC |
| 95a7cd4 | Anish Tondwalkar | 30 July 2019, 18:46:43 UTC | progress on state example: isolated bug some strage interaction between forall and implicits this causes forall a. h ~> n -> ... to get scoped as ``` forall n ... /\ forall h ... ``` instead of ``` forall n ... forall h .... ``` | 30 July 2019, 18:46:43 UTC |
| 0dc1fc4 | Anish Tondwalkar | 30 July 2019, 18:40:47 UTC | Mixed up forall and rforall in CGen | 30 July 2019, 18:40:47 UTC |
| 3936ebc | Anish Tondwalkar | 29 July 2019, 15:15:06 UTC | add subtyping rule fox right-hand implicits | 29 July 2019, 15:15:06 UTC |
| 4c79ff0 | Anish Tondwalkar | 29 July 2019, 05:25:06 UTC | implement decr in pointers example. start init[ but seems there's a checker bug blocking init | 29 July 2019, 05:25:06 UTC |
| bb8b279 | Anish Tondwalkar | 29 July 2019, 04:54:52 UTC | added store primitive | 29 July 2019, 04:54:52 UTC |
| 60787e2 | Anish Tondwalkar | 26 July 2019, 07:16:05 UTC | added map store | 28 July 2019, 22:30:41 UTC |
| 035e56a | Anish Tondwalkar | 24 July 2019, 11:40:18 UTC | Set is a Ctor | 24 July 2019, 11:45:36 UTC |
| d70ff51 | Anish Tondwalkar | 22 July 2019, 23:55:09 UTC | split off todo/for.hs from shill | 22 July 2019, 23:55:09 UTC |
| 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 |
