cb1805b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add local namespace access to Elab

commitcb1805b37934b545c8b8fa3eadde1142e444abfc authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 4 Jun 2015, 12:52 (11 years ago) parent74bfa88

11 files changed+41−27

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+9 src/Idris/AbsSyntax.hs+5−5 src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/DSL.hs+2−2 src/Idris/DeepSeq.hs+1−1 src/Idris/Elab/Term.hs+10−7 src/Idris/ElabQuasiquote.hs+2−2 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+7−5 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+1−1

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

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

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

8989

9090 prim__SourceLocation : Elab SourceLocation

91+ prim__Namespace : Elab (List String)

9192

9293 prim__Forget : TT -> Elab Raw

9394

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

280281 fill (quote loc)

281282 solve

282283

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+

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

284293 |||

285294 ||| 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

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

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

10291029 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

10311031 en t = t

10321032

10331033 nselem x [] = False

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

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

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

14951495 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

14971497 imps top env _ = return ()

14981498

14991499 pibind using [] sc = sc

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

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

16191619 (fmap (ai True env ds) g)

16201620 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

16221622 ai qq env ds tm = tm

16231623

16241624 handleErr (Left err) = PElabError err

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

20422042 sm xs (PHidden x) = PHidden (sm xs x)

20432043 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

20442044 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

20462046 sm xs x = x

20472047

20482048 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

21712171 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

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

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

21752175 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

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

864864 | PUnquote PTerm -- ^ ~Term

865865 | 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.

867867 deriving (Eq, Data, Typeable)

868868

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

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

12331233

12341234data Using = UImplicit Name PTerm

12351235 | UConstraint Name [Name]

1236− deriving (Show, Eq)

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

12371237{-!

12381238deriving instance Binary Using

12391239deriving instance NFData Using

src/Idris/DSL.hs+2−2

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

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

113113

114114expandSugar 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

116116expandSugar dsl t = t

117117

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

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

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

199199 r' <- db' r

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

202202 db' t = return t

203203

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

src/Idris/DeepSeq.hs+1−1

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

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

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

263263 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` ()

265265

266266instance NFData PAltType where

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

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

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

11351135 delayElab 10 $ do focus h

11361136 dotterm

11371137 elab' ina fc t

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

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

11391139 do attack

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

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

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

11481148 focus n

11491149 elab' ina (Just fc') tm

11501150 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

11521152 solve

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

11541154

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

16961696 when autoSolve solveAll

16971697

16981698

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

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

1701− runTacTm tm'

1702− return ()

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

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

1701+ runTacTm tm'

1702+ return ()

17031703 where

17041704 eval tm = do ctxt <- get_context

17051705 return $ normaliseAll ctxt env (finalise tm)

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

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

18131813 = fmap fst . checkClosed $

18141814 reflectFC fc

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

1816+ = fmap fst . checkClosed $

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

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

18161819 = do env <- get_env

18171820 fmap fst . checkClosed $ reflectEnv env

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

19601963 datatypes <- get_datatypes

19611964 env <- get_env

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

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

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

19641967 (newProof recH ctxt datatypes goalTT)

19651968 let tm_out = getProofTerm (pterm p)

19661969 updateAux $ const aux'

src/Idris/ElabQuasiquote.hs+2−2

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

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

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

168168 extractUnquotes (n-1) tm

169−extractUnquotes n (PRunElab fc tm)

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

169+extractUnquotes n (PRunElab fc tm ns)

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

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

172172

173173

src/Idris/Error.hs+1−1

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

150150warnDisamb ist (PQuoteName _) = return ()

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

152152warnDisamb 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

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 111

44+ibcVersion = 112

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

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

16211621 put x2

16221622 PUniverse x1 -> do putWord8 38

16231623 put x1

1624− PRunElab x1 x2 -> do putWord8 39

1625− put x1

1626− put x2

1624+ PRunElab x1 x2 x3 -> do putWord8 39

1625+ put x1

1626+ put x2

1627+ put x3

16271628 PAs x1 x2 x3 -> do putWord8 40

16281629 put x1

16291630 put x2

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

17591760 return (PUniverse x1)

17601761 39 -> do x1 <- get

17611762 x2 <- get

1762− return (PRunElab x1 x2)

1763+ x3 <- get

1764+ return (PRunElab x1 x2 x3)

17631765 40 -> do x1 <- get

17641766 x2 <- get

17651767 x3 <- get

src/Idris/IdrisDoc.hs+1−1

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

320320extractPTermNames (PDisamb _ p) = extract p

321321extractPTermNames (PUnifyLog p) = extract p

322322extractPTermNames (PNoImplicits p) = extract p

323−extractPTermNames (PRunElab _ p) = extract p

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

324324extractPTermNames _ = []

325325

326326-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+1−1

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

510510 fc <- getFC

511511 tm <- simpleExpr syn

512512 i <- get

513− return $ PRunElab fc tm

513+ return $ PRunElab fc tm (syn_namespace syn)

514514 <?> "new-style tactics expression"

515515

516516{- | Parses a disambiguation expression