git.iko.soy/Idris-dev
on master help sign in
Overloaded quasiquotations

Now, quasiquotations can generate Raw terms in addition to TT terms.

commitb04814059fbacd685ddca4823b8b3c641eb277cb authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 20 Feb 2015, 08:29 (12 years ago) parent9249aae
6 files changed+23−2
compare with master
unifiedsplit
CHANGELOG+3 idris.cabal+3 src/Idris/ElabTerm.hs+5−2 test/quasiquote005/Quasiquote005.idr+9 test/quasiquote005/expected test/quasiquote005/run+3
CHANGELOG+3
@@ -5,6 +5,9 @@ New in 0.9.17:
55* A new tactic "claim N TY" that introduces a new hole named N with type TY
66* A new tactic "unfocus" that moves the current hole to the bottom of the
77 hole stack
8+* Quasiquotation supports the generation of Language.Reflection.Raw terms
9+ in addition to Language.Reflection.TT. Types are used for disambiguation,
10+ defaulting to TT at the REPL.
811
912New in 0.9.16:
1013--------------
idris.cabal+3
@@ -513,6 +513,9 @@ Extra-source-files:
513513 test/quasiquote004/run
514514 test/quasiquote004/*.idr
515515 test/quasiquote004/expected
516+ test/quasiquote005/run
517+ test/quasiquote005/*.idr
518+ test/quasiquote005/expected
516519
517520
518521 test/records001/run
src/Idris/ElabTerm.hs+5−2
@@ -940,10 +940,13 @@ elab ist info emode opts fn tm
940940 elab' ina fc (PQuasiquote t goal)
941941 = do -- First extract the unquoted subterms, replacing them with fresh
942942 -- names in the quasiquoted term. Claim their reflections to be
943− -- of type TT.
943+ -- an inferred type (to support polytypic quasiquotes).
944944 (t, unq) <- extractUnquotes 0 t
945945 let unquoteNames = map fst unq
946− mapM_ (flip claim (Var tt)) unquoteNames
946+ mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")
947+ claim uqh RType
948+ movelast uqh
949+ claim uqn (Var uqh)) unquoteNames
947950
948951
949952 -- Save the old state - we need a fresh proof state to avoid
test/quasiquote005/Quasiquote005.idrnew file+9
@@ -0,0 +1,9 @@
1+module Quasiquote005
2+
3+test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =
4+ RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))
5+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
6+ (Var (NS (UN "Z") ["Nat", "Prelude"]))))
7+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))
8+ (Var (NS (UN "Z") ["Nat", "Prelude"])))
9+test = Refl
test/quasiquote005/expectednew file

No changes to the content.

test/quasiquote005/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check --nocolour Quasiquote005.idr
3+rm -f *.ibc