rosette-notes.txt (2811B)
1 2016-08-31 -------------------- 2 3 Rosette TODO: 4 - fix documentation of synthesize 5 - #:forall accepts everything, not just constant?s 6 7 2016-08-31 -------------------- 8 9 Adding typed define/debug, debug (from query/debug), render (from lib/query): 10 - revealed problems with the way Rosette tracks source locations 11 - in query/debug.rkt: https://github.com/emina/rosette/blob/cb877b9094f368c5f392518e7538ae8a061433a2/rosette/query/debug.rkt#L38 12 - specifically, make-variable-like-transformer does not preserve src loc 13 properly, see: https://github.com/emina/rosette/issues/40 14 15 Workaround: manually set the src loc in #%app to surface program 16 - this causes taint problems bc rosette #%app uses syntax-rules, which taints 17 its output, which causes problems when we try to destructure it 18 minimal example: 19 #lang racket 20 (require (for-syntax syntax/parse)) 21 (define-syntax-rule (mac x) 22 (#%app add1 x)) 23 (define-syntax test 24 (syntax-parser 25 [(_ x) 26 #:with e (local-expand #'(mac x) 'expression null) 27 (datum->syntax #'e (syntax-e #'e))])) 28 (test 1) 29 - calling syntax-disarm on the expanded pieces of a Rosette #%app appears to 30 prevent the taint errors 31 32 2016-08-29 -------------------- 33 34 Interesting parts of Typed Rosette 35 - only need a single U symbolic constructor 36 - assert-type, using cast-type and assertion store 37 38 2016-08-25 -------------------- 39 40 TODOs: 41 - add pred properties to types 42 - use it to validate given pred in define-symbolic 43 - STARTED 2016-08-25 44 - implement assert-type, which adds to the assertion store 45 - DONE 2016-08-25 46 - add polymorphism 47 - regular polymorphism 48 - extend BV type with a size 49 - requires BV-size-polymorpism? 50 - add Any type? 51 - STARTED 2016-08-26 52 - support internal definition contexts 53 - fix type of Vector and List to differentiate homogeneous/hetero 54 - variable arity polymorphism 55 - CSolution? 56 - make libs have appropriate require paths 57 - eg typed/rosette/query/debug 58 - make typed/rosette a separate pkg 59 - depends on macrotypes and rosette 60 - create version of turnstile that does not provide #%module-begin 61 - eg rename existing turnstile to turnstile/lang? 62 - remove my-this-syntax stx param 63 - add symbolic True and False? 64 - orig stx prop confuses distinction between symbolic and non-sym values 65 66 2016-08-25 -------------------- 67 68 ** Problem: 69 70 The following subtyping relation holds but is potentially unintuitive for a 71 programmer: 72 73 (U Int Bool) <: (U CInt Bool) 74 75 ** Possible Solutions: 76 1) leave as is 77 2) allow only symbolic arguments to user-facing U constructor 78 - user-facing U constructor expands to U** flattening constructor, 79 which then expands to internal U* constructor 80 - disadvantage: an if expression will expose the internal U** constructor, 81 since if may need to create a symbolic union from potentially concrete types 82 83 Choosing #1 for now.