cb1805b · Idris-dev · git.iko.soy

libs/prelude/Language/Reflection/Elab.idr+9

compare with master

unifiedsplit

@@ -88,6 +88,7 @@ data Elab : Type -> Type where

88 prim__Check : Raw -> Elab (TT, TT)

89

90 prim__SourceLocation : Elab SourceLocation

91+ prim__Namespace : Elab (List String)

91

92

92 prim__Forget : TT -> Elab Raw

93 prim__Forget : TT -> Elab Raw

93

94

@@ -280,6 +281,14 @@ namespace Tactics

280 fill (quote loc)

281 fill (quote loc)

281 solve

282 solve

282

283

284+ ||| Get the current namespace at the point of tactic execution. This

285+ ||| allows scripts to define top-level names conveniently.

286+ |||

287+ ||| The namespace is represented as a reverse-order list of strings,

288+ ||| just as in the representation of names.

289+ currentNamespace : Elab (List String)

290+ currentNamespace = prim__Namespace

291+

283 ||| Attempt to rewrite the goal using an equality.

292 ||| Attempt to rewrite the goal using an equality.

284 |||

293 |||

285 ||| The tactic searches the goal for applicable subterms, and

294 ||| The tactic searches the goal for applicable subterms, and

src/Idris/AbsSyntax.hs+5−5

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

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

1028 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1029 en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

1030− en (PRunElab fc tm) = PRunElab fc (en tm)

1030+ en (PRunElab fc tm ns) = PRunElab fc (en tm) ns

1031 en t = t

1032

1033 nselem x [] = False

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

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

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

1495 imps top env (PNoImplicits tm) = imps False env tm

1496− imps top env (PRunElab fc tm) = imps False env tm

1496+ imps top env (PRunElab fc tm ns) = imps False env tm

1497 imps top env _ = return ()

1498

1499 pibind using [] sc = sc

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

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

1619 (fmap (ai True env ds) g)

1620 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1621− ai qq env ds (PRunElab fc tm) = PRunElab fc (ai False env ds tm)

1621+ ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns

1622 ai qq env ds tm = tm

1623

1624 handleErr (Left err) = PElabError err

@@ -2042,7 +2042,7 @@ substMatchShadow n shs tm t = sm shs t where

2042 sm xs (PHidden x) = PHidden (sm xs x)

2043 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2044 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

2045− sm xs (PRunElab fc script) = PRunElab fc (sm xs script)

2045+ sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns

2046 sm xs x = x

2047

2048 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

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

2171 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

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

2173 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

2174− mkUniq (PRunElab fc ts) = liftM (PRunElab fc ) (mkUniq ts)

2174+ mkUniq (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq ts)

2175 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+2−2

@@ -863,7 +863,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

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

864 | PUnquote PTerm -- ^ ~Term

865 | PQuoteName Name -- ^ `{n}

866− | PRunElab FC PTerm -- ^ %runElab tm - New-style proof script

866+ | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

867 deriving (Eq, Data, Typeable)

868

869data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

@@ -1233,7 +1233,7 @@ initDSL = DSL (PRef f (sUN ">>="))

1233

1234data Using = UImplicit Name PTerm

1235 | UConstraint Name [Name]

1236− deriving (Show, Eq)

1236+ deriving (Show, Eq, Data, Typeable)

1237{-!

1238deriving instance Binary Using

1239deriving instance NFData Using

src/Idris/DSL.hs+2−2

@@ -112,7 +112,7 @@ expandSugar dsl (PDoBlock ds)

112 block b _ = PElabError (Msg "Invalid statement in do block")

113

114expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

115−expandSugar dsl (PRunElab fc tm) = PRunElab fc $ expandSugar dsl tm

115+expandSugar dsl (PRunElab fc tm ns) = PRunElab fc (expandSugar dsl tm) ns

116expandSugar dsl t = t

117

118-- | Replace DSL-bound variable in a term

@@ -198,7 +198,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

198 db' (PDPair fc p l t r) = do l' <- db' l

199 r' <- db' r

200 return (PDPair fc p l' t r')

201− db' (PRunElab fc t) = fmap (PRunElab fc) (db' t)

201+ db' (PRunElab fc t ns) = fmap (\tm -> PRunElab fc tm ns) (db' t)

202 db' t = return t

203

204 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+1−1

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

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

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

263 rnf (PQuoteName x1) = rnf x1 `seq` ()

264− rnf (PRunElab x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

264+ rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

265

266instance NFData PAltType where

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

src/Idris/Elab/Term.hs+10−7

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

1135 delayElab 10 $ do focus h

1136 dotterm

1137 elab' ina fc t

1138− elab' ina fc (PRunElab fc' tm) =

1138+ elab' ina fc (PRunElab fc' tm ns) =

1139 do attack

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

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

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

1148 focus n

1149 elab' ina (Just fc') tm

1150 env <- get_env

1151− runTactical ist (maybe fc' id fc) env (P Bound n' Erased)

1151+ runTactical ist (maybe fc' id fc) env (P Bound n' Erased) ns

1152 solve

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

1154

@@ -1696,10 +1696,10 @@ case_ ind autoSolve ist fn tm = do

1696 when autoSolve solveAll

1697

1698

1699−runTactical :: IState -> FC -> Env -> Term -> ElabD ()

1699+runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD ()

1700−runTactical ist fc env tm = do tm' <- eval tm

1700+runTactical ist fc env tm ns = do tm' <- eval tm

1701− runTacTm tm'

1701+ runTacTm tm'

1702− return ()

1702+ return ()

1703 where

1704 eval tm = do ctxt <- get_context

1705 return $ normaliseAll ctxt env (finalise tm)

@@ -1812,6 +1812,9 @@ runTactical ist fc env tm = do tm' <- eval tm

1812 | n == tacN "prim__SourceLocation", [] <- args

1813 = fmap fst . checkClosed $

1814 reflectFC fc

1815+ | n == tacN "prim__Namespace", [] <- args

1816+ = fmap fst . checkClosed $

1817+ rawList (RConstant StrType) (map (RConstant . Str) ns)

1815 | n == tacN "prim__Env", [] <- args

1818 | n == tacN "prim__Env", [] <- args

1816 = do env <- get_env

1819 = do env <- get_env

1817 fmap fst . checkClosed $ reflectEnv env

1820 fmap fst . checkClosed $ reflectEnv env

@@ -1960,7 +1963,7 @@ runTactical ist fc env tm = do tm' <- eval tm

1960 datatypes <- get_datatypes

1963 datatypes <- get_datatypes

1961 env <- get_env

1964 env <- get_env

1962 (_, ES (p, aux') _ _) <-

1965 (_, ES (p, aux') _ _) <-

1963− lift $ runElab aux (runTactical ist fc [] script)

1966+ lift $ runElab aux (runTactical ist fc [] script ns)

1964 (newProof recH ctxt datatypes goalTT)

1967 (newProof recH ctxt datatypes goalTT)

1965 let tm_out = getProofTerm (pterm p)

1968 let tm_out = getProofTerm (pterm p)

1966 updateAux $ const aux'

1969 updateAux $ const aux'

src/Idris/ElabQuasiquote.hs+2−2

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

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

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

168 extractUnquotes (n-1) tm

169−extractUnquotes n (PRunElab fc tm)

169+extractUnquotes n (PRunElab fc tm ns)

170− = fmap (\(tm', ex) -> (PRunElab fc tm', ex)) $ extractUnquotes n tm

170+ = fmap (\(tm', ex) -> (PRunElab fc tm' ns, ex)) $ extractUnquotes n tm

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

172

173

src/Idris/Error.hs+1−1

@@ -150,4 +150,4 @@ warnDisamb ist (PUnquote tm) = warnDisamb ist tm

150warnDisamb ist (PQuoteName _) = return ()

151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

153−warnDisamb ist (PRunElab _ tm) = warnDisamb ist tm

153+warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm

src/Idris/IBC.hs+7−5

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

41import Util.Zlib (decompressEither)

42

43ibcVersion :: Word16

44−ibcVersion = 111

44+ibcVersion = 112

45

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

@@ -1621,9 +1621,10 @@ instance Binary PTerm where

1621 put x2

1622 PUniverse x1 -> do putWord8 38

1623 put x1

1624− PRunElab x1 x2 -> do putWord8 39

1624+ PRunElab x1 x2 x3 -> do putWord8 39

1625− put x1

1625+ put x1

1626− put x2

1626+ put x2

1627+ put x3

1627 PAs x1 x2 x3 -> do putWord8 40

1628 PAs x1 x2 x3 -> do putWord8 40

1628 put x1

1629 put x1

1629 put x2

1630 put x2

@@ -1759,7 +1760,8 @@ instance Binary PTerm where

1759 return (PUniverse x1)

1760 return (PUniverse x1)

1760 39 -> do x1 <- get

1761 39 -> do x1 <- get

1761 x2 <- get

1762 x2 <- get

1763+ x3 <- get

1762− return (PRunElab x1 x2)

1764+ return (PRunElab x1 x2 x3)

1763 40 -> do x1 <- get

1765 40 -> do x1 <- get

1764 x2 <- get

1766 x2 <- get

1765 x3 <- get

1767 x3 <- get

src/Idris/IdrisDoc.hs+1−1

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

320extractPTermNames (PDisamb _ p) = extract p

321extractPTermNames (PUnifyLog p) = extract p

322extractPTermNames (PNoImplicits p) = extract p

323−extractPTermNames (PRunElab _ p) = extract p

323+extractPTermNames (PRunElab _ p _) = extract p

324extractPTermNames _ = []

325

326-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+1−1

@@ -510,7 +510,7 @@ runElab syn = do try (lchar '%' *> reserved "runElab")

510 fc <- getFC

511 tm <- simpleExpr syn

512 i <- get

513− return $ PRunElab fc tm

513+ return $ PRunElab fc tm (syn_namespace syn)

514 <?> "new-style tactics expression"

515

516{- | Parses a disambiguation expression