e95c877 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+40−31

@@ -874,21 +874,21 @@ expandParams dec ps ns infs tm = en tm

874874 mkShadow (MN i n) = MN (i+1) n

875875 mkShadow (NS x s) = NS (mkShadow x) s

876876

877− en (PLam n t s)

877+ en (PLam fc n t s)

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

879879 = let n' = mkShadow n in

880− PLam n' (en t) (en (shadow n n' s))

881− | otherwise = PLam n (en t) (en s)

880+ PLam fc n' (en t) (en (shadow n n' s))

881+ | otherwise = PLam fc n (en t) (en s)

882882 en (PPi p n t s)

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

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

885885 PPi (enTacImp p) n' (en t) (en (shadow n n' s))

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

887− en (PLet n ty v s)

887+ en (PLet fc n ty v s)

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

889889 = let n' = mkShadow n in

890− PLet n' (en ty) (en v) (en (shadow n n' s))

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

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

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

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

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

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

@@ -1396,7 +1396,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

13961396 = do (decls, ns) <- get

13971397 let isn = concatMap (namesIn uvars ist) as

13981398 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1399− imps top env (PLam n ty sc)

1399+ imps top env (PLam fc n ty sc)

14001400 = do imps False env ty

14011401 imps False (n:env) sc

14021402 imps top env (PHidden tm) = imps False env tm

@@ -1488,15 +1488,24 @@ addImpl' inpat env infns ist ptm

14881488 -- definition which is passed through addImpl again with more scope

14891489 -- information

14901490 PCase fc c' os

1491− ai qq env ds (PLam n ty sc)

1492− = let ty' = ai qq env ds ty

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

1494− PLam n ty' sc'

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

1496− = let ty' = ai qq env ds ty

1497− val' = ai qq env ds val

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

1499− PLet n ty' val' sc'

1491+ -- If the name in a lambda is a constructor name, do this as a 'case'

1492+ -- instead (it is harmless to do so, especially since the lambda will

1493+ -- be lifted anyway!)

1494+ ai qq env ds (PLam fc n ty sc)

1495+ = case lookupDef n (tt_ctxt ist) of

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

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

1498+ PLam fc n ty' sc'

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

1500+ (PCase fc (PRef fc (sMN 0 "lamp") )

1501+ [(PRef fc n, sc)]))

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

1503+ = case lookupDef n (tt_ctxt ist) of

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

1505+ val' = ai qq env ds val

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

1507+ PLet fc n ty' val' sc'

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

15001509 ai qq env ds (PPi p n ty sc)

15011510 = let ty' = ai qq env ds ty

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

@@ -1696,7 +1705,7 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

16961705 else PAlternative b alts'

16971706 su (PPair fc p l r) = PPair fc p (su l) (su r)

16981707 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1699− su t@(PLam _ _ _) = PHidden t

1708+ su t@(PLam fc _ _ _) = PHidden t

17001709 su t@(PPi _ _ _ _) = PHidden t

17011710 su t@(PEq _ _ _ _ _) = PHidden t

17021711 su t = t

@@ -1843,13 +1852,13 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

18431852 match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'

18441853 ms <- match' s s'

18451854 return (mt ++ ms)

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

1847− ms <- match' s s'

1848− return (mt ++ ms)

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

1850− mty <- match' ty ty'

1851− ms <- match' s s'

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

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

1856+ ms <- match' s s'

1857+ return (mt ++ ms)

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

1859+ mty <- match' ty ty'

1860+ ms <- match' s s'

1861+ return (mt ++ mty ++ ms)

18531862 match (PHidden x) (PHidden y)

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

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

@@ -1892,7 +1901,7 @@ substMatch n = substMatchShadow n []

18921901substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm

18931902substMatchShadow n shs tm t = sm shs t where

18941903 sm xs (PRef _ n') | n == n' = tm

1895− sm xs (PLam x t sc) = PLam x (sm xs t) (sm xs sc)

1904+ sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)

18961905 sm xs (PPi p x t sc)

18971906 | x `elem` xs

18981907 = let x' = nextName x in

@@ -1919,9 +1928,9 @@ substMatchShadow n shs tm t = sm shs t where

19191928shadow :: Name -> Name -> PTerm -> PTerm

19201929shadow n n' t = sm t where

19211930 sm (PRef fc x) | n == x = PRef fc n'

1922− sm (PLam x t sc) | n /= x = PLam x (sm t) (sm sc)

1931+ sm (PLam fc x t sc) | n /= x = PLam fc x (sm t) (sm sc)

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

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

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

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

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

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

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

19601969 mkUniqT tac = return tac

19611970

19621971 mkUniq :: PTerm -> State (S.Set Name) PTerm

1963− mkUniq (PLam n ty sc)

1972+ mkUniq (PLam fc n ty sc)

19641973 = do env <- get

19651974 (n', sc') <-

19661975 if n `S.member` env

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

19711980 put (S.insert n' env)

19721981 ty' <- mkUniq ty

19731982 sc'' <- mkUniq sc'

1974− return $! PLam n' ty' sc''

1983+ return $! PLam fc n' ty' sc''

19751984 mkUniq (PPi p n ty sc)

19761985 = do env <- get

19771986 (n', sc') <-

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

19841993 ty' <- mkUniq ty

19851994 sc'' <- mkUniq sc'

19861995 return $! PPi p n' ty' sc''

1987− mkUniq (PLet n ty val sc)

1996+ mkUniq (PLet fc n ty val sc)

19881997 = do env <- get

19891998 (n', sc') <-

19901999 if n `S.member` env

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

19952004 put (S.insert n' env)

19962005 ty' <- mkUniq ty; val' <- mkUniq val

19972006 sc'' <- mkUniq sc'

1998− return $! PLet n' ty' val' sc''

2007+ return $! PLet fc n' ty' val' sc''

19992008 mkUniq (PApp fc t args)

20002009 = do t' <- mkUniq t

20012010 args' <- mapM mkUniqA args

src/Idris/AbsSyntaxTree.hs+14−14

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

720720 | PRef FC Name -- ^ A reference to a variable

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

722722 | PPatvar FC Name -- ^ A pattern variable

723− | PLam Name PTerm PTerm -- ^ A lambda abstraction

723+ | PLam FC Name PTerm PTerm -- ^ A lambda abstraction

724724 | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2

725− | PLet Name PTerm PTerm PTerm -- ^ A let binding

725+ | PLet FC Name PTerm PTerm PTerm -- ^ A let binding

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

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

728728 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

@@ -767,9 +767,9 @@ deriving instance NFData PTerm

767767

768768mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

769769mapPT f t = f (mpt t) where

770− mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)

770+ mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)

771771 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

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

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

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

774774 (fmap (mapPT f) g)

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

@@ -1285,11 +1285,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

12851285 | Just str <- slist p bnd e = str

12861286 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

12871287 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1288− prettySe p bnd (PLam n ty sc) =

1288+ prettySe p bnd (PLam fc n ty sc) =

12891289 bracket p 2 . group . align . hang 2 $

12901290 text "\\" <> bindingOf n False <+> text "=>" <$>

12911291 prettySe 10 ((n, False):bnd) sc

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

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

12931293 bracket p 2 . group . align $

12941294 kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>

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

@@ -1692,9 +1692,9 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

16921692instance Sized PTerm where

16931693 size (PQuote rawTerm) = size rawTerm

16941694 size (PRef fc name) = size name

1695− size (PLam name ty bdy) = 1 + size ty + size bdy

1695+ size (PLam fc name ty bdy) = 1 + size ty + size bdy

16961696 size (PPi plicity name ty bdy) = 1 + size ty + size bdy

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

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

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

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

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

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

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

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

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

1742− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1742+ ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

17431743 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

17441744 ni env (PHidden tm) = ni env tm

17451745 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

@@ -1764,8 +1764,8 @@ boundNamesIn tm = nub $ ni tm

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

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

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

1767− ni (PLam n ty sc) = n : (ni ty ++ ni sc)

1768− ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1767+ ni (PLam fc n ty sc) = n : (ni ty ++ ni sc)

1768+ ni (PLet fc n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

17691769 ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

17701770 ni (PEq _ _ _ l r) = ni l ++ ni r

17711771 ni (PRewrite _ l r _) = ni l ++ ni r

@@ -1801,7 +1801,7 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

18011801 -- names in 'os', not counting the names bound in the cases

18021802 (nub (concatMap (ni env) (map snd os))

18031803 \\ nub (concatMap (ni env) (map fst os)))

1804− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1804+ ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

18051805 ni env (PPi p n ty sc) = ni env ty ++ ni (n:env) sc

18061806 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

18071807 ni env (PRewrite _ l r _) = ni env l ++ ni env r

@@ -1831,7 +1831,7 @@ namesIn uvars ist tm = nub $ ni [] tm

18311831 -- names in 'os', not counting the names bound in the cases

18321832 (nub (concatMap (ni env) (map snd os))

18331833 \\ nub (concatMap (ni env) (map fst os)))

1834− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1834+ ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

18351835 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

18361836 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

18371837 ni env (PRewrite _ l r _) = ni env l ++ ni env r

@@ -1862,7 +1862,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

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

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

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

1865− ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1865+ ni env (PLam fc n ty sc) = ni env ty ++ ni (n:env) sc

18661866 ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

18671867 ni env (PEq _ _ _ l r) = ni env l ++ ni env r

18681868 ni env (PRewrite _ l r _) = ni env l ++ ni env r

src/Idris/DSL.hs+19−19

@@ -18,16 +18,16 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in

1818 t' -- addImpl i t'

1919

2020expandDo :: DSL -> PTerm -> PTerm

21−expandDo dsl (PLam n ty tm)

21+expandDo dsl (PLam fc n ty tm)

2222 | Just lam <- dsl_lambda dsl

23− = let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in

23+ = let sc = PApp fc lam [pexp (var dsl n tm 0)] in

2424 expandDo dsl sc

25−expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

26−expandDo dsl (PLet n ty v tm)

25+expandDo dsl (PLam fc n ty tm) = PLam fc n (expandDo dsl ty) (expandDo dsl tm)

26+expandDo dsl (PLet fc n ty v tm)

2727 | Just letb <- dsl_let dsl

2828 = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

2929 expandDo dsl sc

30−expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

30+expandDo dsl (PLet fc n ty v tm) = PLet fc n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

3131expandDo dsl (PPi p n ty tm)

3232 | Just pi <- dsl_pi dsl

3333 = let sc = PApp (fileFC "(dsl)") pi [pexp ty, pexp (var dsl n tm 0)] in

@@ -60,19 +60,19 @@ expandDo dsl (PDoBlock ds)

6060 block b [DoExp fc tm] = tm

6161 block b [a] = PElabError (Msg "Last statement in do block must be an expression")

6262 block b (DoBind fc n tm : rest)

63− = PApp fc b [pexp tm, pexp (PLam n Placeholder (block b rest))]

63+ = PApp fc b [pexp tm, pexp (PLam fc n Placeholder (block b rest))]

6464 block b (DoBindP fc p tm alts : rest)

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

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

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

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

6868 block b (DoLet fc n ty tm : rest)

69− = PLet n ty tm (block b rest)

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

7070 block b (DoLetP fc p tm : rest)

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

7272 block b (DoExp fc tm : rest)

7373 = PApp fc b

7474 [pexp tm,

75− pexp (PLam (sMN 0 "bindx") Placeholder (block b rest))]

75+ pexp (PLam fc (sMN 0 "bindx") Placeholder (block b rest))]

7676 block b _ = PElabError (Msg "Invalid statement in do block")

7777

7878expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

@@ -84,14 +84,14 @@ var dsl n t i = v' i t where

8484 case dsl_var dsl of

8585 Nothing -> PElabError (Msg "No 'variable' defined in dsl")

8686 Just v -> PApp fc v [pexp (mkVar fc i)]

87− v' i (PLam n ty sc)

87+ v' i (PLam fc n ty sc)

8888 | Nothing <- dsl_lambda dsl

89− = PLam n ty (v' i sc)

90− | otherwise = PLam n (v' i ty) (v' (i + 1) sc)

91− v' i (PLet n ty val sc)

89+ = PLam fc n ty (v' i sc)

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

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

9292 | Nothing <- dsl_let dsl

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

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

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

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

9595 v' i (PPi p n ty sc)

9696 | Nothing <- dsl_pi dsl

9797 = PPi p n (v' i ty) (v' i sc)

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

146146 = do t' <- db' t

147147 args' <- mapM dbArg args

148148 return (PApp fc t' args')

149− db' (PLam n ty sc) = return (PLam n ty (debind b sc))

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

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

149+ db' (PLam fc n ty sc) = return (PLam fc n ty (debind b sc))

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

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

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

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

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

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

170170

171171 bindAll [] tm = tm

172172 bindAll ((n, fc, t) : bs) tm

173− = PApp fc b [pexp t, pexp (PLam n Placeholder (bindAll bs tm))]

173+ = PApp fc b [pexp t, pexp (PLam fc n Placeholder (bindAll bs tm))]

174174

175175

src/Idris/DeepSeq.hs+2−2

@@ -191,10 +191,10 @@ instance NFData PTerm where

191191 rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

192192 rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

193193 rnf (PPatvar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

194− rnf (PLam x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

194+ rnf (PLam _ x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

195195 rnf (PPi x1 x2 x3 x4)

196196 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

197− rnf (PLet x1 x2 x3 x4)

197+ rnf (PLet _ x1 x2 x3 x4)

198198 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

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

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

src/Idris/Delaborate.hs+5−5

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

5656 Just (Just _, mi, _) -> mkMVApp n []

5757 _ -> PRef un n

5858 de env _ (Bind n (Lam ty) sc)

59− = PLam n (de env [] ty) (de ((n,n):env) [] sc)

59+ = PLam un n (de env [] ty) (de ((n,n):env) [] sc)

6060 de env ((PImp { argopts = opts }):is) (Bind n (Pi ty _) sc)

6161 = PPi (Imp opts Dynamic False) n (de env [] ty) (de ((n,n):env) is sc)

6262 de env (PConstraint _ _ _ _:is) (Bind n (Pi ty _) sc)

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

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

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

7878 | otherwise =

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

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

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

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

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

@@ -382,10 +382,10 @@ addImplicitDiffs x y

382382 else (a { getTm = a' } : as',

383383 b { getTm = b' } : bs')

384384 addShows xs ys = (xs, ys)

385− addI (PLam n a b) (PLam n' c d)

385+ addI (PLam fc n a b) (PLam fc' n' c d)

386386 = let (a', c') = addI a c

387387 (b', d') = addI b d in

388− (PLam n a' b', PLam n' c' d')

388+ (PLam fc n a' b', PLam fc' n' c' d')

389389 addI (PPi p n a b) (PPi p' n' c d)

390390 = let (a', c') = addI a c

391391 (b', d') = addI b d in

@@ -435,7 +435,7 @@ addImplicitDiffs x y

435435 and (zipWith expLike (getExps as) (getExps as'))

436436 expLike (PPi _ n s t) (PPi _ n' s' t')

437437 = n == n' && expLike s s' && expLike t t'

438− expLike (PLam n s t) (PLam n' s' t')

438+ expLike (PLam _ n s t) (PLam _ n' s' t')

439439 = n == n' && expLike s s' && expLike t t'

440440 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

441441 expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

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

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

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

1414 bindPats [] rhs = rhs

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

16− = PLet n Placeholder tm (bindPats ps rhs)

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

1717

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

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

src/Idris/Elab/Instance.hs+2−2

@@ -195,9 +195,9 @@ elabInstance info syn what fc cs n ps t expn ds = do

195195 mkMethApp (n, _, _, ty)

196196 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

197197 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

198− = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

198+ = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

199199 lamBind i (PPi _ n ty sc) sc'

200− = PLam (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

200+ = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')

201201 lamBind i _ sc = sc

202202 methArgs i (PPi (Imp _ _ _) n ty sc)

203203 = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

src/Idris/ElabQuasiquote.hs+4−4

@@ -70,19 +70,19 @@ extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be qua

7070

7171

7272extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])

73−extractUnquotes n (PLam name ty body)

73+extractUnquotes n (PLam fc name ty body)

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

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

76− return (PLam name ty' body', ex1 ++ ex2)

76+ return (PLam fc name ty' body', ex1 ++ ex2)

7777extractUnquotes n (PPi plicity name ty body)

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

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

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

81−extractUnquotes n (PLet name ty val body)

81+extractUnquotes n (PLet fc name ty val body)

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

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

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

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

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

8686extractUnquotes n (PTyped tm ty)

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

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

src/Idris/ElabTerm.hs+11−11

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

362362 _ -> asType

363363 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)

364364 [pexp t,

365− pexp (PLam n Placeholder r)])

365+ pexp (PLam fc n Placeholder r)])

366366 asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)

367367 [pimp (sMN 0 "a") t False,

368368 pimp (sMN 0 "P") Placeholder True,

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

434434 | pattern && not reflection && e_nomatching ina

435435 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

436436 | otherwise = erun fc $ do apply (Var n) []; solve

437− elab' ina fc (PLam n Placeholder sc)

437+ elab' ina _ (PLam fc n Placeholder sc)

438438 = do -- if n is a type constructor name, this makes no sense...

439439 ctxt <- get_context

440440 when (isTConName n ctxt) $

@@ -442,8 +442,8 @@ elab ist info emode opts fn tm

442442 checkPiGoal n

443443 attack; intro (Just n);

444444 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)

445− elabE (ina { e_inarg = True } ) fc sc; solve

446− elab' ec fc (PLam n ty sc)

445+ elabE (ina { e_inarg = True } ) (Just fc) sc; solve

446+ elab' ec _ (PLam fc n ty sc)

447447 = do tyn <- getNameFrom (sMN 0 "lamty")

448448 -- if n is a type constructor name, this makes no sense...

449449 ctxt <- get_context

@@ -458,8 +458,8 @@ elab ist info emode opts fn tm

458458 introTy (Var tyn) (Just n)

459459 focus tyn

460460

461− elabE (ec { e_inarg = True, e_intype = True }) fc ty

462− elabE (ec { e_inarg = True }) fc sc

461+ elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty

462+ elabE (ec { e_inarg = True }) (Just fc) sc

463463 solve

464464 elab' ina fc (PPi _ n Placeholder sc)

465465 = do attack; arg n (sMN 0 "ty")

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

477477 elabE ec' fc ty

478478 elabE ec' fc sc

479479 solve

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

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

481481 = do attack

482482 ivs <- get_instances

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

@@ -491,13 +491,13 @@ elab ist info emode opts fn tm

491491 _ -> do focus tyn

492492 explicit tyn

493493 elabE (ina { e_inarg = True, e_intype = True })

494− fc ty

494+ (Just fc) ty

495495 focus valn

496496 elabE (ina { e_inarg = True, e_intype = True })

497− fc val

497+ (Just fc) val

498498 ivs' <- get_instances

499499 env <- get_env

500− elabE (ina { e_inarg = True }) fc sc

500+ elabE (ina { e_inarg = True }) (Just fc) sc

501501 when (not pattern) $

502502 mapM_ (\n -> do focus n

503503 g <- goal

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

673673 PAlternative False _ -> 5

674674 PAlternative True _ -> 2

675675 PTactics _ -> 150

676− PLam _ _ _ -> 3

676+ PLam _ _ _ _ -> 3

677677 PRewrite _ _ _ _ -> 4

678678 PResolveTC _ -> 0

679679 PHidden _ -> 150

src/Idris/Error.hs+2−2

@@ -87,9 +87,9 @@ warnDisamb ist (PQuote _) = return ()

8787warnDisamb ist (PRef _ _) = return ()

8888warnDisamb ist (PInferRef _ _) = return ()

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

90−warnDisamb ist (PLam _ t b) = warnDisamb ist t >> warnDisamb ist b

90+warnDisamb ist (PLam _ _ t b) = warnDisamb ist t >> warnDisamb ist b

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

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

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

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

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

9595 mapM_ (warnDisamb ist . getTm) args

src/Idris/IBC.hs+16−12

@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)

3232import Util.Zlib (decompressEither)

3333

3434ibcVersion :: Word8

35−ibcVersion = 88

35+ibcVersion = 89

3636

3737data IBCFile = IBCFile { ver :: Word8,

3838 sourcefile :: FilePath,

@@ -1428,20 +1428,22 @@ instance Binary PTerm where

14281428 PPatvar x1 x2 -> do putWord8 3

14291429 put x1

14301430 put x2

1431− PLam x1 x2 x3 -> do putWord8 4

1432− put x1

1433− put x2

1434− put x3

1431+ PLam x1 x2 x3 x4 -> do putWord8 4

1432+ put x1

1433+ put x2

1434+ put x3

1435+ put x4

14351436 PPi x1 x2 x3 x4 -> do putWord8 5

14361437 put x1

14371438 put x2

14381439 put x3

14391440 put x4

1440− PLet x1 x2 x3 x4 -> do putWord8 6

1441− put x1

1442− put x2

1443− put x3

1444− put x4

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

1442+ put x1

1443+ put x2

1444+ put x3

1445+ put x4

1446+ put x5

14451447 PTyped x1 x2 -> do putWord8 7

14461448 put x1

14471449 put x2

@@ -1547,7 +1549,8 @@ instance Binary PTerm where

15471549 4 -> do x1 <- get

15481550 x2 <- get

15491551 x3 <- get

1550− return (PLam x1 x2 x3)

1552+ x4 <- get

1553+ return (PLam x1 x2 x3 x4)

15511554 5 -> do x1 <- get

15521555 x2 <- get

15531556 x3 <- get

@@ -1557,7 +1560,8 @@ instance Binary PTerm where

15571560 x2 <- get

15581561 x3 <- get

15591562 x4 <- get

1560− return (PLet x1 x2 x3 x4)

1563+ x5 <- get

1564+ return (PLet x1 x2 x3 x4 x5)

15611565 7 -> do x1 <- get

15621566 x2 <- get

15631567 return (PTyped x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -273,9 +273,9 @@ extractPTermNames :: PTerm -- ^ Where to extract names from

273273extractPTermNames (PRef _ n) = [n]

274274extractPTermNames (PInferRef _ n) = [n]

275275extractPTermNames (PPatvar _ n) = [n]

276−extractPTermNames (PLam n p1 p2) = n : concatMap extract [p1, p2]

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

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

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

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

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

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

281281 in (extract p) ++ names

src/Idris/Interactive.hs+2−2

@@ -199,8 +199,8 @@ doProofSearch fn updatefile rec l n hints (Just depth)

199199 else iPrintResult newmv

200200 where dropCtxt 0 sc = sc

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

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

203− dropCtxt i (PLam _ _ sc) = dropCtxt (i - 1) sc

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

203+ dropCtxt i (PLam _ _ _ sc) = dropCtxt (i - 1) sc

204204 dropCtxt _ t = t

205205

206206 stripNS tm = mapPT dens tm where

src/Idris/ParseExpr.hs+14−13

@@ -165,13 +165,13 @@ extension syn ns rules =

165165 update ns (PRef fc n) = case lookup n ns of

166166 Just (SynTm t) -> t

167167 _ -> PRef fc n

168− update ns (PLam n ty sc)

169− = PLam (updateB ns n) (update ns ty) (update (dropn n ns) sc)

168+ update ns (PLam fc n ty sc)

169+ = PLam fc (updateB ns n) (update ns ty) (update (dropn n ns) sc)

170170 update ns (PPi p n ty sc)

171171 = PPi (updTacImp ns p) (updateB ns n)

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

173− update ns (PLet n ty val sc)

174− = PLet (updateB ns n) (update ns ty)

173+ update ns (PLet fc n ty val sc)

174+ = PLet fc (updateB ns n) (update ns ty)

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

176176 update ns (PApp fc t args)

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

@@ -388,7 +388,7 @@ bracketed' syn =

388388 -- No prefix operators! (bit of a hack here...)

389389 if (o == "-" || o == "!")

390390 then fail "minus not allowed in section"

391− else return $ PLam (sMN 1000 "ARG") Placeholder

391+ else return $ PLam fc (sMN 1000 "ARG") Placeholder

392392 (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

393393 pexp e]))

394394 <|> try (do l <- simpleExpr syn

@@ -398,7 +398,7 @@ bracketed' syn =

398398 fc0 <- getFC

399399 case op of

400400 Nothing -> bracketedExpr syn l

401− Just o -> return $ PLam (sMN 1000 "ARG") Placeholder

401+ Just o -> return $ PLam fc0 (sMN 1000 "ARG") Placeholder

402402 (PApp fc0 (PRef fc0 (sUN o)) [pexp l,

403403 pexp (PRef fc0 (sMN 1000 "ARG"))]))

404404 <|> do l <- expr syn

@@ -532,7 +532,7 @@ app syn = do f <- reserved "mkForeign"

532532 args <- many (do notEndApp; arg syn)

533533 i <- get

534534 let ap = PApp fc (PRef fc (sUN "liftPrimIO"))

535− [pexp (PLam (sMN 0 "w")

535+ [pexp (PLam fc (sMN 0 "w")

536536 Placeholder

537537 (PApp fc (PRef fc (sUN "mkForeignPrim"))

538538 (fn : args ++

@@ -543,7 +543,7 @@ app syn = do f <- reserved "mkForeign"

543543 (do try $ reservedOp "<=="

544544 fc <- getFC

545545 ff <- fnName

546− return (PLet (sMN 0 "match")

546+ return (PLet fc (sMN 0 "match")

547547 f

548548 (PMatchApp fc ff)

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

@@ -667,13 +667,13 @@ recordType syn =

667667 Left fields ->

668668 case rec of

669669 Nothing ->

670− return (PLam (sMN 0 "fldx") Placeholder

670+ return (PLam fc (sMN 0 "fldx") Placeholder

671671 (applyAll fc fields (PRef fc (sMN 0 "fldx"))))

672672 Just v -> return (applyAll fc fields v)

673673 Right fields ->

674674 case rec of

675675 Nothing ->

676− return (PLam (sMN 0 "fldx") Placeholder

676+ return (PLam fc (sMN 0 "fldx") Placeholder

677677 (getAll fc (reverse fields)

678678 (PRef fc (sMN 0 "fldx"))))

679679 Just v -> return (getAll fc (reverse fields) v)

@@ -752,9 +752,10 @@ SimpleExprList ::=

752752lambda :: SyntaxInfo -> IdrisParser PTerm

753753lambda syn = do lchar '\\' <?> "lambda expression"

754754 (do xt <- try $ tyOptDeclList syn

755+ fc <- getFC

755756 symbol "=>"

756757 sc <- expr syn

757− return (bindList PLam xt sc)) <|> do

758+ return (bindList (PLam fc) xt sc)) <|> do

758759 ps <- sepBy (do fc <- getFC

759760 e <- simpleExpr syn

760761 return (fc, e)) (lchar ',')

@@ -765,7 +766,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"

765766 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm

766767 pmList [] sc = sc

767768 pmList ((i, (fc, x)) : xs) sc

768− = PLam (sMN i "lamp") Placeholder

769+ = PLam fc (sMN i "lamp") Placeholder

769770 (PCase fc (PRef fc (sMN i "lamp"))

770771 [(x, pmList xs sc)])

771772

@@ -806,7 +807,7 @@ let_ syn = try (do reserved "let"

806807 <?> "let binding"

807808 where buildLets [] sc = sc

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

809− = PLet n ty v (buildLets ls sc)

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

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

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

812813

src/Idris/Parser.hs+8−7

@@ -758,10 +758,11 @@ RHSName ::= '{' FnName '}';

758758rhs :: SyntaxInfo -> Name -> IdrisParser PTerm

759759rhs syn n = do lchar '='; expr syn

760760 <|> do symbol "?=";

761+ fc <- getFC

761762 name <- option n' (do symbol "{"; n <- fnName; symbol "}";

762763 return n)

763764 r <- expr syn

764− return (addLet name r)

765+ return (addLet fc name r)

765766 <|> do reserved "impossible"; return PImpossible

766767 <?> "function right hand side"

767768 where mkN :: Name -> Name

@@ -771,11 +772,11 @@ rhs syn n = do lchar '='; expr syn

771772 mkN (NS x n) = NS (mkN x) n

772773 n' :: Name

773774 n' = mkN n

774− addLet :: Name -> PTerm -> PTerm

775− addLet nm (PLet n ty val r) = PLet n ty val (addLet nm r)

776− addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)

777− where addLetC (l, r) = (l, addLet nm r)

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

775+ addLet :: FC -> Name -> PTerm -> PTerm

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

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

778+ where addLetC (l, r) = (l, addLet fc nm r)

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

779780

780781{- |Parses a function clause

781782

@@ -841,7 +842,7 @@ clause syn

841842 return x,

842843 do terminator

843844 return ([], [])]

844− let capp = PLet (sMN 0 "match")

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

845846 ty

846847 (PMatchApp fc n)

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