a458e29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Take care when calling allNamesIn

a458e29Edwin Brady11 years ago

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

compare with master

unifiedsplit

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

477 let lhs = addImplPat i lhs_in

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

479 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

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

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

482 do setContext ctxt'

484 do setContext ctxt'

483 processTacticDecls info newDecls

485 processTacticDecls info newDecls

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

492 recoverableCoverage ctxt err)

494 recoverableCoverage ctxt err)

493

495

494

496

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

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

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

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

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

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

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

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

499 | Placeholder <- getTm t,

501 | Placeholder <- getTm t,

500 n `elem` ps,

502 n `elem` ps,

501− not (n `elem` allNamesIn tm)

503+ not (n `elem` bound)

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

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

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

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

504 addP _ ts = ts

506 addP _ ts = ts

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

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

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

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

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

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

508 = case lookupCtxt n (idris_implicits i) of

510 = case lookupCtxt n (idris_implicits i) of

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

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

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

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

512 where isImplicit [] n = False

514 where isImplicit [] n = False

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

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

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

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

515−propagateParams i ps t x = x

517+propagateParams i ps t bound x = x

516

518

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

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

518findUnique ctxt env (Bind n b sc)

520findUnique 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

561 let tcparams = getTCParamsInType i [] fn_is norm_ty

563 let tcparams = getTCParamsInType i [] fn_is norm_ty

562

564

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

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

565-- let lhs = mkLHSapp $

567-- let lhs = mkLHSapp $

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

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

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

569 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

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

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

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

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

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

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

576 probs <- get_probs

580 probs <- get_probs

577 inj <- get_inj

581 inj <- get_inj

578 return (res, probs, inj))

582 return (res, probs, inj))

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

813 [t] -> t

817 [t] -> t

814 _ -> []

818 _ -> []

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

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

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

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

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

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

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

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

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

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

822 setContext ctxt'

830 setContext ctxt'

823 processTacticDecls info newDecls

831 processTacticDecls info newDecls

824 sendHighlighting highlights

832 sendHighlighting highlights

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

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

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

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

140

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

142 ElabD ElabResult

144 ElabD ElabResult

143−buildTC ist info emode opts fn tm

145+buildTC ist info emode opts fn ns tm

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

145− let ns = allNamesIn tm

146− let tmIn = tm

146+ = do let tmIn = tm

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

148 [TIPartial] -> True

149 _ -> False

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

150 initNextNameFrom ns

151 initNextNameFrom ns

151 elab ist info emode opts fn tm

152 elab ist info emode opts fn tm

152 probs <- get_probs

153 probs <- get_probs

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

2540 let fc = fileFC "elab_reflected_totality"

2541 let fc = fileFC "elab_reflected_totality"

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

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

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

2543 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

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

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

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

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

2546 -- want to run infinitely many times

2548 -- 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

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

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

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

60− (infTerm lhs)))

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

61 setContext ctxt'

62 processTacticDecls info newDecls

63 sendHighlighting highlights