William J. Bowman
8e768a7029
Require/provide now export/import gamma and sigma
2015-01-30 16:33:22 -05:00
William J. Bowman
434c1aa72b
Progress: module+ works, require/provide not yet.
2015-01-30 03:31:29 -05:00
William J. Bowman
59aff98158
Merge branch 'reflection' into cross-modules
2015-01-29 22:47:12 -05:00
William J. Bowman
e1ceb8a7d8
Renamed more curnels
2015-01-29 22:46:53 -05:00
William J. Bowman
d4aeb944e3
Merge branch 'master' into cross-modules
2015-01-29 22:45:03 -05:00
William J. Bowman
c537287df4
Merge branch 'master' into reflection
2015-01-29 22:44:55 -05:00
William J. Bowman
ec95026066
Renamed kernel to curnel. An important pun.
2015-01-29 22:44:30 -05:00
William J. Bowman
7170ed2496
Started cross-module work
2015-01-29 18:26:38 -05:00
William J. Bowman
8396165665
Typo in the README
2015-01-29 15:53:58 -05:00
William J. Bowman
fc93df8e40
Tweaking the README
2015-01-29 15:53:57 -05:00
William J. Bowman
0bb4dbbed2
Fixed README indentation
2015-01-29 15:53:56 -05:00
William J. Bowman
b0e350885a
Typo in the README
2015-01-28 23:45:23 -05:00
William J. Bowman
2e7dca5e4b
Tweaking the README
2015-01-28 23:42:55 -05:00
William J. Bowman
14b3b8eac7
Fixed README indentation
2015-01-28 20:19:25 -05:00
William J. Bowman
1c94591c27
Fixed various errors in expansion
...
* Expansion now proceeds correctly on all examples, although reduction
does not
* Drastically reorganized how wrapper work.
* Added/remove TODOs
2015-01-28 19:56:50 -05:00
William J. Bowman
8349ed1184
Shrinking core, added reflection tools
...
* Removed auto currying from core. These are now provided by sugar.
* Exposed type-infer, type-check, and normalize
* Attempting to track down strange bugs regarding local-expand
2015-01-28 15:27:20 -05:00
William J. Bowman
c7879c5b4c
Trying to fix bizarre issue with expand.
...
Sometimes (expand '((and P) Q)) causes an error. But not always. Can't
figure out why.
2015-01-28 00:41:53 -05:00
William J. Bowman
c24650ef01
Started work to enable reflection
...
* sigma, gamma extended at expand time
* All type-checking happens at expand time
* Locally expand all forms into core redex forms. However, this seems to
be causing problems. Probably not controlling expansion just right.
2015-01-27 23:55:50 -05:00
William J. Bowman
96f9343029
Reorganizing "pltools" to be more suggestive
2015-01-27 19:10:54 -05:00
William J. Bowman
9ebc1723c6
Renamed project to cur. tehe
2015-01-27 19:07:17 -05:00
William J. Bowman
0198b39f38
Added TODO, made example cleaner
2015-01-23 01:34:26 -05:00
William J. Bowman
bd31f51f64
Removed literals, Tweaked input syntax/tested
2015-01-23 01:16:21 -05:00
William J. Bowman
0a5568b78c
Fixed hygeine issues in define-language
...
* Now data gets properly defined!
* Export begin from redex-core.
* Added nat, needed by pltools.
2015-01-23 01:09:06 -05:00
William J. Bowman
69711620db
Added define-language macro
...
* Added the define-language form, which parses a BNF grammar and creates
a bunch of inductives. It is mostly finished, but doesn't yet work.
2015-01-23 00:14:21 -05:00
William J. Bowman
d508d9bcff
Started factoring into libraries.
2015-01-22 12:37:48 -05:00
William J. Bowman
f4a47cc7d6
Added coq code generator
2015-01-21 18:34:09 -05:00
William J. Bowman
6a29a1e4ef
stlc type system in new syntax, fixed import
...
* Finished the STLC type system in the new syntax!
* Fixed import/export of syntax/parse in redex-core
2015-01-21 09:55:43 -05:00
William J. Bowman
94926a42ee
Export all syntax-parse
2015-01-21 01:38:41 -05:00
William J. Bowman
9ec162b079
Added untested macro for defining inferrence rules
2015-01-21 01:37:50 -05:00
William J. Bowman
b57f2d4a85
STLC now works! Or, type-checks.
2015-01-20 00:56:18 -05:00
William J. Bowman
124531e3c2
Added TODOs of various new features
...
* Added description of new reflection features
* Cleaned up assorted comments
2015-01-20 00:55:37 -05:00
William J. Bowman
aaec536cf5
Fixed bad calls to terminates?
2015-01-20 00:55:23 -05:00
William J. Bowman
f94894aacf
Draft of STLC with type system
...
* STLC + syntax for writing STLC terms naturally, without explicitly
applying inductive constructors.
* Complete STLC type system, although it's not quite correct yet.
2015-01-19 20:45:18 -05:00
William J. Bowman
862d530b42
Added TODO about define/environments
2015-01-19 20:30:22 -05:00
William J. Bowman
de202fa6a0
Added plus, fixed some comments
2015-01-19 20:20:25 -05:00
William J. Bowman
c359631268
Added fix, without termination checking
...
Can now write recursive functions. Fix will probably change as I add
termination checking.
2015-01-19 20:15:55 -05:00
William J. Bowman
ec38e652a7
Started modeling STLC
2015-01-19 13:15:16 -05:00
William J. Bowman
48360533b1
Added better case syntax, better thm/qed macros
2015-01-16 23:24:56 -05:00
William J. Bowman
89c5c1ba68
Fixed various bugs related to case and inductives
...
case would fail when used on an inductive family. Fixed this, added more
test cases, and cleaned up examples.
2015-01-16 22:54:35 -05:00
William J. Bowman
a5358575f3
Fixed to well-formed env, tinkering with PFF
2014-08-01 16:54:37 +02:00
William J. Bowman
ff4bd337fb
Added implementation of proofs for free extension
...
* Implemented the dual-mode extension to proofs for free, complete with
a neat theorem.
2014-07-28 18:25:42 +02:00
William J. Bowman
58619df30b
Serious reorganization of examples file
2014-07-28 18:25:28 +02:00
William J. Bowman
2c6daa6224
Fixed missing universe rule
2014-07-28 18:25:28 +02:00
William J. Bowman
5d2988adf0
Extensive examples, syntax extensions out of core
2014-07-25 13:53:14 +02:00
William J. Bowman
febe276569
Renamed to racket-cic; language are cic*
2014-07-22 21:25:55 +02:00
William J. Bowman
754a32a3ea
Module language, positivity checking, more tests
...
* redex-core is now a module language, complete with fancyness. For
documentation, TODO.
* Added examples file using the module language.
2014-07-22 21:20:35 +02:00
William J. Bowman
176f08dd92
Added inductive types; assorted fixes
...
* Fixed variable typing; weakening is no longer a rule but built into
lookup logic.
* Fixed substitution.
2014-07-16 18:51:02 +02:00
William J. Bowman
944e9690dc
Fixed rule names, working on type inference
2014-07-12 23:46:02 +02:00
William J. Bowman
0b004d9ccb
Added type reduction and infer-core
...
* Can't get β-equiv rule to work, so normalize types then check.
* Added infer-core, a closer to surface language on which to do
inference.
2014-07-12 22:28:57 +02:00
William J. Bowman
7179e30fe1
Removed annotation from core language
2014-07-12 22:28:06 +02:00
