git.iko.soy/Idris-dev
on master help sign in
Add simple test for quasiquotations
9a3082bDavid Raymond Christiansen
idris.cabal+4
compare with master
unifiedsplit
@@ -415,6 +415,10 @@ Extra-source-files:
415 test/proof004/*.idr
415 test/proof004/*.idr
416 test/proof004/expected
416 test/proof004/expected
417
417
418+ test/quasiquote001/run
419+ test/quasiquote001/*.idr
420+ test/quasiquote001/expected
421+
418 test/records001/run
422 test/records001/run
419 test/records001/*.idr
423 test/records001/*.idr
420 test/records001/expected
424 test/records001/expected
test/quasiquote001/QuasiquoteBasics.idrnew file+34
@@ -0,0 +1,34 @@
1+module QuasiquoteBasics
2+
3+import Language.Reflection
4+import Language.Reflection.Utils
5+
6+nat : TT
7+nat = `(Nat)
8+
9+three : TT
10+three = `(S (S (S Z)))
11+
12+twoElems : TT
13+twoElems = `(with List [(), ()])
14+
15+copy : TT -> TT
16+copy q = `((~q,~q))
17+
18+thing : TT -> TT
19+thing tm = `(with List [Type, ~tm])
20+
21+getTyArg : TT -> Maybe TT
22+getTyArg `(~f ~x) = Just x
23+getTyArg _ = Nothing
24+
25+
26+
27+
28+namespace Main
29+ main : IO ()
30+ main = do putStrLn . show $ thing (copy nat)
31+ putStrLn "--------------"
32+ putStrLn . show $ getTyArg nat
33+ putStrLn "--------------"
34+ putStrLn . show $ getTyArg (twoElems)
test/quasiquote001/expectednew file+5
@@ -0,0 +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)))))
2+--------------
3+Nothing
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)))))
test/quasiquote001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ QuasiquoteBasics.idr -o quasiquote001
3+./quasiquote001
4+rm -f quasiquote001 *.ibc