initialise-binding initialise-storing initialise-giving finalise-failing finalise-throwing scope
  (collateral (bind
    ("readArray",
     allocate-variable (functions
       (tuples ((values)*),
        values))),
  bind
    ("printArray",
     allocate-variable (functions
       (tuples ((values)*),
        values))),
  bind
    ("transArray",
     allocate-variable (functions
       (tuples ((values)*),
        values))),
  bind
    ("mulArray",
     allocate-variable (functions
       (tuples ((values)*),
        values))),
  bind
    ("main",
     allocate-variable (functions
       (tuples ((values)*),
        values)))),
   sequential (assign
     (bound ("readArray"),
      function closure (scope
        (match
          (given,
           tuple (pattern closure (bind
             ("a",
              allocate-initialised-variable
                (values,
                 given))))),
         handle-return (scope
           (bind
             ("m",
              allocate-initialised-variable
                (values,
                 integer-subtract
                   (length (vector-elements (assigned (bound ("a")))),
                    decimal-natural ("1")))),
            scope
              (bind
                ("n",
                 allocate-initialised-variable
                   (values,
                    integer-subtract
                      (length (vector-elements (assigned (checked index
                        (integer-add
                          (1,
                           decimal-natural ("0")),
                         vector-elements (assigned (bound ("a"))))))),
                       decimal-natural ("1")))),
               scope
                 (bind
                   ("i",
                    allocate-initialised-variable
                      (values,
                       decimal-natural ("0"))),
                  while
                    (is-less-or-equal
                      (assigned (bound ("i")),
                       assigned (bound ("m"))),
                     sequential
                       (sequential
                         (print ("Line ",
                         integer-add
                           (assigned (bound ("i")),
                            decimal-natural ("1")),
                         " (",
                         integer-add
                           (assigned (bound ("n")),
                            decimal-natural ("1")),
                         " elements): "),
                          scope
                            (bind
                              ("j",
                               allocate-initialised-variable
                                 (values,
                                  decimal-natural ("0"))),
                             while
                               (is-less-or-equal
                                 (assigned (bound ("j")),
                                  assigned (bound ("n"))),
                                sequential
                                  (effect (give
                                    (read,
                                     sequential
                                       (assign
                                         (checked index
                                           (integer-add
                                             (1,
                                              assigned (bound ("j"))),
                                            vector-elements (assigned (checked index
                                              (integer-add
                                                (1,
                                                 assigned (bound ("i"))),
                                               vector-elements (assigned (bound ("a"))))))),
                                          given),
                                        given))),
                                   effect (give
                                     (bound ("j"),
                                      sequential
                                        (assign
                                          (given,
                                           integer-add
                                             (assigned (given),
                                              1)),
                                         assigned (given)))))))),
                        effect (give
                          (bound ("i"),
                           sequential
                             (assign
                               (given,
                                integer-add
                                  (assigned (given),
                                   1)),
                              assigned (given))))))))))))),
   assign
     (bound ("printArray"),
      function closure (scope
        (match
          (given,
           tuple (pattern closure (bind
             ("a",
              allocate-initialised-variable
                (values,
                 given))))),
         handle-return (scope
           (bind
             ("m",
              allocate-initialised-variable
                (values,
                 integer-subtract
                   (length (vector-elements (assigned (bound ("a")))),
                    decimal-natural ("1")))),
            scope
              (bind
                ("n",
                 allocate-initialised-variable
                   (values,
                    integer-subtract
                      (length (vector-elements (assigned (checked index
                        (integer-add
                          (1,
                           decimal-natural ("0")),
                         vector-elements (assigned (bound ("a"))))))),
                       decimal-natural ("1")))),
               scope
                 (bind
                   ("i",
                    allocate-initialised-variable
                      (values,
                       decimal-natural ("0"))),
                  while
                    (is-less-or-equal
                      (assigned (bound ("i")),
                       assigned (bound ("m"))),
                     sequential
                       (sequential
                         (print ("Line ",
                         integer-add
                           (assigned (bound ("i")),
                            decimal-natural ("1")),
                         " (",
                         integer-add
                           (assigned (bound ("n")),
                            decimal-natural ("1")),
                         " elements):"),
                          scope
                            (bind
                              ("j",
                               allocate-initialised-variable
                                 (values,
                                  decimal-natural ("0"))),
                             while
                               (is-less-or-equal
                                 (assigned (bound ("j")),
                                  assigned (bound ("n"))),
                                sequential
                                  (print (" ",
                                  assigned (checked index
                                    (integer-add
                                      (1,
                                       assigned (bound ("j"))),
                                     vector-elements (assigned (checked index
                                       (integer-add
                                         (1,
                                          assigned (bound ("i"))),
                                        vector-elements (assigned (bound ("a"))))))))),
                                   effect (give
                                     (bound ("j"),
                                      sequential
                                        (assign
                                          (given,
                                           integer-add
                                             (assigned (given),
                                              1)),
                                         assigned (given))))))),
                          print ("\n")),
                        effect (give
                          (bound ("i"),
                           sequential
                             (assign
                               (given,
                                integer-add
                                  (assigned (given),
                                   1)),
                              assigned (given))))))))))))),
   assign
     (bound ("transArray"),
      function closure (scope
        (match
          (given,
           tuple (pattern closure (bind
             ("a",
              allocate-initialised-variable
                (values,
                 given))))),
         handle-return (scope
           (bind
             ("m",
              allocate-initialised-variable
                (values,
                 integer-subtract
                   (length (vector-elements (assigned (bound ("a")))),
                    decimal-natural ("1")))),
            scope
              (bind
                ("n",
                 allocate-initialised-variable
                   (values,
                    integer-subtract
                      (length (vector-elements (assigned (checked index
                        (integer-add
                          (1,
                           decimal-natural ("0")),
                         vector-elements (assigned (bound ("a"))))))),
                       decimal-natural ("1")))),
               scope
                 (bind
                   ("b",
                    allocate-nested-vectors (integer-add
                      (assigned (bound ("n")),
                       decimal-natural ("1")),
                    integer-add
                      (assigned (bound ("m")),
                       decimal-natural ("1")))),
                  sequential
                    (scope
                      (bind
                        ("i",
                         allocate-initialised-variable
                           (values,
                            decimal-natural ("0"))),
                       while
                         (is-less-or-equal
                           (assigned (bound ("i")),
                            assigned (bound ("m"))),
                          sequential
                            (scope
                              (bind
                                ("j",
                                 allocate-initialised-variable
                                   (values,
                                    decimal-natural ("0"))),
                               while
                                 (is-less-or-equal
                                   (assigned (bound ("j")),
                                    assigned (bound ("n"))),
                                  sequential
                                    (effect (give
                                      (assigned (checked index
                                        (integer-add
                                          (1,
                                           assigned (bound ("j"))),
                                         vector-elements (assigned (checked index
                                           (integer-add
                                             (1,
                                              assigned (bound ("i"))),
                                            vector-elements (assigned (bound ("a")))))))),
                                       sequential
                                         (assign
                                           (checked index
                                             (integer-add
                                               (1,
                                                assigned (bound ("i"))),
                                              vector-elements (assigned (checked index
                                                (integer-add
                                                  (1,
                                                   assigned (bound ("j"))),
                                                 vector-elements (assigned (bound ("b"))))))),
                                            given),
                                          given))),
                                     effect (give
                                       (bound ("j"),
                                        sequential
                                          (assign
                                            (given,
                                             integer-add
                                               (assigned (given),
                                                1)),
                                           assigned (given))))))),
                             effect (give
                               (bound ("i"),
                                sequential
                                  (assign
                                    (given,
                                     integer-add
                                       (assigned (given),
                                        1)),
                                   assigned (given))))))),
                     return (assigned (bound ("b"))))))))))),
   assign
     (bound ("mulArray"),
      function closure (scope
        (match
          (given,
           tuple (pattern closure (bind
             ("a",
              allocate-initialised-variable
                (values,
                 given))),
           pattern closure (bind
             ("b",
              allocate-initialised-variable
                (values,
                 given))))),
         handle-return (scope
           (bind
             ("m",
              allocate-initialised-variable
                (values,
                 integer-subtract
                   (length (vector-elements (assigned (bound ("a")))),
                    decimal-natural ("1")))),
            scope
              (bind
                ("n",
                 allocate-initialised-variable
                   (values,
                    integer-subtract
                      (length (vector-elements (assigned (bound ("b")))),
                       decimal-natural ("1")))),
               scope
                 (bind
                   ("p",
                    allocate-initialised-variable
                      (values,
                       integer-subtract
                         (length (vector-elements (assigned (checked index
                           (integer-add
                             (1,
                              decimal-natural ("0")),
                            vector-elements (assigned (bound ("b"))))))),
                          decimal-natural ("1")))),
                  scope
                    (bind
                      ("c",
                       allocate-nested-vectors (integer-add
                         (assigned (bound ("m")),
                          decimal-natural ("1")),
                       integer-add
                         (assigned (bound ("p")),
                          decimal-natural ("1")))),
                     sequential
                       (scope
                         (bind
                           ("i",
                            allocate-initialised-variable
                              (values,
                               decimal-natural ("0"))),
                          while
                            (is-less-or-equal
                              (assigned (bound ("i")),
                               assigned (bound ("m"))),
                             sequential
                               (scope
                                 (bind
                                   ("j",
                                    allocate-initialised-variable
                                      (values,
                                       decimal-natural ("0"))),
                                  while
                                    (is-less-or-equal
                                      (assigned (bound ("j")),
                                       assigned (bound ("p"))),
                                     sequential
                                       (sequential
                                         (effect (give
                                           (decimal-natural ("0"),
                                            sequential
                                              (assign
                                                (checked index
                                                  (integer-add
                                                    (1,
                                                     assigned (bound ("j"))),
                                                   vector-elements (assigned (checked index
                                                     (integer-add
                                                       (1,
                                                        assigned (bound ("i"))),
                                                      vector-elements (assigned (bound ("c"))))))),
                                                 given),
                                               given))),
                                          scope
                                            (bind
                                              ("k",
                                               allocate-initialised-variable
                                                 (values,
                                                  decimal-natural ("0"))),
                                             while
                                               (is-less-or-equal
                                                 (assigned (bound ("k")),
                                                  assigned (bound ("n"))),
                                                sequential
                                                  (effect (give
                                                    (integer-add
                                                      (assigned (checked index
                                                        (integer-add
                                                          (1,
                                                           assigned (bound ("j"))),
                                                         vector-elements (assigned (checked index
                                                           (integer-add
                                                             (1,
                                                              assigned (bound ("i"))),
                                                            vector-elements (assigned (bound ("c")))))))),
                                                       integer-multiply
                                                         (assigned (checked index
                                                           (integer-add
                                                             (1,
                                                              assigned (bound ("k"))),
                                                            vector-elements (assigned (checked index
                                                              (integer-add
                                                                (1,
                                                                 assigned (bound ("i"))),
                                                               vector-elements (assigned (bound ("a")))))))),
                                                          assigned (checked index
                                                            (integer-add
                                                              (1,
                                                               assigned (bound ("j"))),
                                                             vector-elements (assigned (checked index
                                                               (integer-add
                                                                 (1,
                                                                  assigned (bound ("k"))),
                                                                vector-elements (assigned (bound ("b")))))))))),
                                                     sequential
                                                       (assign
                                                         (checked index
                                                           (integer-add
                                                             (1,
                                                              assigned (bound ("j"))),
                                                            vector-elements (assigned (checked index
                                                              (integer-add
                                                                (1,
                                                                 assigned (bound ("i"))),
                                                               vector-elements (assigned (bound ("c"))))))),
                                                          given),
                                                        given))),
                                                   effect (give
                                                     (bound ("k"),
                                                      sequential
                                                        (assign
                                                          (given,
                                                           integer-add
                                                             (assigned (given),
                                                              1)),
                                                         assigned (given)))))))),
                                        effect (give
                                          (bound ("j"),
                                           sequential
                                             (assign
                                               (given,
                                                integer-add
                                                  (assigned (given),
                                                   1)),
                                              assigned (given))))))),
                                effect (give
                                  (bound ("i"),
                                   sequential
                                     (assign
                                       (given,
                                        integer-add
                                          (assigned (given),
                                           1)),
                                      assigned (given))))))),
                        return (assigned (bound ("c")))))))))))),
   assign
     (bound ("main"),
      function closure (scope
        (match
          (given,
           tuple ()),
         handle-return (sequential
           (print ("Input the number of lines and columns (two natural numbers): "),
            scope
              (bind
                ("x",
                 allocate-initialised-variable
                   (values,
                    read)),
               scope
                 (bind
                   ("y",
                    allocate-initialised-variable
                      (values,
                       read)),
                  scope
                    (bind
                      ("a",
                       allocate-nested-vectors (assigned (bound ("x")),
                       assigned (bound ("y")))),
                     sequential
                       (effect (apply
                         (assigned (bound ("readArray")),
                          tuple (assigned (bound ("a"))))),
                        print ("Your matrix is:\n"),
                        effect (apply
                          (assigned (bound ("printArray")),
                           tuple (assigned (bound ("a"))))),
                        print ("The transpose of your matrix is:\n"),
                        effect (apply
                          (assigned (bound ("printArray")),
                           tuple (apply
                             (assigned (bound ("transArray")),
                              tuple (assigned (bound ("a"))))))),
                        print ("You matrix multiplied with its transpose is:\n"),
                        effect (apply
                          (assigned (bound ("printArray")),
                           tuple (apply
                             (assigned (bound ("mulArray")),
                              tuple (assigned (bound ("a")),
                              apply
                                (assigned (bound ("transArray")),
                                 tuple (assigned (bound ("a"))))))))),
                        print ("The transpose of your matrix multiplied with your matrix is:\n"),
                        effect (apply
                          (assigned (bound ("printArray")),
                           tuple (apply
                             (assigned (bound ("mulArray")),
                              tuple (apply
                                (assigned (bound ("transArray")),
                                 tuple (assigned (bound ("a")))),
                              assigned (bound ("a")))))))))))))))),
   apply
     (assigned (bound ("main")),
      tuple ())))