0419a12 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+13−13

@@ -962,11 +962,11 @@ expandParams dec ps ns infs tm = en tm

962962 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

963963 PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))

964964 | otherwise = PPi (enTacImp p) n nfc (en t) (en s)

965− en (PLet fc n ty v s)

965+ en (PLet fc n nfc ty v s)

966966 | n `elem` (map fst ps ++ ns)

967967 = let n' = mkShadow n in

968− PLet fc n' (en ty) (en v) (en (shadow n n' s))

969− | otherwise = PLet fc n (en ty) (en v) (en s)

968+ PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))

969+ | otherwise = PLet fc n nfc (en ty) (en v) (en s)

970970 -- FIXME: Should only do this in a type signature!

971971 en (PDPair f p (PRef f' n) t r)

972972 | n `elem` (map fst ps ++ ns) && t /= Placeholder

@@ -1591,12 +1591,12 @@ addImpl' inpat env infns imp_meths ist ptm

15911591 _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty

15921592 (PCase fc (PRef fc (sMN 0 "lamp") )

15931593 [(PRef fc n, sc)]))

1594− ai qq env ds (PLet fc n ty val sc)

1594+ ai qq env ds (PLet fc n nfc ty val sc)

15951595 = case lookupDef n (tt_ctxt ist) of

15961596 [] -> let ty' = ai qq env ds ty

15971597 val' = ai qq env ds val

15981598 sc' = ai qq ((n, Just ty):env) ds sc in

1599− PLet fc n ty' val' sc'

1599+ PLet fc n nfc ty' val' sc'

16001600 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

16011601 ai qq env ds (PPi p n nfc ty sc)

16021602 = let ty' = ai qq env ds ty

@@ -1965,10 +1965,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

19651965 match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'

19661966 ms <- match' s s'

19671967 return (mt ++ ms)

1968− match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'

1969− mty <- match' ty ty'

1970− ms <- match' s s'

1971− return (mt ++ mty ++ ms)

1968+ match (PLet _ _ _ t ty s) (PLet _ _ _ t' ty' s') = do mt <- match' t t'

1969+ mty <- match' ty ty'

1970+ ms <- match' s s'

1971+ return (mt ++ mty ++ ms)

19721972 match (PHidden x) (PHidden y)

19731973 | RightOK xs <- match x y = return xs -- to collect variables

19741974 | otherwise = return [] -- Otherwise hidden things are unmatchable

@@ -2044,8 +2044,8 @@ shadow n n' t = sm t where

20442044 | otherwise = PLam fc x xfc (sm t) sc

20452045 sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)

20462046 | otherwise = PPi p x fc (sm t) sc

2047− sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)

2048− | otherwise = PLet fc x (sm t) (sm v) sc

2047+ sm (PLet fc x xfc t v sc) | n /= x = PLet fc x xfc (sm t) (sm v) (sm sc)

2048+ | otherwise = PLet fc x xfc (sm t) (sm v) sc

20492049 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

20502050 sm (PAppBind f x as) = PAppBind f (sm x) (map (fmap sm) as)

20512051 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

@@ -2109,7 +2109,7 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

21092109 ty' <- mkUniq ty

21102110 sc'' <- mkUniq sc'

21112111 return $! PPi p n' fc ty' sc''

2112− mkUniq (PLet fc n ty val sc)

2112+ mkUniq (PLet fc n nfc ty val sc)

21132113 = do env <- get

21142114 (n', sc') <-

21152115 if n `S.member` env

@@ -2120,7 +2120,7 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

21202120 put (S.insert n' env)

21212121 ty' <- mkUniq ty; val' <- mkUniq val

21222122 sc'' <- mkUniq sc'

2123− return $! PLet fc n' ty' val' sc''

2123+ return $! PLet fc n' nfc ty' val' sc''

21242124 mkUniq (PApp fc t args)

21252125 = do t' <- mkUniq t

21262126 args' <- mapM mkUniqA args

src/Idris/AbsSyntaxTree.hs+10−10

@@ -817,8 +817,8 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

817817 | PInferRef FC Name -- ^ A name to be defined later

818818 | PPatvar FC Name -- ^ A pattern variable

819819 | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.

820− | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the variable

821− | PLet FC Name PTerm PTerm PTerm -- ^ A let binding

820+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable

821+ | PLet FC Name FC PTerm PTerm PTerm -- ^ A let binding (second FC is precise name location)

822822 | PTyped PTerm PTerm -- ^ Term with explicit type

823823 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

824824 | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

@@ -869,7 +869,7 @@ mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

869869mapPT f t = f (mpt t) where

870870 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)

871871 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)

872− mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)

872+ mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

873873 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

874874 (fmap (mapPT f) g)

875875 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

@@ -959,7 +959,7 @@ type PTactic = PTactic' PTerm

959959data PDo' t = DoExp FC t

960960 | DoBind FC Name FC t -- ^ second FC is precise name location

961961 | DoBindP FC t t [(t,t)]

962− | DoLet FC Name t t

962+ | DoLet FC Name FC t t -- ^ second FC is precise name location

963963 | DoLetP FC t t

964964 deriving (Eq, Functor, Data, Typeable)

965965{-!

@@ -971,7 +971,7 @@ instance Sized a => Sized (PDo' a) where

971971 size (DoExp fc t) = 1 + size fc + size t

972972 size (DoBind fc nm nfc t) = 1 + size fc + size nm + size nfc + size t

973973 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

974− size (DoLet fc nm l r) = 1 + size fc + size nm + size l + size r

974+ size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r

975975 size (DoLetP fc l r) = 1 + size fc + size l + size r

976976

977977type PDo = PDo' PTerm

@@ -1028,7 +1028,7 @@ highestFC (PInferRef fc _) = Just fc

10281028highestFC (PPatvar fc _) = Just fc

10291029highestFC (PLam fc _ _ _ _) = Just fc

10301030highestFC (PPi _ _ _ _ _) = Nothing

1031−highestFC (PLet fc _ _ _ _) = Just fc

1031+highestFC (PLet fc _ _ _ _ _) = Just fc

10321032highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty

10331033highestFC (PApp fc _ _) = Just fc

10341034highestFC (PAppBind fc _ _) = Just fc

@@ -1061,7 +1061,7 @@ highestFC (PDoBlock lines) =

10611061 getDoFC (DoExp fc t) = fc

10621062 getDoFC (DoBind fc nm nfc t) = fc

10631063 getDoFC (DoBindP fc l r alts) = fc

1064− getDoFC (DoLet fc nm l r) = fc

1064+ getDoFC (DoLet fc nm nfc l r) = fc

10651065 getDoFC (DoLetP fc l r) = fc

10661066

10671067highestFC (PIdiom fc _) = Just fc

@@ -1455,7 +1455,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

14551455 bracket p startPrec . group . align . hang 2 $

14561456 text "\\" <> prettyBindingOf n False <+> text "=>" <$>

14571457 prettySe startPrec ((n, False):bnd) sc

1458− prettySe p bnd (PLet fc n ty v sc) =

1458+ prettySe p bnd (PLet fc n nfc ty v sc) =

14591459 bracket p startPrec . group . align $

14601460 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

14611461 kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

@@ -1874,7 +1874,7 @@ instance Sized PTerm where

18741874 size (PRef fc name) = size name

18751875 size (PLam fc name _ ty bdy) = 1 + size ty + size bdy

18761876 size (PPi plicity name fc ty bdy) = 1 + size ty + size fc + size bdy

1877− size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy

1877+ size (PLet fc name nfc ty def bdy) = 1 + size ty + size def + size bdy

18781878 size (PTyped trm ty) = 1 + size trm + size ty

18791879 size (PApp fc name args) = 1 + size args

18801880 size (PAppBind fc name args) = 1 + size args

@@ -1949,7 +1949,7 @@ boundNamesIn tm = S.toList (ni S.empty tm)

19491949 ni set (PCase _ c os) = niTms (ni set c) (map snd os)

19501950 ni set (PIfThenElse _ c t f) = niTms set [c, t, f]

19511951 ni set (PLam fc n _ ty sc) = S.insert n $ ni (ni set ty) sc

1952− ni set (PLet fc n ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

1952+ ni set (PLet fc n nfc ty val sc) = S.insert n $ ni (ni (ni set ty) val) sc

19531953 ni set (PPi p n _ ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

19541954 ni set (PEq _ _ _ l r) = ni (ni set l) r

19551955 ni set (PRewrite _ l r _) = ni (ni set l) r

src/Idris/DSL.hs+9−9

@@ -51,13 +51,13 @@ expandSugar dsl (PLam fc n nfc ty tm)

5151 , pexp (var dsl n tm 0)]

5252 in expandSugar dsl sc

5353expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)

54−expandSugar dsl (PLet fc n ty v tm)

54+expandSugar dsl (PLet fc n nfc ty v tm)

5555 | Just letb <- dsl_let dsl

5656 = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)

5757 , pexp v

5858 , pexp (var dsl n tm 0)]

5959 in expandSugar dsl sc

60−expandSugar dsl (PLet fc n ty v tm) = PLet fc n (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)

60+expandSugar dsl (PLet fc n nfc ty v tm) = PLet fc n nfc (expandSugar dsl ty) (expandSugar dsl v) (expandSugar dsl tm)

6161expandSugar dsl (PPi p n fc ty tm)

6262 | Just pi <- dsl_pi dsl

6363 = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)

@@ -103,8 +103,8 @@ expandSugar dsl (PDoBlock ds)

103103 = PApp fc b [pexp tm, pexp (PLam fc (sMN 0 "bpat") NoFC Placeholder

104104 (PCase fc (PRef fc (sMN 0 "bpat"))

105105 ((p, block b rest) : alts)))]

106− block b (DoLet fc n ty tm : rest)

107− = PLet fc n ty tm (block b rest)

106+ block b (DoLet fc n nfc ty tm : rest)

107+ = PLet fc n nfc ty tm (block b rest)

108108 block b (DoLetP fc p tm : rest)

109109 = PCase fc tm [(p, block b rest)]

110110 block b (DoExp fc tm : rest)

@@ -128,10 +128,10 @@ var dsl n t i = v' i t where

128128 | Nothing <- dsl_lambda dsl

129129 = PLam fc n nfc ty (v' i sc)

130130 | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)

131− v' i (PLet fc n ty val sc)

131+ v' i (PLet fc n nfc ty val sc)

132132 | Nothing <- dsl_let dsl

133− = PLet fc n (v' i ty) (v' i val) (v' i sc)

134− | otherwise = PLet fc n (v' i ty) (v' i val) (v' (i + 1) sc)

133+ = PLet fc n nfc (v' i ty) (v' i val) (v' i sc)

134+ | otherwise = PLet fc n nfc (v' i ty) (v' i val) (v' (i + 1) sc)

135135 v' i (PPi p n fc ty sc)

136136 | Nothing <- dsl_pi dsl

137137 = PPi p n fc (v' i ty) (v' i sc)

@@ -191,8 +191,8 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

191191 args' <- mapM dbArg args

192192 return (PApp fc t' args')

193193 db' (PLam fc n nfc ty sc) = return (PLam fc n nfc ty (debind b sc))

194− db' (PLet fc n ty v sc) = do v' <- db' v

195− return (PLet fc n ty v' (debind b sc))

194+ db' (PLet fc n nfc ty v sc) = do v' <- db' v

195+ return (PLet fc n nfc ty v' (debind b sc))

196196 db' (PCase fc s opts) = do s' <- db' s

197197 return (PCase fc s' (map (pmap (debind b)) opts))

198198 db' (PPair fc p l r) = do l' <- db' l

src/Idris/DeepSeq.hs+4−4

@@ -221,8 +221,8 @@ instance NFData PTerm where

221221 rnf (PLam _ x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

222222 rnf (PPi x1 x2 x3 x4 x5)

223223 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

224− rnf (PLet _ x1 x2 x3 x4)

225− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

224+ rnf (PLet _ x1 x2 x3 x4 x5)

225+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

226226 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

227227 rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

228228 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

@@ -318,8 +318,8 @@ instance (NFData t) => NFData (PDo' t) where

318318 rnf (DoExp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

319319 rnf (DoBind x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

320320 rnf (DoBindP x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

321− rnf (DoLet x1 x2 x3 x4)

322− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

321+ rnf (DoLet x1 x2 x3 x4 x5)

322+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

323323 rnf (DoLetP x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

324324

325325instance (NFData t) => NFData (PArg' t) where

src/Idris/Delaborate.hs+1−1

@@ -86,7 +86,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

8686 , (P _ cOp _, args) <- unApply sc

8787 , Just caseblock <- delabCase env imps n val cOp args = caseblock

8888 | otherwise =

89− PLet un n (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

89+ PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

9090 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

9191 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

9292 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

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

@@ -17,7 +17,7 @@ desugarAs lhs rhs

1717 bindPats :: [(Name, FC, PTerm)] -> PTerm -> PTerm

1818 bindPats [] rhs = rhs

1919 bindPats ((n, fc, tm) : ps) rhs

20− = PLet fc n Placeholder tm (bindPats ps rhs)

20+ = PLet fc n NoFC Placeholder tm (bindPats ps rhs)

2121

2222collectAs :: PTerm -> State [(Name, FC, PTerm)] PTerm

2323collectAs (PAs fc n tm) = do tm' <- collectAs tm

src/Idris/Elab/Term.hs+2−1

@@ -570,7 +570,7 @@ elab ist info emode opts fn tm

570570 elabE ec' fc sc

571571 solve

572572 highlightSource nfc (AnnBoundName n False)

573− elab' ina _ (PLet fc n ty val sc)

573+ elab' ina _ (PLet fc n nfc ty val sc)

574574 = do attack

575575 ivs <- get_instances

576576 tyn <- getNameFrom (sMN 0 "letty")

@@ -606,6 +606,7 @@ elab ist info emode opts fn tm

606606 Just (Let t v) -> v

607607 other -> error ("Value not a let binding: " ++ show other))

608608 solve

609+ highlightSource nfc (AnnBoundName n False)

609610 elab' ina _ (PGoal fc r n sc) = do

610611 rty <- goal

611612 attack

src/Idris/ElabQuasiquote.hs+4−4

@@ -63,10 +63,10 @@ extractDoUnquotes d (DoBind fc n nfc tm)

6363 return (DoBind fc n nfc tm', ex)

6464extractDoUnquotes d (DoBindP fc t t' alts)

6565 = fail "Pattern-matching binds cannot be quasiquoted"

66−extractDoUnquotes d (DoLet fc n v b)

66+extractDoUnquotes d (DoLet fc n nfc v b)

6767 = do (v', ex1) <- extractUnquotes d v

6868 (b', ex2) <- extractUnquotes d b

69− return (DoLet fc n v' b', ex1 ++ ex2)

69+ return (DoLet fc n nfc v' b', ex1 ++ ex2)

7070extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"

7171

7272

@@ -79,11 +79,11 @@ extractUnquotes n (PPi plicity name fc ty body)

7979 = do (ty', ex1) <- extractUnquotes n ty

8080 (body', ex2) <- extractUnquotes n body

8181 return (PPi plicity name fc ty' body', ex1 ++ ex2)

82−extractUnquotes n (PLet fc name ty val body)

82+extractUnquotes n (PLet fc name nfc ty val body)

8383 = do (ty', ex1) <- extractUnquotes n ty

8484 (val', ex2) <- extractUnquotes n val

8585 (body', ex3) <- extractUnquotes n body

86− return (PLet fc name ty' val' body', ex1 ++ ex2 ++ ex3)

86+ return (PLet fc name nfc ty' val' body', ex1 ++ ex2 ++ ex3)

8787extractUnquotes n (PTyped tm ty)

8888 = do (tm', ex1) <- extractUnquotes n tm

8989 (ty', ex2) <- extractUnquotes n ty

src/Idris/Error.hs+2−2

@@ -93,7 +93,7 @@ warnDisamb ist (PInferRef _ _) = return ()

9393warnDisamb ist (PPatvar _ _) = return ()

9494warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

9595warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

96−warnDisamb ist (PLet _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b

96+warnDisamb ist (PLet _ _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b

9797warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t

9898warnDisamb ist (PApp _ t args) = warnDisamb ist t >>

9999 mapM_ (warnDisamb ist . getTm) args

@@ -124,7 +124,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

124124 wStep (DoBind _ _ _ x) = warnDisamb ist x

125125 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

126126 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

127− wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y

127+ wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

128128 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

129129warnDisamb ist (PIdiom _ x) = warnDisamb ist x

130130warnDisamb ist (PReturn _) = return ()

src/Idris/IBC.hs+17−13

@@ -1528,12 +1528,13 @@ instance Binary PTerm where

15281528 put x3

15291529 put x4

15301530 put x5

1531− PLet x1 x2 x3 x4 x5 -> do putWord8 6

1532− put x1

1533− put x2

1534− put x3

1535− put x4

1536− put x5

1531+ PLet x1 x2 x3 x4 x5 x6 -> do putWord8 6

1532+ put x1

1533+ put x2

1534+ put x3

1535+ put x4

1536+ put x5

1537+ put x6

15371538 PTyped x1 x2 -> do putWord8 7

15381539 put x1

15391540 put x2

@@ -1677,7 +1678,8 @@ instance Binary PTerm where

16771678 x3 <- get

16781679 x4 <- get

16791680 x5 <- get

1680− return (PLet x1 x2 x3 x4 x5)

1681+ x6 <- get

1682+ return (PLet x1 x2 x3 x4 x5 x6)

16811683 7 -> do x1 <- get

16821684 x2 <- get

16831685 return (PTyped x1 x2)

@@ -1969,11 +1971,12 @@ instance (Binary t) => Binary (PDo' t) where

19691971 put x2

19701972 put x3

19711973 put x4

1972− DoLet x1 x2 x3 x4 -> do putWord8 3

1973− put x1

1974− put x2

1975− put x3

1976− put x4

1974+ DoLet x1 x2 x3 x4 x5 -> do putWord8 3

1975+ put x1

1976+ put x2

1977+ put x3

1978+ put x4

1979+ put x5

19771980 DoLetP x1 x2 x3 -> do putWord8 4

19781981 put x1

19791982 put x2

@@ -1998,7 +2001,8 @@ instance (Binary t) => Binary (PDo' t) where

19982001 x2 <- get

19992002 x3 <- get

20002003 x4 <- get

2001− return (DoLet x1 x2 x3 x4)

2004+ x5 <- get

2005+ return (DoLet x1 x2 x3 x4 x5)

20022006 4 -> do x1 <- get

20032007 x2 <- get

20042008 x3 <- get

src/Idris/IdrisDoc.hs+8−8

@@ -293,7 +293,7 @@ extractPTermNames (PInferRef _ n) = [n]

293293extractPTermNames (PPatvar _ n) = [n]

294294extractPTermNames (PLam _ n _ p1 p2) = n : concatMap extract [p1, p2]

295295extractPTermNames (PPi _ n _ p1 p2) = n : concatMap extract [p1, p2]

296−extractPTermNames (PLet _ n p1 p2 p3) = n : concatMap extract [p1, p2, p3]

296+extractPTermNames (PLet _ n _ p1 p2 p3) = n : concatMap extract [p1, p2, p3]

297297extractPTermNames (PTyped p1 p2) = concatMap extract [p1, p2]

298298extractPTermNames (PApp _ p pas) = let names = concatMap extractPArg pas

299299 in (extract p) ++ names

@@ -340,13 +340,13 @@ extractPArg (PTacImplicit {pname=n, getScript=p1, getTm=p2})

340340

341341-- | Helper function for extractPTermNames

342342extractPDo :: PDo -> [Name]

343−extractPDo (DoExp _ p) = extract p

344−extractPDo (DoBind _ n _ p) = n : extract p

345−extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

346− ps' = ps1 ++ ps2

347− in concatMap extract (p1 : p2 : ps')

348−extractPDo (DoLet _ n p1 p2) = n : concatMap extract [p1, p2]

349−extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

343+extractPDo (DoExp _ p) = extract p

344+extractPDo (DoBind _ n _ p) = n : extract p

345+extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

346+ ps' = ps1 ++ ps2

347+ in concatMap extract (p1 : p2 : ps')

348+extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]

349+extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

350350

351351-- | Helper function for extractPTermNames

352352extractPTactic :: PTactic -> [Name]

src/Idris/Interactive.hs+1−1

@@ -198,7 +198,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

198198 else iPrintResult newmv

199199 where dropCtxt 0 sc = sc

200200 dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc

201− dropCtxt i (PLet _ _ _ _ sc) = dropCtxt (i - 1) sc

201+ dropCtxt i (PLet _ _ _ _ _ sc) = dropCtxt (i - 1) sc

202202 dropCtxt i (PLam _ _ _ _ sc) = dropCtxt (i - 1) sc

203203 dropCtxt _ t = t

204204

src/Idris/ParseExpr.hs+11−11

@@ -169,8 +169,8 @@ extension syn ns rules =

169169 update ns (PPi p n fc ty sc)

170170 = PPi (updTacImp ns p) (updateB ns n) fc

171171 (update ns ty) (update (dropn n ns) sc)

172− update ns (PLet fc n ty val sc)

173− = PLet fc (updateB ns n) (update ns ty)

172+ update ns (PLet fc n nfc ty val sc)

173+ = PLet fc (updateB ns n) nfc (update ns ty)

174174 (update ns val) (update (dropn n ns) sc)

175175 update ns (PApp fc t args)

176176 = PApp fc (update ns t) (map (fmap (update ns)) args)

@@ -189,8 +189,8 @@ extension syn ns rules =

189189 where upd :: [(Name, SynMatch)] -> [PDo] -> [PDo]

190190 upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

191191 upd ns (DoBind fc n nfc t : ds) = DoBind fc n nfc (update ns t) : upd (dropn n ns) ds

192− upd ns (DoLet fc n ty t : ds) = DoLet fc n (update ns ty) (update ns t)

193− : upd (dropn n ns) ds

192+ upd ns (DoLet fc n nfc ty t : ds) = DoLet fc n nfc (update ns ty) (update ns t)

193+ : upd (dropn n ns) ds

194194 upd ns (DoBindP fc i t ts : ds)

195195 = DoBindP fc (update ns i) (update ns t)

196196 (map (\(l,r) -> (update ns l, update ns r)) ts)

@@ -559,7 +559,7 @@ app syn = do f <- simpleExpr syn

559559 (do try $ reservedOp "<=="

560560 fc <- getFC

561561 ff <- fst <$> fnName

562− return (PLet fc (sMN 0 "match")

562+ return (PLet fc (sMN 0 "match") NoFC

563563 f

564564 (PMatchApp fc ff)

565565 (PRef fc (sMN 0 "match")))

@@ -834,12 +834,12 @@ let_ syn = try (do reserved "let"

834834 return (buildLets ls sc))

835835 <?> "let binding"

836836 where buildLets [] sc = sc

837− buildLets ((fc,PRef _ n,ty,v,[]):ls) sc

838− = PLet fc n ty v (buildLets ls sc)

839− buildLets ((fc,pat,ty,v,alts):ls) sc

837+ buildLets ((fc, PRef nfc n, ty, v, []) : ls) sc

838+ = PLet fc n nfc ty v (buildLets ls sc)

839+ buildLets ((fc, pat, ty, v, alts) : ls) sc

840840 = PCase fc v ((pat, buildLets ls sc) : alts)

841841

842−let_binding syn = do fc <- getFC;

842+let_binding syn = do fc <- getFC;

843843 pat <- expr' (syn { inPattern = True })

844844 ty <- option Placeholder (do lchar ':'; expr' syn)

845845 lchar '='

@@ -1142,13 +1142,13 @@ Do ::=

11421142do_ :: SyntaxInfo -> IdrisParser PDo

11431143do_ syn

11441144 = try (do reserved "let"

1145− i <- fst <$> name

1145+ (i, ifc) <- name

11461146 ty <- option Placeholder (do lchar ':'

11471147 expr' syn)

11481148 reservedOp "="

11491149 fc <- getFC

11501150 e <- expr syn

1151− return (DoLet fc i ty e))

1151+ return (DoLet fc i ifc ty e))

11521152 <|> try (do reserved "let"

11531153 i <- expr' syn

11541154 reservedOp "="

src/Idris/Parser.hs+6−6

@@ -324,8 +324,8 @@ syntaxRule syn

324324 n' <- gensym n

325325 body' <- fixBind ((n,n'):rens) body

326326 return $ (PPi plic n' nfc ty' body')

327− fixBind rens (PLet fc n ty val body)

328− | n `elem` userNames = liftM3 (PLet fc n)

327+ fixBind rens (PLet fc n nfc ty val body)

328+ | n `elem` userNames = liftM3 (PLet fc n nfc)

329329 (fixBind rens ty)

330330 (fixBind rens val)

331331 (fixBind rens body)

@@ -334,7 +334,7 @@ syntaxRule syn

334334 val' <- fixBind rens val

335335 n' <- gensym n

336336 body' <- fixBind ((n,n'):rens) body

337− return $ (PLet fc n' ty' val' body')

337+ return $ PLet fc n' nfc ty' val' body'

338338 fixBind rens (PMatchApp fc n) | Just n' <- lookup n rens =

339339 return $ PMatchApp fc n'

340340 fixBind rens x = descendM (fixBind rens) x

@@ -861,10 +861,10 @@ rhs syn n = do lchar '='; expr syn

861861 n' :: Name

862862 n' = mkN n

863863 addLet :: FC -> Name -> PTerm -> PTerm

864− addLet fc nm (PLet fc' n ty val r) = PLet fc' n ty val (addLet fc nm r)

864+ addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)

865865 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)

866866 where addLetC (l, r) = (l, addLet fc nm r)

867− addLet fc nm r = (PLet fc (sUN "value") Placeholder r (PMetavar nm))

867+ addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar nm))

868868

869869{- |Parses a function clause

870870

@@ -931,7 +931,7 @@ clause syn

931931 return x,

932932 do terminator

933933 return ([], [])]

934− let capp = PLet fc (sMN 0 "match")

934+ let capp = PLet fc (sMN 0 "match") NoFC

935935 ty

936936 (PMatchApp fc n)

937937 (PRef fc (sMN 0 "match"))