Куча говна / Говнокод #27455 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 Hijikata, (Updated )

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

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

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

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

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

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

Из-за тебя ушел bormand, guest!

    А не использовать ли нам bbcode?


    8