Commits

Show all
Author Commit Message Labels Comments Date
Rob Simmons
Add a clown/joker example, not beautifully motivated by functors or deriviatives or logic or anything, just code.
Branches
fast_linear
Rob Simmons
Add Aaron's example
Branches
fast_linear
Rob Simmons
Turn off goal printing
Branches
fast_linear
Rob Simmons
Add figure 3 to Minamide's example
Branches
fast_linear
Rob Simmons
Binary insertion
Branches
fast_linear
Rob Simmons
Figure 2
Branches
fast_linear
Rob Simmons
Added tag holey-blog-3 for changeset 3e4e86d071a0
Branches
fast_linear
Rob Simmons
Error in linzipper: probably shoulda tested that
Tags
holey-blog-3
Branches
fast_linear
Rob Simmons
Added tag holey-blog-3 for changeset 24e3cede8b89
Branches
fast_linear
Rob Simmons
Bug fix noticed while preparing blog post, could have caused Not_found to be raised in the coverage checker when a type-correct pattern matching on the inside of a linear function is written if that pattern is known to be vacuous by subordination.
Branches
fast_linear
Rob Simmons
Added tag holey-blog-3 for changeset a933a8fa55a9
Branches
fast_linear
Rob Simmons
Fix a bug that occured when the immedate successor of the hole's type along the subordination relation was the outside type, but the outside type was not actually subordinate to itself. Also introduce an optimize syntax for the same situation.
Branches
fast_linear
Rob Simmons
Messing around with the scrap your zipper example
Branches
fast_linear
Rob Simmons
Added example insipred by Michael Adams' 'Scrap Your Zippers'
Branches
fast_linear
Rob Simmons
Add safe versions to both the zipper examples
Branches
fast_linear
Rob Simmons
Adapt Huet's original zipper example to linear functions
Branches
fast_linear
Rob Simmons
And now inside linear coverage checking works!
Branches
fast_linear
Rob Simmons
Add extra argument to case that tracks typing information
Branches
fast_linear
Rob Simmons
I can compute the necessary patterns for an inside-matching linear type, but I'm foiled. Given the pattern '[hole] f (Cons i hole)', I absolutely must have the contextual information about what type I'm pattern matching against or I don't know what the codomain of f is (and therefore I can't work out what type I'm pattern matching against). So I'm going to have to record the types of case analyses in typechecking in order to avoid doing type checking entirely inside of coverage.ml
Branches
fast_linear
Rob Simmons
Add (immediate) annotations to immediate dependencies
Branches
fast_linear
Rob Simmons
(Unchecked) inside pattern matching is now functional!
Branches
fast_linear
Rob Simmons
Modify interpreter with backpointers to make pattern matching at the end work
Branches
fast_linear
Rob Simmons
Add Case', to be produced by the coverage checker, manipulated later
Branches
fast_linear
Rob Simmons
Change coverage checker to potentially manipulate terms
Branches
fast_linear
Rob Simmons
I think just formatting
Branches
fast_linear
Rob Simmons
Revise closure code. Because that's fun.
Branches
fast_linear
Rob Simmons
merge to holey, with appropriate changes
Branches
fast_linear
Rob Simmons
merge to datatype
Branches
matching
Rob Simmons
merge to modprec again
Branches
default_modprec
Rob Simmons
Fix typo introduced by previous committ
  1. Prev
  2. Next