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

222 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
William J. Bowman
ba9bf0ee2b Fixed some broken comments 2015-03-24 20:13:42 -04:00
William J. Bowman
a468890817 Reduced complexity of substitution 2015-03-24 20:11:18 -04:00
William J. Bowman
807c4d7851 Added Type shorthand for tests 2015-03-23 17:39:02 -04:00
William J. Bowman
2ddf7ce352 Fixed several bugs, found several more 
Trying to fix proofs for free examples; found several bugs but more
still exist. Added TODOs
 2015-02-20 19:12:06 -05:00
William J. Bowman
6b0d09c7d9 Redex 1.6 enables caching of judgment forms! 
* Judgment form caching enables running test suite in seconds instead of
  days.
* Fixed numerous bugs after properly exercising the oll/stlc examples.
 2015-02-20 18:22:04 -05:00
William J. Bowman
b3388c5413 Changed Type to Unv 0 
* Type should be not be in the core language. Converted all uses of Type
  to Unv 0, potentially fixing a universe bug in the process.
* Added macro Type to Curnel that enables existing code to work more or
  less as before.
 2015-02-20 18:20:55 -05:00
William J. Bowman
38c1ac928a Cleaning up dead code 2015-02-20 09:55:35 -05:00
William J. Bowman
b2afc8f9d9 Bug fixes 2015-02-15 21:25:39 -05:00
William J. Bowman
410ee11cbe Fixed typo 2015-02-06 01:05:26 -05:00
William J. Bowman
af0b1a908f Fixed duplicate literal in syntax-parse 2015-02-05 12:35:44 -05:00
William J. Bowman
efcf8c1f97 Typo fixes 2015-02-05 02:39:25 -05:00
William J. Bowman
51972880b3 Note about the core, various fixes 2015-02-05 02:34:15 -05:00
William J. Bowman
027f031b20 Added some pointers about what to look at 2015-02-05 02:32:50 -05:00
William J. Bowman
b13bf6471d Fixed various typos/bug, added latex generation 2015-02-05 01:40:58 -05:00
William J. Bowman
448ee8a83a Added support for generating theorems,proofs,defs 
* cur-expand can now accept additional stop identifiers.
* Coq generator can now generate theorems, proofs, and definitions.
 2015-02-04 20:30:24 -05:00
William J. Bowman
999800d6f1 Can now translate case to match 2015-02-04 18:48:47 -05:00
William J. Bowman
be2fd4a6af Reorganized stdlib; fixed some tests 2015-02-04 18:47:15 -05:00
William J. Bowman
26ac41f104 Splitting modules and cleaning up; most tests pass 
* Split prop, nat, bool, maybe, and stlc into modules
* Reverted proofs-for-free stuff to the pre-me-fucking-about version,
  and cleaned it up.
* Fixed redex-curnel test suite. Redefinition of module+ was causing
  issues.
* Moved various var stuff to oll.
* Moved stlc examples to seperate module.
 2015-01-31 00:43:07 -05:00
William J. Bowman
116449ad44 Copied examples, added TODOs 2015-01-30 18:01:46 -05:00
William J. Bowman
a958056bbb Tweaked README 2015-01-30 17:57:16 -05:00
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