git.iko.soy/Idris-dev
on 76ec3fe help sign in
Idris-dev/test/sourceLocation001/SourceLoc.idr
102 lines 2.9 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 printLn 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
57 lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t')
58 lam_ _ = Lam
60exec : Tm [] t -> IO ()
61exec tm = case run tm [] of
62 Left loc => putStrLn $ "Error at " ++ show loc
63 Right _ => putStrLn $ "Success!"
65dsl lang
66 variable = Var
67 index_first = FZ
68 index_next = FS
69 lambda = lam_
71testTerm1 : Tm [] (Arr U U)
72testTerm1 = lang (\x=>Die)
74testTerm2 : Tm [] U
75testTerm2 = App testTerm1 MkU
77testTerm3 : Tm [] (Arr U U)
78testTerm3 = lang (\x => MkU)
80testTerm4 : Tm [] U
81testTerm4 = App testTerm3 MkU
83namespace Main
84 main : IO ()
85 main = do putStrLn "Testing using definition"
86 printLn fromRHS
87 putStrLn "Testing using inline tactics"
88 printLn fromProofScript
89 putStrLn "Testing using metavariable with later definition"
90 printLn fromMetavar
91 putStrLn "-----------------------"
92 sequence_ $ with List [ exec testTerm1
93 , exec testTerm2
94 , exec testTerm3
95 , exec testTerm4
96 ]
97---------- Proofs ----------
98SourceLoc.meta = proof
99 sourceLocation