6
올바르게 이해한다면 (주로 applyTactic 기능의 존재로), Idris의 정리 해설자에 대한 사용자 지정 전략을 작성할 수 있습니다. 어떻게하는지 배우는 데 사용할 수있는 몇 가지 예가 무엇입니까?Idris의 사용자 정의 도우미 기술
A
답변
7
Idris에서 사용자 지정 전술을 작성하는 데는 두 가지 메커니즘이 있습니다. 상위 수준과 하위 수준의 반영입니다.
높은 수준의 리플렉션을 사용하면 평가 된 데이터가 아닌 구문에 대해 실행되는 함수를 작성합니다.이 인수는 인수를 줄이지 않습니다. 이 함수는 Idris의 기존 전술을 사용하여 정의 된 새로운 전술을 반환합니다. 증명 기간을 직접 반환하려면 Exact을 사용하면됩니다. 이러한 유형의 반영에 대한 예는 the effects library에서 찾을 수 있습니다. 높은 수준의 반영 전술은 증명 모드에서 byReflection을 사용하여 호출됩니다.
하위 레벨 반영에서는 Idris의 코어 유형 이론에서 인용 된 용어로 직접 작업합니다. 전술은 TT -> List (TTName, TT) -> Tactic의 함수이며 첫 번째 인수는 목표 유형이고 두 번째 인수는 로컬 증명 컨텍스트이며 반환 결과는 고수준 리플렉션과 동일합니다. 이것은 laughadelic이 above에 연결된 것입니다. 이는 증명 모드에서 applyTactic을 사용하여 호출됩니다.
나는 그것을 쓰고 사용하는 방법에 대해서는 아무것도 몰라.하지만 나는 최근에 보았다. [맞춤 전략의 예] (https://github.com/idris-lang/Idris-dev/blob/master) /libs/base/Data/Vect.idr#L18-L22) 및 [사용 예] (https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/) HVect.idr # L57). 희망이 도움이 될 것입니다. – laughedelic
감사합니다. –
위의 링크는 repo의 HEAD를 참조하기 때문에 더 이상 유효하지 않습니다. 대신 여기를 참조하십시오 : [첫 번째] (https://github.com/idris-lang/Idris-dev/blob/10ef56b8c1629347ab213e97bfff551ee27e11d0/libs/base/Data/Vect.idr#L18-L22), [초] (https : //github.com/idris-lang/Idris-dev/blob/fb6a0ed1ad5e3acc3795d7ab674977bdb419129a/libs/base/Data/HVect.idr#L57) –