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

git.iko.soy/Idris-dev

on master help sign in

Performance improvement: name supply

8b7f8adEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+6−6

compare with master

unifiedsplit

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

700

701eqTy = UN "="

702eqCon = UN "refl"

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

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

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

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

705 PType)

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

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

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

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

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

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

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

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

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

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

712 where n a = MN 0 a

src/Idris/AbsSyntaxTree.hs+1

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

1388 where

1389 ni env (PRef _ n)

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

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

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

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

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

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

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

1394 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

64 Just st -> put st

65 _ -> fail "Nothing to undo"

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+

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

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

68errAt thing n elab = do s <- get

96errAt thing n elab = do s <- get

69 case runStateT elab s of

97 case runStateT elab s of

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

209 = do ES p _ _ <- get

237 = do ES p _ _ <- get

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

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

211 bound_in (ptype (fst p))

239 bound_in (ptype (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

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

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

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

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

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

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

250+ case n' of

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

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

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

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

253+ _ -> return ()

218 return n'

254 return n'

219 where

255 where

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

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

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

312

348

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

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

314patvar n = do env <- get_env

350patvar n = do env <- get_env

351+ hs <- get_holes

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

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

316 else do n' <- case n of

353 else do n' <- case n of

317 UN _ -> return n

354 UN _ -> return n

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

362undo = processTactic' Undo

399undo = processTactic' Undo

363

400

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

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

365−prepare_apply fn imps =

402+prepare_apply fn imps =

366 do ty <- get_type fn

403 do ty <- get_type fn

367 ctxt <- get_context

404 ctxt <- get_context

368 env <- get_env

405 env <- get_env

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

381 where

418 where

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

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

383 do let t = rebind hs t_in

420 do let t = rebind hs t_in

384− n <- unique_hole (mkMN n')

421+ n <- getNameFrom (mkMN n')

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

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

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

423 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)) $

388 claim n (forget t)

425 claim n (forget t)

389 when i (movelast n)

426 when i (movelast n)

390 mkClaims sc' is (n : claims) hs

427 mkClaims sc' is (n : claims) hs

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

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

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

401 when i (movelast n)

438 when i (movelast n)

402

439

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

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

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

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

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

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

406 mkMN (NS n xs) = NS (mkMN n) xs

443 mkMN (NS n xs) = NS (mkMN n) xs

407

444

408 rebind hs (Bind n t sc)

445 rebind hs (Bind n t sc)

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

428 ptm <- get_term

465 ptm <- get_term

429 hs <- get_holes

466 hs <- get_holes

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

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

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

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

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

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

433 else

470 else

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

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

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

447 end_unify

484 end_unify

448 ptm <- get_term

485 ptm <- get_term

449 return (map (updateUnify unify) args)

486 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

451 Just (P _ t _) -> t

488 Just (P _ t _) -> t

452 _ -> n

489 _ -> n

453

490

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

512 focus n; elaboration; elabClaims failed r xs

549 focus n; elaboration; elabClaims failed r xs

513

550

514 mkMN n@(MN _ _) = n

551 mkMN n@(MN _ _) = n

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

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

516 mkMN (NS n ns) = NS (mkMN n) ns

553 mkMN (NS n ns) = NS (mkMN n) ns

517

554

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

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

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

521 = do g <- goal

558 = do g <- goal

522 case g of

559 case g of

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

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

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

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

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

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

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

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

527 claim a RType

564 claim a RType

528 claim b RType

565 claim b RType

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

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

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

535

572

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

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

537simple_app fun arg appstr =

574simple_app fun arg appstr =

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

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

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

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

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

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

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

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

542 claim a RType

579 claim a RType

543 claim b RType

580 claim b RType

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

581 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

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

247 | SN SpecialName -- ^ Decorated function names

248 deriving (Eq, Ord)

249+

249{-!

250{-!

250deriving instance Binary Name

251deriving instance Binary Name

251deriving instance NFData Name

252deriving instance NFData Name

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

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

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

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

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

655 (==) (V x) (V y) = x == y

656 (==) (V x) (V y) = x == y

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

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

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

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

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

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

659 (==) (Constant x) (Constant y) = x == y

660 (==) (Constant x) (Constant y) = x == y

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

661 (==) (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

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

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

673 (do pbinds lhs_tm

674+ setNextName

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

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

675 erun fc $ psolve lhs_tm

676 erun fc $ psolve lhs_tm

676 tt <- get_term

677 tt <- get_term

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

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

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

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

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

1300 (do pbinds lhs_tm

1301 (do pbinds lhs_tm

1302+ setNextName

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

1303 (_, _, 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))

1303 errAt "right hand side of " fname

1305 errAt "right hand side of " fname

1304 (erun fc $ psolve lhs_tm)

1306 (erun fc $ psolve lhs_tm)

1305 hs <- get_holes

1307 hs <- get_holes

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

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

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

1449 (bindTyArgs PVTy bargs infP) []

1451 (bindTyArgs PVTy bargs infP) []

1450 (do pbinds lhs_tm

1452 (do pbinds lhs_tm

1453+ setNextName

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

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

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

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

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

1456 (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)

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

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

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

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

1513 (do pbinds lhs_tm

1516 (do pbinds lhs_tm

1517+ setNextName

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

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

1515 psolve lhs_tm

1519 psolve lhs_tm

1516 tt <- get_term

1520 tt <- get_term

src/Idris/ElabTerm.hs+55−56

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

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

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

83buildTC 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

84− = do elab ist info pattern opts fn tm

87+ elab ist info pattern opts fn tm

85 probs <- get_probs

88 probs <- get_probs

86 tm <- get_term

89 tm <- get_term

87 case probs of

90 case probs of

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

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

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

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

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

173 elab' ina (PResolveTC fc)

176 elab' ina (PResolveTC fc)

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

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

175 instanceArg c

178 instanceArg c

176 | otherwise = do g <- goal

179 | otherwise = do g <- goal

177 try (resolveTC 2 g fn ist)

180 try (resolveTC 2 g fn ist)

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

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

179 instanceArg c)

182 instanceArg c)

180 elab' ina (PRefl fc t)

183 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,

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

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

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

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

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

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

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

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

186 pexp l, pexp r])

189 pexp l, pexp r])

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

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

188 = do hnf_compute

191 = do hnf_compute

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

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

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

273 = do hsin <- get_holes

276 = do hsin <- get_holes

274 ptmin <- get_term

277 ptmin <- get_term

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

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

276 checkPiGoal n

279 checkPiGoal n

277 claim tyn RType

280 claim tyn RType

278 explicit tyn

281 explicit tyn

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

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

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

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

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

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

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

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

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

294 claim tyn RType

297 claim tyn RType

295 n' <- case n of

298 n' <- case n of

296 MN _ _ -> unique_hole n

299 MN _ _ -> unique_hole n

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

302 solve

305 solve

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

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

304 = do attack;

307 = do attack;

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

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

306 claim tyn RType

309 claim tyn RType

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

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

308 claim valn (Var tyn)

311 claim valn (Var tyn)

309 explicit valn

312 explicit valn

310 letbind n (Var tyn) (Var valn)

313 letbind n (Var tyn) (Var valn)

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

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

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

326 rty <- goal

329 rty <- goal

327 attack

330 attack

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

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

329 claim tyn RType

332 claim tyn RType

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

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

331 claim valn (Var tyn)

334 claim valn (Var tyn)

332 letbind n (Var tyn) (Var valn)

335 letbind n (Var tyn) (Var valn)

333 focus valn

336 focus valn

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

346 -- new function name

349 -- new function name

347 env <- get_env

350 env <- get_env

348 argTys <- claimArgTys env args

351 argTys <- claimArgTys env args

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

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

350 let fty = fnTy argTys rty

353 let fty = fnTy argTys rty

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

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

352 -- build and defer the function application

355 -- build and defer the function application

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

360 ans <- claimArgTys env xs

363 ans <- claimArgTys env xs

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

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

362 claimArgTys env (_ : xs)

365 claimArgTys env (_ : xs)

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

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

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

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

365 claim an RType

368 claim an RType

366 claim aval (Var an)

369 claim aval (Var an)

367 ans <- claimArgTys env xs

370 ans <- claimArgTys env xs

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

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

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

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

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

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

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

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

400+ 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

401+ = do env <- get_env

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

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

404 then -- simple app, as below

403 then -- simple app, as below

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

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

407 (show tm)

406 (show tm)

408 solve

407 solve

409 else

408 else

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

416 -- we can unify with them

415 -- we can unify with them

417 case lookupCtxt f (idris_classes ist) of

416 case lookupCtxt f (idris_classes ist) of

418 [] -> return ()

417 [] -> return ()

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

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

420 ctxt <- get_context

419 ctxt <- get_context

421 let guarded = isConName f ctxt

420 let guarded = isConName f ctxt

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

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

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

429 (zip ns args)

428 (zip ns args)

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

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

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

430 [] 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

433 solve

432 solve

434 ptm <- get_term

433 ptm <- get_term

435 ivs' <- get_instances

434 ivs' <- get_instances

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

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

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

479 elab' ina (PRewrite fc r sc newg)

478 elab' ina (PRewrite fc r sc newg)

480 = do attack

479 = do attack

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

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

482 claim tyn RType

481 claim tyn RType

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

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

484 claim valn (Var tyn)

483 claim valn (Var tyn)

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

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

486 letbind letn (Var tyn) (Var valn)

485 letbind letn (Var tyn) (Var valn)

487 focus valn

486 focus valn

488 elab' ina r

487 elab' ina r

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

497 solve

496 solve

498 where doEquiv t sc =

497 where doEquiv t sc =

499 do attack

498 do attack

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

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

501 claim tyn RType

500 claim tyn RType

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

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

503 claim valn (Var tyn)

502 claim valn (Var tyn)

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

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

505 letbind letn (Var tyn) (Var valn)

504 letbind letn (Var tyn) (Var valn)

506 focus tyn

505 focus tyn

507 elab' ina t

506 elab' ina t

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

511 solve

510 solve

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

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

513 = do attack

512 = do attack

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

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

515 claim tyn RType

514 claim tyn RType

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

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

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

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

518 claim valn (Var tyn)

517 claim valn (Var tyn)

519 letbind scvn (Var tyn) (Var valn)

518 letbind scvn (Var tyn) (Var valn)

520 focus valn

519 focus valn

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

872 when autoSolve solveAll

871 when autoSolve solveAll

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

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

874 = do attack

873 = do attack

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

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

876 claim tyn RType

875 claim tyn RType

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

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

878 claim valn (Var tyn)

877 claim valn (Var tyn)

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

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

880 letbind letn (Var tyn) (Var valn)

879 letbind letn (Var tyn) (Var valn)

881 focus tyn

880 focus tyn

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

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

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

884 when autoSolve solveAll

883 when autoSolve solveAll

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

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

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

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

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

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

888 -- start_unify h

887 -- start_unify h

889 claim tyn RType

888 claim tyn RType

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

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

891 claim valn (Var tyn)

890 claim valn (Var tyn)

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

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

893 letbind letn (Var tyn) (Var valn)

892 letbind letn (Var tyn) (Var valn)

894 focus valn

893 focus valn

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

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

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

900 when autoSolve solveAll

899 when autoSolve solveAll

901 runT (LetTac n tm)

900 runT (LetTac n tm)

902 = do attack

901 = do attack

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

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

904 claim tyn RType

903 claim tyn RType

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

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

906 claim valn (Var tyn)

905 claim valn (Var tyn)

907 letn <- unique_hole n

906 letn <- unique_hole n

908 letbind letn (Var tyn) (Var valn)

907 letbind letn (Var tyn) (Var valn)

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

911 when autoSolve solveAll

910 when autoSolve solveAll

912 runT (LetTacTy n ty tm)

911 runT (LetTacTy n ty tm)

913 = do attack

912 = do attack

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

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

915 claim tyn RType

914 claim tyn RType

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

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

917 claim valn (Var tyn)

916 claim valn (Var tyn)

918 letn <- unique_hole n

917 letn <- unique_hole n

919 letbind letn (Var tyn) (Var valn)

918 letbind letn (Var tyn) (Var valn)

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

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

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

934 tgoal <- goal -- store the goal

933 tgoal <- goal -- store the goal

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

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

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

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

937 claim script scriptTy

936 claim script scriptTy

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

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

939 letbind scriptvar scriptTy (Var script)

938 letbind scriptvar scriptTy (Var script)

940 focus script

939 focus script

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

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

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

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

943 -- now that we have the script apply

942 -- now that we have the script apply

944 -- it to the reflected goal and context

943 -- it to the reflected goal and context

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

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

946 claim restac tacticTy

945 claim restac tacticTy

947 focus restac

946 focus restac

948 fill (raw_apply (forget script')

947 fill (raw_apply (forget script')

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

965 -- goal, then apply the resulting reflected Tactic

964 -- goal, then apply the resulting reflected Tactic

966 = do tgoal <- goal

965 = do tgoal <- goal

967 attack

966 attack

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

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

969 claim script scriptTy

968 claim script scriptTy

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

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

971 letbind scriptvar scriptTy (Var script)

970 letbind scriptvar scriptTy (Var script)

972 focus script

971 focus script

973 ptm <- get_term

972 ptm <- get_term

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

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

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

977 -- now that we have the script apply

976 -- now that we have the script apply

978 -- it to the reflected goal

977 -- it to the reflected goal

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

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

980 claim restac tacticTy

979 claim restac tacticTy

981 focus restac

980 focus restac

982 fill (forget script')

981 fill (forget script')

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

992 scriptTy = tacticTy

991 scriptTy = tacticTy

993

992

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

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

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

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

996 claim tyn RType

995 claim tyn RType

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

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

998 claim valn (Var tyn)

997 claim valn (Var tyn)

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

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

1000 letbind letn (Var tyn) (Var valn)

999 letbind letn (Var tyn) (Var valn)

1001 focus valn

1000 focus valn

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

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

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

1006 let value' = hnf ctxt env value

1005 let value' = hnf ctxt env value

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

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

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

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

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

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

1010 claim tyn RType

1009 claim tyn RType

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

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

1012 claim valn (Var tyn)

1011 claim valn (Var tyn)

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

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

1014 letbind letn (Var tyn) (Var valn)

1013 letbind letn (Var tyn) (Var valn)

1015 focus valn

1014 focus valn

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

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

src/Idris/ParseExpr.hs+1−1

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

645typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

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

649 <?> "type signature"

650

651{- | Parses a lambda expression

src/Idris/Parser.hs+1−1

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

515 cn <- name

516 args <- many (simpleExpr syn)

517 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

519 ds <- option [] (instanceBlock syn)

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

521 <?> "instance declaration"

test/test037/expected+1−1

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

1In file ErrorReflection.idr line 78 column 5

2 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 ()

5Original error: