We are hiring ! See our job offers.
swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6

sort by:
Revision Author Date Message Commit Date
b39be83 Added RIFun to freshRType 13 November 2019, 19:53:32 UTC
4769704 Pagination with tokens 11 November 2019, 17:54:16 UTC
cf8ef66 More interesting forSigma test 11 November 2019, 06:30:06 UTC
b49f5df Added implicit sigma types. Test and usage are in pos/forSigma.hs 11 November 2019, 06:13:23 UTC
e61ad1f Removed unneeded implicits 09 November 2019, 04:42:49 UTC
08d0b00 Fixed typo in forSigma 09 November 2019, 04:11:29 UTC
0d63594 WIP on forSigma 09 November 2019, 01:27:07 UTC
1b5d6ba Support for Higher-Rank Types you need double parens (see hrts.hs) 09 November 2019, 01:07:33 UTC
739d4a2 Pagination tokens 09 November 2019, 00:04:13 UTC
a48dc6a Removing ANF 08 November 2019, 00:40:29 UTC
5b56304 Commit before disabling ANF 06 November 2019, 23:14:02 UTC
0f1485f Removed strengthening 05 November 2019, 01:07:29 UTC
b52fffe Updated pure in tests 01 November 2019, 18:17:40 UTC
883df18 CPS script 29 October 2019, 22:35:08 UTC
082f610 Refixed parser 22 October 2019, 21:56:49 UTC
a90a8af More tests 22 October 2019, 21:46:04 UTC
f59c0b0 Merge commit of some sort 22 October 2019, 21:46:04 UTC
e7cedf6 shillSet experiments 22 October 2019, 21:46:04 UTC
5f94d69 added TCP client example 21 October 2019, 18:07:18 UTC
f9d43a2 run tests with setVerbosity Quiet 20 October 2019, 06:22:20 UTC
23ef471 Update to ticktock3 Add send/recv channels and prove that unreachable states are unreachable 18 October 2019, 19:01:34 UTC
c56ef6c Added twoPhaseCommit 17 October 2019, 21:33:07 UTC
ce240b3 added ticktock and pagination 17 October 2019, 02:31:23 UTC
f1d86f3 Read verbosity from command line instead of statically specifying it 17 October 2019, 02:31:23 UTC
3050d85 Added or and implication 14 October 2019, 18:56:59 UTC
a139996 idr_login finally works! 11 October 2019, 00:38:30 UTC
5570953 edits to idr_login 20 September 2019, 20:16:26 UTC
6aae376 Added implicit lambda term former 12 September 2019, 21:35:20 UTC
8ca0371 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 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 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 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 Added todo/for case with refinement on iter index 09 September 2019, 20:12:25 UTC
9d7c337 - Fixed subtyping for constructors in Checker. - Made existential instantiation more robust. 29 August 2019, 18:36:54 UTC
c9b4d70 Fixed set annotations in shillSet 26 August 2019, 22:42:02 UTC
5ea1864 Fixed parsing of annotated lets and added negative test 26 August 2019, 20:40:22 UTC
ad522c2 Annotated let binders 21 August 2019, 03:43:02 UTC
22dbb0e correctly serialize type constructors to FP 21 August 2019, 01:06:17 UTC
579b1dc Better parse errors 19 August 2019, 09:38:42 UTC
a62e4b2 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 Better formatted error messages from solver failures 15 August 2019, 23:20:00 UTC
b681213 Fixed printf format string 15 August 2019, 23:08:18 UTC
c3df68d Fixed Set bug 15 August 2019, 23:03:10 UTC
68df304 refactored SSParsedExpr 15 August 2019, 22:46:36 UTC
95861d2 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 Fixed test framework to use new config object 15 August 2019, 22:40:46 UTC
065c068 Added read option to mist 15 August 2019, 22:33:50 UTC
7069a8e start work on idris login example 07 August 2019, 18:51:37 UTC
ea1aad5 cleanup pointers example 04 August 2019, 05:52:42 UTC
97f6408 fix bug with implicits after forall 04 August 2019, 05:52:10 UTC
0c3f096 oops 04 August 2019, 05:30:22 UTC
e2b69aa unit in pointers_noalias.hs 02 August 2019, 18:44:06 UTC
4d122d5 Make pattern matcher timeout go away in ToFixpoint 02 August 2019, 18:11:54 UTC
ff589c2 Add unit Type 02 August 2019, 17:58:48 UTC
088d2fc Improve debugging output from CGen.hs 02 August 2019, 17:49:19 UTC
82249de Fix equal primOp 02 August 2019, 07:44:51 UTC
72aa198 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 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 Mixed up forall and rforall in CGen 30 July 2019, 18:40:47 UTC
3936ebc add subtyping rule fox right-hand implicits 29 July 2019, 15:15:06 UTC
4c79ff0 implement decr in pointers example. start init[ but seems there's a checker bug blocking init 29 July 2019, 05:25:06 UTC
bb8b279 added store primitive 29 July 2019, 04:54:52 UTC
60787e2 added map store 28 July 2019, 22:30:41 UTC
035e56a Set is a Ctor 24 July 2019, 11:45:36 UTC
d70ff51 split off todo/for.hs from shill 22 July 2019, 23:55:09 UTC
7eaf80d Fixed fixpoint scoping bug next: cryptic Checker error 20 July 2019, 22:24:09 UTC
47d4396 added TODOs 19 July 2019, 23:03:18 UTC
0a83b72 Parse nested RApp 19 July 2019, 22:59:50 UTC
e395635 Clean up type signatures 19 July 2019, 22:53:06 UTC
257b123 fix mistake in shillset 19 July 2019, 22:42:30 UTC
e964cb4 Added subset prim next: parse nested RApp? 19 July 2019, 22:40:17 UTC
124be31 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 renamed examples from the paper filenames should be more meaningful now 19 July 2019, 21:30:50 UTC
588b557 Update revoke test 19 July 2019, 00:53:01 UTC
9891638 deadline commit 18 July 2019, 23:21:41 UTC
84316f0 Fixed typo in revoke example 10 July 2019, 21:23:27 UTC
3eb6028 Debugging changes 10 July 2019, 20:31:40 UTC
e5ba0f4 Fix CGen.<: for tick 10 July 2019, 18:24:01 UTC
7b4b829 Fix RRTy in CGen; bump fp 10 July 2019, 09:06:56 UTC
9c14620 new tests 10 July 2019, 08:25:38 UTC
d4c2c4d Fixing mkAll and mkExists 10 July 2019, 06:55:12 UTC
a60d2f9 Fixing mkAll 10 July 2019, 06:30:18 UTC
7e87b34 Fix more Sort problems with revoke now runs through, but returns unsafe 10 July 2019, 02:00:04 UTC
729c6f4 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 quantifers are now base if used at an implicit 09 July 2019, 22:26:36 UTC
5372728 No more refinement polymorphism 09 July 2019, 22:15:23 UTC
ffbaca0 Updating tests 09 July 2019, 20:27:01 UTC
9f79c7b Pruning in pretty-printer 09 July 2019, 20:26:53 UTC
16967d0 Recursive and strengthening 09 July 2019, 18:06:01 UTC
5943edc Recursion without strengthening 09 July 2019, 18:03:15 UTC
5d46b87 revoke now generates well-sorted constraints 08 July 2019, 21:02:16 UTC
485358c Reduce the number of kvars generated 08 July 2019, 18:09:08 UTC
f0d849d Fixed sorts 08 July 2019, 04:45:49 UTC
19d4c14 Added set prims and wrote revoke example in mist 08 July 2019, 04:40:00 UTC
6369b84 added Set type for grant/revoke 08 July 2019, 04:37:23 UTC
cb6719d Redid revoke and made linear types a full checker 07 July 2019, 06:27:55 UTC
f5813c8 New tests 06 July 2019, 17:52:01 UTC
bf7edfe 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 Uninterpreted functions 05 July 2019, 22:08:48 UTC
150ed33 remove flattenRType 04 July 2019, 23:15:18 UTC
back to top