207ab7f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge remote-tracking branch 'refs/remotes/origin/wip/tactical' into wip/tactical

commit207ab7fc55489c84691ad45529692caf4b7acc49 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 8 Jun 2015, 14:41 (11 years ago) parent89c19be 9056a4a

14 files changed+65−29

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+14−10 src/Idris/ElabQuasiquote.hs+2−2 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+6−4 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+1−1 test/meta003/BadDef.idr+12 test/meta003/expected+6 test/meta003/run+3

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

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

20472047 sm xs (PHidden x) = PHidden (sm xs x)

20482048 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

20492049 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

20512051 sm xs x = x

20522052

20532053 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

21762176 mkUniq (PNoImplicits t) = liftM PNoImplicits (mkUniq t)

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

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

21802180 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

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

865865 | PUnquote PTerm -- ^ ~Term

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

868868 deriving (Eq, Data, Typeable)

869869

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

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

12341234

12351235data Using = UImplicit Name PTerm

12361236 | UConstraint Name [Name]

1237− deriving (Show, Eq)

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

12381238{-!

12391239deriving instance Binary Using

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

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

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

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

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

266266

267267instance NFData PAltType where

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

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

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

1616import Idris.Core.Evaluate

1717import Idris.Core.Unify

1818import Idris.Core.ProofTerm (getProofTerm)

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

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

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

2121import Idris.ErrReverse (errReverse)

2222import Idris.ElabQuasiquote (extractUnquotes)

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

11361136 delayElab 10 $ do focus h

11371137 dotterm

11381138 elab' ina fc t

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

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

11401140 do attack

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

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

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

11491149 focus n

11501150 elab' ina (Just fc') tm

11511151 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

11531153 solve

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

11551155

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

16971697 when autoSolve solveAll

16981698

16991699

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

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

1702− runTacTm tm'

1703− return ()

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

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

1702+ runTacTm tm'

1703+ return ()

17041704 where

17051705 eval tm = do ctxt <- get_context

17061706 return $ normaliseAll ctxt env (finalise tm)

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

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

17221722 clauses' <- forM clauses (\case

17231723 RMkFunClause lhs rhs ->

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

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

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

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

1726+ lift $ converts ctxt [] lty rty

17261727 return $ Right (lhs', rhs')

17271728 RMkImpossibleClause lhs ->

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

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

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

18131814 = fmap fst . checkClosed $

18141815 reflectFC fc

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

1817+ = fmap fst . checkClosed $

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

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

18161820 = do env <- get_env

18171821 fmap fst . checkClosed $ reflectEnv env

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

19601964 datatypes <- get_datatypes

19611965 env <- get_env

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

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

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

19641968 (newProof recH ctxt datatypes goalTT)

19651969 let tm_out = getProofTerm (pterm p)

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

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

16251625 put x2

16261626 PUniverse x1 -> do putWord8 38

16271627 put x1

1628− PRunElab x1 x2 -> do putWord8 39

1629− put x1

1630− put x2

1628+ PRunElab x1 x2 x3 -> do putWord8 39

1629+ put x1

1630+ put x2

1631+ put x3

16311632 PAs x1 x2 x3 -> do putWord8 40

16321633 put x1

16331634 put x2

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

17631764 return (PUniverse x1)

17641765 39 -> do x1 <- get

17651766 x2 <- get

1766− return (PRunElab x1 x2)

1767+ x3 <- get

1768+ return (PRunElab x1 x2 x3)

17671769 40 -> do x1 <- get

17681770 x2 <- get

17691771 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

test/meta003/BadDef.idrnew file+12

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

1+module BadDef

3+import Language.Reflection.Elab

5+mkN : String -> TTName

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

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