Commit Graph

173 Commits

Author SHA1 Message Date
Stephen Chang
3ec2dfa431 drop [⊢ [e-stx]] ⇐-conclusion since it causes ambiguity and is undocumented 2016-10-05 10:32:53 -04:00
Stephen Chang
5296774b9a modify mlish app, lam and define to more closely resemble paper 2016-10-05 09:44:03 -04:00
Stephen Chang
0e0d4ce192 [docs] extend explanation of current-type-eval 2016-10-04 14:46:34 -04:00
Stephen Chang
7c68789628 convert mlish+adhoc define-instance to turnstile 2016-10-04 14:18:38 -04:00
Stephen Chang
80d0cec122 port rest of mlish+adhoc to turnstile 2016-10-04 13:44:22 -04:00
Stephen Chang
7113debd3c use more turnstile features in mlish+adhoc: define-type and match2 2016-10-03 18:41:43 -04:00
Stephen Chang
0d3b9b6550 [docs] add #:error conclusion 2016-10-03 16:01:36 -04:00
Stephen Chang
140843cf06 start move of mlish+adhoc to turnstile -- tests passing 2016-10-03 15:52:29 -04:00
Stephen Chang
b6a8d6bc95 add test-omit-paths 2016-10-03 15:45:46 -04:00
Stephen Chang
362b0f310d manually merge mlish.rkt from adhoc branch to mlish+adhoc.rkt 2016-10-03 14:28:15 -04:00
Stephen Chang
e8faad889b add τ= in addition to τ⊑ 2016-10-03 10:16:42 -04:00
AlexKnauth
41491136b6 put the guide and reference onto separate pages 2016-09-30 14:44:41 -04:00
AlexKnauth
0275d0143d use tc instead of inf and use . tc in the stx class 2016-09-30 14:07:07 -04:00
Stephen Chang
c78c085e60 [docs] dont include stx for-label 2016-09-30 12:53:21 -04:00
Stephen Chang
590c51bbac remove rosette dep; dont build rosette files 2016-09-30 12:51:38 -04:00
Stephen Chang
383634e14f polish and extend reference
- mention key in inf-elem
- specify phase of bindings
- add type=? examples
2016-09-30 12:09:37 -04:00
Stephen Chang
577f47f46a [docs] polish guide, add more examples 2016-09-30 11:10:23 -04:00
Ben Greenman
ffa0a05e26 [scribblings] respond to comments on PR #29
- add `#lang turnstile` to Sec 2.7
- use eval:error in @examples[]
- remove @literal
2016-09-30 10:14:03 -04:00
Ben Greenman
9116cfd5a2 [scribblings] typos & minor fixes to docs 2016-09-29 18:13:14 -04:00
Stephen Chang
e308dad709 add more #:no-provide options; add eval'ed doc examples
- cant get scribble/example to automatically catch and print type errs
2016-09-29 16:04:47 -04:00
Stephen Chang
df4c26dd8d type=? handles binding types by default
- closes #32
2016-09-29 14:27:17 -04:00
Stephen Chang
cf619325a6 docs: add authors 2016-09-29 10:47:17 -04:00
Stephen Chang
384e4962cd docs: better link for stx template 2016-09-26 14:48:30 -04:00
Stephen Chang
2b6c1964c8 docs: fix remaining broken links; add some stx util fns 2016-09-26 14:38:16 -04:00
Stephen Chang
8183efe1a6 fix broken techlinks 2016-09-26 14:26:51 -04:00
Stephen Chang
7dd277e814 docs: add extends and reuse 2016-09-26 13:03:09 -04:00
Stephen Chang
8a3f3f5e38 docs: revise guide to incorporate predeclared forms 2016-09-26 12:56:44 -04:00
Stephen Chang
853ef3f897 docs: update reference with predeclared forms 2016-09-26 12:21:00 -04:00
Stephen Chang
b898e255a5 docs: add #:export-as option in define-typed-syntax 2016-09-26 10:46:37 -04:00
Stephen Chang
94c7578ad6 docs: small reference edits 2016-09-26 10:46:37 -04:00
Stephen Chang
dc4f6d4466 add separate doc-utils file 2016-09-26 10:46:37 -04:00
Stephen Chang
f10190c26a docs: guide rough draft 2016-09-26 10:46:37 -04:00
Stephen Chang
e68480f0e6 docs: reference rough draft 2016-09-26 10:46:37 -04:00
Stephen Chang
e5cedb5c33 refactor guide and reference into separate files 2016-09-26 10:46:37 -04:00
Stephen Chang
1761c452cc docs: add introduction draft 2016-09-26 10:46:37 -04:00
AlexKnauth
ad9c33ac32 more work on docs 2016-09-26 10:46:37 -04:00
AlexKnauth
1e9f9025ad start on documentation 2016-09-26 10:46:37 -04:00
Stephen Chang
df63a0bf57 predefine "type" stx-category and define-primop in typecheck.rkt (and turnstile) 2016-09-24 16:43:17 -04:00
Stephen Chang
088635c33a check define-typed-stx has > 0 clauses to match stx-parse; add other paper abbrvs 2016-09-24 15:12:45 -04:00
Stephen Chang
d0c14c7e07 define-typed-syntax: support define-simple-macro-like single-clause syntax 2016-09-24 15:12:45 -04:00
Stephen Chang
bce55e8741 allow omitting "_ ≫" in conclusion 2016-09-24 15:12:45 -04:00
Stephen Chang
e1ea378f7d drop more parens 2016-09-24 15:12:45 -04:00
Stephen Chang
f545503d19 allow optionally eliding more parens
- single env
- \vdash rhs
2016-09-24 15:12:45 -04:00
AlexKnauth
ccdb667fac move default-type-eval into typecheck.rkt 2016-09-17 09:15:41 -04:00
AlexKnauth
a075b9b4f8 fix ~?Some pattern expander 2016-09-02 10:57:46 -04:00
AlexKnauth
a56250b26e start on tests from section 3 of the Guide 2016-08-31 18:59:54 -04:00
AlexKnauth
3d92dbdde3 add #lang turnstile/lang; change #lang turnstile's #%module-begin 2016-08-31 18:49:25 -04:00
Stephen Chang
98c5a6c231 support multiple exprs in let body; add set! 2016-08-31 16:57:23 -04:00
Stephen Chang
3f61c468be rename rosette-guide-tests -> rosette-guide-sec2-tests 2016-08-31 16:22:55 -04:00
Stephen Chang
5436f70de3 add remaining Rosette guide, sec2 examples 2016-08-31 16:22:08 -04:00
Stephen Chang
761645833d split Bool into True and False in stlc+union; add current-bitwidth to rosett2 2016-08-31 15:42:29 -04:00
Stephen Chang
af98a9dec9 add solve 2016-08-31 15:19:12 -04:00
Stephen Chang
90e9517b3a add synthesize and lib/synthax 2016-08-31 15:02:21 -04:00
Stephen Chang
60fa8ab91f fix syntax taint errs produced by srcloc workaround in #%app 2016-08-31 12:58:56 -04:00
Stephen Chang
10a143a16d add verify, evaluate; and debug, render in separate libs 2016-08-30 16:58:15 -04:00
Stephen Chang
2a6167e4d0 add immutable vectors; add "of" suffix to data structure type constructors 2016-08-30 11:41:40 -04:00
Stephen Chang
54c0ee1cb6 fix inf loop in current-sub?
- add more guide tests
2016-08-29 16:57:50 -04:00
AlexKnauth
513f6dcfd4 use type-cast and assert-pred for assert-type 2016-08-29 16:13:46 -04:00
Stephen Chang
1a14c5e377 add rosette-guide-tests; add various forms
- let-symbolic
- vector
- begin
2016-08-29 15:25:26 -04:00
AlexKnauth
98e5cdc77f add more assert-type tests 2016-08-29 11:26:22 -04:00
Stephen Chang
a9cf9cb217 add tests for assert-type; use new lifted bitvector? as BVPred "pred" stx prop 2016-08-26 17:01:48 -04:00
AlexKnauth
49fa6f5c38 add a lifted bitvector? predicate 2016-08-26 16:52:06 -04:00
Stephen Chang
d28893eb31 add Any; remove rosette1 dependencies 2016-08-26 15:15:49 -04:00
AlexKnauth
a2d702f221 add check-type+asserts 2016-08-26 14:28:08 -04:00
Stephen Chang
34ded75744 fix bv sdsl tests 2016-08-26 12:42:06 -04:00
AlexKnauth
eb3ff40404 convert bv.rkt to extend rosette2 2016-08-26 11:56:21 -04:00
Stephen Chang
d7ab2d0f29 add some forms required by bv sdsl: Param, let, define (no tests yet) 2016-08-26 11:11:15 -04:00
AlexKnauth
5df20847cb uncomment more tests 2016-08-25 17:00:05 -04:00
Stephen Chang
c3540ed7a9 add pred stx props and assert-type 2016-08-25 16:43:07 -04:00
AlexKnauth
25fa722acf uncomment more tests 2016-08-25 15:38:30 -04:00
Stephen Chang
32c13d9ae2 fix BVPred to not use old rosette version 2016-08-25 15:27:24 -04:00
Stephen Chang
9e2b2ddd3c add if and define-symbolic 2016-08-25 14:17:46 -04:00
AlexKnauth
e07f912cf7 rosette2: support more bv operations 2016-08-25 11:59:17 -04:00
AlexKnauth
6ee48d12a5 rosette2: start on bv operations 2016-08-25 11:38:20 -04:00
AlexKnauth
f3014ef2e7 rosette2: add sub1 and + 2016-08-25 11:09:58 -04:00
AlexKnauth
cc27c76ab8 rosette2: support applying symbolic function types 2016-08-25 10:07:00 -04:00
AlexKnauth
9743656778 rosette2: support applying Ccase-> functions 2016-08-25 09:53:22 -04:00
AlexKnauth
add4a2d7d5 more work on rosette2 2016-08-24 19:42:03 -04:00
Stephen Chang
b30a1a9425 start rosette2 2016-08-24 16:54:55 -04:00
AlexKnauth
0eefdab628 add case-> to rosette 2016-08-24 15:27:04 -04:00
AlexKnauth
cddfdc0349 use flatten/depth-lens instead of stx-append*n-lens 2016-08-24 09:33:54 -04:00
Stephen Chang
268af37ff0 add stlc+union+case 2016-08-22 10:49:36 -04:00
Stephen Chang
efbf03c258 start stlc+union 2016-08-22 09:30:30 -04:00
Stephen Chang
bb74d26ddc start typed ifc 2016-08-22 09:25:01 -04:00
Stephen Chang
541c1e64a9 add list to typed rosette 2016-08-22 09:21:57 -04:00
Stephen Chang
8b81c93692 typed fsm lang uses choose from typed rosette 2016-08-22 09:21:55 -04:00
Stephen Chang
4e48285d7f add more fsm tests 2016-08-22 09:18:59 -04:00
Stephen Chang
abf74414f0 fix choose in typed fsm lang
- convert typed rosette and its langs to use rosette's #%module-begin
2016-08-22 09:18:52 -04:00
AlexKnauth
eacf9d50d0 support #:do and #:fail-when syntax-parse options 2016-08-18 17:08:16 -04:00
Stephen Chang
ebecdb663c allow arbitrary number of dashes in type rules
closes #23
2016-08-18 16:49:23 -04:00
Stephen Chang
6d99f352db allow single env, implies empty tvctx 2016-08-18 15:17:26 -04:00
Stephen Chang
aa0136cf29 make prop tag optional, defaults to : 2016-08-18 14:52:50 -04:00
AlexKnauth
e673527813 add #:attributes decleration 2016-08-18 13:15:29 -04:00
AlexKnauth
e9230e0ba3 remove square brackets around syntax-parse kws 2016-08-17 17:49:37 -04:00
AlexKnauth
2ddf45f8de remove brackets around e ≫ e- 2016-07-26 11:44:17 -04:00
AlexKnauth
dac08d9b15 support multiple ellipses on ind-clauses 2016-07-26 09:27:14 -04:00
AlexKnauth
d698bce58b refactor turnstile 2016-07-26 08:46:34 -04:00
AlexKnauth
b73857d151 support multiple ellipses in the rhs of turnstile clauses 2016-07-25 10:24:42 -04:00
Stephen Chang
a0bb758a42 use stx lenses from lens pkg instead of append-lens.rkt 2016-07-20 19:05:58 -04:00
Stephen Chang
3707d90531 enable use of define-type-alias in language implementations
- using \tau.norm in define-type-alias implementation causes
  "invalid type" errors when the file is compiled
2016-07-20 18:44:15 -04:00