Powerful meta-programming for powerful types.

Go to file

William J. Bowman 024f4e188e Fixed reduction of (elim ==) Fixed eliminator reduction, at least for the == type. Code currently does the minimum required to make #23 work, but may have introduced bugs in the process.		2015-09-26 00:57:36 -04:00
curnel	Fixed reduction of (elim ==)	2015-09-26 00:57:36 -04:00
examples	Updated documentation and examples to new elim	2015-09-25 17:50:03 -04:00
lang	cur is now a pkg and a #lang	2015-09-16 12:25:22 -04:00
scribblings	Added query-type command to sugar	2015-09-25 20:08:07 -04:00
stdlib	Fixed reduction of (elim ==)	2015-09-26 00:57:36 -04:00
.gitignore	cur is now a pkg and a #lang	2015-09-16 12:25:22 -04:00
cur.rkt	Added top-interactive support/fixed top-level eval	2015-09-22 14:06:03 -04:00
info.rkt	Added missing dependency	2015-09-22 15:30:00 -04:00
LICENSE	Updated LICENSE to BSD 2-clause	2015-09-15 16:12:15 -04:00
oll.rkt	Fixed coq generator for elim	2015-09-25 18:08:20 -04:00
README.md	Tweaks to README	2015-09-23 21:41:04 -04:00

README.md

cur

A language with static dependent-types and dynamic types, type annotations and parentheses, theorem proving and meta-programming.

Noun
cur (plural curs)

1. (archaic) A mongrel.
2. (archaic) A detestable person.

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. These may or may not be fixed shortly.

Getting started

Install cur via raco pkg install cur.

Try it out: open up DrRacket and put the following in the definition area:

#lang cur
(require 
 cur/stdlib/bool
 cur/stdlib/nat)

(if true
    false
    true)

Try entering the following in the interaction area:

(sub1 (s (s z)))

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 examples/proofs-for-free.rkt to see an implementation of the translation defined in Proofs for Free as a meta-program.

Open up stdlib/tactics to see tactics, implemented entirely via meta-programming.

Open up anything in 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.