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

    • ava JloJle4Ka 05.06.2021 02:16 # 0

      Я ничего не понимаю, где именно здесь смешное (ну или грустное)?
      Ответить

      • ava Hijikata 05.06.2021 02:58 # +2

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

        Грустное, там в итоге разворачивается цель невъебенного объема, но по-другому это и не сделать, к сожалению
        Ответить

        • ava bormand 05.06.2021 03:06 # +1

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

          Или это и есть самый нижний уровень?
          Ответить

          • ava Hijikata 05.06.2021 03:11 # +1

            Наверное, можно что-то придумать, но это пока что использовалось только в одном месте для очень специфичной леммы (нет застрявших термов), так что пока точно сказать не могу. Мб можно доказать это для отдельных инструкций и просто все добавить к кокоподсказкам
            Ответить

            • ava Hijikata 05.06.2021 03:12 # +1

              Но вообще в коке очень не хватает (или я такую не знаю) какой-то тактики в духе "развернуть все из конкретного модуля"
              Ответить

              • ava bormand 05.06.2021 03:14 # +1

                Да можно сделать, наверное. Рефлексия же есть в ltac'е?

                (Я сварщица не настоящая, только первый том SF дочитала и немножко от второго).
                Ответить

                • ava Hijikata 05.06.2021 03:22 # +1

                  Честно говоря, не знаю, но мб можно через мл как-то подступиться
                  Ответить

                • ava Hijikata 05.06.2021 03:30 # +1

                  У меня курс в универе по коку тоже состоял из sf, а там, к сожалению, слишком модельные примеры автоматизации
                  Ответить

    • ava bormand 05.06.2021 02:41 # +1

      Ну, по крайней мере это не надо писать руками в каждом пруфе...
      Ответить

    • ava MAKAKA 05.06.2021 02:42 # 0

      коок
      Ответить

      • ava bormand 05.06.2021 02:49 # +2

        У меня с самого начала была какая-то тактика и я её придерживался.
        Ответить

    • ava bormand 05.06.2021 02:50 # 0

      > hvc

      Ого, гиперколл какой-нибудь?
      Ответить

    • ava nuTepcKuu_nemyx 05.06.2021 13:18 # 0

      Ничего не понимаю. Переведи на "PHP".
      Ответить

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