반성
반성 (Reflection)
- 내장 타입들 (Builtin types)
- 메타프로그래밍 (Metaprogramming)
내장 타입들 (Builtin types)
이름 (Names)
내장 QNAME 타입은 인용된 이름을 나타내며 동등성, 순서, 그리고 show 함수가 함께 제공돼.
postulate Name : Set
{-# BUILTIN QNAME Name #-}
primitive
primQNameEquality : Name → Name → Bool
primQNameLess : Name → Name → Bool
primShowQName : Name → String
이름의 고정도(fixity)도 조회할 수 있어.
primitive
primQNameFixity : Name → Fixity
--safe 옵션으로 일치(matching) 가능한 명제 동등성을 정의하려면, 내장 64비트 기계 단어 쌍으로의 변환을 사용할 수 있어:
primitive
primQNameToWord64s : Name → Σ Word64 (λ _ → Word64)
Properties 모듈의 단사성(injectivity) 증명과 함께 말이야:
primitive
primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b
Name 리터럴은 quote 키워드로 생성되며 용어와 패턴 모두에 나타날 수 있어:
nameOfNat : Name
nameOfNat = quote Nat
isNat : Name → Bool
isNat (quote Nat) = true
isNat _ = false
인용되는 이름은 범위 안에 있어야 한다는 점에 주의해.
메타변수 (Metavariables)
메타변수는 내장 AGDAMETA 타입으로 표현돼. 원시 동등성, 순서, show, 그리고 Nat으로의 변환이 있어:
postulate Meta : Set
{-# BUILTIN AGDAMETA Meta #-}
primitive
primMetaEquality : Meta → Meta → Bool
primMetaLess : Meta → Meta → Bool
primShowMeta : Meta → String
primMetaToNat : Meta → Nat
내장 메타변수는 반성된 용어에 나타나. Properties에는 primMetaToNat의 단사성 증명이 있어:
primitive
primMetaToNatInjective : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b
이것은 --safe 옵션으로 일치 가능한 명제 동등성을 정의하는 데 사용할 수 있어.
리터럴 (Literals)
리터럴은 내장 AGDALITERAL 데이터 타입에 매핑돼. Nat, Float 등의 타입에 대한 적절한 내장 바인딩이 주어지면 AGDALITERAL 데이터 타입은 다음과 같은 형태를 가져:
data Literal : Set where
nat : (n : Nat) → Literal
word64 : (n : Word64) → Literal
float : (x : Float) → Literal
char : (c : Char) → Literal
string : (s : String) → Literal
name : (x : Name) → Literal
meta : (x : Meta) → Literal
{-# BUILTIN AGDALITERAL Literal #-}
{-# BUILTIN AGDALITNAT nat #-}
{-# BUILTIN AGDALITWORD64 word64 #-}
{-# BUILTIN AGDALITFLOAT float #-}
{-# BUILTIN AGDALITCHAR char #-}
{-# BUILTIN AGDALITSTRING string #-}
{-# BUILTIN AGDALITQNAME name #-}
{-# BUILTIN AGDALITMETA meta #-}
인자 (Arguments)
인자는 (가시적), {숨김}, 또는 {{인스턴스}}가 될 수 있어:
data Visibility : Set where
visible hidden instance′ : Visibility
{-# BUILTIN HIDING Visibility #-}
{-# BUILTIN VISIBLE visible #-}
{-# BUILTIN HIDDEN hidden #-}
{-# BUILTIN INSTANCE instance′ #-}
인자는 관련(relevant)이거나 비관련(irrelevant)일 수 있어:
data Relevance : Set where
relevant irrelevant : Relevance
{-# BUILTIN RELEVANCE Relevance #-}
{-# BUILTIN RELEVANT relevant #-}
{-# BUILTIN IRRELEVANT irrelevant #-}
인자에는 또한 양(quantity)이 있어:
data Quantity : Set where
quantity-0 quantity-ω : Quantity
{-# BUILTIN QUANTITY Quantity #-}
{-# BUILTIN QUANTITY-0 quantity-0 #-}
{-# BUILTIN QUANTITY-ω quantity-ω #-}
Relevance와 quantity는 모달리티(modality)로 결합돼:
data Modality : Set where
modality : (r : Relevance) (q : Quantity) → Modality
{-# BUILTIN MODALITY Modality #-}
{-# BUILTIN MODALITY-CONSTRUCTOR modality #-}
가시성과 모달리티는 인자의 동작을 특징짓는다:
data ArgInfo : Set where
arg-info : (v : Visibility) (m : Modality) → ArgInfo
data Arg (A : Set) : Set where
arg : (i : ArgInfo) (x : A) → Arg A
{-# BUILTIN ARGINFO ArgInfo #-}
{-# BUILTIN ARGARGINFO arg-info #-}
{-# BUILTIN ARG Arg #-}
{-# BUILTIN ARGARG arg #-}
이름 추상화 (Name abstraction)
data Abs (A : Set) : Set where
abs : (s : String) (x : A) → Abs A
{-# BUILTIN ABS Abs #-}
{-# BUILTIN ABSABS abs #-}
용어 (Terms)
용어, 소트, 패턴, 절은 상호 재귀적이며 각각 AGDATERM, AGDASORT, AGDAPATTERN, AGDACLAUSE 내장에 매핑돼. 타입은 단순히 용어야. 용어와 패턴은 변수를 나타내기 위해 de Bruijn 지수를 사용해:
data Term : Set
data Sort : Set
data Pattern : Set
data Clause : Set
Type = Term
Telescope = List (Σ String λ _ → Arg Type)
data Term where
var : (x : Nat) (args : List (Arg Term)) → Term
con : (c : Name) (args : List (Arg Term)) → Term
def : (f : Name) (args : List (Arg Term)) → Term
lam : (v : Visibility) (t : Abs Term) → Term
pat-lam : (cs : List Clause) (args : List (Arg Term)) → Term
pi : (a : Arg Type) (b : Abs Type) → Term
agda-sort : (s : Sort) → Term
lit : (l : Literal) → Term
meta : (x : Meta) → List (Arg Term) → Term
unknown : Term -- Treated as '_' when unquoting.
data Sort where
set : (t : Term) → Sort -- A Set of a given (possibly neutral) level.
lit : (n : Nat) → Sort -- A Set of a given concrete level.
prop : (t : Term) → Sort -- A Prop of a given (possibly neutral) level.
propLit : (n : Nat) → Sort -- A Prop of a given concrete level.
inf : (n : Nat) → Sort -- Setωi of a given concrete level i.
unknown : Sort
data Pattern where
con : (c : Name) (ps : List (Arg Pattern)) → Pattern
dot : (t : Term) → Pattern
var : (x : Nat ) → Pattern
lit : (l : Literal) → Pattern
proj : (f : Name) → Pattern
absurd : (x : Nat) → Pattern -- Absurd patterns have de Bruijn indices
data Clause where
clause : (tel : Telescope) (ps : List (Arg Pattern)) (t : Term) → Clause
absurd-clause : (tel : Telescope) (ps : List (Arg Pattern)) → Clause
{-# BUILTIN AGDATERM Term #-}
{-# BUILTIN AGDASORT Sort #-}
{-# BUILTIN AGDAPATTERN Pattern #-}
{-# BUILTIN AGDACLAUSE Clause #-}
{-# BUILTIN AGDATERMVAR var #-}
{-# BUILTIN AGDATERMCON con #-}
{-# BUILTIN AGDATERMDEF def #-}
{-# BUILTIN AGDATERMMETA meta #-}
{-# BUILTIN AGDATERMLAM lam #-}
{-# BUILTIN AGDATERMEXTLAM pat-lam #-}
{-# BUILTIN AGDATERMPI pi #-}
{-# BUILTIN AGDATERMSORT agda-sort #-}
{-# BUILTIN AGDATERMLIT lit #-}
{-# BUILTIN AGDATERMUNSUPPORTED unknown #-}
{-# BUILTIN AGDASORTSET set #-}
{-# BUILTIN AGDASORTLIT lit #-}
{-# BUILTIN AGDASORTPROP prop #-}
{-# BUILTIN AGDASORTPROPLIT propLit #-}
{-# BUILTIN AGDASORTINF inf #-}
{-# BUILTIN AGDASORTUNSUPPORTED unknown #-}
{-# BUILTIN AGDAPATCON con #-}
{-# BUILTIN AGDAPATDOT dot #-}
{-# BUILTIN AGDAPATVAR var #-}
{-# BUILTIN AGDAPATLIT lit #-}
{-# BUILTIN AGDAPATPROJ proj #-}
{-# BUILTIN AGDAPATABSURD absurd #-}
{-# BUILTIN AGDACLAUSECLAUSE clause #-}
{-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}
터무니없는 람다(부조리 람다) λ ()는 부조리 절을 가진 확장 람다로 인용돼. 내장 생성자 AGDATERMUNSUPPORTED와 AGDASORTUNSUPPORTED는 언쿼팅할 때 메타변수로 번역돼.
선언 (Declarations)
정의를 나타내는 내장 타입 AGDADEFINITION이 있어. 이 타입의 값은 아래에 설명된 AGDATCMGETDEFINITION 내장이 반환해:
data Definition : Set where
function : (cs : List Clause) → Definition
data-type : (pars : Nat) (cs : List Name) → Definition -- parameters and constructors
record-type : (c : Name) (fs : List (Arg Name)) → -- c: name of record constructor
Definition -- fs: fields
data-cons : (d : Name) (q : Quantity) → Definition -- d: name of data type
-- q: constructor quantity
axiom : Definition
prim-fun : Definition
{-# BUILTIN AGDADEFINITION Definition #-}
{-# BUILTIN AGDADEFINITIONFUNDEF function #-}
{-# BUILTIN AGDADEFINITIONDATADEF data-type #-}
{-# BUILTIN AGDADEFINITIONRECORDDEF record-type #-}
{-# BUILTIN AGDADEFINITIONDATACONSTRUCTOR data-cons #-}
{-# BUILTIN AGDADEFINITIONPOSTULATE axiom #-}
{-# BUILTIN AGDADEFINITIONPRIMITIVE prim-fun #-}
타입 오류 (Type errors)
타입 검사 계산(아래 참조)은 오류, 즉 ErrorPart 목록으로 실패할 수 있어. 이것은 메타프로그램이 반성된 용어에 대한 예쁜 인쇄를 구현하지 않고도 멋진 오류를 생성하게 해줘.
-- Error messages can contain embedded names and terms.
data ErrorPart : Set where
strErr : String → ErrorPart
termErr : Term → ErrorPart
pattErr : Pattern → ErrorPart
nameErr : Name → ErrorPart
{-# BUILTIN AGDAERRORPART ErrorPart #-}
{-# BUILTIN AGDAERRORPARTSTRING strErr #-}
{-# BUILTIN AGDAERRORPARTTERM termErr #-}
{-# BUILTIN AGDAERRORPARTNAME nameErr #-}
차단기 (Blockers)
차단기는 반성 계산의 진행을 막는 메타변수들의 집합을 나타내. (예를 들어) 매크로가 훑은 용어의 모든 메타를 포함하는 차단기를 사용하는 것은 메타들을 개별적으로 마주칠 때마다 차단하는 것보다 훨씬 효율적이야.
data Blocker : Set where
blockerAny : List Blocker → Blocker
blockerAll : List Blocker → Blocker
blockerMeta : Meta → Blocker
{-# BUILTIN AGDABLOCKER Blocker #-}
{-# BUILTIN AGDABLOCKERANY blockerAny #-}
{-# BUILTIN AGDABLOCKERALL blockerAll #-}
{-# BUILTIN AGDABLOCKERMETA blockerMeta #-}
타입 검사 계산 (Type checking computations)
메타프로그램, 즉 다른 프로그램을 만드는 프로그램은 내장 타입 검사 모나드 TC에서 실행돼:
postulate
TC : ∀ {a} → Set a → Set a
returnTC : ∀ {a} {A : Set a} → A → TC A
bindTC : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
{-# BUILTIN AGDATCM TC #-}
{-# BUILTIN AGDATCMRETURN returnTC #-}
{-# BUILTIN AGDATCMBIND bindTC #-}
TC 모나드는 다음 원시 연산들을 사용해 Agda 타입 검사기에 대한 인터페이스를 제공해:
postulate
-- Unify two terms, potentially solving metavariables in the process.
unify : Term → Term → TC ⊤
-- Throw a type error. Can be caught by catchTC.
typeError : ∀ {a} {A : Set a} → List ErrorPart → TC A
-- Block a type checking computation on a blocker. This will abort
-- the computation and restart it (from the beginning) when the
-- blocker has been solved.
blockTC : ∀ {a} {A : Set a} → Blocker → TC A
-- Prevent current solutions of metavariables from being rolled back in
-- case 'blockOnMeta' is called.
commitTC : TC ⊤
-- Backtrack and try the second argument if the first argument throws a
-- type error.
catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
-- Infer the type of a given term
inferType : Term → TC Type
-- Check a term against a given type. This may resolve implicit arguments
-- in the term, so a new refined term is returned. Can be used to create
-- new metavariables: newMeta t = checkType unknown t
checkType : Term → Type → TC Term
-- Compute the normal form of a term.
normalise : Term → TC Term
-- Compute the weak head normal form of a term.
reduce : Term → TC Term
-- Get the current context. Returns the context in reverse order, so that
-- it is indexable by deBruijn index. Note that the types in the context are
-- valid in the rest of the context. To use in the current context they need
-- to be weakened by 1 + their position in the list.
getContext : TC Telescope
-- Extend the current context with a variable of the given type and its name.
extendContext : ∀ {a} {A : Set a} → String → Arg Type → TC A → TC A
-- Set the current context relative to the context the TC computation
-- is invoked from. Takes a context telescope entries in reverse
-- order, as given by `getContext`. Each type should be valid in the
-- context formed by the remaining elements in the list.
inContext : ∀ {a} {A : Set a} → Telescope → TC A → TC A
-- Quote a value, returning the corresponding Term.
quoteTC : ∀ {a} {A : Set a} → A → TC Term
-- Unquote a Term, returning the corresponding value.
unquoteTC : ∀ {a} {A : Set a} → Term → TC A
-- Quote a value in Setω, returning the corresponding Term
quoteωTC : ∀ {A : Setω} → A → TC Term
-- Create a fresh name.
freshName : String → TC Name
-- Declare a new function of the given type. The function must be defined
-- later using 'defineFun'. Takes an Arg Name to allow declaring instances
-- and irrelevant functions. The Visibility of the Arg must not be hidden.
declareDef : Arg Name → Type → TC ⊤
-- Declare a new postulate of the given type. The Visibility of the Arg
-- must not be hidden. It fails when executed from command-line with --safe
-- option.
declarePostulate : Arg Name → Type → TC ⊤
-- Declare a new datatype. The second argument is the number of parameters.
-- The third argument is the type of the datatype, i.e. its parameters and
-- indices. The datatype must be defined later using 'defineData'.
declareData : Name → Nat → Type → TC ⊤
-- Define a declared datatype. The datatype must have been declared using
-- 'declareData`. The second argument is a list of triples in which each triple
-- is the name of a constructor, its erasure status and its type.
defineData : Name → List (Σ Name (λ _ → Σ Quantity (λ _ → Type))) → TC ⊤
-- Define a declared function. The function may have been declared using
-- 'declareDef' or with an explicit type signature in the program.
defineFun : Name → List Clause → TC ⊤
-- Get the type of a defined name relative to the current
-- module. Replaces 'primNameType'.
getType : Name → TC Type
-- Get the definition of a defined name relative to the current
-- module. Replaces 'primNameDefinition'.
getDefinition : Name → TC Definition
-- Check if a name refers to a macro
isMacro : Name → TC Bool
-- Generate FOREIGN pragma with specified backend and top-level backend-dependent text.
pragmaForeign : String → String → TC ⊤
-- Generate COMPILE pragma with specified backend, associated name and backend-dependent text.
pragmaCompile : String → Name → String → TC ⊤
-- Change the behaviour of inferType, checkType, quoteTC, getContext
-- to normalise (or not) their results. The default behaviour is no
-- normalisation.
withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
askNormalisation : TC Bool
-- If 'true', makes the following primitives to reconstruct hidden arguments:
-- getDefinition, normalise, reduce, inferType, checkType and getContext
withReconstructed : ∀ {a} {A : Set a} → Bool → TC A → TC A
askReconstructed : TC Bool
-- Whether implicit arguments at the end should be turned into metavariables
withExpandLast : ∀ {a} {A : Set a} → Bool → TC A → TC A
askExpandLast : TC Bool
-- White/blacklist specific definitions for reduction while executing the TC computation
-- 'true' for whitelist, 'false' for blacklist
withReduceDefs : ∀ {a} {A : Set a} → (Σ Bool λ _ → List Name) → TC A → TC A
askReduceDefs : TC (Σ Bool λ _ → List Name)
-- Parse and type check the given string against the given type, returning
-- the resulting term (when successful).
checkFromStringTC : String → Type → TC Term
-- Prints the third argument to the debug buffer in Emacs
-- if the verbosity level (set by the -v flag to Agda)
-- is higher than the second argument. Note that Level 0 and 1 are printed
-- to the info buffer instead. For instance, giving -v a.b.c:10 enables
-- printing from debugPrint "a.b.c.d" 10 msg.
debugPrint : String → Nat → List ErrorPart → TC ⊤
-- Return the formatted string of the argument using the internal pretty printer.
formatErrorParts : List ErrorPart → TC String
-- Fail if the given computation gives rise to new, unsolved
-- "blocking" constraints.
noConstraints : ∀ {a} {A : Set a} → TC A → TC A
-- Run the given computation at the type level, allowing use of erased things.
workOnTypes : ∀ {a} {A : Set a} → TC A → TC A
-- Run the given TC action and return the first component. Resets to
-- the old TC state if the second component is 'false', or keep the
-- new TC state if it is 'true'.
runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
-- Get a list of all possible instance candidates for the given meta
-- variable (it does not have to be an instance meta).
getInstances : Meta → TC (List Term)
-- Try to solve open instance constraints. When wrapped in `noConstraints`,
-- fails if there are unsolved instance constraints left over that originate
-- from the current macro invokation. Outside constraints are still attempted,
-- but failure to solve them are ignored by `noConstraints`.
solveInstanceConstraints : TC ⊤
{-# BUILTIN AGDATCMUNIFY unify #-}
{-# BUILTIN AGDATCMTYPEERROR typeError #-}
{-# BUILTIN AGDATCMBLOCK blockTC #-}
{-# BUILTIN AGDATCMCATCHERROR catchTC #-}
{-# BUILTIN AGDATCMINFERTYPE inferType #-}
{-# BUILTIN AGDATCMCHECKTYPE checkType #-}
{-# BUILTIN AGDATCMNORMALISE normalise #-}
{-# BUILTIN AGDATCMREDUCE reduce #-}
{-# BUILTIN AGDATCMGETCONTEXT getContext #-}
{-# BUILTIN AGDATCMEXTENDCONTEXT extendContext #-}
{-# BUILTIN AGDATCMINCONTEXT inContext #-}
{-# BUILTIN AGDATCMQUOTETERM quoteTC #-}
{-# BUILTIN AGDATCMUNQUOTETERM unquoteTC #-}
{-# BUILTIN AGDATCMQUOTEOMEGATERM quoteωTC #-}
{-# BUILTIN AGDATCMFRESHNAME freshName #-}
{-# BUILTIN AGDATCMDECLAREDEF declareDef #-}
{-# BUILTIN AGDATCMDECLAREPOSTULATE declarePostulate #-}
{-# BUILTIN AGDATCMDECLAREDATA declareData #-}
{-# BUILTIN AGDATCMDEFINEDATA defineData #-}
{-# BUILTIN AGDATCMDEFINEFUN defineFun #-}
{-# BUILTIN AGDATCMGETTYPE getType #-}
{-# BUILTIN AGDATCMGETDEFINITION getDefinition #-}
{-# BUILTIN AGDATCMCOMMIT commitTC #-}
{-# BUILTIN AGDATCMISMACRO isMacro #-}
{-# BUILTIN AGDATCMPRAGMAFOREIGN pragmaForeign #-}
{-# BUILTIN AGDATCMPRAGMACOMPILE pragmaCompile #-}
{-# BUILTIN AGDATCMWITHNORMALISATION withNormalisation #-}
{-# BUILTIN AGDATCMWITHRECONSTRUCTED withReconstructed #-}
{-# BUILTIN AGDATCMWITHEXPANDLAST withExpandLast #-}
{-# BUILTIN AGDATCMWITHREDUCEDEFS withReduceDefs #-}
{-# BUILTIN AGDATCMASKNORMALISATION askNormalisation #-}
{-# BUILTIN AGDATCMASKRECONSTRUCTED askReconstructed #-}
{-# BUILTIN AGDATCMASKEXPANDLAST askExpandLast #-}
{-# BUILTIN AGDATCMASKREDUCEDEFS askReduceDefs #-}
{-# BUILTIN AGDATCMDEBUGPRINT debugPrint #-}
{-# BUILTIN AGDATCMNOCONSTRAINTS noConstraints #-}
{-# BUILTIN AGDATCMWORKONTYPES workOnTypes #-}
{-# BUILTIN AGDATCMRUNSPECULATIVE runSpeculative #-}
{-# BUILTIN AGDATCMGETINSTANCES getInstances #-}
{-# BUILTIN AGDATCMSOLVEINSTANCES solveInstanceConstraints #-}
메타프로그래밍 (Metaprogramming)
메타프로그램(TC 계산)을 실행하는 방법은 세 가지가 있어. 용어 위치에서 메타프로그램을 실행하려면 매크로(macro)를 사용해. 최상위 정의를 만들기 위해 메타프로그램을 실행하려면 unquoteDecl과 unquoteDef 원시를 사용할 수 있어 (Unquoting Declarations 참조).
매크로 (Macros)
매크로는 macro 블록에 정의된 타입 t₁ → t₂ → .. → Term → TC ⊤의 함수야. 마지막 인자는 타입 검사기가 공급하며, 그 매크로의 결과로 인스턴스화되어야 할 메타변수의 표현이 될 거야.
매크로 적용은 매크로의 타입에 의해 안내되며, 여기서 Term과 Name 인자는 매크로에 전달되기 전에 인용돼. 그 외의 다른 타입의 인자는 그대로 보존돼.
예를 들어, f : Term → Name → Bool → Term → TC ⊤인 매크로 적용 f u v w는 다음과 같이 디슈거(desugar)돼:
unquote (f (quoteTerm u) (quote v) w)
여기서 quoteTerm u는 임의 타입의 u를 받아 Term 데이터 타입에서의 표현을 반환하고, unquote m은 TC 모나드에서 계산을 실행해. 구체적으로, 어떤 타입 A에 대해 unquote m : A를 검사할 때 타입 검사기는 다음과 같이 진행해:
m : Term → TC ⊤를 검사해.- 새로운 메타변수
hole : A를 만들어. qhole : Term이hole의 인용된 표현이 되게 해.m qhole을 실행해.- (이제 바라건대 인스턴스화된)
hole을 반환해.
반성된 매크로 호출은 def 생성자를 사용해 구성되므로, 매크로 g : Term → TC ⊤가 주어지면 용어 def (quote g) []는 g에 대한 매크로 호출로 언쿼트돼.
참고:
quoteTerm과unquote원시는 언어에서 사용 가능하지만, 매크로를 선호해 그것을 피하는 것이 권장돼.
제한 사항:
- 매크로는 재귀적일 수 없어. 이것은 재귀 함수를 매크로 블록 밖에 정의하고 매크로가 그 재귀 함수를 호출하게 함으로써 우회할 수 있어.
- 매크로와
quoteTerm은 내부에 대화형 구멍(interactive hole)이 있는 용어를 인용할 때 차단될 수 있어.--quote-metas를 활성화해 이 차단을 비활성화하면, 인용된 구멍이 매크로 언쿼팅에 의해 제약될 수 있어.
간단한 예:
macro
plus-to-times : Term → Term → TC ⊤
plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole =
unify hole (def (quote _*_) (a ∷ b ∷ []))
plus-to-times v hole = unify hole v
thm : (a b : Nat) → plus-to-times (a + b) ≡ a * b
thm a b = refl
매크로는 문법적 오버헤드 없이 적용할 수 있는 전술(tactic)을 작성하게 해줘. 예를 들어, 반성된 목표를 받아 (성공 시) 증명을 출력하는 솔버가 있다고 하자:
magic : Type → Term
그러면 다음 매크로를 정의할 수 있어:
macro
by-magic : Term → TC ⊤
by-magic hole =
bindTC (inferType hole) λ goal →
unify hole (magic goal)
이를 통해 magic 전술을 일반 함수처럼 적용할 수 있어:
thm : ¬ P ≡ NP
thm = by-magic
전술 인자 (Tactic Arguments)
@(tactic t) 주석을 사용해 특정 암시 인자를 풀기 위해 사용할 전술을 선언할 수 있어. 제공된 전술은 용어 t : Term → TC ⊤이어야 해. 예를 들어,
defaultTo : {A : Set} (x : A) → Term → TC ⊤
defaultTo x hole = bindTC (quoteTC x) (unify hole)
f : {@(tactic defaultTo true) x : Bool} → Bool
f {x} = x
test-f : f ≡ true
test-f = refl
f 호출에서, x가 명시적으로 주어지지 않으면 x에 대해 삽입된 메타변수에 defaultTo true가 호출돼.
전술은 함수에 대한 이전 인자들에 의존할 수 있어. 예를 들어,
g : (x : Nat) {@(tactic defaultTo x) y : Nat} → Nat
g x {y} = x + y
test-g : g 4 ≡ 8
test-g = refl
레코드 필드도 전술로 주석을 달 수 있어, 생성자 적용, 레코드 구성, 그리고 코-패턴 매칭에서 그것을 생략할 수 있게 해줘:
record Bools : Set where
constructor mkBools
field fst : Bool
@(tactic defaultTo fst) {snd} : Bool
open Bools
tt₀ tt₁ tt₂ tt₃ : Bools
tt₀ = mkBools true {true}
tt₁ = mkBools true
tt₂ = record{ fst = true }
tt₃ .fst = true
test-tt : tt₁ ∷ tt₂ ∷ tt₃ ∷ [] ≡ tt₀ ∷ tt₀ ∷ tt₀ ∷ []
test-tt = refl
선언 언쿼팅 (Unquoting Declarations)
매크로는 용어를 만들기 위한 메타프로그램을 작성하게 해주지만, 최상위 정의를 만드는 것도 유용해. 매크로에서 declareDef, declareData, defineFun, defineData 원시를 사용해 이것을 할 수 있지만, 그런 정의들을 범위 안으로 가져올 방법은 없어. 이 목적을 위해 선언 위치에서 TC 계산을 실행하는 두 개의 최상위 원시 unquoteDecl과 unquoteDef가 있어. 둘 다 함수 정의를 선언하는 데 같은 형식을 가져:
unquoteDecl x₁ .. xₙ = m
unquoteDef x₁ .. xₙ = m
다만 이름 목록이 unquoteDecl에서는 비어 있을 수 있지만 unquoteDef에서는 비어 있을 수 없어. 두 경우 모두 m은 타입 TC ⊤이어야 해. 두 원시의 주요 차이는 unquoteDecl은 m이 xᵢ를 선언(declareDef로)하고 정의(defineFun으로)하는 것을 모두 요구하는 반면, unquoteDef는 xᵢ가 이미 선언되어 있기를 기대한다는 것이야. 다시 말해, unquoteDecl은 xᵢ를 범위 안으로 가져오지만 unquoteDef는 그것들이 이미 범위 안에 있을 것을 요구해.
m에서 xᵢ는 실제 함수가 아니라 정의되는 함수들의 이름을 나타내(즉 xᵢ : Name).
unquoteDef가 unquoteDecl보다 나은 한 가지 장점은 unquoteDef가 mutual 블록에서 허용되어, 생성된 정의와 손으로 작성한 정의 사이의 상호 재귀를 허용한다는 것이야.
사용 예:
arg′ : {A : Set} → Visibility → A → Arg A
arg′ v = arg (arg-info v (modality relevant quantity-ω))
-- Defining: id-name {A} x = x
defId : (id-name : Name) → TC ⊤
defId id-name = do
defineFun id-name
[ clause
( ("A" , arg′ visible (agda-sort (lit 0)))
∷ ("x" , arg′ visible (var 0 []))
∷ [])
( arg′ hidden (var 1)
∷ arg′ visible (var 0)
∷ [] )
(var 0 [])
]
id : {A : Set} (x : A) → A
unquoteDef id = defId id
mkId : (id-name : Name) → TC ⊤
mkId id-name = do
ty ← quoteTC ({A : Set} (x : A) → A)
declareDef (arg′ visible id-name) ty
defId id-name
unquoteDecl id′ = mkId id′
unquoteDecl의 또 다른 형식은 데이터 타입을 선언하는 데 사용돼:
unquoteDecl data x constructor c₁ .. cₙ = m
m은 declareData와 defineData를 사용해 데이터 타입 x와 그 생성자들 c₁부터 cₙ을 선언하고 정의하는 메타프로그램이야.
참고:
unquoteDecl과unquoteDef가 생성한 코드를 디버깅하려면, 상세(verbosity) 플래그-v tc.unquote.decl:10(타입 시그니처용)과-v tc.unquote.def:10(정의 본문용)을 켜는 것이 유용할 수 있어. 이것은 명령줄에서 실행할 때 생성된 코드가 stdout에 인쇄되고, 편집기에서 로드할 때는 디버그 버퍼에 인쇄되게 해.
다른 상세 플래그와 달리, 이 두 가지는 Agda가 debug Cabal 플래그로 빌드되었더라도 사용할 수 있어.
시스템 호출 (System Calls)
메타프로그램의 일부로 시스템 호출을 실행하는 것이 가능해. execTC 빌트인을 사용해서 말이야. 이 기능을 사용해 타입 프로바이더를 구현하거나 외부 솔버를 호출할 수 있어. 예를 들어, 다음 예는 Agda에서 /bin/echo를 호출해:
postulate
execTC : (exe : String) (args : List String) (stdIn : String)
→ TC (Σ Nat (λ _ → Σ String (λ _ → String)))
{-# BUILTIN AGDATCMEXEC execTC #-}
macro
echo : List String → Term → TC ⊤
echo args hole = do
(exitCode , (stdOut , stdErr)) ← execTC "echo" args ""
unify hole (lit (string stdOut))
_ : echo ("hello" ∷ "world" ∷ []) ≡ "hello world\n"
_ = refl
execTC 빌트인은 세 개의 인자를 받아:
- 실행 파일의 기본 이름(basename, 예:
"echo"), - 인자 목록,
- 표준 입력의 내용.
그리고 세 쌍(트리플)을 반환해:
- 종료 코드(자연수로),
- 표준 출력의 내용,
- 표준 오류의 내용.
Agda가 임의의 시스템 호출을 하게 허용하는 것은 현명하지 않을 거야. 따라서 이 기능은 명령줄이나 프래그마로 --allow-exec 옵션을 전달함으로써 활성화해야 해. (--allow-exec는 --safe와 호환되지 않는다는 점에 주의해.)
게다가 Agda는 신뢰할 수 있는 실행 파일 목록인 ~/.agda/executables에 나열된 실행 파일만 호출할 수 있어. 예를 들어 위 예를 실행하려면 /bin/echo를 이 파일에 추가해야 해:
# contents of ~/.agda/executables
/bin/echo
그런 다음 실행 파일을 execTC에 그 기본 이름을 전달해 호출할 수 있어 (Windows에서는 .exe를 제외).
메타 인용 (Quote Metas)
--quote-metas 옵션은 용어에 메타변수가 있어도 용어 인용 제약이 해결될 수 있게 해. 이것은 매크로를 위한 타입 구멍 주도 개발(typed hole-driven development)을 가능하게 하는데, 여기서 매크로에 인용된 인자로 주어진 대화형 구멍의 기대 타입이 매크로의 언쿼팅에 의해 제약될 수 있어.
--quote-metas가 없는 다음 예에서, 대화형 구멍은 제약이 차단되게 하며, 이는 quoteTerm ?0 : Term (blocked on _17)처럼 보이지:
open import Agda.Builtin.Unit
open import Agda.Builtin.Nat
open import Agda.Builtin.List
repeat-helper : Nat → Name → Term → Term
repeat-helper zero f a = a
repeat-helper (suc n) f a = con f ((arg (arg-info visible (modality relevant quantity-ω)) (repeat-helper n f a)) ∷ [])
macro
repeat : Nat → Name → Term → Term → TC ⊤
repeat n f a hole = unify hole (repeat-helper n f a)
_ : Nat
_ = repeat 10 suc {! !}
그러나 실제로 매크로를 언쿼팅하면 대화형 구멍이 타입 ℕ이어야 함이 드러날 거야. --quote-metas를 활성화하면 정확히 이것이 가능해.
{-# OPTIONS --quote-metas #-}
-- ...
ex1 = repeat 10 f {! !}
이제 매크로가 언쿼팅되는데, 이 스플라이스(splied) 코드에서는 구멍의 값에 f를 적용해. 이것은 구멍의 타입을 ℕ으로 제약하고, 사용자는 구멍의 기대 맥락과 타입을 검사해 이것을 배울 수 있어.
참고: 이 예에서 구멍의 타입은 스플라이스된 코드에 의해 제약되지 않으므로, 알 수 없는 추론된 타입을 가질 거야.
ex2 = repeat 0 f {! !}