debug.rkt (1141B)
1 #lang turnstile 2 (require 3 (prefix-in t/ro: (only-in "../rosette2.rkt" 4 λ ann begin C→ Nothing Bool CSolution)) 5 (prefix-in ro: rosette/query/debug)) 6 7 (provide define/debug debug) 8 9 (define-typed-syntax define/debug #:datum-literals (: -> →) 10 [(_ x:id e) ≫ 11 [⊢ [e ≫ e- ⇒ : τ]] 12 #:with y (generate-temporary #'x) 13 -------- 14 [_ ≻ (begin- 15 (define-syntax- x (make-rename-transformer (⊢ y : τ))) 16 (ro:define/debug y e-))]] 17 [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫ 18 ; [⊢ [e ≫ e- ⇒ : ty_e]] 19 #:with f- (generate-temporary #'f) 20 -------- 21 [_ ≻ (begin- 22 (define-syntax- f 23 (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out)))) 24 (ro:define/debug f- 25 (t/ro:λ ([x : ty] ...) 26 (t/ro:ann (t/ro:begin e ...) : ty_out))))]]) 27 28 (define-typed-syntax debug 29 [(_ (solvable-pred ...+) e) ≫ 30 [⊢ solvable-pred ≫ solvable-pred- ⇐ (t/ro:C→ t/ro:Nothing t/ro:Bool)] ... 31 [⊢ [e ≫ e- ⇒ : τ]] 32 -------- 33 [⊢ [_ ≫ (ro:debug (solvable-pred- ...) e-) ⇒ : t/ro:CSolution]]]) 34