git.iko.soy/Idris-dev
on master help sign in
Plumb source locations through Tactical's elab
commit13e8ad83b7b2691310de6670bb8574277525800f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 19 Feb 2015, 12:55 (12 years ago) parent2f96f33
8 files changed+23−19
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+4−4 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/DeepSeq.hs+1−1 src/Idris/ElabQuasiquote.hs+2−2 src/Idris/ElabTerm.hs+5−5 src/Idris/IBC.hs+6−4 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+3−1
src/Idris/AbsSyntax.hs+4−4
@@ -974,7 +974,7 @@ expandParams dec ps ns infs tm = en tm
974974 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
975975 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
976976 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
977− en (PRunTactics tm) = PRunTactics (en tm)
977+ en (PRunTactics fc tm) = PRunTactics fc (en tm)
978978 en t = t
979979
980980 nselem x [] = False
@@ -1445,7 +1445,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14451445 imps top env (PHidden tm) = imps False env tm
14461446 imps top env (PUnifyLog tm) = imps False env tm
14471447 imps top env (PNoImplicits tm) = imps False env tm
1448− imps top env (PRunTactics tm) = imps False env tm
1448+ imps top env (PRunTactics fc tm) = imps False env tm
14491449 imps top env _ = return ()
14501450
14511451 pibind using [] sc = sc
@@ -1567,7 +1567,7 @@ addImpl' inpat env infns ist ptm
15671567 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)
15681568 (fmap (ai True env ds) g)
15691569 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)
1570− ai qq env ds (PRunTactics tm) = PRunTactics (ai False env ds tm)
1570+ ai qq env ds (PRunTactics fc tm) = PRunTactics fc (ai False env ds tm)
15711571 ai qq env ds tm = tm
15721572
15731573 handleErr (Left err) = PElabError err
@@ -2092,5 +2092,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
20922092 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)
20932093 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)
20942094 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
2095− mkUniq (PRunTactics ts) = liftM PRunTactics (mkUniq ts)
2095+ mkUniq (PRunTactics fc ts) = liftM (PRunTactics fc ) (mkUniq ts)
20962096 mkUniq t = return t
src/Idris/AbsSyntaxTree.hs+1−1
@@ -791,7 +791,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
791791 | PNoImplicits PTerm -- ^ never run implicit converions on the term
792792 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])
793793 | PUnquote PTerm -- ^ ~Term
794− | PRunTactics PTerm -- ^ %run_tactics tm - New-style proof script
794+ | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script
795795 deriving (Eq, Data, Typeable)
796796
797797
src/Idris/DeepSeq.hs+1−1
@@ -239,7 +239,7 @@ instance NFData PTerm where
239239 rnf (PNoImplicits x1) = rnf x1 `seq` ()
240240 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
241241 rnf (PUnquote x1) = rnf x1 `seq` ()
242− rnf (PRunTactics x1) = rnf x1 `seq` ()
242+ rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
243243
244244instance (NFData t) => NFData (PTactic' t) where
245245 rnf (Intro x1) = rnf x1 `seq` ()
src/Idris/ElabQuasiquote.hs+2−2
@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)
170170 return (PRef (fileFC "(unquote)") n, [(n, tm)])
171171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $
172172 extractUnquotes (n-1) tm
173−extractUnquotes n (PRunTactics tm)
174− = fmap (\(tm', ex) -> (PRunTactics tm', ex)) $ extractUnquotes n tm
173+extractUnquotes n (PRunTactics fc tm)
174+ = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm
175175extractUnquotes n x = return (x, []) -- no subterms!
176176
177177
src/Idris/ElabTerm.hs+5−5
@@ -1029,7 +1029,7 @@ elab ist info emode opts fn tm
10291029 delayElab $ do focus h
10301030 dotterm
10311031 elab' ina fc t
1032− elab' ina fc (PRunTactics tm) =
1032+ elab' ina _ (PRunTactics fc tm) =
10331033 do attack
10341034 n <- getNameFrom (sMN 0 "tacticScript")
10351035 n' <- getNameFrom (sMN 0 "tacticExpr")
@@ -1038,10 +1038,10 @@ elab ist info emode opts fn tm
10381038 movelast n
10391039 letbind n' scriptTy (Var n)
10401040 focus n
1041− elab' ina fc tm
1041+ elab' ina (Just fc) tm
10421042 env <- get_env
10431043 ctxt <- get_context
1044− runTactical ctxt env (P Bound n' Erased)
1044+ runTactical fc ctxt env (P Bound n' Erased)
10451045 solve
10461046 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10471047
@@ -1465,8 +1465,8 @@ case_ ind autoSolve ist fn tm = do
14651465 else casetac (forget val)
14661466 when autoSolve solveAll
14671467
1468−runTactical :: Context -> Env -> Term -> ElabD ()
1469−runTactical ctxt env tm = runTacTm (eval tm) >> return ()
1468+runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1469+runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
14701470 where
14711471 eval = normaliseAll ctxt env
14721472 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
src/Idris/IBC.hs+6−4
@@ -36,7 +36,7 @@ import Codec.Compression.Zlib (compress)
3636import Util.Zlib (decompressEither)
3737
3838ibcVersion :: Word8
39−ibcVersion = 97
39+ibcVersion = 98
4040
4141data IBCFile = IBCFile { ver :: Word8,
4242 sourcefile :: FilePath,
@@ -1571,8 +1571,9 @@ instance Binary PTerm where
15711571 put x2
15721572 PUniverse x1 -> do putWord8 38
15731573 put x1
1574− PRunTactics x1 -> do putWord8 39
1575− put x1
1574+ PRunTactics x1 x2 -> do putWord8 39
1575+ put x1
1576+ put x2
15761577
15771578 get
15781579 = do i <- getWord8
@@ -1692,7 +1693,8 @@ instance Binary PTerm where
16921693 38 -> do x1 <- get
16931694 return (PUniverse x1)
16941695 39 -> do x1 <- get
1695− return (PRunTactics x1)
1696+ x2 <- get
1697+ return (PRunTactics x1 x2)
16961698 _ -> error "Corrupted binary data for PTerm"
16971699
16981700instance (Binary t) => Binary (PTactic' t) where
src/Idris/IdrisDoc.hs+1−1
@@ -318,7 +318,7 @@ extractPTermNames (PCoerced p) = extract p
318318extractPTermNames (PDisamb _ p) = extract p
319319extractPTermNames (PUnifyLog p) = extract p
320320extractPTermNames (PNoImplicits p) = extract p
321−extractPTermNames (PRunTactics p) = extract p
321+extractPTermNames (PRunTactics _ p) = extract p
322322extractPTermNames _ = []
323323
324324-- | Shorter name for extractPTermNames
src/Idris/ParseExpr.hs+3−1
@@ -495,8 +495,10 @@ RunTactics ::=
495495-}
496496runTactics :: SyntaxInfo -> IdrisParser PTerm
497497runTactics syn = do try (lchar '%' *> reserved "runTactics")
498+ fc <- getFC
498499 tm <- simpleExpr syn
499− return (PRunTactics tm)
500+ i <- get
501+ return $ debindApp syn (desugar syn i (PRunTactics fc tm))
500502 <?> "new-style tactics expression"
501503
502504{- | Parses a disambiguation expression