William J. Bowman
ed57d034dc
Updated documentation
2016-01-18 14:03:42 -05:00
William J. Bowman
c3f5719b30
Removed implementation of case & case*
2016-01-18 14:03:33 -05:00
William J. Bowman
2fcba80950
Fixed use of case*, added TODO about things
2016-01-18 12:10:13 -05:00
William J. Bowman
04619e1f0b
Removed case and case* exports
2016-01-18 11:52:01 -05:00
William J. Bowman
174e4560d1
All tests pass! Sugar simplified
2016-01-18 11:48:51 -05:00
William J. Bowman
d48a5a0647
Advanced match!
...
Advanced match now works in all stdlib. case and case* deprecated.
2016-01-18 00:22:28 -05:00
William J. Bowman
b52dca0114
[Buggy] Partially fixed match on type familes.
...
Fixed various application syntax bugs in match.
Match still fails to infer the correct motive on type familes.
This is due to indices being instantiated differently between motive and
match clause.
2016-01-17 17:31:33 -05:00
William J. Bowman
09f47481ab
Fixing redex-lang to aid in debugging
2016-01-17 17:28:57 -05:00
William J. Bowman
ceb2a1aefc
[Untested] Fixed advanced version of match.
...
Need to start testing/converting stdlib, replacing case and case*
2016-01-15 18:29:10 -05:00
William J. Bowman
6820c07cd1
[Broken?] Advanced match
...
Right now, there are two pattern-matching-esque constructs.
Match is the better one, but fails often.
Time to improve it via syntax parse, more inferrence, and optional
arguments.
However, currently some of these changes seem to conflict with how the
redex-core works.
2016-01-15 17:14:20 -05:00
William J. Bowman
8d46cbf206
Converted cur-lib to simpler sugar
2016-01-15 17:12:39 -05:00
William J. Bowman
df741faa83
Simplifying the syntax sugar
...
Right now, the syntax sugar provided by Cur is instructive, but annoying
to use.
Time to make it easier to use.
2016-01-15 16:32:08 -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
William J. Bowman
b853d49b31
Fixed some tactic docs; tests that print to stdout
2015-10-03 03:55:22 -04:00
William J. Bowman
822c114f62
Fixed prop; removed define-theorem and qed macros
...
These macros were not really serving a good purpose. They were defined
early on to demonstrate that metaprogramming can give us Coq-like
notation, but really, we have much more interesting demos.
2015-10-03 03:33:12 -04:00
