git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1382 from david-christiansen/incomplete-quasiquote

Properly type check quasiquotes

commita430c3e2c89592d0c82a76a2dd7125782d1efce4 authorDavid Christiansen <david@davidchristiansen.dk> dateMon 14 Jul 2014, 11:50 (12 years ago) parent29c02f490bb76d
7 files changed+37−18
compare with master
unifiedsplit
idris.cabal+4 src/Idris/ElabTerm.hs+11−7 test/quasiquote001/QuasiquoteBasics.idr+4−8 test/quasiquote001/expected+3−3 test/quasiquote003/NoInfer.idr+10 test/quasiquote003/expected+2 test/quasiquote003/run+3
idris.cabal+4
@@ -424,6 +424,10 @@ Extra-source-files:
424424 test/quasiquote002/run
425425 test/quasiquote002/*.idr
426426 test/quasiquote002/expected
427+ test/quasiquote003/run
428+ test/quasiquote003/*.idr
429+ test/quasiquote003/expected
430+
427431
428432 test/records001/run
429433 test/records001/*.idr
src/Idris/ElabTerm.hs+11−7
@@ -14,7 +14,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
1414import Idris.Core.TT
1515import Idris.Core.Evaluate
1616import Idris.Core.Unify
17−import Idris.Core.Typecheck (check)
17+import Idris.Core.Typecheck (check, recheck)
1818import Idris.ErrReverse (errReverse)
1919import Idris.ElabQuasiquote (extractUnquotes)
2020
@@ -729,12 +729,16 @@ elab ist info emode opts fn tm
729729 -- original goal in the original proof state.
730730 env <- get_env
731731 loadState
732− case fmap (explicitNames . binderVal) $ lookup nTm env of
733− Just q
734− | pattern -> reflectQuotePattern unquoteNames q
735− | otherwise -> do fill $ reflectQuote unquoteNames q
736− solve
737− Nothing -> fail "Broken elaboration of quasiquote"
732+ let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
733+
734+ case quoted of
735+ Just q -> do ctxt <- get_context
736+ (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
737+ if pattern
738+ then reflectQuotePattern unquoteNames q'
739+ else do fill $ reflectQuote unquoteNames q'
740+ solve
741+ Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
738742
739743 -- Finally fill in the terms or patterns from the unquotes. This
740744 -- happens last so that their holes still exist while elaborating
test/quasiquote001/QuasiquoteBasics.idr+4−8
@@ -13,22 +13,18 @@ twoElems : TT
1313twoElems = `(with List [(), ()])
1414
1515copy : TT -> TT
16−copy q = `((~q,~q))
16+copy q = `((~q,~q) : (Type, Type))
1717
1818thing : TT -> TT
1919thing tm = `(with List [Type, ~tm])
2020
21−getTyArg : TT -> Maybe TT
22−getTyArg `(~f ~x) = Just x
23−getTyArg _ = Nothing
24−
2521
2622
2723
2824namespace Main
2925 main : IO ()
30− main = do putStrLn . show $ thing (copy nat)
26+ main = do putStrLn . show $ twoElems
3127 putStrLn "--------------"
32− putStrLn . show $ getTyArg nat
28+ putStrLn . show . thing $ copy nat
3329 putStrLn "--------------"
34− putStrLn . show $ getTyArg (twoElems)
30+ putStrLn . show . copy . copy $ `(Type)
test/quasiquote001/expected+3−3
@@ -1,5 +1,5 @@
1−(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (TType (UVal 0))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVal 0))) (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 (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVal 0)))))
1+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 7 0) (MN 0 "__Unit") (TType (UVar 6))))))
22--------------
3−Nothing
3+(App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 110))) (TType (UVar 112))) (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (TType (UVar 114))) (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))))))) (TType (UVar 108))) (TType (UVar 110))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1)))) (P (TCon 15 0) (NS (UN Nat) ["Nat", "Prelude"]) (TType (UVar -1))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (TType (UVar 116)))))
44--------------
5−Just (App (App (App (P (DCon 1 3) (NS (UN ::) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (Bind (MN 0 "_t") (Pi (V 0)) (Bind (MN 2 "_t") (Pi (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 2)))))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))) (P (DCon 0 0) (MN 0 "__II") (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6))))) (App (P (DCon 0 1) (NS (UN Nil) ["List", "Prelude"]) (Bind (UN a) (Pi (TType (UVar -1))) (App (P (TCon 0 0) (NS (UN List) ["List", "Prelude"]) Erased) (V 0)))) (P (TCon 0 0) (MN 0 "__Unit") (TType (UVar 6)))))
5+(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))))))) (TType (UVar 108))) (TType (UVar 110))) (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))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110)))) (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))))))) (TType (UVar 108))) (TType (UVar 110))) (TType (UVar 110))) (TType (UVar 110))))
test/quasiquote003/NoInfer.idrnew file+10
@@ -0,0 +1,10 @@
1+module NoInfer
2+
3+import Language.Reflection
4+import Language.Reflection.Utils
5+
6+zzz2 : TT
7+zzz2 = `(fZ : Fin 3)
8+
9+zzz : TT
10+zzz = `(fZ)
test/quasiquote003/expectednew file+2
@@ -0,0 +1,2 @@
1+NoInfer.idr:10:5:When elaborating right hand side of zzz:
2+No such variable k
test/quasiquote003/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ --check NoInfer.idr
3+rm -f *.ibc