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

src/Idris/AbsSyntax.hs+13−13

compare with master

unifiedsplit

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

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

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

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

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

967 = let n' = mkShadow n in

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

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

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

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

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

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

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

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

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

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

1593 [(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)

1595 = case lookupDef n (tt_ctxt ist) of

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

1597 val' = ai qq env ds val

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

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

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

1602 = let ty' = ai qq env ds ty

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

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

1966 ms <- match' s s'

1967 return (mt ++ ms)

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

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

1969− mty <- match' ty ty'

1969+ mty <- match' ty ty'

1970− ms <- match' s s'

1970+ ms <- match' s s'

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

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

1972 match (PHidden x) (PHidden y)

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

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

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

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

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

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

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 (sm t) (sm v) sc

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

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

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

2051 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

2109 ty' <- mkUniq ty

2110 sc'' <- mkUniq sc'

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

2112− mkUniq (PLet fc n ty val sc)

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

2113 = do env <- get

2114 (n', sc') <-

2115 if n `S.member` env

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

2120 put (S.insert n' env)

2121 ty' <- mkUniq ty; val' <- mkUniq val

2122 sc'' <- mkUniq sc'

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

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

2124 mkUniq (PApp fc t args)

2125 = do t' <- mkUniq t

2126 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

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

818 | PPatvar FC Name -- ^ A pattern variable

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

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 PTerm PTerm PTerm -- ^ A let binding

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

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

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

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

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

869mapPT f t = f (mpt t) where

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

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

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

874 (fmap (mapPT f) g)

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

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

959data PDo' t = DoExp FC t

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

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

963 | DoLetP FC t t

964 deriving (Eq, Functor, Data, Typeable)

965{-!

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

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

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

973 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

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

976

977type PDo = PDo' PTerm

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

1028highestFC (PPatvar fc _) = Just fc

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

1030highestFC (PPi _ _ _ _ _) = Nothing

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

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

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

1033highestFC (PApp fc _ _) = Just fc

1034highestFC (PAppBind fc _ _) = Just fc

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

1061 getDoFC (DoExp fc t) = fc

1062 getDoFC (DoBind fc nm nfc t) = fc

1063 getDoFC (DoBindP fc l r alts) = fc

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

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

1065 getDoFC (DoLetP fc l r) = fc

1066

1067highestFC (PIdiom fc _) = Just fc

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

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

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

1457 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) =

1459 bracket p startPrec . group . align $

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

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

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

1874 size (PRef fc name) = size name

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

1876 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

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

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

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

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

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

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

1951 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

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

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

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

51 , pexp (var dsl n tm 0)]

52 in expandSugar dsl sc

53expandSugar 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)

55 | Just letb <- dsl_let dsl

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

57 , pexp v

58 , pexp (var dsl n tm 0)]

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

61expandSugar dsl (PPi p n fc ty tm)

62 | Just pi <- dsl_pi dsl

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

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

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

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

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

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

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

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

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

108 block b (DoLetP fc p tm : rest)

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

110 block b (DoExp fc tm : rest)

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

128 | Nothing <- dsl_lambda dsl

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

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

132 | Nothing <- dsl_let dsl

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

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

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

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

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

136 | Nothing <- dsl_pi dsl

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

191 args' <- mapM dbArg args

192 return (PApp fc t' args')

193 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

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

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

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

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

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

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

src/Idris/DeepSeq.hs+4−4

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

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

222 rnf (PPi x1 x2 x3 x4 x5)

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

224− rnf (PLet _ x1 x2 x3 x4)

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

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

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

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

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

228 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

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

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

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

321+ rnf (DoLet x1 x2 x3 x4 x5)

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

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

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

324

325instance (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

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

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

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

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

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

92 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

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

18 bindPats [] rhs = rhs

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

21

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

23collectAs (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

570 elabE ec' fc sc

571 solve

572 highlightSource nfc (AnnBoundName n False)

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

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

574 = do attack

575 ivs <- get_instances

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

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

606 Just (Let t v) -> v

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

608 solve

609+ highlightSource nfc (AnnBoundName n False)

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

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

610 rty <- goal

611 rty <- goal

611 attack

612 attack

src/Idris/ElabQuasiquote.hs+4−4

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

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

64extractDoUnquotes d (DoBindP fc t t' alts)

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

66−extractDoUnquotes d (DoLet fc n v b)

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

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

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

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

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

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

71

72

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

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

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

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

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

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

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

87extractUnquotes n (PTyped tm ty)

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

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

src/Idris/Error.hs+2−2

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

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

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

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

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

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

99 mapM_ (warnDisamb ist . getTm) args

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

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

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

126 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

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

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

130warnDisamb ist (PReturn _) = return ()

src/Idris/IBC.hs+17−13

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

1528 put x3

1529 put x4

1530 put x5

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

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

1532− put x1

1532+ put x1

1533− put x2

1533+ put x2

1534− put x3

1534+ put x3

1535− put x4

1535+ put x4

1536− put x5

1536+ put x5

1537+ put x6

1537 PTyped x1 x2 -> do putWord8 7

1538 PTyped x1 x2 -> do putWord8 7

1538 put x1

1539 put x1

1539 put x2

1540 put x2

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

1677 x3 <- get

1678 x3 <- get

1678 x4 <- get

1679 x4 <- get

1679 x5 <- get

1680 x5 <- get

1681+ x6 <- get

1680− return (PLet x1 x2 x3 x4 x5)

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

1681 7 -> do x1 <- get

1683 7 -> do x1 <- get

1682 x2 <- get

1684 x2 <- get

1683 return (PTyped x1 x2)

1685 return (PTyped x1 x2)

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

1969 put x2

1971 put x2

1970 put x3

1972 put x3

1971 put x4

1973 put x4

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

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

1973− put x1

1975+ put x1

1974− put x2

1976+ put x2

1975− put x3

1977+ put x3

1976− put x4

1978+ put x4

1979+ put x5

1977 DoLetP x1 x2 x3 -> do putWord8 4

1980 DoLetP x1 x2 x3 -> do putWord8 4

1978 put x1

1981 put x1

1979 put x2

1982 put x2

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

1998 x2 <- get

2001 x2 <- get

1999 x3 <- get

2002 x3 <- get

2000 x4 <- get

2003 x4 <- get

2004+ x5 <- get

2001− return (DoLet x1 x2 x3 x4)

2005+ return (DoLet x1 x2 x3 x4 x5)

2002 4 -> do x1 <- get

2006 4 -> do x1 <- get

2003 x2 <- get

2007 x2 <- get

2004 x3 <- get

2008 x3 <- get

src/Idris/IdrisDoc.hs+8−8

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

293extractPTermNames (PPatvar _ n) = [n]

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

295extractPTermNames (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]

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

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

299 in (extract p) ++ names

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

340

341-- | Helper function for extractPTermNames

342extractPDo :: PDo -> [Name]

343−extractPDo (DoExp _ p) = extract p

343+extractPDo (DoExp _ p) = extract p

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

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

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

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

346− ps' = ps1 ++ ps2

346+ ps' = ps1 ++ ps2

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

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

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

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

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

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

350

351-- | Helper function for extractPTermNames

352extractPTactic :: PTactic -> [Name]

src/Idris/Interactive.hs+1−1

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

198 else iPrintResult newmv

199 where dropCtxt 0 sc = sc

200 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

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

203 dropCtxt _ t = t

204

src/Idris/ParseExpr.hs+11−11

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

169 update ns (PPi p n fc ty sc)

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

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

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

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

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

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

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

175 update ns (PApp fc t args)

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

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

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

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

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

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

193+ : upd (dropn n ns) ds

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

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

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

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

559 (do try $ reservedOp "<=="

560 fc <- getFC

561 ff <- fst <$> fnName

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

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

563 f

564 (PMatchApp fc ff)

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

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

834 return (buildLets ls sc))

835 <?> "let binding"

836 where buildLets [] sc = sc

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

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

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

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

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

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

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

841

842−let_binding syn = do fc <- getFC;

842+let_binding syn = do fc <- getFC;

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

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

845 lchar '='

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

1142do_ :: SyntaxInfo -> IdrisParser PDo

1143do_ syn

1144 = try (do reserved "let"

1145− i <- fst <$> name

1145+ (i, ifc) <- name

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

1147 expr' syn)

1148 reservedOp "="

1149 fc <- getFC

1150 e <- expr syn

1151− return (DoLet fc i ty e))

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

1152 <|> try (do reserved "let"

1153 i <- expr' syn

1154 reservedOp "="

src/Idris/Parser.hs+6−6

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

324 n' <- gensym n

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

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

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

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

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

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

329 (fixBind rens ty)

330 (fixBind rens val)

331 (fixBind rens body)

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

334 val' <- fixBind rens val

335 n' <- gensym n

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

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

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

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

339 return $ PMatchApp fc n'

340 fixBind rens x = descendM (fixBind rens) x

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

861 n' :: Name

862 n' = mkN n

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

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

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

868

869{- |Parses a function clause

870

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

931 return x,

932 do terminator

933 return ([], [])]

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

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

935 ty

936 (PMatchApp fc n)

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