이사벨 구문 번역 : Force eta-expansion?

Question

이자벨의 목록 이론 filter에 대한 구문 번역을 설정 한 :

syntax 
    -- {* Special syntax for filter *} 
    "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])") 

translations 
    "[x<-xs . P]"== "CONST filter (%x. P) xs" 

을 실제로 term "filter (λ x. ¬(P x)) l" 멋지게

"[x←l . ¬ P x]" :: "int list" 

를 인쇄하지만 표현은 간단 경우, 예를 들어, ilter (λ x. P x) l, ETA 수축이 일어날 것으로 보인다 나는

"filter P l" :: "int list" 

내가 어떻게 든 여기뿐만 아니라 좋은 구문 (즉 [x←l . P x])를 강제 할 수 표시 얻을?

Answer 1

print_translation을 적절하게 설치하여 수축을 방지 할 수 있습니다. HOL 소스의 바인더와 튜플에 대한 몇 가지 예가 있습니다 (예 : THE, HOL.thy).

print_translation {* 
    [(@{const_syntax filter}, fn _ => fn [Abs abs, xs] => 
    let val (x, t) = Syntax_Trans.atomic_abs_tr' abs 
    in Syntax.const @{syntax_const "_filter"} $ x $ t $ xs end)] 
*} -- {* To avoid eta-contraction of body *}