314ec0f | mkolosick | 23 November 2019, 01:43:04 UTC | app-succ and app-succ0 | 23 November 2019, 01:43:04 UTC |
340b80e | mkolosick | 23 November 2019, 01:29:11 UTC | app-succ and repeat | 23 November 2019, 01:29:11 UTC |
f6db5fa | mkolosick | 22 November 2019, 01:57:45 UTC | Repeat is back | 22 November 2019, 01:57:45 UTC |
242582c | mkolosick | 22 November 2019, 01:44:02 UTC | mochi-d2 | 22 November 2019, 01:44:25 UTC |
bea7946 | mkolosick | 22 November 2019, 01:36:31 UTC | Move mochi d2 to neg | 22 November 2019, 01:44:25 UTC |
347be3b | Anish Tondwalkar | 22 November 2019, 01:36:28 UTC | added mochi tests | 22 November 2019, 01:36:28 UTC |
80cebdd | mkolosick | 20 November 2019, 05:47:01 UTC | Tick tick doesn't work | 20 November 2019, 05:47:01 UTC |
6f5b475 | mkolosick | 20 November 2019, 05:37:09 UTC | Omega isn't loop | 20 November 2019, 05:37:09 UTC |
093ff88 | mkolosick | 20 November 2019, 05:34:36 UTC | Tick tock 3: some real ticks and tocks | 20 November 2019, 05:34:36 UTC |
942eb2f | mkolosick | 20 November 2019, 03:19:40 UTC | Minor changes | 20 November 2019, 03:19:40 UTC |
0545284 | Anish Tondwalkar | 20 November 2019, 03:18:38 UTC | add some of the tests from mochi | 20 November 2019, 03:18:38 UTC |
68d3acd | mkolosick | 19 November 2019, 07:26:18 UTC | Actual unbounded loop: DOES NOT WORK YET | 19 November 2019, 07:26:18 UTC |
2836ad7 | mkolosick | 19 November 2019, 05:36:34 UTC | Removed printing | 19 November 2019, 05:36:34 UTC |
9a417f5 | mkolosick | 19 November 2019, 01:47:25 UTC | Full looping for | 19 November 2019, 01:47:25 UTC |
91f9eff | mkolosick | 19 November 2019, 00:35:44 UTC | Automatically unpacking sigmas | 19 November 2019, 00:35:44 UTC |
0d76623 | Anish Tondwalkar | 18 November 2019, 21:46:22 UTC | Wrote sigma-elaborator | 18 November 2019, 21:46:22 UTC |
fb48833 | Anish Tondwalkar | 18 November 2019, 21:45:54 UTC | cleanup and hygiene | 18 November 2019, 21:45:54 UTC |
09636e9 | mkolosick | 18 November 2019, 05:41:12 UTC | Initial ANF sigma work | 18 November 2019, 05:41:12 UTC |
19db75a | mkolosick | 16 November 2019, 08:40:55 UTC | Fixed polymorphism bug | 16 November 2019, 08:50:42 UTC |
4350cd5 | mkolosick | 16 November 2019, 07:00:22 UTC | Switched to sigmas on some examples | 16 November 2019, 07:00:22 UTC |
7886cde | mkolosick | 16 November 2019, 06:24:57 UTC | Fixed freshRType bug | 16 November 2019, 06:24:57 UTC |
49bb9d0 | mkolosick | 13 November 2019, 19:53:32 UTC | Added RIFun to freshRType | 13 November 2019, 19:56:36 UTC |
5c0120a | mkolosick | 11 November 2019, 17:54:16 UTC | Pagination with tokens | 13 November 2019, 19:56:36 UTC |
301208f | mkolosick | 11 November 2019, 06:30:06 UTC | More interesting forSigma test | 13 November 2019, 19:56:36 UTC |
0b071dc | mkolosick | 11 November 2019, 06:13:23 UTC | Added implicit sigma types. Test and usage are in pos/forSigma.hs | 13 November 2019, 19:56:36 UTC |
ca8def0 | mkolosick | 09 November 2019, 04:42:49 UTC | Removed unneeded implicits | 13 November 2019, 19:56:36 UTC |
e0df534 | mkolosick | 09 November 2019, 04:11:29 UTC | Fixed typo in forSigma | 13 November 2019, 19:56:36 UTC |
3063e0e | mkolosick | 09 November 2019, 01:27:07 UTC | WIP on forSigma | 13 November 2019, 19:56:36 UTC |
66181ea | Anish Tondwalkar | 09 November 2019, 01:07:19 UTC | Support for Higher-Rank Types you need double parens (see hrts.hs) | 13 November 2019, 19:56:36 UTC |
12b8e31 | mkolosick | 09 November 2019, 00:04:13 UTC | Pagination tokens | 13 November 2019, 19:56:36 UTC |
f791d87 | mkolosick | 08 November 2019, 00:40:29 UTC | Removing ANF | 13 November 2019, 19:56:36 UTC |
dca1c45 | mkolosick | 06 November 2019, 23:14:02 UTC | Commit before disabling ANF | 13 November 2019, 19:56:36 UTC |
ecf9dd9 | mkolosick | 05 November 2019, 01:07:29 UTC | Removed strengthening | 13 November 2019, 19:56:36 UTC |
d6c8677 | Anish Tondwalkar | 08 November 2019, 23:20:16 UTC | Add partial pagination3 | 08 November 2019, 23:20:40 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 |