module SourceLoc import Data.Vect import Data.Fin import Language.Reflection import Language.Reflection.Utils %default total %language DSLNotation ||| A "function" that returns where it is called in the source getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation getLoc {x} = x ||| A test of getLoc fromRHS : SourceLocation fromRHS = getLoc ||| Testing getting source locations from RHS proof scripts fromProofScript : SourceLocation fromProofScript = proof sourceLocation ||| Testing getting source locations from deferred proofs. fromMetavar : SourceLocation fromMetavar = ?meta --- Testing that getting source locations in ASTs constructed with DSL notation data Ty = U | Arr Ty Ty interp : Ty -> Type interp U = () interp (Arr x y) = interp x -> Either SourceLocation (interp y) using (ctxt : Vect n Ty) data Tm : Vect n Ty -> Ty -> Type where MkU : Tm ctxt U Var : (i : Fin n) -> Tm ctxt (index i ctxt) Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t') App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t' ||| A term that makes the program halt and printLn where it halted Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t data Env : Vect n Ty -> Type where Nil : Env [] (::) : interp t -> Env ctxt -> Env (t::ctxt) index : (i : Fin n) -> Env ctxt -> interp (index i ctxt) index FZ (x::env) = x index (FS i) (x::env) = index i env run : Tm ctxt t -> Env ctxt -> Either SourceLocation (interp t) run MkU _ = pure () run (Var i) env = pure $ index i env run (Lam bdy) env = pure $ \x => run bdy (x::env) run (App f x) env = !(run f env) !(run x env) run (Die {loc}) _ = Left loc lam_ : _ -> Tm (t::ctxt) t' -> Tm ctxt (Arr t t') lam_ _ = Lam exec : Tm [] t -> IO () exec tm = case run tm [] of Left loc => putStrLn $ "Error at " ++ show loc Right _ => putStrLn $ "Success!" dsl lang variable = Var index_first = FZ index_next = FS lambda = lam_ testTerm1 : Tm [] (Arr U U) testTerm1 = lang (\x=>Die) testTerm2 : Tm [] U testTerm2 = App testTerm1 MkU testTerm3 : Tm [] (Arr U U) testTerm3 = lang (\x => MkU) testTerm4 : Tm [] U testTerm4 = App testTerm3 MkU namespace Main main : IO () main = do putStrLn "Testing using definition" printLn fromRHS putStrLn "Testing using inline tactics" printLn fromProofScript putStrLn "Testing using metavariable with later definition" printLn fromMetavar putStrLn "-----------------------" sequence_ $ with List [ exec testTerm1 , exec testTerm2 , exec testTerm3 , exec testTerm4 ] ---------- Proofs ---------- SourceLoc.meta = proof sourceLocation