8b7f8ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Performance improvement: name supply

Use a name supply instead of checking for uniqueness of names when creating holes. Huge speed improvements on large definitions!

commit8b7f8ada89aa08d7fd1bd5eeda47dd0bbd9bf0a0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 15 Jan 2014, 23:48 (13 years ago) parentf47329c

9 files changed+131−89

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−6 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Elaborate.hs+58−21 src/Idris/Core/TT.hs+3−2 src/Idris/ElabDecls.hs+5−1 src/Idris/ElabTerm.hs+55−56 src/Idris/ParseExpr.hs+1−1 src/Idris/Parser.hs+1−1 test/test037/expected+1−1

src/Idris/AbsSyntax.hs+6−6

@@ -700,13 +700,13 @@ pairOpts = []

700700

701701eqTy = UN "="

702702eqCon = UN "refl"

703−eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

704− (n "x", PRef bi (n "a")), (n "y", PRef bi (n "b"))]

703+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),

704+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

705705 PType)

706− [("", eqCon, PPi impl (n "a") PType (

707− PPi impl (n "x") (PRef bi (n "a"))

708− (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,

709− pimp (n "b") Placeholder False,

706+ [("", eqCon, PPi impl (n "A") PType (

707+ PPi impl (n "x") (PRef bi (n "A"))

708+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

709+ pimp (n "B") Placeholder False,

710710 pexp (PRef bi (n "x")),

711711 pexp (PRef bi (n "x"))])), bi)]

712712 where n a = MN 0 a

src/Idris/AbsSyntaxTree.hs+1

@@ -1388,6 +1388,7 @@ allNamesIn tm = nub $ ni [] tm

13881388 where

13891389 ni env (PRef _ n)

13901390 | not (n `elem` env) = [n]

1391+ ni env (PPatvar _ n) = [n]

13911392 ni env (PApp _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

13921393 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

13931394 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

src/Idris/Core/Elaborate.hs+58−21

@@ -64,6 +64,34 @@ loadState = do (ES p s e) <- get

6464 Just st -> put st

6565 _ -> fail "Nothing to undo"

6666

67+getNameFrom :: Name -> Elab' aux Name

68+getNameFrom n = do (ES (p, a) s e) <- get

69+ let next = nextname p

70+ let p' = p { nextname = next + 1 }

71+ put (ES (p', a) s e)

72+ let n' = case n of

73+ UN x -> MN (next+100) x

74+ MN i x -> if i == 99999

75+ then MN (next+500) x

76+ else MN (next+100) x

77+ NS (UN x) s -> MN (next+100) x

78+ return n'

79+

80+setNextName :: Elab' aux ()

81+setNextName = do env <- get_env

82+ ES (p, a) s e <- get

83+ let pargs = map fst (getArgTys (ptype p))

84+ initNextNameFrom (pargs ++ map fst env)

85+

86+initNextNameFrom :: [Name] -> Elab' aux ()

87+initNextNameFrom ns = do ES (p, a) s e <- get

88+ let n' = maxName (nextname p) ns

89+ put (ES (p { nextname = n' }, a) s e)

90+ where

91+ maxName m ((MN i _) : xs) = maxName (max m i) xs

92+ maxName m (_ : xs) = maxName m xs

93+ maxName m [] = m + 1

94+

6795errAt :: String -> Name -> Elab' aux a -> Elab' aux a

6896errAt thing n elab = do s <- get

6997 case runStateT elab s of

@@ -209,12 +237,20 @@ unique_hole' reusable n

209237 = do ES p _ _ <- get

210238 let bs = bound_in (pterm (fst p)) ++

211239 bound_in (ptype (fst p))

212− n' <- return $ uniqueNameCtxt (context (fst p)) n (holes (fst p)

213− ++ bs ++ dontunify (fst p) ++ usedns (fst p))

240+ let nouse = holes (fst p) ++ bs ++ dontunify (fst p) ++ usedns (fst p)

241+ n' <-

242+-- case lookupTy n (context (fst p)) of

243+-- [] -> if not (n `elem` holes (fst p) ++

244+-- bs ++ dontunify (fst p) ++ usedns (fst p))

245+-- then return n

246+-- else getNameFrom n

247+-- _ -> getNameFrom n

248+ return $ uniqueNameCtxt (context (fst p)) n nouse

214249 ES (p, a) s u <- get

215− -- Hmm: Do we need this level of uniqueness?

216− let p' = p -- if reusable then p else p { usedns = n' : usedns p }

217− put (ES (p', a) s u)

250+ case n' of

251+ MN i _ -> when (i >= nextname p) $

252+ put (ES (p { nextname = i + 1 }, a) s u)

253+ _ -> return ()

218254 return n'

219255 where

220256 bound_in (Bind n b sc) = n : bi b ++ bound_in sc

@@ -312,6 +348,7 @@ equiv tm = processTactic' (Equiv tm)

312348

313349patvar :: Name -> Elab' aux ()

314350patvar n = do env <- get_env

351+ hs <- get_holes

315352 if (n `elem` map fst env) then do apply (Var n) []; solve

316353 else do n' <- case n of

317354 UN _ -> return n

@@ -362,7 +399,7 @@ undo :: Elab' aux ()

362399undo = processTactic' Undo

363400

364401prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]

365−prepare_apply fn imps =

402+prepare_apply fn imps =

366403 do ty <- get_type fn

367404 ctxt <- get_context

368405 env <- get_env

@@ -381,10 +418,10 @@ prepare_apply fn imps =

381418 where

382419 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

383420 do let t = rebind hs t_in

384− n <- unique_hole (mkMN n')

421+ n <- getNameFrom (mkMN n')

385422-- when (null claims) (start_unify n)

386423 let sc' = instantiate (P Bound n t) sc

387−-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show hs) $

424+-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

388425 claim n (forget t)

389426 when i (movelast n)

390427 mkClaims sc' is (n : claims) hs

@@ -400,9 +437,9 @@ prepare_apply fn imps =

400437 doClaim ((i, _), n, t) = do claim n t

401438 when i (movelast n)

402439

403− mkMN n@(MN _ _) = n

404− mkMN n@(UN x) = MN 1000 x

405− mkMN n@(SN s) = MN 1000 (show s)

440+ mkMN n@(MN i _) = n

441+ mkMN n@(UN x) = MN 99999 x

442+ mkMN n@(SN s) = MN 99999 (show s)

406443 mkMN (NS n xs) = NS (mkMN n) xs

407444

408445 rebind hs (Bind n t sc)

@@ -428,7 +465,7 @@ apply' fillt fn imps =

428465 ptm <- get_term

429466 hs <- get_holes

430467 ES (p, a) s prev <- get

431− let dont = nub $ head hs : dontunify p ++

468+ let dont = head hs : dontunify p ++

432469 if null imps then [] -- do all we can

433470 else

434471 map fst (filter (not.snd) (zip args (map fst imps)))

@@ -447,7 +484,7 @@ apply' fillt fn imps =

447484 end_unify

448485 ptm <- get_term

449486 return (map (updateUnify unify) args)

450− where updateUnify hs n = case lookup n hs of

487+ where updateUnify us n = case lookup n us of

451488 Just (P _ t _) -> t

452489 _ -> n

453490

@@ -512,7 +549,7 @@ apply_elab n args =

512549 focus n; elaboration; elabClaims failed r xs

513550

514551 mkMN n@(MN _ _) = n

515− mkMN n@(UN x) = MN 1000 x

552+ mkMN n@(UN x) = MN 0 x

516553 mkMN (NS n ns) = NS (mkMN n) ns

517554

518555-- If the goal is not a Pi-type, invent some names and make it a pi type

@@ -521,9 +558,9 @@ checkPiGoal n

521558 = do g <- goal

522559 case g of

523560 Bind _ (Pi _) _ -> return ()

524− _ -> do a <- unique_hole (MN 0 "pargTy")

525− b <- unique_hole (MN 0 "pretTy")

526− f <- unique_hole (MN 0 "pf")

561+ _ -> do a <- getNameFrom (MN 0 "pargTy")

562+ b <- getNameFrom (MN 0 "pretTy")

563+ f <- getNameFrom (MN 0 "pf")

527564 claim a RType

528565 claim b RType

529566 claim f (RBind n (Pi (Var a)) (Var b))

@@ -535,10 +572,10 @@ checkPiGoal n

535572

536573simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

537574simple_app fun arg appstr =

538− do a <- unique_hole (MN 0 "argTy")

539− b <- unique_hole (MN 0 "retTy")

540− f <- unique_hole (MN 0 "f")

541− s <- unique_hole (MN 0 "s")

575+ do a <- getNameFrom (MN 0 "argTy")

576+ b <- getNameFrom (MN 0 "retTy")

577+ f <- getNameFrom (MN 0 "f")

578+ s <- getNameFrom (MN 0 "s")

542579 claim a RType

543580 claim b RType

544581 claim f (RBind (MN 0 "aX") (Pi (Var a)) (Var b))

src/Idris/Core/TT.hs+3−2

@@ -246,6 +246,7 @@ data Name = UN String -- ^ User-provided name

246246 | NErased -- ^ Name of somethng which is never used in scope

247247 | SN SpecialName -- ^ Decorated function names

248248 deriving (Eq, Ord)

249+

249250{-!

250251deriving instance Binary Name

251252deriving instance NFData Name

@@ -653,8 +654,8 @@ data Datatype n = Data { d_typename :: n,

653654instance Eq n => Eq (TT n) where

654655 (==) (P xt x _) (P yt y _) = x == y

655656 (==) (V x) (V y) = x == y

656− (==) (Bind _ xb xs) (Bind _ yb ys) = xb == yb && xs == ys

657− (==) (App fx ax) (App fy ay) = fx == fy && ax == ay

657+ (==) (Bind _ xb xs) (Bind _ yb ys) = xs == ys && xb == yb

658+ (==) (App fx ax) (App fy ay) = ax == ay && fx == fy

658659 (==) (TType _) (TType _) = True -- deal with constraints later

659660 (==) (Constant x) (Constant y) = x == y

660661 (==) (Proj x i) (Proj y j) = x == y && i == j

src/Idris/ElabDecls.hs+5−1

@@ -671,6 +671,7 @@ elabTransform info fc safe lhs_in rhs_in

671671 ((rhs', defer), _) <-

672672 tclift $ elaborate ctxt (MN 0 "transRHS") clhs_ty []

673673 (do pbinds lhs_tm

674+ setNextName

674675 erun fc (build i info False [] (UN "transform") rhs)

675676 erun fc $ psolve lhs_tm

676677 tt <- get_term

@@ -1298,8 +1299,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

12981299 ((rhs', defer, is), _) <-

12991300 tclift $ elaborate ctxt (MN 0 "patRHS") clhsty []

13001301 (do pbinds lhs_tm

1302+ setNextName

13011303 (_, _, is) <- errAt "right hand side of " fname

1302− (erun fc (build i info False opts fname rhs))

1304+ (erun fc (build i info False opts fname rhs))

13031305 errAt "right hand side of " fname

13041306 (erun fc $ psolve lhs_tm)

13051307 hs <- get_holes

@@ -1448,6 +1450,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

14481450 tclift $ elaborate ctxt (MN 0 "withRHS")

14491451 (bindTyArgs PVTy bargs infP) []

14501452 (do pbinds lhs_tm

1453+ setNextName

14511454 -- TODO: may want where here - see winfo abpve

14521455 (_', d, is) <- errAt "with value in " fname

14531456 (erun fc (build i info False opts fname (infTerm wval)))

@@ -1511,6 +1514,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

15111514 ((rhs', defer, is), _) <-

15121515 tclift $ elaborate ctxt (MN 0 "wpatRHS") clhsty []

15131516 (do pbinds lhs_tm

1517+ setNextName

15141518 (_, d, is) <- erun fc (build i info False opts fname rhs)

15151519 psolve lhs_tm

15161520 tt <- get_term

src/Idris/ElabTerm.hs+55−56

@@ -81,7 +81,10 @@ build ist info pattern opts fn tm

8181buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm ->

8282 ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

8383buildTC ist info pattern opts fn tm

84− = do elab ist info pattern opts fn tm

84+ = do -- set name supply to begin after highest index in tm

85+ let ns = allNamesIn tm

86+ initNextNameFrom ns

87+ elab ist info pattern opts fn tm

8588 probs <- get_probs

8689 tm <- get_term

8790 case probs of

@@ -171,18 +174,18 @@ elab ist info pattern opts fn tm

171174 elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

172175 = do g <- goal; resolveTC 5 g fn ist

173176 elab' ina (PResolveTC fc)

174− | True = do c <- unique_hole (MN 0 "class")

177+ | True = do c <- getNameFrom (MN 0 "class")

175178 instanceArg c

176179 | otherwise = do g <- goal

177180 try (resolveTC 2 g fn ist)

178− (do c <- unique_hole (MN 0 "class")

181+ (do c <- getNameFrom (MN 0 "class")

179182 instanceArg c)

180183 elab' ina (PRefl fc t)

181− = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder True,

184+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "A") Placeholder True,

182185 pimp (MN 0 "x") t False])

183186 elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

184− [pimp (MN 0 "a") Placeholder True,

185− pimp (MN 0 "b") Placeholder False,

187+ [pimp (MN 0 "A") Placeholder True,

188+ pimp (MN 0 "B") Placeholder False,

186189 pexp l, pexp r])

187190 elab' ina@(_, a, inty) (PPair fc l r)

188191 = do hnf_compute

@@ -272,7 +275,7 @@ elab ist info pattern opts fn tm

272275 elab' ina@(_, a, inty) (PLam n ty sc)

273276 = do hsin <- get_holes

274277 ptmin <- get_term

275− tyn <- unique_hole (MN 0 "lamty")

278+ tyn <- getNameFrom (MN 0 "lamty")

276279 checkPiGoal n

277280 claim tyn RType

278281 explicit tyn

@@ -290,7 +293,7 @@ elab ist info pattern opts fn tm

290293 elab' ina@(_, a, _) (PPi _ n Placeholder sc)

291294 = do attack; arg n (MN 0 "ty"); elabE (True, a, True) sc; solve

292295 elab' ina@(_, a, _) (PPi _ n ty sc)

293− = do attack; tyn <- unique_hole (MN 0 "ty")

296+ = do attack; tyn <- getNameFrom (MN 0 "ty")

294297 claim tyn RType

295298 n' <- case n of

296299 MN _ _ -> unique_hole n

@@ -302,9 +305,9 @@ elab ist info pattern opts fn tm

302305 solve

303306 elab' ina@(_, a, inty) (PLet n ty val sc)

304307 = do attack;

305− tyn <- unique_hole (MN 0 "letty")

308+ tyn <- getNameFrom (MN 0 "letty")

306309 claim tyn RType

307− valn <- unique_hole (MN 0 "letval")

310+ valn <- getNameFrom (MN 0 "letval")

308311 claim valn (Var tyn)

309312 explicit valn

310313 letbind n (Var tyn) (Var valn)

@@ -325,9 +328,9 @@ elab ist info pattern opts fn tm

325328 elab' ina@(_, a, inty) (PGoal fc r n sc) = do

326329 rty <- goal

327330 attack

328− tyn <- unique_hole (MN 0 "letty")

331+ tyn <- getNameFrom (MN 0 "letty")

329332 claim tyn RType

330− valn <- unique_hole (MN 0 "letval")

333+ valn <- getNameFrom (MN 0 "letval")

331334 claim valn (Var tyn)

332335 letbind n (Var tyn) (Var valn)

333336 focus valn

@@ -346,7 +349,7 @@ elab ist info pattern opts fn tm

346349 -- new function name

347350 env <- get_env

348351 argTys <- claimArgTys env args

349− fn <- unique_hole (MN 0 "inf_fn")

352+ fn <- getNameFrom (MN 0 "inf_fn")

350353 let fty = fnTy argTys rty

351354-- trace (show (ptm, map fst argTys)) $ focus fn

352355 -- build and defer the function application

@@ -360,8 +363,8 @@ elab ist info pattern opts fn tm

360363 ans <- claimArgTys env xs

361364 return ((n, (False, forget nty)) : ans)

362365 claimArgTys env (_ : xs)

363− = do an <- unique_hole (MN 0 "inf_argTy")

364− aval <- unique_hole (MN 0 "inf_arg")

366+ = do an <- getNameFrom (MN 0 "inf_argTy")

367+ aval <- getNameFrom (MN 0 "inf_arg")

365368 claim an RType

366369 claim aval (Var an)

367370 ans <- claimArgTys env xs

@@ -394,16 +397,12 @@ elab ist info pattern opts fn tm

394397 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

395398 = lift $ tfail (Msg "Typecase is not allowed")

396399 -- if f is local, just do a simple_app

397− elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args')

398− = do let args = {- case lookupCtxt f (inblock info) of

399− Just ps -> (map (pexp . (PRef fc)) ps ++ args')

400− _ -> -} args'

401−-- newtm <- mkSpecialised ist fc f (map getTm args') tm

402− env <- get_env

403− if (f `elem` map fst env && length args' == 1)

400+ elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

401+ = do env <- get_env

402+ if (f `elem` map fst env && length args == 1)

404403 then -- simple app, as below

405404 do simple_app (elabE (ina, g, inty) (PRef fc f))

406− (elabE (True, g, inty) (getTm (head args')))

405+ (elabE (True, g, inty) (getTm (head args)))

407406 (show tm)

408407 solve

409408 else

@@ -416,7 +415,7 @@ elab ist info pattern opts fn tm

416415 -- we can unify with them

417416 case lookupCtxt f (idris_classes ist) of

418417 [] -> return ()

419− _ -> mapM_ setInjective (map getTm args')

418+ _ -> mapM_ setInjective (map getTm args)

420419 ctxt <- get_context

421420 let guarded = isConName f ctxt

422421 ns <- apply (Var f) (map isph args)

@@ -429,7 +428,7 @@ elab ist info pattern opts fn tm

429428 (zip ns args)

430429 elabArgs (ina || not isinf, guarded, inty)

431430 [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

432− mkSpecialised ist fc f (map getTm args') tm

431+ mkSpecialised ist fc f (map getTm args) tm

433432 solve

434433 ptm <- get_term

435434 ivs' <- get_instances

@@ -478,11 +477,11 @@ elab ist info pattern opts fn tm

478477 elab' ina (PElabError e) = fail (pshow ist e)

479478 elab' ina (PRewrite fc r sc newg)

480479 = do attack

481− tyn <- unique_hole (MN 0 "rty")

480+ tyn <- getNameFrom (MN 0 "rty")

482481 claim tyn RType

483− valn <- unique_hole (MN 0 "rval")

482+ valn <- getNameFrom (MN 0 "rval")

484483 claim valn (Var tyn)

485− letn <- unique_hole (MN 0 "rewrite_rule")

484+ letn <- getNameFrom (MN 0 "rewrite_rule")

486485 letbind letn (Var tyn) (Var valn)

487486 focus valn

488487 elab' ina r

@@ -497,11 +496,11 @@ elab ist info pattern opts fn tm

497496 solve

498497 where doEquiv t sc =

499498 do attack

500− tyn <- unique_hole (MN 0 "ety")

499+ tyn <- getNameFrom (MN 0 "ety")

501500 claim tyn RType

502− valn <- unique_hole (MN 0 "eqval")

501+ valn <- getNameFrom (MN 0 "eqval")

503502 claim valn (Var tyn)

504− letn <- unique_hole (MN 0 "equiv_val")

503+ letn <- getNameFrom (MN 0 "equiv_val")

505504 letbind letn (Var tyn) (Var valn)

506505 focus tyn

507506 elab' ina t

@@ -511,10 +510,10 @@ elab ist info pattern opts fn tm

511510 solve

512511 elab' ina@(_, a, inty) c@(PCase fc scr opts)

513512 = do attack

514− tyn <- unique_hole (MN 0 "scty")

513+ tyn <- getNameFrom (MN 0 "scty")

515514 claim tyn RType

516− valn <- unique_hole (MN 0 "scval")

517− scvn <- unique_hole (MN 0 "scvar")

515+ valn <- getNameFrom (MN 0 "scval")

516+ scvn <- getNameFrom (MN 0 "scvar")

518517 claim valn (Var tyn)

519518 letbind scvn (Var tyn) (Var valn)

520519 focus valn

@@ -872,11 +871,11 @@ runTac autoSolve ist tac

872871 when autoSolve solveAll

873872 runT (Equiv tm) -- let bind tm, then

874873 = do attack

875− tyn <- unique_hole (MN 0 "ety")

874+ tyn <- getNameFrom (MN 0 "ety")

876875 claim tyn RType

877− valn <- unique_hole (MN 0 "eqval")

876+ valn <- getNameFrom (MN 0 "eqval")

878877 claim valn (Var tyn)

879− letn <- unique_hole (MN 0 "equiv_val")

878+ letn <- getNameFrom (MN 0 "equiv_val")

880879 letbind letn (Var tyn) (Var valn)

881880 focus tyn

882881 elab ist toplevel False [] (MN 0 "tac") tm

@@ -884,12 +883,12 @@ runTac autoSolve ist tac

884883 when autoSolve solveAll

885884 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

886885 = do attack; -- (h:_) <- get_holes

887− tyn <- unique_hole (MN 0 "rty")

886+ tyn <- getNameFrom (MN 0 "rty")

888887 -- start_unify h

889888 claim tyn RType

890− valn <- unique_hole (MN 0 "rval")

889+ valn <- getNameFrom (MN 0 "rval")

891890 claim valn (Var tyn)

892− letn <- unique_hole (MN 0 "rewrite_rule")

891+ letn <- getNameFrom (MN 0 "rewrite_rule")

893892 letbind letn (Var tyn) (Var valn)

894893 focus valn

895894 elab ist toplevel False [] (MN 0 "tac") tm

@@ -900,9 +899,9 @@ runTac autoSolve ist tac

900899 when autoSolve solveAll

901900 runT (LetTac n tm)

902901 = do attack

903− tyn <- unique_hole (MN 0 "letty")

902+ tyn <- getNameFrom (MN 0 "letty")

904903 claim tyn RType

905− valn <- unique_hole (MN 0 "letval")

904+ valn <- getNameFrom (MN 0 "letval")

906905 claim valn (Var tyn)

907906 letn <- unique_hole n

908907 letbind letn (Var tyn) (Var valn)

@@ -911,9 +910,9 @@ runTac autoSolve ist tac

911910 when autoSolve solveAll

912911 runT (LetTacTy n ty tm)

913912 = do attack

914− tyn <- unique_hole (MN 0 "letty")

913+ tyn <- getNameFrom (MN 0 "letty")

915914 claim tyn RType

916− valn <- unique_hole (MN 0 "letval")

915+ valn <- getNameFrom (MN 0 "letval")

917916 claim valn (Var tyn)

918917 letn <- unique_hole n

919918 letbind letn (Var tyn) (Var valn)

@@ -933,16 +932,16 @@ runTac autoSolve ist tac

933932 runT (ApplyTactic tm) = do tenv <- get_env -- store the environment

934933 tgoal <- goal -- store the goal

935934 attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...

936− script <- unique_hole (MN 0 "script")

935+ script <- getNameFrom (MN 0 "script")

937936 claim script scriptTy

938− scriptvar <- unique_hole (MN 0 "scriptvar" )

937+ scriptvar <- getNameFrom (MN 0 "scriptvar" )

939938 letbind scriptvar scriptTy (Var script)

940939 focus script

941940 elab ist toplevel False [] (MN 0 "tac") tm

942941 (script', _) <- get_type_val (Var scriptvar)

943942 -- now that we have the script apply

944943 -- it to the reflected goal and context

945− restac <- unique_hole (MN 0 "restac")

944+ restac <- getNameFrom (MN 0 "restac")

946945 claim restac tacticTy

947946 focus restac

948947 fill (raw_apply (forget script')

@@ -965,9 +964,9 @@ runTac autoSolve ist tac

965964 -- goal, then apply the resulting reflected Tactic

966965 = do tgoal <- goal

967966 attack

968− script <- unique_hole (MN 0 "script")

967+ script <- getNameFrom (MN 0 "script")

969968 claim script scriptTy

970− scriptvar <- unique_hole (MN 0 "scriptvar" )

969+ scriptvar <- getNameFrom (MN 0 "scriptvar" )

971970 letbind scriptvar scriptTy (Var script)

972971 focus script

973972 ptm <- get_term

@@ -976,7 +975,7 @@ runTac autoSolve ist tac

976975 (script', _) <- get_type_val (Var scriptvar)

977976 -- now that we have the script apply

978977 -- it to the reflected goal

979− restac <- unique_hole (MN 0 "restac")

978+ restac <- getNameFrom (MN 0 "restac")

980979 claim restac tacticTy

981980 focus restac

982981 fill (forget script')

@@ -992,11 +991,11 @@ runTac autoSolve ist tac

992991 scriptTy = tacticTy

993992

994993 runT (Reflect v) = do attack -- let x = reflect v in ...

995− tyn <- unique_hole (MN 0 "letty")

994+ tyn <- getNameFrom (MN 0 "letty")

996995 claim tyn RType

997− valn <- unique_hole (MN 0 "letval")

996+ valn <- getNameFrom (MN 0 "letval")

998997 claim valn (Var tyn)

999− letn <- unique_hole (MN 0 "letvar")

998+ letn <- getNameFrom (MN 0 "letvar")

1000999 letbind letn (Var tyn) (Var valn)

10011000 focus valn

10021001 elab ist toplevel False [] (MN 0 "tac") v

@@ -1006,11 +1005,11 @@ runTac autoSolve ist tac

10061005 let value' = hnf ctxt env value

10071006 runTac autoSolve ist (Exact $ PQuote (reflect value'))

10081007 runT (Fill v) = do attack -- let x = fill x in ...

1009− tyn <- unique_hole (MN 0 "letty")

1008+ tyn <- getNameFrom (MN 0 "letty")

10101009 claim tyn RType

1011− valn <- unique_hole (MN 0 "letval")

1010+ valn <- getNameFrom (MN 0 "letval")

10121011 claim valn (Var tyn)

1013− letn <- unique_hole (MN 0 "letvar")

1012+ letn <- getNameFrom (MN 0 "letvar")

10141013 letbind letn (Var tyn) (Var valn)

10151014 focus valn

10161015 elab ist toplevel False [] (MN 0 "tac") v

src/Idris/ParseExpr.hs+1−1

@@ -645,7 +645,7 @@ TypeExpr ::= ConstraintList? Expr;

645645typeExpr :: SyntaxInfo -> IdrisParser PTerm

646646typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

647647 sc <- expr syn

648− return (bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc)

648+ return (bindList (PPi constraint) (map (\x -> (MN 0 "constrarg", x)) cs) sc)

649649 <?> "type signature"

650650

651651{- | Parses a lambda expression

src/Idris/Parser.hs+1−1

@@ -515,7 +515,7 @@ instance_ syn = do reserved "instance"; fc <- getFC

515515 cn <- name

516516 args <- many (simpleExpr syn)

517517 let sc = PApp fc (PRef fc cn) (map pexp args)

518− let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc

518+ let t = bindList (PPi constraint) (map (\x -> (MN 0 "constraint", x)) cs) sc

519519 ds <- option [] (instanceBlock syn)

520520 return [PInstance syn fc cs cn args t en ds]

521521 <?> "instance declaration"

test/test037/expected+1−1

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

11In file ErrorReflection.idr line 78 column 5

22 When elaborating right hand side of Main.bad :

3− DSL type error: (t'(1000) => t'(1000)) doesn't match ()

3+ DSL type error: (t'(504) => t'(504)) doesn't match ()

55Original error: