1. Куча / Говнокод #27455

    +1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    Ltac solveInstr :=
      unfold mov, ldr,
      str, cmp,
      jnz, jmp, halt, fail,
      hvc, run, yield, share, lend, donate,
      retrieve, relinquish, reclaim, send, wait,
      option_state_unpack, unpack_hvc_result_normal, unpack_hvc_result_yield,
      get_reg, update_reg, update_incr_PC, get_memory, update_memory;
      repeat case_match;
      subst; eauto.

    Запостил: Hijikata, 05 Июня 2021

    Комментарии (15) RSS

    • Я ничего не понимаю, где именно здесь смешное (ну или грустное)?
      Ответить
      • Анфолд разворачивает имя в определение, остальные тактики помогают хоть как-то это упростить

        Грустное, там в итоге разворачивается цель невъебенного объема, но по-другому это и не сделать, к сожалению
        Ответить
        • Ну возможно каких-то мелких лемм про инструкции и состояния надоказывать, чтобы больше на такой лоу-левл не опускаться и не анфолдить всё подряд?

          Или это и есть самый нижний уровень?
          Ответить
          • Наверное, можно что-то придумать, но это пока что использовалось только в одном месте для очень специфичной леммы (нет застрявших термов), так что пока точно сказать не могу. Мб можно доказать это для отдельных инструкций и просто все добавить к кокоподсказкам
            Ответить
            • Но вообще в коке очень не хватает (или я такую не знаю) какой-то тактики в духе "развернуть все из конкретного модуля"
              Ответить
              • Да можно сделать, наверное. Рефлексия же есть в ltac'е?

                (Я сварщица не настоящая, только первый том SF дочитала и немножко от второго).
                Ответить
                • Честно говоря, не знаю, но мб можно через мл как-то подступиться
                  Ответить
                • У меня курс в универе по коку тоже состоял из sf, а там, к сожалению, слишком модельные примеры автоматизации
                  Ответить
    • Ну, по крайней мере это не надо писать руками в каждом пруфе...
      Ответить
    • коок
      Ответить
      • У меня с самого начала была какая-то тактика и я её придерживался.
        Ответить
    • > hvc

      Ого, гиперколл какой-нибудь?
      Ответить
    • Ничего не понимаю. Переведи на "PHP".
      Ответить

    Добавить комментарий