initialise-binding initialise-storing initialise-giving finalise-failing finalise-throwing scope
  (collateral (bind
    ("main",
     allocate-variable (functions
       (tuples ((values)*),
        values))),
  bind
    ("insertion_sort",
     allocate-variable (functions
       (tuples ((values)*),
        values)))),
   sequential (assign
     (bound ("main"),
      function closure (scope
        (match
          (given,
           tuple ()),
         handle-return (scope
           (bind
             ("a",
              allocate-nested-vectors (decimal-natural ("5"))),
            sequential
              (effect (give
                (decimal-natural ("5"),
                 sequential
                   (assign
                     (checked index
                       (integer-add
                         (1,
                          decimal-natural ("0")),
                        vector-elements (assigned (bound ("a")))),
                      given),
                    given))),
               effect (give
                 (decimal-natural ("4"),
                  sequential
                    (assign
                      (checked index
                        (integer-add
                          (1,
                           decimal-natural ("1")),
                         vector-elements (assigned (bound ("a")))),
                       given),
                     given))),
               effect (give
                 (decimal-natural ("1"),
                  sequential
                    (assign
                      (checked index
                        (integer-add
                          (1,
                           decimal-natural ("2")),
                         vector-elements (assigned (bound ("a")))),
                       given),
                     given))),
               effect (give
                 (decimal-natural ("8"),
                  sequential
                    (assign
                      (checked index
                        (integer-add
                          (1,
                           decimal-natural ("3")),
                         vector-elements (assigned (bound ("a")))),
                       given),
                     given))),
               effect (give
                 (decimal-natural ("7"),
                  sequential
                    (assign
                      (checked index
                        (integer-add
                          (1,
                           decimal-natural ("4")),
                         vector-elements (assigned (bound ("a")))),
                       given),
                     given))),
               effect (apply
                 (assigned (bound ("insertion_sort")),
                  tuple (assigned (bound ("a"))))),
               scope
                 (bind
                   ("i",
                    allocate-initialised-variable
                      (values,
                       decimal-natural ("0"))),
                  while
                    (is-less
                      (assigned (bound ("i")),
                       length (vector-elements (assigned (bound ("a"))))),
                     sequential
                       (print (assigned (checked index
                         (integer-add
                           (1,
                            assigned (bound ("i"))),
                          vector-elements (assigned (bound ("a")))))),
                        effect (give
                          (bound ("i"),
                           sequential
                             (assign
                               (given,
                                integer-add
                                  (assigned (given),
                                   1)),
                              assigned (given))))))))))))),
   assign
     (bound ("insertion_sort"),
      function closure (scope
        (match
          (given,
           tuple (pattern closure (bind
             ("a",
              allocate-initialised-variable
                (values,
                 given))))),
         handle-return (scope
           (bind
             ("i",
              allocate-initialised-variable
                (values,
                 decimal-natural ("1"))),
            while
              (is-less
                (assigned (bound ("i")),
                 length (vector-elements (assigned (bound ("a"))))),
               sequential
                 (scope
                   (bind
                     ("val_i",
                      allocate-initialised-variable
                        (values,
                         assigned (checked index
                           (integer-add
                             (1,
                              assigned (bound ("i"))),
                            vector-elements (assigned (bound ("a"))))))),
                    scope
                      (bind
                        ("j",
                         allocate-initialised-variable
                           (values,
                            assigned (bound ("i")))),
                       sequential
                         (while
                           (if-else
                             (is-greater
                               (assigned (bound ("j")),
                                decimal-natural ("0")),
                              is-less
                                (assigned (bound ("val_i")),
                                 assigned (checked index
                                   (integer-add
                                     (1,
                                      integer-subtract
                                        (assigned (bound ("j")),
                                         decimal-natural ("1"))),
                                    vector-elements (assigned (bound ("a")))))),
                              false),
                            sequential
                              (effect (give
                                (assigned (checked index
                                  (integer-add
                                    (1,
                                     integer-subtract
                                       (assigned (bound ("j")),
                                        decimal-natural ("1"))),
                                   vector-elements (assigned (bound ("a"))))),
                                 sequential
                                   (assign
                                     (checked index
                                       (integer-add
                                         (1,
                                          assigned (bound ("j"))),
                                        vector-elements (assigned (bound ("a")))),
                                      given),
                                    given))),
                               effect (give
                                 (integer-subtract
                                   (assigned (bound ("j")),
                                    decimal-natural ("1")),
                                  sequential
                                    (assign
                                      (bound ("j"),
                                       given),
                                     given))))),
                          effect (give
                            (assigned (bound ("val_i")),
                             sequential
                               (assign
                                 (checked index
                                   (integer-add
                                     (1,
                                      assigned (bound ("j"))),
                                    vector-elements (assigned (bound ("a")))),
                                  given),
                                given)))))),
                  effect (give
                    (bound ("i"),
                     sequential
                       (assign
                         (given,
                          integer-add
                            (assigned (given),
                             1)),
                        assigned (given))))))))))),
   apply
     (assigned (bound ("main")),
      tuple ())))