Stephen Chang
9f9294dc4c
reduce lens dependency to lens-common and lens-unstable
2017-01-25 14:18:13 -05:00
Stephen Chang
691ba9c51c
Turnstile forms no longer automatically provide; add type-out
...
- not auto-providing more closely adheres to idiomatic Racket
- this commit changes:
- define-typed-syntax
- removed #:export-as option
- define-base-type
- removed #:no-provide option
- define-type-constructor
- removed #:no-provide option
- type-out helps with providing defined types
- in examples, move define and define-type-alias to ext-stlc
- fix bug in reuse where renamed id not provided
2016-10-12 10:46:05 -04:00
Stephen Chang
fc5731de00
dont auto provide define-primops; add typed-out
2016-10-09 18:12:12 -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
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
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
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
Stephen Chang
268af37ff0
add stlc+union+case
2016-08-22 10:49:36 -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
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
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
Stephen Chang
6e7a8aedf3
fix rosette tests again
2016-07-19 16:27:38 -04:00
Stephen Chang
580ffdd1ac
add typed fsm forms except verification forms
2016-07-19 15:46:55 -04:00
Stephen Chang
6fdffbcb34
fix bv tests
2016-07-19 15:46:03 -04:00