| Tue, 10 Mar 2009 12:44:40 -0400 |
Adam Chlipala |
ListEdit demo, minus prose |
| Tue, 24 Feb 2009 15:54:05 -0500 |
Adam Chlipala |
Folder generation for functors |
| Tue, 24 Feb 2009 15:38:01 -0500 |
Adam Chlipala |
Folder generation for functions |
| Tue, 24 Feb 2009 15:12:13 -0500 |
Adam Chlipala |
Demos compile again, with manual folders |
| Tue, 24 Feb 2009 13:46:08 -0500 |
Adam Chlipala |
Top.Fold.concat elaborates |
| Tue, 24 Feb 2009 12:01:24 -0500 |
Adam Chlipala |
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses |
| Sun, 22 Feb 2009 16:10:25 -0500 |
Adam Chlipala |
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top |
| Sat, 21 Feb 2009 16:11:56 -0500 |
Adam Chlipala |
Debug reverse-engineering unification |
| Sat, 21 Feb 2009 15:33:20 -0500 |
Adam Chlipala |
"Hello world" compiles, after replacing type-level fold with map |
| Tue, 13 Jan 2009 15:17:11 -0500 |
Adam Chlipala |
Initial experiments with nested <dyn> |
| Fri, 19 Dec 2008 10:27:58 -0500 |
Adam Chlipala |
Monad type class seems to be working |
| Fri, 19 Dec 2008 10:03:31 -0500 |
Adam Chlipala |
Initial conversion to arbitrary-kind classes |
| Thu, 27 Nov 2008 11:17:56 -0500 |
Adam Chlipala |
Remove some isUnitCon cases |
| Thu, 27 Nov 2008 10:40:29 -0500 |
Adam Chlipala |
Remove unnecessary lifts in ElabEnv.pushCRel |
| Thu, 27 Nov 2008 10:13:22 -0500 |
Adam Chlipala |
Remove unnecessary [kindof] calls |
| Tue, 11 Nov 2008 19:20:37 -0500 |
Adam Chlipala |
Add CutMulti |
| Sat, 08 Nov 2008 16:02:59 -0500 |
Adam Chlipala |
Especialize handles records better |
| Sat, 08 Nov 2008 13:15:00 -0500 |
Adam Chlipala |
Some small changes while failing to write [restrict] |
| Thu, 06 Nov 2008 19:43:48 -0500 |
Adam Chlipala |
Tree demo working (and other assorted regressions fixed) |
| Thu, 06 Nov 2008 17:09:53 -0500 |
Adam Chlipala |
About to begin optimization of recursive transaction functions |
| Thu, 06 Nov 2008 15:37:38 -0500 |
Adam Chlipala |
Inserted a NULL value |
| Thu, 06 Nov 2008 10:43:48 -0500 |
Adam Chlipala |
Cookies through explify |
| Thu, 06 Nov 2008 10:29:55 -0500 |
Adam Chlipala |
Cookies through elaborate |
| Sat, 01 Nov 2008 17:19:12 -0400 |
Adam Chlipala |
Fix some type-class detection |
| Sat, 01 Nov 2008 11:17:29 -0400 |
Adam Chlipala |
Elaborating 'let' |
| Fri, 31 Oct 2008 09:30:22 -0400 |
Adam Chlipala |
Replace 'with' with '++' |
| Tue, 21 Oct 2008 19:56:20 -0400 |
Adam Chlipala |
Sum prose |
| Tue, 21 Oct 2008 19:31:11 -0400 |
Adam Chlipala |
Infering sum rows |
| Tue, 21 Oct 2008 19:24:39 -0400 |
Adam Chlipala |
Sum demo, minus inference of {Unit}s |
| Tue, 21 Oct 2008 16:41:11 -0400 |
Adam Chlipala |
New implicit argument handling |
| Tue, 21 Oct 2008 15:11:42 -0400 |
Adam Chlipala |
Recursive unurlify for Default datatypes |
| Tue, 21 Oct 2008 12:06:35 -0400 |
Adam Chlipala |
ListShop skeleton |
| Tue, 14 Oct 2008 17:18:59 -0400 |
Adam Chlipala |
Reusable column handlers for Crud |
| Sat, 04 Oct 2008 20:05:50 -0400 |
Adam Chlipala |
Expand cases where expression wildcards are allowed |
| Sat, 04 Oct 2008 19:56:59 -0400 |
Adam Chlipala |
Improved inference of records of tuples |
| Sat, 04 Oct 2008 15:50:28 -0400 |
Adam Chlipala |
Merge CDisjoint and TDisjoint |
| Sun, 14 Sep 2008 19:03:55 -0400 |
Adam Chlipala |
Crud update form |
| Sun, 14 Sep 2008 15:10:04 -0400 |
Adam Chlipala |
Crud supports INSERT |
| Sun, 14 Sep 2008 11:02:18 -0400 |
Adam Chlipala |
SQL sequences |
| Sat, 13 Sep 2008 19:49:53 -0400 |
Adam Chlipala |
queryX |
| Sat, 13 Sep 2008 10:30:45 -0400 |
Adam Chlipala |
foldTR2 |
| Thu, 11 Sep 2008 19:59:31 -0400 |
Adam Chlipala |
Fixed a mind-numbing De Bruijn bug |
| Thu, 11 Sep 2008 18:36:20 -0400 |
Adam Chlipala |
Fix bug in subsignature check for con synonyms |
| Thu, 11 Sep 2008 18:32:41 -0400 |
Adam Chlipala |
Crud list works |
| Thu, 11 Sep 2008 17:41:52 -0400 |
Adam Chlipala |
Crud listing IDs |
| Tue, 09 Sep 2008 09:15:00 -0400 |
Adam Chlipala |
Datatype positivity check |
| Sun, 07 Sep 2008 10:13:02 -0400 |
Adam Chlipala |
intToString |
| Tue, 02 Sep 2008 17:31:45 -0400 |
Adam Chlipala |
Compiling a parametrized query the inefficient way |
| Tue, 02 Sep 2008 10:51:41 -0400 |
Adam Chlipala |
'database' declaration threaded through compiler |
| Sun, 31 Aug 2008 15:15:41 -0400 |
Adam Chlipala |
'eq' type class |
| Sun, 31 Aug 2008 15:04:10 -0400 |
Adam Chlipala |
Monoized GROUP BY |
| Sun, 31 Aug 2008 09:45:23 -0400 |
Adam Chlipala |
Corify transaction wrappers |
| Thu, 28 Aug 2008 14:48:33 -0400 |
Adam Chlipala |
Transactions and queries, at source level |
| Thu, 28 Aug 2008 13:13:16 -0400 |
Adam Chlipala |
Checking for well-formed 'val rec' |
| Thu, 28 Aug 2008 11:17:14 -0400 |
Adam Chlipala |
SELECTing arbitrary expressions |
| Thu, 21 Aug 2008 14:45:31 -0400 |
Adam Chlipala |
Resolving lingering type class constraints |
| Thu, 21 Aug 2008 12:49:29 -0400 |
Adam Chlipala |
Queries back to working as well as before, after start of refactoring to support grouping |
| Sat, 16 Aug 2008 17:35:28 -0400 |
Adam Chlipala |
SQL boolean operators |
| Sat, 16 Aug 2008 16:57:21 -0400 |
Adam Chlipala |
Signature ascription for type classes |
| Sat, 16 Aug 2008 16:30:07 -0400 |
Adam Chlipala |
Fun with type classes and modules |
| Sat, 16 Aug 2008 15:58:25 -0400 |
Adam Chlipala |
Looking up in a type class from a module |
| Sat, 16 Aug 2008 14:45:23 -0400 |
Adam Chlipala |
Explifying type classes |
| Sat, 16 Aug 2008 14:32:18 -0400 |
Adam Chlipala |
Initial type class support |
| Sat, 16 Aug 2008 12:35:46 -0400 |
Adam Chlipala |
Inferring sql_type's |
| Sat, 16 Aug 2008 12:15:38 -0400 |
Adam Chlipala |
Stub WHERE support |
| Thu, 14 Aug 2008 18:35:08 -0400 |
Adam Chlipala |
Non-star SELECT |
| Thu, 14 Aug 2008 15:27:35 -0400 |
Adam Chlipala |
Remove extraneous disjointness goal |
| Thu, 14 Aug 2008 15:24:59 -0400 |
Adam Chlipala |
Elaborating 'SELECT *' queries |
| Thu, 14 Aug 2008 13:20:29 -0400 |
Adam Chlipala |
Parsing and elaborating 'table' |
| Sat, 09 Aug 2008 08:47:36 -0400 |
Adam Chlipala |
A multi-parameter datatype all the way through |
| Fri, 08 Aug 2008 10:28:32 -0400 |
Adam Chlipala |
Parametrized datatypes through explify |
| Sun, 03 Aug 2008 19:49:21 -0400 |
Adam Chlipala |
Datatype representation optimization |
| Sun, 03 Aug 2008 12:43:20 -0400 |
Adam Chlipala |
Compiled pattern matching to C |
| Thu, 31 Jul 2008 16:28:55 -0400 |
Adam Chlipala |
Case through explify |
| Thu, 31 Jul 2008 13:08:57 -0400 |
Adam Chlipala |
Elaborating record patterns |
| Thu, 31 Jul 2008 11:28:55 -0400 |
Adam Chlipala |
Elaborating module constructor patterns; parsing record patterns |
| Thu, 31 Jul 2008 10:44:52 -0400 |
Adam Chlipala |
Patterns for int and string constants |
| Thu, 31 Jul 2008 10:31:30 -0400 |
Adam Chlipala |
Pattern match coverage checking |
| Thu, 31 Jul 2008 10:06:27 -0400 |
Adam Chlipala |
Elaborating some basic pattern matching |
| Tue, 29 Jul 2008 16:38:15 -0400 |
Adam Chlipala |
Parsing basic patterns |
| Tue, 29 Jul 2008 12:30:04 -0400 |
Adam Chlipala |
Add datatype import constructor annotations; datatypes through explify |
| Thu, 24 Jul 2008 16:51:24 -0400 |
Adam Chlipala |
Normalize datatype choice during SgiDatatypeImp elaboration |
| Thu, 24 Jul 2008 16:48:47 -0400 |
Adam Chlipala |
Datatype import signature-matches abstract datatype |
| Thu, 24 Jul 2008 16:41:12 -0400 |
Adam Chlipala |
Abstracting datatypes with signature ascription |
| Thu, 24 Jul 2008 16:36:41 -0400 |
Adam Chlipala |
More datatype module stuff |
| Thu, 24 Jul 2008 15:49:30 -0400 |
Adam Chlipala |
Basic datatype importing works |
| Thu, 24 Jul 2008 15:02:03 -0400 |
Adam Chlipala |
Start of datatype support |
| Thu, 24 Jul 2008 11:10:23 -0400 |
Adam Chlipala |
radio and radioOption |
| Thu, 24 Jul 2008 10:41:53 -0400 |
Adam Chlipala |
textarea |
| Thu, 24 Jul 2008 10:09:21 -0400 |
Adam Chlipala |
Record cut |
| Tue, 22 Jul 2008 18:46:04 -0400 |
Adam Chlipala |
Meta-programming forms |
| Tue, 22 Jul 2008 18:20:13 -0400 |
Adam Chlipala |
Fix opening and corifying of functors |
| Sun, 20 Jul 2008 11:33:23 -0400 |
Adam Chlipala |
Initial form support |
| Sun, 20 Jul 2008 10:40:25 -0400 |
Adam Chlipala |
A simpler context encoding |
| Sun, 20 Jul 2008 10:11:16 -0400 |
Adam Chlipala |
Form binding parameters threaded through |
| Thu, 17 Jul 2008 10:09:34 -0400 |
Adam Chlipala |
Parsing and elaborating (non-mutual) 'val rec' |
| Sun, 13 Jul 2008 11:43:57 -0400 |
Adam Chlipala |
Starting with closure links |
| Sun, 13 Jul 2008 10:17:06 -0400 |
Adam Chlipala |
Remove closure conversion in favor of zany fun with modules, which also replaces 'page' |
| Thu, 10 Jul 2008 10:11:35 -0400 |
Adam Chlipala |
page declaration, up through monoize |
| Thu, 03 Jul 2008 17:14:35 -0400 |
Adam Chlipala |
More fun with HTML |
| Thu, 03 Jul 2008 17:02:42 -0400 |
Adam Chlipala |
XML tags with contents |
| Thu, 03 Jul 2008 16:26:28 -0400 |
Adam Chlipala |
Basic XML stuff |
| Thu, 03 Jul 2008 11:04:25 -0400 |
Adam Chlipala |
Fancier head normalization pushed inside of Disjoint |
| Tue, 01 Jul 2008 15:58:02 -0400 |
Adam Chlipala |
Constraints in modules |
| Tue, 01 Jul 2008 13:19:14 -0400 |
Adam Chlipala |
More with disjointness assumptions |
| Tue, 01 Jul 2008 12:25:12 -0400 |
Adam Chlipala |
Disjointness assumptions in expressions |
| Tue, 01 Jul 2008 12:10:46 -0400 |
Adam Chlipala |
Disjointness assumptions |
| Tue, 01 Jul 2008 11:39:14 -0400 |
Adam Chlipala |
Threading disjointness conditions through Elaborate |
| Tue, 01 Jul 2008 10:55:38 -0400 |
Adam Chlipala |
Initial disjointness prover |
| Tue, 01 Jul 2008 09:29:49 -0400 |
Adam Chlipala |
Factor some operations into ElabOps |
| Sun, 29 Jun 2008 11:23:22 -0400 |
Adam Chlipala |
A little more conservative unification |
| Sun, 29 Jun 2008 11:20:34 -0400 |
Adam Chlipala |
More hardcore unification |
| Sun, 29 Jun 2008 11:05:38 -0400 |
Adam Chlipala |
Implicit structure members |
| Sun, 29 Jun 2008 10:39:43 -0400 |
Adam Chlipala |
Broaden unification context |
| Thu, 26 Jun 2008 12:35:26 -0400 |
Adam Chlipala |
Folding through a functor |
| Thu, 26 Jun 2008 12:12:06 -0400 |
Adam Chlipala |
Reduce efold |
| Thu, 26 Jun 2008 11:09:30 -0400 |
Adam Chlipala |
Elaborate efold |
| Thu, 26 Jun 2008 09:48:54 -0400 |
Adam Chlipala |
Elaborating cfold |
| Thu, 26 Jun 2008 09:09:30 -0400 |
Adam Chlipala |
Proper subsignaturing for sub-structures |
| Thu, 26 Jun 2008 09:03:38 -0400 |
Adam Chlipala |
Proper subsignaturing for sub-signatures |
| Thu, 26 Jun 2008 08:54:49 -0400 |
Adam Chlipala |
Proper hiding of shadowed bindings in principal signatures |
| Sun, 22 Jun 2008 20:11:59 -0400 |
Adam Chlipala |
Signature duplicate entry checking for principal signatures |
| Sun, 22 Jun 2008 19:44:01 -0400 |
Adam Chlipala |
Signature duplicate entry checking |
| Sun, 22 Jun 2008 19:34:35 -0400 |
Adam Chlipala |
open |
| Sun, 22 Jun 2008 19:10:38 -0400 |
Adam Chlipala |
Subsignatures |
| Sun, 22 Jun 2008 18:17:21 -0400 |
Adam Chlipala |
include |
| Sun, 22 Jun 2008 14:23:05 -0400 |
Adam Chlipala |
Separate compilation and automatic basis importation |
| Sun, 22 Jun 2008 09:27:29 -0400 |
Adam Chlipala |
Start of FFI |
| Thu, 19 Jun 2008 17:55:36 -0400 |
Adam Chlipala |
Corifying functors |
| Thu, 19 Jun 2008 17:04:08 -0400 |
Adam Chlipala |
Elaborating functor applications |
| Thu, 19 Jun 2008 16:43:24 -0400 |
Adam Chlipala |
Subtyping for functor signatures |
| Thu, 19 Jun 2008 16:35:40 -0400 |
Adam Chlipala |
Elaborating 'where' |
| Thu, 19 Jun 2008 16:04:28 -0400 |
Adam Chlipala |
Beginning of functor elaboration |
| Thu, 19 Jun 2008 15:15:00 -0400 |
Adam Chlipala |
Functor parsing |
| Tue, 17 Jun 2008 17:08:28 -0400 |
Adam Chlipala |
Proper selfification |
| Tue, 17 Jun 2008 16:38:54 -0400 |
Adam Chlipala |
Elaborating module projection |
| Thu, 12 Jun 2008 17:41:32 -0400 |
Adam Chlipala |
Matching structures in signatures |
| Thu, 12 Jun 2008 17:35:51 -0400 |
Adam Chlipala |
Matching values in signatures |
| Thu, 12 Jun 2008 17:16:20 -0400 |
Adam Chlipala |
Simple signature matching |
| Thu, 12 Jun 2008 14:04:22 -0400 |
Adam Chlipala |
Parsing and printing basic module system |
| Tue, 10 Jun 2008 18:28:43 -0400 |
Adam Chlipala |
Translation to Cjr |
| Tue, 10 Jun 2008 15:56:33 -0400 |
Adam Chlipala |
Closure conversion |
| Sun, 08 Jun 2008 14:25:27 -0400 |
Adam Chlipala |
Unification wildcards |
| Sun, 08 Jun 2008 14:10:51 -0400 |
Adam Chlipala |
Further experiments with implicit arguments |
| Sun, 08 Jun 2008 13:00:12 -0400 |
Adam Chlipala |
Implicit constructor arguments |
| Sun, 08 Jun 2008 12:27:08 -0400 |
Adam Chlipala |
Primitive type constants |
| Sun, 08 Jun 2008 11:32:48 -0400 |
Adam Chlipala |
Lifting cons in ElabEnv |
| Fri, 28 Mar 2008 17:34:57 -0400 |
Adam Chlipala |
Fun with records |
| Fri, 28 Mar 2008 15:20:46 -0400 |
Adam Chlipala |
Simple elaboration working |
| Fri, 28 Mar 2008 13:59:03 -0400 |
Adam Chlipala |
Start of elaborating expressions |
| Sat, 26 Jan 2008 17:26:14 -0500 |
Adam Chlipala |
Added simple expression constructors to Elab |
| Sat, 26 Jan 2008 17:10:26 -0500 |
Adam Chlipala |
Parsing basic expressions |
| Sat, 26 Jan 2008 16:44:39 -0500 |
Adam Chlipala |
Check for leftover kind unifs |
| Sat, 26 Jan 2008 16:02:47 -0500 |
Adam Chlipala |
Elaborating files |
| Sat, 26 Jan 2008 15:29:09 -0500 |
Adam Chlipala |
Rename Laconic* modules to Source* |
| Sat, 26 Jan 2008 15:26:12 -0500 |
Adam Chlipala |
Elaborating cons and decls |
| Sat, 26 Jan 2008 14:27:33 -0500 |
Adam Chlipala |
Start of elaboration |
