0
HOL Lightには、ocamlの構文を変更するためのいくつかの悩ましいcamlp5ロジックがあります。私はocaml 4.04と6.17で動作するようにパッチを当てましたが、camlp5の下でのみ動作しますstrict mode。 STRICTが定義されていない場合STRICTが定義され、そして最初にされている場合、これは2番目のマクロの分岐を実行する必要があり、私の理解の最高にcamlp5 IFNDEF STRICTは、私が期待しているものとは逆の働きをしています。
value vala_map f =
IFNDEF STRICT THEN
fun x -> f x
ELSE
fun
[ Ploc.VaAnt s -> Ploc.VaAnt s
| Ploc.VaVal x -> Ploc.VaVal (f x) ]
END
;
：私はthe following codeに問題をトレースしてきました。私はcamlp5r pa_macro.cmo -definedでSTRICTがcamlp5 strictモードのマシンに定義されており、camlp5 transitionalモードのマシンでは定義されていないことを確認しました。
残念ながら、両方のマシンで2番目のブランチが使用され、あたかもSTRICTが両方のマシンに定義されています。 IFNDEF STRICT THENをIFNDEF BLAH THENに変更すると、最初のブランチに切り替わり、再びSTRICTが両方に定義されているかのようになります。ただし、コードの直前にUNDEF STRICT;を置くことは効果がありません。
私は迷っています。何が起きているのか、次に実行するための実験については何かアドバイスがあります。