idris-lang/Idris-dev — pull request #1331 by david-christiansen (2014-06-25 22:11:33+00:00)
Title: Quasiquote support

This PR introduces quasiquotes for reflected terms. Examples:

```
module Quasiquote

import Language.Reflection
import Language.Reflection.Utils

nat : TT
nat = `(Nat)

three : TT
three = `(S (S (S Z)))

twoElems : TT
twoElems = `(with List [(), ()])

copy : TT -> TT
copy q = `((~q,~q))

thing : TT -> TT
thing tm = `(with List [Type, ~tm])

getTyArg : TT -> Maybe TT
getTyArg `(~f ~x) = Just x
getTyArg _ = Nothing
```

and then:
```
*Quasiquote> nat
P (TCon 15 0)
(NS (UN "Nat") ["Nat", "Prelude"])
(TType (UVar -1)) : TT
*Quasiquote> three
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))
(P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)))
(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))
(P (TCon 0 0) (NS (UN "Nat") ["Nat", "Prelude"]) Erased)))
(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))
(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
*Quasiquote> copy `(Z)
App (App (App (App (P (DCon 0 4)
(MN 0 "__MkPair")
(Bind (MN 0 "A")
(Pi (TType (UVar 36)))
(Bind (MN 0 "B")
(Pi (TType (UVar 38)))
(Bind (MN 0 "a")
(Pi (V 1))
(Bind (MN 0 "b")
(Pi (V 1))
(App (App (P (TCon 0 0)
(MN 0 "__Pair")
(Bind (MN 1 "A")
(Pi (TType (UVar 28)))
(Bind (MN 1
"B")
(Pi (TType (UVar 30)))
(TType (UVar 32)))))
(V 3))
(V 2)))))))
(P Bound (MN 106 "A") (TType (UVal 0))))
(P Bound (MN 107 "B") (TType (UVal 0))))
(P (DCon 0 0)
(NS (UN "Z") ["Nat", "Prelude"])
(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
*Quasiquote> getTyArg `(Vect Z ())
Just (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6))) : Maybe TT
```