207ab7f · 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

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

2047 sm xs (PHidden x) = PHidden (sm xs x)

2048 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2049 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

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

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

2051 sm xs x = x

2052

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

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

2176 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

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

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

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

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

2180 mkUniq t = return t

src/Idris/AbsSyntaxTree.hs+2−2

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

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

865 | PUnquote PTerm -- ^ ~Term

866 | PQuoteName Name -- ^ `{n}

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

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

868 deriving (Eq, Data, Typeable)

869

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

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

1234

1235data Using = UImplicit Name PTerm

1236 | UConstraint Name [Name]

1237− deriving (Show, Eq)

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

1238{-!

1239deriving instance Binary Using

1240deriving 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

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

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

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

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

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

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

266

267instance NFData PAltType where

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

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

@@ -16,7 +16,7 @@ import Idris.Core.TT

16import Idris.Core.Evaluate

17import Idris.Core.Unify

18import Idris.Core.ProofTerm (getProofTerm)

19−import Idris.Core.Typecheck (check, recheck, isType)

19+import Idris.Core.Typecheck (check, recheck, converts, isType)

20import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

21import Idris.ErrReverse (errReverse)

22import Idris.ElabQuasiquote (extractUnquotes)

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

1136 delayElab 10 $ do focus h

1137 dotterm

1138 elab' ina fc t

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

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

1140 do attack

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

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

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

1149 focus n

1150 elab' ina (Just fc') tm

1151 env <- get_env

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

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

1153 solve

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

1155

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

1697 when autoSolve solveAll

1698

1699

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

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

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

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

1702− runTacTm tm'

1702+ runTacTm tm'

1703− return ()

1703+ return ()

1704 where

1705 eval tm = do ctxt <- get_context

1706 return $ normaliseAll ctxt env (finalise tm)

@@ -1721,8 +1721,9 @@ runTactical ist fc env tm = do tm' <- eval tm

1721 let info = CaseInfo True True False -- TODO document and figure out

1722 clauses' <- forM clauses (\case

1723 RMkFunClause lhs rhs ->

1724− do lhs' <- fmap fst . lift $ check ctxt [] lhs

1724+ do (lhs', lty) <- lift $ check ctxt [] lhs

1725− rhs' <- fmap fst . lift $ check ctxt [] rhs

1725+ (rhs', rty) <- lift $ check ctxt [] rhs

1726+ lift $ converts ctxt [] lty rty

1726 return $ Right (lhs', rhs')

1727 return $ Right (lhs', rhs')

1727 RMkImpossibleClause lhs ->

1728 RMkImpossibleClause lhs ->

1728 do lhs' <- fmap fst . lift $ check ctxt [] lhs

1729 do lhs' <- fmap fst . lift $ check ctxt [] lhs

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

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

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

1813 = fmap fst . checkClosed $

1814 = fmap fst . checkClosed $

1814 reflectFC fc

1815 reflectFC fc

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

1817+ = fmap fst . checkClosed $

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

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

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

1816 = do env <- get_env

1820 = do env <- get_env

1817 fmap fst . checkClosed $ reflectEnv env

1821 fmap fst . checkClosed $ reflectEnv env

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

1960 datatypes <- get_datatypes

1964 datatypes <- get_datatypes

1961 env <- get_env

1965 env <- get_env

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

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

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

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

1964 (newProof recH ctxt datatypes goalTT)

1968 (newProof recH ctxt datatypes goalTT)

1965 let tm_out = getProofTerm (pterm p)

1969 let tm_out = getProofTerm (pterm p)

1966 updateAux $ const aux'

1970 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+6−4

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

1625 put x2

1626 PUniverse x1 -> do putWord8 38

1627 put x1

1628− PRunElab x1 x2 -> do putWord8 39

1628+ PRunElab x1 x2 x3 -> do putWord8 39

1629− put x1

1629+ put x1

1630− put x2

1630+ put x2

1631+ put x3

1631 PAs x1 x2 x3 -> do putWord8 40

1632 PAs x1 x2 x3 -> do putWord8 40

1632 put x1

1633 put x1

1633 put x2

1634 put x2

@@ -1763,7 +1764,8 @@ instance Binary PTerm where

1763 return (PUniverse x1)

1764 return (PUniverse x1)

1764 39 -> do x1 <- get

1765 39 -> do x1 <- get

1765 x2 <- get

1766 x2 <- get

1767+ x3 <- get

1766− return (PRunElab x1 x2)

1768+ return (PRunElab x1 x2 x3)

1767 40 -> do x1 <- get

1769 40 -> do x1 <- get

1768 x2 <- get

1770 x2 <- get

1769 x3 <- get

1771 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

test/meta003/BadDef.idrnew file+12

@@ -0,0 +1,12 @@

1+module BadDef

2+

3+import Language.Reflection.Elab

4+

5+mkN : String -> TTName

6+mkN n = NS (UN n) ["BadDef"]

7+

8+mkBadDef1 : Elab ()

9+mkBadDef1 = do declareType $ Declare (mkN "bad1") [] `(() -> ())

10+ defineFunction $ DefineFun (mkN "bad1") [MkFunClause `(():()) `("hi")]

11+runBad1 : ()

12+runBad1 = %runElab (mkBadDef1 *> search)

test/meta003/expectednew file+6

@@ -0,0 +1,6 @@

1+BadDef.idr:12:9:

2+When checking right hand side of runBad1:

3+Type mismatch between

4+ ()

5+and

6+ String

test/meta003/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ --nocolour --check --consolewidth 70 BadDef.idr

3+rm -f *.ibc