Skip to main content
swh:1:snp:aeaf3dbb58f5be84b565e73b5ade1503ee8cb6d6
sort by:
RevisionAuthorDateMessageCommit Date
cda4560 Anish Tondwalkar16 March 2020, 20:43:43 UTCfix tests16 March 2020, 20:43:43 UTC
8d287eb mkolosick02 March 2020, 23:01:12 UTCMore mochi02 March 2020, 23:01:12 UTC
a2b5559 mkolosick02 March 2020, 07:42:11 UTCMochi tests in progress02 March 2020, 07:42:11 UTC
e494a2f mkolosick02 March 2020, 07:41:39 UTCUpdated fstar incr02 March 2020, 07:41:39 UTC
d8391ff mkolosick26 February 2020, 02:54:16 UTCAdding fstar tests26 February 2020, 02:54:16 UTC
9a832b4 Anish Tondwalkar26 February 2020, 00:17:51 UTCoops26 February 2020, 00:17:51 UTC
dc49dfd Anish Tondwalkar26 February 2020, 00:07:03 UTCAdded emptySet and intersection primOps26 February 2020, 00:07:03 UTC
c915c9c mkolosick23 November 2019, 02:43:12 UTCmochi-d2 and mochi-d323 November 2019, 02:43:12 UTC
314ec0f mkolosick23 November 2019, 01:43:04 UTCapp-succ and app-succ023 November 2019, 01:43:04 UTC
340b80e mkolosick23 November 2019, 01:29:11 UTCapp-succ and repeat23 November 2019, 01:29:11 UTC
f6db5fa mkolosick22 November 2019, 01:57:45 UTCRepeat is back22 November 2019, 01:57:45 UTC
242582c mkolosick22 November 2019, 01:44:02 UTCmochi-d222 November 2019, 01:44:25 UTC
bea7946 mkolosick22 November 2019, 01:36:31 UTCMove mochi d2 to neg22 November 2019, 01:44:25 UTC
347be3b Anish Tondwalkar22 November 2019, 01:36:28 UTCadded mochi tests22 November 2019, 01:36:28 UTC
80cebdd mkolosick20 November 2019, 05:47:01 UTCTick tick doesn't work20 November 2019, 05:47:01 UTC
6f5b475 mkolosick20 November 2019, 05:37:09 UTCOmega isn't loop20 November 2019, 05:37:09 UTC
093ff88 mkolosick20 November 2019, 05:34:36 UTCTick tock 3: some real ticks and tocks20 November 2019, 05:34:36 UTC
942eb2f mkolosick20 November 2019, 03:19:40 UTCMinor changes20 November 2019, 03:19:40 UTC
0545284 Anish Tondwalkar20 November 2019, 03:18:38 UTCadd some of the tests from mochi20 November 2019, 03:18:38 UTC
68d3acd mkolosick19 November 2019, 07:26:18 UTCActual unbounded loop: DOES NOT WORK YET19 November 2019, 07:26:18 UTC
2836ad7 mkolosick19 November 2019, 05:36:34 UTCRemoved printing19 November 2019, 05:36:34 UTC
9a417f5 mkolosick19 November 2019, 01:47:25 UTCFull looping for19 November 2019, 01:47:25 UTC
91f9eff mkolosick19 November 2019, 00:35:44 UTCAutomatically unpacking sigmas19 November 2019, 00:35:44 UTC
0d76623 Anish Tondwalkar18 November 2019, 21:46:22 UTCWrote sigma-elaborator18 November 2019, 21:46:22 UTC
fb48833 Anish Tondwalkar18 November 2019, 21:45:54 UTCcleanup and hygiene18 November 2019, 21:45:54 UTC
09636e9 mkolosick18 November 2019, 05:41:12 UTCInitial ANF sigma work18 November 2019, 05:41:12 UTC
19db75a mkolosick16 November 2019, 08:40:55 UTCFixed polymorphism bug16 November 2019, 08:50:42 UTC
4350cd5 mkolosick16 November 2019, 07:00:22 UTCSwitched to sigmas on some examples16 November 2019, 07:00:22 UTC
7886cde mkolosick16 November 2019, 06:24:57 UTCFixed freshRType bug16 November 2019, 06:24:57 UTC
49bb9d0 mkolosick13 November 2019, 19:53:32 UTCAdded RIFun to freshRType13 November 2019, 19:56:36 UTC
5c0120a mkolosick11 November 2019, 17:54:16 UTCPagination with tokens13 November 2019, 19:56:36 UTC
301208f mkolosick11 November 2019, 06:30:06 UTCMore interesting forSigma test13 November 2019, 19:56:36 UTC
0b071dc mkolosick11 November 2019, 06:13:23 UTCAdded implicit sigma types. Test and usage are in pos/forSigma.hs13 November 2019, 19:56:36 UTC
ca8def0 mkolosick09 November 2019, 04:42:49 UTCRemoved unneeded implicits13 November 2019, 19:56:36 UTC
e0df534 mkolosick09 November 2019, 04:11:29 UTCFixed typo in forSigma13 November 2019, 19:56:36 UTC
3063e0e mkolosick09 November 2019, 01:27:07 UTCWIP on forSigma13 November 2019, 19:56:36 UTC
66181ea Anish Tondwalkar09 November 2019, 01:07:19 UTCSupport for Higher-Rank Types you need double parens (see hrts.hs)13 November 2019, 19:56:36 UTC
12b8e31 mkolosick09 November 2019, 00:04:13 UTCPagination tokens13 November 2019, 19:56:36 UTC
f791d87 mkolosick08 November 2019, 00:40:29 UTCRemoving ANF13 November 2019, 19:56:36 UTC
dca1c45 mkolosick06 November 2019, 23:14:02 UTCCommit before disabling ANF13 November 2019, 19:56:36 UTC
ecf9dd9 mkolosick05 November 2019, 01:07:29 UTCRemoved strengthening13 November 2019, 19:56:36 UTC
d6c8677 Anish Tondwalkar08 November 2019, 23:20:16 UTCAdd partial pagination308 November 2019, 23:20:40 UTC
b52fffe mkolosick01 November 2019, 18:17:40 UTCUpdated pure in tests01 November 2019, 18:17:40 UTC
883df18 mkolosick29 October 2019, 22:35:08 UTCCPS script29 October 2019, 22:35:08 UTC
082f610 mkolosick22 October 2019, 21:56:49 UTCRefixed parser22 October 2019, 21:56:49 UTC
a90a8af mkolosick21 October 2019, 18:24:24 UTCMore tests22 October 2019, 21:46:04 UTC
f59c0b0 mkolosick21 October 2019, 18:23:13 UTCMerge commit of some sort22 October 2019, 21:46:04 UTC
e7cedf6 mkolosick21 October 2019, 17:47:01 UTCshillSet experiments22 October 2019, 21:46:04 UTC
5f94d69 Anish Tondwalkar21 October 2019, 18:07:18 UTCadded TCP client example21 October 2019, 18:07:18 UTC
f9d43a2 Anish Tondwalkar20 October 2019, 05:17:02 UTCrun tests with setVerbosity Quiet20 October 2019, 06:22:20 UTC
23ef471 Anish Tondwalkar18 October 2019, 19:01:34 UTCUpdate to ticktock3 Add send/recv channels and prove that unreachable states are unreachable18 October 2019, 19:01:34 UTC
c56ef6c Anish Tondwalkar17 October 2019, 21:33:07 UTCAdded twoPhaseCommit17 October 2019, 21:33:07 UTC
ce240b3 Anish Tondwalkar17 October 2019, 02:31:05 UTCadded ticktock and pagination17 October 2019, 02:31:23 UTC
f1d86f3 Anish Tondwalkar17 October 2019, 00:20:03 UTCRead verbosity from command line instead of statically specifying it17 October 2019, 02:31:23 UTC
3050d85 mkolosick14 October 2019, 18:56:59 UTCAdded or and implication14 October 2019, 18:56:59 UTC
a139996 Anish Tondwalkar11 October 2019, 00:38:30 UTCidr_login finally works!11 October 2019, 00:38:30 UTC
5570953 Anish Tondwalkar20 September 2019, 20:16:26 UTCedits to idr_login20 September 2019, 20:16:26 UTC
6aae376 mkolosick12 September 2019, 21:34:45 UTCAdded implicit lambda term former12 September 2019, 21:35:20 UTC
8ca0371 Anish Tondwalkar12 September 2019, 20:30:00 UTCMore 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 happy12 September 2019, 20:30:00 UTC
5c17971 Anish Tondwalkar10 September 2019, 18:29:33 UTCAdded test for renamer bug implicit args are in scope in the body in cgen, which is correct, but not in the renamer10 September 2019, 18:29:33 UTC
6787ad4 Anish Tondwalkar10 September 2019, 06:58:30 UTCFirst 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 upon10 September 2019, 06:58:30 UTC
cd20f0c mkolosick09 September 2019, 21:24:19 UTCFixed 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 Tondwalkar09 September 2019, 20:12:25 UTCAdded todo/for case with refinement on iter index09 September 2019, 20:12:25 UTC
9d7c337 mkolosick29 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 mkolosick26 August 2019, 22:42:02 UTCFixed set annotations in shillSet26 August 2019, 22:42:02 UTC
5ea1864 mkolosick26 August 2019, 20:40:22 UTCFixed parsing of annotated lets and added negative test26 August 2019, 20:40:22 UTC
ad522c2 Anish Tondwalkar21 August 2019, 03:39:42 UTCAnnotated let binders21 August 2019, 03:43:02 UTC
22dbb0e Anish Tondwalkar21 August 2019, 01:06:17 UTCcorrectly serialize type constructors to FP21 August 2019, 01:06:17 UTC
579b1dc Anish Tondwalkar19 August 2019, 09:38:42 UTCBetter parse errors19 August 2019, 09:38:42 UTC
a62e4b2 Anish Tondwalkar19 August 2019, 08:45:23 UTCUpdate 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 lts19 August 2019, 08:45:23 UTC
71eb919 mkolosick15 August 2019, 23:20:00 UTCBetter formatted error messages from solver failures15 August 2019, 23:20:00 UTC
b681213 mkolosick15 August 2019, 23:08:18 UTCFixed printf format string15 August 2019, 23:08:18 UTC
c3df68d mkolosick15 August 2019, 23:03:10 UTCFixed Set bug15 August 2019, 23:03:10 UTC
68df304 Anish Tondwalkar15 August 2019, 22:42:01 UTCrefactored SSParsedExpr15 August 2019, 22:46:36 UTC
95861d2 Anish Tondwalkar15 August 2019, 17:59:20 UTCSSParsedExpr is now recursive This recursion should probably be done at the ParsedExpr level, but that's an involved refactoring15 August 2019, 22:45:56 UTC
9d2a590 mkolosick15 August 2019, 22:40:46 UTCFixed test framework to use new config object15 August 2019, 22:40:46 UTC
065c068 mkolosick15 August 2019, 22:33:50 UTCAdded read option to mist15 August 2019, 22:33:50 UTC
7069a8e Anish Tondwalkar07 August 2019, 18:51:37 UTCstart work on idris login example07 August 2019, 18:51:37 UTC
ea1aad5 Anish Tondwalkar04 August 2019, 05:52:42 UTCcleanup pointers example04 August 2019, 05:52:42 UTC
97f6408 Anish Tondwalkar04 August 2019, 05:31:33 UTCfix bug with implicits after forall04 August 2019, 05:52:10 UTC
0c3f096 Anish Tondwalkar04 August 2019, 05:30:22 UTCoops04 August 2019, 05:30:22 UTC
e2b69aa Anish Tondwalkar02 August 2019, 18:44:06 UTCunit in pointers_noalias.hs02 August 2019, 18:44:06 UTC
4d122d5 Anish Tondwalkar02 August 2019, 18:11:54 UTCMake pattern matcher timeout go away in ToFixpoint02 August 2019, 18:11:54 UTC
ff589c2 Anish Tondwalkar02 August 2019, 17:58:48 UTCAdd unit Type02 August 2019, 17:58:48 UTC
088d2fc Anish Tondwalkar02 August 2019, 17:49:19 UTCImprove debugging output from CGen.hs02 August 2019, 17:49:19 UTC
82249de Anish Tondwalkar02 August 2019, 07:44:51 UTCFix equal primOp02 August 2019, 07:44:51 UTC
72aa198 Anish Tondwalkar01 August 2019, 07:53:00 UTCisolated 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 Tondwalkar30 July 2019, 18:46:43 UTCprogress 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 Tondwalkar30 July 2019, 18:40:47 UTCMixed up forall and rforall in CGen30 July 2019, 18:40:47 UTC
3936ebc Anish Tondwalkar29 July 2019, 15:15:06 UTCadd subtyping rule fox right-hand implicits29 July 2019, 15:15:06 UTC
4c79ff0 Anish Tondwalkar29 July 2019, 05:25:06 UTCimplement decr in pointers example. start init[ but seems there's a checker bug blocking init29 July 2019, 05:25:06 UTC
bb8b279 Anish Tondwalkar29 July 2019, 04:54:52 UTCadded store primitive29 July 2019, 04:54:52 UTC
60787e2 Anish Tondwalkar26 July 2019, 07:16:05 UTCadded map store28 July 2019, 22:30:41 UTC
035e56a Anish Tondwalkar24 July 2019, 11:40:18 UTCSet is a Ctor24 July 2019, 11:45:36 UTC
d70ff51 Anish Tondwalkar22 July 2019, 23:55:09 UTCsplit off todo/for.hs from shill22 July 2019, 23:55:09 UTC
7eaf80d Anish Tondwalkar20 July 2019, 22:24:09 UTCFixed fixpoint scoping bug next: cryptic Checker error20 July 2019, 22:24:09 UTC
47d4396 Anish Tondwalkar19 July 2019, 23:03:18 UTCadded TODOs19 July 2019, 23:03:18 UTC
0a83b72 Anish Tondwalkar19 July 2019, 22:59:50 UTCParse nested RApp19 July 2019, 22:59:50 UTC
e395635 Anish Tondwalkar19 July 2019, 22:53:06 UTCClean up type signatures19 July 2019, 22:53:06 UTC
257b123 Anish Tondwalkar19 July 2019, 22:42:30 UTCfix mistake in shillset19 July 2019, 22:42:30 UTC