f1e161d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

A new primitive tactic for getting source locations

f1e161dDavid Raymond Christiansen12 years ago

CHANGELOG+6

compare with master

unifiedsplit

@@ -1,3 +1,9 @@

1+New in 0.9.16:

2+--------------

3+* A new tactic sourceLocation that fills the current hole with the current

4+ source code span, if this information is available. If not, it raises an

5+ error.

1New in 0.9.15:

7New in 0.9.15:

2--------------

8--------------

3* Two new tactics: skip and fail. Skip does nothing, and fail takes a string

9* Two new tactics: skip and fail. Skip does nothing, and fail takes a string

idris.cabal+4

@@ -483,6 +483,10 @@ Extra-source-files:

483 test/records003/*.idr

484 test/records003/expected

485

486+ test/sourceLocation001/run

487+ test/sourceLocation001/*.idr

488+ test/sourceLocation001/expected

489+

486 test/sugar001/run

490 test/sugar001/run

487 test/sugar001/*.idr

491 test/sugar001/*.idr

488 test/sugar001/expected

492 test/sugar001/expected

libs/base/Language/Reflection.idr+9−1

@@ -175,6 +175,11 @@ data Raw =

175 RConstant Const

176%name Raw tm, tm'

177

178+data SourceLocation : Type where

179+ FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

180+

181+%name SourceLocation loc

182+

178||| Error reports are a list of report parts

183||| Error reports are a list of report parts

179data ErrorReportPart =

184data ErrorReportPart =

180 ||| A human-readable string

185 ||| A human-readable string

@@ -239,7 +244,9 @@ data Tactic =

239 ||| Do nothing

244 ||| Do nothing

240 Skip |

245 Skip |

241 ||| Fail with an error message

246 ||| Fail with an error message

242− Fail (List ErrorReportPart)

247+ Fail (List ErrorReportPart) |

248+ ||| Attempt to fill the hole with source code information

249+ SourceFC

243%name Tactic tac, tac'

250%name Tactic tac, tac'

244

251

245

252

@@ -477,3 +484,4 @@ instance Quotable Tactic where

477 quote Compute = `(Compute)

484 quote Compute = `(Compute)

478 quote Skip = `(Skip)

485 quote Skip = `(Skip)

479 quote (Fail xs) = `(Fail ~(quote xs))

486 quote (Fail xs) = `(Fail ~(quote xs))

487+ quote SourceFC = `(SourceFC)

libs/base/Language/Reflection/Errors.idr−4

@@ -2,10 +2,6 @@ module Language.Reflection.Errors

3import Language.Reflection

5−data SourceLocation : Type where

6− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation

7−

8−%name SourceLocation loc

10data Err = Msg String

6data Err = Msg String

11 | InternalMsg String

7 | InternalMsg String

src/Idris/AbsSyntaxTree.hs+5−2

@@ -50,12 +50,13 @@ data ElabWhat = ETypes | EDefns | EAll

50data ElabInfo = EInfo { params :: [(Name, PTerm)],

51 inblock :: Ctxt [Name], -- names in the block, and their params

52 liftname :: Name -> Name,

53− namespace :: Maybe [String],

53+ namespace :: Maybe [String],

54+ elabFC :: Maybe FC,

54 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

55 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->

55 Idris () }

56 Idris () }

57toplevel :: ElabInfo

58toplevel :: ElabInfo

58−toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")

59+toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")

60eInfoNames :: ElabInfo -> [Name]

61eInfoNames :: ElabInfo -> [Name]

61eInfoNames info = map fst (params info) ++ M.keys (inblock info)

62eInfoNames info = map fst (params info) ++ M.keys (inblock info)

@@ -809,6 +810,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

809 | Skip

810 | Skip

810 | TFail [ErrorReportPart]

811 | TFail [ErrorReportPart]

811 | Qed | Abandon

812 | Qed | Abandon

813+ | SourceFC

812 deriving (Show, Eq, Functor, Foldable, Traversable)

814 deriving (Show, Eq, Functor, Foldable, Traversable)

813{-!

815{-!

814deriving instance Binary PTactic'

816deriving instance Binary PTactic'

@@ -839,6 +841,7 @@ instance Sized a => Sized (PTactic' a) where

839 size Abandon = 1

841 size Abandon = 1

840 size Skip = 1

842 size Skip = 1

841 size (TFail ts) = 1 + size ts

843 size (TFail ts) = 1 + size ts

844+ size SourceFC = 1

842

845

843type PTactic = PTactic' PTerm

846type PTactic = PTactic' PTerm

844

847

src/Idris/Completion.hs+2−1

@@ -52,7 +52,8 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

52 , (":eval", Just ExprTArg)

53 ] ++ map (\x -> (x, Nothing)) [

54 "intros", "compute", "trivial", "search", "solve", "attack",

55− "unify", "state", "term", "undo", "qed", "abandon", ":q"

55+ "unify", "state", "term", "undo", "qed", "abandon", ":q",

56+ "sourceLocation"

56 ]

57 ]

57tactics = map fst tacticArgs

58tactics = map fst tacticArgs

src/Idris/DeepSeq.hs+1

@@ -262,6 +262,7 @@ instance (NFData t) => NFData (PTactic' t) where

262 rnf Abandon = ()

263 rnf Skip = ()

264 rnf (TFail x1) = rnf x1 `seq` ()

265+ rnf SourceFC = ()

265

266

266instance NFData ErrorReportPart where

267instance NFData ErrorReportPart where

267 rnf (TermPart x1) = rnf x1 `seq` ()

268 rnf (TermPart x1) = rnf x1 `seq` ()

src/Idris/Elab/Clause.hs+5−3

@@ -56,8 +56,10 @@ import Numeric

56-- | Elaborate a collection of left-hand and right-hand pairs - that is, a

57-- top-level definition.

58elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

59−elabClauses info fc opts n_in cs = let n = liftname info n_in in

59+elabClauses info' fc opts n_in cs =

60+ do let n = liftname info n_in

61+ info = info' { elabFC = Just fc }

60− do ctxt <- getContext

62+ ctxt <- getContext

61 ist <- getIState

63 ist <- getIState

62 optimise <- getOptimise

64 optimise <- getOptimise

63 let petrans = PETransform `elem` optimise

65 let petrans = PETransform `elem` optimise

@@ -618,7 +620,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

618 let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm

620 let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm

619 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

621 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all

620

622

621− let winfo = pinfo info newargs defs windex

623+ let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }

622 let wb = map (mkStatic static_names) $

624 let wb = map (mkStatic static_names) $

623 map (expandParamsD False ist decorate newargs defs) whereblock

625 map (expandParamsD False ist decorate newargs defs) whereblock

624

626

src/Idris/ElabDecls.hs+1−1

@@ -62,7 +62,7 @@ import Util.Pretty(pretty, text)

63-- Top level elaborator info, supporting recursive elaboration

64recinfo :: ElabInfo

65−recinfo = EInfo [] emptyContext id Nothing elabDecl'

65+recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'

67-- | Return the elaborated term which calls 'main'

68elabMain :: Idris Term

src/Idris/ElabTerm.hs+150−125

@@ -144,7 +144,8 @@ elab ist info emode opts fn tm

144 = do let loglvl = opt_logLevel (idris_options ist)

145 when (loglvl > 5) $ unifyLog True

146 compute -- expand type synonyms, etc

147+ let fc = maybe "(unknown)"

147− elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)

148+ elabE (False, False, False, False) (elabFC info) tm -- (in argument, guarded, in type, in qquote)

148 end_unify

149 end_unify

149 ptm <- get_term

150 ptm <- get_term

150 when pattern -- convert remaining holes to pattern vars

151 when pattern -- convert remaining holes to pattern vars

@@ -166,11 +167,11 @@ elab ist info emode opts fn tm

166

167

167 toElab ina arg = case getTm arg of

168 toElab ina arg = case getTm arg of

168 Placeholder -> Nothing

169 Placeholder -> Nothing

169− v -> Just (priority arg, elabE ina v)

170+ v -> Just (priority arg, elabE ina (elabFC info) v)

170

171

171 toElab' ina arg = case getTm arg of

172 toElab' ina arg = case getTm arg of

172 Placeholder -> Nothing

173 Placeholder -> Nothing

173− v -> Just (elabE ina v)

174+ v -> Just (elabE ina (elabFC info) v)

174

175

175 mkPat = do hs <- get_holes

176 mkPat = do hs <- get_holes

176 tm <- get_term

177 tm <- get_term

@@ -182,30 +183,30 @@ elab ist info emode opts fn tm

182 -- and forces/delays. If you make a recursive call in elab', it is

183 -- and forces/delays. If you make a recursive call in elab', it is

183 -- normally correct to call elabE - the ones that don't are desugarings

184 -- normally correct to call elabE - the ones that don't are desugarings

184 -- typically

185 -- typically

185− elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()

186+ elabE :: (Bool, Bool, Bool, Bool) -> Maybe FC -> PTerm -> ElabD ()

186− elabE ina t =

187+ elabE ina fc' t =

187− --do g <- goal

188+ --do g <- goal

188− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

189+ --trace ("Elaborating " ++ show t ++ " : " ++ show g) $

189− do ct <- insertCoerce ina t

190+ do ct <- insertCoerce ina t

190− t' <- insertLazy ct

191+ t' <- insertLazy ct

191− g <- goal

192+ g <- goal

192− tm <- get_term

193+ tm <- get_term

193− ps <- get_probs

194+ ps <- get_probs

194− hs <- get_holes

195+ hs <- get_holes

195− --trace ("Elaborating " ++ show t' ++ " in " ++ show g

196+ --trace ("Elaborating " ++ show t' ++ " in " ++ show g

196− -- ++ "\n" ++ show tm

197+ -- ++ "\n" ++ show tm

197− -- ++ "\nholes " ++ show hs

198+ -- ++ "\nholes " ++ show hs

198− -- ++ "\nproblems " ++ show ps

199+ -- ++ "\nproblems " ++ show ps

199− -- ++ "\n-----------\n") $

200+ -- ++ "\n-----------\n") $

200− --trace ("ELAB " ++ show t') $

201+ --trace ("ELAB " ++ show t') $

201− let fc = fileFC "Force"

202+ let fc = fileFC "Force"

202− env <- get_env

203+ env <- get_env

203− handleError (forceErr env)

204+ handleError (forceErr env)

204− (elab' ina t')

205+ (elab' ina fc' t')

205− (elab' ina (PApp fc (PRef fc (sUN "Force"))

206+ (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

206− [pimp (sUN "t") Placeholder True,

207+ [pimp (sUN "t") Placeholder True,

207− pimp (sUN "a") Placeholder True,

208+ pimp (sUN "a") Placeholder True,

208− pexp ct])) True

209+ pexp ct])) True

209

210

210 forceErr env (CantUnify _ t t' _ _ _)

211 forceErr env (CantUnify _ t t' _ _ _)

211 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

212 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

@@ -235,35 +236,36 @@ elab ist info emode opts fn tm

235 -- "guarded" means immediately under a constructor, to help find patvars

236 -- "guarded" means immediately under a constructor, to help find patvars

236

237

237 elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)

238 elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)

239+ -> Maybe FC -- ^ The closest FC in the syntax tree, if applicable

238 -> PTerm -- ^ The term to elaborate

240 -> PTerm -- ^ The term to elaborate

239 -> ElabD ()

241 -> ElabD ()

240− elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step

242+ elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step

241− elab' ina PType = do apply RType []; solve

243+ elab' ina fc PType = do apply RType []; solve

242− elab' ina (PUniverse u) = do apply (RUType u) []; solve

244+ elab' ina fc (PUniverse u) = do apply (RUType u) []; solve

243-- elab' (_,_,inty) (PConstant c)

245-- elab' (_,_,inty) (PConstant c)

244-- | constType c && pattern && not reflection && not inty

246-- | constType c && pattern && not reflection && not inty

245-- = lift $ tfail (Msg "Typecase is not allowed")

247-- = lift $ tfail (Msg "Typecase is not allowed")

246− elab' ina (PConstant c) = do apply (RConstant c) []; solve

248+ elab' ina fc (PConstant c) = do apply (RConstant c) []; solve

247− elab' ina (PQuote r) = do fill r; solve

249+ elab' ina fc (PQuote r) = do fill r; solve

248− elab' ina (PTrue fc _) =

250+ elab' ina _ (PTrue fc _) =

249 do hnf_compute

251 do hnf_compute

250 g <- goal

252 g <- goal

251 case g of

253 case g of

252− TType _ -> elab' ina (PRef fc unitTy)

254+ TType _ -> elab' ina (Just fc) (PRef fc unitTy)

253− _ -> elab' ina (PRef fc unitCon)

255+ _ -> elab' ina (Just fc) (PRef fc unitCon)

254− elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

256+ elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

255 = do g <- goal; resolveTC False 5 g fn ist

257 = do g <- goal; resolveTC False 5 g fn ist

256− elab' ina (PResolveTC fc)

258+ elab' ina fc (PResolveTC fc')

257 = do c <- getNameFrom (sMN 0 "class")

259 = do c <- getNameFrom (sMN 0 "class")

258 instanceArg c

260 instanceArg c

259− elab' ina (PRefl fc t)

261+ elab' ina _ (PRefl fc t)

260− = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

262+ = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

261− pimp (sMN 0 "x") t False])

263+ pimp (sMN 0 "x") t False])

262− elab' ina (PEq fc Placeholder Placeholder l r)

264+ elab' ina _ (PEq fc Placeholder Placeholder l r)

263 = try (do tyn <- getNameFrom (sMN 0 "aqty")

265 = try (do tyn <- getNameFrom (sMN 0 "aqty")

264 claim tyn RType

266 claim tyn RType

265 movelast tyn

267 movelast tyn

266− elab' ina (PApp fc (PRef fc eqTy)

268+ elab' ina (Just fc) (PApp fc (PRef fc eqTy)

267 [pimp (sUN "A") (PRef fc tyn) True,

269 [pimp (sUN "A") (PRef fc tyn) True,

268 pimp (sUN "B") (PRef fc tyn) False,

270 pimp (sUN "B") (PRef fc tyn) False,

269 pexp l, pexp r]))

271 pexp l, pexp r]))

@@ -273,26 +275,26 @@ elab ist info emode opts fn tm

273 movelast atyn

275 movelast atyn

274 claim btyn RType

276 claim btyn RType

275 movelast btyn

277 movelast btyn

276− elab' ina (PApp fc (PRef fc eqTy)

278+ elab' ina (Just fc) (PApp fc (PRef fc eqTy)

277− [pimp (sUN "A") (PRef fc atyn) True,

279+ [pimp (sUN "A") (PRef fc atyn) True,

278− pimp (sUN "B") (PRef fc btyn) False,

280+ pimp (sUN "B") (PRef fc btyn) False,

279− pexp l, pexp r]))

281+ pexp l, pexp r]))

280−

282+

281− elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)

283+ elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)

282− [pimp (sUN "A") lt True,

284+ [pimp (sUN "A") lt True,

283− pimp (sUN "B") rt False,

285+ pimp (sUN "B") rt False,

284− pexp l, pexp r])

286+ pexp l, pexp r])

285− elab' ina@(_, a, inty, qq) (PPair fc _ l r)

287+ elab' ina@(_, a, inty, qq) _ (PPair fc _ l r)

286 = do hnf_compute

288 = do hnf_compute

287 g <- goal

289 g <- goal

288 case g of

290 case g of

289− TType _ -> elab' ina (PApp fc (PRef fc pairTy)

291+ TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)

290 [pexp l,pexp r])

292 [pexp l,pexp r])

291− _ -> elab' ina (PApp fc (PRef fc pairCon)

293+ _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)

292 [pimp (sUN "A") Placeholder False,

294 [pimp (sUN "A") Placeholder False,

293 pimp (sUN "B") Placeholder False,

295 pimp (sUN "B") Placeholder False,

294 pexp l, pexp r])

296 pexp l, pexp r])

295− elab' ina (PDPair fc p l@(PRef _ n) t r)

297+ elab' ina _ (PDPair fc p l@(PRef _ n) t r)

296 = case t of

298 = case t of

297 Placeholder ->

299 Placeholder ->

298 do hnf_compute

300 do hnf_compute

@@ -301,18 +303,18 @@ elab ist info emode opts fn tm

301 TType _ -> asType

303 TType _ -> asType

302 _ -> asValue

304 _ -> asValue

303 _ -> asType

305 _ -> asType

304− where asType = elab' ina (PApp fc (PRef fc sigmaTy)

306+ where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)

305 [pexp t,

307 [pexp t,

306 pexp (PLam n Placeholder r)])

308 pexp (PLam n Placeholder r)])

307− asValue = elab' ina (PApp fc (PRef fc existsCon)

309+ asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

308 [pimp (sMN 0 "a") t False,

310 [pimp (sMN 0 "a") t False,

309 pimp (sMN 0 "P") Placeholder True,

311 pimp (sMN 0 "P") Placeholder True,

310 pexp l, pexp r])

312 pexp l, pexp r])

311− elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)

313+ elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

312 [pimp (sMN 0 "a") t False,

314 [pimp (sMN 0 "a") t False,

313 pimp (sMN 0 "P") Placeholder True,

315 pimp (sMN 0 "P") Placeholder True,

314 pexp l, pexp r])

316 pexp l, pexp r])

315− elab' ina (PAlternative True as)

317+ elab' ina fc (PAlternative True as)

316 = do hnf_compute

318 = do hnf_compute

317 ty <- goal

319 ty <- goal

318 ctxt <- get_context

320 ctxt <- get_context

@@ -322,24 +324,24 @@ elab ist info emode opts fn tm

322-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++

324-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++

323-- show (length as') ++ "\n" ++

325-- show (length as') ++ "\n" ++

324-- showSep ", " (map showTmImpls as') ++ "\nEND") $

326-- showSep ", " (map showTmImpls as') ++ "\nEND") $

325− tryAll (zip (map (elab' ina) as') (map showHd as'))

327+ tryAll (zip (map (elab' ina fc) as') (map showHd as'))

326 where showHd (PApp _ (PRef _ n) _) = n

328 where showHd (PApp _ (PRef _ n) _) = n

327 showHd (PRef _ n) = n

329 showHd (PRef _ n) = n

328 showHd (PApp _ h _) = showHd h

330 showHd (PApp _ h _) = showHd h

329 showHd x = NErased -- We probably should do something better than this here

331 showHd x = NErased -- We probably should do something better than this here

330− elab' ina (PAlternative False as)

332+ elab' ina fc (PAlternative False as)

331 = trySeq as

333 = trySeq as

332 where -- if none work, take the error from the first

334 where -- if none work, take the error from the first

333− trySeq (x : xs) = let e1 = elab' ina x in

335+ trySeq (x : xs) = let e1 = elab' ina fc x in

334 try' e1 (trySeq' e1 xs) True

336 try' e1 (trySeq' e1 xs) True

335 trySeq' deferr [] = proofFail deferr

337 trySeq' deferr [] = proofFail deferr

336 trySeq' deferr (x : xs)

338 trySeq' deferr (x : xs)

337− = try' (elab' ina x) (trySeq' deferr xs) True

339+ = try' (elab' ina fc x) (trySeq' deferr xs) True

338− elab' ina (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

340+ elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats

339-- elab' (_, _, inty) (PRef fc f)

341-- elab' (_, _, inty) (PRef fc f)

340-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

342-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

341-- = lift $ tfail (Msg "Typecase is not allowed")

343-- = lift $ tfail (Msg "Typecase is not allowed")

342− elab' (ina, guarded, inty, qq) (PRef fc n)

344+ elab' (ina, guarded, inty, qq) _ (PRef fc n)

343 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

345 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq

344 = do ctxt <- get_context

346 = do ctxt <- get_context

345 let defined = case lookupTy n ctxt of

347 let defined = case lookupTy n ctxt of

@@ -358,9 +360,9 @@ elab ist info emode opts fn tm

358 bindable (NS _ _) = False

360 bindable (NS _ _) = False

359 bindable (UN xs) = True

361 bindable (UN xs) = True

360 bindable n = implicitable n

362 bindable n = implicitable n

361− elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])

363+ elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])

362− elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve

364+ elab' ina _ (PRef fc n) = erun fc $ do apply (Var n) []; solve

363− elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)

365+ elab' ina@(_, a, inty, qq) fc (PLam n Placeholder sc)

364 = do -- if n is a type constructor name, this makes no sense...

366 = do -- if n is a type constructor name, this makes no sense...

365 ctxt <- get_context

367 ctxt <- get_context

366 when (isTConName n ctxt) $

368 when (isTConName n ctxt) $

@@ -368,8 +370,8 @@ elab ist info emode opts fn tm

368 checkPiGoal n

370 checkPiGoal n

369 attack; intro (Just n);

371 attack; intro (Just n);

370 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

372 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

371− elabE (True, a, inty, qq) sc; solve

373+ elabE (True, a, inty, qq) fc sc; solve

372− elab' ina@(_, a, inty, qq) (PLam n ty sc)

374+ elab' ina@(_, a, inty, qq) fc (PLam n ty sc)

373 = do tyn <- getNameFrom (sMN 0 "lamty")

375 = do tyn <- getNameFrom (sMN 0 "lamty")

374 -- if n is a type constructor name, this makes no sense...

376 -- if n is a type constructor name, this makes no sense...

375 ctxt <- get_context

377 ctxt <- get_context

@@ -383,12 +385,12 @@ elab ist info emode opts fn tm

383 hs <- get_holes

385 hs <- get_holes

384 introTy (Var tyn) (Just n)

386 introTy (Var tyn) (Just n)

385 focus tyn

387 focus tyn

386− elabE (True, a, True, qq) ty

388+ elabE (True, a, True, qq) fc ty

387− elabE (True, a, inty, qq) sc

389+ elabE (True, a, inty, qq) fc sc

388 solve

390 solve

389− elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)

391+ elab' ina@(_, a, _, qq) fc (PPi _ n Placeholder sc)

390− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve

392+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) fc sc; solve

391− elab' ina@(_, a, _, qq) (PPi _ n ty sc)

393+ elab' ina@(_, a, _, qq) fc (PPi _ n ty sc)

392 = do attack; tyn <- getNameFrom (sMN 0 "ty")

394 = do attack; tyn <- getNameFrom (sMN 0 "ty")

393 claim tyn RType

395 claim tyn RType

394 n' <- case n of

396 n' <- case n of

@@ -396,10 +398,10 @@ elab ist info emode opts fn tm

396 _ -> return n

398 _ -> return n

397 forall n' (Var tyn)

399 forall n' (Var tyn)

398 focus tyn

400 focus tyn

399− elabE (True, a, True, qq) ty

401+ elabE (True, a, True, qq) fc ty

400− elabE (True, a, True, qq) sc

402+ elabE (True, a, True, qq) fc sc

401 solve

403 solve

402− elab' ina@(_, a, inty, qq) (PLet n ty val sc)

404+ elab' ina@(_, a, inty, qq) fc (PLet n ty val sc)

403 = do attack

405 = do attack

404 ivs <- get_instances

406 ivs <- get_instances

405 tyn <- getNameFrom (sMN 0 "letty")

407 tyn <- getNameFrom (sMN 0 "letty")

@@ -412,12 +414,12 @@ elab ist info emode opts fn tm

412 Placeholder -> return ()

414 Placeholder -> return ()

413 _ -> do focus tyn

415 _ -> do focus tyn

414 explicit tyn

416 explicit tyn

415− elabE (True, a, True, qq) ty

417+ elabE (True, a, True, qq) fc ty

416 focus valn

418 focus valn

417− elabE (True, a, True, qq) val

419+ elabE (True, a, True, qq) fc val

418 ivs' <- get_instances

420 ivs' <- get_instances

419 env <- get_env

421 env <- get_env

420− elabE (True, a, inty, qq) sc

422+ elabE (True, a, inty, qq) fc sc

421 when (not pattern) $

423 when (not pattern) $

422 mapM_ (\n -> do focus n

424 mapM_ (\n -> do focus n

423 g <- goal

425 g <- goal

@@ -433,7 +435,7 @@ elab ist info emode opts fn tm

433 expandLet n (case lookup n env of

435 expandLet n (case lookup n env of

434 Just (Let t v) -> v)

436 Just (Let t v) -> v)

435 solve

437 solve

436− elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do

438+ elab' ina@(_, a, inty, qq) _ (PGoal fc r n sc) = do

437 rty <- goal

439 rty <- goal

438 attack

440 attack

439 tyn <- getNameFrom (sMN 0 "letty")

441 tyn <- getNameFrom (sMN 0 "letty")

@@ -442,14 +444,14 @@ elab ist info emode opts fn tm

442 claim valn (Var tyn)

444 claim valn (Var tyn)

443 letbind n (Var tyn) (Var valn)

445 letbind n (Var tyn) (Var valn)

444 focus valn

446 focus valn

445− elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])

447+ elabE (True, a, True, qq) (Just fc) (PApp fc r [pexp (delab ist rty)])

446 env <- get_env

448 env <- get_env

447 computeLet n

449 computeLet n

448− elabE (True, a, inty, qq) sc

450+ elabE (True, a, inty, qq) (Just fc) sc

449 solve

451 solve

450−-- elab' ina (PLet n Placeholder

452+-- elab' ina fc (PLet n Placeholder

451-- (PApp fc r [pexp (delab ist rty)]) sc)

453-- (PApp fc r [pexp (delab ist rty)]) sc)

452− elab' ina tm@(PApp fc (PInferRef _ f) args) = do

454+ elab' ina _ tm@(PApp fc (PInferRef _ f) args) = do

453 rty <- goal

455 rty <- goal

454 ds <- get_deferred

456 ds <- get_deferred

455 ctxt <- get_context

457 ctxt <- get_context

@@ -486,7 +488,8 @@ elab ist info emode opts fn tm

486 _ -> Nothing

488 _ -> Nothing

487 localVar env _ = Nothing

489 localVar env _ = Nothing

488

490

491+ elabIArg ((n, (True, ty)), def) =

489− elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)

492+ do focus n; elabE ina (Just fc) (getTm def)

490 elabIArg _ = return () -- already done, just a name

493 elabIArg _ = return () -- already done, just a name

491

494

492 mkN n@(NS _ _) = n

495 mkN n@(NS _ _) = n

@@ -495,7 +498,7 @@ elab ist info emode opts fn tm

495 Just xs@(_:_) -> sNS n xs

498 Just xs@(_:_) -> sNS n xs

496 _ -> n

499 _ -> n

497

500

498− elab' ina (PMatchApp fc fn)

501+ elab' ina _ (PMatchApp fc fn)

499 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

502 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

500 [(n, args)] -> return (n, map (const True) args)

503 [(n, args)] -> return (n, map (const True) args)

501 _ -> lift $ tfail (NoSuchVariable fn)

504 _ -> lift $ tfail (NoSuchVariable fn)

@@ -507,12 +510,12 @@ elab ist info emode opts fn tm

507-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

510-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

508-- = lift $ tfail (Msg "Typecase is not allowed")

511-- = lift $ tfail (Msg "Typecase is not allowed")

509 -- if f is local, just do a simple_app

512 -- if f is local, just do a simple_app

510− elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)

513+ elab' (ina, g, inty, qq) _ tm@(PApp fc (PRef _ f) args)

511 = do env <- get_env

514 = do env <- get_env

512 if (f `elem` map fst env && length args == 1)

515 if (f `elem` map fst env && length args == 1)

513 then -- simple app, as below

516 then -- simple app, as below

514− do simple_app (elabE (ina, g, inty, qq) (PRef fc f))

517+ do simple_app (elabE (ina, g, inty, qq) (Just fc) (PRef fc f))

515− (elabE (True, g, inty, qq) (getTm (head args)))

518+ (elabE (True, g, inty, qq) (Just fc) (getTm (head args)))

516 (show tm)

519 (show tm)

517 solve

520 solve

518 else

521 else

@@ -630,14 +633,14 @@ elab ist info emode opts fn tm

630 setInjective (PApp _ (PRef _ n) _) = setinj n

633 setInjective (PApp _ (PRef _ n) _) = setinj n

631 setInjective _ = return ()

634 setInjective _ = return ()

632

635

633− elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])

636+ elab' ina@(_, a, inty, qq) _ tm@(PApp fc f [arg])

634 = erun fc $

637 = erun fc $

635− do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))

638+ do simple_app (elabE ina (Just fc) f) (elabE (True, a, inty, qq) (Just fc) (getTm arg))

636 (show tm)

639 (show tm)

637 solve

640 solve

638− elab' ina Placeholder = do (h : hs) <- get_holes

641+ elab' ina fc Placeholder = do (h : hs) <- get_holes

639− movelast h

642+ movelast h

640− elab' ina (PMetavar n) =

643+ elab' ina fc (PMetavar n) =

641 do ptm <- get_term

644 do ptm <- get_term

642 -- When building the metavar application, leave out the unique

645 -- When building the metavar application, leave out the unique

643 -- names which have been used elsewhere in the term, since we

646 -- names which have been used elsewhere in the term, since we

@@ -651,12 +654,12 @@ elab ist info emode opts fn tm

651 mkN n = case namespace info of

654 mkN n = case namespace info of

652 Just xs@(_:_) -> sNS n xs

655 Just xs@(_:_) -> sNS n xs

653 _ -> n

656 _ -> n

654− elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts

657+ elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

655− elab' ina (PTactics ts)

658+ elab' ina fc (PTactics ts)

656− | not pattern = do mapM_ (runTac False ist fn) ts

659+ | not pattern = do mapM_ (runTac False ist fc fn) ts

657− | otherwise = elab' ina Placeholder

660+ | otherwise = elab' ina fc Placeholder

658− elab' ina (PElabError e) = fail (pshow ist e)

661+ elab' ina fc (PElabError e) = fail (pshow ist e)

659− elab' ina (PRewrite fc r sc newg)

662+ elab' ina _ (PRewrite fc r sc newg)

660 = do attack

663 = do attack

661 tyn <- getNameFrom (sMN 0 "rty")

664 tyn <- getNameFrom (sMN 0 "rty")

662 claim tyn RType

665 claim tyn RType

@@ -665,14 +668,14 @@ elab ist info emode opts fn tm

665 letn <- getNameFrom (sMN 0 "_rewrite_rule")

668 letn <- getNameFrom (sMN 0 "_rewrite_rule")

666 letbind letn (Var tyn) (Var valn)

669 letbind letn (Var tyn) (Var valn)

667 focus valn

670 focus valn

668− elab' ina r

671+ elab' ina (Just fc) r

669 compute

672 compute

670 g <- goal

673 g <- goal

671 rewrite (Var letn)

674 rewrite (Var letn)

672 g' <- goal

675 g' <- goal

673 when (g == g') $ lift $ tfail (NoRewriting g)

676 when (g == g') $ lift $ tfail (NoRewriting g)

674 case newg of

677 case newg of

675− Nothing -> elab' ina sc

678+ Nothing -> elab' ina (Just fc) sc

676 Just t -> doEquiv t sc

679 Just t -> doEquiv t sc

677 solve

680 solve

678 where doEquiv t sc =

681 where doEquiv t sc =

@@ -684,12 +687,12 @@ elab ist info emode opts fn tm

684 letn <- getNameFrom (sMN 0 "equiv_val")

687 letn <- getNameFrom (sMN 0 "equiv_val")

685 letbind letn (Var tyn) (Var valn)

688 letbind letn (Var tyn) (Var valn)

686 focus tyn

689 focus tyn

687− elab' ina t

690+ elab' ina (Just fc) t

688 focus valn

691 focus valn

689− elab' ina sc

692+ elab' ina (Just fc) sc

690− elab' ina (PRef fc letn)

693+ elab' ina (Just fc) (PRef fc letn)

691 solve

694 solve

692− elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)

695+ elab' ina@(_, a, inty, qq) _ c@(PCase fc scr opts)

693 = do attack

696 = do attack

694 tyn <- getNameFrom (sMN 0 "scty")

697 tyn <- getNameFrom (sMN 0 "scty")

695 claim tyn RType

698 claim tyn RType

@@ -698,7 +701,7 @@ elab ist info emode opts fn tm

698 claim valn (Var tyn)

701 claim valn (Var tyn)

699 letbind scvn (Var tyn) (Var valn)

702 letbind scvn (Var tyn) (Var valn)

700 focus valn

703 focus valn

701− elabE (True, a, inty, qq) scr

704+ elabE (True, a, inty, qq) (Just fc) scr

702 -- Solve any remaining implicits - we need to solve as many

705 -- Solve any remaining implicits - we need to solve as many

703 -- as possible before making the 'case' type

706 -- as possible before making the 'case' type

704 unifyProblems

707 unifyProblems

@@ -714,7 +717,7 @@ elab ist info emode opts fn tm

714

717

715 cname <- unique_hole' True (mkCaseName fn)

718 cname <- unique_hole' True (mkCaseName fn)

716 let cname' = mkN cname

719 let cname' = mkN cname

717−-- elab' ina (PMetavar cname')

720+-- elab' ina fc (PMetavar cname')

718 attack; defer argsDropped cname'; solve

721 attack; defer argsDropped cname'; solve

719

722

720 -- if the scrutinee is one of the 'args' in env, we should

723 -- if the scrutinee is one of the 'args' in env, we should

@@ -776,10 +779,10 @@ elab ist info emode opts fn tm

776 ((n,b) : args)

779 ((n,b) : args)

777 Nothing -> extendAcc ns acc args

780 Nothing -> extendAcc ns acc args

778

781

779− elab' ina (PUnifyLog t) = do unifyLog True

782+ elab' ina fc (PUnifyLog t) = do unifyLog True

780− elab' ina t

783+ elab' ina fc t

781− unifyLog False

784+ unifyLog False

782− elab' (ina, g, inty, qq) (PQuasiquote t goal) -- TODO: goal type

785+ elab' (ina, g, inty, qq) fc (PQuasiquote t goal) -- TODO: goal type

783 = do -- First extract the unquoted subterms, replacing them with fresh

786 = do -- First extract the unquoted subterms, replacing them with fresh

784 -- names in the quasiquoted term. Claim their reflections to be

787 -- names in the quasiquoted term. Claim their reflections to be

785 -- of type TT.

788 -- of type TT.

@@ -824,11 +827,11 @@ elab ist info emode opts fn tm

824 case goal of

827 case goal of

825 Nothing -> return ()

828 Nothing -> return ()

826 Just gTy -> do focus qTy

829 Just gTy -> do focus qTy

827− elabE (ina, g, inty, True) gTy

830+ elabE (ina, g, inty, True) fc gTy

828

831

829 -- Elaborate the quasiquoted term into the hole

832 -- Elaborate the quasiquoted term into the hole

830 focus qTm

833 focus qTm

831− elabE (ina, g, inty, True) t

834+ elabE (ina, g, inty, True) fc t

832 end_unify

835 end_unify

833

836

834 -- We now have an elaborated term. Reflect it and solve the

837 -- We now have an elaborated term. Reflect it and solve the

@@ -854,11 +857,11 @@ elab ist info emode opts fn tm

854

857

855 elabUnquote (n, tm)

858 elabUnquote (n, tm)

856 = do focus n

859 = do focus n

857− elabE (ina, g, inty, False) tm

860+ elabE (ina, g, inty, False) fc tm

858

861

859

862

860− elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"

863+ elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

861− elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

864+ elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

862

865

863 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

866 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

864 isScr (PRef _ n) (n', b) = (n', (n == n', b))

867 isScr (PRef _ n) (n', b) = (n', (n == n', b))

@@ -994,7 +997,7 @@ elab ist info emode opts fn tm

994 g <- goal

997 g <- goal

995 ulog <- getUnifyLog

998 ulog <- getUnifyLog

996 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

999 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $

997− elab ina t; return failed

1000+ elab ina (Just fc) t; return failed

998 False -> return failed

1001 False -> return failed

999 done_elaborating_arg f argName

1002 done_elaborating_arg f argName

1000 elabArgs ist ina failed fc r f ns force args

1003 elabArgs ist ina failed fc r f ns force args

@@ -1227,8 +1230,8 @@ case_ ind autoSolve ist fn tm = do

1227-- Running tactics directly

1230-- Running tactics directly

1228-- if a tactic adds unification problems, return an error

1231-- if a tactic adds unification problems, return an error

1229

1232

1230−runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

1233+runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()

1231−runTac autoSolve ist fn tac

1234+runTac autoSolve ist perhapsFC fn tac

1232 = do env <- get_env

1235 = do env <- get_env

1233 g <- goal

1236 g <- goal

1234 let tac' = fmap (addImplBound ist (map fst env)) tac

1237 let tac' = fmap (addImplBound ist (map fst env)) tac

@@ -1427,7 +1430,7 @@ runTac autoSolve ist fn tac

1427 ctxt <- get_context

1430 ctxt <- get_context

1428 env <- get_env

1431 env <- get_env

1429 let value' = hnf ctxt env value

1432 let value' = hnf ctxt env value

1430− runTac autoSolve ist fn (Exact $ PQuote (reflect value'))

1433+ runTac autoSolve ist perhapsFC fn (Exact $ PQuote (reflect value'))

1431 runT (Fill v) = do attack -- let x = fill x in ...

1434 runT (Fill v) = do attack -- let x = fill x in ...

1432 tyn <- getNameFrom (sMN 0 "letty")

1435 tyn <- getNameFrom (sMN 0 "letty")

1433 claim tyn RType

1436 claim tyn RType

@@ -1442,7 +1445,7 @@ runTac autoSolve ist fn tac

1442 env <- get_env

1445 env <- get_env

1443 let value' = normalise ctxt env value

1446 let value' = normalise ctxt env value

1444 rawValue <- reifyRaw value'

1447 rawValue <- reifyRaw value'

1445− runTac autoSolve ist fn (Exact $ PQuote rawValue)

1448+ runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)

1446 runT (GoalType n tac) = do g <- goal

1449 runT (GoalType n tac) = do g <- goal

1447 case unApply g of

1450 case unApply g of

1448 (P _ n' _, _) ->

1451 (P _ n' _, _) ->

@@ -1454,10 +1457,31 @@ runTac autoSolve ist fn tac

1454 return ()

1457 return ()

1455 runT Skip = return ()

1458 runT Skip = return ()

1456 runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")

1459 runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")

1460+ runT SourceFC =

1461+ case perhapsFC of

1462+ Nothing -> lift . tfail $ Msg "There is no source location available."

1463+ Just fc ->

1464+ do let intTy = RConstant (AType (ATInt ITNative))

1465+ fill $ raw_apply (Var (reflm "FileLoc"))

1466+ [ RConstant (Str (fc_fname fc))

1467+ , raw_apply (Var pairCon) $

1468+ [intTy, intTy] ++

1469+ map (RConstant . I)

1470+ [ fst (fc_start fc)

1471+ , snd (fc_start fc)

1472+ ]

1473+ , raw_apply (Var pairCon) $

1474+ [intTy, intTy] ++

1475+ map (RConstant . I)

1476+ [ fst (fc_end fc)

1477+ , snd (fc_end fc)

1478+ ]

1479+ ]

1480+ solve

1457 runT x = fail $ "Not implemented " ++ show x

1481 runT x = fail $ "Not implemented " ++ show x

1458

1482

1459 runReflected t = do t' <- reify ist t

1483 runReflected t = do t' <- reify ist t

1460− runTac autoSolve ist fn t'

1484+ runTac autoSolve ist perhapsFC fn t'

1461

1485

1462-- | Prefix a name with the "Language.Reflection" namespace

1486-- | Prefix a name with the "Language.Reflection" namespace

1463reflm :: String -> Name

1487reflm :: String -> Name

@@ -1472,6 +1496,7 @@ reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

1472reify _ (P _ n _) | n == reflm "Solve" = return Solve

1496reify _ (P _ n _) | n == reflm "Solve" = return Solve

1473reify _ (P _ n _) | n == reflm "Compute" = return Compute

1497reify _ (P _ n _) | n == reflm "Compute" = return Compute

1474reify _ (P _ n _) | n == reflm "Skip" = return Skip

1498reify _ (P _ n _) | n == reflm "Skip" = return Skip

1499+reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC

1475reify ist t@(App _ _)

1500reify ist t@(App _ _)

1476 | (P _ f _, args) <- unApply t = reifyApp ist f args

1501 | (P _ f _, args) <- unApply t = reifyApp ist f args

1477reify _ t = fail ("Unknown tactic " ++ show t)

1502reify _ t = fail ("Unknown tactic " ++ show t)

src/Idris/IBC.hs+3−1

@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)

32import Util.Zlib (decompressEither)

34ibcVersion :: Word8

35−ibcVersion = 84

35+ibcVersion = 85

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

@@ -1683,6 +1683,7 @@ instance (Binary t) => Binary (PTactic' t) where

1683 DoUnify -> putWord8 22

1684 CaseTac x1 -> do putWord8 23

1685 put x1

1686+ SourceFC -> putWord8 24

1686 get

1687 get

1687 = do i <- getWord8

1688 = do i <- getWord8

1688 case i of

1689 case i of

@@ -1733,6 +1734,7 @@ instance (Binary t) => Binary (PTactic' t) where

1733 22 -> return DoUnify

1734 22 -> return DoUnify

1734 23 -> do x1 <- get

1735 23 -> do x1 <- get

1735 return (CaseTac x1)

1736 return (CaseTac x1)

1737+ 24 -> return SourceFC

1736 _ -> error "Corrupted binary data for PTactic'"

1738 _ -> error "Corrupted binary data for PTactic'"

1737

1739

1738

1740

src/Idris/ParseExpr.hs+1

@@ -1296,6 +1296,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1296 <|> do reserved "fail"

1297 msg <- stringLiteral

1298 return $ TFail [Idris.Core.TT.TextPart msg]

1299+ <|> do reserved "sourceLocation"; return SourceFC

1299 <|> do lchar ':';

1300 <|> do lchar ':';

1300 ( (do reserved "q"; return Abandon)

1301 ( (do reserved "q"; return Abandon)

1301 <|> (do (reserved "e" <|> reserved "eval");

1302 <|> (do (reserved "e" <|> reserved "eval");

src/Idris/Prover.hs+6−3

@@ -245,9 +245,10 @@ ploop fn d prompt prf e h

245 Success (TEval t) -> evalTerm t e

246 Success (TDocStr x) -> docStr x

247 Success (TSearch t) -> search t

248+ Success tac ->

248− Success tac -> do (_, e) <- elabStep e saveState

249+ do (_, e) <- elabStep e saveState

249− (_, st) <- elabStep e (runTac autoSolve i fn tac)

250+ (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)

250− return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

251+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))

251 (\err -> return (False, e, False, prf, Left err))

252 (\err -> return (False, e, False, prf, Left err))

252 ideslavePutSExp "write-proof-state" (prf', length prf')

253 ideslavePutSExp "write-proof-state" (prf', length prf')

253 case res of

254 case res of

@@ -300,6 +301,8 @@ ploop fn d prompt prf e h

300 return (False, e, False, prf, Right action))

301 return (False, e, False, prf, Right action))

301 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

302 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

302

303

304+ proverFC = FC "(prover shell)" (0, 0) (0, 0)

305+

303 evalTerm t e = withErrorReflection $

306 evalTerm t e = withErrorReflection $

304 do ctxt <- getContext

307 do ctxt <- getContext

305 ist <- getIState

308 ist <- getIState

test/sourceLocation001/SourceLoc.idrnew file+98

@@ -0,0 +1,98 @@

1+module SourceLoc

3+import Language.Reflection

4+import Language.Reflection.Utils

6+%default total

8+||| A "function" that returns where it is called in the source

9+getLoc : {default tactics { sourceLocation } x : SourceLocation} -> SourceLocation

10+getLoc {x} = x

11+

12+||| A test of getLoc

13+fromRHS : SourceLocation

14+fromRHS = getLoc

15+

16+||| Testing getting source locations from RHS proof scripts

17+fromProofScript : SourceLocation

18+fromProofScript = proof sourceLocation

19+

20+||| Testing getting source locations from deferred proofs.

21+fromMetavar : SourceLocation

22+fromMetavar = ?meta

23+

24+--- Testing that getting source locations in ASTs constructed with DSL notation

25+data Ty = U | Arr Ty Ty

26+

27+interp : Ty -> Type

28+interp U = ()

29+interp (Arr x y) = interp x -> Either SourceLocation (interp y)

30+

31+using (ctxt : Vect n Ty)

32+ data Tm : Vect n Ty -> Ty -> Type where

33+ MkU : Tm ctxt U

34+ Var : (i : Fin n) -> Tm ctxt (index i ctxt)

35+ Lam : Tm (t::ctxt) t' -> Tm ctxt (Arr t t')

36+ App : Tm ctxt (Arr t t') -> Tm ctxt t -> Tm ctxt t'

37+ ||| A term that makes the program halt and print where it halted

38+ Die : {default tactics { sourceLocation } loc : SourceLocation} -> Tm ctxt t

39+

40+ data Env : Vect n Ty -> Type where

41+ Nil : Env []

42+ (::) : interp t -> Env ctxt -> Env (t::ctxt)

43+

44+ index : (i : Fin n) -> Env ctxt -> interp (index i ctxt)

45+ index FZ (x::env) = x

46+ index (FS i) (x::env) = index i env

47+

48+ run : Tm ctxt t -> Env ctxt -> Either SourceLocation (interp t)

49+ run MkU _ = pure ()

50+ run (Var i) env = pure $ index i env

51+ run (Lam bdy) env = pure $ \x => run bdy (x::env)

52+ run (App f x) env = !(run f env) !(run x env)

53+ run (Die {loc}) _ = Left loc

54+

55+

56+exec : Tm [] t -> IO ()

57+exec tm = case run tm [] of

58+ Left loc => putStrLn $ "Error at " ++ show loc

59+ Right _ => putStrLn $ "Success!"

60+

61+dsl lang

62+ variable = Var

63+ index_first = FZ

64+ index_next = FS

65+ lambda = Lam

66+

67+testTerm1 : Tm [] (Arr U U)

68+testTerm1 = lang (\x=>Die)

69+

70+testTerm2 : Tm [] U

71+testTerm2 = App testTerm1 MkU

72+

73+testTerm3 : Tm [] (Arr U U)

74+testTerm3 = lang (\x => MkU)

75+

76+testTerm4 : Tm [] U

77+testTerm4 = App testTerm3 MkU

78+

79+namespace Main

80+ main : IO ()

81+ main = do putStrLn "Testing using definition"

82+ print fromRHS

83+ putStrLn "Testing using inline tactics"

84+ print fromProofScript

85+ putStrLn "Testing using metavariable with later definition"

86+ print fromMetavar

87+ putStrLn "-----------------------"

88+ sequence_ $ with List [ exec testTerm1

89+ , exec testTerm2

90+ , exec testTerm3

91+ , exec testTerm4

92+ ]

93+---------- Proofs ----------

94+SourceLoc.meta = proof

95+ sourceLocation

96+

97+

98+

test/sourceLocation001/expectednew file+11

@@ -0,0 +1,11 @@

1+Testing using definition

2+FileLoc "SourceLoc.idr" (14, 11) (14, 11)

3+Testing using inline tactics

4+FileLoc "SourceLoc.idr" (18, 17) (18, 17)

5+Testing using metavariable with later definition

6+FileLoc "SourceLoc.idr" (94, 16) (94, 16)

7+-----------------------

8+Success!

9+Error at FileLoc "SourceLoc.idr" (68, 23) (68, 23)

10+Success!

11+Success!

test/sourceLocation001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ SourceLoc.idr -o sourceLocation001

3+./sourceLocation001

4+rm -f sourceLocation001 *.ibc