e95c877 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make pattern matching consistent in lambda/let

e95c877Edwin Brady12 years ago

src/Idris/AbsSyntax.hs+40−31

compare with master

unifiedsplit

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

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

875 mkShadow (NS x s) = NS (mkShadow x) s

876

877− en (PLam n t s)

877+ en (PLam fc n t s)

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

879 = let n' = mkShadow n in

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

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

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

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

882 en (PPi p n t s)

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

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

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

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

887− en (PLet n ty v s)

887+ en (PLet fc n ty v s)

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

889 = let n' = mkShadow n in

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

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

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

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

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

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

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

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

1396 = do (decls, ns) <- get

1397 let isn = concatMap (namesIn uvars ist) as

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

1400 = do imps False env ty

1401 imps False (n:env) sc

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

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

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

1489 -- information

1490 PCase fc c' os

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

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

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

1495+ = case lookupDef n (tt_ctxt ist) of

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

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

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

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

1494− PLam n ty' sc'

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

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

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

1503+ = case lookupDef n (tt_ctxt ist) of

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

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

1497− val' = ai qq env ds val

1505+ val' = ai qq env ds val

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

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

1499− PLet n ty' val' sc'

1507+ PLet fc n ty' val' sc'

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

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

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

1501 = let ty' = ai qq env ds ty

1510 = let ty' = ai qq env ds ty

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

1511 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

1696 else PAlternative b alts'

1705 else PAlternative b alts'

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

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

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

1707 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

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

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

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

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

1702 su t = t

1711 su t = t

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

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

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

1844 ms <- match' s s'

1853 ms <- match' s s'

1845 return (mt ++ ms)

1854 return (mt ++ ms)

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

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

1847− ms <- match' s s'

1856+ ms <- match' s s'

1848− return (mt ++ ms)

1857+ return (mt ++ ms)

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

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

1850− mty <- match' ty ty'

1859+ mty <- match' ty ty'

1851− ms <- match' s s'

1860+ ms <- match' s s'

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

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

1853 match (PHidden x) (PHidden y)

1862 match (PHidden x) (PHidden y)

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

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

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

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

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

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

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

1893substMatchShadow n shs tm t = sm shs t where

1902substMatchShadow n shs tm t = sm shs t where

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

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

1896 sm xs (PPi p x t sc)

1905 sm xs (PPi p x t sc)

1897 | x `elem` xs

1906 | x `elem` xs

1898 = let x' = nextName x in

1907 = let x' = nextName x in

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

1919shadow :: Name -> Name -> PTerm -> PTerm

1928shadow :: Name -> Name -> PTerm -> PTerm

1920shadow n n' t = sm t where

1929shadow n n' t = sm t where

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

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

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

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

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

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

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

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

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

1936 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

1960 mkUniqT tac = return tac

1969 mkUniqT tac = return tac

1961

1970

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

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

1963− mkUniq (PLam n ty sc)

1972+ mkUniq (PLam fc n ty sc)

1964 = do env <- get

1973 = do env <- get

1965 (n', sc') <-

1974 (n', sc') <-

1966 if n `S.member` env

1975 if n `S.member` env

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

1971 put (S.insert n' env)

1980 put (S.insert n' env)

1972 ty' <- mkUniq ty

1981 ty' <- mkUniq ty

1973 sc'' <- mkUniq sc'

1982 sc'' <- mkUniq sc'

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

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

1975 mkUniq (PPi p n ty sc)

1984 mkUniq (PPi p n ty sc)

1976 = do env <- get

1985 = do env <- get

1977 (n', sc') <-

1986 (n', sc') <-

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

1984 ty' <- mkUniq ty

1993 ty' <- mkUniq ty

1985 sc'' <- mkUniq sc'

1994 sc'' <- mkUniq sc'

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

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

1987− mkUniq (PLet n ty val sc)

1996+ mkUniq (PLet fc n ty val sc)

1988 = do env <- get

1997 = do env <- get

1989 (n', sc') <-

1998 (n', sc') <-

1990 if n `S.member` env

1999 if n `S.member` env

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

1995 put (S.insert n' env)

2004 put (S.insert n' env)

1996 ty' <- mkUniq ty; val' <- mkUniq val

2005 ty' <- mkUniq ty; val' <- mkUniq val

1997 sc'' <- mkUniq sc'

2006 sc'' <- mkUniq sc'

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

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

1999 mkUniq (PApp fc t args)

2008 mkUniq (PApp fc t args)

2000 = do t' <- mkUniq t

2009 = do t' <- mkUniq t

2001 args' <- mapM mkUniqA args

2010 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

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

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

722 | PPatvar FC Name -- ^ A pattern variable

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

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

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

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

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

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

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

767

768mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

769mapPT 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)

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

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

774 (fmap (mapPT f) g)

775 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

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

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

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

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

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

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

1293 bracket p 2 . group . align $

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

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

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

1692instance Sized PTerm where

1693 size (PQuote rawTerm) = size rawTerm

1694 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

1696 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

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

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

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

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

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

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

1741 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

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

1744 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1864 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

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

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

1868 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

18 t' -- addImpl i t'

20expandDo :: DSL -> PTerm -> PTerm

21−expandDo dsl (PLam n ty tm)

21+expandDo dsl (PLam fc n ty tm)

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

24 expandDo dsl sc

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

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

26−expandDo dsl (PLet n ty v tm)

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

27 | Just letb <- dsl_let dsl

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

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

31expandDo dsl (PPi p n ty tm)

32 | Just pi <- dsl_pi dsl

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

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

60 block b [DoExp fc tm] = tm

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

62 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))]

64 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

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

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

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

70 block b (DoLetP fc p tm : rest)

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

72 block b (DoExp fc tm : rest)

73 = PApp fc b

74 [pexp tm,

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

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

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

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

84 case dsl_var dsl of

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

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

87− v' i (PLam n ty sc)

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

88 | Nothing <- dsl_lambda dsl

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

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

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

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

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

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

92 | Nothing <- dsl_let dsl

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

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

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

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

95 v' i (PPi p n ty sc)

96 | Nothing <- dsl_pi dsl

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

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

146 = do t' <- db' t

147 args' <- mapM dbArg args

148 return (PApp fc t' args')

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

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

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

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

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

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

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

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

154 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

170

171 bindAll [] tm = tm

172 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))]

174

175

src/Idris/DeepSeq.hs+2−2

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

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

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

193 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` ()

195 rnf (PPi x1 x2 x3 x4)

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

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

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

200 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

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

57 _ -> PRef un n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

387 (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')

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

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

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

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

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

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

437 = 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')

439 = n == n' && expLike s s' && expLike t t'

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

441 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

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

14 bindPats [] rhs = rhs

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

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

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

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

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

195 mkMethApp (n, _, _, ty)

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

197 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')

199 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')

201 lamBind i _ sc = sc

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

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

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

73−extractUnquotes n (PLam name ty body)

73+extractUnquotes n (PLam fc name ty body)

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

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

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

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

77extractUnquotes n (PPi plicity name ty body)

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

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

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

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

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

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

86extractUnquotes n (PTyped tm ty)

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

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

src/Idris/ElabTerm.hs+11−11

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

362 _ -> asType

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

364 [pexp t,

365− pexp (PLam n Placeholder r)])

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

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

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

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

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

434 | pattern && not reflection && e_nomatching ina

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

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

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

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

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

439 ctxt <- get_context

440 when (isTConName n ctxt) $

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

442 checkPiGoal n

443 attack; intro (Just n);

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

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

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

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

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

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

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

449 ctxt <- get_context

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

458 introTy (Var tyn) (Just n)

459 focus tyn

460

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

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

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

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

463 solve

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

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

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

477 elabE ec' fc ty

478 elabE ec' fc sc

479 solve

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

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

481 = do attack

482 ivs <- get_instances

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

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

491 _ -> do focus tyn

492 explicit tyn

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

494− fc ty

494+ (Just fc) ty

495 focus valn

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

497− fc val

497+ (Just fc) val

498 ivs' <- get_instances

499 env <- get_env

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

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

501 when (not pattern) $

502 mapM_ (\n -> do focus n

503 g <- goal

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

673 PAlternative False _ -> 5

674 PAlternative True _ -> 2

675 PTactics _ -> 150

676− PLam _ _ _ -> 3

676+ PLam _ _ _ _ -> 3

677 PRewrite _ _ _ _ -> 4

678 PResolveTC _ -> 0

679 PHidden _ -> 150

src/Idris/Error.hs+2−2

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

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

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

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

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

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

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

95 mapM_ (warnDisamb ist . getTm) args

src/Idris/IBC.hs+16−12

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

32import Util.Zlib (decompressEither)

34ibcVersion :: Word8

35−ibcVersion = 88

35+ibcVersion = 89

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

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

1428 PPatvar x1 x2 -> do putWord8 3

1429 put x1

1430 put x2

1431− PLam x1 x2 x3 -> do putWord8 4

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

1432− put x1

1432+ put x1

1433− put x2

1433+ put x2

1434− put x3

1434+ put x3

1435+ put x4

1435 PPi x1 x2 x3 x4 -> do putWord8 5

1436 PPi x1 x2 x3 x4 -> do putWord8 5

1436 put x1

1437 put x1

1437 put x2

1438 put x2

1438 put x3

1439 put x3

1439 put x4

1440 put x4

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

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

1441− put x1

1442+ put x1

1442− put x2

1443+ put x2

1443− put x3

1444+ put x3

1444− put x4

1445+ put x4

1446+ put x5

1445 PTyped x1 x2 -> do putWord8 7

1447 PTyped x1 x2 -> do putWord8 7

1446 put x1

1448 put x1

1447 put x2

1449 put x2

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

1547 4 -> do x1 <- get

1549 4 -> do x1 <- get

1548 x2 <- get

1550 x2 <- get

1549 x3 <- get

1551 x3 <- get

1552+ x4 <- get

1550− return (PLam x1 x2 x3)

1553+ return (PLam x1 x2 x3 x4)

1551 5 -> do x1 <- get

1554 5 -> do x1 <- get

1552 x2 <- get

1555 x2 <- get

1553 x3 <- get

1556 x3 <- get

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

1557 x2 <- get

1560 x2 <- get

1558 x3 <- get

1561 x3 <- get

1559 x4 <- get

1562 x4 <- get

1563+ x5 <- get

1560− return (PLet x1 x2 x3 x4)

1564+ return (PLet x1 x2 x3 x4 x5)

1561 7 -> do x1 <- get

1565 7 -> do x1 <- get

1562 x2 <- get

1566 x2 <- get

1563 return (PTyped x1 x2)

1567 return (PTyped x1 x2)

src/Idris/IdrisDoc.hs+2−2

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

273extractPTermNames (PRef _ n) = [n]

274extractPTermNames (PInferRef _ n) = [n]

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

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

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

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

281 in (extract p) ++ names

src/Idris/Interactive.hs+2−2

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

199 else iPrintResult newmv

200 where dropCtxt 0 sc = sc

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

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

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

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

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

204 dropCtxt _ t = t

205

206 stripNS tm = mapPT dens tm where

src/Idris/ParseExpr.hs+14−13

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

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

166 Just (SynTm t) -> t

167 _ -> PRef fc n

168− update ns (PLam n ty sc)

168+ update ns (PLam fc n ty sc)

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

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

170 update ns (PPi p n ty sc)

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

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

173− update ns (PLet n ty val sc)

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

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

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

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

176 update ns (PApp fc t args)

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

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

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

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

390 then fail "minus not allowed in section"

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

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

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

393 pexp e]))

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

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

398 fc0 <- getFC

399 case op of

400 Nothing -> bracketedExpr syn l

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

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

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

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

404 <|> do l <- expr syn

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

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

533 i <- get

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

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

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

536 Placeholder

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

538 (fn : args ++

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

543 (do try $ reservedOp "<=="

544 fc <- getFC

545 ff <- fnName

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

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

547 f

548 (PMatchApp fc ff)

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

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

667 Left fields ->

668 case rec of

669 Nothing ->

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

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

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

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

673 Right fields ->

674 case rec of

675 Nothing ->

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

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

677 (getAll fc (reverse fields)

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

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

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

752lambda :: SyntaxInfo -> IdrisParser PTerm

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

754 (do xt <- try $ tyOptDeclList syn

755+ fc <- getFC

755 symbol "=>"

756 symbol "=>"

756 sc <- expr syn

757 sc <- expr syn

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

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

758 ps <- sepBy (do fc <- getFC

759 ps <- sepBy (do fc <- getFC

759 e <- simpleExpr syn

760 e <- simpleExpr syn

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

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

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

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

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

766 pmList [] sc = sc

767 pmList [] sc = sc

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

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

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

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

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

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

770 [(x, pmList xs sc)])

771 [(x, pmList xs sc)])

771

772

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

806 <?> "let binding"

807 <?> "let binding"

807 where buildLets [] sc = sc

808 where buildLets [] sc = sc

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

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

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

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

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

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

812

813

src/Idris/Parser.hs+8−7

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

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

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

760 <|> do symbol "?=";

761+ fc <- getFC

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

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

762 return n)

763 return n)

763 r <- expr syn

764 r <- expr syn

764− return (addLet name r)

765+ return (addLet fc name r)

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

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

766 <?> "function right hand side"

767 <?> "function right hand side"

767 where mkN :: Name -> Name

768 where mkN :: Name -> Name

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

771 mkN (NS x n) = NS (mkN x) n

772 mkN (NS x n) = NS (mkN x) n

772 n' :: Name

773 n' :: Name

773 n' = mkN n

774 n' = mkN n

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

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

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

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

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

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

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

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

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

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

779

780

780{- |Parses a function clause

781{- |Parses a function clause

781

782

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

841 return x,

842 return x,

842 do terminator

843 do terminator

843 return ([], [])]

844 return ([], [])]

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

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

845 ty

846 ty

846 (PMatchApp fc n)

847 (PMatchApp fc n)

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

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