sort by:
Revision Author Date Message Commit Date
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
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
back to top