William J. Bowman
3af3d8dbe9
Small syntax fixes
2016-01-19 11:20:19 -05:00
William J. Bowman
22404dfe98
Fixed up inferrence rules
2016-01-19 11:12:04 -05:00
William J. Bowman
0e46da74ab
[Broken] rewriting the rest of olly
...
Rewriting the rest of olly, including the latex and coq generators, and
the define-relation form.
Unfortunately, managed to break parsing somehow.
2016-01-19 11:12:03 -05:00
William J. Bowman
d613b53700
Renamed "nested-expression" syntax to match docs
2016-01-19 11:12:03 -05:00
William J. Bowman
c7aefdb032
Removed Var "abstractions"
...
Olly uses De Bruijn, but was attempting to use abstractions to allow
changing that. Unfortunately, these were not really abstractions. So
they're now gone.
2016-01-19 11:12:03 -05:00
William J. Bowman
fd52c764da
Fixed bug in define-relation
...
Previously, define-relation would not accept declarations with types
that did not match syntax-class id
2016-01-19 11:12:02 -05:00
William J. Bowman
fb39a88eac
Converted stlc example to use List for environment
2016-01-19 11:12:02 -05:00
William J. Bowman
9fb4c55799
Fixed binding in olly
2016-01-19 11:12:02 -05:00
William J. Bowman
f0dce3bf92
Fixed syntax-class of non-terminal definitions
...
Previously, syntax class would accept definitions for which I could not
generate inductive constructors. Changed the syntax class to rule these out.
2016-01-19 11:12:01 -05:00
William J. Bowman
345c12f040
Rewrote define-language
...
Working on #9 and fixing issues in Olly
2016-01-19 11:12:01 -05:00
William J. Bowman
3a644fae90
Added length function
2016-01-19 11:11:31 -05:00
William J. Bowman
b0a5f3fc09
Removed outdated comments
2016-01-19 11:11:30 -05:00
William J. Bowman
4ef32ff3fa
Fixed bug in docs
2016-01-19 11:07:57 -05:00
William J. Bowman
bf987cdb06
Better surface syntax. Closes #34
...
* Unified the surface syntax. There are no longer distinctions between
single-arity and multi-arity function/function types.
* Removed case and case*, in favor of match, a single advanced pattern
matching construct.
* Updated all libraries, tests and documentation to use these new syntax.
* Some work to provide improved error messages in surface syntax.
2016-01-18 14:14:05 -05:00
William J. Bowman
e162ef3acc
Documented list library
2016-01-13 21:14:54 -05:00
William J. Bowman
8c149fcef2
Fixed inductive elimination. Closes #33
...
Previously, inductive elimination could fail due to non-determinisic
matching in the reduction-relation and reduction over open terms via
reflection.
2016-01-13 21:00:04 -05:00
William J. Bowman
0596e4a0f6
[FAILING] Implemented list; found bug in elim
...
Implemented a list data type, but the tests revealed a bug in reducing
eliminators. Needs investigation.
2016-01-13 14:48:51 -05:00
William J. Bowman
ebdb419dd7
Changed oll to olly
2016-01-11 15:46:55 -05:00
William J. Bowman
792d37252f
Split and reorganized package. Closes #14
...
Created split packages: cur, cur-lib, cur-test, cur-doc, similar to
other Racket packages, e.g., redex.
* Moved tests out of core and into cur-test
* Moved docs into cur-doc
* Moved cur implementation and libraries into cur-lib
* Added cur meta-pacakge that installs all of the above
2016-01-10 19:10:12 -05:00
William J. Bowman
647229a577
'Fixed' some documentation issues caused #31
...
While the documentation renders correctly, only because imports are
hidden in the sandbox.
2016-01-09 14:37:20 -05:00
William J. Bowman
35f12827fe
More namespace hacks for REPLs
...
REPL namespace hack seems to have broken; partially repaired it will
more hacks, but still broken. see #31
2016-01-09 04:29:48 -05:00
William J. Bowman
dbc3b057dc
Fixed typo in docs
2016-01-09 04:24:41 -05:00
William J. Bowman
8eb512ebcc
Documented new nat functions
2016-01-09 04:24:25 -05:00
William J. Bowman
1b01c48df5
Disabled some tests as they take took long to run
2016-01-09 04:24:05 -05:00
William J. Bowman
e03cbfc1e4
Added match documentation
2016-01-09 04:23:43 -05:00
William J. Bowman
61e99c8a2e
Improvements to match; replacing uses of case
...
* Match now infers the result more by adding pattern variables to
local-env while inferring types.
* Replaced uses of case* and case with match when possible
2016-01-09 00:24:23 -05:00
William J. Bowman
7b10648eb9
Added optional arg to type-infer/syn for local env
...
Added undocumented feature to type-infer/syn. An optional argument can
be used to locally extend gamma attempting to infer the type.
2016-01-09 00:20:37 -05:00
William J. Bowman
63bbb50752
Exported new nat functions
2016-01-08 22:59:53 -05:00
William J. Bowman
691b01e15a
Added mult, exp; square via staging
2016-01-08 22:54:31 -05:00
William J. Bowman
ca2b62fc70
Fixed cur-equal?
2016-01-08 22:53:18 -05:00
William J. Bowman
c3efd3ae6e
Added better pattern matcher. Undocumented
...
Added match, a better pattern matching construct than case.
Automatically infers inductive arguments, and feature a "recur" syntax.
Converted several functions from stdlib/nat to use this.
2016-01-08 21:40:17 -05:00
William J. Bowman
8eaedabe3b
Fixed broken test caused by fix to Π dyn. sem.
2016-01-08 20:06:00 -05:00
William J. Bowman
15593e1c98
Fixed issues w/ α-equivalence tests and telescopes
2016-01-08 20:04:57 -05:00
William J. Bowman
cfa81e3508
Fixed issue with type-infer, application case
...
Application case was expecting type-infer to return a normal form.
This cannot be expected.
2016-01-08 19:52:18 -05:00
William J. Bowman
86a2e0d2ed
Renaming Σ to Δ
...
In dependent type system, Σ is normally the symbol for strong sums, not
signatures/declarations.
While Δ is sometimes used as an alternative to Γ, using it for
inductive signatures.
2016-01-08 19:52:18 -05:00
William J. Bowman
588d5b3758
[FAILS] Π-types cannot appears in app position
...
Not sure why I thought they coud; fixed, but some tests not
passing.
2016-01-08 19:48:20 -05:00
William J. Bowman
c978b2e45e
Bumped Redex version, trying to solve #30
2015-12-17 16:02:13 -05:00
William J. Bowman
b75d2ef5f4
Whitespace
2015-11-10 18:28:19 -05:00
William J. Bowman
27931803b0
More documentation
2015-11-10 18:24:38 -05:00
William J. Bowman
a57a719fdf
Fixed some issues with top-interactive
...
Previous, top-interactive was full of hacks and likely to break under
various scenarios. Now, it is less full of hacks and less likely to
break.
2015-11-10 17:57:32 -05:00
William J. Bowman
11f07080bd
More documentation
2015-11-10 16:30:46 -05:00
William J. Bowman
57ece3f787
More documentation fixes
2015-11-10 16:16:33 -05:00
William J. Bowman
2b69999380
Simplfied universe rules
...
Based on better understanding of universes and predicativity after
reading Luo's ECC work.
2015-11-10 14:11:46 -05:00
William J. Bowman
548b553e43
A little more docs for tactics
2015-11-10 13:42:04 -05:00
William J. Bowman
1b4ea69548
Documented bools
2015-11-10 13:41:43 -05:00
William J. Bowman
7624090e5a
Updated require Redex version
2015-10-28 15:50:14 -04:00
William J. Bowman
25e475e289
Merge branch 'redex-with-binding'
2015-10-28 15:49:17 -04:00
William J. Bowman
c3716bf3ad
Added strict positivity checker
...
Had to implement this for another reason, so added to cur core.
Closes #3
2015-10-25 01:18:48 -04:00
William J. Bowman
4ce0a9ba35
Disable deterministic reduction check
...
This check is overly aggressive and giving mostly false positives.
2015-10-09 12:04:09 -04:00
William J. Bowman
b050c4f192
Better error messages for let, in certain cases
2015-10-03 04:09:16 -04:00
