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

sort by:
Revision Author Date Message Commit Date
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
0082ea4 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 Updated pretty-print to include cubifying 02 July 2019, 22:41:45 UTC
09b6bd6 Pseudo mist linear examples 02 July 2019, 22:41:29 UTC
7833fdc pseudo-mist revoke, tick, and linear access 02 July 2019, 16:00:47 UTC
a2b22e3 renaming split on accident 28 June 2019, 18:12:20 UTC
829fca4 removed debugging info 28 June 2019, 18:11:40 UTC
d5df0e5 Updated todo testing framework 05 June 2019, 21:18:44 UTC
fe707ec oops; added todo tests back 05 June 2019, 18:21:10 UTC
8f3cf15 fix tests/todo 01 June 2019, 21:52:01 UTC
6ef4dfd Merge pull request #13 from ucsd-progsys/bidi bidirectional constraint generation 30 May 2019, 21:18:11 UTC
7290276 make fixpoint a submodule 30 May 2019, 21:17:05 UTC
cfb38bd incrState actually increments 29 May 2019, 23:00:40 UTC
6aa997c Fixed more substitutions 29 May 2019, 22:01:11 UTC
b2c12f7 Added pretty print script 29 May 2019, 21:54:27 UTC
59775fb Added pretty print script 29 May 2019, 21:49:24 UTC
7027c40 Removing subst1 forms 29 May 2019, 21:47:38 UTC
88ae0a1 Added constraint kinds simplification to CGen 24 May 2019, 21:35:59 UTC
92878ee Split incrState and incrState poly examples 21 May 2019, 21:42:00 UTC
fd138ab 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 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 Fixed pprint for RApp 07 May 2019, 16:18:53 UTC
d3755a8 Make example work: get >> get 03 May 2019, 17:33:09 UTC
39dc9b7 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 Merge pull request #12 from ucsd-progsys/tycon Type Constructors 30 April 2019, 08:23:04 UTC
62681dd bump fp 30 April 2019, 08:01:52 UTC
a610328 start: make cgen bidirectional again 29 April 2019, 20:52:55 UTC
40de375 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 fix crash, incrState:foTypes should mirror foBinds 28 April 2019, 00:31:11 UTC
309931f add semantic whitespace to parser 26 April 2019, 17:45:23 UTC
34b1fa6 Subtyping should respect variance 26 April 2019, 17:45:23 UTC
4d368ea Whitespace and new test 25 April 2019, 21:40:32 UTC
7b41627 Fixed incrState syntax 23 April 2019, 20:32:59 UTC
da4119b oops commited the wrong file 23 April 2019, 20:23:03 UTC
4460a0b Cgen RApp <: RApp case 23 April 2019, 20:19:19 UTC
0411239 Fixed error by squashing higher-order kvar params 23 April 2019, 20:16:49 UTC
8d56902 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 Fixed annotation in synthesizeSpine 23 April 2019, 20:01:00 UTC
d32554a Improved printing of type application 23 April 2019, 20:00:19 UTC
72b4dc7 Partially corrected temporary cgen error printing 23 April 2019, 20:00:07 UTC
41444b0 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 fresh RType on CTor 15 April 2019, 18:17:30 UTC
c470669 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 Parser: Refactored RFun and RIFun into one parser 12 April 2019, 16:12:03 UTC
c7b763d Progress Towards Typechecking incrState 12 April 2019, 04:12:30 UTC
ebcd665 Fixed incr00 test syntax 10 April 2019, 21:38:23 UTC
c0a5ea6 Changed printing of errors in runMist 10 April 2019, 21:38:03 UTC
6c3602d Added single equal as other equality operator 10 April 2019, 20:58:43 UTC
195dd5b Fixed parse error 10 April 2019, 20:57:07 UTC
adbba40 Added tycon tests 10 April 2019, 20:24:07 UTC
9d3d6c6 more parser tweaks 04 April 2019, 23:46:44 UTC
0070386 Tweaked Expression Parser 04 April 2019, 23:11:54 UTC
c11f653 propogate assumes 03 April 2019, 21:09:16 UTC
4cd10cd parse Ctor with variance 01 April 2019, 23:35:42 UTC
d764f6e 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 Merge pull request #11 from ucsd-progsys/typed-anf Adding annotation points to every AST node 28 March 2019, 22:42:05 UTC
f72ed27 bump lf 28 March 2019, 22:41:39 UTC
2c6463f Annotating each node before ANF 26 March 2019, 19:50:08 UTC
c565421 Moving to annotated expression forms 26 March 2019, 19:49:13 UTC
0546d63 Added type annotations to App and TApp 22 March 2019, 01:01:19 UTC
6ff8ddf Compiles with new Expr annotated forms 21 March 2019, 23:27:37 UTC
e8eb56c Switched Prim2 to Prim apart from ANF 18 March 2019, 18:30:01 UTC
9ee6750 Correctly substituting for existentials in annotations 14 March 2019, 20:56:25 UTC
0c0da4d Merge pull request #10 from ucsd-progsys/implicits Implicits 12 March 2019, 17:39:25 UTC
385d693 Merge pull request #9 from ucsd-progsys/liquid-cgen Liquid cgen 12 March 2019, 17:39:13 UTC
20b2c74 implement implicits 08 March 2019, 19:25:34 UTC
80d7162 added testcase that breaks checker 24 February 2019, 09:44:41 UTC
1157f0d tests pass 24 February 2019, 09:42:24 UTC
bfa9b26 cgen: fresh (Gamma) and subst bug 22 February 2019, 20:50:27 UTC
efd594f Added initial unit test for CGen 22 February 2019, 07:00:21 UTC
1aebb7e Left todo for normalizer 22 February 2019, 02:10:34 UTC
7073357 Testing new cgen for lets 21 February 2019, 19:08:02 UTC
1543ace Fixed bug in collecting kvars 21 February 2019, 18:57:30 UTC
83aafe7 Surfacing solver result in mist runner 20 February 2019, 18:56:58 UTC
69f4a4a Adding refinement checker failing test 20 February 2019, 00:03:41 UTC
back to top