2016-12-12 2 views
0

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 THENIFNDEF BLAH THEN으로 변경하면 첫 번째 분기로 전환되며 다시 STRICT이 둘 다 정의됩니다. 그러나 코드 바로 앞에 UNDEF STRICT;을 넣는 것은 효과가 없습니다.

나는 손실이 있으며, 어떤 일이 일어나고 있는지 또는 다음에 실험 할 제안을 원합니다.

답변

0

수수께끼 해결 : 해당 파일로 가져온 모듈 중 하나가 명시 적으로 엄격 모드로 설정됩니다. UNDEF은 효과가 없었습니다. STRICT이 특수하게 처리 된 내장입니다.