32269f8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2711 from david-christiansen/no-more-ugly-script

Improvements to Elab user-friendliness

commit32269f8e438497110e7056c402c4c05d5f913940 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 9 Oct 2015, 08:31 (11 years ago) parent76f9286 32ce95f

9 files changed+78−25

compare with master

unifiedsplit

libs/prelude/Language/Reflection/Elab.idr+41−17 src/Idris/Core/Binary.hs+3 src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+1 src/Idris/Delaborate.hs+4 src/Idris/Elab/Term.hs+19−4 src/Idris/IBC.hs+1−1 test/meta002/Tacs.idr+7−2 test/meta002/expected+1−1

libs/prelude/Language/Reflection/Elab.idr+41−17

@@ -183,27 +183,28 @@ namespace Tactics

183183 fail : List ErrorReportPart -> Elab a

184184 fail err = prim__Fail err

185185

186− ||| Look up the lexical binding at the focused hole

186+ ||| Look up the lexical binding at the focused hole. Fails if no holes are present.

187187 getEnv : Elab (List (TTName, Binder TT))

188188 getEnv = prim__Env

189189

190− ||| Get the name and type of the focused hole

190+ ||| Get the name and type of the focused hole. Fails if not holes are present.

191191 getGoal : Elab (TTName, TT)

192192 getGoal = prim__Goal

193193

194− ||| Get the hole queue, in order

194+ ||| Get the hole queue, in order.

195195 getHoles : Elab (List TTName)

196196 getHoles = prim__Holes

197197

198− ||| If the current hole contains a guess, return it

198+ ||| If the current hole contains a guess, return it. Otherwise, fail.

199199 getGuess : Elab (Maybe TT)

200200 getGuess = prim__Guess

201201

202− ||| Look up the types of every overloading of a name

202+ ||| Look up the types of every overloading of a name.

203203 lookupTy : TTName -> Elab (List (TTName, NameType, TT))

204204 lookupTy n = prim__LookupTy n

205205

206− ||| Get the type of a fully-qualified name

206+ ||| Get the type of a fully-qualified name. Fail if it doesn not

207+ ||| resolve uniquely.

207208 lookupTyExact : TTName -> Elab (TTName, NameType, TT)

208209 lookupTyExact n = case !(lookupTy n) of

209210 [res] => return res

@@ -211,28 +212,29 @@ namespace Tactics

211212 xs => fail [NamePart n, TextPart "is ambiguous."]

212213

213214 ||| Find the reflected representation of all datatypes whose names

214− ||| are overloadings of some name

215+ ||| are overloadings of some name.

215216 lookupDatatype : TTName -> Elab (List Datatype)

216217 lookupDatatype n = prim__LookupDatatype n

217218

218219 ||| Find the reflected representation of a datatype, given its

219− ||| fully-qualified name.

220+ ||| fully-qualified name. Fail if the name does not uniquely resolve

221+ ||| to a datatype.

220222 lookupDatatypeExact : TTName -> Elab Datatype

221223 lookupDatatypeExact n = case !(lookupDatatype n) of

222224 [res] => return res

223225 [] => fail [TextPart "No datatype named", NamePart n]

224226 xs => fail [TextPart "More than one datatype named", NamePart n]

225227

226− ||| Attempt to type-check a term, getting back itself and its type

228+ ||| Attempt to type-check a term, getting back itself and its type.

227229 check : (tm : Raw) -> Elab (TT, TT)

228230 check tm = prim__Check tm

229231

230232 ||| Convert a type-annotated reflected term to its untyped

231− ||| equivalent

233+ ||| equivalent.

232234 forgetTypes : TT -> Elab Raw

233235 forgetTypes tt = prim__Forget tt

234236

235− ||| Get the goal type as a Raw term

237+ ||| Get the goal type as a Raw term. Fails if there are no holes.

236238 goalType : Elab Raw

237239 goalType = do g <- getGoal

238240 forgetTypes (snd g)

@@ -249,7 +251,8 @@ namespace Tactics

249251 solve : Elab ()

250252 solve = prim__Solve

251253

252− ||| Place a term into a hole, unifying its type

254+ ||| Place a term into a hole, unifying its type. Fails if the focus

255+ ||| is not a hole.

253256 fill : Raw -> Elab ()

254257 fill tm = prim__Fill tm

255258

@@ -297,7 +300,8 @@ namespace Tactics

297300 Elab (List (TTName, TTName))

298301 matchApply tm argSpec = prim__Apply tm argSpec

299302

300− ||| Move the focus to the specified hole

303+ ||| Move the focus to the specified hole. Fails if the hole does not

304+ ||| exist.

301305 |||

302306 ||| @ hole the hole to focus on

303307 focus : (hole : TTName) -> Elab ()

@@ -308,7 +312,9 @@ namespace Tactics

308312 unfocus : TTName -> Elab ()

309313 unfocus hole = prim__Unfocus hole

310314

311− ||| Convert a hole to make it suitable for bindings.

315+ ||| Convert a hole to make it suitable for bindings - that is,

316+ ||| transform it such that it has the form `?h : t . h` as opposed to

317+ ||| `?h : t . f h`.

312318 |||

313319 ||| The binding tactics require that a hole be directly under its

314320 ||| binding, or else the scopes of the generated terms won't make

@@ -320,7 +326,8 @@ namespace Tactics

320326 ||| Introduce a new hole with a specified name and type.

321327 |||

322328 ||| The new hole will be focused, and the previously-focused hole

323− ||| will be immediately after it in the hole queue.

329+ ||| will be immediately after it in the hole queue. Because this

330+ ||| tactic introduces a new binding, you may need to `attack` first.

324331 claim : TTName -> Raw -> Elab ()

325332 claim n ty = prim__Claim n ty

326333

@@ -333,12 +340,19 @@ namespace Tactics

333340 intro n = prim__Intro (Just n)

334341

335342 ||| Introduce a lambda binding around the current hole and focus on

336− ||| the body, using the name provided by the type of the hole.

343+ ||| the body, using the name provided by the type of the

344+ ||| hole.

345+ |||

346+ ||| Requires that the hole be immediately under its binder (use

347+ ||| `attack` if it might not be).

337348 intro' : Elab ()

338349 intro' = prim__Intro Nothing

339350

340351 ||| Introduce a dependent function type binding into the current hole,

341352 ||| and focus on the body.

353+ |||

354+ ||| Requires that the hole be immediately under its binder (use

355+ ||| `attack` if it might not be).

342356 forall : TTName -> Raw -> Elab ()

343357 forall n ty = prim__Forall n ty

344358

@@ -347,10 +361,16 @@ namespace Tactics

347361 patvar n = prim__PatVar n

348362

349363 ||| Introduce a new pattern binding.

364+ |||

365+ ||| Requires that the hole be immediately under its binder (use

366+ ||| `attack` if it might not be).

350367 patbind : TTName -> Elab ()

351368 patbind n = prim__PatBind n

352369

353− ||| Introduce a new let binding

370+ ||| Introduce a new let binding.

371+ |||

372+ ||| Requires that the hole be immediately under its binder (use

373+ ||| `attack` if it might not be).

354374 |||

355375 ||| @ n the name to let bind

356376 ||| @ ty the type of the term to be let-bound

@@ -415,6 +435,10 @@ namespace Tactics

415435 ||| constructs a context for `replace` using them. In some cases,

416436 ||| this is not possible, and `replace` must be called manually with

417437 ||| an appropriate context.

438+ |||

439+ ||| Because this tactic internally introduces a `let` binding, it

440+ ||| requires that the hole be immediately under its binder (use

441+ ||| `attack` if it might not be).

418442 rewriteWith : Raw -> Elab ()

419443 rewriteWith rule = prim__Rewrite rule

420444

src/Idris/Core/Binary.hs+3

@@ -188,6 +188,8 @@ instance Binary a => Binary (Err' a) where

188188 put ns

189189 put (RunningElabScript e) = do putWord8 42

190190 put e

191+ put (ElabScriptStaging n) = do putWord8 43

192+ put n

191193

192194 get = do i <- getWord8

193195 case i of

@@ -259,6 +261,7 @@ instance Binary a => Binary (Err' a) where

259261 return $ UnknownImplicit x y

260262 41 -> fmap NoValidAlts get

261263 42 -> fmap RunningElabScript get

264+ 43 -> fmap ElabScriptStaging get

262265 _ -> error "Corrupted binary data for Err'"

263266----- Generated by 'derive'

264267

src/Idris/Core/DeepSeq.hs+1

@@ -154,6 +154,7 @@ instance NFData Err where

154154 rnf (ElabScriptDebug x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

155155 rnf (ElabScriptStuck x1) = rnf x1 `seq` ()

156156 rnf (RunningElabScript x1) = rnf x1 `seq` ()

157+ rnf (ElabScriptStaging x1) = rnf x1 `seq` ()

157158

158159instance NFData ErrorReportPart where

159160 rnf (TextPart x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+1

@@ -293,6 +293,7 @@ data Err' t

293293 -- ^ User-specified message, proof term, goals with context (first goal is focused)

294294 | ElabScriptStuck t

295295 | RunningElabScript (Err' t) -- ^ The error occurred during a top-level elaboration script

296+ | ElabScriptStaging Name

296297 deriving (Eq, Functor, Data, Typeable)

297298

298299type Err = Err' Term

src/Idris/Delaborate.hs+4

@@ -503,6 +503,10 @@ pprintErr' i (ElabScriptStuck tm) =

503503 text "Is it a stuck term?"

504504pprintErr' i (RunningElabScript e) =

505505 text "While running an elaboration script, the following error occurred" <> colon <$> pprintErr' i e

506+pprintErr' i (ElabScriptStaging n) =

507+ text "Can't run elaboration script because it contains pattern matching that has not yet been elaborated." <$>

508+ text "Try lifting the script to a top-level definition." <$>

509+ text "In particular, the problem is caused by:" <+> annName n

506510

507511showPart :: IState -> ErrorReportPart -> Doc OutputAnnotation

508512showPart ist (TextPart str) = fillSep . map text . words $ str

src/Idris/Elab/Term.hs+19−4

@@ -28,6 +28,7 @@ import qualified Util.Pretty as U

2828import Control.Applicative ((<$>))

2929import Control.Monad

3030import Control.Monad.State.Strict

31+import Data.Foldable (for_)

3132import Data.List

3233import qualified Data.Map as M

3334import Data.Maybe (mapMaybe, fromMaybe, catMaybes)

@@ -1237,17 +1238,18 @@ elab ist info emode opts fn tm

12371238 elab' ina fc (PRunElab fc' tm ns) =

12381239 do attack

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

1240− n' <- getNameFrom (sMN 0 "tacticExpr")

12411241 let scriptTy = RApp (Var (sNS (sUN "Elab")

12421242 ["Elab", "Reflection", "Language"]))

12431243 (Var unitTy)

12441244 claim n scriptTy

1245− movelast n

1246− letbind n' scriptTy (Var n)

12471245 focus n

1246+ attack -- to get an extra hole

12481247 elab' ina (Just fc') tm

1248+ script <- get_guess

1249+ fullyElaborated script

1250+ solve -- eliminate the hole. Becuase there are no references, the script is only in the binding

12491251 env <- get_env

1250− runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns

1252+ runElabAction ist (maybe fc' id fc) env script ns

12511253 solve

12521254 elab' ina fc (PConstSugar constFC tm) =

12531255 -- Here we elaborate the contained term, then calculate

@@ -1360,6 +1362,19 @@ elab ist info emode opts fn tm

13601362 getFC d (PAlternative _ _ (x:_)) = getFC d x

13611363 getFC d x = d

13621364

1365+ -- Fail if a term is not yet fully elaborated (e.g. if it contains

1366+ -- case block functions that don't yet exist)

1367+ fullyElaborated :: Term -> ElabD ()

1368+ fullyElaborated (P _ n _) =

1369+ do EState cases _ _ _ <- getAux

1370+ case lookup n cases of

1371+ Nothing -> return ()

1372+ Just _ -> lift . tfail $ ElabScriptStaging n

1373+ fullyElaborated (Bind n b body) = fullyElaborated body >> for_ b fullyElaborated

1374+ fullyElaborated (App _ l r) = fullyElaborated l >> fullyElaborated r

1375+ fullyElaborated (Proj t _) = fullyElaborated t

1376+ fullyElaborated _ = return ()

1377+

13631378 insertLazy :: PTerm -> ElabD PTerm

13641379 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

13651380 insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 121

43+ibcVersion = 122

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

test/meta002/Tacs.idr+7−2

@@ -53,6 +53,7 @@ test1 = %runElab triv

5353test2 : Nat

5454test2 = %runElab triv

5555

56+partial

5657obvious : Elab ()

5758obvious = do g <- goalType

5859 case g of

@@ -120,8 +121,12 @@ namespace STLC

120121 unfocus holeName

121122 return holeName

122123

123− foo : %runElab (elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT))

124− foo = id

124+ -- FIXME: Removing the let-bound Elab script showed a deficiency in

125+ -- how accessible arguments are identified in type signatures. It

126+ -- would be nice if this worked without the extraneous

127+ -- `let`. (perhaps a flag on Pi that says it came from the parser?)

128+ someDef : let x = () in %runElab ((elabTy $ ARR (ARR UNIT UNIT) (ARR UNIT UNIT)))

129+ someDef = id

125130

126131 namespace Untyped

127132 ||| Completely untyped terms

test/meta002/expected+1−1

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

1−Tacs.idr:291:15:

1+Tacs.idr:296:15:

22When checking right hand side of testElab3:

33Unifying ty and ARR ty t would lead to infinite value