IDE 프로토콜
IDE 프로토콜 (The IDE Protocol)
Idris REPL에는 두 가지 상호작용 모드가 있어요: 터미널에서 직접 사용하기 위해 설계된 사람이 읽을 수 있는 문법, 그리고 외부 도구의 백엔드로 Idris를 사용하기 위해 설계된 기계가 읽을 수 있는 문법.
출처: 문서
본문
프로토콜 개요 (Protocol Overview)
통신 프로토콜은 비동기 요청-응답 스타일이에요: 클라이언트의 단일 요청은 Idris가 한 번에 하나씩 처리해요.
Idris는 표준 입력 스트림에서 요청을 기다리고, 답(또는 답들)을 표준 출력으로 출력해요.
요청의 결과는 성공, 실패, 또는 중간 출력일 수 있어요; 그리고 결과가 전달되기 전에 추가 메타-메시지가 있을 수도 있어요.
응답은 여러 메시지로 구성될 수 있어요: 요청의 진행 상황이나 다른 정보 출력에 대해 사용자에게 알리는 임의의 수의 메시지, 그리고 마지막에 결과(ok 또는 error)가 있어요.
온-더-와이어 형식은 메시지의 길이를 문자 수로, 6자리 16진수로 인코딩한 다음, S-표현식(sexp)으로 인코딩된 메시지가 뒤따르는 것이에요.
추가로, 각 요청은 (위로 세는) 고유한 정수를 포함하고, 그 정수는 그 요청에 대응하는 모든 메시지에서 반복돼요.
/home/hannes/empty.idr 파일을 로드하는 상호작용의 예시는 와이어 상에서 다음과 같아요:
00002a((:load-file "/home/hannes/empty.idr") 1)
000039(:write-string "Type checking /home/hannes/empty.idr" 1)
000025(:set-prompt "/home/hannes/empty" 1)
000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)
첫 번째 메시지는 idris-mode가 특정 파일을 로드하라는 요청이며, 그 길이는 16진수 2a, 십진수 42예요 (끝의 줄바꿈 포함).
요청 식별자는 1로 설정돼요.
Idris의 첫 번째 메시지는 문자열 Type checking /home/hannes/empty.idr을 쓰는 것이고, 다른 하나는 프롬프트를 /home/hannes/empty로 설정하는 것이에요.
:return으로 시작하는 답은 ok이며, 추가 정보로 파일이 로드되었다는 내용이에요.
와이어 언어에는 세 가지 원자(atom)가 있어요: 숫자, 문자열, 심볼.
유일한 복합 객체는 리스트이며, 괄호로 둘러싸여 있어요.
문법은:
A ::= NUM | '"' STR '"' | ':' ALPHA+
S ::= A | '(' S* ')' | nil
여기서 NUM은 0 또는 양의 정수, ALPHA는 알파벳 문자, STR은 문자열의 내용으로 "는 백슬래시로 이스케이프돼요.
일부 regexp pretty-printing 루틴과의 호환성을 위해 원자 nil이 () 대신 받아들여져요.
Idris 프로세스의 상태는 주로 활성 파일이며, 편집기와 Idris 사이에 동기화되어 유지되어야 해요.
이것은 이미 본 :load-file 명령으로 달성돼요.
사용 가능한 명령들은 다음과 같아요:
(:load-file FILENAME [LINE])
이름이 있는 파일을 로드해요. LINE 번호가 제공되면, 파일이 그 줄까지만 로드돼요. 그렇지 않으면 파일 전체가 로드돼요.
(:interpret STRING)
Idris REPL에서 STRING을 해석하고, 형광(highlighted)된 결과를 반환해요.
(:type-of STRING)
STRING에 Idris 문법으로 쓰인 이름의 타입을 반환해요. 응답은 형광 정보를 포함할 수 있어요.
(:case-split LINE NAME)
프로그램 줄 LINE의 패턴 변수 NAME에 대한 case-분할을 생성해요. 대체될 패턴-매칭 경우들은 형광 없는 문자열로 반환돼요.
(:add-clause LINE NAME)
프로그램 줄 LINE에서 NAME으로 선언된 함수에 대한 초기 패턴-매칭 절을 생성해요. 초기 절은 형광 없는 문자열로 반환돼요.
(:add-proof-clause LINE NAME)
<== 문법에 의해 구동되는 절을 추가해요.
(:add-missing LINE NAME)
프로그램 줄 LINE의 NAME으로 선언된 함수를 전체성 검사함으로써 발견된 누락된 case들을 추가해요. 누락된 절들은 형광 없는 문자열로 반환돼요.
(:make-with LINE NAME)
줄 LINE의 함수 NAME의 절에 대한 with-규칙 패턴 매칭 템플릿을 만들어요. 새 코드는 형광 없이 반환돼요.
(:make-case LINE NAME)
줄 LINE의 함수 NAME의 절에 대한 case 패턴 매칭 템플릿을 만들어요. 새 코드는 형광 없이 반환돼요.
(:make-lemma LINE NAME)
줄 LINE에서 NAME으로 이름 붙은 hole을 해결하는 타입을 가진 최상위 함수를 만들어요.
(:proof-search LINE NAME HINTS)
증명 검색으로 LINE의 NAME으로 이름 붙은 hole들을 채우려 시도해요. HINTS는 검색하는 동안 시도할 추가 사항들의, 아마 비어 있는 리스트예요.
(:docs-for NAME [MODE])
NAME의 문서를 찾고 형광 문자열로 반환해요. MODE가 :overview이면, NAME에 대해 문서의 첫 문단만 제공돼요. MODE가 :full이거나 생략되면, NAME에 대해 전체 문서가 반환돼요.
(:apropos STRING)
STRING의 언급을 위해 문서를 검색하고, 발견된 것들을 형광 문자열들의 리스트로 반환해요.
(:metavariables WIDTH)
현재-활성인 hole들을, WIDTH 열로 pretty-print된 타입과 함께 나열해요.
(:who-calls NAME)
NAME의 호출자 목록을 가져와요.
(:calls-who NAME)
NAME의 피호출자 목록을 가져와요.
(:browse-namespace NAMESPACE)
커맨드-라인 REPL의 :browse처럼 NAMESPACE의 내용을 반환해요.
(:normalise-term TM)
직렬화된 용어 TM(이전에는 문자열의 tt-term 속성으로 보냈을 것)을 정규화한 결과로 구성된 형광 문자열을 반환해요.
(:show-term-implicits TM)
직렬화된 용어 TM(이전에는 문자열의 tt-term 속성으로 보냈을 것)의 모든 인자를 명시적으로 만든 결과로 구성된 형광 문자열을 반환해요.
(:hide-term-implicits TM)
직렬화된 용어 TM(이전에는 문자열의 tt-term 속성으로 보냈을 것)의 모든 인자를 그들의 평소 묵시성 설정을 따르게 만든 결과로 구성된 형광 문자열을 반환해요.
(:elaborate-term TM)
직렬화된 용어 TM(이전에는 문자열의 tt-term 속성으로 보냈을 것)에 대응하는 코어 언어 용어로 구성된 형광 문자열을 반환해요.
(:print-definition NAME)
NAME의 정의를 형광 문자열로 반환해요.
(:repl-completions NAME)
NAME을 포함하는 이름, 타입, 문서를 검색해요. NAME을 REPL 명령으로 탭-완성한 결과를 반환해요.
:version
Idris 컴파일러의 버전 정보를 반환해요.
가능한 응답에는 정상적인 최종 응답이 포함돼요:
(:return (:ok SEXP [HIGHLIGHTING]))
(:return (:error String [HIGHLIGHTING]))
정상적인 중간 응답:
(:output (:ok SEXP [HIGHLIGHTING]))
(:output (:error String [HIGHLIGHTING]))
정보성 및/또는 비정상 응답:
(:write-string String)
(:set-prompt String)
(:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]))
증명 모드 응답:
(:start-proof-mode)
(:write-proof-state [String] [HIGHLIGHTING])
(:end-proof-mode)
(:write-goal String)
출력 형광 (Output Highlighting)
Idris 모드는 Idris로부터의 출력 형광을 지원해요.
실제로 이 형광은 Idris 컴파일러에 의해 제어돼요.
Idris의 일부 반환 형식은 선택적인 추가 매개변수를 지원해요: 텍스트의 범위(span)들을 그 텍스트에 대한 메타데이터에 매핑하는 리스트예요.
클라이언트는 이 리스트를 사용해 표시된 출력을 형광 처리하고, 더 많은 메타데이터가 존재함으로써 더 풍부한 상호작용을 가능하게 할 수 있어요.
예를 들어, Emacs 모드는 식별자를 오른쪽-클릭해 문서와 타입 시그니처에 접근하는 메뉴를 얻을 수 있게 해줘요.
특정 의미 범위(semantic span)는 세 요소 리스트예요.
리스트의 첫 번째 요소는 범위가 시작하는 인덱스, 두 번째 요소는 범위에 포함된 문자 수, 세 번째는 의미 데이터 자체예요.
의미 데이터는 리스트들의 리스트예요.
각 리스트의 머리(head)는 리스트에 어떤 종류의 메타데이터가 있는지를 나타내는 키(key)이고, 꼬리(tail)는 메타데이터 자체예요.
다음 키들이 사용 가능해요:
name
완전히 한정된 Idris 이름에 대한 참조를 줘요.
implicit
그 영역이 묵시적 인자의 이름이면 True인 Boolean 값을 제공해요.
decor
토큰의 카테고리를 설명하며, type, function, data, keyword, 또는 bound일 수 있어요.
source-loc
그 영역이 소스 코드 위치를 참조한다는 것을 명시해요. 그 본문은 키-값 쌍의 모음이며, 다음과 같은 가능성이 있어요:
filename 파일 이름을 제공해요.
start 소스 위치가 시작하는 줄과 열을 두 요소 꼬리로 제공해요.
end 소스 위치가 끝나는 줄과 열을 두 요소 꼬리로 제공해요.
text-formatting
형식화된 텍스트의 속성을 제공해요. 이것은 자연어 텍스트(코드 아님)용으로, 현재는 인라인 문서에서만 방출돼요. 잠재적 값은 bold, italic, underline이에요.
link-href 대응하는 텍스트가 링크인 URL을 제공해요.
quasiquotation 그 영역이 quasiquote되었음을 명시해요.
antiquotation 그 영역이 antiquote되었음을 명시해요.
tt-term 텍스트 영역에 대응하는 Idris 코어 용어의 직렬화된 표현.
소스 코드 형광 (Source Code Highlighting)
Idris는 편집기에게 코드를 어떻게 색칠할지 지시하는 것을 지원해요.
소스 코드나 REPL 입력을 정교화할 때, Idris는 이름에 대응하는 소스 코드의 영역을 찾고, 출력 형광과 같은 메타데이터를 사용해 이 이름들에 대한 정보를 방출해요.
이 메시지들은 정교화를 일으킨 명령(예: :load-file 또는 :interpret)에 대한 응답으로 도착할 거예요.
그것들은 다음 형식을 가지고 있어요:
(:output (:ok (:highlight-source POSNS)))
여기서 POSNS는 형광 처리할 위치들의 리스트예요. 각각은 두 요소 리스트인데, 그 첫 요소는 위치(위의 source-loc 속성처럼 인코딩됨)이고, 두 번째 요소는 출력에 사용된 것과 같은 형식의 형광 메타데이터예요.