William J. Bowman
14960fd038
More quasisyntax/loc for better error messages
2016-01-21 16:07:16 -05:00
William J. Bowman
cc502671a6
[FAILING] Fixing design and running tests
...
Fixed up some of the design and started testing.
2016-01-21 15:14:13 -05:00
William J. Bowman
83fb144c24
[UNTESTED, DESIGN BUGS] Design for typed macros
...
Started working on a promising design for lifting type checking into the
macros for easy syntax extensions over the typed language. Works on some
examples, but running into performance issues and haven't
tested/finished design.
2016-01-20 17:52:37 -05:00
William J. Bowman
76933bd3b1
Fixed coq->cur to setup local-env, tweaked ->
...
* Fixed up coq->cur to track local-env while expanding.
* Tweaked -> to give better error messages
2016-01-19 16:57:17 -05:00
William J. Bowman
87bc0e44bc
[FAILING] cur-lib builds, tests fail
...
New application macro requires many extensions to manually keep up the
term environment while expanding/running code at compile-time.
This is not unreasonable, but does require some more changes.
2016-01-19 15:32:03 -05:00
William J. Bowman
b52ae2617b
Better error messages for application
2016-01-19 14:25:51 -05:00
William J. Bowman
961a5b7bb9
Rewrote Olly
...
Olly is now properly designed. This also fixes some issues with binding,
i.e. fixes #32 , and extraction to Coq and Latex
Makes progress on #9 .
2016-01-19 11:23:49 -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
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
William J. Bowman
4cae9688fb
Fix inner-expand bug, changed type error output
...
* Fix inner-expand? issue which could prevent type-checking terms
properly.
* No longer print out gamma and sigma when type checking fails
2015-10-03 03:31:27 -04:00
