Idris 코드 문서화
Idris 코드 문서화 (Documenting Idris Code)
Idris 문서화는 두 가지 주요 형태로 제공돼요: 독자의 교훈을 위해 존재하고 컴파일러는 무시하는 주석(comments), 그리고 컴파일러가 파싱해 미래의 참조를 위해 저장하는 인라인 API 문서. 선언 f에 대한 문서를 열람하려면 REPL에 :doc f를 작성하거나, 편집기에서 적절한 명령을 사용해요 (Emacs에서는 C-c C-d, Vim에서는 <LocalLeader>h).
출처: 문서
본문
주석 (Comments)
주석을 사용해 코드가 왜 그렇게 작성되었는지 설명해요. Idris의 주석 문법은 Haskell의 그것과 같아요: --로 시작하는 줄은 주석이고, {-와 -}로 묶인 영역은 여러 줄에 걸쳐 있어도 주석이에요. 이것들은 코드 줄을 주석 처리하거나 Idris 코드 독자에게 간단한 문서를 제공하는 데 사용할 수 있어요.
인라인 문서 (Inline Documentation)
Idris는 Idris 코드가 생성되도록 하는 포괄적이고 풍부한 인라인 문법을 지원해요. 이 문법은 또한 Javadoc 매개변수 주석과 유사한 문법을 사용해 타입 시그니처 안의 이름 있는 매개변수와 변수를 개별적으로 주석을 달 수 있게 해줘요.
문서화는 항상 문서화되는 선언 앞에 와요. 인라인 문서는 최상위 선언 또는 생성자에 적용돼요. 생성자, 타입 생성자, 또는 함수의 특정 인자에 대한 문서는 이름을 사용해 그 인자들과 연관시킬 수 있어요.
선언에 대한 인라인 문서는 각 줄이 |||(파이프 기호 세 개)로 시작하는 끊기지 않는 줄들의 문자열이에요. 문서의 첫 번째 문단은 개요(overview)로 간주되며, 일부 맥락에서는 이 개요만 표시돼요. 선언 전체에 대한 문서 후, 특정 이름 있는 매개변수와 문서를 연관시킬 수 있어요. 그것은 명시적으로 이름이 붙거나 자유 변수를 묵시적 매개변수로 변환한 결과일 수 있어요. 주석은 Javadoc 주석과 같아요. 즉, 이름 있는 매개변수 (n : T)에 대해, 대응하는 주석은 선언 앞에 놓이는 ||| @ n Some description that is이에요.
문서는 Markdown으로 작성돼요. 다만 모든 맥락이 모든 가능한 서식을 표시하지는 않아요 (예를 들어, REPL에서 문서를 볼 때 이미지는 표시되지 않고, 일부 터미널만 이탤릭을 올바르게 렌더링해요). 포괄적인 예시 집합이 아래에 주어져 있어요.
||| Modules can also be documented.
module Docs
||| Add some numbers.
|||
||| Addition is really great. This paragraph is not part of the overview.
||| Still the same paragraph.
|||
||| You can even provide examples which are inlined in the documentation:
||| ```idris example
||| add 4 5
||| ```
|||
||| Lists are also nifty:
||| * Really nifty!
||| * Yep!
||| * The name `add` is a **bold** choice
||| @ n is the recursive param
||| @ m is not
add : (n, m : Nat) -> Nat
add Z m = m
add (S n) m = S (add n m)
||| Append some vectors
||| @ a the contents of the vectors
||| @ xs the first vector (recursive param)
||| @ ys the second vector (not analysed)
appendV : (xs : Vect n a) -> (ys : Vect m a) -> Vect (add n m) a
appendV [] ys = ys
appendV (x::xs) ys = x :: appendV xs ys
||| Here's a simple datatype
data Ty =
||| Unit
UNIT |
||| Functions
ARR Ty Ty
||| Points to a place in a typing context
data Elem : Vect n Ty -> Ty -> Type where
Here : {ts : Vect n Ty} -> Elem (t::ts) t
There : {ts : Vect n Ty} -> Elem ts t -> Elem (t'::ts) t
||| A more interesting datatype
||| @ n the number of free variables
||| @ ctxt a typing context for the free variables
||| @ ty the type of the term
data Term : (ctxt : Vect n Ty) -> (ty : Ty) -> Type where
||| The constructor of the unit type
||| More comment
||| @ ctxt the typing context
UnitCon : {ctxt : Vect n Ty} -> Term ctxt UNIT
||| Function application
||| @ f the function to apply
||| @ x the argument
App : {ctxt : Vect n Ty} -> (f : Term ctxt (ARR t1 t2)) -> (x : Term ctxt t1) -> Term ctxt t2
||| Lambda
||| @ body the function body
Lam : {ctxt : Vect n Ty} -> (body : Term (t1::ctxt) t2) -> Term ctxt (ARR t1 t2)
||| Variables
||| @ i de Bruijn index
Var : {ctxt : Vect n Ty} -> (i : Elem ctxt t) -> Term ctxt t
||| A computation that may someday finish
codata Partial : Type -> Type where
||| A finished computation
||| @ value the result
Now : (value : a) -> Partial a
||| A not-yet-finished computation
||| @ rest the remaining work
Later : (rest : Partial a) -> Partial a
||| We can document records, including their fields and constructors
record Yummy where
||| Make a yummy
constructor MkYummy
||| What to eat
food : String