Обзор квазиоборота в Идрисе

Question

Я не осознавал, что у Идриса квазиквартиры, пока я не наткнулся на some tests in the test suite.

Вот краткий пример в РЕПЛ:

Idris> :module Language.Reflection 
Idris> `(S Z) 
App (P (DCon 1 1) 
     (NS (UN "S") ["Nat", "Prelude"]) 
     (Bind (MN 0 "_t") 
      (Pi (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased) 
       (TType (UVar "./Prelude/Nat.idr" 22))) 
      (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased))) 
    (P (DCon 0 0) 
     (NS (UN "Z") ["Nat", "Prelude"]) 
     (P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)) : TT 

Я хотел бы понять, что это все о. Краткий обзор и/или некоторые ссылки будут оценены!

Answer 1

В статье Elaborator Reflection: Extending Idris in Idris определяет представление Идриса основного языка Идриса под названием TT:

язык ядра представлены двумя отдельных типов данных: Raw и TT. Raw используется для представления терминов, которые должны быть отправлены , чтобы проверить тип, а TT представляет собой термины, произведенные контролером типа.

Рисунок 3 дает следующую схему Raw и TT:

-- Variable names 
data TTName = ... 

-- Constants 
data Const = I Int | Str String | ... 

-- Binders 
data Binder : (tmTy : Type) -> Type where 
    Lam : (ty : a) -> Binder a 
    Pi : (ty, kind : a) -> Binder a 
    Let : (ty, val : a) -> Binder a 
    PVar : (ty : a) -> Binder a 
    Hole : (ty : a) -> Binder a 
    Guess : (ty, val : a) -> Binder a 

-- Terms which have not yet been typechecked 
data Raw = Var TTName 
    | RBind TTName (Binder Raw) Raw 
    | RApp Raw Raw 
    | RType 
    | RConstant Const 

-- Well typed, de Bruijn indexed terms 
data TT = P NameType TTName TT 
    | V Int 
    | Bind TTName (Binder TT) TT 
    | App TT TT 
    | TConst Const 
    | TType TTUExp 

Он также ссылается на бумагу Type-Directed Elaboration of Quasiquotations, что описанный механизм quasiquotation.