We are hiring ! See our job offers.
swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
sort by:
Revision Author Date Message Commit Date
cda4560 Anish Tondwalkar 16 March 2020, 20:43:43 UTC fix tests 16 March 2020, 20:43:43 UTC
8d287eb mkolosick 02 March 2020, 23:01:12 UTC More mochi 02 March 2020, 23:01:12 UTC
a2b5559 mkolosick 02 March 2020, 07:42:11 UTC Mochi tests in progress 02 March 2020, 07:42:11 UTC
e494a2f mkolosick 02 March 2020, 07:41:39 UTC Updated fstar incr 02 March 2020, 07:41:39 UTC
d8391ff mkolosick 26 February 2020, 02:54:16 UTC Adding fstar tests 26 February 2020, 02:54:16 UTC
9a832b4 Anish Tondwalkar 26 February 2020, 00:17:51 UTC oops 26 February 2020, 00:17:51 UTC
dc49dfd Anish Tondwalkar 26 February 2020, 00:07:03 UTC Added emptySet and intersection primOps 26 February 2020, 00:07:03 UTC
c915c9c mkolosick 23 November 2019, 02:43:12 UTC mochi-d2 and mochi-d3 23 November 2019, 02:43:12 UTC
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
back to top