www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

synthax.rkt (642B)

      1 #lang turnstile
      2 (require
      3  (only-in "../rosette2.rkt" rosette-typed-out)
      4  (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool C→ CSolution Unit))
      5  (prefix-in ro: rosette/lib/synthax))
      6 
      7 (provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)])
      8          ??)
      9 
     10 (define-typed-syntax ??
     11   [(qq) ≫
     12    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
     13    --------
     14    [⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
     15   [(qq pred : ty:type) ≫
     16    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
     17    [⊢ [pred ≫ pred- ⇐ : (t/ro:C→ ty.norm t/ro:Bool)]]
     18    --------
     19    [⊢ [_ ≫ (??/progsrc pred-) ⇒ : ty.norm]]])