git.iko.soy/Idris-dev
on master help sign in
A new primitive tactic for getting source locations

The tactic sourceLocation fills the hole with the current location in the file. If such information is unavailable, it fails. This is to be used by DSL implementers to provide useful error messages that can't be caught at type-check time. Additionally, it may prove useful for debugging and assertion libraries, so they can report errors. Because the tactic merely fills out an implicit argument in a particular way, it doesn't break referential transparency, at least not of the core language. This is similar to the technique used in Scala Virtualized.

commitf1e161d562c860eea0518c4a2c9151b6d736899e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 27 Nov 2014, 15:18 (12 years ago) parent1437f86
16 files changed+306−141
compare with master
unifiedsplit
CHANGELOG+6 idris.cabal+4 libs/base/Language/Reflection.idr+9−1 libs/base/Language/Reflection/Errors.idr−4 src/Idris/AbsSyntaxTree.hs+5−2 src/Idris/Completion.hs+2−1 src/Idris/DeepSeq.hs+1 src/Idris/Elab/Clause.hs+5−3 src/Idris/ElabDecls.hs+1−1 src/Idris/ElabTerm.hs+150−125 src/Idris/IBC.hs+3−1 src/Idris/ParseExpr.hs+1 src/Idris/Prover.hs+6−3 test/sourceLocation001/SourceLoc.idr+98 test/sourceLocation001/expected+11 test/sourceLocation001/run+4
CHANGELOG+6
@@ -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.
6+
17New in 0.9.15:
28--------------
39* Two new tactics: skip and fail. Skip does nothing, and fail takes a string
idris.cabal+4
@@ -483,6 +483,10 @@ Extra-source-files:
483483 test/records003/*.idr
484484 test/records003/expected
485485
486+ test/sourceLocation001/run
487+ test/sourceLocation001/*.idr
488+ test/sourceLocation001/expected
489+
486490 test/sugar001/run
487491 test/sugar001/*.idr
488492 test/sugar001/expected
libs/base/Language/Reflection.idr+9−1
@@ -175,6 +175,11 @@ data Raw =
175175 RConstant Const
176176%name Raw tm, tm'
177177
178+data SourceLocation : Type where
179+ FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
180+
181+%name SourceLocation loc
182+
178183||| Error reports are a list of report parts
179184data ErrorReportPart =
180185 ||| A human-readable string
@@ -239,7 +244,9 @@ data Tactic =
239244 ||| Do nothing
240245 Skip |
241246 ||| 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
243250%name Tactic tac, tac'
244251
245252
@@ -477,3 +484,4 @@ instance Quotable Tactic where
477484 quote Compute = `(Compute)
478485 quote Skip = `(Skip)
479486 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
22
33import Language.Reflection
44
5−data SourceLocation : Type where
6− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
7−
8−%name SourceLocation loc
95
106data Err = Msg String
117 | InternalMsg String
src/Idris/AbsSyntaxTree.hs+5−2
@@ -50,12 +50,13 @@ data ElabWhat = ETypes | EDefns | EAll
5050data ElabInfo = EInfo { params :: [(Name, PTerm)],
5151 inblock :: Ctxt [Name], -- names in the block, and their params
5252 liftname :: Name -> Name,
53− namespace :: Maybe [String],
53+ namespace :: Maybe [String],
54+ elabFC :: Maybe FC,
5455 rec_elabDecl :: ElabWhat -> ElabInfo -> PDecl ->
5556 Idris () }
5657
5758toplevel :: ElabInfo
58−toplevel = EInfo [] emptyContext id Nothing (\_ _ _ -> fail "Not implemented")
59+toplevel = EInfo [] emptyContext id Nothing Nothing (\_ _ _ -> fail "Not implemented")
5960
6061eInfoNames :: ElabInfo -> [Name]
6162eInfoNames info = map fst (params info) ++ M.keys (inblock info)
@@ -809,6 +810,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name
809810 | Skip
810811 | TFail [ErrorReportPart]
811812 | Qed | Abandon
813+ | SourceFC
812814 deriving (Show, Eq, Functor, Foldable, Traversable)
813815{-!
814816deriving instance Binary PTactic'
@@ -839,6 +841,7 @@ instance Sized a => Sized (PTactic' a) where
839841 size Abandon = 1
840842 size Skip = 1
841843 size (TFail ts) = 1 + size ts
844+ size SourceFC = 1
842845
843846type PTactic = PTactic' PTerm
844847
src/Idris/Completion.hs+2−1
@@ -52,7 +52,8 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)
5252 , (":eval", Just ExprTArg)
5353 ] ++ map (\x -> (x, Nothing)) [
5454 "intros", "compute", "trivial", "search", "solve", "attack",
55− "unify", "state", "term", "undo", "qed", "abandon", ":q"
55+ "unify", "state", "term", "undo", "qed", "abandon", ":q",
56+ "sourceLocation"
5657 ]
5758tactics = map fst tacticArgs
5859
src/Idris/DeepSeq.hs+1
@@ -262,6 +262,7 @@ instance (NFData t) => NFData (PTactic' t) where
262262 rnf Abandon = ()
263263 rnf Skip = ()
264264 rnf (TFail x1) = rnf x1 `seq` ()
265+ rnf SourceFC = ()
265266
266267instance NFData ErrorReportPart where
267268 rnf (TermPart x1) = rnf x1 `seq` ()
src/Idris/Elab/Clause.hs+5−3
@@ -56,8 +56,10 @@ import Numeric
5656-- | Elaborate a collection of left-hand and right-hand pairs - that is, a
5757-- top-level definition.
5858elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()
59−elabClauses info fc opts n_in cs = let n = liftname info n_in in
60− do ctxt <- getContext
59+elabClauses info' fc opts n_in cs =
60+ do let n = liftname info n_in
61+ info = info' { elabFC = Just fc }
62+ ctxt <- getContext
6163 ist <- getIState
6264 optimise <- getOptimise
6365 let petrans = PETransform `elem` optimise
@@ -618,7 +620,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
618620 let uniqargs = findUnique (tt_ctxt ist) [] lhs_tm
619621 let newargs = filter (\(n,_) -> n `notElem` uniqargs) newargs_all
620622
621− let winfo = pinfo info newargs defs windex
623+ let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }
622624 let wb = map (mkStatic static_names) $
623625 map (expandParamsD False ist decorate newargs defs) whereblock
624626
src/Idris/ElabDecls.hs+1−1
@@ -62,7 +62,7 @@ import Util.Pretty(pretty, text)
6262
6363-- Top level elaborator info, supporting recursive elaboration
6464recinfo :: ElabInfo
65−recinfo = EInfo [] emptyContext id Nothing elabDecl'
65+recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'
6666
6767-- | Return the elaborated term which calls 'main'
6868elabMain :: Idris Term
src/Idris/ElabTerm.hs+150−125
@@ -144,7 +144,8 @@ elab ist info emode opts fn tm
144144 = do let loglvl = opt_logLevel (idris_options ist)
145145 when (loglvl > 5) $ unifyLog True
146146 compute -- expand type synonyms, etc
147− elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)
147+ let fc = maybe "(unknown)"
148+ elabE (False, False, False, False) (elabFC info) tm -- (in argument, guarded, in type, in qquote)
148149 end_unify
149150 ptm <- get_term
150151 when pattern -- convert remaining holes to pattern vars
@@ -166,11 +167,11 @@ elab ist info emode opts fn tm
166167
167168 toElab ina arg = case getTm arg of
168169 Placeholder -> Nothing
169− v -> Just (priority arg, elabE ina v)
170+ v -> Just (priority arg, elabE ina (elabFC info) v)
170171
171172 toElab' ina arg = case getTm arg of
172173 Placeholder -> Nothing
173− v -> Just (elabE ina v)
174+ v -> Just (elabE ina (elabFC info) v)
174175
175176 mkPat = do hs <- get_holes
176177 tm <- get_term
@@ -182,30 +183,30 @@ elab ist info emode opts fn tm
182183 -- and forces/delays. If you make a recursive call in elab', it is
183184 -- normally correct to call elabE - the ones that don't are desugarings
184185 -- typically
185− elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()
186− elabE ina t =
187− --do g <- goal
188− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
189− do ct <- insertCoerce ina t
190− t' <- insertLazy ct
191− g <- goal
192− tm <- get_term
193− ps <- get_probs
194− hs <- get_holes
195− --trace ("Elaborating " ++ show t' ++ " in " ++ show g
196− -- ++ "\n" ++ show tm
197− -- ++ "\nholes " ++ show hs
198− -- ++ "\nproblems " ++ show ps
199− -- ++ "\n-----------\n") $
200− --trace ("ELAB " ++ show t') $
201− let fc = fileFC "Force"
202− env <- get_env
203− handleError (forceErr env)
204− (elab' ina t')
205− (elab' ina (PApp fc (PRef fc (sUN "Force"))
206− [pimp (sUN "t") Placeholder True,
207− pimp (sUN "a") Placeholder True,
208− pexp ct])) True
186+ elabE :: (Bool, Bool, Bool, Bool) -> Maybe FC -> PTerm -> ElabD ()
187+ elabE ina fc' t =
188+ --do g <- goal
189+ --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
190+ do ct <- insertCoerce ina t
191+ t' <- insertLazy ct
192+ g <- goal
193+ tm <- get_term
194+ ps <- get_probs
195+ hs <- get_holes
196+ --trace ("Elaborating " ++ show t' ++ " in " ++ show g
197+ -- ++ "\n" ++ show tm
198+ -- ++ "\nholes " ++ show hs
199+ -- ++ "\nproblems " ++ show ps
200+ -- ++ "\n-----------\n") $
201+ --trace ("ELAB " ++ show t') $
202+ let fc = fileFC "Force"
203+ env <- get_env
204+ handleError (forceErr env)
205+ (elab' ina fc' t')
206+ (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))
207+ [pimp (sUN "t") Placeholder True,
208+ pimp (sUN "a") Placeholder True,
209+ pexp ct])) True
209210
210211 forceErr env (CantUnify _ t t' _ _ _)
211212 | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
@@ -235,35 +236,36 @@ elab ist info emode opts fn tm
235236 -- "guarded" means immediately under a constructor, to help find patvars
236237
237238 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
238240 -> PTerm -- ^ The term to elaborate
239241 -> ElabD ()
240− elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
241− elab' ina PType = do apply RType []; solve
242− elab' ina (PUniverse u) = do apply (RUType u) []; solve
242+ elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step
243+ elab' ina fc PType = do apply RType []; solve
244+ elab' ina fc (PUniverse u) = do apply (RUType u) []; solve
243245-- elab' (_,_,inty) (PConstant c)
244246-- | constType c && pattern && not reflection && not inty
245247-- = lift $ tfail (Msg "Typecase is not allowed")
246− elab' ina (PConstant c) = do apply (RConstant c) []; solve
247− elab' ina (PQuote r) = do fill r; solve
248− elab' ina (PTrue fc _) =
248+ elab' ina fc (PConstant c) = do apply (RConstant c) []; solve
249+ elab' ina fc (PQuote r) = do fill r; solve
250+ elab' ina _ (PTrue fc _) =
249251 do hnf_compute
250252 g <- goal
251253 case g of
252− TType _ -> elab' ina (PRef fc unitTy)
253− _ -> elab' ina (PRef fc unitCon)
254− elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
254+ TType _ -> elab' ina (Just fc) (PRef fc unitTy)
255+ _ -> elab' ina (Just fc) (PRef fc unitCon)
256+ elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
255257 = do g <- goal; resolveTC False 5 g fn ist
256− elab' ina (PResolveTC fc)
258+ elab' ina fc (PResolveTC fc')
257259 = do c <- getNameFrom (sMN 0 "class")
258260 instanceArg c
259− elab' ina (PRefl fc t)
260− = elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
261− pimp (sMN 0 "x") t False])
262− elab' ina (PEq fc Placeholder Placeholder l r)
261+ elab' ina _ (PRefl fc t)
262+ = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
263+ pimp (sMN 0 "x") t False])
264+ elab' ina _ (PEq fc Placeholder Placeholder l r)
263265 = try (do tyn <- getNameFrom (sMN 0 "aqty")
264266 claim tyn RType
265267 movelast tyn
266− elab' ina (PApp fc (PRef fc eqTy)
268+ elab' ina (Just fc) (PApp fc (PRef fc eqTy)
267269 [pimp (sUN "A") (PRef fc tyn) True,
268270 pimp (sUN "B") (PRef fc tyn) False,
269271 pexp l, pexp r]))
@@ -273,26 +275,26 @@ elab ist info emode opts fn tm
273275 movelast atyn
274276 claim btyn RType
275277 movelast btyn
276− elab' ina (PApp fc (PRef fc eqTy)
277− [pimp (sUN "A") (PRef fc atyn) True,
278− pimp (sUN "B") (PRef fc btyn) False,
279− pexp l, pexp r]))
280−
281− elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
282− [pimp (sUN "A") lt True,
283− pimp (sUN "B") rt False,
284− pexp l, pexp r])
285− elab' ina@(_, a, inty, qq) (PPair fc _ l r)
278+ elab' ina (Just fc) (PApp fc (PRef fc eqTy)
279+ [pimp (sUN "A") (PRef fc atyn) True,
280+ pimp (sUN "B") (PRef fc btyn) False,
281+ pexp l, pexp r]))
282+
283+ elab' ina _ (PEq fc lt rt l r) = elab' ina (Just fc) (PApp fc (PRef fc eqTy)
284+ [pimp (sUN "A") lt True,
285+ pimp (sUN "B") rt False,
286+ pexp l, pexp r])
287+ elab' ina@(_, a, inty, qq) _ (PPair fc _ l r)
286288 = do hnf_compute
287289 g <- goal
288290 case g of
289− TType _ -> elab' ina (PApp fc (PRef fc pairTy)
291+ TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
290292 [pexp l,pexp r])
291− _ -> elab' ina (PApp fc (PRef fc pairCon)
293+ _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
292294 [pimp (sUN "A") Placeholder False,
293295 pimp (sUN "B") Placeholder False,
294296 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)
296298 = case t of
297299 Placeholder ->
298300 do hnf_compute
@@ -301,18 +303,18 @@ elab ist info emode opts fn tm
301303 TType _ -> asType
302304 _ -> asValue
303305 _ -> asType
304− where asType = elab' ina (PApp fc (PRef fc sigmaTy)
306+ where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
305307 [pexp t,
306308 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)
308310 [pimp (sMN 0 "a") t False,
309311 pimp (sMN 0 "P") Placeholder True,
310312 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)
312314 [pimp (sMN 0 "a") t False,
313315 pimp (sMN 0 "P") Placeholder True,
314316 pexp l, pexp r])
315− elab' ina (PAlternative True as)
317+ elab' ina fc (PAlternative True as)
316318 = do hnf_compute
317319 ty <- goal
318320 ctxt <- get_context
@@ -322,24 +324,24 @@ elab ist info emode opts fn tm
322324-- trace (-- show tc ++ " " ++ show as ++ "\n ==> " ++
323325-- show (length as') ++ "\n" ++
324326-- 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'))
326328 where showHd (PApp _ (PRef _ n) _) = n
327329 showHd (PRef _ n) = n
328330 showHd (PApp _ h _) = showHd h
329331 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)
331333 = trySeq as
332334 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
334336 try' e1 (trySeq' e1 xs) True
335337 trySeq' deferr [] = proofFail deferr
336338 trySeq' deferr (x : xs)
337− = try' (elab' ina x) (trySeq' deferr xs) True
338− elab' ina (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats
339+ = try' (elab' ina fc x) (trySeq' deferr xs) True
340+ elab' ina _ (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats
339341-- elab' (_, _, inty) (PRef fc f)
340342-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
341343-- = 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)
343345 | (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
344346 = do ctxt <- get_context
345347 let defined = case lookupTy n ctxt of
@@ -358,9 +360,9 @@ elab ist info emode opts fn tm
358360 bindable (NS _ _) = False
359361 bindable (UN xs) = True
360362 bindable n = implicitable n
361− elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
362− elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
363− elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)
363+ elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp fc f [])
364+ elab' ina _ (PRef fc n) = erun fc $ do apply (Var n) []; solve
365+ elab' ina@(_, a, inty, qq) fc (PLam n Placeholder sc)
364366 = do -- if n is a type constructor name, this makes no sense...
365367 ctxt <- get_context
366368 when (isTConName n ctxt) $
@@ -368,8 +370,8 @@ elab ist info emode opts fn tm
368370 checkPiGoal n
369371 attack; intro (Just n);
370372 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
371− elabE (True, a, inty, qq) sc; solve
372− elab' ina@(_, a, inty, qq) (PLam n ty sc)
373+ elabE (True, a, inty, qq) fc sc; solve
374+ elab' ina@(_, a, inty, qq) fc (PLam n ty sc)
373375 = do tyn <- getNameFrom (sMN 0 "lamty")
374376 -- if n is a type constructor name, this makes no sense...
375377 ctxt <- get_context
@@ -383,12 +385,12 @@ elab ist info emode opts fn tm
383385 hs <- get_holes
384386 introTy (Var tyn) (Just n)
385387 focus tyn
386− elabE (True, a, True, qq) ty
387− elabE (True, a, inty, qq) sc
388+ elabE (True, a, True, qq) fc ty
389+ elabE (True, a, inty, qq) fc sc
388390 solve
389− elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)
390− = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve
391− elab' ina@(_, a, _, qq) (PPi _ n ty sc)
391+ elab' ina@(_, a, _, qq) fc (PPi _ n Placeholder sc)
392+ = do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) fc sc; solve
393+ elab' ina@(_, a, _, qq) fc (PPi _ n ty sc)
392394 = do attack; tyn <- getNameFrom (sMN 0 "ty")
393395 claim tyn RType
394396 n' <- case n of
@@ -396,10 +398,10 @@ elab ist info emode opts fn tm
396398 _ -> return n
397399 forall n' (Var tyn)
398400 focus tyn
399− elabE (True, a, True, qq) ty
400− elabE (True, a, True, qq) sc
401+ elabE (True, a, True, qq) fc ty
402+ elabE (True, a, True, qq) fc sc
401403 solve
402− elab' ina@(_, a, inty, qq) (PLet n ty val sc)
404+ elab' ina@(_, a, inty, qq) fc (PLet n ty val sc)
403405 = do attack
404406 ivs <- get_instances
405407 tyn <- getNameFrom (sMN 0 "letty")
@@ -412,12 +414,12 @@ elab ist info emode opts fn tm
412414 Placeholder -> return ()
413415 _ -> do focus tyn
414416 explicit tyn
415− elabE (True, a, True, qq) ty
417+ elabE (True, a, True, qq) fc ty
416418 focus valn
417− elabE (True, a, True, qq) val
419+ elabE (True, a, True, qq) fc val
418420 ivs' <- get_instances
419421 env <- get_env
420− elabE (True, a, inty, qq) sc
422+ elabE (True, a, inty, qq) fc sc
421423 when (not pattern) $
422424 mapM_ (\n -> do focus n
423425 g <- goal
@@ -433,7 +435,7 @@ elab ist info emode opts fn tm
433435 expandLet n (case lookup n env of
434436 Just (Let t v) -> v)
435437 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
437439 rty <- goal
438440 attack
439441 tyn <- getNameFrom (sMN 0 "letty")
@@ -442,14 +444,14 @@ elab ist info emode opts fn tm
442444 claim valn (Var tyn)
443445 letbind n (Var tyn) (Var valn)
444446 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)])
446448 env <- get_env
447449 computeLet n
448− elabE (True, a, inty, qq) sc
450+ elabE (True, a, inty, qq) (Just fc) sc
449451 solve
450−-- elab' ina (PLet n Placeholder
452+-- elab' ina fc (PLet n Placeholder
451453-- (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
453455 rty <- goal
454456 ds <- get_deferred
455457 ctxt <- get_context
@@ -486,7 +488,8 @@ elab ist info emode opts fn tm
486488 _ -> Nothing
487489 localVar env _ = Nothing
488490
489− elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
491+ elabIArg ((n, (True, ty)), def) =
492+ do focus n; elabE ina (Just fc) (getTm def)
490493 elabIArg _ = return () -- already done, just a name
491494
492495 mkN n@(NS _ _) = n
@@ -495,7 +498,7 @@ elab ist info emode opts fn tm
495498 Just xs@(_:_) -> sNS n xs
496499 _ -> n
497500
498− elab' ina (PMatchApp fc fn)
501+ elab' ina _ (PMatchApp fc fn)
499502 = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
500503 [(n, args)] -> return (n, map (const True) args)
501504 _ -> lift $ tfail (NoSuchVariable fn)
@@ -507,12 +510,12 @@ elab ist info emode opts fn tm
507510-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
508511-- = lift $ tfail (Msg "Typecase is not allowed")
509512 -- 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)
511514 = do env <- get_env
512515 if (f `elem` map fst env && length args == 1)
513516 then -- simple app, as below
514− do simple_app (elabE (ina, g, inty, qq) (PRef fc f))
515− (elabE (True, g, inty, qq) (getTm (head args)))
517+ do simple_app (elabE (ina, g, inty, qq) (Just fc) (PRef fc f))
518+ (elabE (True, g, inty, qq) (Just fc) (getTm (head args)))
516519 (show tm)
517520 solve
518521 else
@@ -630,14 +633,14 @@ elab ist info emode opts fn tm
630633 setInjective (PApp _ (PRef _ n) _) = setinj n
631634 setInjective _ = return ()
632635
633− elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])
636+ elab' ina@(_, a, inty, qq) _ tm@(PApp fc f [arg])
634637 = 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))
636639 (show tm)
637640 solve
638− elab' ina Placeholder = do (h : hs) <- get_holes
639− movelast h
640− elab' ina (PMetavar n) =
641+ elab' ina fc Placeholder = do (h : hs) <- get_holes
642+ movelast h
643+ elab' ina fc (PMetavar n) =
641644 do ptm <- get_term
642645 -- When building the metavar application, leave out the unique
643646 -- names which have been used elsewhere in the term, since we
@@ -651,12 +654,12 @@ elab ist info emode opts fn tm
651654 mkN n = case namespace info of
652655 Just xs@(_:_) -> sNS n xs
653656 _ -> n
654− elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts
655− elab' ina (PTactics ts)
656− | not pattern = do mapM_ (runTac False ist fn) ts
657− | otherwise = elab' ina Placeholder
658− elab' ina (PElabError e) = fail (pshow ist e)
659− elab' ina (PRewrite fc r sc newg)
657+ elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
658+ elab' ina fc (PTactics ts)
659+ | not pattern = do mapM_ (runTac False ist fc fn) ts
660+ | otherwise = elab' ina fc Placeholder
661+ elab' ina fc (PElabError e) = fail (pshow ist e)
662+ elab' ina _ (PRewrite fc r sc newg)
660663 = do attack
661664 tyn <- getNameFrom (sMN 0 "rty")
662665 claim tyn RType
@@ -665,14 +668,14 @@ elab ist info emode opts fn tm
665668 letn <- getNameFrom (sMN 0 "_rewrite_rule")
666669 letbind letn (Var tyn) (Var valn)
667670 focus valn
668− elab' ina r
671+ elab' ina (Just fc) r
669672 compute
670673 g <- goal
671674 rewrite (Var letn)
672675 g' <- goal
673676 when (g == g') $ lift $ tfail (NoRewriting g)
674677 case newg of
675− Nothing -> elab' ina sc
678+ Nothing -> elab' ina (Just fc) sc
676679 Just t -> doEquiv t sc
677680 solve
678681 where doEquiv t sc =
@@ -684,12 +687,12 @@ elab ist info emode opts fn tm
684687 letn <- getNameFrom (sMN 0 "equiv_val")
685688 letbind letn (Var tyn) (Var valn)
686689 focus tyn
687− elab' ina t
690+ elab' ina (Just fc) t
688691 focus valn
689− elab' ina sc
690− elab' ina (PRef fc letn)
692+ elab' ina (Just fc) sc
693+ elab' ina (Just fc) (PRef fc letn)
691694 solve
692− elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)
695+ elab' ina@(_, a, inty, qq) _ c@(PCase fc scr opts)
693696 = do attack
694697 tyn <- getNameFrom (sMN 0 "scty")
695698 claim tyn RType
@@ -698,7 +701,7 @@ elab ist info emode opts fn tm
698701 claim valn (Var tyn)
699702 letbind scvn (Var tyn) (Var valn)
700703 focus valn
701− elabE (True, a, inty, qq) scr
704+ elabE (True, a, inty, qq) (Just fc) scr
702705 -- Solve any remaining implicits - we need to solve as many
703706 -- as possible before making the 'case' type
704707 unifyProblems
@@ -714,7 +717,7 @@ elab ist info emode opts fn tm
714717
715718 cname <- unique_hole' True (mkCaseName fn)
716719 let cname' = mkN cname
717−-- elab' ina (PMetavar cname')
720+-- elab' ina fc (PMetavar cname')
718721 attack; defer argsDropped cname'; solve
719722
720723 -- if the scrutinee is one of the 'args' in env, we should
@@ -776,10 +779,10 @@ elab ist info emode opts fn tm
776779 ((n,b) : args)
777780 Nothing -> extendAcc ns acc args
778781
779− elab' ina (PUnifyLog t) = do unifyLog True
780− elab' ina t
781− unifyLog False
782− elab' (ina, g, inty, qq) (PQuasiquote t goal) -- TODO: goal type
782+ elab' ina fc (PUnifyLog t) = do unifyLog True
783+ elab' ina fc t
784+ unifyLog False
785+ elab' (ina, g, inty, qq) fc (PQuasiquote t goal) -- TODO: goal type
783786 = do -- First extract the unquoted subterms, replacing them with fresh
784787 -- names in the quasiquoted term. Claim their reflections to be
785788 -- of type TT.
@@ -824,11 +827,11 @@ elab ist info emode opts fn tm
824827 case goal of
825828 Nothing -> return ()
826829 Just gTy -> do focus qTy
827− elabE (ina, g, inty, True) gTy
830+ elabE (ina, g, inty, True) fc gTy
828831
829832 -- Elaborate the quasiquoted term into the hole
830833 focus qTm
831− elabE (ina, g, inty, True) t
834+ elabE (ina, g, inty, True) fc t
832835 end_unify
833836
834837 -- We now have an elaborated term. Reflect it and solve the
@@ -854,11 +857,11 @@ elab ist info emode opts fn tm
854857
855858 elabUnquote (n, tm)
856859 = do focus n
857− elabE (ina, g, inty, False) tm
860+ elabE (ina, g, inty, False) fc tm
858861
859862
860− elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
861− elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
863+ elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
864+ elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
862865
863866 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
864867 isScr (PRef _ n) (n', b) = (n', (n == n', b))
@@ -994,7 +997,7 @@ elab ist info emode opts fn tm
994997 g <- goal
995998 ulog <- getUnifyLog
996999 traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
997− elab ina t; return failed
1000+ elab ina (Just fc) t; return failed
9981001 False -> return failed
9991002 done_elaborating_arg f argName
10001003 elabArgs ist ina failed fc r f ns force args
@@ -1227,8 +1230,8 @@ case_ ind autoSolve ist fn tm = do
12271230-- Running tactics directly
12281231-- if a tactic adds unification problems, return an error
12291232
1230−runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
1231−runTac autoSolve ist fn tac
1233+runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
1234+runTac autoSolve ist perhapsFC fn tac
12321235 = do env <- get_env
12331236 g <- goal
12341237 let tac' = fmap (addImplBound ist (map fst env)) tac
@@ -1427,7 +1430,7 @@ runTac autoSolve ist fn tac
14271430 ctxt <- get_context
14281431 env <- get_env
14291432 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'))
14311434 runT (Fill v) = do attack -- let x = fill x in ...
14321435 tyn <- getNameFrom (sMN 0 "letty")
14331436 claim tyn RType
@@ -1442,7 +1445,7 @@ runTac autoSolve ist fn tac
14421445 env <- get_env
14431446 let value' = normalise ctxt env value
14441447 rawValue <- reifyRaw value'
1445− runTac autoSolve ist fn (Exact $ PQuote rawValue)
1448+ runTac autoSolve ist perhapsFC fn (Exact $ PQuote rawValue)
14461449 runT (GoalType n tac) = do g <- goal
14471450 case unApply g of
14481451 (P _ n' _, _) ->
@@ -1454,10 +1457,31 @@ runTac autoSolve ist fn tac
14541457 return ()
14551458 runT Skip = return ()
14561459 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
14571481 runT x = fail $ "Not implemented " ++ show x
14581482
14591483 runReflected t = do t' <- reify ist t
1460− runTac autoSolve ist fn t'
1484+ runTac autoSolve ist perhapsFC fn t'
14611485
14621486-- | Prefix a name with the "Language.Reflection" namespace
14631487reflm :: String -> Name
@@ -1472,6 +1496,7 @@ reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
14721496reify _ (P _ n _) | n == reflm "Solve" = return Solve
14731497reify _ (P _ n _) | n == reflm "Compute" = return Compute
14741498reify _ (P _ n _) | n == reflm "Skip" = return Skip
1499+reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
14751500reify ist t@(App _ _)
14761501 | (P _ f _, args) <- unApply t = reifyApp ist f args
14771502reify _ t = fail ("Unknown tactic " ++ show t)
src/Idris/IBC.hs+3−1
@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)
3232import Util.Zlib (decompressEither)
3333
3434ibcVersion :: Word8
35−ibcVersion = 84
35+ibcVersion = 85
3636
3737data IBCFile = IBCFile { ver :: Word8,
3838 sourcefile :: FilePath,
@@ -1683,6 +1683,7 @@ instance (Binary t) => Binary (PTactic' t) where
16831683 DoUnify -> putWord8 22
16841684 CaseTac x1 -> do putWord8 23
16851685 put x1
1686+ SourceFC -> putWord8 24
16861687 get
16871688 = do i <- getWord8
16881689 case i of
@@ -1733,6 +1734,7 @@ instance (Binary t) => Binary (PTactic' t) where
17331734 22 -> return DoUnify
17341735 23 -> do x1 <- get
17351736 return (CaseTac x1)
1737+ 24 -> return SourceFC
17361738 _ -> error "Corrupted binary data for PTactic'"
17371739
17381740
src/Idris/ParseExpr.hs+1
@@ -1296,6 +1296,7 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (
12961296 <|> do reserved "fail"
12971297 msg <- stringLiteral
12981298 return $ TFail [Idris.Core.TT.TextPart msg]
1299+ <|> do reserved "sourceLocation"; return SourceFC
12991300 <|> do lchar ':';
13001301 ( (do reserved "q"; return Abandon)
13011302 <|> (do (reserved "e" <|> reserved "eval");
src/Idris/Prover.hs+6−3
@@ -245,9 +245,10 @@ ploop fn d prompt prf e h
245245 Success (TEval t) -> evalTerm t e
246246 Success (TDocStr x) -> docStr x
247247 Success (TSearch t) -> search t
248− Success tac -> do (_, e) <- elabStep e saveState
249− (_, st) <- elabStep e (runTac autoSolve i fn tac)
250− return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
248+ Success tac ->
249+ do (_, e) <- elabStep e saveState
250+ (_, st) <- elabStep e (runTac autoSolve i (Just proverFC) fn tac)
251+ return (True, st, False, prf ++ [step], Right $ iPrintResult ""))
251252 (\err -> return (False, e, False, prf, Left err))
252253 ideslavePutSExp "write-proof-state" (prf', length prf')
253254 case res of
@@ -300,6 +301,8 @@ ploop fn d prompt prf e h
300301 return (False, e, False, prf, Right action))
301302 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
302303
304+ proverFC = FC "(prover shell)" (0, 0) (0, 0)
305+
303306 evalTerm t e = withErrorReflection $
304307 do ctxt <- getContext
305308 ist <- getIState
test/sourceLocation001/SourceLoc.idrnew file+98
@@ -0,0 +1,98 @@
1+module SourceLoc
2+
3+import Language.Reflection
4+import Language.Reflection.Utils
5+
6+%default total
7+
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