git.iko.soy/Idris-dev
on master help sign in
Add simple test for quasiquotations
commit9a3082ba3246727e88cc62d1a7cc0af6d4301ff5 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 25 Jun 2014, 23:58 (12 years ago) parent84cdb10
4 files changed+47
compare with master
unifiedsplit
idris.cabal+4 test/quasiquote001/QuasiquoteBasics.idr+34 test/quasiquote001/expected+5 test/quasiquote001/run+4
idris.cabal+4
@@ -415,6 +415,10 @@ Extra-source-files:
415415 test/proof004/*.idr
416416 test/proof004/expected
417417
418+ test/quasiquote001/run
419+ test/quasiquote001/*.idr
420+ test/quasiquote001/expected
421+
418422 test/records001/run
419423 test/records001/*.idr
420424 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