Make contracts from these types.

[akuhlens]

#lang typed/racket/no-check

;; The diffs between languages are one of the best sources of documentation
;; of what passes do to the language grammar that we currently have.
;; I want to leave them in place until we have contracts that are able to
;; dynamically check the language grammars. With the hopes that we will
;; be able to calculate the contracts based on the diffs.

#|-----------------------------------------------------------------------------+
| Language/Cast3 created by interpret-casts                                    |
+-----------------------------------------------------------------------------|#

(define-type Cast-or-Coerce3-Lang
  (Prog (List String Natural Grift-Type)
    (Static* (List CoC3-Bnd*)
             CoC3-Expr)))


(define-type CoC3-Expr
  (Rec E (U (Castable-Lambda-Forms E)
            (Fn-Proxy-Forms E)
            (Letrec (Bnd* E) E)
            (Let (Bnd* E) E)
            (Var Uid) 
            (Global String)
            (Assign Id E)
            (Gen-Data-Forms E)
            (Code-Forms E)
            (Quote-Coercion Grift-Coercion)
            (Coercion-Operation-Forms E)
            (Quote-HCoercion Mixed-Coercion) 
            (Hyper-Coercion-Operation-Forms E)
            (Type Grift-Type)
            (Type-Operation-Forms E)
            (Control-Flow-Forms E)
            (Op Grift-Primitive (Listof E))
            (Quote Cast-Literal)
            No-Op
            (Blame E)
            (Observe E Grift-Type)
            (Unguarded-Forms E)
            (Guarded-Proxy-Forms E)
            (Monotonic-Forms E Grift-Type)
            (Error E)
            (Tuple-Operation-Forms E))))

#;
(define-type CoC3-Expr
  (Rec E (U
          (Construct CoC3-Gen-Data CoC3-Gen-Ctor (Listof E))
          (Access CoC3-Gen-Data CoC3-Gen-Access E (Option E))
          (Check CoC3-Gen-Data CoC3-Gen-Pred E (Listof E))
          (Observe E Grift-Type) 
          No-Op
          ;; Code Labels
          (Code-Label Uid)
          (Labels CoC3-Bnd-Code* E)
          (App-Code E (Listof E))
          ;; Functions as an interface
          (Lambda Uid* (Castable (Option Uid) E))
          (Fn-Caster E)
          (App-Fn E (Listof E))
          ;; Our Lovely Function Proxy Representation
          (App-Fn-or-Proxy Uid E (Listof E))
          (Fn-Proxy (List Index Uid) E E)
          (Fn-Proxy-Huh E)
          (Fn-Proxy-Closure E)
          (Fn-Proxy-Coercion E)
          ;; Coercions
          (Quote-Coercion Grift-Coercion)
          (Quote-HCoercion Mixed-Coercion)
          (Compose-Coercions E E)
          (Id-Coercion-Huh E)
          (Fn-Coercion-Huh E)
          (Make-Fn-Coercion Uid E E E)
          (Fn-Coercion (Listof E) E)
          (Fn-Coercion-Arg E E)
          (Fn-Coercion-Return E)
          (Fn-Coercion-Arity E)
          (Id-Fn-Coercion E)
          (Fn-Coercion-Return-Set! E E)
          (Fn-Coercion-Arg-Set! E E E) 
          (Ref-Coercion E E E)
          (Ref-Coercion-Huh E)
          (Ref-Coercion-Read E)
          (Ref-Coercion-Write E)
          (Ref-Coercion-Ref-Huh E)
          (Sequence-Coercion E E)
          (Sequence-Coercion-Huh E)
          (Sequence-Coercion-Fst E)
          (Sequence-Coercion-Snd E)
          (Project-Coercion E E)
          (Project-Coercion-Huh E)
          (Project-Coercion-Type E)
          (Project-Coercion-Label E)
          (Inject-Coercion E)
          (Inject-Coercion-Type E)
          (Inject-Coercion-Huh E)
          (Failed-Coercion E)
          (Failed-Coercion-Huh E)
          (Failed-Coercion-Label E)
          (HC E E E E E E)
          (HC-Inject-Huh E)
          (HC-Project-Huh E)
          (HC-Identity-Huh E)
          (HC-Label E)
          (HC-T1 E)
          (HC-T2 E)
          (HC-Med E)
          ;;Type operations
          (Type Grift-Type)
          (Type-Dyn-Huh E)
          (Type-Fn-Huh E)
          (Type-Fn-arity E)
          (Type-Fn-arg E E)
          (Type-Fn-return E)
          (Type-GRef-Huh E)
          (Type-GRef-Of  E)
          (Type-GVect-Huh E)
          (Type-GVect-Of E)
          (Type-Mu-Huh E)
          (Type-Mu-Body E)
          ;; Tags are exposed before specify This is bad
          ;; TODO fix this after the deadline
          (Type-Tag E)
          (Tag Tag-Symbol)
          ;; Binding Forms - Lambda
          (Letrec CoC3-Bnd* E)
          (Let CoC3-Bnd* E)
          (Var Uid)
          (Global String)
          (Assign Id E)
          ;; Control Flow
          (If E E E)
          (Switch E (Switch-Case* E) E)
          (Begin CoC3-Expr* E)
          (Repeat Uid E E Uid E E)
          Break-Repeat
          ;;Primitives
          (Op Grift-Primitive (Listof E))
          (Quote Cast-Literal)
          ;; Observations
          (Blame E)
          (Observe E Grift-Type)
          ;; Unguarded-Representation
          (Unguarded-Box E)
          (Unguarded-Box-Ref E)
          (Unguarded-Box-Set! E E)
          (Unguarded-Vect E E)
          (Unguarded-Vect-Ref E E)
          (Unguarded-Vect-Set! E E E)
          (Guarded-Proxy-Huh E)
          (Guarded-Proxy E (Twosome E E E))
          (Guarded-Proxy E (Coercion E))
          (Guarded-Proxy-Ref E)
          (Guarded-Proxy-Source E)
          (Guarded-Proxy-Target E)
          (Guarded-Proxy-Blames E)
          (Guarded-Proxy-Coercion E)
          (Unguarded-Vect-length E)
          ;; Monotonic references
          (Mbox E Grift-Type)
          (Mbox-val-set! E E)
          (Mbox-val-ref E)
          (Mbox-rtti-set! E E)
          (Mbox-rtti-ref E)
          (Make-GLB-Two-Fn-Types Uid E E)
          (Make-GLB-Two-Tuple-Types Uid E E)
          (MRef-Coercion-Huh E)
          (MRef-Coercion-Type E)
          (MRef-Coercion E)
          (Type-GRef E) ;; glb need to create new types in runtime
          (Type-GVect E)
          (Type-MRef E)
          (Type-MRef-Huh E)
          (Type-MRef-Of E)
          (Mvector E E Grift-Type)
          (Mvector-length E)
          (Mvector-val-ref E E VectorAccessMode)
          (Mvector-val-set! E E E VectorAccessMode)
          (Mvector-rtti-ref E)
          (Mvector-rtti-set! E E)
          (Type-MVect E)
          (Type-MVect-Huh E)
          (Type-MVect-Of E)
          (MVect-Coercion-Huh E)
          (MVect-Coercion-Type E)
          (MVect-Coercion E)
          (Error E)
          (Create-tuple (Listof E))
          (Tuple-proj E E)
          (Tuple-Coercion-Huh E)
          (Tuple-Coercion-Num E)
          (Tuple-Coercion-Item E E)
          (Id-Tuple-Coercion E)
          (Tuple-Coercion-Item-Set! E E E)
          (Coerce-Tuple Uid E E)
          (Coerce-Tuple-In-Place Uid E E E E E)
          (Cast-Tuple Uid E E E E)
          (Cast-Tuple-In-Place Uid E E E E E E E)
          (Type-Tuple-Huh E)
          (Type-Tuple-num E)
          (Type-Tuple-item E E)
          (Make-Tuple-Coercion Uid E E E)
          (Mediating-Coercion-Huh E))))

;; Hoist Types and Coercions
(define-type (HT&C+ E)
  (U (Type Immediate-Type)
     (Quote-Coercion Immediate-Coercion)
     (Mvector E E Immediate-Type)
     (Mbox E Immediate-Type)))

(define-type (HT&C- E)
  (U (Type Grift-Type)
     (Quote-Coercion Grift-Coercion)
     (Quote-HCoercion Mixed-Coercion)
     (Mvector E E Grift-Type)
     (Mbox E Grift-Type)))

(define-type (HT&C= E)
  (U (Monotonic-Forms-w/o-Constructors E)
     (Castable-Lambda-Forms E)
     (Fn-Proxy-Forms E) 
     (Letrec (Bnd* E) E)
     (Let (Bnd* E) E)
     (Var Uid)
     (Global String)
     (Assign Id E)
     (Gen-Data-Forms E)
     (Code-Forms E)
     (Coercion-Operation-Forms E)
     (Hyper-Coercion-Operation-Forms E)
     (Type-Operation-Forms E)
     (Control-Flow-Forms E)
     (Op Grift-Primitive (Listof E))
     (Quote Cast-Literal)
     No-Op
     (Blame E)
     (Observe E Grift-Type)
     (Unguarded-Forms E)
     (Guarded-Proxy-Forms E)
     (Error E)
     (Tuple-Operation-Forms E)))


(define-type (Closure-Ops E)
  (U (Let-Closures Uid E)
     (Closure-Code E)
     (Closure-Caster E)
     (Closure-App E)))

(define-type (Closure-Ops/Ref E)
  (U (Let-Closures E E)
     (Closure-Code E)
     (Closure-Caster E)
     (Closure-Ref E) 
     (Closure-App E)))

(define-type (Hybrid-Fn-Proxy-Forms E)
  (U Closure-Proxy
     (Hybrid-Proxy-Huh E)
     (Hybrid-Proxy-Closure E)
     (Hybrid-Proxy-Coercion E)))

(define-type (Data-Fn-Proxy-Forms E)
  (U (Fn-Proxy Index E E)
     (Fn-Proxy-Huh E)
     (Fn-Proxy-Closure E)
     (Fn-Proxy-Coercion E)))


(define-type Cast-or-Coerce6-Lang
  (Prog (List String Natural Grift-Type)
        (Static*
         (List Bnd-Mu-Type*
               Bnd-Type*
               Bnd-Mu-Crcn*
               Bnd-Crcn*
               (Bnd* (Fun CoC6-Expr))
               (Closure* CoC6-Expr CoC6-Expr)
               (Bnd* CoC6-Expr))
         CoC6-Expr)))


(define-type CoC6-Expr
  (Rec
   E
   (U (Closure-Ops/Ref E)
      (Data-Fn-Proxy-Forms E)
      (Hybrid-Fn-Proxy-Forms E)
      (Gen-Data-Forms E)
      (Code-Forms E)
      (Quote-Coercion Immediate-Coercion)
      (Hyper-Coercion-Operation-Forms E)
      (Coercion-Operation-Forms E)
      (Type Immediate-Type)
      (Type-Operation-Forms E)
      (Let (Bnd* E) E)
      (Var Uid)
      (Global String)
      (Assign Id E)
      (Control-Flow-Forms E)
      (Op Grift-Primitive (Listof E))
      No-Op
      (Quote Cast-Literal)
      (Blame E)
      (Observe E Grift-Type)
      (Unguarded-Forms E)
      (Guarded-Proxy-Forms E)
      (Monotonic-Forms E Immediate-Type)
      (Error E)
      (Tuple-Operation-Forms E))))

(define-type Code-Generation
  (U
   ;; both code and closure
   'regular
   ;; Only generate the code, but be compatible with
   ;; any identical fv-list. This is used for the
   ;; definition closure-casters, and when a well-known
   ;; closure shares the closures of closure that isn't
   ;; well-known.
   ;; TODO list invarients needed by 'code-only-code
   'code-only
   ;; Only allocate the closure, don't generate the
   ;; code. This is used to share code between function
   ;; cast, apply-casted closure, of the same arity.
   'closure-only))

;; Uncover Free Eliminates the following forms
(define-type (U- E)
  (U (Named-Castable-Lambda-Forms E)
     (Fn-Proxy-Forms E)))

;; Uncover Free Adds The following forms
(define-type (U+ E)
  (U (Closure-Ops E)
     (Data-Fn-Proxy-Forms E)
     (Hybrid-Fn-Proxy-Forms E)))

;; Uncover Free is invariant in the following forms
(define-type (U= E)
  (U (Gen-Data-Forms E)
     (Code-Forms E)
     (Quote-Coercion Immediate-Coercion)
     (Hyper-Coercion-Operation-Forms E)
     (Coercion-Operation-Forms E)
     (Type Immediate-Type)
     (Type-Operation-Forms E)
     (Let (Bnd* E) E)
     (Var Uid)
     (Global String)
     (Assign Id E)
     (Control-Flow-Forms E)
     (Op Grift-Primitive (Listof E))
     No-Op
     (Quote Cast-Literal)
     (Blame E)
     (Observe E Grift-Type)
     (Unguarded-Forms E)
     (Guarded-Proxy-Forms E)
     (Monotonic-Forms E Immediate-Type)
     (Error E)
     (Tuple-Operation-Forms E)))

;; This pass removes Lambdas from expression contexts
(define-type (Label-Lambdas- E)
  (Castable-Lambda E))

;; And leaves the rest expression forms alone.
(define-type (Label-Lambdas= E)
  (U (Named-Castable-Lambda-Forms E)
     (App-Fn E (Listof E))
     (Fn-Proxy-Forms E)
     (Let (Bnd* E) E)
     (Var Uid)
     (Global String)
     (Assign Id E)
     (Gen-Data-Forms E)
     (Code-Forms E)
     (Quote-Coercion Immediate-Coercion)
     (Coercion-Operation-Forms E)
     (Hyper-Coercion-Operation-Forms E)
     (Type Immediate-Type)
     (Type-Operation-Forms E)
     (Control-Flow-Forms E)
     (Op Grift-Primitive (Listof E))
     (Quote Cast-Literal)
     No-Op
     (Blame E)
     (Observe E Grift-Type)
     (Unguarded-Forms E)
     (Guarded-Proxy-Forms E)
     (Monotonic-Forms E Immediate-Type)
     (Error E)
     (Tuple-Operation-Forms E)))

(define-type Cast-or-Coerce3.1-Lang
  (Prog (List String Natural Grift-Type)
    (Static* (List
              Bnd-Mu-Type*
              Bnd-Type*
              Bnd-Mu-Crcn*
              Bnd-Crcn*
              CoC3.1-Bnd*) 
             CoC3.1-Expr)))

(define-type (Castable-Lambda E) (CLambda E))

(define-type (Gen-Data-Forms E)
  (U (Construct Gen-Data Gen-Ctor (Listof E))
     (Access Gen-Data Gen-Access E (Option E))
     (Check Gen-Data Gen-Pred E (Listof E))))

(define-type (Code-Forms E)
  (U (Code-Label Uid)
     (Labels (Bnd* (Code Uid* E)) E)
     (App-Code E (Listof E))))

(define-type (Fn-Proxy-Forms E)
  (U (App-Fn-or-Proxy Uid E (Listof E))
     (Fn-Proxy (List Index Uid) E E)
     (Fn-Proxy-Huh E)
     (Fn-Proxy-Closure E)
     (Fn-Proxy-Coercion E)))

(define-type (Coercion-Operation-Forms E)
  (U
   (Sequence-Coercion E E)
   (Sequence-Coercion-Huh E)
   (Sequence-Coercion-Fst E)
   (Sequence-Coercion-Snd E)

   (Project-Coercion E E)
   (Project-Coercion-Huh E)
   (Project-Coercion-Type E)
   (Project-Coercion-Label E)

   (Inject-Coercion E)
   (Inject-Coercion-Huh E)
   (Inject-Coercion-Type E)

   (Mediating-Coercion-Huh E)
     
   (Make-Fn-Coercion Uid E E E)
   (Id-Coercion-Huh E)
   (Id-Fn-Coercion E) 
   (Fn-Coercion-Huh E)
   (Fn-Coercion (Listof E) E)
   (Fn-Coercion-Arity E)
   (Fn-Coercion-Arg E E)
   (Fn-Coercion-Return E)
   (Fn-Coercion-Return-Set! E E)
   (Fn-Coercion-Arg-Set! E E E)

   (Ref-Coercion E E E)
   (Ref-Coercion-Huh E)
   (Ref-Coercion-Read E)
   (Ref-Coercion-Write E)
   (Ref-Coercion-Ref-Huh E)

   (MRef-Coercion E)
   (MRef-Coercion-Huh E)
   (MRef-Coercion-Type E)

   (MVect-Coercion-Huh E)
   (MVect-Coercion-Type E)
   (MVect-Coercion E)

   (Failed-Coercion E)
   (Failed-Coercion-Huh E)
   (Failed-Coercion-Label E)

   (Make-Tuple-Coercion Uid E E E)
   (Id-Tuple-Coercion E)
   (Tuple-Coercion-Huh E)
   (Tuple-Coercion-Num E)
   (Tuple-Coercion-Item E E)
   (Tuple-Coercion-Item-Set! E E E)
   
   Make-Mu-Coercion
   (Mu-Coercion-Huh E)
   (Mu-Coercion-Body-Set! E E)
   (Mu-Coercion-Body E)))

(define-type (Type-Operation-Forms E)
  (U (Type-Dyn-Huh E)
     (Type-Fn-Huh E)
     (Type-Fn-arity E)
     (Type-Fn-arg E E)
     (Type-Fn-return E)
     (Type-GRef-Huh E)
     (Type-GRef-Of  E)
     (Type-GVect-Huh E)
     (Type-GVect-Of E)
     (Type-GRef E) 
     (Type-GVect E)
     (Type-MRef E)
     (Type-MRef-Huh E)
     (Type-MRef-Of E)
     (Type-MVect E)
     (Type-MVect-Huh E)
     (Type-MVect-Of E)
     (Type-Tuple-Huh E)
     (Type-Tuple-num E)
     (Type-Tuple-item E E)
     (Type-Mu-Huh E)
     (Type-Mu-Body E)))

(define-type (Tag-Forms E) 
  ;; Tags are exposed before specify This is bad
  ;; TODO fix this after the deadline
  (U (Type-Tag E)
     (Tag Tag-Symbol)))

(define-type (Control-Flow-Forms E)
  (U (If E E E)
     (Switch E (Switch-Case* E) E)
     (Begin (Listof E) E)
     (Repeat Uid E E Uid E E)
     Break-Repeat))

(define-type (Unguarded-Forms E)
  (U (Unguarded-Box E)
     (Unguarded-Box-On-Stack E)
     (Unguarded-Box-Ref E)
     (Unguarded-Box-Set! E E)
     (Unguarded-Vect E E)
     (Unguarded-Vect-Ref E E)
     (Unguarded-Vect-Set! E E E)
     (Unguarded-Vect-length E)))

(define-type (Guarded-Proxy-Forms E)
  (U (Guarded-Proxy-Huh E)
     (Guarded-Proxy E (U (Twosome E E E) (Coercion E)))
     (Guarded-Proxy-Ref E)
     (Guarded-Proxy-Source E)
     (Guarded-Proxy-Target E)
     (Guarded-Proxy-Blames E)
     (Guarded-Proxy-Coercion E)))

(define-type (Monotonic-Forms-w/o-Constructors E)
  (U (Mbox-val-set! E E)
     (Mbox-val-ref E)
     (Mbox-rtti-set! E E)
     (Mbox-rtti-ref E) 
     (Mvector-length E)
     (Mvector-val-ref E E VectorAccessMode)
     (Mvector-val-set! E E E VectorAccessMode)
     (Mvector-rtti-ref E)
     (Mvector-rtti-set! E E) 
     (Make-GLB-Two-Fn-Types Uid E E)
     (Make-GLB-Two-Tuple-Types Uid E E)))

(define-type (Monotonic-Forms E T)
  (U (Mvector E E T)
     (Mbox E T)
     (Monotonic-Forms-w/o-Constructors E)))

(define-type (Hyper-Coercion-Operation-Forms E)
  (U (HC E E E E E E)
     (HC-Inject-Huh E)
     (HC-Project-Huh E)
     (HC-Identity-Huh E)
     (HC-Label E)
     (HC-T1 E)
     (HC-T2 E)
     (HC-Med E)))


(define-type (Tuple-Operation-Forms E)
  (U (Create-tuple (Listof E)) 
     (Tuple-proj E E)
     (Copy-Tuple E E)
     ;; FIXME These forms shouldn't exist anymore
     (Coerce-Tuple Uid E E)
     (Coerce-Tuple-In-Place Uid E E E E E)
     (Cast-Tuple Uid E E E E)
     (Cast-Tuple-In-Place Uid E E E E E E E)))

(define-type (Castable-Lambda-Forms E)
  (U (Lambda Uid* (Castable (Option Uid) E))
     (Fn-Caster E)
     (App-Fn E (Listof E))))

(define-type CoC3.1-Expr
  (Rec E
       (U (Castable-Lambda-Forms E)
          (Fn-Proxy-Forms E)
          (Letrec (Bnd* E) E)
          (Let (Bnd* E) E)
          (Var Uid) 
          (Global String)
          (Assign Id E)
          (Gen-Data-Forms E)
          (Code-Forms E)
          (Quote-Coercion Immediate-Coercion)
          (Coercion-Operation-Forms E)
          (Hyper-Coercion-Operation-Forms E)
          (Type Immediate-Type)
          (Type-Operation-Forms E)
          (Control-Flow-Forms E)
          ;;Primitives
          (Op Grift-Primitive (Listof E))
          (Quote Cast-Literal)
          No-Op
          ;; Observations
          (Blame E)
          (Observe E Grift-Type)
          (Unguarded-Forms E)
          (Guarded-Proxy-Forms E)
          (Monotonic-Forms E Immediate-Type)
          (Error E)
          (Tuple-Operation-Forms E))))

(define-type Cast-or-Coerce3.2-Lang
  (Prog (List String Natural Grift-Type)
    (Static* (List
              Bnd-Mu-Type*
              Bnd-Type*
              Bnd-Mu-Crcn*
              Bnd-Crcn*
              CoC3.2-Bnd*) 
             CoC3.2-Expr)))

(define-type CoC3.2-Expr
  (Rec E
       (U (Named-Castable-Lambda-Forms E)
          (Castable-Lambda E)
          (Fn-Proxy-Forms E)
          (Let (Bnd* E) E)
          (Var Uid)
          (Global String)
          (Assign Id E)
          (Gen-Data-Forms E)
          (Code-Forms E)
          (Quote-Coercion Immediate-Coercion)
          (Coercion-Operation-Forms E)
          (Hyper-Coercion-Operation-Forms E)
          (Type Immediate-Type)
          (Type-Operation-Forms E)
          (Control-Flow-Forms E)
          (Op Grift-Primitive (Listof E))
          (Quote Cast-Literal)
          No-Op
          (Blame E)
          (Observe E Grift-Type)
          (Unguarded-Forms E)
          (Guarded-Proxy-Forms E)
          (Monotonic-Forms E Immediate-Type)
          (Error E)
          (Tuple-Operation-Forms E))))

(define-type (Purify-Letrec+ E)
  (Letrec (Bnd* (Castable-Lambda E)) E))

(define-type (Purify-Letrec- E)
  (Letrec (Bnd* E) E))

(define-type (Purify-Letrec= E)
  (U (Castable-Lambda-Forms E)
     (Fn-Proxy-Forms E) 
     (Let (Bnd* E) E)
     (Var Uid)
     (Global String)
     (Assign Id E)
     (Gen-Data-Forms E)
     (Code-Forms E)
     (Quote-Coercion Immediate-Coercion)
     (Coercion-Operation-Forms E)
     (Hyper-Coercion-Operation-Forms E)
     (Type Immediate-Type)
     (Type-Operation-Forms E)
     (Control-Flow-Forms E)
     ;;Primitives
     (Op Grift-Primitive (Listof E))
     (Quote Cast-Literal)
     No-Op
     ;; Observations
     (Blame E)
     (Observe E Grift-Type)
     (Unguarded-Forms E)
     (Guarded-Proxy-Forms E)
     (Monotonic-Forms E Immediate-Type)
     (Error E)
     (Tuple-Operation-Forms E)))

(define-type Data0-Lang
  (Prog (List String Natural Grift-Type)
        (GlobDecs Uid* D0-Expr)))

(define-type D0-Bnd-Code* (Listof D0-Bnd-Code))
(define-type D0-Bnd-Code (Pairof Uid D0-Code))
(define-type D0-Code (Code Uid* D0-Expr))



(define-type D0-Expr
  (Rec E (U (Labels D0-Bnd-Code* E)
	    (App-Code E (Listof E))
        (UIL-Op! E)
        (UIL-Op E)
        No-Op
	    (If E E E)
        (Switch E (Switch-Case* E) E)
	    (Begin D0-Expr* E)
        (Repeat Uid E E Uid E E)
        Break-Repeat
	    (Var Uid)
        (Global String)
	    (Code-Label Uid)
	    (Quote D0-Literal)
        (Assign Id E)
        Success
        Stack-Alloc)))

(define-type D0-Expr* (Listof D0-Expr))

(define-type Data5-Lang
  (Prog (List String Natural Grift-Type)
	(GlobDecs Uid*
                    (Labels D5-Bnd-Code*
                            D5-Body))))

(define-type D5-Body (Locals Uid* (Bnd* Nat) D5-Tail))
(define-type D5-Bnd-Code* (Listof D5-Bnd-Code))
(define-type D5-Bnd-Code (Pairof Uid D5-Code))
(define-type D5-Code (Code Uid* D5-Body))

(define-type D5-Tail
  (Rec T
   (U (If D5-Pred T T)
      (Switch D5-Trivial (Switch-Case* T) T)
      (Begin D5-Effect* T)
      (Return D5-Value)
      (Return Success))))

(define-type D5-Pred (Relop UIL-Pred-Prim D5-Trivial D5-Trivial))

(define-type D5-Effect
  (U (Repeat Uid D5-Trivial D5-Trivial #f #f (Begin D5-Effect* No-Op))
     (If D5-Pred (Begin D5-Effect* No-Op) (Begin D5-Effect* No-Op))
     Break-Repeat
     (Switch D5-Trivial
             (Switch-Case* (Begin D5-Effect* No-Op))
             (Begin D5-Effect* No-Op))
     (UIL-Op! D5-Trivial)
     (Assign Id D5-Value)
     No-Op))

(define-type D5-Value
  (U D5-Trivial
     Halt
     (UIL-Op D5-Trivial)
     (App-Code D5-Trivial D5-Trivial*)
     (If D5-Pred D5-Trivial D5-Trivial)))

(define-type D5-Trivial
  (U (Code-Label Uid)
     (Var Uid)
     (Global String)
     (Quote D5-Literal)))


(define-type Data4-Lang
  (Prog (List String Natural Grift-Type)
	(GlobDecs Uid*
                    (Labels D4-Bnd-Code*
                            D4-Body))))

(define-type D4-Body (Locals Uid* (Bnd* Nat) D4-Tail))
(define-type D4-Bnd-Code* (Listof D4-Bnd-Code))
(define-type D4-Bnd-Code (Pairof Uid D4-Code))
(define-type D4-Code (Code Uid* D4-Body))

(define-type D4-Tail
  (Rec T
   (U (If D4-Pred T T)
      (Switch D4-Trivial (Switch-Case* T) T)
      (Begin D4-Effect* T)
      (Return D4-Value)
      (Return Success))))

(define-type D4-Pred
 (Rec P
      (U (If D4-Pred P P)
         (Switch D4-Trivial (Switch-Case* P) P)
         (Begin D4-Effect* P)
         (Relop UIL-Pred-Prim D4-Trivial D4-Trivial))))

(define-type D4-Effect
 (Rec E
      (U (If D4-Pred E E)
         (Switch D4-Trivial (Switch-Case* E) E)
         (Begin D4-Effect* No-Op)
         (Repeat Uid D4-Trivial D4-Trivial #f #f E)
         (UIL-Op! D4-Trivial)
         (Assign Id D4-Value)
         Break-Repeat
         No-Op)))

(define-type D4-Value
  (U D4-Trivial
     Halt
     (UIL-Op D4-Trivial)
     (App-Code D4-Trivial D4-Trivial*)))

(define-type D4-Trivial
  (U (Code-Label Uid)
     (Var Uid)
     (Global String)
     (Quote D4-Literal)))

(define-type Data3-Lang
  (Prog (List String Natural Grift-Type)
	(GlobDecs Uid*
                    (Labels D3-Bnd-Code*
                            D3-Body))))

(define-type D3-Body (Locals Uid* (Bnd* Nat) D3-Tail))
(define-type D3-Bnd-Code* (Listof D3-Bnd-Code))
(define-type D3-Bnd-Code (Pairof Uid D3-Code))
(define-type D3-Code (Code Uid* D3-Body))

(define-type D3-Tail
  (Rec T
   (U (If D3-Pred T T)
      (Switch D3-Trivial (Switch-Case* T) T)
      (Begin D3-Effect* T)
      (Return D3-Value)
      (Return Success))))

(define-type D3-Value
 (Rec V
  (U D3-Trivial
     Halt
     (If D3-Pred V V)
     (Switch D3-Trivial (Switch-Case* V) V)
     (Begin D3-Effect* V)
     (Op UIL-Expr-Prim (Listof D3-Trivial))
     (App-Code D3-Trivial D3-Trivial*))))

(define-type D3-Pred
 (Rec P
      (U (If D3-Pred P P)
         (Switch D3-Trivial (Switch-Case* P) P)
         (Begin D3-Effect* P)
         (Relop UIL-Pred-Prim D3-Trivial D3-Trivial))))

(define-type D3-Effect
 (Rec E
      (U (If D3-Pred E E)
         (Switch D3-Trivial (Switch-Case* E) E)
         (Begin D3-Effect* No-Op)
         (Repeat Uid D3-Trivial D3-Trivial #f #f E)
         Break-Repeat
         (App-Code D3-Trivial D3-Trivial*)
         (UIL-Op! D3-Trivial)
         (Assign Id D3-Value)
         No-Op)))

;; (TODO halt is not trivial though because we are targeting c it may be treated so)
;; remove Halt earlier
(define-type D3-Trivial
  (U (Code-Label Uid)
     (Var Uid)
     (Global String)
     (Quote D3-Literal)))

(define-type D3-Value* (Listof D3-Value))

(define-type Data2-Lang
  (Prog (List String Natural Grift-Type)
        (GlobDecs Uid*
                    (Labels D2-Bnd-Code*
                            D2-Body))))

(define-type D2-Body (Locals Uid* (Bnd* Nat) D2-Tail))
(define-type D2-Bnd-Code* (Listof D2-Bnd-Code))
(define-type D2-Bnd-Code (Pairof Uid D2-Code))
(define-type D2-Code (Code Uid* D2-Body))

(define-type D2-Tail D1-Tail)

(define-type D2-Value D1-Value)

(define-type D2-Pred D1-Pred)

(define-type D2-Effect D1-Effect)

(define-type D2-Value* (Listof D2-Value))

(define-type D2-Effect* (Listof D2-Effect))

(define-type D2-Literal Data-Literal)

(define-type Data1-Lang
  (Prog (List String Natural Grift-Type)
        (GlobDecs Uid*
                    (Labels D1-Bnd-Code*
                            D1-Tail))))

(define-type D1-Bnd-Code* (Listof D1-Bnd-Code))
(define-type D1-Bnd-Code (Pairof Uid D1-Code))
(define-type D1-Code (Code Uid* D1-Tail))

(define-type D1-Tail
  (Rec T
   (U (If D1-Pred T T)
      (Switch D1-Value (Switch-Case* T) T)
      (Begin D1-Effect* T)
      (App-Code D1-Value D1-Value*)
      (Op UIL-Expr-Prim D1-Value*)
      (Var Uid)
      (Global String)
      Halt Success Stack-Alloc
      (Var Uid)
      (Code-Label Uid)
      (Quote D1-Literal))))

(define-type D1-Value
 (Rec V
      (U (If D1-Pred V V)
         (Switch V (Switch-Case* V) V)
         (Begin D1-Effect* V)
         (App-Code V (Listof V))
         (Op UIL-Expr-Prim (Listof V))
         Halt
         Stack-Alloc
         (Var Uid)
         (Global String)
         (Code-Label Uid)
         (Quote D1-Literal))))

(define-type D1-Pred
 (Rec P
      (U (If D1-Pred P P)
         (Switch D1-Value (Switch-Case* P) P)
         (Begin D1-Effect* P)
         (Relop UIL-Pred-Prim D1-Value D1-Value))))

(define-type D1-Effect
 (Rec E
      (U (If D1-Pred E E)
         (Switch D1-Value (Switch-Case* E) E)
         (Begin D1-Effect* No-Op)
         (Repeat Uid D1-Value D1-Value #f #f E)
         Break-Repeat
         (App-Code D1-Value D1-Value*)
         (UIL-Op! D1-Value)
         (Assign Id D1-Value)
         No-Op)))

(define-type Cast-or-Coerce4-Lang
  (Prog (List String Natural Grift-Type)
    (Static* (List CoC4-Bnd-Mu-Type*
                   CoC4-Bnd-Type*
                   CoC4-Bnd-Mu-Crcn*
                   CoC4-Bnd-Crcn*
                   CoC4-Bnd-Data*)
             CoC4-Expr)))

(define-type (Named-Castable-Lambda-Forms E)
  (U (Letrec (Bnd* (Castable-Lambda E)) E)
     (Fn-Caster E)
     (App-Fn E (Listof E))))

(define-type CoC4-Expr
  (Rec E (U
          (Gen-Data-Forms E)
          (Code-Forms E)
          (Named-Castable-Lambda-Forms E)
          (Fn-Proxy-Forms E)
          (Quote-Coercion Immediate-Coercion)
          (Hyper-Coercion-Operation-Forms E)
          (Coercion-Operation-Forms E)
          (Type Immediate-Type)
          (Type-Operation-Forms E)
          (Let (Bnd* E) E)
          (Var Uid)
          (Global String)
          (Assign Id E)
          (Control-Flow-Forms E)
          (Op Grift-Primitive (Listof E))
          No-Op
          (Quote Cast-Literal)
          (Blame E)
          (Observe E Grift-Type)
          (Unguarded-Forms E)
          (Guarded-Proxy-Forms E)
          (Monotonic-Forms E Immediate-Type)
          (Error E)
          (Tuple-Operation-Forms E)
          )))

(define-type Cast0-Lang
  (Prog (List String Natural Grift-Type) C0-Top*))

(define-type C0-Top* (Listof C0-Top))

(define-type C0-Top
  (U (Define Boolean Uid Grift-Type C0-Expr)
     (Observe C0-Expr Grift-Type)))

(define-type Cast0.5-Lang
  (Prog (List String Natural Grift-Type) C0-Expr))

(define-type C0-Expr
  (Rec E (U ;; Non-Terminals
          (Observe E Grift-Type)
          (Lambda Uid* E)
          (Letrec C0-Bnd* E)
          (Let C0-Bnd* E)
          (App E (Listof E))
          (Op Grift-Primitive (Listof E))
          (If E E E)
          (Switch E (Switch-Case* E) E)
          (Cast E (Twosome Grift-Type Grift-Type Blame-Label))
          (Begin C0-Expr* E)
          (Repeat Uid E E Uid E E)
          ;; Guarded effects
          (Gbox E)
          (Gunbox E)
          (Gbox-set! E E)
          (Gvector E E)
          (Gvector-set! E E E)
          (Gvector-ref E E)
          (Gvector-length E)
          ;; Monotonic
          (Mbox E Grift-Type)
          (Munbox E) ;; fast read
          (Mbox-set! E E) ;; fast write
          (MBoxCastedRef E Grift-Type)
          (MBoxCastedSet! E E Grift-Type)
          (Mvector E E Grift-Type)
          (Mvector-ref E E) ;; fast read
          (Mvector-set! E E E) ;; fast write
          (MVectCastedRef E E Grift-Type)
          (MVectCastedSet! E E E Grift-Type)
          (Mvector-length E)
          ;; Dynamic Operations
          (Dyn-GVector-Set! E E E Grift-Type Blame-Label)
          (Dyn-GVector-Ref E E Blame-Label)
          (Dyn-GVector-Len E E)
          (Dyn-GRef-Set! E E Grift-Type Blame-Label)
          (Dyn-GRef-Ref E Blame-Label)
          (Dyn-MVector-Set! E E E Grift-Type Blame-Label)
          (Dyn-MVector-Ref E E Blame-Label)
          (Dyn-MRef-Set! E E Grift-Type Blame-Label)
          (Dyn-MRef-Ref E Blame-Label)
          (Dyn-Fn-App E C0-Expr* Grift-Type* Blame-Label)
          (Dyn-Tuple-Proj E E E)
          (Create-tuple (Listof E))
          (Tuple-proj E Index)
          ;; Terminals
          (Var Uid)
          (Quote Cast-Literal)
          No-Op)))

(define-type C0-Expr* (Listof C0-Expr))

(define-type Cast-or-Coerce5-Lang
  (Prog (List String Natural Grift-Type)
    (Let-Static* Bnd-Mu-Type*
                 Bnd-Type*
                 Bnd-Mu-Crcn*
                 Bnd-Crcn* 
                 CoC5-Expr)))

(define-type CoC5-Expr
  (Rec E
       (U
        (Construct CoC5-Gen-Data CoC5-Gen-Ctor (Listof E))
        (Access CoC5-Gen-Data CoC5-Gen-Access E (Option E))
        (Check CoC5-Gen-Data CoC5-Gen-Pred E (Listof E))
        ;; Code Labels
        (Code-Label Uid)
        (Labels CoC5-Bnd-Code* E)
        (App-Code E (Listof E))
        ;; Functions as an interface
        (Lambda Uid* (Castable (Option Uid) E))
        (Fn-Caster E)
        (App-Fn E (Listof E))
        ;; Our Lovely Function Proxy Representation
        (App-Fn-or-Proxy Uid E (Listof E))
        (Fn-Proxy (List Index Uid) E E)
        (Fn-Proxy-Huh E)
        (Fn-Proxy-Closure E)
        (Fn-Proxy-Coercion E)
        ;; Coercions
        (Quote-Coercion Immediate-Coercion)
        ;(Compose-Coercions E E)
        (HC E E E E E E)
        (HC-Inject-Huh E)
        (HC-Project-Huh E)
        (HC-Identity-Huh E)
        (HC-Label E)
        (HC-T1 E)
        (HC-T2 E)
        (HC-Med E)
        (Id-Coercion-Huh E)
        (Fn-Coercion-Huh E)
        (Make-Fn-Coercion Uid E E E)
        (Fn-Coercion (Listof E) E)
        (Fn-Coercion-Arity E)
        (Fn-Coercion-Arg E E)
        (Fn-Coercion-Return E)
        (Id-Fn-Coercion E)
        (Fn-Coercion-Return-Set! E E)
        (Fn-Coercion-Arg-Set! E E E)
        (Ref-Coercion E E E)
        (Ref-Coercion-Huh E)
        (Ref-Coercion-Read E)
        (Ref-Coercion-Write E)
        (Ref-Coercion-Ref-Huh E)
        (Sequence-Coercion E E)
        (Sequence-Coercion-Huh E)
        (Sequence-Coercion-Fst E)
        (Sequence-Coercion-Snd E)
        (Project-Coercion E E)
        (Project-Coercion-Huh E)
        (Project-Coercion-Type E)
        (Project-Coercion-Label E)
        (Inject-Coercion E)
        (Inject-Coercion-Type E)
        (Inject-Coercion-Huh E)
        (Failed-Coercion E)
        (Failed-Coercion-Huh E)
        (Failed-Coercion-Label E)
        ;;Type operations
        (Type Immediate-Type)
        (Type-Fn-arity E)
        (Type-Fn-arg E E)
        (Type-Fn-return E)
        (Type-GRef-Of  E)
        (Type-GVect-Of E)
        (Type-Dyn-Huh E)
        (Type-Fn-Huh E)
        (Type-GRef-Huh E)
        (Type-GVect-Huh E)
        (Type-Mu-Huh E)
        (Type-Mu-Body E)
        ;; Tags are exposed before specify This is bad
        ;; TODO fix this after the deadline
        (Type-Tag E)
        (Tag Tag-Symbol)
        ;;(Type-Ctr-Case E Type-Ctr-Case-Clause* E)
        ;; Binding Forms - Lambda
        (Letrec CoC5-Bnd-Lambda* E)
        (Let CoC5-Bnd-Data* E)
        (Var Uid)
        (Global String)
        (Assign Id E)
        ;; Controll Flow
        (If E E E)
        (Switch E (Switch-Case* E) E)
        (Begin CoC5-Expr* E)
        (Repeat Uid E E Uid E E)
        Break-Repeat
        ;;Primitives
        (Op Grift-Primitive (Listof E))
        No-Op
        (Quote Cast-Literal)
        ;; Observations
        (Blame E)
        (Observe E Grift-Type)
        ;; Unguarded-Representation
        (Unguarded-Box E)
        (Unguarded-Box-Ref E)
        (Unguarded-Box-Set! E E)
        (Unguarded-Vect E E)
        (Unguarded-Vect-Ref E E)
        (Unguarded-Vect-Set! E E E)
        (Guarded-Proxy-Huh E)
        (Guarded-Proxy E (Twosome E E E))
        (Guarded-Proxy E (Coercion E))
        (Guarded-Proxy-Ref E)
        (Guarded-Proxy-Source E)
        (Guarded-Proxy-Target E)
        (Guarded-Proxy-Blames E)
        (Guarded-Proxy-Coercion E)
        (Unguarded-Vect-length E)
        ;; Monotonic references
        (Mbox E Immediate-Type)
        (Mbox-val-set! E E)
        (Mbox-val-ref E)
        (Mbox-rtti-set! E E)
        (Mbox-rtti-ref E)
        (Make-GLB-Two-Fn-Types Uid E E)
        (Make-GLB-Two-Tuple-Types Uid E E)
        (MRef-Coercion-Huh E)
        (MRef-Coercion-Type E)
        (MRef-Coercion E)
        (Type-GRef E) ;; glb need to create new types in runtime
        (Type-GVect E)
        (Type-MRef E)
        (Type-MRef-Huh E)
        (Type-MRef-Of E)
        (Error E)
        (Mvector E E Immediate-Type)
        (Mvector-length E)
        (Mvector-val-ref E E VectorAccessMode)
        (Mvector-val-set! E E E VectorAccessMode)
        (Mvector-rtti-ref E)
        (Mvector-rtti-set! E E)
        (Type-MVect E)
        (Type-MVect-Huh E)
        (Type-MVect-Of E)
        (MVect-Coercion-Huh E)
        (MVect-Coercion-Type E)
        (MVect-Coercion E)
        ;;
        (Create-tuple (Listof E))
        (Copy-Tuple E E)
        (Tuple-proj E E)
        (Tuple-Coercion-Huh E)
        (Tuple-Coercion-Num E)
        (Tuple-Coercion-Item E E)
        (Id-Tuple-Coercion E)
        (Tuple-Coercion-Item-Set! E E E)
        (Coerce-Tuple Uid E E)
        (Coerce-Tuple-In-Place Uid E E E E E)
        (Cast-Tuple Uid E E E E)
        (Cast-Tuple-In-Place Uid E E E E E E E)
        (Type-Tuple-Huh E)
        (Type-Tuple-num E)
        (Type-Tuple-item E E)
        (Make-Tuple-Coercion Uid E E E)
        (Mediating-Coercion-Huh E))))

(define-type CoC5-Expr* (Listof CoC5-Expr))
(define-type CoC5-Code (Code Uid* CoC5-Expr))
(define-type CoC5-Bnd-Code (Pairof Uid CoC5-Code))
(define-type CoC5-Bnd-Code* (Listof CoC5-Bnd-Code))
(define-type CoC5-Lambda (Lambda Uid* (Free (Option Uid) Uid* CoC5-Expr)))
(define-type CoC5-Bnd-Lambda  (Pairof Uid CoC5-Lambda))
(define-type CoC5-Bnd-Lambda* (Listof CoC5-Bnd-Lambda))
(define-type CoC5-Bnd-Data  (Pairof Uid CoC5-Expr))
(define-type CoC5-Bnd-Data* (Listof CoC5-Bnd-Data))



(define-type Lambda1-Lang
  (Prog (List String Natural Grift-Type)
    (Let-Static* Bnd-Mu-Type*
                 Bnd-Type*
                 Bnd-Mu-Crcn*
                 Bnd-Crcn*
                 L1-Expr)))

(define-type L1-Lambda (Lambda Uid* (Castable (Option Uid) L1-Expr)))

(define-type L1-Expr
  (Rec E (U
          (Construct L1-Gen-Data L1-Gen-Ctor (Listof E))
          (Access L1-Gen-Data L1-Gen-Access E (Option E))
          (Check L1-Gen-Data L1-Gen-Pred E (Listof E))
          ;; Code Labels
          (Code-Label Uid)
          (Labels L1-Bnd-Code* E)
          (App-Code E (Listof E))
          ;; Functions as an interface
          L1-Lambda
          (Fn-Caster E)
          (App-Fn E (Listof E))
          ;; Our Lovely Function Proxy Representation
          (App-Fn-or-Proxy Uid E (Listof E))
          (Fn-Proxy (List Index Uid) E E)
          (Fn-Proxy-Huh E)
          (Fn-Proxy-Closure E)
          (Fn-Proxy-Coercion E)
          ;; Coercions
          (Quote-Coercion Immediate-Coercion)
          (Compose-Coercions E E)
          (HC E E E E E E)
          (HC-Inject-Huh E)
          (HC-Project-Huh E)
          (HC-Identity-Huh E)
          (HC-Label E)
          (HC-T1 E)
          (HC-T2 E)
          (HC-Med E)
          (Id-Coercion-Huh E)
          (Fn-Coercion-Huh E)
          (Make-Fn-Coercion Uid E E E)
          (Fn-Coercion (Listof E) E)
          (Fn-Coercion-Arity E)
          (Fn-Coercion-Arg E E)
          (Fn-Coercion-Return E)
          (Fn-Coercion-Return-Set! E E)
          (Fn-Coercion-Arg-Set! E E E)
          (Id-Fn-Coercion E) 
          (Ref-Coercion E E E)
          (Ref-Coercion-Huh E)
          (Ref-Coercion-Read E)
          (Ref-Coercion-Write E)
          (Ref-Coercion-Ref-Huh E)
          (Sequence-Coercion E E)
          (Sequence-Coercion-Huh E)
          (Sequence-Coercion-Fst E)
          (Sequence-Coercion-Snd E)
          (Project-Coercion E E)
          (Project-Coercion-Huh E)
          (Project-Coercion-Type E)
          (Project-Coercion-Label E)
          (Inject-Coercion E)
          (Inject-Coercion-Type E)
          (Inject-Coercion-Huh E)
          (Failed-Coercion E)
          (Failed-Coercion-Huh E)
          (Failed-Coercion-Label E)
          ;;Type operations
          (Type Immediate-Type)
          (Type-Dyn-Huh E)
          (Type-Fn-Huh E)
          (Type-Fn-arity E)
          (Type-Fn-arg E E)
          (Type-Fn-return E)
          (Type-GRef-Huh E)
          (Type-GRef-Of  E)
          (Type-GVect-Huh E)
          (Type-GVect-Of E)
          ;; Tags are exposed before specify This is bad
          ;; TODO fix this after the deadline
          (Type-Tag E)
          (Tag Tag-Symbol)
          ;;(Type-Ctr-Case E Type-Ctr-Case-Clause* E)
          ;; Binding Forms - Lambda
	  (Letrec L1-Bnd-Lambda* E)
	  (Let L1-Bnd* E)
          (Var Uid)
          (Global String)
          (Assign Id E)
          ;; Controll Flow
          (If E E E)
          (Switch E (Switch-Case* E) E)
          (Begin L1-Expr* E)
          (Repeat Uid E E Uid E E)
          Break-Repeat
          ;;Primitives
          (Op Grift-Primitive (Listof E))
          (Quote Cast-Literal)
          ;; Observations
          (Blame E)
          (Observe E Grift-Type)
          ;; Unguarded-Representation
          (Unguarded-Box E)
          (Unguarded-Box-Ref E)
          (Unguarded-Box-Set! E E)
          (Unguarded-Vect E E)
          (Unguarded-Vect-Ref E E)
          (Unguarded-Vect-Set! E E E)
          (Guarded-Proxy-Huh E)
          (Guarded-Proxy E (Twosome E E E))
          (Guarded-Proxy E (Coercion E))
          (Guarded-Proxy-Ref E)
          (Guarded-Proxy-Source E)
          (Guarded-Proxy-Target E)
          (Guarded-Proxy-Blames E)
          (Guarded-Proxy-Coercion E)
          (Unguarded-Vect-length E)
          ;; Monotonic references
          (Mbox E Immediate-Type)
          (Mbox-val-set! E E)
          (Mbox-val-ref E)
          (Mbox-rtti-set! E E)
          (Mbox-rtti-ref E)
          (Make-GLB-Two-Fn-Types Uid E E)
          (Make-GLB-Two-Tuple-Types Uid E E)
          (MRef-Coercion-Huh E)
          (MRef-Coercion-Type E)
          (MRef-Coercion E)
          (Type-GRef E) ;; glb need to create new types in runtime
          (Type-GVect E)
          (Type-MRef E)
          (Type-MRef-Huh E)
          (Type-MRef-Of E)
          (Error E)
          (Mvector E E Immediate-Type)
          (Mvector-length E)
          (Mvector-val-ref E E VectorAccessMode)
          (Mvector-val-set! E E E VectorAccessMode)
          (Mvector-rtti-ref E)
          (Mvector-rtti-set! E E)
          (Type-MVect E)
          (Type-MVect-Huh E)
          (Type-MVect-Of E)
          (MVect-Coercion-Huh E)
          (MVect-Coercion-Type E)
          (MVect-Coercion E)
          ;;
          (Create-tuple (Listof E))
          (Tuple-proj E E)
          (Tuple-Coercion-Huh E)
          (Tuple-Coercion-Num E)
          (Tuple-Coercion-Item E E)
          (Tuple-Coercion-Item-Set! E E E)
          (Id-Tuple-Coercion E)
          (Coerce-Tuple Uid E E)
          (Coerce-Tuple-In-Place Uid E E E E E)
          (Cast-Tuple Uid E E E E)
          (Cast-Tuple-In-Place Uid E E E E E E E)
          (Type-Tuple-Huh E)
          (Type-Tuple-num E)
          (Type-Tuple-item E E)
          (Make-Tuple-Coercion Uid E E E)
          (Mediating-Coercion-Huh E)
          No-Op)))

(define-type L1-Code (Code Uid* L1-Expr))
(define-type L1-Expr* (Listof L1-Expr))
(define-type L1-Bnd (Pairof Uid L1-Expr))
(define-type L1-Bnd* (Listof L1-Bnd))
(define-type L1-Bnd-Code (Pairof Uid L1-Code))
(define-type L1-Bnd-Code* (Listof L1-Bnd-Code))
(define-type L1-Bnd-Lambda (Pairof Uid L1-Lambda))
(define-type L1-Bnd-Lambda* (Listof L1-Bnd-Lambda))

(define-type Syntax-Lang (Prog String (Listof Any)))



#|-----------------------------------------------------------------------------+
| Language/Grift0 this is the language returned by grift/syntax->grift0
+-----------------------------------------------------------------------------|#
(define-type Grift0-Lang
  (Prog (List String Natural) (Listof G0-Top)))

(define-type G0-Top
  ;; Using Ann2 here instead of Ann keeps a bug in typed racket
  ;; from getting Ann at different places in the type signature
  ;; confused.
  (Ann2 (U (Observe G0-Ann-Expr (Option Grift-Type))
           (Define Boolean Uid (Option Grift-Type) G0-Ann-Expr))
        srcloc))
(define-type G0-Top* (Listof G0-Top))

(define-type G0-Ann-Expr (Ann G0-Expr Src))
(define-type G0-Ann-Expr* (Listof G0-Ann-Expr))

(define-type G0-Expr
  (U (Lambda Grift-Fml* (List G0-Ann-Expr (Option Grift-Type)))
     (Letrec G0-Bnd* G0-Ann-Expr)
     (Let G0-Bnd* G0-Ann-Expr)
     (App G0-Ann-Expr G0-Ann-Expr*)
     (Op Grift-Primitive G0-Ann-Expr*)
     (If G0-Ann-Expr G0-Ann-Expr G0-Ann-Expr)
     (Switch G0-Ann-Expr (Switch-Case* G0-Ann-Expr) G0-Ann-Expr)
     (Ascribe G0-Ann-Expr Grift-Type (Option Blame-Label))
     (Var Uid)
     (Quote Grift-Literal)
     (Begin G0-Ann-Expr* G0-Ann-Expr)
     (Repeat Uid G0-Ann-Expr G0-Ann-Expr (List Uid (Option Grift-Type)) G0-Ann-Expr G0-Ann-Expr)
     ;; Monotonic effects
     (MboxS G0-Ann-Expr)
     (Munbox G0-Ann-Expr)
     (Mbox-set! G0-Ann-Expr G0-Ann-Expr)
     (MvectorS G0-Ann-Expr G0-Ann-Expr)
     (Mvector-set! G0-Ann-Expr G0-Ann-Expr G0-Ann-Expr)
     (Mvector-ref G0-Ann-Expr G0-Ann-Expr)
     (Mvector-length G0-Ann-Expr)
     ;; Guarded effects
     (Gbox G0-Ann-Expr)
     (Gunbox G0-Ann-Expr)
     (Gbox-set! G0-Ann-Expr G0-Ann-Expr)
     (Gvector G0-Ann-Expr G0-Ann-Expr)
     (Gvector-set! G0-Ann-Expr G0-Ann-Expr G0-Ann-Expr)
     (Gvector-ref G0-Ann-Expr G0-Ann-Expr)
     (Gvector-length G0-Ann-Expr)
     ;;
     (Create-tuple G0-Ann-Expr*)
     (Tuple-proj G0-Ann-Expr Index)))
(define-type G0-Expr* (Listof G0-Expr))

(define-type G0-Bnd (Bnd Uid Grift-Type? G0-Ann-Expr))
(define-type G0-Bnd* (Listof G0-Bnd))


(define-type Grift1-Lang
  (Prog (List String Natural Grift-Type) (Listof G1-Top)))

(define-type G1-Top
  (U (Define Boolean Uid Grift-Type G1-Ann-Expr)
     (Observe G1-Ann-Expr Grift-Type)))
(define-type G1-Top* (Listof G1-Top))

(define-type G1-Ann-Expr (Ann G1-Expr (Pair Src Grift-Type)))
(define-type G1-Ann-Expr* (Listof G1-Ann-Expr))

(define-type G1-Expr
  (U
   (Lambda Grift-Fml* G1-Ann-Expr)
   (Letrec G1-Bnd* G1-Ann-Expr)
   (Let G1-Bnd* G1-Ann-Expr)
   (App G1-Ann-Expr (Listof G1-Ann-Expr))
   (Op (List Grift-Primitive Grift-Type*) (Listof G1-Ann-Expr))
   (If G1-Ann-Expr G1-Ann-Expr G1-Ann-Expr)
   (Switch G1-Ann-Expr (Switch-Case* G1-Ann-Expr) G1-Ann-Expr)
   (Ascribe G1-Ann-Expr Grift-Type (Option Blame-Label))
   (Var Uid)
   (Quote Grift-Literal)
   (Begin (Listof G1-Ann-Expr) G1-Ann-Expr)
   (Repeat Uid G1-Ann-Expr G1-Ann-Expr Uid G1-Ann-Expr G1-Ann-Expr)
   ;; Monotonic effects
   (Mbox G1-Ann-Expr Grift-Type)
   (Munbox G1-Ann-Expr)
   (Mbox-set! G1-Ann-Expr G1-Ann-Expr)
   (Mvector G1-Ann-Expr G1-Ann-Expr Grift-Type)
   (Mvector-ref G1-Ann-Expr G1-Ann-Expr)
   (Mvector-set! G1-Ann-Expr G1-Ann-Expr G1-Ann-Expr)
   (Mvector-length G1-Ann-Expr)
   ;; Guarded effects
   (Gbox G1-Ann-Expr)
   (Gunbox G1-Ann-Expr)
   (Gbox-set! G1-Ann-Expr G1-Ann-Expr)
   (Gvector G1-Ann-Expr G1-Ann-Expr)
   (Gvector-set! G1-Ann-Expr G1-Ann-Expr G1-Ann-Expr)
   (Gvector-ref G1-Ann-Expr G1-Ann-Expr)
   (Gvector-length G1-Ann-Expr)
   ;;
   (Create-tuple (Listof G1-Ann-Expr))
   (Tuple-proj G1-Ann-Expr Index)))
(define-type G1-Expr* (Listof G1-Expr))

(define-type G1-Bnd (Bnd Uid Grift-Type G1-Ann-Expr))
(define-type G1-Bnd* (Listof G1-Bnd))