samedi 27 août 2016

Overview of quasiquotation in Idris

I hadn't realised that Idris has a quasiquotes until I came across some tests in the test suite.

Here's a short example in the REPL:

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

I'd like to understand what that's all about. A brief overview and/or some references would be appreciated!





Aucun commentaire:

Enregistrer un commentaire