suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Updated README

Browse Source
This commit is contained in:
William J. Bowman 2016-01-10 18:47:03 -05:00
parent f8b19801fd
commit 0a1a14b850
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 20 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
README.md
View File

@ -15,20 +15,30 @@ cur (plural curs)
Disclaimer
==========
Cur is currently under active hackery and is not fit for use for any
particular purpose. It is fraught with unreadable code, errors, and
hacks that should never have been written by a reasonable human being.
particular purpose. It is fraught with unreadable code, errors,
performance bugs, and hacks that should never have been written by a
reasonable human being.
These may or may not be fixed shortly.
Getting started
===============
Easy mode:
Install cur via `raco pkg install cur`.
Advanced mode:
Cur is actually distributed as several packages.
`cur-lib` provides the implementation and all standard
libraries.
`cur-doc` provides the documentation.
`cur-test` provides a test suite and examples.
Try it out: open up DrRacket and put the following in the definition area:
```racket
#lang cur
(require
(require
cur/stdlib/bool
cur/stdlib/nat)
@ -44,27 +54,20 @@ Try entering the following in the interaction area:
See the docs: `raco docs cur`.
Most of the standard library is currently undocumented, so just see the source.
Going further
=============
Open up `examples/example.rkt` to see a tour of Cur's features.
Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
Open up `oll.rkt` to see the implementation of the meta-programs used to
enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
syntax, and Coq and LaTeX generators.
Open up `cur-tests/cur/tests/stlc.rkt` to see an example of the
simply-typed lambda-calculus modeled in Cur, with a parser and syntax
extension to enable deeply embedding.
Open up `examples/proofs-for-free.rkt` to see an implementation of the
translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program.
Open up `stdlib/tactics` to see tactics, implemented entirely via
meta-programming.
Open up `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
Open up anything in `stdlib/` to see some standard dependent-type
Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
formalisms.
Open up `curnel/redex-core.rkt` to see the entire "trusted" (after a
large test suite) core.
Open up `cur-lib/cur/curnel/redex-core.rkt` to see the entire
implementation of the core language, <600 lines of code.