git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/test/sourceLocation001/SourceLoc.idr
103 lines 2.9 kB history raw
1module SourceLoc
3import Data.Vect
4import Data.Fin
5import Language.Reflection
6import Language.Reflection.Utils
8%default total
9%language DSLNotation
11||| A "function" that returns where it is called in the source
12getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation
13getLoc {x} = x
15||| A test of getLoc
16fromRHS : SourceLocation
17fromRHS = getLoc
19||| Testing getting source locations from RHS proof scripts
20fromProofScript : SourceLocation
21fromProofScript = proof sourceLocation
23||| Testing getting source locations from deferred proofs.
24fromMetavar : SourceLocation
25fromMetavar = ?meta
27--- Testing that getting source locations in ASTs constructed with DSL notation
28data Ty = U | Arr Ty Ty
30interp : Ty -> Type
31interp U = ()
32interp (Arr x y) = interp x -> Either SourceLocation (interp y)
34using (ctxt : Vect n Ty)
35 data Tm : Vect n Ty -> Ty -> Type where
36 MkU : Tm ctxt U
37 Var : (i : Fin n) -> Tm ctxt (index i ctxt)
38 Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
39 App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'
40 ||| A term that makes the program halt and printLn where it halted
41 Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t
43 data Env : Vect n Ty -> Type where
44 Nil : Env []
45 (::) : interp t -> Env ctxt -> Env (t::ctxt)
47 index : (i : Fin n) -> Env ctxt -> interp (index i ctxt)
48 index FZ (x::env) = x
49 index (FS i) (x::env) = index i env
51 run : Tm ctxt t -> Env ctxt -> Either SourceLocation (interp t)
52 run MkU _ = pure ()
53 run (Var i) env = pure $ index i env
54 run (Lam bdy) env = pure $ \x => run bdy (x::env)
55 run (App f x) env = !(run f env) !(run x env)
56 run (Die {loc}) _ = Left loc
58 lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
59 lam_ _ = Lam
61exec : Tm [] t -> IO ()
62exec tm = case run tm [] of
63 Left loc => putStrLn $ "Error at " ++ show loc
64 Right _ => putStrLn $ "Success!"
66dsl lang
67 variable = Var
68 index_first = FZ
69 index_next = FS
70 lambda = lam_
72testTerm1 : Tm [] (Arr U U)
73testTerm1 = lang (\x=>Die)
75testTerm2 : Tm [] U
76testTerm2 = App testTerm1 MkU
78testTerm3 : Tm [] (Arr U U)
79testTerm3 = lang (\x => MkU)
81testTerm4 : Tm [] U
82testTerm4 = App testTerm3 MkU
84namespace Main
85 main : IO ()
86 main = do putStrLn "Testing using definition"
87 printLn fromRHS
88 putStrLn "Testing using inline tactics"
89 printLn fromProofScript
90 putStrLn "Testing using metavariable with later definition"
91 printLn fromMetavar
92 putStrLn "-----------------------"
93 sequence_ $ with List [ exec testTerm1
94 , exec testTerm2
95 , exec testTerm3
96 , exec testTerm4
97 ]
98---------- Proofs ----------
99SourceLoc.meta = proof
100 sourceLocation