Что такое EvalOp в Coq CompCert

Определение EvalOp находится в compcert.backend.SplitLongproof:

Ltac EvalOp :=
  eauto;
  match goal with
  | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
  | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
  | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
  | _ => idtac
  end.

Что странно в этом определении, так это то, что coqdoc --html распознает Eval и Op как два отдельных токена:

<span class="id" title="keyword">Eval</span><span class="id" title="var">Op</span>

Почему Coq допускает использование двух токенов без разделителей (пробелов) посередине? Или это баг coqdoc? Спасибо за помощь!


coq coq-tactic coq-extraction compcert
person Jian Wang    schedule 26.03.2018    source источник
comment
Здесь я вижу <span class="id">EvalOp</span>.   -  person Anton Trunov    schedule 27.03.2018
comment
@AntonTrunov Я скомпилировал CompCert и документ, используя coq 8.7.1+2 в opam. Моя команда doc — coqdoc --html -q -R lib compcert.lib -R common compcert.common -R x86_64 compcert.x86_64 -R x86 compcert.x86 -R backend compcert.backend -R cfrontend compcert.cfrontend -R driver compcert.driver -R flocq compcert.flocq -R exportclight compcert.exportclight -R cparser compcert.cparser --vernac-file lib/*.v common/*.v x86_64/*.v x86/*.v backend/*.v cfrontend/*.v driver/*.v flocq/*.v exportclight/*.v cparser/*.v Знаете ли вы, как компилируется официальная документация и почему эта ошибка возникает на моей машине?   -  person Jian Wang    schedule 27.03.2018
comment
@AntonTrunov Или это может быть потому, что в compcert 3.2 есть ошибка, в то время как ошибка была устранена в основной версии compcert?   -  person Jian Wang    schedule 27.03.2018
comment
Я не знаю, но может ли это быть экземпляром issue #2366?   -  person Anton Trunov    schedule 27.03.2018
comment
Кроме того, может ли CompCert использовать coq2html вместо coqdoc для создания HTML?   -  person Anton Trunov    schedule 27.03.2018
comment
@AntonTrunov Понятно, так что, скорее всего, это ошибка в coqdoc --html. Я хотел бы попробовать решить проблему № 2366 (cd theories && coqdoc -toc -html -d html *.v), но как это применимо к случаю, когда файлы v находятся в нескольких папках? Например, если я запущу coqdoc один раз для каждой папки в compcert, я думаю, я потеряю ссылки переменной href для переменных, определенных в разных папках?   -  person Jian Wang    schedule 27.03.2018
comment
Извините, я не знаю. Я либо использую сгенерированные файлы coqdoc, либо просто просматриваю/просматриваю исходный код.   -  person Anton Trunov    schedule 27.03.2018
comment
Eval будучи общеупотребительным токеном, я думаю, что это просто какой-то инструмент в цепочке, который запутался в правильной токенизации. :-(   -  person Ptival    schedule 27.03.2018
comment
@Ptival Как вы думаете, ошибка в парсере Coq? Использует ли coqdoc тот же парсер, что и coqc? Если да, то coqc безопасен в этом случае?   -  person Jian Wang    schedule 28.03.2018
comment
Последнее, что я проверял, coqdoc и coqc использовали разные синтаксические анализаторы. В любом случае, у coqc такой проблемы нет.   -  person Jason Gross    schedule 10.05.2018

Ответы (1)


arrow_upward
3
arrow_downward

Почему Coq допускает использование двух токенов без разделителей (пробелов) посередине? Или это баг coqdoc?

Это ошибка coqdoc. Coq не допускает двух буквенных токенов без буквенно-цифровых символов между ними, но есть много других примеров токенов без разделителей. Например, это допустимый Coq:

Definition(*no-spaces*)foo:=1.

Я полагаю, что это лексируется как токены Definition, комментарии (*no-spaces*), foo, :=, 1 и .. Вы также можете играть в глупые игры с числовыми жетонами, например,

Coercion Nat.add:nat>->Funclass.
Axiom a:nat.
Check 1a:nat.

Поскольку идентификаторы не могут начинаться с цифр, Coq анализирует 1a как 1, примененное к a, который выполняет проверку типов из-за Coercion. Вы, вероятно, не должны играть в такие игры с парсером Coq.

person Jason Gross    schedule 10.05.2018