changeset | 56db662ebcfd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fun with type classes and modules |
files |
changeset | 38b299373676 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Looking up in a type class from a module |
files |
changeset | 0343557355fc |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Explifying type classes |
files |
changeset | e86411f647c6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Initial type class support |
files |
changeset | f4033abd6ab1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Inferring sql_type's |
files |
changeset | 1487c712eb12 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Stub WHERE support |
files |
changeset | cc68da3801bc |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Non-star SELECT |
files |
changeset | cb8493759a7b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Remove extraneous disjointness goal |
files |
changeset | cb8f69556975 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborating 'SELECT *' queries |
files |
changeset | dd82457fda82 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parsing and elaborating 'table' |
files |
changeset | df5fd8f6913a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | A multi-parameter datatype all the way through |
files |
changeset | aa54250f58ac |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parametrized datatypes through explify |
files |
changeset | 8e9f97508f0d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Datatype representation optimization |
files |
changeset | d11754ffe252 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Compiled pattern matching to C |
files |
changeset | 33d4a8eea484 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Case through explify |
files |
changeset | b2d752455182 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborating record patterns |
files |
changeset | 7ee424760d2f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborating module constructor patterns; parsing record patterns |
files |
changeset | 8221b95cc24c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Patterns for int and string constants |
files |
changeset | 021f5beb6f8d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Pattern match coverage checking |
files |
changeset | c7a6e6dbc318 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborating some basic pattern matching |
files |
changeset | a158f8c5aa55 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parsing basic patterns |
files |
changeset | 06a98129b23f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Add datatype import constructor annotations; datatypes through explify |
files |
changeset | a5ae7b3e37a4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Normalize datatype choice during SgiDatatypeImp elaboration |
files |
changeset | 870e8abbe3b9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Datatype import signature-matches abstract datatype |
files |
changeset | 1e382d10e832 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Abstracting datatypes with signature ascription |
files |
changeset | b4b70de488e9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | More datatype module stuff |
files |
changeset | adc4e42e3adc |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Basic datatype importing works |
files |
changeset | 34ccd7d2bea8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of datatype support |
files |
changeset | cfe6f9db74aa |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | radio and radioOption |
files |
changeset | 67ab26888839 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | textarea |
files |
changeset | 7420fa18d657 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Record cut |
files |
changeset | eb16f2aadbe9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Meta-programming forms |
files |
changeset | 80ac94b54e41 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fix opening and corifying of functors |
files |
changeset | 63c699450281 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Initial form support |
files |
changeset | f214c535d253 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | A simpler context encoding |
files |
changeset | adfa2c7a75da |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Form binding parameters threaded through |
files |
changeset | e3041657d653 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parsing and elaborating (non-mutual) 'val rec' |
files |
changeset | 3739af9e727a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Starting with closure links |
files |
changeset | 813e5a52063d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Remove closure conversion in favor of zany fun with modules, which also replaces 'page' |
files |
changeset | f0f59e918cac |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | page declaration, up through monoize |
files |
changeset | 94afff1ff7f6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | More fun with HTML |
files |
changeset | 1a4c51fa615c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | XML tags with contents |
files |
changeset | 4327abd52997 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Basic XML stuff |
files |
changeset | 94ef20a31550 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fancier head normalization pushed inside of Disjoint |
files |
changeset | 7bab29834cd6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Constraints in modules |
files |
changeset | 7f9bcc8bfa1e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | More with disjointness assumptions |
files |
changeset | 1f85890c9846 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Disjointness assumptions in expressions |
files |
changeset | e86370850c30 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Disjointness assumptions |
files |
changeset | 0a1baddd8ab2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Threading disjointness conditions through Elaborate |
files |
changeset | b4f2a258e52c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Initial disjointness prover |
files |
changeset | 60d97de1bbe8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Factor some operations into ElabOps |
files |
changeset | 321cb9805c8e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | A little more conservative unification |
files |
changeset | 37847b504cc6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | More hardcore unification |
files |
changeset | a6d45c6819c9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Implicit structure members |
files |
changeset | 522f4bd3955e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Broaden unification context |
files |
changeset | 88ffb3d61817 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Folding through a functor |
files |
changeset | 144d082b47ae |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Reduce efold |
files |
changeset | 6431b315a1e3 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborate efold |
files |
changeset | 9f89f0b00b84 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Elaborating cfold |
files |
changeset | 1ec5703c09c4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Proper subsignaturing for sub-structures |
files |