a458e29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Take care when calling allNamesIn

If we've expanded alternatives, the term could be very big, and we'll get the same results if we call before expanding alternatives. If we do need to know all the names a user has written in a term, call before expanding the alternatives. This addresses part of the slowness identified in #2657

commita458e29d0941f81d093779aee15e874739444914 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Oct 2015, 17:09 (11 years ago) parent83f0af1

3 files changed+29−19

compare with master

unifiedsplit

src/Idris/Elab/Clause.hs+20−12 src/Idris/Elab/Term.hs+8−6 src/Idris/Elab/Transform.hs+1−1

src/Idris/Elab/Clause.hs+20−12

@@ -477,7 +477,9 @@ checkPossible info fc tcgen fname lhs_in

477477 let lhs = addImplPat i lhs_in

478478 -- if the LHS type checks, it is possible

479479 case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

480− (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

480+ (erun fc (buildTC i info ELHS [] fname

481+ (allNamesIn lhs_in)

482+ (infTerm lhs))) of

481483 OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->

482484 do setContext ctxt'

483485 processTacticDecls info newDecls

@@ -492,19 +494,19 @@ checkPossible info fc tcgen fname lhs_in

492494 recoverableCoverage ctxt err)

493495

494496

495−propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

496−propagateParams i ps t tm@(PApp _ (PRef fc hls n) args)

497+propagateParams :: IState -> [Name] -> Type -> [Name] -> PTerm -> PTerm

498+propagateParams i ps t bound tm@(PApp _ (PRef fc hls n) args)

497499 = PApp fc (PRef fc hls n) (addP t args)

498500 where addP (Bind n _ sc) (t : ts)

499501 | Placeholder <- getTm t,

500502 n `elem` ps,

501− not (n `elem` allNamesIn tm)

503+ not (n `elem` bound)

502504 = t { getTm = PRef NoFC [] n } : addP sc ts

503505 addP (Bind n _ sc) (t : ts) = t : addP sc ts

504506 addP _ ts = ts

505−propagateParams i ps t tm@(PApp fc ap args)

506− = PApp fc (propagateParams i ps t ap) args

507−propagateParams i ps t (PRef fc hls n)

507+propagateParams i ps t bound (PApp fc ap args)

508+ = PApp fc (propagateParams i ps t bound ap) args

509+propagateParams i ps t bound (PRef fc hls n)

508510 = case lookupCtxt n (idris_implicits i) of

509511 [is] -> let ps' = filter (isImplicit is) ps in

510512 PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')

@@ -512,7 +514,7 @@ propagateParams i ps t (PRef fc hls n)

512514 where isImplicit [] n = False

513515 isImplicit (PImp _ _ _ x _ : is) n | x == n = True

514516 isImplicit (_ : is) n = isImplicit is n

515−propagateParams i ps t x = x

517+propagateParams i ps t bound x = x

516518

517519findUnique :: Context -> Env -> Term -> [Name]

518520findUnique ctxt env (Bind n b sc)

@@ -561,7 +563,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

561563 let tcparams = getTCParamsInType i [] fn_is norm_ty

562564

563565 let lhs = mkLHSapp $ stripLinear i $ stripUnmatchable i $

564− propagateParams i params norm_ty (addImplPat i lhs_in)

566+ propagateParams i params norm_ty (allNamesIn lhs_in) (addImplPat i lhs_in)

565567-- let lhs = mkLHSapp $

566568-- propagateParams i params fn_ty (addImplPat i lhs_in)

567569 logLvl 10 (show (params, fn_ty) ++ " " ++ showTmImpls (addImplPat i lhs_in))

@@ -572,7 +574,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

572574 ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-

573575 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

574576 (do res <- errAt "left hand side of " fname Nothing

575− (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

577+ (erun fc (buildTC i info ELHS opts fname

578+ (allNamesIn lhs_in)

579+ (infTerm lhs)))

576580 probs <- get_probs

577581 inj <- get_inj

578582 return (res, probs, inj))

@@ -813,12 +817,16 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

813817 [t] -> t

814818 _ -> []

815819 let params = getParamsInType i [] fn_is (normalise ctxt [] fn_ty)

816− let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

820+ let lhs = stripLinear i $ stripUnmatchable i $

821+ propagateParams i params fn_ty (allNamesIn lhs_in)

822+ (addImplPat i lhs_in)

817823 logLvl 2 ("LHS: " ++ show lhs)

818824 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

819825 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

820826 (errAt "left hand side of with in " fname Nothing

821− (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

827+ (erun fc (buildTC i info ELHS opts fname

828+ (allNamesIn lhs_in)

829+ (infTerm lhs))) )

822830 setContext ctxt'

823831 processTacticDecls info newDecls

824832 sendHighlighting highlights

src/Idris/Elab/Term.hs+8−6

@@ -138,15 +138,16 @@ build ist info emode opts fn tm

138138-- (Separate, so we don't go overboard resolving things that we don't

139139-- know about yet on the LHS of a pattern def)

140140

141−buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

141+buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name ->

142+ [Name] -> -- Cached names in the PTerm, before adding PAlternatives

143+ PTerm ->

142144 ElabD ElabResult

143−buildTC ist info emode opts fn tm

144− = do -- set name supply to begin after highest index in tm

145− let ns = allNamesIn tm

146− let tmIn = tm

145+buildTC ist info emode opts fn ns tm

146+ = do let tmIn = tm

147147 let inf = case lookupCtxt fn (idris_tyinfodata ist) of

148148 [TIPartial] -> True

149149 _ -> False

150+ -- set name supply to begin after highest index in tm

150151 initNextNameFrom ns

151152 elab ist info emode opts fn tm

152153 probs <- get_probs

@@ -2540,7 +2541,8 @@ processTacticDecls info steps =

25402541 let fc = fileFC "elab_reflected_totality"

25412542 let tcgen = False -- TODO: later we may support dictionary generation

25422543 case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState

2543− (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of

2544+ (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)

2545+ (infTerm lhs))) of

25442546 OK (ElabResult lhs' _ _ _ _ _, _) ->

25452547 do -- not recursively calling here, because we don't

25462548 -- want to run infinitely many times

src/Idris/Elab/Transform.hs+1−1

@@ -57,7 +57,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

5757 (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

5858 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

5959 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

60− (infTerm lhs)))

60+ (allNamesIn lhs_in) (infTerm lhs)))

6161 setContext ctxt'

6262 processTacticDecls info newDecls

6363 sendHighlighting highlights