HOL Light에는 ocaml의 구문을 변경하는 일부 고문 camlp5 로직이 있습니다. ocaml 4.04 및 6.17에서 작동하도록 패치했지만 camlp5 strict mode에서만 작동합니다. STRICT
가 정의되어있는 경우 내 이해의 자부합니다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
;
, 이것은 두 번째 매크로 분기를 실행해야하고, STRICT
경우 첫 번째는 정의되지 않은 : 나는 the following code에 문제를 추적했습니다. camlp5r pa_macro.cmo -defined
으로 STRICT
이 내 컴퓨터에서 camlp5 strict 모드로 정의되어 있고 내 컴퓨터에서 camlp5 전환 모드로 정의되지 않았 음을 확인했습니다.
둘 모두에 STRICT
이 정의 된 것처럼 두 번째 분기가 두 시스템에서 사용됩니다. IFNDEF STRICT THEN
을 IFNDEF BLAH THEN
으로 변경하면 첫 번째 분기로 전환되며 다시 STRICT
이 둘 다 정의됩니다. 그러나 코드 바로 앞에 UNDEF STRICT;
을 넣는 것은 효과가 없습니다.
나는 손실이 있으며, 어떤 일이 일어나고 있는지 또는 다음에 실험 할 제안을 원합니다.