689e64b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Highlight pi and lambda binders

689e64bDavid Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+59−57

compare with master

unifiedsplit

@@ -952,16 +952,16 @@ expandParams dec ps ns infs tm = en tm

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

953 mkShadow (NS x s) = NS (mkShadow x) s

954

955− en (PLam fc n t s)

955+ en (PLam fc n nfc t s)

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

957 = let n' = mkShadow n in

958− PLam fc n' (en t) (en (shadow n n' s))

958+ PLam fc n' nfc (en t) (en (shadow n n' s))

959− | otherwise = PLam fc n (en t) (en s)

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

960− en (PPi p n t s)

960+ en (PPi p n nfc t s)

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

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

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

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

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

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

965 en (PLet fc n ty v s)

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

967 = let n' = mkShadow n in

@@ -1136,7 +1136,7 @@ getPriority i tm = 1 -- pri tm

1136 ((P (TCon _ _) _ _):_) -> 1

1137 ((P Ref _ _):_) -> 1

1138 [] -> 0 -- must be locally bound, if it's not an error...

1139− pri (PPi _ _ x y) = max 5 (max (pri x) (pri y))

1139+ pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

1140 pri (PTrue _ _) = 0

1141 pri (PRefl _ _) = 1

1142 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))

@@ -1182,10 +1182,10 @@ addStatics n tm ptm =

1182 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

1183 addIBC (IBCStatic n)

1184 where

1185− initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)

1185+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)

1186− | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in

1186+ | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in

1187 (static, (n, ty) : dynamic)

1188− initStatics (Bind n (Pi _ ty _) sc) (PPi p n' _ s)

1188+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc _ s)

1189 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in

1190 if pstatic p == Static then ((n, ty) : static, dynamic)

1191 else if (not (searchArg p))

@@ -1254,16 +1254,16 @@ addUsingConstraints syn fc t

1254 -- if all of args in ns, then add it

1255 doAdd (UConstraint c args : cs) ns t

1256 | all (\n -> elem n ns) args

1257− = PPi (Constraint [] Dynamic) (sMN 0 "cu")

1257+ = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC

1258 (mkConst c args) (doAdd cs ns t)

1259 | otherwise = doAdd cs ns t

1260

1261 mkConst c args = PApp fc (PRef fc c)

1262 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)

1263

1264− getConstraints (PPi (Constraint _ _) _ c sc)

1264+ getConstraints (PPi (Constraint _ _) _ _ c sc)

1265 = getcapp c ++ getConstraints sc

1266− getConstraints (PPi _ _ c sc) = getConstraints sc

1266+ getConstraints (PPi _ _ _ c sc) = getConstraints sc

1267 getConstraints _ = []

1268

1269 getcapp (PApp _ (PRef _ c) args)

@@ -1300,7 +1300,7 @@ addUsingImpls syn n fc t

1300 -- if all of args in ns, then add it

1301 doAdd (UImplicit n ty : cs) ns t

1302 | elem n ns

1303− = PPi (Imp [] Dynamic False Nothing) n ty (doAdd cs ns t)

1303+ = PPi (Imp [] Dynamic False Nothing) n NoFC ty (doAdd cs ns t)

1304 | otherwise = doAdd cs ns t

1305

1306 -- bind the free names which weren't in the using block

@@ -1308,9 +1308,9 @@ addUsingImpls syn n fc t

1308 bindFree (n:ns) tm

1309 | elem n (map iname uimpls) = bindFree ns tm

1310 | otherwise

1311− = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)

1311+ = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)

1312

1313− getArgnames (PPi _ n c sc)

1313+ getArgnames (PPi _ n _ c sc)

1314 = n : getArgnames sc

1315 getArgnames _ = []

1316

@@ -1319,7 +1319,7 @@ addUsingImpls syn n fc t

1319

1320getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]

1321getUnboundImplicits i t tm = getImps t (collectImps tm)

1322− where collectImps (PPi p n t sc)

1322+ where collectImps (PPi p n _ t sc)

1323 = (n, (p, t)) : collectImps sc

1324 collectImps _ = []

1325

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

1419 = do (decls, ns) <- get

1420 let isn = concatMap (namesIn uvars ist) (map getTm as)

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

1422− imps top env (PPi (Imp l _ _ _) n ty sc)

1422+ imps top env (PPi (Imp l _ _ _) n _ ty sc)

1423 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]

1424 (decls , ns) <- get

1425 put (PImp (getPriority ist ty) True l n Placeholder : decls,

1426 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1427 imps True (n:env) sc

1428− imps top env (PPi (Exp l _ _) n ty sc)

1428+ imps top env (PPi (Exp l _ _) n _ ty sc)

1429 = do let isn = nub (implNamesIn uvars ty ++ case sc of

1430 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1431 _ -> [])

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

1433 put (PExp (getPriority ist ty) l n Placeholder : decls,

1434 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1435 imps True (n:env) sc

1436− imps top env (PPi (Constraint l _) n ty sc)

1436+ imps top env (PPi (Constraint l _) n _ ty sc)

1437 = do let isn = nub (implNamesIn uvars ty ++ case sc of

1438 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1439 _ -> [])

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

1441 put (PConstraint 10 l n Placeholder : decls,

1442 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

1443 imps True (n:env) sc

1444− imps top env (PPi (TacImp l _ scr) n ty sc)

1444+ imps top env (PPi (TacImp l _ scr) n _ ty sc)

1445 = do let isn = nub (implNamesIn uvars ty ++ case sc of

1446 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1447 _ -> [])

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

1476 = do (decls, ns) <- get

1477 let isn = concatMap (namesIn uvars ist) as

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

1479− imps top env (PLam fc n ty sc)

1479+ imps top env (PLam fc n _ ty sc)

1480 = do imps False env ty

1481 imps False (n:env) sc

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

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

1488 pibind using [] sc = sc

1489 pibind using (n:ns) sc

1490 = case lookup n using of

1491− Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)

1491+ Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)

1492− Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder

1492+ Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder

1493 (pibind using ns sc)

1494

1495-- Add implicit arguments in function calls

@@ -1572,18 +1572,20 @@ addImpl' inpat env infns imp_meths ist ptm

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

1573 -- information

1574 PCase fc c' os

1575− -- If the name in a lambda is a constructor name, do this as a 'case'

1575+

1576− -- instead (it is harmless to do so, especially since the lambda will

1577− -- be lifted anyway!)

1578 ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)

1576 ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)

1579 (ai qq env ds t)

1577 (ai qq env ds t)

1580 (ai qq env ds f)

1578 (ai qq env ds f)

1579+

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

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

1582+ -- be lifted anyway!)

1581− ai qq env ds (PLam fc n ty sc)

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

1582 = case lookupDef n (tt_ctxt ist) of

1584 = case lookupDef n (tt_ctxt ist) of

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

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

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

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

1585− PLam fc n ty' sc'

1587+ PLam fc n nfc ty' sc'

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

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

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

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

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

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

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

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

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

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

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

1594 PLet fc n ty' val' sc'

1596 PLet fc n ty' val' sc'

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

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

1596− ai qq env ds (PPi p n ty sc)

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

1597 = let ty' = ai qq env ds ty

1599 = let ty' = ai qq env ds ty

1598 env' = if n `elem` imp_meths then env

1600 env' = if n `elem` imp_meths then env

1599 else ((n, Just ty) : env)

1601 else ((n, Just ty) : env)

1600 sc' = ai qq env' ds sc in

1602 sc' = ai qq env' ds sc in

1601− PPi p n ty' sc'

1603+ PPi p n nfc ty' sc'

1602 ai qq env ds (PGoal fc r n sc)

1604 ai qq env ds (PGoal fc r n sc)

1603 = let r' = ai qq env ds r

1605 = let r' = ai qq env ds r

1604 sc' = ai qq ((n, Nothing):env) ds sc in

1606 sc' = ai qq ((n, Nothing):env) ds sc in

@@ -1808,8 +1810,8 @@ stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

1808 else PAlternative b alts'

1810 else PAlternative b alts'

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

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

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

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

1811− su t@(PLam fc _ _ _) = PHidden t

1813+ su t@(PLam _ _ _ _ _) = PHidden t

1812− su t@(PPi _ _ _ _) = PHidden t

1814+ su t@(PPi _ _ _ _ _) = PHidden t

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

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

1814 su t = t

1816 su t = t

1815

1817

@@ -1833,7 +1835,7 @@ findStatics :: IState -> PTerm -> (PTerm, [Bool])

1833findStatics ist tm = trace (show tm) $

1835findStatics ist tm = trace (show tm) $

1834 let (ns, ss) = fs tm in

1836 let (ns, ss) = fs tm in

1835 runState (pos ns ss tm) []

1837 runState (pos ns ss tm) []

1836− where fs (PPi p n t sc)

1838+ where fs (PPi p n fc t sc)

1837 | Static <- pstatic p

1839 | Static <- pstatic p

1838 = let (ns, ss) = fs sc in

1840 = let (ns, ss) = fs sc in

1839 (namesIn [] ist t : ns, n : ss)

1841 (namesIn [] ist t : ns, n : ss)

@@ -1843,15 +1845,15 @@ findStatics ist tm = trace (show tm) $

1843

1845

1844 inOne n ns = length (filter id (map (elem n) ns)) == 1

1846 inOne n ns = length (filter id (map (elem n) ns)) == 1

1845

1847

1846− pos ns ss (PPi p n t sc)

1848+ pos ns ss (PPi p n fc t sc)

1847 | elem n ss = do sc' <- pos ns ss sc

1849 | elem n ss = do sc' <- pos ns ss sc

1848 spos <- get

1850 spos <- get

1849 put (True : spos)

1851 put (True : spos)

1850− return (PPi (p { pstatic = Static }) n t sc')

1852+ return (PPi (p { pstatic = Static }) n fc t sc')

1851 | otherwise = do sc' <- pos ns ss sc

1853 | otherwise = do sc' <- pos ns ss sc

1852 spos <- get

1854 spos <- get

1853 put (False : spos)

1855 put (False : spos)

1854− return (PPi p n t sc')

1856+ return (PPi p n fc t sc')

1855 pos ns ss t = return t

1857 pos ns ss t = return t

1856

1858

1857-- for 6.12/7 compatibility

1859-- for 6.12/7 compatibility

@@ -1951,12 +1953,12 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1951 match (PResolveTC _) (PResolveTC _) = return []

1953 match (PResolveTC _) (PResolveTC _) = return []

1952 match (PTrue _ _) (PTrue _ _) = return []

1954 match (PTrue _ _) (PTrue _ _) = return []

1953 match (PReturn _) (PReturn _) = return []

1955 match (PReturn _) (PReturn _) = return []

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

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

1955− ms <- match' s s'

1957+ ms <- match' s s'

1956− return (mt ++ ms)

1958+ return (mt ++ ms)

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

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

1958− ms <- match' s s'

1960+ ms <- match' s s'

1959− return (mt ++ ms)

1961+ return (mt ++ ms)

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

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

1961 mty <- match' ty ty'

1963 mty <- match' ty ty'

1962 ms <- match' s s'

1964 ms <- match' s s'

@@ -2003,13 +2005,13 @@ substMatch n = substMatchShadow n []

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

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

2004substMatchShadow n shs tm t = sm shs t where

2006substMatchShadow n shs tm t = sm shs t where

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

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

2006− sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)

2008+ sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)

2007− sm xs (PPi p x t sc)

2009+ sm xs (PPi p x fc t sc)

2008 | x `elem` xs

2010 | x `elem` xs

2009 = let x' = nextName x in

2011 = let x' = nextName x in

2010− PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))

2012+ PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC x') t))

2011− (sm (x':xs) (substMatch x (PRef emptyFC x') sc))

2013+ (sm (x':xs) (substMatch x (PRef emptyFC x') sc))

2012− | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

2014+ | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)

2013 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2015 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

2014 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2016 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

2015 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2017 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

@@ -2032,10 +2034,10 @@ substMatchShadow n shs tm t = sm shs t where

2032shadow :: Name -> Name -> PTerm -> PTerm

2034shadow :: Name -> Name -> PTerm -> PTerm

2033shadow n n' t = sm t where

2035shadow n n' t = sm t where

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

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

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

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

2036− | otherwise = PLam fc x (sm t) sc

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

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

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

2038− | otherwise = PPi p x (sm t) sc

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

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

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

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

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

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

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

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

2077 mkUniqT tac = return tac

2079 mkUniqT tac = return tac

2078

2080

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

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

2080− mkUniq (PLam fc n ty sc)

2082+ mkUniq (PLam fc n nfc ty sc)

2081 = do env <- get

2083 = do env <- get

2082 (n', sc') <-

2084 (n', sc') <-

2083 if n `S.member` env

2085 if n `S.member` env

@@ -2088,8 +2090,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

2088 put (S.insert n' env)

2090 put (S.insert n' env)

2089 ty' <- mkUniq ty

2091 ty' <- mkUniq ty

2090 sc'' <- mkUniq sc'

2092 sc'' <- mkUniq sc'

2091− return $! PLam fc n' ty' sc''

2093+ return $! PLam fc n' nfc ty' sc''

2092− mkUniq (PPi p n ty sc)

2094+ mkUniq (PPi p n fc ty sc)

2093 = do env <- get

2095 = do env <- get

2094 (n', sc') <-

2096 (n', sc') <-

2095 if n `S.member` env

2097 if n `S.member` env

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

2100 put (S.insert n' env)

2102 put (S.insert n' env)

2101 ty' <- mkUniq ty

2103 ty' <- mkUniq ty

2102 sc'' <- mkUniq sc'

2104 sc'' <- mkUniq sc'

2103− return $! PPi p n' ty' sc''

2105+ return $! PPi p n' fc ty' sc''

2104 mkUniq (PLet fc n ty val sc)

2106 mkUniq (PLet fc n ty val sc)

2105 = do env <- get

2107 = do env <- get

2106 (n', sc') <-

2108 (n', sc') <-

src/Idris/AbsSyntaxTree.hs+30−30

@@ -603,7 +603,7 @@ data PDecl' t

603 | PNamespace String [PDecl' t] -- ^ New namespace

604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts

605 Name -- Record name

606− [(Name, Plicity, t)] -- Parameters

606+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span

607 [(Name, Docstring (Either Err PTerm))] -- Param Docs

608 [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields

609 (Maybe Name) -- Optional constructor name

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

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

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

812 | PPatvar FC Name -- ^ A pattern variable

813− | PLam FC Name PTerm PTerm -- ^ A lambda abstraction

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

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

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

815 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding

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

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

@@ -861,8 +861,8 @@ deriving instance NFData PTerm

861

862mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm

863mapPT f t = f (mpt t) where

864− mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)

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

865− mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

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

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

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

868 (fmap (mapPT f) g)

@@ -1020,8 +1020,8 @@ highestFC (PQuote _) = Nothing

1020highestFC (PRef fc _) = Just fc

1021highestFC (PInferRef fc _) = Just fc

1022highestFC (PPatvar fc _) = Just fc

1023−highestFC (PLam fc _ _ _) = Just fc

1023+highestFC (PLam fc _ _ _ _) = Just fc

1024−highestFC (PPi _ _ _ _) = Nothing

1024+highestFC (PPi _ _ _ _ _) = Nothing

1025highestFC (PLet fc _ _ _ _) = Just fc

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

1027highestFC (PApp fc _ _) = Just fc

@@ -1262,8 +1262,8 @@ inferTy = sMN 0 "__Infer"

1262inferCon = sMN 0 "__infer"

1263inferDecl = PDatadecl inferTy

1264 (PType bi)

1265− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") (PType bi) (

1265+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") NoFC (PType bi) (

1266− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

1266+ PPi expl (sMN 0 "ival") NoFC (PRef bi (sMN 0 "iType"))

1267 (PRef bi inferTy)), bi, [])]

1268inferOpts = []

1269

@@ -1321,8 +1321,8 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

1321 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1322 (PType bi)))

1323 [(reflDoc, reflParamDoc,

1324− eqCon, PPi impl (n "A") (PType bi) (

1324+ eqCon, PPi impl (n "A") NoFC (PType bi) (

1325− PPi impl (n "x") (PRef bi (n "A"))

1325+ PPi impl (n "x") NoFC (PRef bi (n "A"))

1326 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

1327 pimp (n "B") Placeholder False,

1328 pexp (PRef bi (n "x")),

@@ -1356,7 +1356,7 @@ piBind = piBindp expl

1356

1357piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

1358piBindp p [] t = t

1359−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1359+piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)

1360

1361

1362-- Pretty-printing declarations and terms

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

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

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

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

1448− prettySe p bnd (PLam fc n ty sc) =

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

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

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

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

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

1453 bracket p startPrec . group . align $

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

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

1456− prettySe p bnd (PPi (Exp l s _) n ty sc)

1456+ prettySe p bnd (PPi (Exp l s _) n _ ty sc)

1457 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1458 bracket p startPrec . group $

1459 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

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

1466 case s of

1467 Static -> text "[static]" <> space

1468 _ -> empty

1469− prettySe p bnd (PPi (Imp l s _ fa) n ty sc)

1469+ prettySe p bnd (PPi (Imp l s _ fa) n _ ty sc)

1470 | ppopt_impl ppo =

1471 bracket p startPrec $

1472 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

@@ -1477,10 +1477,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1477 case s of

1478 Static -> text "[static]" <> space

1479 _ -> empty

1480− prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1480+ prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =

1481 bracket p startPrec $

1482 prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc

1483− prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1483+ prettySe p bnd (PPi (TacImp _ _ s) n _ ty sc) =

1484 bracket p startPrec $

1485 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

1486 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc

@@ -1866,8 +1866,8 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

1866instance Sized PTerm where

1867 size (PQuote rawTerm) = size rawTerm

1868 size (PRef fc name) = size name

1869− size (PLam fc name ty bdy) = 1 + size ty + size bdy

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

1870− size (PPi plicity name ty bdy) = 1 + size ty + size bdy

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

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

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

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

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

1900 size _ = 0

1901

1902getPArity :: PTerm -> Int

1903−getPArity (PPi _ _ _ sc) = 1 + getPArity sc

1903+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc

1904getPArity _ = 0

1905

1906-- Return all names, free or globally bound, in the given term.

@@ -1915,8 +1915,8 @@ allNamesIn tm = nub $ ni [] tm

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

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

1917 ni env (PIfThenElse _ c t f) = ni env c ++ ni env t ++ ni env f

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

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

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

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

1920 ni env (PHidden tm) = ni env tm

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

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

@@ -1942,9 +1942,9 @@ boundNamesIn tm = S.toList (ni S.empty tm)

1942 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)

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

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

1945− ni set (PLam fc n ty sc) = S.insert n $ ni (ni set ty) sc

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

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

1947− ni set (PPi p n ty sc) = niTacImp (S.insert n $ ni (ni set ty) sc) p

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

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

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

1950 ni set (PTyped l r) = ni (ni set l) r

@@ -1983,8 +1983,8 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

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

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

1985 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

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

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

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

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

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

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

1990 ni env (PTyped l r) = ni env l ++ ni env r

@@ -2014,8 +2014,8 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

2016 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

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

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

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

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

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

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

2021 ni env (PTyped l r) = ni env l ++ ni env r

@@ -2046,8 +2046,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm

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

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

2048 ni env (PIfThenElse _ c t f) = concatMap (ni env) [c, t, f]

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

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

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

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

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

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

2053 ni env (PTyped l r) = ni env l ++ ni env r

src/Idris/CaseSplit.hs+6−6

@@ -346,19 +346,19 @@ getClause l fn fp

346 return (show fn ++ " " ++ ap ++ "= ?"

347 ++ show fn ++ "_rhs")

348 where mkApp :: IState -> PTerm -> [Name] -> String

349− mkApp i (PPi (Exp _ _ False) (MN _ _) ty sc) used

349+ mkApp i (PPi (Exp _ _ False) (MN _ _) _ ty sc) used

350 = let n = getNameFrom i used ty in

351 show n ++ " " ++ mkApp i sc (n : used)

352− mkApp i (PPi (Exp _ _ False) (UN n) ty sc) used

352+ mkApp i (PPi (Exp _ _ False) (UN n) _ ty sc) used

353 | thead n == '_'

354 = let n = getNameFrom i used ty in

355 show n ++ " " ++ mkApp i sc (n : used)

356− mkApp i (PPi (Exp _ _ False) n _ sc) used

356+ mkApp i (PPi (Exp _ _ False) n _ _ sc) used

357 = show n ++ " " ++ mkApp i sc (n : used)

358− mkApp i (PPi _ _ _ sc) used = mkApp i sc used

358+ mkApp i (PPi _ _ _ _ sc) used = mkApp i sc used

359 mkApp i _ _ = ""

360

361− getNameFrom i used (PPi _ _ _ _)

361+ getNameFrom i used (PPi _ _ _ _ _)

362 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used

363 getNameFrom i used (PApp fc f as) = getNameFrom i used f

364 getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom (mkSupply [sUN "prf"]) used

@@ -388,7 +388,7 @@ getProofClause :: Int -- ^ line number that the type is declared

388getProofClause l fn fp

389 = do ty <- getInternalApp fp l

390 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")

391− where mkApp (PPi _ _ _ sc) = mkApp sc

391+ where mkApp (PPi _ _ _ _ sc) = mkApp sc

392 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn

393

394-- Purely syntactic - turn a pattern match clause into a with and a new

src/Idris/DSL.hs+15−15

@@ -45,12 +45,12 @@ mkTTName fc n =

45 otherwise -> PRef fc $ reflm "NErased"

47expandSugar :: DSL -> PTerm -> PTerm

48−expandSugar dsl (PLam fc n ty tm)

48+expandSugar dsl (PLam fc n nfc ty tm)

49 | Just lam <- dsl_lambda dsl

50 = let sc = PApp fc lam [ pexp (mkTTName fc n)

51 , pexp (var dsl n tm 0)]

52 in expandSugar dsl sc

53−expandSugar dsl (PLam fc n ty tm) = PLam fc n (expandSugar dsl ty) (expandSugar dsl tm)

53+expandSugar dsl (PLam fc n nfc ty tm) = PLam fc n nfc (expandSugar dsl ty) (expandSugar dsl tm)

54expandSugar dsl (PLet fc n ty v tm)

55 | Just letb <- dsl_let dsl

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

@@ -58,13 +58,13 @@ expandSugar dsl (PLet fc n ty v tm)

58 , pexp (var dsl n tm 0)]

59 in expandSugar dsl sc

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

61−expandSugar dsl (PPi p n ty tm)

61+expandSugar 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)

64 , pexp ty

65 , pexp (var dsl n tm 0)]

66 in expandSugar dsl sc

67−expandSugar dsl (PPi p n ty tm) = PPi p n (expandSugar dsl ty) (expandSugar dsl tm)

67+expandSugar dsl (PPi p n fc ty tm) = PPi p n fc (expandSugar dsl ty) (expandSugar dsl tm)

68expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)

69 (map (fmap (expandSugar dsl)) args)

70expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)

@@ -98,9 +98,9 @@ expandSugar dsl (PDoBlock ds)

98 block b [DoExp fc tm] = tm

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

100 block b (DoBind fc n tm : rest)

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

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

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

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

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)

@@ -110,7 +110,7 @@ expandSugar dsl (PDoBlock ds)

110 block b (DoExp fc tm : rest)

111 = PApp fc b

112 [pexp tm,

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

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

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

115

116expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

@@ -124,18 +124,18 @@ var dsl n t i = v' i t where

124 case dsl_var dsl of

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

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

127− v' i (PLam fc n ty sc)

127+ v' i (PLam fc n nfc ty sc)

128 | Nothing <- dsl_lambda dsl

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

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

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

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

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

132 | Nothing <- dsl_let dsl

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

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

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

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

136 | Nothing <- dsl_pi dsl

137− = PPi p n (v' i ty) (v' i sc)

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

138− | otherwise = PPi p n (v' i ty) (v' (i+1) sc)

138+ | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)

139 v' i (PTyped l r) = PTyped (v' i l) (v' i r)

140 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)

141 v' i (PCase f t as) = PCase f (v' i t) (fmap (pmap (v' i)) as)

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

190 = do t' <- db' t

191 args' <- mapM dbArg args

192 return (PApp fc t' args')

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

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

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

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

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

215

216 bindAll [] tm = tm

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

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

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

219

220

src/Idris/DeepSeq.hs+3−3

@@ -200,9 +200,9 @@ instance NFData PTerm where

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

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

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

203− rnf (PLam _ x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

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

204− rnf (PPi x1 x2 x3 x4)

204+ rnf (PPi x1 x2 x3 x4 x5)

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

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

206 rnf (PLet _ x1 x2 x3 x4)

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

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

src/Idris/Delaborate.hs+14−14

@@ -61,25 +61,25 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

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

62 _ -> PRef un n

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

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

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

65 de env is (Bind n (Pi (Just impl) ty _) sc)

66 | tcinstance impl

67− = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

67+ = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

68 | otherwise

69− = PPi (Imp [] Dynamic False (Just impl)) n (de env [] ty) (de ((n,n):env) is sc)

69+ = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

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

71+ = PPi (Imp opts Dynamic False Nothing) n NoFC (de env [] ty) (de ((n,n):env) is sc)

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

73− = PPi constraint n (de env [] ty) (de ((n,n):env) is sc)

73+ = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

74 de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi _ ty _) sc)

75− = PPi (tacimpl tac) n (de env [] ty) (de ((n,n):env) is sc)

75+ = PPi (tacimpl tac) n NoFC (de env [] ty) (de ((n,n):env) is sc)

76 de env (plic:is) (Bind n (Pi _ ty _) sc)

77 = PPi (Exp (argopts plic) Dynamic False)

78− n

78+ n NoFC

79 (de env [] ty)

80 (de ((n,n):env) is sc)

81 de env [] (Bind n (Pi _ ty _) sc)

82− = PPi expl n (de env [] ty) (de ((n,n):env) [] sc)

82+ = PPi expl n NoFC (de env [] ty) (de ((n,n):env) [] sc)

84 de env imps (Bind n (Let ty val) sc)

85 | isCaseApp sc

@@ -477,14 +477,14 @@ addImplicitDiffs x y

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

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

479 addShows xs ys = (xs, ys)

480− addI (PLam fc n a b) (PLam fc' n' c d)

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

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

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

483− (PLam fc n a' b', PLam fc' n' c' d')

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

484− addI (PPi p n a b) (PPi p' n' c d)

484+ addI (PPi p n fc a b) (PPi p' n' fc' c d)

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

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

487− (PPi p n a' b', PPi p' n' c' d')

487+ (PPi p n fc a' b', PPi p' n' fc' c' d')

488 addI (PRefl fc a) (PRefl fc' b)

489 = let (a', b') = addI a b in

490 (PRefl fc a', PRefl fc' b')

@@ -528,9 +528,9 @@ addImplicitDiffs x y

528 expLike (PApp _ f as) (PApp _ f' as')

529 = expLike f f' && length as == length as' &&

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

531− expLike (PPi _ n s t) (PPi _ n' s' t')

531+ expLike (PPi _ n fc s t) (PPi _ n' fc' s' t')

532 = n == n' && expLike s s' && expLike t t'

533− expLike (PLam _ n s t) (PLam _ n' s' t')

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

534 = n == n' && expLike s s' && expLike t t'

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

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

src/Idris/Docs.hs+7−7

@@ -163,8 +163,8 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

163 dumpInstance :: PTerm -> Doc OutputAnnotation

164 dumpInstance = pprintPTerm ppo params' [] infixes

165

166− prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

166+ prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm

167− prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

167+ prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2)

168 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args

169 prettifySubclasses tm = tm

170

@@ -178,8 +178,8 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)

178 updateRef nm (PRef fc _) = PRef fc nm

179 updateRef _ pt = pt

180

181− isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'

181+ isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'

182− isSubclass (PPi _ _ _ pt) = isSubclass pt

182+ isSubclass (PPi _ _ _ _ pt) = isSubclass pt

183 isSubclass _ = False

184

185 prettyParameters =

@@ -262,9 +262,9 @@ docClass n ci

262 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t

263 getDInst _ = Nothing

264

265− isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

265+ isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))

266 = nm == n && map getTm args == map getTm args'

267− isSubclass (PPi _ _ _ pt)

267+ isSubclass (PPi _ _ _ _ pt)

268 = isSubclass pt

269 isSubclass _

270 = False

@@ -290,7 +290,7 @@ docFun n

290 funName n = show n

291

292getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]

293−getPArgNames (PPi plicity name ty body) ds =

293+getPArgNames (PPi plicity name _ ty body) ds =

294 (name, ty, plicity, lookup name ds) : getPArgNames body ds

295getPArgNames _ _ = []

296

src/Idris/Elab/Class.hs+14−14

@@ -106,13 +106,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

106 where

107 nodoc (n, (_, o, t)) = (n, (o, t))

108 pibind [] x = x

109− pibind ((n, ty): ns) x = PPi expl n ty (pibind ns (chkUniq ty x))

109+ pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

110

111 -- To make sure the type constructor of the class is in the appropriate

112 -- uniqueness hierarchy

113 chkUniq u@(PUniverse _) (PType _) = u

114 chkUniq (PUniverse l) (PUniverse r) = PUniverse (min l r)

115− chkUniq (PPi _ _ _ sc) t = chkUniq sc t

115+ chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t

116 chkUniq _ t = t

117

118 mdec :: Name -> Name

@@ -134,10 +134,10 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

134

135 impbind :: [(Name, PTerm)] -> PTerm -> PTerm

136 impbind [] x = x

137− impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)

137+ impbind ((n, ty): ns) x = PPi impl n NoFC ty (impbind ns x)

138

139 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

140− conbind ((c, ty) : ns) x = PPi constraint c ty (conbind ns x)

140+ conbind ((c, ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

141 conbind [] x = x

142

143 getMName (PTy _ _ _ _ _ n _) = nsroot n

@@ -181,7 +181,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

181 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

182 let lhs = PApp fc (PRef fc cfn) [pconst capp]

183 let rhs = PResolveTC (fileFC "HACK")

184− let ty = PPi constraint cnm c con

184+ let ty = PPi constraint cnm NoFC c con

185 logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)

186 logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

187 i <- getIState

@@ -213,9 +213,9 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

213 return [PTy doc [] syn fc o m ty',

214 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

215

216− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA n : getMArgs sc

216+ getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc

217− getMArgs (PPi (Exp _ _ _) n ty sc) = EA n : getMArgs sc

217+ getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc

218− getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

218+ getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc

219 getMArgs _ = []

220

221 getMeth (m:ms) (a:as) x | x == a = PRef fc m

@@ -231,16 +231,16 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

231 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

232 rhsArgs [] _ = []

233

234− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

234+ insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)

235− = PPi p n ty (insertConstraint c sc)

235+ = PPi p n fc ty (insertConstraint c sc)

236 insertConstraint c sc = PPi (constraint { pstatic = Static })

237− (sMN 0 "class") c sc

237+ (sMN 0 "class") NoFC c sc

238

239 -- make arguments explicit and don't bind class parameters

240− toExp ns e (PPi (Imp l s p _) n ty sc)

240+ toExp ns e (PPi (Imp l s p _) n fc ty sc)

241 | n `elem` ns = toExp ns e sc

242− | otherwise = PPi (e l s p) n ty (toExp ns e sc)

242+ | otherwise = PPi (e l s p) n fc ty (toExp ns e sc)

243− toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

243+ toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

244 toExp ns e sc = sc

245

246-- In a top level type for a method, expand all the method names namespaces

src/Idris/Elab/Data.hs+9−9

@@ -251,13 +251,13 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

251 else return ()

252 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))

253

254− mkLazy (PPi pl n ty sc)

254+ mkLazy (PPi pl n nfc ty sc)

255 = let ty' = if getTyName ty

256 then PApp fc (PRef fc (sUN "Lazy'"))

257 [pexp (PRef fc (sUN "LazyCodata")),

258 pexp ty]

259 else ty in

260− PPi pl n ty' (mkLazy sc)

260+ PPi pl n nfc ty' (mkLazy sc)

261 mkLazy t = t

262

263 getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

@@ -266,8 +266,8 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, t_in, fc, forcenames)

266

267

268 getNamePos :: Int -> PTerm -> Name -> Maybe Int

269− getNamePos i (PPi _ n _ sc) x | n == x = Just i

269+ getNamePos i (PPi _ n _ _ sc) x | n == x = Just i

270− | otherwise = getNamePos (i + 1) sc x

270+ | otherwise = getNamePos (i + 1) sc x

271 getNamePos _ _ _ = Nothing

272

273 -- if the constructor is a UniqueType, the datatype must be too

@@ -353,8 +353,8 @@ elabCaseFun ind paramPos n ty cons info = do

353 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)

354 splitPi = splitPi' []

355 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)

356− splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr

356+ splitPi' acc (PPi pl n _ tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr

357− splitPi' acc t = (reverse acc, t)

357+ splitPi' acc t = (reverse acc, t)

358

359 splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])

360 splitPms cnstrs = (map fst pms, map fst idxs)

@@ -418,7 +418,7 @@ elabCaseFun ind paramPos n ty cons info = do

418

419 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

420 piConstr [] ty = ty

421− piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)

421+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n NoFC tyb (piConstr tyr ty)

422

423 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]

424 interlievePos idxs [] l2 i = l2

@@ -436,9 +436,9 @@ elabCaseFun ind paramPos n ty cons info = do

436 _ -> cns

437

438 removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm

439− removeParamPis oldParams params (PPi pl n tyb tyr) =

439+ removeParamPis oldParams params (PPi pl n fc tyb tyr) =

440 case findIndex (== n) oldParams of

441− Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))

441+ Nothing -> (PPi pl n fc (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))

442 Just i -> (removeParamPis oldParams params tyr)

443 removeParamPis oldParams params (PRef _ n) =

444 case findIndex (== n) oldParams of

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

@@ -201,7 +201,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

201 _ -> Nothing

202 overlapping t' = tclift $ tfail (At fc (Msg $

203 "Overlapping instance: " ++ show t' ++ " already defined"))

204− getRetType (PPi _ _ _ sc) = getRetType sc

204+ getRetType (PPi _ _ _ _ sc) = getRetType sc

205 getRetType t = t

206

207 matchArgs i dets x y =

@@ -216,16 +216,16 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

216

217 mkMethApp (n, _, _, ty)

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

219− lamBind i (PPi (Constraint _ _) _ _ sc) sc'

219+ lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

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

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

221− lamBind i (PPi _ n ty sc) sc'

221+ lamBind i (PPi _ n _ ty sc) sc'

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

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

223 lamBind i _ sc = sc

224− methArgs i (PPi (Imp _ _ _ _) n ty sc)

224+ methArgs i (PPi (Imp _ _ _ _) n _ ty sc)

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

226− methArgs i (PPi (Exp _ _ _) n ty sc)

226+ methArgs i (PPi (Exp _ _ _) n _ ty sc)

227 = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

228− methArgs i (PPi (Constraint _ _) n ty sc)

228+ methArgs i (PPi (Constraint _ _) n _ ty sc)

229 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc

230 methArgs i _ = []

231

@@ -250,11 +250,11 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

250 (mkUniqueNames [] t)

251

252 conbind :: [(Name, PTerm)] -> PTerm -> PTerm

253− conbind ((c,ty) : ns) x = PPi constraint c ty (conbind ns x)

253+ conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

254 conbind [] x = x

255

256 coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

257− coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

257+ coninsert cs (PPi p@(Imp _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)

258 coninsert cs sc = conbind cs sc

259

260 -- Reorder declarations to be in the same order as defined in the

src/Idris/Elab/Record.hs+20−20

@@ -37,7 +37,7 @@ elabRecord :: ElabInfo

37 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

38 -> SyntaxInfo -> FC -> DataOpts

39 -> Name -- ^ The name of the type being defined

40− -> [(Name, Plicity, PTerm)] -- ^ Parameters

40+ -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters

41 -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs

42 -> [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields

43 -> Maybe Name -- ^ Constructor Name

@@ -51,7 +51,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

51 logLvl 1 $ "Type constructor " ++ showTmImpls tycon

53 -- Data constructor

54− dconName <- generateDConName cname

54+ dconName <- generateDConName cname

55 let dconTy = generateDConType params fieldsWithNameAndDoc

56 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy

@@ -62,11 +62,11 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

63 iLOG $ "fieldsWithName " ++ show fieldsWithName

64 iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

65− elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

65+ elabRecordFunctions info rsyn fc tyn [(n, p, t, d) | (n, _, p, t, d) <- paramsAndDoc] fieldsWithNameAndDoc dconName target

66 where

67 -- | Generates a type constructor.

68− generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm

68+ generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm

69− generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)

69+ generateTyConType ((n, nfc, p, t) : rest) = PPi p (nsroot n) nfc t (generateTyConType rest)

70 generateTyConType [] = (PType fc)

72 -- | Generates a name for the data constructor if none was specified.

@@ -81,24 +81,24 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

81 Nothing -> return n

83 -- | Generates the data constructor type.

84− generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm

84+ generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm

85− generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)

85+ generateDConType ((n, nfc, _, t) : ps) as = PPi impl (nsroot n) NoFC t (generateDConType ps as)

86− generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) t (generateDConType [] as)

86+ generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) NoFC t (generateDConType [] as)

87 generateDConType [] [] = target

89 -- | The target for the constructor and projection functions. Also the source of the update functions.

90 target :: PTerm

91− target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, _) <- params]

91+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, _, p, _) <- params]

93− paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]

93+ paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]

94 paramsAndDoc = pad params paramDocs

95 where

96− pad :: [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]

96+ pad :: [(Name, FC, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]

97− pad ((n, p, t) : rest) docs

97+ pad ((n, fc, p, t) : rest) docs

98 = let d = case lookup n docs of

99 Just d' -> d

100 Nothing -> emptyDocstring

101− in (n, p, t, d) : (pad rest docs)

101+ in (n, fc, p, t, d) : (pad rest docs)

102 pad _ _ = []

103

104 dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]

@@ -149,7 +149,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

149 iLOG $ "Fields: " ++ show fieldNames

150 iLOG $ "Params: " ++ show paramNames

151 -- The elaborated constructor type for the data declaration

152− i <- getIState

152+ i <- getIState

153 ttConsTy <-

154 case lookupTyExact dconName (tt_ctxt i) of

155 Just as -> return as

@@ -238,7 +238,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

238 paramName (UN n) = sUN ("param_" ++ str n)

239 paramName (MN i n) = sMN i ("param_" ++ str n)

240 paramName (NS n s) = NS (paramName n) s

241− paramName n = n

241+ paramName n = n

242

243 -- | Elaborate the projection functions.

244 elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()

@@ -264,14 +264,14 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target

264 -- | A map from a field name to the other fields it depends on.

265 fieldDependencies :: [(Name, [Name])]

266 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]

267− where

267+ where

268 fieldDep :: Name -> PTerm -> (Name, [Name])

269 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)

270

271 -- | A list of fields depending on another field.

272 dependentFields :: [Name]

273 dependentFields = filter depends fieldNames

274− where

274+ where

275 depends :: Name -> Bool

276 depends n = case lookup n fieldDependencies of

277 Just xs -> not $ null xs

@@ -313,7 +313,7 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

313 where

314 -- | The type of the projection function.

315 generateTy :: PDecl

316− generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName targetTy projTy

316+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName NoFC targetTy projTy

317

318 -- | The left hand side of the projection function.

319 generateLhs :: PTerm

@@ -373,9 +373,9 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

373 then logLvl 1 $ "Could not generate update function for " ++ show pname

374 else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}

375 where

376− -- | The type of the udpate function.

376+ -- | The type of the update function.

377 generateTy :: PDecl

378− generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) pty (PPi expl recName sty (substInput sty))

378+ generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) NoFC pty (PPi expl recName NoFC sty (substInput sty))

379 where substInput = substMatches [(cname, PRef fc (nsroot pname))]

380

381 -- | The "_set" name.

src/Idris/Elab/Term.hs+18−11

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

418 _ -> asType

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

420 [pexp t,

421+ -- TODO: save the FC from the dependent pair

422+ -- syntax and put it on this lambda for interactive

423+ -- semantic highlighting support. NoFC for now.

421− pexp (PLam fc n Placeholder r)])

424+ pexp (PLam fc n NoFC Placeholder r)])

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

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

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

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

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

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

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

514 solve

517 solve

515 highlightSource fc hl

518 highlightSource fc hl

516 else elab' ina fc' (PApp fc tm [])

519 else elab' ina fc' (PApp fc tm [])

517− elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

520+ elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

518− elab' ina _ (PLam fc n Placeholder sc)

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

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

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

520 ctxt <- get_context

523 ctxt <- get_context

521 when (isTConName n ctxt) $

524 when (isTConName n ctxt) $

@@ -524,7 +527,8 @@ elab ist info emode opts fn tm

524 attack; intro (Just n);

527 attack; intro (Just n);

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

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

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

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

530+ highlightSource nfc (AnnBoundName n False)

527− elab' ec _ (PLam fc n ty sc)

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

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

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

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

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

530 ctxt <- get_context

534 ctxt <- get_context

@@ -542,11 +546,13 @@ elab ist info emode opts fn tm

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

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

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

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

544 solve

548 solve

549+ highlightSource nfc (AnnBoundName n False)

545− elab' ina fc (PPi p n Placeholder sc)

550+ elab' ina fc (PPi p n nfc Placeholder sc)

546− = do attack; arg n (is_scoped p) (sMN 0 "ty")

551+ = do attack; arg n (is_scoped p) (sMN 0 "ty")

547 elabE (ina { e_inarg = True, e_intype = True }) fc sc

552 elabE (ina { e_inarg = True, e_intype = True }) fc sc

548 solve

553 solve

554+ highlightSource nfc (AnnBoundName n False)

549− elab' ina fc (PPi p n ty sc)

555+ elab' ina fc (PPi p n nfc ty sc)

550 = do attack; tyn <- getNameFrom (sMN 0 "ty")

556 = do attack; tyn <- getNameFrom (sMN 0 "ty")

551 claim tyn RType

557 claim tyn RType

552 n' <- case n of

558 n' <- case n of

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

558 elabE ec' fc ty

564 elabE ec' fc ty

559 elabE ec' fc sc

565 elabE ec' fc sc

560 solve

566 solve

567+ highlightSource nfc (AnnBoundName n False)

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

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

562 = do attack

569 = do attack

563 ivs <- get_instances

570 ivs <- get_instances

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

793 PAlternative False _ -> 5

800 PAlternative False _ -> 5

794 PAlternative True _ -> 2

801 PAlternative True _ -> 2

795 PTactics _ -> 150

802 PTactics _ -> 150

796− PLam _ _ _ _ -> 3

803+ PLam _ _ _ _ _ -> 3

797 PRewrite _ _ _ _ -> 4

804 PRewrite _ _ _ _ -> 4

798 PResolveTC _ -> 0

805 PResolveTC _ -> 0

799 PHidden _ -> 150

806 PHidden _ -> 150

@@ -1254,9 +1261,9 @@ elab ist info emode opts fn tm

1254 do impn <- unique_hole (sMN 0 "imp")

1261 do impn <- unique_hole (sMN 0 "imp")

1255 if e_isfn ina -- apply to an implicit immediately

1262 if e_isfn ina -- apply to an implicit immediately

1256 then return (PApp emptyFC

1263 then return (PApp emptyFC

1257− (PLam emptyFC impn Placeholder t)

1264+ (PLam emptyFC impn NoFC Placeholder t)

1258 [pexp Placeholder])

1265 [pexp Placeholder])

1259− else return (PLam emptyFC impn Placeholder t)

1266+ else return (PLam emptyFC impn NoFC Placeholder t)

1260 addLam _ t = return t

1267 addLam _ t = return t

1261

1268

1262 insertCoerce ina t@(PCase _ _ _) = return t

1269 insertCoerce ina t@(PCase _ _ _) = return t

@@ -1390,7 +1397,7 @@ pruneByType env (P _ n _) ctxt as

1390 where

1397 where

1391 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1398 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1392 headIs var f (PApp _ f' _) = headIs var f f'

1399 headIs var f (PApp _ f' _) = headIs var f f'

1393− headIs var f (PPi _ _ _ sc) = headIs var f sc

1400+ headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1394 headIs var f (PHidden t) = headIs var f t

1401 headIs var f (PHidden t) = headIs var f t

1395 headIs _ _ _ = True -- keep if it's not an application

1402 headIs _ _ _ = True -- keep if it's not an application

1396

1403

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

@@ -203,8 +203,8 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

203 -- for making an internalapp, we only want the explicit ones, and don't

204 -- want the parameters, so just take the arguments which correspond to the

205 -- user declared explicit ones

206− mergeTy (PPi e n ty sc) (PPi e' n' _ sc')

206+ mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')

207− | e == e' = PPi e n ty (mergeTy sc sc')

207+ | e == e' = PPi e n fc ty (mergeTy sc sc')

208 | otherwise = mergeTy sc sc'

209 mergeTy _ sc = sc

210

src/Idris/Elab/Utils.hs+6−6

@@ -66,9 +66,9 @@ inaccessibleImps _ _ _ = []

67-- | Get the list of (index, name) of inaccessible arguments from the type.

68inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

69−inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

69+inaccessibleArgs i (PPi (Imp _ _ _ _) n _ Placeholder t)

70 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

71−inaccessibleArgs i (PPi plicity n ty t)

71+inaccessibleArgs i (PPi plicity n _ ty t)

72 | InaccessibleArg `elem` pargopts plicity

73 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}

74 | otherwise

@@ -117,7 +117,7 @@ inferredDiff fc inf user =

117-- found, or it will give spurious errors.

118checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()

119checkDocs fc args tm = cd (Map.fromList args) tm

120− where cd as (PPi _ n _ sc) = cd (Map.delete n as) sc

120+ where cd as (PPi _ n _ _ sc) = cd (Map.delete n as) sc

121 cd as _ | Map.null as = return ()

122 | otherwise = ierror . At fc . Msg $

123 "There is documentation for argument(s) "

@@ -277,9 +277,9 @@ mkStatic ns (PTy doc argdocs syn fc o n ty)

277mkStatic ns t = t

278

279mkStaticTy :: [Name] -> PTerm -> PTerm

280−mkStaticTy ns (PPi p n ty sc)

280+mkStaticTy ns (PPi p n fc ty sc)

281− | n `elem` ns = PPi (p { pstatic = Static }) n ty (mkStaticTy ns sc)

281+ | n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)

282− | otherwise = PPi p n ty (mkStaticTy ns sc)

282+ | otherwise = PPi p n fc ty (mkStaticTy ns sc)

283mkStaticTy ns t = t

284

285

src/Idris/ElabQuasiquote.hs+4−4

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

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

74−extractUnquotes n (PLam fc name ty body)

74+extractUnquotes n (PLam fc name nfc ty body)

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

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

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

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

78−extractUnquotes n (PPi plicity name ty body)

78+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 ty' body', ex1 ++ ex2)

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

82extractUnquotes n (PLet fc name ty val body)

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

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

src/Idris/Error.hs+2−2

@@ -91,8 +91,8 @@ warnDisamb ist (PQuote _) = return ()

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

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

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

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

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

95−warnDisamb ist (PPi _ _ t b) = warnDisamb ist t >> warnDisamb ist b

95+warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

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

src/Idris/IBC.hs+16−12

@@ -1500,16 +1500,18 @@ instance Binary PTerm where

1500 PPatvar x1 x2 -> do putWord8 3

1501 put x1

1502 put x2

1503− PLam x1 x2 x3 x4 -> do putWord8 4

1503+ PLam x1 x2 x3 x4 x5 -> do putWord8 4

1504− put x1

1504+ put x1

1505− put x2

1505+ put x2

1506− put x3

1506+ put x3

1507− put x4

1507+ put x4

1508+ put x5

1508− PPi x1 x2 x3 x4 -> do putWord8 5

1509+ PPi x1 x2 x3 x4 x5 -> do putWord8 5

1509− put x1

1510+ put x1

1510− put x2

1511+ put x2

1511− put x3

1512+ put x3

1512− put x4

1513+ put x4

1514+ put x5

1513 PLet x1 x2 x3 x4 x5 -> do putWord8 6

1515 PLet x1 x2 x3 x4 x5 -> do putWord8 6

1514 put x1

1516 put x1

1515 put x2

1517 put x2

@@ -1646,12 +1648,14 @@ instance Binary PTerm where

1646 x2 <- get

1648 x2 <- get

1647 x3 <- get

1649 x3 <- get

1648 x4 <- get

1650 x4 <- get

1651+ x5 <- get

1649− return (PLam x1 x2 x3 x4)

1652+ return (PLam x1 x2 x3 x4 x5)

1650 5 -> do x1 <- get

1653 5 -> do x1 <- get

1651 x2 <- get

1654 x2 <- get

1652 x3 <- get

1655 x3 <- get

1653 x4 <- get

1656 x4 <- get

1657+ x5 <- get

1654− return (PPi x1 x2 x3 x4)

1658+ return (PPi x1 x2 x3 x4 x5)

1655 6 -> do x1 <- get

1659 6 -> do x1 <- get

1656 x2 <- get

1660 x2 <- get

1657 x3 <- get

1661 x3 <- get

src/Idris/IdrisDoc.hs+2−2

@@ -291,8 +291,8 @@ extractPTermNames :: PTerm -- ^ Where to extract names from

291extractPTermNames (PRef _ n) = [n]

292extractPTermNames (PInferRef _ n) = [n]

293extractPTermNames (PPatvar _ n) = [n]

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

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

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

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

296extractPTermNames (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

src/Idris/Interactive.hs+5−5

@@ -197,9 +197,9 @@ doProofSearch fn updatefile rec l n hints (Just depth)

197 runIO $ copyFile fb fn

198 else iPrintResult newmv

199 where dropCtxt 0 sc = sc

200− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc

200+ dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc

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

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

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

203 dropCtxt _ t = t

204

205 stripNS tm = mapPT dens tm where

@@ -304,11 +304,11 @@ makeLemma fn updatefile l n

304 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

305 appArgs skip i _ = ""

306

307− stripMNBind skip (PPi b n@(UN c) ty sc)

307+ stripMNBind skip (PPi b n@(UN c) _ ty sc)

308 | (thead c /= '_' && n `notElem` skip) ||

309 take 4 (str c) == "__pi" -- keep in type, but not in app

310− = PPi b n ty (stripMNBind skip sc)

310+ = PPi b n NoFC ty (stripMNBind skip sc)

311− stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc

311+ stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc

312 stripMNBind skip t = t

313

314 -- Guess which binders should be implicits in the generated lemma.

src/Idris/ParseData.hs+16−16

@@ -64,10 +64,10 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

64 Nothing -> return ()

65 return $ PRecord doc rsyn fc opts tyn params paramDocs fields cname cdoc syn

66 <?> "record type declaration"

67− where

67+ where

68 getRecNames :: SyntaxInfo -> PTerm -> [Name]

69− getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

69+ getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]

70− ++ getRecNames syn sc

70+ ++ getRecNames syn sc

71 getRecNames _ _ = []

73 toFreeze :: Maybe Accessibility -> Maybe Accessibility

@@ -117,28 +117,28 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

117 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

118 annotate syn ist = annotCode $ tryFullExpr syn ist

119

120−recordParameter :: SyntaxInfo -> IdrisParser (Name, Plicity, PTerm)

120+recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)

121recordParameter syn =

122 (do lchar '('

123− (n, pt) <- (namedTy syn <|> onlyName syn)

123+ (n, nfc, pt) <- (namedTy syn <|> onlyName syn)

124 lchar ')'

125− return (n, expl, pt))

125+ return (n, nfc, expl, pt))

126 <|>

127− (do (n, pt) <- onlyName syn

127+ (do (n, nfc, pt) <- onlyName syn

128− return (n, expl, pt))

128+ return (n, nfc, expl, pt))

129−

129+

130 where

131− namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)

131+ namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)

132 namedTy syn =

133− do n <- fst <$> fnName

133+ do (n, nfc) <- fnName

134 lchar ':'

135 ty <- typeExpr (allowImp syn)

136− return (expandNS syn n, ty)

136+ return (expandNS syn n, nfc, ty)

137− onlyName :: SyntaxInfo -> IdrisParser (Name, PTerm)

137+ onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)

138 onlyName syn =

139− do n <- fst <$> fnName

139+ do (n, nfc) <- fnName

140 fc <- getFC

141− return (expandNS syn n, PType fc)

141+ return (expandNS syn n, nfc, PType fc)

142

143{- | Parses data declaration type (normal or codata)

144DataI ::= 'data' | 'codata';

@@ -230,7 +230,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

230 mkPApp fc t [] = t

231 mkPApp fc t xs = PApp fc t (map pexp xs)

232 bindArgs :: [PTerm] -> PTerm -> PTerm

233− bindArgs xs t = foldr (PPi expl (sMN 0 "_t")) t xs

233+ bindArgs xs t = foldr (PPi expl (sMN 0 "_t") NoFC) t xs

234 combineDataOpts :: DataOpts -> DataOpts

235 combineDataOpts opts = if Codata `elem` opts

236 then delete DefaultEliminator opts

src/Idris/ParseExpr.hs+28−28

@@ -164,10 +164,10 @@ extension syn ns rules =

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

165 Just (SynTm t) -> t

166 _ -> PRef fc n

167− update ns (PLam fc n ty sc)

167+ update ns (PLam fc n nfc ty sc)

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

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

169− update ns (PPi p n ty sc)

169+ update ns (PPi p n fc ty sc)

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

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)

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

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

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

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

405 then fail "minus not allowed in section"

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

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

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

408 pexp e]))

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

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

413 fc0 <- getFC

414 case op of

415 Nothing -> bracketedExpr syn l

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

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

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

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

419 <|> do l <- expr syn

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

688 Left fields ->

689 case rec of

690 Nothing ->

691− return (PLam fc (sMN 0 "fldx") Placeholder

691+ return (PLam fc (sMN 0 "fldx") NoFC Placeholder

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

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

694 Right fields ->

695 case rec of

696 Nothing ->

697− return (PLam fc (sMN 0 "fldx") Placeholder

697+ return (PLam fc (sMN 0 "fldx") NoFC Placeholder

698 (getAll fc (reverse fields)

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

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

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

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

792 pmList [] sc = sc

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

794− = PLam fc (sMN i "lamp") Placeholder

794+ = PLam fc (sMN i "lamp") NoFC Placeholder

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

796 [(x, pmList xs sc)])

797 lambdaTail :: IdrisParser PTerm

@@ -946,7 +946,7 @@ normalImplicit opts st syn = do

946 return (bindList (PPi im) xt

947 (bindList (PPi cl) cs sc))

948

949−implicitPi opts st syn =

949+implicitPi opts st syn =

950 autoImplicit opts st syn

951 <|> defaultImplicit opts st syn

952 <|> normalImplicit opts st syn

@@ -955,7 +955,7 @@ unboundPi opts st syn = do

955 x <- opExpr syn

956 (do binder <- bindsymbol opts st syn

957 sc <- expr syn

958− return (PPi binder (sUN "__pi_arg") x sc))

958+ return (PPi binder (sUN "__pi_arg") NoFC x sc))

959 <|> return x

960

961pi :: SyntaxInfo -> IdrisParser PTerm

@@ -987,11 +987,11 @@ ConstraintList ::=

987 ;

988@

989-}

990−constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

990+constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

991constraintList syn = try (constraintList1 syn)

992 <|> return []

993

994−constraintList1 :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

994+constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

995constraintList1 syn = try (do lchar '('

996 tys <- sepBy1 nexpr (lchar ',')

997 lchar ')'

@@ -999,13 +999,13 @@ constraintList1 syn = try (do lchar '('

999 return tys)

1000 <|> try (do t <- opExpr (disallowImp syn)

1001 reservedOp "=>"

1002− return [(defname, t)])

1002+ return [(defname, NoFC, t)])

1003 <?> "type constraint list"

1004− where nexpr = try (do n <- fst <$> name; lchar ':'

1004+ where nexpr = try (do (n, fc) <- name; lchar ':'

1005 e <- expr syn

1006− return (n, e))

1006+ return (n, fc, e))

1007 <|> do e <- expr syn

1008− return (defname, e)

1008+ return (defname, NoFC, e)

1009 defname = sMN 0 "constrarg"

1010

1011{- | Parses a type declaration list

@@ -1023,16 +1023,16 @@ FunctionSignatureList ::=

1023 ;

1024@

1025-}

1026−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

1026+typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1027−typeDeclList syn = try (sepBy1 (do x <- fst <$> fnName

1027+typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName

1028 lchar ':'

1029 t <- typeExpr (disallowImp syn)

1030− return (x,t))

1030+ return (x, xfc, t))

1031 (lchar ','))

1032− <|> do ns <- sepBy1 (fst <$> name) (lchar ',')

1032+ <|> do ns <- sepBy1 name (lchar ',')

1033 lchar ':'

1034 t <- typeExpr (disallowImp syn)

1035− return (map (\x -> (x, t)) ns)

1035+ return (map (\(x, xfc) -> (x, xfc, t)) ns)

1036 <?> "type declaration list"

1037

1038{- | Parses a type declaration list with optional parameters

@@ -1047,17 +1047,17 @@ TypeOptDeclList ::=

1047NameOrPlaceHolder ::= Name | '_';

1048@

1049-}

1050−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

1050+tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]

1051−tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder

1051+tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder

1052 t <- option Placeholder (do lchar ':'

1053 expr syn)

1054− return (x,t))

1054+ return (x, fc, t))

1055 (lchar ',')

1056 <?> "type declaration list"

1057− where nameOrPlaceholder :: IdrisParser Name

1057+ where nameOrPlaceholder :: IdrisParser (Name, FC)

1058− nameOrPlaceholder = fst <$> fnName

1058+ nameOrPlaceholder = fnName

1059 <|> do symbol "_"

1060− return (sMN 0 "underscore")

1060+ return (sMN 0 "underscore", NoFC)

1061 <?> "name or placeholder"

1062

1063{- | Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ]

src/Idris/ParseHelpers.hs+3−3

@@ -402,9 +402,9 @@ getFC = do s <- position

402

403{-* Syntax helpers-}

404-- | Bind constraints to term

405−bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm

405+bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm

406−bindList b [] sc = sc

406+bindList b [] sc = sc

407−bindList b ((n, t):bs) sc = b n t (bindList b bs sc)

407+bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

408

409{- * Layout helpers -}

410

src/Idris/Parser.hs+13−10

@@ -310,20 +310,20 @@ syntaxRule syn

310 return $ PRef fc n'

311 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =

312 return $ PPatvar fc n'

313− fixBind rens (PLam fc n ty body)

313+ fixBind rens (PLam fc n nfc ty body)

314− | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)

314+ | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)

315 | otherwise =

316 do ty' <- fixBind rens ty

317 n' <- gensym n

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

319− return $ PLam fc n' ty' body'

319+ return $ PLam fc n' nfc ty' body'

320− fixBind rens (PPi plic n argTy body)

320+ fixBind rens (PPi plic n nfc argTy body)

321− | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)

321+ | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)

322 | otherwise =

323 do ty' <- fixBind rens argTy

324 n' <- gensym n

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

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

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

327 fixBind rens (PLet fc n ty val body)

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

329 (fixBind rens ty)

@@ -555,12 +555,13 @@ Params ::=

555params :: SyntaxInfo -> IdrisParser [PDecl]

556params syn =

557 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'

558+ let ns' = [(n, ty) | (n, _, ty) <- ns]

558 openBlock

559 openBlock

559 let pvars = syn_params syn

560 let pvars = syn_params syn

560− ds <- many (decl syn { syn_params = pvars ++ ns })

561+ ds <- many (decl syn { syn_params = pvars ++ ns' })

561 closeBlock

562 closeBlock

562 fc <- getFC

563 fc <- getFC

563− return [PParams fc ns (concat ds)]

564+ return [PParams fc ns' (concat ds)]

564 <?> "parameters declaration"

565 <?> "parameters declaration"

565

566

566{- | Parses a mutual declaration (for mutually recursive functions)

567{- | Parses a mutual declaration (for mutually recursive functions)

@@ -659,13 +660,14 @@ class_ syn = do (doc, argDocs, acc)

659 return (doc, argDocs, acc))

660 return (doc, argDocs, acc))

660 fc <- getFC

661 fc <- getFC

661 cons <- constraintList syn

662 cons <- constraintList syn

663+ let cons' = [(c, ty) | (c, _, ty) <- cons]

662 n_in <- fst <$> fnName

664 n_in <- fst <$> fnName

663 let n = expandNS syn n_in

665 let n = expandNS syn n_in

664 cs <- many carg

666 cs <- many carg

665 fds <- option (map fst cs) fundeps

667 fds <- option (map fst cs) fundeps

666 ds <- option [] (classBlock syn)

668 ds <- option [] (classBlock syn)

667 accData acc n (concatMap declared ds)

669 accData acc n (concatMap declared ds)

668− return [PClass doc syn fc cons n cs argDocs fds ds]

670+ return [PClass doc syn fc cons' n cs argDocs fds ds]

669 <?> "type-class declaration"

671 <?> "type-class declaration"

670 where

672 where

671 fundeps :: IdrisParser [Name]

673 fundeps :: IdrisParser [Name]

@@ -696,12 +698,13 @@ instance_ syn = do (doc, argDocs)

696 fc <- getFC

698 fc <- getFC

697 en <- optional instanceName

699 en <- optional instanceName

698 cs <- constraintList syn

700 cs <- constraintList syn

701+ let cs' = [(c, ty) | (c, _, ty) <- cs]

699 cn <- fst <$> fnName

702 cn <- fst <$> fnName

700 args <- many (simpleExpr syn)

703 args <- many (simpleExpr syn)

701 let sc = PApp fc (PRef fc cn) (map pexp args)

704 let sc = PApp fc (PRef fc cn) (map pexp args)

702 let t = bindList (PPi constraint) cs sc

705 let t = bindList (PPi constraint) cs sc

703 ds <- option [] (instanceBlock syn)

706 ds <- option [] (instanceBlock syn)

704− return [PInstance doc argDocs syn fc cs cn args t en ds]

707+ return [PInstance doc argDocs syn fc cs' cn args t en ds]

705 <?> "instance declaration"

708 <?> "instance declaration"

706 where instanceName :: IdrisParser Name

709 where instanceName :: IdrisParser Name

707 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

710 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

src/Idris/PartialEval.hs+3−3

@@ -128,12 +128,12 @@ mkPE_TyDecl :: IState -> [(PEArgType, Term)] -> Type -> PTerm

128mkPE_TyDecl ist args ty = mkty args ty

129 where

130 mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

131− = PPi expl n (delab ist (generaliseIn t)) (mkty xs sc)

131+ = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

132 mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

133 | concreteClass ist t = mkty xs sc

134 | classConstraint ist t

135− = PPi constraint n (delab ist (generaliseIn t)) (mkty xs sc)

135+ = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

136− | otherwise = PPi impl n (delab ist (generaliseIn t)) (mkty xs sc)

136+ | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

137

138 mkty (_ : xs) t

139 = mkty xs t

src/Idris/REPL.hs+1−1

@@ -906,7 +906,7 @@ process fn (Check (PRef _ n))

906 (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

907 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

908 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

909− putTy ppo ist i bnd (PPi _ n t sc)

909+ putTy ppo ist i bnd (PPi _ n _ t sc)

910 = let current = text " " <>

911 (case n of

912 MN _ _ -> text "_"