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