suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
52 Commits 29 Branches 0 Tags 790 KiB
reflection
Commit Graph

52 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
William J. Bowman
b79e64523a Reflection, now with the ability to run code! 2015-01-30 17:55:09 -05:00
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