13e8ad8 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+4−4

compare with master

unifiedsplit

@@ -974,7 +974,7 @@ expandParams dec ps ns infs tm = en tm

974 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

975 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

976 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)

978 en t = t

979

980 nselem x [] = False

@@ -1445,7 +1445,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1445 imps top env (PHidden tm) = imps False env tm

1446 imps top env (PUnifyLog tm) = imps False env tm

1447 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

1449 imps top env _ = return ()

1450

1451 pibind using [] sc = sc

@@ -1567,7 +1567,7 @@ addImpl' inpat env infns ist ptm

1567 ai qq env ds (PQuasiquote tm g) = PQuasiquote (ai True env ds tm)

1568 (fmap (ai True env ds) g)

1569 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)

1571 ai qq env ds tm = tm

1572

1573 handleErr (Left err) = PElabError err

@@ -2092,5 +2092,5 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2092 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

2093 mkUniq (PProof ts) = liftM PProof (mapM mkUniqT ts)

2094 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)

2096 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

791 | PNoImplicits PTerm -- ^ never run implicit converions on the term

792 | PQuasiquote PTerm (Maybe PTerm) -- ^ `(Term [: Term])

793 | PUnquote PTerm -- ^ ~Term

794− | PRunTactics PTerm -- ^ %run_tactics tm - New-style proof script

794+ | PRunTactics FC PTerm -- ^ %runTactics tm - New-style proof script

795 deriving (Eq, Data, Typeable)

796

797

src/Idris/DeepSeq.hs+1−1

@@ -239,7 +239,7 @@ instance NFData PTerm where

239 rnf (PNoImplicits x1) = rnf x1 `seq` ()

240 rnf (PQuasiquote x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

241 rnf (PUnquote x1) = rnf x1 `seq` ()

242− rnf (PRunTactics x1) = rnf x1 `seq` ()

242+ rnf (PRunTactics x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

243

244instance (NFData t) => NFData (PTactic' t) where

245 rnf (Intro x1) = rnf x1 `seq` ()

src/Idris/ElabQuasiquote.hs+2−2

@@ -170,8 +170,8 @@ extractUnquotes n (PUnquote tm)

170 return (PRef (fileFC "(unquote)") n, [(n, tm)])

171 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

172 extractUnquotes (n-1) tm

173−extractUnquotes n (PRunTactics tm)

173+extractUnquotes n (PRunTactics fc tm)

174− = fmap (\(tm', ex) -> (PRunTactics tm', ex)) $ extractUnquotes n tm

174+ = fmap (\(tm', ex) -> (PRunTactics fc tm', ex)) $ extractUnquotes n tm

175extractUnquotes n x = return (x, []) -- no subterms!

176

177

src/Idris/ElabTerm.hs+5−5

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

1029 delayElab $ do focus h

1030 dotterm

1031 elab' ina fc t

1032− elab' ina fc (PRunTactics tm) =

1032+ elab' ina _ (PRunTactics fc tm) =

1033 do attack

1034 n <- getNameFrom (sMN 0 "tacticScript")

1035 n' <- getNameFrom (sMN 0 "tacticExpr")

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

1038 movelast n

1039 letbind n' scriptTy (Var n)

1040 focus n

1041− elab' ina fc tm

1041+ elab' ina (Just fc) tm

1042 env <- get_env

1043 ctxt <- get_context

1044− runTactical ctxt env (P Bound n' Erased)

1044+ runTactical fc ctxt env (P Bound n' Erased)

1045 solve

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

1047

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

1465 else casetac (forget val)

1466 when autoSolve solveAll

1467

1468−runTactical :: Context -> Env -> Term -> ElabD ()

1468+runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1469−runTactical ctxt env tm = runTacTm (eval tm) >> return ()

1469+runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1470 where

1471 eval = normaliseAll ctxt env

1472 tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

src/Idris/IBC.hs+6−4

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

36import Util.Zlib (decompressEither)

37

38ibcVersion :: Word8

39−ibcVersion = 97

39+ibcVersion = 98

40

41data IBCFile = IBCFile { ver :: Word8,

42 sourcefile :: FilePath,

@@ -1571,8 +1571,9 @@ instance Binary PTerm where

1571 put x2

1572 PUniverse x1 -> do putWord8 38

1573 put x1

1574− PRunTactics x1 -> do putWord8 39

1574+ PRunTactics x1 x2 -> do putWord8 39

1575− put x1

1575+ put x1

1576+ put x2

1576

1577

1577 get

1578 get

1578 = do i <- getWord8

1579 = do i <- getWord8

@@ -1692,7 +1693,8 @@ instance Binary PTerm where

1692 38 -> do x1 <- get

1693 38 -> do x1 <- get

1693 return (PUniverse x1)

1694 return (PUniverse x1)

1694 39 -> do x1 <- get

1695 39 -> do x1 <- get

1696+ x2 <- get

1695− return (PRunTactics x1)

1697+ return (PRunTactics x1 x2)

1696 _ -> error "Corrupted binary data for PTerm"

1698 _ -> error "Corrupted binary data for PTerm"

1697

1699

1698instance (Binary t) => Binary (PTactic' t) where

1700instance (Binary t) => Binary (PTactic' t) where

src/Idris/IdrisDoc.hs+1−1

@@ -318,7 +318,7 @@ extractPTermNames (PCoerced p) = extract p

318extractPTermNames (PDisamb _ p) = extract p

319extractPTermNames (PUnifyLog p) = extract p

320extractPTermNames (PNoImplicits p) = extract p

321−extractPTermNames (PRunTactics p) = extract p

321+extractPTermNames (PRunTactics _ p) = extract p

322extractPTermNames _ = []

323

324-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+3−1

@@ -495,8 +495,10 @@ RunTactics ::=

495-}

496runTactics :: SyntaxInfo -> IdrisParser PTerm

497runTactics syn = do try (lchar '%' *> reserved "runTactics")

498+ fc <- getFC

498 tm <- simpleExpr syn

499 tm <- simpleExpr syn

500+ i <- get

499− return (PRunTactics tm)

501+ return $ debindApp syn (desugar syn i (PRunTactics fc tm))

500 <?> "new-style tactics expression"

502 <?> "new-style tactics expression"

501

503

502{- | Parses a disambiguation expression

504{- | Parses a disambiguation expression