git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1382 from david-christiansen/incomplete-quasiquote
a430c3eDavid Christiansen
idris.cabal+4
compare with master
unifiedsplit
@@ -424,6 +424,10 @@ Extra-source-files:
424 test/quasiquote002/run
424 test/quasiquote002/run
425 test/quasiquote002/*.idr
425 test/quasiquote002/*.idr
426 test/quasiquote002/expected
426 test/quasiquote002/expected
427+ test/quasiquote003/run
428+ test/quasiquote003/*.idr
429+ test/quasiquote003/expected
430+
427
431
428 test/records001/run
432 test/records001/run
429 test/records001/*.idr
433 test/records001/*.idr
src/Idris/ElabTerm.hs+11−7
@@ -14,7 +14,7 @@ import Idris.Core.Elaborate hiding (Tactic(..))
14import Idris.Core.TT
14import Idris.Core.TT
15import Idris.Core.Evaluate
15import Idris.Core.Evaluate
16import Idris.Core.Unify
16import Idris.Core.Unify
17−import Idris.Core.Typecheck (check)
17+import Idris.Core.Typecheck (check, recheck)
18import Idris.ErrReverse (errReverse)
18import Idris.ErrReverse (errReverse)
19import Idris.ElabQuasiquote (extractUnquotes)
19import Idris.ElabQuasiquote (extractUnquotes)
20
20
@@ -729,12 +729,16 @@ elab ist info emode opts fn tm
729 -- original goal in the original proof state.
729 -- original goal in the original proof state.
730 env <- get_env
730 env <- get_env
731 loadState
731 loadState
732− case fmap (explicitNames . binderVal) $ lookup nTm env of
732+ let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
733− Just q
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
734− | pattern -> reflectQuotePattern unquoteNames q
738+ then reflectQuotePattern unquoteNames q'
735− | otherwise -> do fill $ reflectQuote unquoteNames q
739+ else do fill $ reflectQuote unquoteNames q'
736− solve
740+ solve
737− Nothing -> fail "Broken elaboration of quasiquote"
741+ Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
738
742
739 -- Finally fill in the terms or patterns from the unquotes. This
743 -- Finally fill in the terms or patterns from the unquotes. This
740 -- happens last so that their holes still exist while elaborating
744 -- happens last so that their holes still exist while elaborating
test/quasiquote001/QuasiquoteBasics.idr+4−8
@@ -13,22 +13,18 @@ twoElems : TT
13twoElems = `(with List [(), ()])
13twoElems = `(with List [(), ()])
14
14
15copy : TT -> TT
15copy : TT -> TT
16−copy q = `((~q,~q))
16+copy q = `((~q,~q) : (Type, Type))
17
17
18thing : TT -> TT
18thing : TT -> TT
19thing tm = `(with List [Type, ~tm])
19thing tm = `(with List [Type, ~tm])
20
20
21−getTyArg : TT -> Maybe TT
22−getTyArg `(~f ~x) = Just x
23−getTyArg _ = Nothing
24−
25
21
26
22
27
23
28namespace Main
24namespace Main
29 main : IO ()
25 main : IO ()
30− main = do putStrLn . show $ thing (copy nat)
26+ main = do putStrLn . show $ twoElems
31 putStrLn "--------------"
27 putStrLn "--------------"
32− putStrLn . show $ getTyArg nat
28+ putStrLn . show . thing $ copy nat
33 putStrLn "--------------"
29 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))))))
2--------------
2--------------
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)))))
4--------------
4--------------
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