;;;;; Stateful Contracts for Affine Types
;;;;; Jesse Tov and Riccardo Pucella

;; This appears to require PLT Scheme 4.1.4.2.
;; It doesn't work in 4.1.4.  (Sorry.)

;;
;; A multi-language calculus with two type systems:
;;  - Conventional simple types ("Conventional")
;;  - Simple types with one-shot functions ("Affine")
;; The type systems mix at the level of modules -- that is, each module
;; is written in one language or the other, and there is a main expression
;; in the unlimited language.
;;
;; This models a slightly older version of the calculus than is
;; in the paper -- mainly, it doesn't have polymorphism.
;;

#lang scheme

(require redex)
(require srfi/1)
(require (for-syntax scheme/base stxclass))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Examples from the paper ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; Try (check ex1) or (run ex1).

;; A Type-Correct Blame-Free Program
(define ex1
  (term (((module A (ap : ((int -1o int) -+o (int -1o int)))
            (lambda (f : (int -1o int))
              (lambda (x : int)
                (f x))))
          (module A (inc : (int -+o int))
            (lambda (y : int)
              ((ap (lambda (z : int) (succ z))) y))))
         (inc 5))))

;; An Ill-Typed A Module (type error)
(define ex2
  (term (((module A (ap : ((int -1o int) -+o (int -1o int)))
            (lambda (f : (int -1o int))
              (lambda (x : int)
                (f x))))
          (module A (inc2 : (int -+o int))
            (lambda (y : int)
              (let [g (ap (lambda (z : int) (succ z)))]
                (g (g y))))))
         (inc2 5))))

;; A Blameworthy C Module (blame inc2)
(define ex3
  (term (((module A (ap : ((int -1o int) -+o (int -1o int)))
            (lambda (f : (int -1o int))
              (lambda (x : int)
                (f x))))
          (module C (inc2 : (int -> int))
            (lambda (y : int)
              (let [g (ap (lambda (z : int) (succ z)))]
                (g (g y))))))
         (inc2 5))))

;; The C Module, Corrected
(define ex4
  (term (((module A (ap : ((int -1o int) -+o (int -1o int)))
            (lambda (f : (int -1o int))
              (lambda (x : int)
                (f x))))
          (module C (inc2 : (int -> int))
            (lambda (y : int)
              (let [g (ap (lambda (z : int) (succ z)))]
                (let [h (ap (lambda (z : int) (succ z)))]
                  (h (g y)))))))
         (inc2 5))))

;; A Call from A into C
(define ex5
  (term (((module C (ap : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x))))
          (module A (inc : (int -+o int))
            (lambda (y : int)
              ((ap (lambda (z : int) (succ z))) y))))
         (inc 5))))

;; An Ill-Typed A-to-C Call (type error)
(define ex6
  (term (((module C (ap : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x))))
          (module A (inc : (int -+o int))
            (lambda (y : int)
              ((lambda (g : (int -1o int))
                 ((ap g) y))
               (lambda (z : int) (succ z))))))
         (inc 5))))

;; An Interface Module Intervenes
(define ex7
  (term (((module C (ap : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x))))
          (interface (iap :> ((int -1o int) -+o (int -1o int))) ap)
          (module A (inc : (int -+o int))
            (lambda (y : int)
              ((lambda (g : (int -1o int))
                 ((iap g) y))
               (lambda (z : int) (succ z))))))
         (inc 5))))

;; A Lying Interface Module (blame iap2)
(define ex8
  (term (((module C (ap2 : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f (f x)))))
          (interface (iap2 :> ((int -1o int) -+o (int -1o int))) ap2)
          (module A (inc : (int -+o int))
            (lambda (y : int)
              ((lambda (g : (int -1o int))
                 ((iap2 g) y))
               (lambda (z : int) (succ z))))))
         (inc 5))))

;; Syntax for the source languages.
(define-language affine
  ;; A program
  (P     (M ec))
  ;; A declaration
  (M     (m ...))
  ;; Modules
  (m     mc  ;; conventional module
         ma  ;; affine module
         mi) ;; interface module
  ;; Qualifiers
  (Q     U
         A)
  
  ;; An interface module
  (mi    (interface (f :> ta^u) f))
  
  ;; The conventional language:
  (mc    (module C (f : tc) vc))
  (tc    int
         (tc * tc)
         (tc -> tc)
         (ta^o aff))
  (vc    cc
         (cons vc vc)
         (lambda (x : tc) ec))
  (ec    vc
         x
         (ec ec)
         (if0 ec ec ec)
         (let [x ec] ec)
         (cons ec ec)
         (let [(cons x x) ec] ec))
  (cc    n
         pred
         succ
         -)
  ;; Bindings and environments
  (Bc    (x : tc))
  (Gc    (Bc ...))

  ;; The affine language  
  (ma    (module A (f : ta^u) va))
  (ta    ta^a
         ta^u)
  ;; Unlimited types
  (ta^u  int
         (ta -+o ta)
         (ta^u * ta^u))
  ;; Affine types
  (ta^a  (ta ref)
         (ta -1o ta)
         (ta^a * ta)
         (ta * ta^a))
  ;; Opaque types
  (ta^o  (ta ref)
         (ta^a * ta)
         (ta * ta^a))
  (-*o   -+o
         -1o)
  (va    ca
         (cons va va)
         (lambda (x : ta) ea))
  (ea    va
         x
         (ea ea)
         (if0 ea ea ea)
         (let [x ea] ea)
         (cons ea ea)
         (let [(cons x x) ea] ea))
  (ca    n
         pred
         succ
         -
         [new ta]
         [swap ta ta])

  ;; Bindings and environments
  (Ba    (x : ta))
  (Ga    (Ba ...))

  ;; Common to both languages:
  ;; Variables / module names
  ((x y f g)
         variable-not-otherwise-mentioned)
  ;; Numeric constants
  (n     number)
  
  ;; Partial orders are defined on Q and ta
  (PO    Q
         ta)
  ;; Booleans (used as the result of some metafunctions)
  (boolean
         #t
         #f)
  
  ; Convenience:
  ;; Two kinds of arrows:
  (-*    -o
         ->))

;;;;;
;;;;; THE TYPE SYSTEM
;;;;;

;;;
;;; Types, subtyping, and environments
;;;

;; We define a lattice on qualifiers:
;;   A
;;   |
;;   U

(define-metafunction affine
  ta->Q : ta -> Q
  [(ta->Q ta^u)      U]
  [(ta->Q ta^a)      A])

;; We define a partial order on types, which gives a subtyping relation
;; under which unlimited functions may be used where an affine function
;; is allowed/expected.
(define-metafunction affine
  lub : PO PO -> PO
  ;; For ta:
  [(lub int int)
   int]
  [(lub (ta ref) (ta ref))
   (ta ref)]
  [(lub (ta_1 * ta_2) (ta_3 * ta_4))
   ((lub ta_1 ta_3) * (lub ta_2 ta_4))]
  [(lub (ta_1 -+o ta_2) (ta_3 -+o ta_4))
   ((glb ta_1 ta_3) -+o (lub ta_2 ta_4))]
  [(lub (ta_1 -+o ta_2) (ta_3 -1o ta_4))
   ((glb ta_1 ta_3) -1o (lub ta_2 ta_4))]
  [(lub (ta_1 -1o ta_2) (ta_3 -+o ta_4))
   ((glb ta_1 ta_3) -1o (lub ta_2 ta_4))]
  [(lub (ta_1 -1o ta_2) (ta_3 -1o ta_4))
   ((glb ta_1 ta_3) -1o (lub ta_2 ta_4))]
  
  ;; For Q:
  [(lub U   U)
   U]
  [(lub Q_1 Q_2)
   A])

(define-metafunction affine
  glb : PO PO -> PO
  ;; For ta:
  [(glb int int)
   int]
  [(glb (ta ref) (ta ref))
   (ta ref)]
  [(glb (ta_1 * ta_2) (ta_3 * ta_4))
   ((glb ta_1 ta_3) * (glb ta_2 ta_4))]
  [(glb (ta_1 -+o ta_2) (ta_3 -+o ta_4))
   ((lub ta_1 ta_3) -+o (glb ta_2 ta_4))]
  [(glb (ta_1 -+o ta_2) (ta_3 -1o ta_4))
   ((lub ta_1 ta_3) -+o (glb ta_2 ta_4))]
  [(glb (ta_1 -1o ta_2) (ta_3 -+o ta_4))
   ((lub ta_1 ta_3) -+o (glb ta_2 ta_4))]
  [(glb (ta_1 -1o ta_2) (ta_3 -1o ta_4))
   ((lub ta_1 ta_3) -1o (glb ta_2 ta_4))]
  
  ;; For Q:
  [(glb A   A)
   A]
  [(glb Q_1 Q_2)
   U])

;; Our partial order's less-than relation gives subsumption: if (<: ta_1 ta_2)
;; then a term of type ta_1 may be used where ta_2 is expected.
(define-metafunction affine
  <: : PO PO -> boolean
  [(<: PO_1 PO_2)
   ,(equal? (term PO_2) (term (lub PO_1 PO_2)))])


;; We need to project affine types down to unlimited types, which gives us
;; the types that unlimited modules see when they refer to affine modules.
(define-metafunction affine
  ta->tc : ta -> tc
  [(ta->tc int)
   int]
  [(ta->tc (ta_1 -*o ta_2))
   ((ta->tc ta_1) -> (ta->tc ta_2))]
  [(ta->tc (ta^u_1 * ta^u_2))
   ((ta->tc ta^u_1) * (ta->tc ta^u_2))]
  [(ta->tc ta^o)
   (ta^o aff)])
  
;; We embed unlimited types back into affine types.
(define-metafunction affine
  tc->ta : tc -> ta
  [(tc->ta int)
   int]
  [(tc->ta (tc_1 * tc_2))
   ((tc->ta tc_1) * (tc->ta tc_2))]
  [(tc->ta (tc_1 -> tc_2))
   ((tc->ta tc_1) -+o (tc->ta tc_2))]
  [(tc->ta (ta^o aff))
   ta^o])
  
;; Add a binding to a type environment.  Removes any previous binding
;; for the same name, which makes lookup easier.
(define-metafunction affine
  bindc : Bc Gc -> Gc
  [(bindc (x : tc) (Bc_1 ... (x : tc_o) Bc_2 ...))
   (Bc_1 ... (x : tc) Bc_2 ...)]
  [(bindc (x : tc) (Bc_1 ...))
   ((x : tc) Bc_1 ...)])
(define-metafunction affine
  binda : Ba Ga -> Ga
  [(binda (x : ta) (Ba_1 ... (x : ta_o) Ba_2 ...))
   (Ba_1 ... (x : ta) Ba_2 ...)]
  [(binda (x : ta) (Ba_1 ...))
   ((x : ta) Ba_1 ...)])

;;;
;;; Decorating a program & run-time syntax
;;;

;; We add two kinds of decorations to source programs before we can
;; type-check and then reduce them:
;;  - Sharing analysis adds sharing annotations to each lambda- or let-bound
;; variable in the A language indicating its usage.  Qualifier A means that
;; variable can be given an affine type; U means it must be unlimited.
;;  - Each variable occurence is annotated with the module in which it
;; statically resides, which gives the negative party when a contract is
;; applied there.  We do it this way because we cannot at this stage
;; distinguish variables, native module calls, and foreign modules calls.
;;
;; On paper we consider these decorations to exist already.  On paper, we
;; avoid sharing analysis by using non-deterministic context splitting.

(define-extended-language affine-static affine
  (ea    ....
         (var x [f])
         (let [x[Q] ea] ea)
         (let [(cons x[Q] x[Q]) ea] ea))
  (va    ....
         (lambda (x[Q] : ta) ea))
  (ec    ....
         (var x [f]))
  
  ;; Environment for sharing analysis:
  (G/use ((x Q) ...)))

;; Decorating programs -- note that the type (P -> P) is deceptive --
;; this ought to take an undecorated P and produce a decorated P.
(define-metafunction affine-static
  decorate-program : P -> P
  [(decorate-program ((m ...) ec))
   (((decorate-m m) ...) (decorate-ec *main* ec))])

;; Decorate each kind of module:
(define-metafunction affine-static
  decorate-m : m -> m
  [(decorate-m (module C (f : tc) vc))
   (module C (f : tc) (decorate-ec f vc))]
  [(decorate-m (module A (f : ta) va))
   ,(*term-let affine-static
       ([(G/use va_*) (term (decorate-ea f va))])
     (term (module A (f : ta) va_*)))]
  [(decorate-m mi)
   mi])

(define-metafunction affine-static
  decorate-ec : f ec -> ec
  [(decorate-ec f ca)
   ca]
  [(decorate-ec f (lambda (x : tc) ec))
   (lambda (x : tc) (decorate-ec f ec))]
  [(decorate-ec f x)
   (var x [f])]
  [(decorate-ec f (ec_1 ec_2))
   ((decorate-ec f ec_1) (decorate-ec f ec_2))]
  [(decorate-ec f (if0 ec_1 ec_2 ec_3))
   (if0 (decorate-ec f ec_1)
        (decorate-ec f ec_2)
        (decorate-ec f ec_3))]
  [(decorate-ec f (let [x ec_1] ec_2))
   (let [x (decorate-ec f ec_1)]
     (decorate-ec f ec_2))]
  [(decorate-ec f (cons ec_1 ec_2))
   (cons (decorate-ec f ec_1)
         (decorate-ec f ec_2))]
  [(decorate-ec f (let [(cons x y) ec_1] ec2))
   (let [(cons x y) (decorate-ec f ec_1)]
     (decorate-ec f ec_2))])

;; Let's just do both decorations in a single pass:
(define-metafunction affine-static
  decorate-ea : f ea -> (G/use ea)
  [(decorate-ea f ca)
   (() ca)]
  [(decorate-ea f (lambda (x : ta) ea))
   ,(*term-let affine-static
       ([(G/use_1 ea_*) (term (decorate-ea f ea))]
        [(G/use_2 Q)    (term (<<->> G/use_1 x))])<
     (term (G/use_2 (lambda (x[Q] : ta) ea_*))))]
  [(decorate-ea f x)
   (((x A)) (var x [f]))]
  [(decorate-ea f (ea_1 ea_2))
   ,(*term-let affine-static
       ([(G/use_1 ea_1*) (term (decorate-ea f ea_1))]
        [(G/use_2 ea_2*) (term (decorate-ea f ea_2))])
     (term ((<<*>> G/use_1 G/use_2) (ea_1* ea_2*))))]
  [(decorate-ea f (if0 ea_1 ea_2 ea_3))
   ,(*term-let affine-static
       ([(G/use_1 ea_1*) (term (decorate-ea f ea_1))]
        [(G/use_2 ea_2*) (term (decorate-ea f ea_2))]
        [(G/use_3 ea_3*) (term (decorate-ea f ea_3))])
     (term ((<<*>> G/use_1 (<<+>> G/use_2 G/use_3))
            (if0 ea_1* ea_2* ea_3*))))]
  [(decorate-ea f (let [x ea_1] ea_2))
   ,(*term-let affine-static
       ([(G/use_1 ea_1*) (term (decorate-ea f ea_1))]
        [(G/use_2 ea_2*) (term (decorate-ea f ea_2))]
        [(G/use_2* Q)    (term (<<->> G/use_2 x))])
     (term ((<<*>> G/use_1 G/use_2*)
            (let [x[Q] ea_1*] ea_2*))))]
  [(decorate-ea f (cons ea_1 ea_2))
   ,(*term-let affine-static
       ([(G/use_1 ea_1*) (term (decorate-ea f ea_1))]
        [(G/use_2 ea_2*) (term (decorate-ea f ea_2))])
     (term ((<<*>> G/use_1 G/use_2) (cons ea_1* ea_2*))))]
  [(decorate-ea f (let [(cons x y) ea_1] ea_2))
   ,(*term-let affine-static
       ([(G/use_1 ea_1*) (term (decorate-ea f ea_1))]
        [(G/use_2 ea_2*) (term (decorate-ea f ea_2))]
        [(G/use_2* Q_x)  (term (<<->> G/use_2 x))]
        [(G/use_2** Q_y) (term (<<->> G/use_2* y))])
     (term ((<<*>> G/use_1 G/use_2**)
            (let [(cons x[Q_x] y[Q_y]) ea_1*] ea_2*))))])

;; Use-qualifier-environment multiplication.  This maps all variables found in either
;; environment, and maps those found in both to U.
(define-metafunction affine-static
  <<*>> : G/use G/use -> G/use
  [(<<*>> () G/use)
   G/use]
  [(<<*>> ((x Q_a) (x_r Q_r) ...) ((x_1 Q_1) ... (x Q_b) (x_2 Q_2) ...))
   (<<*>> ((x_r Q_r) ...)
          ((x_1 Q_1) ... (x (glb U (glb Q_a Q_b))) (x_2 Q_2) ...))]
  [(<<*>> ((x Q) (x_r Q_r) ...) ((x_1 Q_1) ...))
   (<<*>> ((x_r Q_r) ...) ((x Q) (x_1 Q_1) ...))])

;; Use-qualifier-environment addition.  This maps all variables found in either
;; environment, and maps those found in both to the weaker condition.
(define-metafunction affine-static
  <<+>> : G/use G/use -> G/use
  [(<<+>> () G/use)
   G/use]
  [(<<+>> ((x Q_a) (x_r Q_r) ...) ((x_1 Q_1) ... (x Q_b) (x_2 Q_2) ...))
   (<<+>> ((x_r Q_r) ...) ((x_1 Q_1) ... (x (glb Q_a Q_b)) (x_2 Q_2) ...))]
  [(<<+>> ((x Q) (x_r Q_r) ...) ((x_1 Q_1) ...))
   (<<+>> ((x_r Q_r) ...) ((x Q) (x_1 Q_1) ...))])

;; Remove a variable from a use environment and return its qualifier as
;; well.  If not present, it hasn't been used more then once, so it's A.
(define-metafunction affine-static
  <<->> : G/use x -> (G/use Q)
  [(<<->> ((x_1 Q_1) ... (x Q) (x_2 Q_2) ...) x)
   (((x_1 Q_1) ... (x_2 Q_2) ...) Q)]
  [(<<->> G/use x)
   (G/use A)])

;;; 
;;; Typechecking a program
;;;

(define-metafunction affine-static
  typecheck-program : P -> ((okay ...) tc)
  [(typecheck-program ((m ...) ec))
   (((typecheck-module M m) ...)
    (typecheck-c M () ec))
   (where M (m ...))])

;; To typecheck a module, we typecheck its body, and then check that the
;; type of the body is compatible with the declared type of the module.
;; For an unlimited module, compatibility is equality, but for an affine
;; module, the declared type may be stronger (greater) than the actual
;; type.
(define-metafunction affine-static
  typecheck-module : M m -> any
  [(typecheck-module M (module C (f : tc) vc))
   okay
   (side-condition (equal? (term tc) (term (typecheck-c M () vc))))]
  [(typecheck-module M (module A (f : ta^u) va))
   okay
   (side-condition (term (<: (typecheck-a M () va) ta^u)))]
  [(typecheck-module (m_1 ... (module C (g : tc) vc) m_2 ...)
                     (interface (f :> ta^u) g))
   okay
   (side-condition (equal? (term (ta->tc ta^u)) (term tc)))])


;;;
;;; Typechecking the U language
;;;

;; To find the type of an expression in the given environment, if possible.
(define-metafunction affine-static
  typecheck-c : M Gc ec -> tc
  ;; TC-Con
  [(typecheck-c M Gc cc)
   (typecheck-c-c cc)]
  ;; TC-Lam
  [(typecheck-c M Gc (lambda (x : tc) ec))
   (tc -> (typecheck-c M (bindc (x : tc) Gc) ec))]
  ;; TC-Var
  [(typecheck-c M (Bc_1 ... (x : tc) Bc_2 ...) (var x [f]))
   tc]
  ;; TC-Mod
  [(typecheck-c (m_1 ... (module C (f : tc) vc) m_2 ...) Gc (var f [g]))
   tc]
  ;; TC-ModA
  [(typecheck-c (m_1 ... (module A (f : ta^u) va) m_2 ...) Gc (var f [g]))
   (ta->tc ta^u)]
  ;; TC-App
  [(typecheck-c M Gc (ec_1 ec_2))
   (typecheck-c-app (typecheck-c M Gc ec_1)
                    (typecheck-c M Gc ec_2))]
  ;; TC-If0
  [(typecheck-c M Gc (if0 ec_1 ec_2 ec_3))
   (typecheck-c-if0 (typecheck-c M Gc ec_1)
                    (typecheck-c M Gc ec_2)
                    (typecheck-c M Gc ec_3))]
  ;; TC-LetVar
  [(typecheck-c M Gc (let [x ec_1] ec))
   (typecheck-c M (bindc (x : (typecheck-c M Gc ec_1)) Gc) ec)]
  ;; TC-Pair
  [(typecheck-c M Gc (cons ec_1 ec_2))
   ((typecheck-c M Gc ec_1) * (typecheck-c M Gc ec_2))]
  ;; TC-Let
  [(typecheck-c M Gc (let [(cons x y) ec_1] ec_2))
   (typecheck-c M (bindc-letpair x y (typecheck-c M Gc ec_1) Gc) ec_2)])

;; Helper function for applications: ensures that the formal argument type
;; matches the actual argument type, returning the result type.
(define-metafunction affine-static
  typecheck-c-app : tc tc -> tc
  [(typecheck-c-app (tc_1 -> tc_2) tc_1)
   tc_2])

;; Helper function for if0 expressions: ensures that the condition is an
;; integer and the two branches have the same type, which is the type of
;; the whole expression.
(define-metafunction affine-static
  typecheck-c-if0 : tc tc tc -> tc
  [(typecheck-c-if0 int tc tc)
   tc])

;; Helper to find the type of a constant in the unlimited language.
(define-metafunction affine-static
  typecheck-c-c : cc -> tc
  [(typecheck-c-c n)
   int]
  [(typecheck-c-c -)
   (int -> (int -> int))]
  [(typecheck-c-c succ)
   (int -> int)]
  [(typecheck-c-c pred)
   (int -> int)])

;; Helper to check destructuring let
(define-metafunction affine-static
  bindc-letpair : x y tc Gc -> Gc
  [(bindc-letpair : x y (tc_x * tc_y) Gc)
   (bindc (x : tc_x) (bindc (y : tc_y) Gc))])

;;;
;;; Type-checking the A language
;;;

;; To find the type of an affine expression.  This differs from how we
;; typecheck conventional expressions in three ways:
;;
;;  1. When a variable is bound to an affine type, we must
;;     ensure that the sharing analysis agrees that it is used at most once.
;;
;;  2. When a lambda closes over some affine values, the lambda itself must
;;     be given an affine (-1o) type; otherwise, it gets unlimited (-+o) type.
;;
;;  3. We compare types not for equality but subsumption, where necessary.

(define-metafunction affine-static
  typecheck-a : M Ga ea -> ta
  ;; TA-Con
  [(typecheck-a M Ga ca)
   (typecheck-a-c ca)]
  ;; TA-LamAff
  [(typecheck-a M Ga (name ea_l (lambda (x[Q] : ta) ea)))
   (ta -1o (typecheck-a M (binda (x : ta) Ga) ea))
   (side-condition (term (<: (ta->Q ta) Q)))
   (side-condition (term (<: A (max-use Ga (fv-a ea_l)))))]
  ;; TA-LamAff
  [(typecheck-a M Ga (lambda (x[Q] : ta) ea))
   (ta -+o (typecheck-a M (binda (x : ta) Ga) ea))
   (side-condition (term (<: (ta->Q ta) Q)))]
  ;; TA-Var
  [(typecheck-a M (Ba_1 ... (x : ta) Ba_2 ...) (var x [f]))
   ta]
  ;; TA-Mod
  [(typecheck-a (m_1 ... (module A (f : ta^u) va) m_2 ...) Ga (var f [g]))
   ta^u]
  ;; TA-ModC
  [(typecheck-a (m_1 ... (module C (f : tc) vc) m_2 ...) Ga (var f [g]))
   (tc->ta tc)]
  ;; TA-ModI
  [(typecheck-a (m_1 ... (interface (f :> ta^u) f_1) m_2 ...) Ga (var f [g]))
   ta^u]
  ;; TA-App
  [(typecheck-a M Ga (ea_1 ea_2))
   (typecheck-a-app (typecheck-a M Ga ea_1)
                    (typecheck-a M Ga ea_2))]
  ;; TA-If0
  [(typecheck-a M Ga (if0 ea_1 ea_2 ea_3))
   (typecheck-a-if0 (typecheck-a M Ga ea_1)
                    (typecheck-a M Ga ea_2)
                    (typecheck-a M Ga ea_3))]
  ;; TA-LetVar
  [(typecheck-a M Ga (let [x[Q] ea_1] ea))
   ,(*term-let affine-static
       ([ta_1 (term (typecheck-a M Ga ea_1))])
     (if (term (<: (ta->Q ta_1) Q))
         (term (typecheck-a M (binda (x : ta_1) Ga) ea))
         (error 'typecheck-a "Use qualifier too weak in LET")))]
  ;; TA-Pair
  [(typecheck-a M Ga (cons ea_1 ea_2))
   ((typecheck-a M Ga ea_1) * (typecheck-a M Ga ea_2))]
  ;; TA-Let
  [(typecheck-a M Ga (let [(cons x[Q_x] y[Q_y]) ea_1] ea))
   ,(*term-let affine-static
       ([(ta_x * ta_y) (term (typecheck-a M Ga ea_1))])
     (if (and (term (<: (ta->Q ta_x) Q_x))
              (term (<: (ta->Q ta_y) Q_y)))
         (term (typecheck-a M (binda (x : ta_x) (binda (y : ta_y) Ga)) ea))
         (error 'typecheck-a "Use qualifier too weak in LET")))])

;; Helper for checking applications.  We can apply both (->) and (-o)
;; functions, and the formal argument type need not match the actual
;; argument type exactly -- the actual argument may have a stronger type
;; than the function expects.
(define-metafunction affine-static
  typecheck-a-app : ta ta -> ta
  [(typecheck-a-app (ta_e -*o ta_r) ta_a)
   ta_r
   (side-condition (term (<: ta_a ta_e)))])

;; Helper for checking if0 expressions.  The types of the branches
;; need not match, as long as they have a least-upper-bound, which gives
;; the type of the whole expression.
(define-metafunction affine-static
  typecheck-a-if0 : ta ta ta -> ta
  [(typecheck-a-if0 ta_c ta_t ta_f)
   (lub ta_t ta_f)
   (side-condition (term (<: ta_c int)))])

;; Helper to find the type of a constant in the affine language.
(define-metafunction affine-static
  typecheck-a-c : ca -> ta
  [(typecheck-a-c n)
   int]
  [(typecheck-a-c -)
   (int -+o (int -+o int))]
  [(typecheck-a-c succ)
   (int -+o int)]
  [(typecheck-a-c pred)
   (int -+o int)]
  [(typecheck-a-c [new ta])
   (ta -+o (ta ref))]
  [(typecheck-a-c [swap ta_1 ta_2])
   (((ta_1 ref) * ta_2) -+o ((ta_2 ref) * ta_1))])

;; Fine the maximum of all the use qualifiers for a set of variables
;; with respect to a type environment.
(define-metafunction affine-static
  max-use : Ga (x ...) -> Q
  [(max-use Ga ())
   U]
  [(max-use (name Ga (Ba_1 ... (x : ta) Ba_2 ...)) (x x_r ...))
   (lub (ta->Q ta) (max-use Ga (x_r ...)))]
  [(max-use Ga (x x_r ...))
   (max-use Ga (x_r ...))])

;; To find the free variables of an expression.
(define-metafunction affine-static
  fv-a : ea -> (x ...)
  [(fv-a ca)
   ()]
  [(fv-a (lambda (x[Q] : ta) ea))
   ,(lset-difference eq? (term (fv-a ea)) (term (x)))]
  [(fv-a (var x [f]))
   (x)]
  [(fv-a (ea_1 ea_2))
   ,(lset-union eq? (term (fv-a ea_1)) (term (fv-a ea_2)))]
  [(fv-a (if0 ea_1 ea_2 ea_3))
   ,(lset-union eq? (term (fv-a ea_1)) (term (fv-a ea_2)) (term (fv-a ea_3)))]
  [(fv-a (let [x[Q] ea_1] ea))
   ,(lset-union eq?
                (term (fv-a ea_1))
                (lset-difference eq?
                                 (term (fv-a ea))
                                 (term (x))))]
  [(fv-a (cons ea_1 ea_2))
   ,(lset-union eq? (term (fv-a ea_1)) (term (fv-a ea_2)))]
  [(fv-a (let [(cons x[Q_x] y[Q_y]) ea_1] ea))
   ,(lset-union eq?
                (term (fv-a ea_1))
                (lset-difference eq?
                                 (term (fv-a ea))
                                 (term (x y))))])

;;;;;
;;;;; Run time
;;;;;

;; Run-time syntax

(define-extended-language affine* affine-static
  (Cfg   (M s ec))           ;; Configuration
  (s     (se ...))           ;; Store
  (se    (l = va)            ;; Store element (cell)
         (l = vc))
  (l     x)                  ;; Location
  
  (ea    ....
         (AC ta f f ec))     ;; Boundary
  (ec    ....
         (CA ta f f ea)      ;; Boundary
         (blame f any ...))
  (va    ....
         (ref l))            ;; Reference cell
  (vc    ....
         (CA [l] ta f f va)) ;; Sealed affine boundary
  
  (ca    ....
         (-/1 n))            ;; Partially-applied subtraction
  (cc    ....
         BLSSD
         DFNCT
         (-/1 n))            ;; Partially-applied subtraction
  
  ;; Evaluation contexts, including evaluation in the other
  ;; language.
  (Ea    hole
         (Ea ea)
         (va Ea)
         (if0 Ea ea ea)
         (let [x[Q] Ea] ea)
         (cons Ea ea)
         (cons va Ea)
         (let [(cons x[Q] x[Q]) Ea] ea)
         (AC ta f f Ec))
  (Ec    hole
         (Ec ec)
         (vc Ec)
         (if0 Ec ec ec)
         (let [x Ec] ec)
         (cons Ec ec)
         (cons vc Ec)
         (let [(cons x x) Ec] ec)
         (CA ta f f Ea))
  
  ;; Evaluation contexts without boundaries, guaranteeing that
  ;; the term in the hole is of the right sort.
  (E/ah  (in-hole Ec (CA ta f f Ea/no-boundary)))
  (E/ch  (in-hole Ec (AC ta f f Ec/no-boundary))
         Ec/no-boundary)
  (Ea/no-boundary
         hole
         (Ea/no-boundary ea)
         (va Ea/no-boundary)
         (if0 Ea/no-boundary ea ea)
         (let [x[Q] Ea/no-boundary] ea)
         (cons Ea/no-boundary ea)
         (cons va Ea/no-boundary)
         (let [(cons x[Q] x[Q]) Ea/no-boundary] ea))
  (Ec/no-boundary
         hole
         (Ec/no-boundary ec)
         (vc Ec/no-boundary)
         (if0 Ec/no-boundary ec ec)
         (let [x Ec/no-boundary] ec)
         (cons Ec/no-boundary ec)
         (cons vc Ec/no-boundary)
         (let [(cons x x) Ec/no-boundary] ec))
  
  ;; Program evaluation contexts, and with particular hole types.
  (P/ah  (M s E/ah))
  (P/ch  (M s E/ch))
  
  ;; Answers
  (a     (M s vc)
         (in-hole P/ch (blame f any ...))))

;;;
;;; The reduction relation
;;;

;; We can't specify our reduction relation exactly like in the paper
;; in redex, because it doesn't allow:
;;
;;  (M s_1 e_1) --> (M s_2 e_2)
;;  -----------------------------------------------------
;;  (M s_1 (in-hole Ea e_1)) --> (M s_2 (in-hole Ea e_2))
;;
;; In particular, the premise isn't allowed to contain patterns, so
;; we need to take a slightly different tack.
;;
;; We define three reduction relations instead:
;;    ec ==>a ec
;;    ea ==>a ea
;;    p  -->  p
;; where all side-effecting steps must be written directly in the
;; last relation.

(define red
  (reduction-relation
   affine*
   
   ;; Discard blame context
   ;; This isn't a rule in the calculus, but it makes it easier to see
   ;; blame when it happens:
   (-->  (M s (in-hole E/ch (blame f any ...)))
         (() () (blame f any ...))
         (side-condition (not (equal? (term E/ch) (term hole)))))
   
   ;; Basic C reduction
   (==>c ((lambda (x : tc) ec) vc)
         (subst-c x vc ec)
         "C-Beta")
   (==>c (let [x vc] ec)
         (subst-c x vc ec)
         "C-LetVar")
   (==>c (cc vc)
         (delta-c cc vc)
         "C-Delta")
   (==>c (if0 0 ec_1 ec_2)
         ec_1
         "C-If0")
   (==>c (if0 n ec_1 ec_2)
          ec_2
         "C-IfZ"
         (side-condition (not (zero? (term n)))))
   (==>c (let [(cons x y) (cons vc_x vc_y)] ec)
         (subst-c x vc_x (subst-c y vc_y ec))
         "C-Let")
   (-->  ((m_1 ... (module C (f : tc) vc) m_2 ...)
          s
          (in-hole E/ch (var f [g])))
         ((m_1 ... (module C (f : tc) vc) m_2 ...)
          s
          (in-hole E/ch vc))
         "C-Mod")

   ;; Basic A reductions
   (==>a ((lambda (x[Q] : ta) ea) va)
         (subst-a x va ea)
         "A-Beta")
   (==>a (let [x[Q] va] ea)
         (subst-a x va ea)
         "A-LetVar")
   (-->  (M s   (in-hole E/ah (ca va)))
         (M s_* (in-hole E/ah va_*))
         (where (s_* va_*) (delta-a l s ca va))
         "A-Delta"
         (fresh l)) ;; We can't allocate a fresh l inside delta-a :(
   (==>a (if0 0 ea_1 ea_2)
         ea_1
         "A-If0")
   (==>a (if0 n ea_1 ea_2)
          ea_2
         "A-IfZ"
         (side-condition (not (zero? (term n)))))
   (==>a (let [(cons x[Q_x] y[Q_y]) (cons va_x va_y)] ea)
         (subst-a x va_x (subst-a y va_y ea))
         "A-Let")
   (-->  ((m_1 ... (module A (f : ta^u) va) m_2 ...)
          s
          (in-hole E/ah (var f [g])))
         ((m_1 ... (module A (f : ta^u) va) m_2 ...)
          s
          (in-hole E/ah va))
         "A-Mod")

  ;; Mixed rules for C
   (-->  ((m_1 ... (module A (f : ta^u) va) m_2 ...)
          s
          (in-hole E/ch (var f [g])))
         ((m_1 ... (module A (f : ta^u) va) m_2 ...)
          s
          (in-hole E/ch (CA ta^u g f (var f [g]))))
         "C-ModA")
   (==>c (CA int f g n)
         n
         "C-Int")
   (==>c (CA (ta_1 -+o ta_2) f g va)
         (lambda (x : (ta->tc ta_1))
           (CA ta_2 f g (va (AC ta_1 g f (var x [f])))))
         "C-Eta"
         (fresh x))
   (-->  (M
          (se ...)
          (in-hole E/ch (CA ta^a f g va)))
         (M
          (se ... (l = BLSSD))
          (in-hole E/ch (CA[l] ta^a f g va)))
         "C-Bless"
         (fresh l))
   (-->  (M
          (se_1 ... (l = BLSSD) se_2 ...)
          (in-hole E/ch ((CA[l] (ta_1 -1o ta_2) f g va) vc)))
         (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ch (CA ta_2 f g (va (AC ta_1 g f vc)))))
         "C-Split")
   (-->  (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ch ((CA[l] (ta_1 -1o ta_2) f g va) vc)))
         (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ch (blame f C-Resplit)))
         "C-Resplit")
   
   ;; Mixed rules for A
   (-->  ((m_1 ... (module C (f : tc) vc) m_2 ...)
          s
          (in-hole E/ah (var f [g])))
         ((m_1 ... (module C (f : tc) vc) m_2 ...)
          s
          (in-hole E/ah (AC (tc->ta tc) g f (var f [g]))))
         "A-ModC")
   (-->  ((m_1 ... (interface (f :> ta^u) f_1) m_2 ...)
          s
          (in-hole E/ah (var f [g])))
         ((m_1 ... (interface (f :> ta^u) f_1) m_2 ...)
          s
          (in-hole E/ah (AC ta^u g f (var f_1 [f]))))
         "A-ModI")
   (==>a (AC int f g n)
         n
         "A-Int")
   (==>a (AC (ta_1 -*o ta_2) f g vc)
         (lambda (x[A] : ta_1)
           (AC ta_2 f g (vc (CA ta_1 g f (var x [f])))))
         "A-Eta"
         (fresh x))
   (-->  (M
          (se_1 ... (l = BLSSD) se_2 ...)
          (in-hole E/ah (AC ta^o_1 g_1 f_1 (CA[l] ta^o f g va))))
         (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ah va))
         "A-Open")
   (-->  (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ah (AC ta^o_1 g_1 f_1 (CA[l] ta^o f g va))))
         (M
          (se_1 ... (l = DFNCT) se_2 ...)
          (in-hole E/ah (AC ta^o_1 g_1 f_1 (blame f A-Reopen))))
         "A-Reopen")
  
   with
   [(--> (in-hole P/ch ec_1) (in-hole P/ch ec_2))
    (==>c ec_1 ec_2)]
   [(--> (in-hole P/ah ea_1) (in-hole P/ah ea_2))
    (==>a ea_1 ea_2)]))

(define-metafunction affine*
  delta-c : cc vc -> vc
  [(delta-c - n)
   (-/1 n)]
  [(delta-c (-/1 n_1) n_2)
   ,(- (term n_1) (term n_2))]
  [(delta-c succ n)
   ,(+ (term n) 1)]
  [(delta-c pred n)
   ,(- (term n) 1)])

(define-metafunction affine*
  delta-a : l s ca va -> (s va)
  [(delta-a l_f s - n)
   (s (-/1 n))]
  [(delta-a l_f s (-/1 n_1) n_2)
   (s ,(- (term n_1) (term n_2)))]
  [(delta-a l_f s succ n)
   (s ,(+ (term n) 1))]
  [(delta-a l_f s pred n)
   (s ,(- (term n) 1))]
  [(delta-a l_f (se ...) [new ta] va)
   ((se ... (l_f = va)) (ref l_f))]
  [(delta-a l_f (se_1 ... (l = va_1) se_2 ...) [swap ta_1 ta_2] (cons (ref l) va_2))
   ((se_1 ... (l = va_2) se_2 ...) (cons (ref l) va_1))])

(define-metafunction affine*
  subst-c : x vc ec -> ec
  [(subst-c x vc cc)
   cc]
  [(subst-c x vc (lambda (x : tc) ec))
   (lambda (x : tc) ec)]
  [(subst-c x vc (lambda (x_1 : tc) ec))
   (lambda (x_1 : tc) (subst-c x vc ec))]
  [(subst-c x vc (var x [f]))
   vc]
  [(subst-c x vc (var x_1 [f]))
   (var x_1 [f])]
  [(subst-c x vc (ec_1 ec_2))
   ((subst-c x vc ec_1) (subst-c x vc ec_2))]
  [(subst-c x vc (if0 ec_1 ec_2 ec_3))
   (if0 (subst-c x vc ec_1) (subst-c x vc ec_2) (subst-c x vc ec_3))]
  [(subst-c x vc (let [x ec_1] ec))
   (let [x (subst-c x vc ec_1)] ec)]
  [(subst-c x vc (let [x_1 ec_1] ec))
   (let [x_1 (subst-c x vc ec_1)] (subst-c x vc ec))]
  [(subst-c x vc (cons ec_1 ec_2))
   (cons (subst-c x vc ec_1) (subst-c x vc ec_2))]
  [(subst-c x vc (let [(cons x x_2) ec_1] ec))
   (let [(cons x x_2) (subst-c x vc ec_1)] ec)]
  [(subst-c x vc (let [(cons x_1 x) ec_1] ec))
   (let [(cons x_1 x) (subst-c x vc ec_1)] ec)]
  [(subst-c x vc (let [(cons x_1 x_2) ec_1] ec))
   (let [(cons x_1 x_2) (subst-c x vc ec_1)] (subst-c x vc ec))]
  [(subst-c x vc (CA ta f g ea))
   (CA ta f g (subst-c-a x vc ea))]
  [(subst-c x vc (CA[l] ta f g ea))
   (CA[l] ta f g (subst-c-a x vc ea))]
  [(subst-c x vc (blame f any ...))
   (blame f any ...)])

(define-metafunction affine*
  subst-a : x va ea -> ea
  [(subst-a x va ca)
   ca]
  [(subst-a x va (ref l))
   (ref l)]
  [(subst-a x va (lambda (x[Q] : ta) ea))
   (lambda (x[Q] : ta) ea)]
  [(subst-a x va (lambda (x_1[Q] : ta) ea))
   (lambda (x_1[Q] : ta) (subst-a x va ea))]
  [(subst-a x va (var x [f]))
   va]
  [(subst-a x va (var x_1 [f]))
   (var x_1 [f])]
  [(subst-a x va (ea_1 ea_2))
   ((subst-a x va ea_1) (subst-a x va ea_2))]
  [(subst-a x va (if0 ea_1 ea_2 ea_3))
   (if0 (subst-a x va ea_1) (subst-a x va ea_2) (subst-a x va ea_3))]
  [(subst-a x va (let [x[Q] ea_1] ea))
   (let [x[Q] (subst-a x va ea_1)] ea)]
  [(subst-a x va (let [x_1[Q] ea_1] ea))
   (let [x_1[Q] (subst-a x va ea_1)] (subst-a x va ea))]
  [(subst-a x va (cons ea_1 ea_2))
   (cons (subst-a x va ea_1) (subst-a x va ea_2))]
  [(subst-a x va (let [(cons x[Q_1] x_2[Q_2]) ea_1] ea))
   (let [(cons x[Q_1] x_2[Q_2]) (subst-a x va ea_1)] ea)]
  [(subst-a x va (let [(cons x_1[Q_1] x[Q_2]) ea_1] ea))
   (let [(cons x_1[Q_1] x[Q_2]) (subst-a x va ea_1)] ea)]
  [(subst-a x va (let [(cons x_1[Q_1] x_2[Q_2]) ea_1] ea))
   (let [(cons x_1[Q_1] x_2[Q_2]) (subst-a x va ea_1)] (subst-a x va ea))]
  [(subst-a x va (AC ta f g ec))
   (AC ta f g (subst-a-c x va ec))])

(define-metafunction affine*
  subst-a-c : x va ec -> ec
  [(subst-a-c x va cc)
   cc]
  [(subst-a-c x va (lambda (x_1 : tc) ec))
   (lambda (x_1 : tc) (subst-a-c x va ec))]
  [(subst-a-c x va (var x_1 [f]))
   (var x_1 [f])]
  [(subst-a-c x va (ec_1 ec_2))
   ((subst-a-c x va ec_1) (subst-a-c x va ec_2))]
  [(subst-a-c x va (if0 ec_1 ec_2 ec_3))
   (if0 (subst-a-c x va ec_1) (subst-a-c x va ec_2) (subst-a-c x va ec_3))]
  [(subst-a-c x va (let [x_1 ec_1] ec))
   (let [x_1 (subst-a-c x va ec_1)] (subst-a-c x va ec))]
  [(subst-a-c x va (cons ec_1 ec_2))
   (cons (subst-a-c x va ec_1) (subst-a-c x va ec_2))]
  [(subst-a-c x va (let [(cons x_1 x_2) ec_1] ec))
   (let [(cons x_1 x_2) (subst-a-c x va ec_1)] (subst-a-c x va ec))]
  [(subst-a-c x va (CA ta f g ea))
   (CA ta f g (subst-a x va ea))]
  [(subst-a-c x va (CA[l] ta f g ea))
   (CA[l] ta f g (subst-a x va ea))]
  [(subst-a-c x va (blame f any ...))
   (blame f any ...)])

(define-metafunction affine*
  subst-c-a : x vc ea -> ea
  [(subst-c-a x vc ca)
   ca]
  [(subst-c-a x vc (ref l))
   (ref l)]
  [(subst-c-a x vc (lambda (x_1[Q] : ta) ea))
   (lambda (x_1[Q] : ta) (subst-c-a x vc ea))]
  [(subst-c-a x vc (var x_1 [f]))
   (var x_1 [f])]
  [(subst-c-a x vc (ea_1 ea_2))
   ((subst-c-a x vc ea_1) (subst-c-a x vc ea_2))]
  [(subst-c-a x vc (if0 ea_1 ea_2 ea_3))
   (if0 (subst-c-a x vc ea_1) (subst-c-a x vc ea_2) (subst-c-a x vc ea_3))]
  [(subst-c-a x vc (let [x_1[Q] ea_1] ea))
   (let [x_1[Q] (subst-c-a x vc ea_1)] (subst-c-a x vc ea))]
  [(subst-c-a x vc (cons ea_1 ea_2))
   (cons (subst-c-a x vc ea_1) (subst-c-a x vc ea_2))]
  [(subst-c-a x vc (let [(cons x_1[Q_1] x_2[Q_2]) ea_1] ea))
   (let [(cons x_1[Q_1] x_2[Q_2]) (subst-c-a x vc ea_1)] (subst-c-a x vc ea))]
  [(subst-c-a x vc (AC ta f g ec))
   (AC ta f g (subst-c x vc ec))])

(define-metafunction affine*
  P->Cfg : P -> Cfg
  [(P->Cfg (M ec))
   (M () ec)])

;;;;;
;;;;; Examples
;;;;;

;; check : P -> ((okay ...) tc)
(define (check P)
  (term (typecheck-program (decorate-program ,P))))

;; run/unchecked : P -> (listof Cfg)
(define (run/unchecked P)
  (apply-reduction-relation* red (term (P->Cfg (decorate-program ,P)))))

;; run : P -> (listof Cfg)
(define (run P)
  (check P)
  (run/unchecked P))

;; run/t : P -> 
(define (run/t P)
  (check P)
  (parameterize
      ([reduction-steps-cutoff 200])
    (traces red (term (P->Cfg (decorate-program ,P))))))

;; More examples:

;; pN : P

(define p1
  (term (() (succ 1))))

(define p2
  (term (((module C (n : int) 3))
         n)))

(define p3
  (term (((module A (n : int) 3))
         (succ n))))

(define p4
  (term (((module C (2+ : (int -> int))
            (lambda (x : int)
              (succ (succ x)))))
         2+)))

(define p5
  (term (((module C (2+ : (int -> int))
            (lambda (x : int)
              (succ (succ x)))))
         (2+ 3))))

(define p6
  (term (((module C (2+ : (int -> int))
            (lambda (x : int)
              (succ (succ x)))))
         (2+ (2+ 3)))))

(define p7
  (term (((module C (apply : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x)))))
         ((apply pred) 9))))

(define p8
  (term (((module C (z : int) 0)
          (module C (+ : (int -> (int -> int)))
            (lambda (x : int)
              (lambda (y : int)
                (if0 x y ((+ (pred x)) (succ y))))))
          (module C (times : (int -> (int -> int)))
            (lambda (x : int)
              (lambda (y : int)
                (if0 x z ((+ y) ((times (pred x)) y)))))))
         ((times 2) 2))))

(define p9
  (term (((module C (+ : (int -> (int -> int)))
            (lambda (x : int)
             (lambda (y : int)
               ((- x) ((- 0) y))))))
         ((+ 10) 20))))

(define p10
  (term (((module A (+ : (int -+o (int -+o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y))))))
         ((+ 10) 20))))

(define p11
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y))))))
         ((+ 10) 20))))

(define p12
  (term (((module A (+ : (int -+o (int -+o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (addtwice : (int -+o (int -+o int)))
            (lambda (x : int)
              (let [adder (+ x)]
                (lambda (y : int)
                  (adder (adder y)))))))
         ((addtwice 1) 3))))

;; type error
(define p13
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (addtwice : (int -+o (int -1o int)))
            (lambda (x : int)
              (let [adder (+ x)]
                (lambda (y : int)
                  (adder (adder y)))))))
         ((addtwice 1) 3))))

;; type error
(define p14
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (addtwice : (int -+o (int -1o int)))
            (lambda (x : int)
              (let [adder (+ x)] ;; adder used twice
                (lambda (y : int)
                  (adder (adder y)))))))
         ((addtwice 1) 3))))

;; type error
(define p15
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (addtwice : (int -+o (int -+o int)))
            (lambda (x : int)
              ((lambda (adder : (int -1o int))
                 (lambda (y : int) ;; can't close over adder
                   (adder (adder y))))
               (+ x)))))
         ((addtwice 1) 3))))

(define p16
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (addtwice : (int -+o (int -1o int)))
            (lambda (x : int)
              (let [adder1 (+ x)]
                (let [adder2 (+ x)]
                  (lambda (y : int)
                    (adder1 (adder2 y))))))))
         ((addtwice 1) 3))))

;; Contract error (blame addtwice)
(define p17
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module C (addtwice : (int -> (int -> int)))
            (lambda (x : int)
              (let [adder (+ x)]
                (lambda (y : int)
                  (adder (adder y)))))))
         ((addtwice 1) 3))))

(define p18
  (term (((module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module C (addtwice : (int -> (int -> int)))
            (lambda (x : int)
              (let [adder1 (+ x)]
                (let [adder2 (+ x)]
                  (lambda (y : int)
                    (adder1 (adder2 y))))))))
         ((addtwice 1) 3))))

;; Type error
(define p19
  (term (((module C (apply : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x))))
          (module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (module A (2+ : (int -+o int))
            (lambda (z : int)
              ((apply (+ 2)) z)))) ;; Can't pass affine function to apply
         (2+ 9))))


(define p20
  (term (((module C (apply : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f x))))
          (module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (interface (my-apply :> ((int -1o int) -+o (int -1o int))) apply)
          (module A (2+ : (int -+o int))
            (lambda (z : int)
              ((my-apply (+ 2)) z))))
         (2+ 9))))

;; contract error (blame my-apply)
(define p21
  (term (((module C (apply2 : ((int -> int) -> (int -> int)))
            (lambda (f : (int -> int))
              (lambda (x : int)
                (f (f x)))))
          (module A (+ : (int -+o (int -1o int)))
            (lambda (x : int)
              (lambda (y : int)
                ((- x) ((- 0) y)))))
          (interface (my-apply :> ((int -1o int) -+o (int -1o int))) apply2)
          (module A (2+ : (int -+o int))
            (lambda (z : int)
              ((my-apply (+ 2)) z))))
         (2+ 9))))

(define p22
  (term (((module A (meh : (int -+o int))
            (lambda (start : int)
              (let [cell ([new int] start)]
                (let [(cons cell v1) ([swap int int] (cons cell 9))]
                  (let [(cons cell v2) ([swap int (int -+o int)] (cons cell succ))]
                    (if0 v1
                         (let [(cons cell v3) ([swap (int -+o int) int]
                                               (cons cell 0))]
                           (v3 v2))
                         v2)))))))
         (meh 0))))

(define p23
  (term (((module A (meh : (int -+o int))
            (lambda (start : int)
              (let [cell ([new int] start)]
                (let [(cons cell v1) ([swap int int] (cons cell 9))]
                  (let [(cons cell v2) ([swap int (int -+o int)] (cons cell succ))]
                    (if0 v1
                         (let [(cons cell v3) ([swap (int -+o int) int]
                                               (cons cell 0))]
                           (v3 v2))
                         v2)))))))
         (meh 3))))

;; Type error
(define p24
  (term (((module A (meh : (int -+o int))
            (lambda (start : int)
              (let [cell1 ([new int] start)]
                (let [(cons cell2 v1) ([swap int int] (cons cell1 9))]
                  (let [(cons cell3 v2) ([swap int (int -+o int)] (cons cell2 succ))]
                    (if0 v2
                         (let [(cons cell4 v3) ([swap (int -+o int) int]
                                               (cons cell3 0))]
                           (v3 v2))
                         (let [(cons cell4 v3) ([swap int int]
                                               (cons cell1 0))]
                           v3))))))))
         (meh 3))))

(define p25
  (term (((module A (meh : (int -+o int))
            (lambda (start : int)
              (let [cell1 ([new int] start)]
                (let [put (lambda (x : int)
                            (let [(cons cell res) ([swap int int] (cons cell1 x))]
                              res))]
                  (let [start1 (put 0)]
                    start1))))))
         (meh 3))))

;; Type error
(define p26
  (term (((module A (meh : (int -+o int))
            (lambda (start : int)
              (let [cell1 ([new int] start)]
                (let [put (lambda (x : int)
                            (let [(cons cell res) ([swap int int] (cons cell1 x))]
                              res))]
                  (let [start1 (put 5)]
                    (put start1)))))))
          (meh 3))))


;; Type error
(define p27
  (term (((module A (ap0 : ((int -1o int) -+o int))
            (lambda (f : (int -1o int))
              (let [r ([new (int -1o int)] f)]
                (let [(cons n1 f1) ([swap int int] (cons r 5))]
                  (pred n1))))))
         (ap0 succ))))

(define p28
  (term (((module A (intref : (int -+o (int ref)))
            (lambda (x : int)
              ([new int] x)))
          (module A (take : ((int ref) -+o int))
            (lambda (r : (int ref))
              (let [(cons r1 n) ([swap int (int -+o int)] (cons r pred))]
                n)))
          (module C (double : (int -> int))
            (lambda (y : int)
              (let [r (intref y)]
                (let [n (take r)]
                  ((- n) ((- 0) n)))))))
         (double 5))))

;; contract violation (blame double)
(define p29
  (term (((module A (intref : (int -+o (int ref)))
            (lambda (x : int)
              ([new int] x)))
          (module A (take : ((int ref) -+o int))
            (lambda (r : (int ref))
              (let [(cons r1 n) ([swap int (int -+o int)] (cons r pred))]
                n)))
          (module C (double : (int -> int))
            (lambda (y : int)
              (let [r (intref y)]
                ((- (take r)) ((- 0) (take r)))))))
         (double 5))))

;; Some helper macros to make this self-contained.
;; (These are due to Sam Tobin-Hochstadt)

(define-syntax no-fail
  (syntax-rules ()
    [(_ e r) (with-handlers ([exn:fail? (lambda _ r)]) e)]
    [(_ e) (no-fail e #f)]))

(define-syntax term-let*
  (syntax-rules ()
    [(term-let* () . e) (term-let () . e)]
    [(term-let* (cl . rest) . e) (term-let (cl) (term-let* rest . e))]))

(define-syntax (match/redex stx)
  (define-syntax-class clause
    #:transparent
    #:description "match/redex clause"
    (pattern [pat ((e:expr) #:min 1) ...*]))
  (syntax-parse stx
   [(_ lang e:expr cl:clause ...)
    #:declare lang static
    (quasisyntax/loc stx
      (let ([r (term e)])
        ((term-match/single 
          lang
          [cl.pat (begin cl.e ...)] ... 
          [any #,(syntax/loc stx (error 'match/redex "no match for term ~a" r))])
         r)))]))

(define-syntax (*term-let-one stx)
  (syntax-case stx ()
    [(_ lang ([pat rhs]) . body)
     (quasisyntax/loc stx
       (let ([r rhs])
         ((term-match/single
           lang
           [pat (begin . body)]
           [any #,(syntax/loc stx (error 'term-let "term ~a did not match pattern ~a" r 'pat))])
          r)))]))

(define-syntax *term-let
  (syntax-rules ()
    [(*term-let lang () . e) (term-let () . e)]
    [(*term-let lang (cl . rest) . e) (*term-let-one lang (cl) (*term-let lang rest . e))]))