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

git.iko.soy/Idris-dev

on master help sign in

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

32269f8David Christiansen11 years ago

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

compare with master

unifiedsplit

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

183 fail : List ErrorReportPart -> Elab a

184 fail err = prim__Fail err

185

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.

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

188 getEnv = prim__Env

189

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.

191 getGoal : Elab (TTName, TT)

192 getGoal = prim__Goal

193

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

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

195 getHoles : Elab (List TTName)

196 getHoles = prim__Holes

197

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

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

199 getGuess : Elab (Maybe TT)

200 getGuess = prim__Guess

201

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

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

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

204 lookupTy n = prim__LookupTy n

205

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.

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

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

208 lookupTyExact n = case !(lookupTy n) of

209 lookupTyExact n = case !(lookupTy n) of

209 [res] => return res

210 [res] => return res

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

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

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

212

213

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

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

214− ||| are overloadings of some name

215+ ||| are overloadings of some name.

215 lookupDatatype : TTName -> Elab (List Datatype)

216 lookupDatatype : TTName -> Elab (List Datatype)

216 lookupDatatype n = prim__LookupDatatype n

217 lookupDatatype n = prim__LookupDatatype n

217

218

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

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

220 lookupDatatypeExact : TTName -> Elab Datatype

222 lookupDatatypeExact : TTName -> Elab Datatype

221 lookupDatatypeExact n = case !(lookupDatatype n) of

223 lookupDatatypeExact n = case !(lookupDatatype n) of

222 [res] => return res

224 [res] => return res

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

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

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

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

225

227

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.

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

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

228 check tm = prim__Check tm

230 check tm = prim__Check tm

229

231

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

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

231− ||| equivalent

233+ ||| equivalent.

232 forgetTypes : TT -> Elab Raw

234 forgetTypes : TT -> Elab Raw

233 forgetTypes tt = prim__Forget tt

235 forgetTypes tt = prim__Forget tt

234

236

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

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

236 goalType : Elab Raw

238 goalType : Elab Raw

237 goalType = do g <- getGoal

239 goalType = do g <- getGoal

238 forgetTypes (snd g)

240 forgetTypes (snd g)

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

249 solve : Elab ()

251 solve : Elab ()

250 solve = prim__Solve

252 solve = prim__Solve

251

253

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.

253 fill : Raw -> Elab ()

256 fill : Raw -> Elab ()

254 fill tm = prim__Fill tm

257 fill tm = prim__Fill tm

255

258

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

297 Elab (List (TTName, TTName))

300 Elab (List (TTName, TTName))

298 matchApply tm argSpec = prim__Apply tm argSpec

301 matchApply tm argSpec = prim__Apply tm argSpec

299

302

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

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

304+ ||| exist.

301 |||

305 |||

302 ||| @ hole the hole to focus on

306 ||| @ hole the hole to focus on

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

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

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

308 unfocus : TTName -> Elab ()

312 unfocus : TTName -> Elab ()

309 unfocus hole = prim__Unfocus hole

313 unfocus hole = prim__Unfocus hole

310

314

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

312 |||

318 |||

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

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

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

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

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

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

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

321 |||

327 |||

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

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

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

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

325 claim n ty = prim__Claim n ty

332 claim n ty = prim__Claim n ty

326

333

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

333 intro n = prim__Intro (Just n)

340 intro n = prim__Intro (Just n)

334

341

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

342 ||| 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).

337 intro' : Elab ()

348 intro' : Elab ()

338 intro' = prim__Intro Nothing

349 intro' = prim__Intro Nothing

339

350

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

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

341 ||| and focus on the body.

352 ||| and focus on the body.

353+ |||

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

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

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

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

343 forall n ty = prim__Forall n ty

357 forall n ty = prim__Forall n ty

344

358

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

347 patvar n = prim__PatVar n

361 patvar n = prim__PatVar n

348

362

349 ||| Introduce a new pattern binding.

363 ||| Introduce a new pattern binding.

364+ |||

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

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

350 patbind : TTName -> Elab ()

367 patbind : TTName -> Elab ()

351 patbind n = prim__PatBind n

368 patbind n = prim__PatBind n

352

369

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

354 |||

374 |||

355 ||| @ n the name to let bind

375 ||| @ n the name to let bind

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

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

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

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

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

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

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

417 ||| an appropriate context.

437 ||| 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).

418 rewriteWith : Raw -> Elab ()

442 rewriteWith : Raw -> Elab ()

419 rewriteWith rule = prim__Rewrite rule

443 rewriteWith rule = prim__Rewrite rule

420

444

src/Idris/Core/Binary.hs+3

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

188 put ns

189 put (RunningElabScript e) = do putWord8 42

190 put e

191+ put (ElabScriptStaging n) = do putWord8 43

192+ put n

191

193

192 get = do i <- getWord8

194 get = do i <- getWord8

193 case i of

195 case i of

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

259 return $ UnknownImplicit x y

261 return $ UnknownImplicit x y

260 41 -> fmap NoValidAlts get

262 41 -> fmap NoValidAlts get

261 42 -> fmap RunningElabScript get

263 42 -> fmap RunningElabScript get

264+ 43 -> fmap ElabScriptStaging get

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

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

263----- Generated by 'derive'

266----- Generated by 'derive'

264

267

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

157

158

158instance NFData ErrorReportPart where

159instance NFData ErrorReportPart where

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

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

src/Idris/Core/TT.hs+1

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

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

294 | ElabScriptStuck t

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

296+ | ElabScriptStaging Name

296 deriving (Eq, Functor, Data, Typeable)

297 deriving (Eq, Functor, Data, Typeable)

297

298

298type Err = Err' Term

299type Err = Err' Term

src/Idris/Delaborate.hs+4

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

503 text "Is it a stuck term?"

504pprintErr' i (RunningElabScript e) =

505 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

506

510

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

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

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

512showPart 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

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

29import Control.Monad

30import Control.Monad.State.Strict

31+import Data.Foldable (for_)

31import Data.List

32import Data.List

32import qualified Data.Map as M

33import qualified Data.Map as M

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

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

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

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

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

1238 do attack

1239 do attack

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

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

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

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

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

1243 (Var unitTy)

1244 claim n scriptTy

1245− movelast n

1246− letbind n' scriptTy (Var n)

1247 focus n

1245 focus n

1246+ attack -- to get an extra hole

1248 elab' ina (Just fc') tm

1247 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

1249 env <- get_env

1251 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

1251 solve

1253 solve

1252 elab' ina fc (PConstSugar constFC tm) =

1254 elab' ina fc (PConstSugar constFC tm) =

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

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

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

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

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

1361 getFC d x = d

1363 getFC d x = d

1362

1364

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+

1363 insertLazy :: PTerm -> ElabD PTerm

1378 insertLazy :: PTerm -> ElabD PTerm

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

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

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

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

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 121

43+ibcVersion = 122

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

test/meta002/Tacs.idr+7−2

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

53test2 : Nat

54test2 = %runElab triv

56+partial

56obvious : Elab ()

57obvious : Elab ()

57obvious = do g <- goalType

58obvious = do g <- goalType

58 case g of

59 case g of

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

120 unfocus holeName

121 unfocus holeName

121 return holeName

122 return holeName

122

123

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

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

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

124− foo = id

129+ someDef = id

125

130

126 namespace Untyped

131 namespace Untyped

127 ||| Completely untyped terms

132 ||| Completely untyped terms

test/meta002/expected+1−1

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

1−Tacs.idr:291:15:

1+Tacs.idr:296:15:

2When checking right hand side of testElab3:

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