git.iko.soy/Idris-dev
on master help sign in
Highlight pi and lambda binders
commit689e64bca864b9d1b34f3a6e608b36fb7077e92c authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 10 May 2015, 22:45 (11 years ago) parentc42673c
25 files changed+306−290
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+59−57 src/Idris/AbsSyntaxTree.hs+30−30 src/Idris/CaseSplit.hs+6−6 src/Idris/DSL.hs+15−15 src/Idris/DeepSeq.hs+3−3 src/Idris/Delaborate.hs+14−14 src/Idris/Docs.hs+7−7 src/Idris/Elab/Class.hs+14−14 src/Idris/Elab/Data.hs+9−9 src/Idris/Elab/Instance.hs+10−10 src/Idris/Elab/Record.hs+20−20 src/Idris/Elab/Term.hs+18−11 src/Idris/Elab/Type.hs+2−2 src/Idris/Elab/Utils.hs+6−6 src/Idris/ElabQuasiquote.hs+4−4 src/Idris/Error.hs+2−2 src/Idris/IBC.hs+16−12 src/Idris/IdrisDoc.hs+2−2 src/Idris/Interactive.hs+5−5 src/Idris/ParseData.hs+16−16 src/Idris/ParseExpr.hs+28−28 src/Idris/ParseHelpers.hs+3−3 src/Idris/Parser.hs+13−10 src/Idris/PartialEval.hs+3−3 src/Idris/REPL.hs+1−1
src/Idris/AbsSyntax.hs+59−57
@@ -952,16 +952,16 @@ expandParams dec ps ns infs tm = en tm
952952 mkShadow (MN i n) = MN (i+1) n
953953 mkShadow (NS x s) = NS (mkShadow x) s
954954
955− en (PLam fc n t s)
955+ en (PLam fc n nfc t s)
956956 | n `elem` (map fst ps ++ ns)
957957 = let n' = mkShadow n in
958− PLam fc n' (en t) (en (shadow n n' s))
959− | otherwise = PLam fc n (en t) (en s)
960− en (PPi p n t s)
958+ PLam fc n' nfc (en t) (en (shadow n n' s))
959+ | otherwise = PLam fc n nfc (en t) (en s)
960+ en (PPi p n nfc t s)
961961 | n `elem` (map fst ps ++ ns)
962962 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
963− PPi (enTacImp p) n' (en t) (en (shadow n n' s))
964− | otherwise = PPi (enTacImp p) n (en t) (en s)
963+ PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))
964+ | otherwise = PPi (enTacImp p) n nfc (en t) (en s)
965965 en (PLet fc n ty v s)
966966 | n `elem` (map fst ps ++ ns)
967967 = let n' = mkShadow n in
@@ -1136,7 +1136,7 @@ getPriority i tm = 1 -- pri tm
11361136 ((P (TCon _ _) _ _):_) -> 1
11371137 ((P Ref _ _):_) -> 1
11381138 [] -> 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))
11401140 pri (PTrue _ _) = 0
11411141 pri (PRefl _ _) = 1
11421142 pri (PEq _ _ _ l r) = max 1 (max (pri l) (pri r))
@@ -1182,10 +1182,10 @@ addStatics n tm ptm =
11821182 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }
11831183 addIBC (IBCStatic n)
11841184 where
1185− initStatics (Bind n (Pi _ ty _) sc) (PPi p n' t s)
1186− | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' t s) in
1185+ initStatics (Bind n (Pi _ ty _) sc) (PPi p n' fc t s)
1186+ | n /= n' = let (static, dynamic) = initStatics sc (PPi p n' fc t s) in
11871187 (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)
11891189 = let (static, dynamic) = initStatics (instantiate (P Bound n ty) sc) s in
11901190 if pstatic p == Static then ((n, ty) : static, dynamic)
11911191 else if (not (searchArg p))
@@ -1254,16 +1254,16 @@ addUsingConstraints syn fc t
12541254 -- if all of args in ns, then add it
12551255 doAdd (UConstraint c args : cs) ns t
12561256 | all (\n -> elem n ns) args
1257− = PPi (Constraint [] Dynamic) (sMN 0 "cu")
1257+ = PPi (Constraint [] Dynamic) (sMN 0 "cu") NoFC
12581258 (mkConst c args) (doAdd cs ns t)
12591259 | otherwise = doAdd cs ns t
12601260
12611261 mkConst c args = PApp fc (PRef fc c)
12621262 (map (\n -> PExp 0 [] (sMN 0 "carg") (PRef fc n)) args)
12631263
1264− getConstraints (PPi (Constraint _ _) _ c sc)
1264+ getConstraints (PPi (Constraint _ _) _ _ c sc)
12651265 = getcapp c ++ getConstraints sc
1266− getConstraints (PPi _ _ c sc) = getConstraints sc
1266+ getConstraints (PPi _ _ _ c sc) = getConstraints sc
12671267 getConstraints _ = []
12681268
12691269 getcapp (PApp _ (PRef _ c) args)
@@ -1300,7 +1300,7 @@ addUsingImpls syn n fc t
13001300 -- if all of args in ns, then add it
13011301 doAdd (UImplicit n ty : cs) ns t
13021302 | 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)
13041304 | otherwise = doAdd cs ns t
13051305
13061306 -- bind the free names which weren't in the using block
@@ -1308,9 +1308,9 @@ addUsingImpls syn n fc t
13081308 bindFree (n:ns) tm
13091309 | elem n (map iname uimpls) = bindFree ns tm
13101310 | otherwise
1311− = PPi (Imp [] Dynamic False Nothing) n Placeholder (bindFree ns tm)
1311+ = PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder (bindFree ns tm)
13121312
1313− getArgnames (PPi _ n c sc)
1313+ getArgnames (PPi _ n _ c sc)
13141314 = n : getArgnames sc
13151315 getArgnames _ = []
13161316
@@ -1319,7 +1319,7 @@ addUsingImpls syn n fc t
13191319
13201320getUnboundImplicits :: IState -> Type -> PTerm -> [(Bool, PArg)]
13211321getUnboundImplicits i t tm = getImps t (collectImps tm)
1322− where collectImps (PPi p n t sc)
1322+ where collectImps (PPi p n _ t sc)
13231323 = (n, (p, t)) : collectImps sc
13241324 collectImps _ = []
13251325
@@ -1419,13 +1419,13 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14191419 = do (decls, ns) <- get
14201420 let isn = concatMap (namesIn uvars ist) (map getTm as)
14211421 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)
14231423 = do let isn = nub (implNamesIn uvars ty) `dropAll` [n]
14241424 (decls , ns) <- get
14251425 put (PImp (getPriority ist ty) True l n Placeholder : decls,
14261426 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
14271427 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)
14291429 = do let isn = nub (implNamesIn uvars ty ++ case sc of
14301430 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
14311431 _ -> [])
@@ -1433,7 +1433,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14331433 put (PExp (getPriority ist ty) l n Placeholder : decls,
14341434 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
14351435 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)
14371437 = do let isn = nub (implNamesIn uvars ty ++ case sc of
14381438 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
14391439 _ -> [])
@@ -1441,7 +1441,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14411441 put (PConstraint 10 l n Placeholder : decls,
14421442 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))
14431443 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)
14451445 = do let isn = nub (implNamesIn uvars ty ++ case sc of
14461446 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]
14471447 _ -> [])
@@ -1476,7 +1476,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14761476 = do (decls, ns) <- get
14771477 let isn = concatMap (namesIn uvars ist) as
14781478 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)
14801480 = do imps False env ty
14811481 imps False (n:env) sc
14821482 imps top env (PHidden tm) = imps False env tm
@@ -1488,8 +1488,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $
14881488 pibind using [] sc = sc
14891489 pibind using (n:ns) sc
14901490 = case lookup n using of
1491− Just ty -> PPi (Imp [] Dynamic False Nothing) n ty (pibind using ns sc)
1492− Nothing -> PPi (Imp [] Dynamic False Nothing) n Placeholder
1491+ Just ty -> PPi (Imp [] Dynamic False Nothing) n NoFC ty (pibind using ns sc)
1492+ Nothing -> PPi (Imp [] Dynamic False Nothing) n NoFC Placeholder
14931493 (pibind using ns sc)
14941494
14951495-- Add implicit arguments in function calls
@@ -1572,18 +1572,20 @@ addImpl' inpat env infns imp_meths ist ptm
15721572 -- definition which is passed through addImpl again with more scope
15731573 -- information
15741574 PCase fc c' os
1575− -- If the name in a lambda is a constructor name, do this as a 'case'
1576− -- instead (it is harmless to do so, especially since the lambda will
1577− -- be lifted anyway!)
1575+
15781576 ai qq env ds (PIfThenElse fc c t f) = PIfThenElse fc (ai qq env ds c)
15791577 (ai qq env ds t)
15801578 (ai qq env ds f)
1581− ai qq env ds (PLam fc n ty sc)
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!)
1583+ ai qq env ds (PLam fc n nfc ty sc)
15821584 = case lookupDef n (tt_ctxt ist) of
15831585 [] -> let ty' = ai qq env ds ty
15841586 sc' = ai qq ((n, Just ty):env) ds sc in
1585− PLam fc n ty' sc'
1586− _ -> ai qq env ds (PLam fc (sMN 0 "lamp") ty
1587+ PLam fc n nfc ty' sc'
1588+ _ -> ai qq env ds (PLam fc (sMN 0 "lamp") NoFC ty
15871589 (PCase fc (PRef fc (sMN 0 "lamp") )
15881590 [(PRef fc n, sc)]))
15891591 ai qq env ds (PLet fc n ty val sc)
@@ -1593,12 +1595,12 @@ addImpl' inpat env infns imp_meths ist ptm
15931595 sc' = ai qq ((n, Just ty):env) ds sc in
15941596 PLet fc n ty' val' sc'
15951597 _ -> 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)
15971599 = let ty' = ai qq env ds ty
15981600 env' = if n `elem` imp_meths then env
15991601 else ((n, Just ty) : env)
16001602 sc' = ai qq env' ds sc in
1601− PPi p n ty' sc'
1603+ PPi p n nfc ty' sc'
16021604 ai qq env ds (PGoal fc r n sc)
16031605 = let r' = ai qq env ds r
16041606 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
18081810 else PAlternative b alts'
18091811 su (PPair fc p l r) = PPair fc p (su l) (su r)
18101812 su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)
1811− su t@(PLam fc _ _ _) = PHidden t
1812− su t@(PPi _ _ _ _) = PHidden t
1813+ su t@(PLam _ _ _ _ _) = PHidden t
1814+ su t@(PPi _ _ _ _ _) = PHidden t
18131815 su t@(PEq _ _ _ _ _) = PHidden t
18141816 su t = t
18151817
@@ -1833,7 +1835,7 @@ findStatics :: IState -> PTerm -> (PTerm, [Bool])
18331835findStatics ist tm = trace (show tm) $
18341836 let (ns, ss) = fs tm in
18351837 runState (pos ns ss tm) []
1836− where fs (PPi p n t sc)
1838+ where fs (PPi p n fc t sc)
18371839 | Static <- pstatic p
18381840 = let (ns, ss) = fs sc in
18391841 (namesIn [] ist t : ns, n : ss)
@@ -1843,15 +1845,15 @@ findStatics ist tm = trace (show tm) $
18431845
18441846 inOne n ns = length (filter id (map (elem n) ns)) == 1
18451847
1846− pos ns ss (PPi p n t sc)
1848+ pos ns ss (PPi p n fc t sc)
18471849 | elem n ss = do sc' <- pos ns ss sc
18481850 spos <- get
18491851 put (True : spos)
1850− return (PPi (p { pstatic = Static }) n t sc')
1852+ return (PPi (p { pstatic = Static }) n fc t sc')
18511853 | otherwise = do sc' <- pos ns ss sc
18521854 spos <- get
18531855 put (False : spos)
1854− return (PPi p n t sc')
1856+ return (PPi p n fc t sc')
18551857 pos ns ss t = return t
18561858
18571859-- for 6.12/7 compatibility
@@ -1951,12 +1953,12 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
19511953 match (PResolveTC _) (PResolveTC _) = return []
19521954 match (PTrue _ _) (PTrue _ _) = return []
19531955 match (PReturn _) (PReturn _) = return []
1954− match (PPi _ _ t s) (PPi _ _ t' s') = do mt <- match' t t'
1955− ms <- match' s s'
1956− return (mt ++ ms)
1957− match (PLam _ _ t s) (PLam _ _ t' s') = do mt <- match' t t'
1958− ms <- match' s s'
1959− return (mt ++ ms)
1956+ match (PPi _ _ _ t s) (PPi _ _ _ t' s') = do mt <- match' t t'
1957+ ms <- match' s s'
1958+ return (mt ++ ms)
1959+ match (PLam _ _ _ t s) (PLam _ _ _ t' s') = do mt <- match' t t'
1960+ ms <- match' s s'
1961+ return (mt ++ ms)
19601962 match (PLet _ _ t ty s) (PLet _ _ t' ty' s') = do mt <- match' t t'
19611963 mty <- match' ty ty'
19621964 ms <- match' s s'
@@ -2003,13 +2005,13 @@ substMatch n = substMatchShadow n []
20032005substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
20042006substMatchShadow n shs tm t = sm shs t where
20052007 sm xs (PRef _ n') | n == n' = tm
2006− sm xs (PLam fc x t sc) = PLam fc x (sm xs t) (sm xs sc)
2007− sm xs (PPi p x t sc)
2008+ sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)
2009+ sm xs (PPi p x fc t sc)
20082010 | x `elem` xs
20092011 = let x' = nextName x in
2010− PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))
2011− (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
2012− | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)
2012+ PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC x') t))
2013+ (sm (x':xs) (substMatch x (PRef emptyFC x') sc))
2014+ | otherwise = PPi p x fc (sm xs t) (sm (x : xs) sc)
20132015 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)
20142016 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)
20152017 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
20322034shadow :: Name -> Name -> PTerm -> PTerm
20332035shadow n n' t = sm t where
20342036 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)
2036− | otherwise = PLam fc x (sm t) sc
2037− sm (PPi p x t sc) | n /= x = PPi p x (sm t) (sm sc)
2038− | otherwise = PPi p x (sm t) sc
2037+ sm (PLam fc x xfc t sc) | n /= x = PLam fc x xfc (sm t) (sm sc)
2038+ | otherwise = PLam fc x xfc (sm t) sc
2039+ sm (PPi p x fc t sc) | n /= x = PPi p x fc (sm t) (sm sc)
2040+ | otherwise = PPi p x fc (sm t) sc
20392041 sm (PLet fc x t v sc) | n /= x = PLet fc x (sm t) (sm v) (sm sc)
20402042 | otherwise = PLet fc x (sm t) (sm v) sc
20412043 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
20772079 mkUniqT tac = return tac
20782080
20792081 mkUniq :: PTerm -> State (S.Set Name) PTerm
2080− mkUniq (PLam fc n ty sc)
2082+ mkUniq (PLam fc n nfc ty sc)
20812083 = do env <- get
20822084 (n', sc') <-
20832085 if n `S.member` env
@@ -2088,8 +2090,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
20882090 put (S.insert n' env)
20892091 ty' <- mkUniq ty
20902092 sc'' <- mkUniq sc'
2091− return $! PLam fc n' ty' sc''
2092− mkUniq (PPi p n ty sc)
2093+ return $! PLam fc n' nfc ty' sc''
2094+ mkUniq (PPi p n fc ty sc)
20932095 = do env <- get
20942096 (n', sc') <-
20952097 if n `S.member` env
@@ -2100,7 +2102,7 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where
21002102 put (S.insert n' env)
21012103 ty' <- mkUniq ty
21022104 sc'' <- mkUniq sc'
2103− return $! PPi p n' ty' sc''
2105+ return $! PPi p n' fc ty' sc''
21042106 mkUniq (PLet fc n ty val sc)
21052107 = do env <- get
21062108 (n', sc') <-
src/Idris/AbsSyntaxTree.hs+30−30
@@ -603,7 +603,7 @@ data PDecl' t
603603 | PNamespace String [PDecl' t] -- ^ New namespace
604604 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
605605 Name -- Record name
606− [(Name, Plicity, t)] -- Parameters
606+ [(Name, FC, Plicity, t)] -- Parameters, where FC is precise name span
607607 [(Name, Docstring (Either Err PTerm))] -- Param Docs
608608 [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
609609 (Maybe Name) -- Optional constructor name
@@ -810,8 +810,8 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua
810810 | PRef FC Name -- ^ A reference to a variable
811811 | PInferRef FC Name -- ^ A name to be defined later
812812 | PPatvar FC Name -- ^ A pattern variable
813− | PLam FC Name PTerm PTerm -- ^ A lambda abstraction
814− | PPi Plicity Name PTerm PTerm -- ^ (n : t1) -> t2
813+ | PLam FC Name FC PTerm PTerm -- ^ A lambda abstraction. Second FC is name span.
814+ | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the variable
815815 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding
816816 | PTyped PTerm PTerm -- ^ Term with explicit type
817817 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x
@@ -861,8 +861,8 @@ deriving instance NFData PTerm
861861
862862mapPT :: (PTerm -> PTerm) -> PTerm -> PTerm
863863mapPT f t = f (mpt t) where
864− mpt (PLam fc n t s) = PLam fc n (mapPT f t) (mapPT f s)
865− mpt (PPi p n t s) = PPi p 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 nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)
866866 mpt (PLet fc n ty v s) = PLet fc n (mapPT f ty) (mapPT f v) (mapPT f s)
867867 mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)
868868 (fmap (mapPT f) g)
@@ -1020,8 +1020,8 @@ highestFC (PQuote _) = Nothing
10201020highestFC (PRef fc _) = Just fc
10211021highestFC (PInferRef fc _) = Just fc
10221022highestFC (PPatvar fc _) = Just fc
1023−highestFC (PLam fc _ _ _) = Just fc
1024−highestFC (PPi _ _ _ _) = Nothing
1023+highestFC (PLam fc _ _ _ _) = Just fc
1024+highestFC (PPi _ _ _ _ _) = Nothing
10251025highestFC (PLet fc _ _ _ _) = Just fc
10261026highestFC (PTyped tm ty) = highestFC tm <|> highestFC ty
10271027highestFC (PApp fc _ _) = Just fc
@@ -1262,8 +1262,8 @@ inferTy = sMN 0 "__Infer"
12621262inferCon = sMN 0 "__infer"
12631263inferDecl = PDatadecl inferTy
12641264 (PType bi)
1265− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") (PType bi) (
1266− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
1265+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") NoFC (PType bi) (
1266+ PPi expl (sMN 0 "ival") NoFC (PRef bi (sMN 0 "iType"))
12671267 (PRef bi inferTy)), bi, [])]
12681268inferOpts = []
12691269
@@ -1321,8 +1321,8 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType bi), (n "B", PType bi)]
13211321 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
13221322 (PType bi)))
13231323 [(reflDoc, reflParamDoc,
1324− eqCon, PPi impl (n "A") (PType bi) (
1325− PPi impl (n "x") (PRef bi (n "A"))
1324+ eqCon, PPi impl (n "A") NoFC (PType bi) (
1325+ PPi impl (n "x") NoFC (PRef bi (n "A"))
13261326 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
13271327 pimp (n "B") Placeholder False,
13281328 pexp (PRef bi (n "x")),
@@ -1356,7 +1356,7 @@ piBind = piBindp expl
13561356
13571357piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
13581358piBindp 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)
13601360
13611361
13621362-- Pretty-printing declarations and terms
@@ -1445,7 +1445,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14451445 | Just str <- slist p bnd e = str
14461446 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
14471447 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) =
14491449 bracket p startPrec . group . align . hang 2 $
14501450 text "\\" <> prettyBindingOf n False <+> text "=>" <$>
14511451 prettySe startPrec ((n, False):bnd) sc
@@ -1453,7 +1453,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14531453 bracket p startPrec . group . align $
14541454 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
14551455 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)
14571457 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
14581458 bracket p startPrec . group $
14591459 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
14661466 case s of
14671467 Static -> text "[static]" <> space
14681468 _ -> 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)
14701470 | ppopt_impl ppo =
14711471 bracket p startPrec $
14721472 lbrace <> prettyBindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
@@ -1477,10 +1477,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
14771477 case s of
14781478 Static -> text "[static]" <> space
14791479 _ -> empty
1480− prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1480+ prettySe p bnd (PPi (Constraint _ _) n _ ty sc) =
14811481 bracket p startPrec $
14821482 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) =
14841484 bracket p startPrec $
14851485 lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
14861486 rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
@@ -1866,8 +1866,8 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
18661866instance Sized PTerm where
18671867 size (PQuote rawTerm) = size rawTerm
18681868 size (PRef fc name) = size name
1869− size (PLam fc name ty bdy) = 1 + size ty + size bdy
1870− size (PPi plicity 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 fc ty bdy) = 1 + size ty + size fc + size bdy
18711871 size (PLet fc name ty def bdy) = 1 + size ty + size def + size bdy
18721872 size (PTyped trm ty) = 1 + size trm + size ty
18731873 size (PApp fc name args) = 1 + size args
@@ -1900,7 +1900,7 @@ instance Sized PTerm where
19001900 size _ = 0
19011901
19021902getPArity :: PTerm -> Int
1903−getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1903+getPArity (PPi _ _ _ _ sc) = 1 + getPArity sc
19041904getPArity _ = 0
19051905
19061906-- Return all names, free or globally bound, in the given term.
@@ -1915,8 +1915,8 @@ allNamesIn tm = nub $ ni [] tm
19151915 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
19161916 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
19171917 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
1919− ni env (PPi p n ty sc) = niTacImp env p ++ 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
19201920 ni env (PHidden tm) = ni env tm
19211921 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
19221922 ni env (PRewrite _ l r _) = ni env l ++ ni env r
@@ -1942,9 +1942,9 @@ boundNamesIn tm = S.toList (ni S.empty tm)
19421942 ni set (PAppBind _ f as) = niTms (ni set f) (map getTm as)
19431943 ni set (PCase _ c os) = niTms (ni set c) (map snd os)
19441944 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
19461946 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
19481948 ni set (PEq _ _ _ l r) = ni (ni set l) r
19491949 ni set (PRewrite _ l r _) = ni (ni set l) r
19501950 ni set (PTyped l r) = ni (ni set l) r
@@ -1983,8 +1983,8 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm
19831983 (nub (concatMap (ni env) (map snd os))
19841984 \\ nub (concatMap (ni env) (map fst os)))
19851985 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
1987− ni env (PPi p 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
19881988 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
19891989 ni env (PRewrite _ l r _) = ni env l ++ ni env r
19901990 ni env (PTyped l r) = ni env l ++ ni env r
@@ -2014,8 +2014,8 @@ namesIn uvars ist tm = nub $ ni [] tm
20142014 (nub (concatMap (ni env) (map snd os))
20152015 \\ nub (concatMap (ni env) (map fst os)))
20162016 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
2018− ni env (PPi p n ty sc) = niTacImp env p ++ 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
20192019 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
20202020 ni env (PRewrite _ l r _) = ni env l ++ ni env r
20212021 ni env (PTyped l r) = ni env l ++ ni env r
@@ -2046,8 +2046,8 @@ usedNamesIn vars ist tm = nub $ ni [] tm
20462046 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)
20472047 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)
20482048 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
2050− ni env (PPi p n ty sc) = niTacImp env p ++ 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
20512051 ni env (PEq _ _ _ l r) = ni env l ++ ni env r
20522052 ni env (PRewrite _ l r _) = ni env l ++ ni env r
20532053 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
346346 return (show fn ++ " " ++ ap ++ "= ?"
347347 ++ show fn ++ "_rhs")
348348 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
350350 = let n = getNameFrom i used ty in
351351 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
353353 | thead n == '_'
354354 = let n = getNameFrom i used ty in
355355 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
357357 = 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
359359 mkApp i _ _ = ""
360360
361− getNameFrom i used (PPi _ _ _ _)
361+ getNameFrom i used (PPi _ _ _ _ _)
362362 = uniqueNameFrom (mkSupply [sUN "f", sUN "g"]) used
363363 getNameFrom i used (PApp fc f as) = getNameFrom i used f
364364 getNameFrom i used (PEq _ _ _ _ _) = uniqueNameFrom (mkSupply [sUN "prf"]) used
@@ -388,7 +388,7 @@ getProofClause :: Int -- ^ line number that the type is declared
388388getProofClause l fn fp
389389 = do ty <- getInternalApp fp l
390390 return (mkApp ty ++ " = ?" ++ show fn ++ "_rhs")
391− where mkApp (PPi _ _ _ sc) = mkApp sc
391+ where mkApp (PPi _ _ _ _ sc) = mkApp sc
392392 mkApp rt = "(" ++ show rt ++ ") <== " ++ show fn
393393
394394-- 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 =
4545 otherwise -> PRef fc $ reflm "NErased"
4646
4747expandSugar :: DSL -> PTerm -> PTerm
48−expandSugar dsl (PLam fc n ty tm)
48+expandSugar dsl (PLam fc n nfc ty tm)
4949 | Just lam <- dsl_lambda dsl
5050 = let sc = PApp fc lam [ pexp (mkTTName fc n)
5151 , pexp (var dsl n tm 0)]
5252 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)
5454expandSugar dsl (PLet fc n ty v tm)
5555 | Just letb <- dsl_let dsl
5656 = let sc = PApp (fileFC "(dsl)") letb [ pexp (mkTTName fc n)
@@ -58,13 +58,13 @@ expandSugar dsl (PLet fc n ty v tm)
5858 , pexp (var dsl n tm 0)]
5959 in expandSugar dsl sc
6060expandSugar 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)
6262 | Just pi <- dsl_pi dsl
6363 = let sc = PApp (fileFC "(dsl)") pi [ pexp (mkTTName (fileFC "(dsl)") n)
6464 , pexp ty
6565 , pexp (var dsl n tm 0)]
6666 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)
6868expandSugar dsl (PApp fc t args) = PApp fc (expandSugar dsl t)
6969 (map (fmap (expandSugar dsl)) args)
7070expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)
@@ -98,9 +98,9 @@ expandSugar dsl (PDoBlock ds)
9898 block b [DoExp fc tm] = tm
9999 block b [a] = PElabError (Msg "Last statement in do block must be an expression")
100100 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))]
102102 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
104104 (PCase fc (PRef fc (sMN 0 "bpat"))
105105 ((p, block b rest) : alts)))]
106106 block b (DoLet fc n ty tm : rest)
@@ -110,7 +110,7 @@ expandSugar dsl (PDoBlock ds)
110110 block b (DoExp fc tm : rest)
111111 = PApp fc b
112112 [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))]
114114 block b _ = PElabError (Msg "Invalid statement in do block")
115115
116116expandSugar 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
124124 case dsl_var dsl of
125125 Nothing -> PElabError (Msg "No 'variable' defined in dsl")
126126 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)
128128 | Nothing <- dsl_lambda dsl
129− = PLam fc n ty (v' i sc)
130− | otherwise = PLam fc n (v' i ty) (v' (i + 1) sc)
129+ = PLam fc n nfc ty (v' i sc)
130+ | otherwise = PLam fc n nfc (v' i ty) (v' (i + 1) sc)
131131 v' i (PLet fc n ty val sc)
132132 | Nothing <- dsl_let dsl
133133 = PLet fc n (v' i ty) (v' i val) (v' i sc)
134134 | 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)
136136 | Nothing <- dsl_pi dsl
137− = PPi p n (v' i ty) (v' i sc)
138− | otherwise = PPi p n (v' i ty) (v' (i+1) sc)
137+ = PPi p n fc (v' i ty) (v' i sc)
138+ | otherwise = PPi p n fc (v' i ty) (v' (i+1) sc)
139139 v' i (PTyped l r) = PTyped (v' i l) (v' i r)
140140 v' i (PApp f x as) = PApp f (v' i x) (fmap (fmap (v' i)) as)
141141 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
190190 = do t' <- db' t
191191 args' <- mapM dbArg args
192192 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))
194194 db' (PLet fc n ty v sc) = do v' <- db' v
195195 return (PLet fc n ty v' (debind b sc))
196196 db' (PCase fc s opts) = do s' <- db' s
@@ -215,6 +215,6 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in
215215
216216 bindAll [] tm = tm
217217 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))]
219219
220220
src/Idris/DeepSeq.hs+3−3
@@ -200,9 +200,9 @@ instance NFData PTerm where
200200 rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
201201 rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
202202 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` ()
204− rnf (PPi x1 x2 x3 x4)
205− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `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 x5)
205+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
206206 rnf (PLet _ x1 x2 x3 x4)
207207 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
208208 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
6161 Just (Just _, mi, _) -> mkMVApp n []
6262 _ -> PRef un n
6363 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)
6565 de env is (Bind n (Pi (Just impl) ty _) sc)
6666 | 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)
6868 | 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)
7070 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)
7272 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)
7474 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)
7676 de env (plic:is) (Bind n (Pi _ ty _) sc)
7777 = PPi (Exp (argopts plic) Dynamic False)
78− n
78+ n NoFC
7979 (de env [] ty)
8080 (de ((n,n):env) is sc)
8181 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)
8383
8484 de env imps (Bind n (Let ty val) sc)
8585 | isCaseApp sc
@@ -477,14 +477,14 @@ addImplicitDiffs x y
477477 else (a { getTm = a' } : as',
478478 b { getTm = b' } : bs')
479479 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)
481481 = let (a', c') = addI a c
482482 (b', d') = addI b d in
483− (PLam fc n a' b', PLam fc' n' c' d')
484− addI (PPi p n a b) (PPi p' n' c d)
483+ (PLam fc n nfc a' b', PLam fc' n' nfc' c' d')
484+ addI (PPi p n fc a b) (PPi p' n' fc' c d)
485485 = let (a', c') = addI a c
486486 (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')
488488 addI (PRefl fc a) (PRefl fc' b)
489489 = let (a', b') = addI a b in
490490 (PRefl fc a', PRefl fc' b')
@@ -528,9 +528,9 @@ addImplicitDiffs x y
528528 expLike (PApp _ f as) (PApp _ f' as')
529529 = expLike f f' && length as == length as' &&
530530 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')
532532 = 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')
534534 = n == n' && expLike s s' && expLike t t'
535535 expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'
536536 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)
163163 dumpInstance :: PTerm -> Doc OutputAnnotation
164164 dumpInstance = pprintPTerm ppo params' [] infixes
165165
166− prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm
167− prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)
166+ prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm
167+ prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2)
168168 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
169169 prettifySubclasses tm = tm
170170
@@ -178,8 +178,8 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
178178 updateRef nm (PRef fc _) = PRef fc nm
179179 updateRef _ pt = pt
180180
181− isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'
182− isSubclass (PPi _ _ _ pt) = isSubclass pt
181+ isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'
182+ isSubclass (PPi _ _ _ _ pt) = isSubclass pt
183183 isSubclass _ = False
184184
185185 prettyParameters =
@@ -262,9 +262,9 @@ docClass n ci
262262 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t
263263 getDInst _ = Nothing
264264
265− isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))
265+ isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))
266266 = nm == n && map getTm args == map getTm args'
267− isSubclass (PPi _ _ _ pt)
267+ isSubclass (PPi _ _ _ _ pt)
268268 = isSubclass pt
269269 isSubclass _
270270 = False
@@ -290,7 +290,7 @@ docFun n
290290 funName n = show n
291291
292292getPArgNames :: 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 =
294294 (name, ty, plicity, lookup name ds) : getPArgNames body ds
295295getPArgNames _ _ = []
296296
src/Idris/Elab/Class.hs+14−14
@@ -106,13 +106,13 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
106106 where
107107 nodoc (n, (_, o, t)) = (n, (o, t))
108108 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))
110110
111111 -- To make sure the type constructor of the class is in the appropriate
112112 -- uniqueness hierarchy
113113 chkUniq u@(PUniverse _) (PType _) = u
114114 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
116116 chkUniq _ t = t
117117
118118 mdec :: Name -> Name
@@ -134,10 +134,10 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
134134
135135 impbind :: [(Name, PTerm)] -> PTerm -> PTerm
136136 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)
138138
139139 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)
141141 conbind [] x = x
142142
143143 getMName (PTy _ _ _ _ _ n _) = nsroot n
@@ -181,7 +181,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
181181 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)
182182 let lhs = PApp fc (PRef fc cfn) [pconst capp]
183183 let rhs = PResolveTC (fileFC "HACK")
184− let ty = PPi constraint cnm c con
184+ let ty = PPi constraint cnm NoFC c con
185185 logLvl 2 ("Dictionary constraint: " ++ showTmImpls ty)
186186 logLvl 2 (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
187187 i <- getIState
@@ -213,9 +213,9 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds
213213 return [PTy doc [] syn fc o m ty',
214214 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
215215
216− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA n : getMArgs sc
217− getMArgs (PPi (Exp _ _ _) n ty sc) = EA n : getMArgs sc
218− getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc
216+ getMArgs (PPi (Imp _ _ _ _) n _ ty sc) = IA n : getMArgs sc
217+ getMArgs (PPi (Exp _ _ _) n _ ty sc) = EA n : getMArgs sc
218+ getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc
219219 getMArgs _ = []
220220
221221 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
231231 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns
232232 rhsArgs [] _ = []
233233
234− insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)
235− = PPi p n ty (insertConstraint c sc)
234+ insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)
235+ = PPi p n fc ty (insertConstraint c sc)
236236 insertConstraint c sc = PPi (constraint { pstatic = Static })
237− (sMN 0 "class") c sc
237+ (sMN 0 "class") NoFC c sc
238238
239239 -- 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)
241241 | n `elem` ns = toExp ns e sc
242− | otherwise = PPi (e l s p) n ty (toExp ns e sc)
243− toExp ns e (PPi p n ty sc) = PPi 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 fc ty sc) = PPi p n fc ty (toExp ns e sc)
244244 toExp ns e sc = sc
245245
246246-- 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)
251251 else return ()
252252 tyIs con t = tclift $ tfail (At fc (Elaborating "constructor " con (Msg (show t ++ " is not " ++ show tn))))
253253
254− mkLazy (PPi pl n ty sc)
254+ mkLazy (PPi pl n nfc ty sc)
255255 = let ty' = if getTyName ty
256256 then PApp fc (PRef fc (sUN "Lazy'"))
257257 [pexp (PRef fc (sUN "LazyCodata")),
258258 pexp ty]
259259 else ty in
260− PPi pl n ty' (mkLazy sc)
260+ PPi pl n nfc ty' (mkLazy sc)
261261 mkLazy t = t
262262
263263 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)
266266
267267
268268 getNamePos :: Int -> PTerm -> Name -> Maybe Int
269− getNamePos i (PPi _ n _ sc) x | n == x = Just i
270− | otherwise = getNamePos (i + 1) sc x
269+ getNamePos i (PPi _ n _ _ sc) x | n == x = Just i
270+ | otherwise = getNamePos (i + 1) sc x
271271 getNamePos _ _ _ = Nothing
272272
273273 -- if the constructor is a UniqueType, the datatype must be too
@@ -353,8 +353,8 @@ elabCaseFun ind paramPos n ty cons info = do
353353 splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
354354 splitPi = splitPi' []
355355 where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
356− splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
357− splitPi' acc t = (reverse acc, t)
356+ splitPi' acc (PPi pl n _ tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
357+ splitPi' acc t = (reverse acc, t)
358358
359359 splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
360360 splitPms cnstrs = (map fst pms, map fst idxs)
@@ -418,7 +418,7 @@ elabCaseFun ind paramPos n ty cons info = do
418418
419419 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
420420 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)
422422
423423 interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
424424 interlievePos idxs [] l2 i = l2
@@ -436,9 +436,9 @@ elabCaseFun ind paramPos n ty cons info = do
436436 _ -> cns
437437
438438 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) =
440440 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))
442442 Just i -> (removeParamPis oldParams params tyr)
443443 removeParamPis oldParams params (PRef _ n) =
444444 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
201201 _ -> Nothing
202202 overlapping t' = tclift $ tfail (At fc (Msg $
203203 "Overlapping instance: " ++ show t' ++ " already defined"))
204− getRetType (PPi _ _ _ sc) = getRetType sc
204+ getRetType (PPi _ _ _ _ sc) = getRetType sc
205205 getRetType t = t
206206
207207 matchArgs i dets x y =
@@ -216,16 +216,16 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
216216
217217 mkMethApp (n, _, _, ty)
218218 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))
219− lamBind i (PPi (Constraint _ _) _ _ sc) sc'
220− = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
221− lamBind i (PPi _ n ty sc) sc'
222− = PLam fc (sMN i "meth") Placeholder (lamBind (i+1) sc sc')
219+ lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'
220+ = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
221+ lamBind i (PPi _ n _ ty sc) sc'
222+ = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')
223223 lamBind i _ sc = sc
224− methArgs i (PPi (Imp _ _ _ _) n ty sc)
224+ methArgs i (PPi (Imp _ _ _ _) n _ ty sc)
225225 = 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)
227227 = 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)
229229 = PConstraint 0 [] (sMN 0 "marg") (PResolveTC fc) : methArgs (i+1) sc
230230 methArgs i _ = []
231231
@@ -250,11 +250,11 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do
250250 (mkUniqueNames [] t)
251251
252252 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)
254254 conbind [] x = x
255255
256256 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)
258258 coninsert cs sc = conbind cs sc
259259
260260 -- 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
3737 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
3838 -> SyntaxInfo -> FC -> DataOpts
3939 -> Name -- ^ The name of the type being defined
40− -> [(Name, Plicity, PTerm)] -- ^ Parameters
40+ -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters
4141 -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs
4242 -> [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields
4343 -> Maybe Name -- ^ Constructor Name
@@ -51,7 +51,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
5151 logLvl 1 $ "Type constructor " ++ showTmImpls tycon
5252
5353 -- Data constructor
54− dconName <- generateDConName cname
54+ dconName <- generateDConName cname
5555 let dconTy = generateDConType params fieldsWithNameAndDoc
5656 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
5757
@@ -62,11 +62,11 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
6262
6363 iLOG $ "fieldsWithName " ++ show fieldsWithName
6464 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
6666 where
6767 -- | Generates a type constructor.
68− generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
69− generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
68+ generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
69+ generateTyConType ((n, nfc, p, t) : rest) = PPi p (nsroot n) nfc t (generateTyConType rest)
7070 generateTyConType [] = (PType fc)
7171
7272 -- | 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
8181 Nothing -> return n
8282
8383 -- | Generates the data constructor type.
84− generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm
85− generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
86− generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) t (generateDConType [] as)
84+ generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm
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) NoFC t (generateDConType [] as)
8787 generateDConType [] [] = target
8888
8989 -- | The target for the constructor and projection functions. Also the source of the update functions.
9090 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]
9292
93− paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
93+ paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
9494 paramsAndDoc = pad params paramDocs
9595 where
96− pad :: [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
97− pad ((n, p, t) : rest) docs
96+ pad :: [(Name, FC, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
97+ pad ((n, fc, p, t) : rest) docs
9898 = let d = case lookup n docs of
9999 Just d' -> d
100100 Nothing -> emptyDocstring
101− in (n, p, t, d) : (pad rest docs)
101+ in (n, fc, p, t, d) : (pad rest docs)
102102 pad _ _ = []
103103
104104 dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
@@ -149,7 +149,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
149149 iLOG $ "Fields: " ++ show fieldNames
150150 iLOG $ "Params: " ++ show paramNames
151151 -- The elaborated constructor type for the data declaration
152− i <- getIState
152+ i <- getIState
153153 ttConsTy <-
154154 case lookupTyExact dconName (tt_ctxt i) of
155155 Just as -> return as
@@ -238,7 +238,7 @@ elabRecordFunctions info rsyn fc tyn params fields dconName target
238238 paramName (UN n) = sUN ("param_" ++ str n)
239239 paramName (MN i n) = sMN i ("param_" ++ str n)
240240 paramName (NS n s) = NS (paramName n) s
241− paramName n = n
241+ paramName n = n
242242
243243 -- | Elaborate the projection functions.
244244 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
264264 -- | A map from a field name to the other fields it depends on.
265265 fieldDependencies :: [(Name, [Name])]
266266 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]
267− where
267+ where
268268 fieldDep :: Name -> PTerm -> (Name, [Name])
269269 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
270270
271271 -- | A list of fields depending on another field.
272272 dependentFields :: [Name]
273273 dependentFields = filter depends fieldNames
274− where
274+ where
275275 depends :: Name -> Bool
276276 depends n = case lookup n fieldDependencies of
277277 Just xs -> not $ null xs
@@ -313,7 +313,7 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f
313313 where
314314 -- | The type of the projection function.
315315 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
317317
318318 -- | The left hand side of the projection function.
319319 generateLhs :: PTerm
@@ -373,9 +373,9 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option
373373 then logLvl 1 $ "Could not generate update function for " ++ show pname
374374 else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
375375 where
376− -- | The type of the udpate function.
376+ -- | The type of the update function.
377377 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))
379379 where substInput = substMatches [(cname, PRef fc (nsroot pname))]
380380
381381 -- | The "_set" name.
src/Idris/Elab/Term.hs+18−11
@@ -418,7 +418,10 @@ elab ist info emode opts fn tm
418418 _ -> asType
419419 where asType = elab' ina (Just fc) (PApp fc (PRef fc sigmaTy)
420420 [pexp t,
421− pexp (PLam fc n Placeholder r)])
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.
424+ pexp (PLam fc n NoFC Placeholder r)])
422425 asValue = elab' ina (Just fc) (PApp fc (PRef fc existsCon)
423426 [pimp (sMN 0 "a") t False,
424427 pimp (sMN 0 "P") Placeholder True,
@@ -514,8 +517,8 @@ elab ist info emode opts fn tm
514517 solve
515518 highlightSource fc hl
516519 else elab' ina fc' (PApp fc tm [])
517− elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
518− elab' ina _ (PLam fc n Placeholder sc)
520+ elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"
521+ elab' ina _ (PLam fc n nfc Placeholder sc)
519522 = do -- if n is a type constructor name, this makes no sense...
520523 ctxt <- get_context
521524 when (isTConName n ctxt) $
@@ -524,7 +527,8 @@ elab ist info emode opts fn tm
524527 attack; intro (Just n);
525528 -- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
526529 elabE (ina { e_inarg = True } ) (Just fc) sc; solve
527− elab' ec _ (PLam fc n ty sc)
530+ highlightSource nfc (AnnBoundName n False)
531+ elab' ec _ (PLam fc n nfc ty sc)
528532 = do tyn <- getNameFrom (sMN 0 "lamty")
529533 -- if n is a type constructor name, this makes no sense...
530534 ctxt <- get_context
@@ -542,11 +546,13 @@ elab ist info emode opts fn tm
542546 elabE (ec { e_inarg = True, e_intype = True }) (Just fc) ty
543547 elabE (ec { e_inarg = True }) (Just fc) sc
544548 solve
545− elab' ina fc (PPi p n Placeholder sc)
546− = do attack; arg n (is_scoped p) (sMN 0 "ty")
549+ highlightSource nfc (AnnBoundName n False)
550+ elab' ina fc (PPi p n nfc Placeholder sc)
551+ = do attack; arg n (is_scoped p) (sMN 0 "ty")
547552 elabE (ina { e_inarg = True, e_intype = True }) fc sc
548553 solve
549− elab' ina fc (PPi p n ty sc)
554+ highlightSource nfc (AnnBoundName n False)
555+ elab' ina fc (PPi p n nfc ty sc)
550556 = do attack; tyn <- getNameFrom (sMN 0 "ty")
551557 claim tyn RType
552558 n' <- case n of
@@ -558,6 +564,7 @@ elab ist info emode opts fn tm
558564 elabE ec' fc ty
559565 elabE ec' fc sc
560566 solve
567+ highlightSource nfc (AnnBoundName n False)
561568 elab' ina _ (PLet fc n ty val sc)
562569 = do attack
563570 ivs <- get_instances
@@ -793,7 +800,7 @@ elab ist info emode opts fn tm
793800 PAlternative False _ -> 5
794801 PAlternative True _ -> 2
795802 PTactics _ -> 150
796− PLam _ _ _ _ -> 3
803+ PLam _ _ _ _ _ -> 3
797804 PRewrite _ _ _ _ -> 4
798805 PResolveTC _ -> 0
799806 PHidden _ -> 150
@@ -1254,9 +1261,9 @@ elab ist info emode opts fn tm
12541261 do impn <- unique_hole (sMN 0 "imp")
12551262 if e_isfn ina -- apply to an implicit immediately
12561263 then return (PApp emptyFC
1257− (PLam emptyFC impn Placeholder t)
1264+ (PLam emptyFC impn NoFC Placeholder t)
12581265 [pexp Placeholder])
1259− else return (PLam emptyFC impn Placeholder t)
1266+ else return (PLam emptyFC impn NoFC Placeholder t)
12601267 addLam _ t = return t
12611268
12621269 insertCoerce ina t@(PCase _ _ _) = return t
@@ -1390,7 +1397,7 @@ pruneByType env (P _ n _) ctxt as
13901397 where
13911398 headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
13921399 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
13941401 headIs var f (PHidden t) = headIs var f t
13951402 headIs _ _ _ = True -- keep if it's not an application
13961403
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
203203 -- for making an internalapp, we only want the explicit ones, and don't
204204 -- want the parameters, so just take the arguments which correspond to the
205205 -- user declared explicit ones
206− mergeTy (PPi e n ty sc) (PPi e' n' _ sc')
207− | e == e' = PPi e n ty (mergeTy sc sc')
206+ mergeTy (PPi e n fc ty sc) (PPi e' n' _ _ sc')
207+ | e == e' = PPi e n fc ty (mergeTy sc sc')
208208 | otherwise = mergeTy sc sc'
209209 mergeTy _ sc = sc
210210
src/Idris/Elab/Utils.hs+6−6
@@ -66,9 +66,9 @@ inaccessibleImps _ _ _ = []
6666
6767-- | Get the list of (index, name) of inaccessible arguments from the type.
6868inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]
69−inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)
69+inaccessibleArgs i (PPi (Imp _ _ _ _) n _ Placeholder t)
7070 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit
71−inaccessibleArgs i (PPi plicity n ty t)
71+inaccessibleArgs i (PPi plicity n _ ty t)
7272 | InaccessibleArg `elem` pargopts plicity
7373 = (i,n) : inaccessibleArgs (i+1) t -- an .{erased : Implicit}
7474 | otherwise
@@ -117,7 +117,7 @@ inferredDiff fc inf user =
117117-- found, or it will give spurious errors.
118118checkDocs :: FC -> [(Name, Docstring a)] -> PTerm -> Idris ()
119119checkDocs 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
121121 cd as _ | Map.null as = return ()
122122 | otherwise = ierror . At fc . Msg $
123123 "There is documentation for argument(s) "
@@ -277,9 +277,9 @@ mkStatic ns (PTy doc argdocs syn fc o n ty)
277277mkStatic ns t = t
278278
279279mkStaticTy :: [Name] -> PTerm -> PTerm
280−mkStaticTy ns (PPi p n ty sc)
281− | n `elem` ns = PPi (p { pstatic = Static }) n ty (mkStaticTy ns sc)
282− | otherwise = PPi p n ty (mkStaticTy ns sc)
280+mkStaticTy ns (PPi p n fc ty sc)
281+ | n `elem` ns = PPi (p { pstatic = Static }) n fc ty (mkStaticTy ns sc)
282+ | otherwise = PPi p n fc ty (mkStaticTy ns sc)
283283mkStaticTy ns t = t
284284
285285
src/Idris/ElabQuasiquote.hs+4−4
@@ -71,14 +71,14 @@ extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be qua
7171
7272
7373extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])
74−extractUnquotes n (PLam fc name ty body)
74+extractUnquotes n (PLam fc name nfc ty body)
7575 = do (ty', ex1) <- extractUnquotes n ty
7676 (body', ex2) <- extractUnquotes n body
77− return (PLam fc name ty' body', ex1 ++ ex2)
78−extractUnquotes n (PPi plicity name ty body)
77+ return (PLam fc name nfc ty' body', ex1 ++ ex2)
78+extractUnquotes n (PPi plicity name fc ty body)
7979 = do (ty', ex1) <- extractUnquotes n ty
8080 (body', ex2) <- extractUnquotes n body
81− return (PPi plicity name ty' body', ex1 ++ ex2)
81+ return (PPi plicity name fc ty' body', ex1 ++ ex2)
8282extractUnquotes n (PLet fc name ty val body)
8383 = do (ty', ex1) <- extractUnquotes n ty
8484 (val', ex2) <- extractUnquotes n val
src/Idris/Error.hs+2−2
@@ -91,8 +91,8 @@ warnDisamb ist (PQuote _) = return ()
9191warnDisamb ist (PRef _ _) = return ()
9292warnDisamb ist (PInferRef _ _) = return ()
9393warnDisamb ist (PPatvar _ _) = return ()
94−warnDisamb ist (PLam _ _ t b) = warnDisamb ist t >> warnDisamb ist b
95−warnDisamb ist (PPi _ _ 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
9696warnDisamb ist (PLet _ _ x t b) = warnDisamb ist x >> warnDisamb ist t >> warnDisamb ist b
9797warnDisamb ist (PTyped x t) = warnDisamb ist x >> warnDisamb ist t
9898warnDisamb ist (PApp _ t args) = warnDisamb ist t >>
src/Idris/IBC.hs+16−12
@@ -1500,16 +1500,18 @@ instance Binary PTerm where
15001500 PPatvar x1 x2 -> do putWord8 3
15011501 put x1
15021502 put x2
1503− PLam x1 x2 x3 x4 -> do putWord8 4
1504− put x1
1505− put x2
1506− put x3
1507− put x4
1508− PPi x1 x2 x3 x4 -> do putWord8 5
1509− put x1
1510− put x2
1511− put x3
1512− put x4
1503+ PLam x1 x2 x3 x4 x5 -> do putWord8 4
1504+ put x1
1505+ put x2
1506+ put x3
1507+ put x4
1508+ put x5
1509+ PPi x1 x2 x3 x4 x5 -> do putWord8 5
1510+ put x1
1511+ put x2
1512+ put x3
1513+ put x4
1514+ put x5
15131515 PLet x1 x2 x3 x4 x5 -> do putWord8 6
15141516 put x1
15151517 put x2
@@ -1646,12 +1648,14 @@ instance Binary PTerm where
16461648 x2 <- get
16471649 x3 <- get
16481650 x4 <- get
1649− return (PLam x1 x2 x3 x4)
1651+ x5 <- get
1652+ return (PLam x1 x2 x3 x4 x5)
16501653 5 -> do x1 <- get
16511654 x2 <- get
16521655 x3 <- get
16531656 x4 <- get
1654− return (PPi x1 x2 x3 x4)
1657+ x5 <- get
1658+ return (PPi x1 x2 x3 x4 x5)
16551659 6 -> do x1 <- get
16561660 x2 <- get
16571661 x3 <- get
src/Idris/IdrisDoc.hs+2−2
@@ -291,8 +291,8 @@ extractPTermNames :: PTerm -- ^ Where to extract names from
291291extractPTermNames (PRef _ n) = [n]
292292extractPTermNames (PInferRef _ n) = [n]
293293extractPTermNames (PPatvar _ n) = [n]
294−extractPTermNames (PLam _ n p1 p2) = n : concatMap extract [p1, p2]
295−extractPTermNames (PPi _ 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]
296296extractPTermNames (PLet _ n p1 p2 p3) = n : concatMap extract [p1, p2, p3]
297297extractPTermNames (PTyped p1 p2) = concatMap extract [p1, p2]
298298extractPTermNames (PApp _ p pas) = let names = concatMap extractPArg pas
src/Idris/Interactive.hs+5−5
@@ -197,9 +197,9 @@ doProofSearch fn updatefile rec l n hints (Just depth)
197197 runIO $ copyFile fb fn
198198 else iPrintResult newmv
199199 where dropCtxt 0 sc = sc
200− dropCtxt i (PPi _ _ _ sc) = dropCtxt (i - 1) sc
200+ dropCtxt i (PPi _ _ _ _ sc) = dropCtxt (i - 1) sc
201201 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
203203 dropCtxt _ t = t
204204
205205 stripNS tm = mapPT dens tm where
@@ -304,11 +304,11 @@ makeLemma fn updatefile l n
304304 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
305305 appArgs skip i _ = ""
306306
307− stripMNBind skip (PPi b n@(UN c) ty sc)
307+ stripMNBind skip (PPi b n@(UN c) _ ty sc)
308308 | (thead c /= '_' && n `notElem` skip) ||
309309 take 4 (str c) == "__pi" -- keep in type, but not in app
310− = PPi b n ty (stripMNBind skip sc)
311− stripMNBind skip (PPi b _ ty sc) = stripMNBind skip sc
310+ = PPi b n NoFC ty (stripMNBind skip sc)
311+ stripMNBind skip (PPi b _ _ ty sc) = stripMNBind skip sc
312312 stripMNBind skip t = t
313313
314314 -- 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
6464 Nothing -> return ()
6565 return $ PRecord doc rsyn fc opts tyn params paramDocs fields cname cdoc syn
6666 <?> "record type declaration"
67− where
67+ where
6868 getRecNames :: SyntaxInfo -> PTerm -> [Name]
69− getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
70− ++ getRecNames syn sc
69+ getRecNames syn (PPi _ n _ _ sc) = [expandNS syn n, expandNS syn (mkType n)]
70+ ++ getRecNames syn sc
7171 getRecNames _ _ = []
7272
7373 toFreeze :: Maybe Accessibility -> Maybe Accessibility
@@ -117,28 +117,28 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
117117 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)
118118 annotate syn ist = annotCode $ tryFullExpr syn ist
119119
120−recordParameter :: SyntaxInfo -> IdrisParser (Name, Plicity, PTerm)
120+recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
121121recordParameter syn =
122122 (do lchar '('
123− (n, pt) <- (namedTy syn <|> onlyName syn)
123+ (n, nfc, pt) <- (namedTy syn <|> onlyName syn)
124124 lchar ')'
125− return (n, expl, pt))
125+ return (n, nfc, expl, pt))
126126 <|>
127− (do (n, pt) <- onlyName syn
128− return (n, expl, pt))
129−
127+ (do (n, nfc, pt) <- onlyName syn
128+ return (n, nfc, expl, pt))
129+
130130 where
131− namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)
131+ namedTy :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
132132 namedTy syn =
133− do n <- fst <$> fnName
133+ do (n, nfc) <- fnName
134134 lchar ':'
135135 ty <- typeExpr (allowImp syn)
136− return (expandNS syn n, ty)
137− onlyName :: SyntaxInfo -> IdrisParser (Name, PTerm)
136+ return (expandNS syn n, nfc, ty)
137+ onlyName :: SyntaxInfo -> IdrisParser (Name, FC, PTerm)
138138 onlyName syn =
139− do n <- fst <$> fnName
139+ do (n, nfc) <- fnName
140140 fc <- getFC
141− return (expandNS syn n, PType fc)
141+ return (expandNS syn n, nfc, PType fc)
142142
143143{- | Parses data declaration type (normal or codata)
144144DataI ::= 'data' | 'codata';
@@ -230,7 +230,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do
230230 mkPApp fc t [] = t
231231 mkPApp fc t xs = PApp fc t (map pexp xs)
232232 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
234234 combineDataOpts :: DataOpts -> DataOpts
235235 combineDataOpts opts = if Codata `elem` opts
236236 then delete DefaultEliminator opts
src/Idris/ParseExpr.hs+28−28
@@ -164,10 +164,10 @@ extension syn ns rules =
164164 update ns (PRef fc n) = case lookup n ns of
165165 Just (SynTm t) -> t
166166 _ -> PRef fc n
167− update ns (PLam fc n ty sc)
168− = PLam fc (updateB ns n) (update ns ty) (update (dropn n ns) sc)
169− update ns (PPi p n ty sc)
170− = PPi (updTacImp ns p) (updateB ns n)
167+ update ns (PLam fc n nfc ty sc)
168+ = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
169+ update ns (PPi p n fc ty sc)
170+ = PPi (updTacImp ns p) (updateB ns n) fc
171171 (update ns ty) (update (dropn n ns) sc)
172172 update ns (PLet fc n ty val sc)
173173 = PLet fc (updateB ns n) (update ns ty)
@@ -403,7 +403,7 @@ bracketed' syn =
403403 -- No prefix operators! (bit of a hack here...)
404404 if (o == "-" || o == "!")
405405 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
407407 (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),
408408 pexp e]))
409409 <|> try (do l <- simpleExpr syn
@@ -413,7 +413,7 @@ bracketed' syn =
413413 fc0 <- getFC
414414 case op of
415415 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
417417 (PApp fc0 (PRef fc0 (sUN o)) [pexp l,
418418 pexp (PRef fc0 (sMN 1000 "ARG"))]))
419419 <|> do l <- expr syn
@@ -688,13 +688,13 @@ recordType syn =
688688 Left fields ->
689689 case rec of
690690 Nothing ->
691− return (PLam fc (sMN 0 "fldx") Placeholder
691+ return (PLam fc (sMN 0 "fldx") NoFC Placeholder
692692 (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
693693 Just v -> return (applyAll fc fields v)
694694 Right fields ->
695695 case rec of
696696 Nothing ->
697− return (PLam fc (sMN 0 "fldx") Placeholder
697+ return (PLam fc (sMN 0 "fldx") NoFC Placeholder
698698 (getAll fc (reverse fields)
699699 (PRef fc (sMN 0 "fldx"))))
700700 Just v -> return (getAll fc (reverse fields) v)
@@ -791,7 +791,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"
791791 where pmList :: [(Int, (FC, PTerm))] -> PTerm -> PTerm
792792 pmList [] sc = sc
793793 pmList ((i, (fc, x)) : xs) sc
794− = PLam fc (sMN i "lamp") Placeholder
794+ = PLam fc (sMN i "lamp") NoFC Placeholder
795795 (PCase fc (PRef fc (sMN i "lamp"))
796796 [(x, pmList xs sc)])
797797 lambdaTail :: IdrisParser PTerm
@@ -946,7 +946,7 @@ normalImplicit opts st syn = do
946946 return (bindList (PPi im) xt
947947 (bindList (PPi cl) cs sc))
948948
949−implicitPi opts st syn =
949+implicitPi opts st syn =
950950 autoImplicit opts st syn
951951 <|> defaultImplicit opts st syn
952952 <|> normalImplicit opts st syn
@@ -955,7 +955,7 @@ unboundPi opts st syn = do
955955 x <- opExpr syn
956956 (do binder <- bindsymbol opts st syn
957957 sc <- expr syn
958− return (PPi binder (sUN "__pi_arg") x sc))
958+ return (PPi binder (sUN "__pi_arg") NoFC x sc))
959959 <|> return x
960960
961961pi :: SyntaxInfo -> IdrisParser PTerm
@@ -987,11 +987,11 @@ ConstraintList ::=
987987 ;
988988@
989989-}
990−constraintList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
990+constraintList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
991991constraintList syn = try (constraintList1 syn)
992992 <|> return []
993993
994−constraintList1 :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
994+constraintList1 :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
995995constraintList1 syn = try (do lchar '('
996996 tys <- sepBy1 nexpr (lchar ',')
997997 lchar ')'
@@ -999,13 +999,13 @@ constraintList1 syn = try (do lchar '('
999999 return tys)
10001000 <|> try (do t <- opExpr (disallowImp syn)
10011001 reservedOp "=>"
1002− return [(defname, t)])
1002+ return [(defname, NoFC, t)])
10031003 <?> "type constraint list"
1004− where nexpr = try (do n <- fst <$> name; lchar ':'
1004+ where nexpr = try (do (n, fc) <- name; lchar ':'
10051005 e <- expr syn
1006− return (n, e))
1006+ return (n, fc, e))
10071007 <|> do e <- expr syn
1008− return (defname, e)
1008+ return (defname, NoFC, e)
10091009 defname = sMN 0 "constrarg"
10101010
10111011{- | Parses a type declaration list
@@ -1023,16 +1023,16 @@ FunctionSignatureList ::=
10231023 ;
10241024@
10251025-}
1026−typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1027−typeDeclList syn = try (sepBy1 (do x <- fst <$> fnName
1026+typeDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1027+typeDeclList syn = try (sepBy1 (do (x, xfc) <- fnName
10281028 lchar ':'
10291029 t <- typeExpr (disallowImp syn)
1030− return (x,t))
1030+ return (x, xfc, t))
10311031 (lchar ','))
1032− <|> do ns <- sepBy1 (fst <$> name) (lchar ',')
1032+ <|> do ns <- sepBy1 name (lchar ',')
10331033 lchar ':'
10341034 t <- typeExpr (disallowImp syn)
1035− return (map (\x -> (x, t)) ns)
1035+ return (map (\(x, xfc) -> (x, xfc, t)) ns)
10361036 <?> "type declaration list"
10371037
10381038{- | Parses a type declaration list with optional parameters
@@ -1047,17 +1047,17 @@ TypeOptDeclList ::=
10471047NameOrPlaceHolder ::= Name | '_';
10481048@
10491049-}
1050−tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
1051−tyOptDeclList syn = sepBy1 (do x <- nameOrPlaceholder
1050+tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, FC, PTerm)]
1051+tyOptDeclList syn = sepBy1 (do (x, fc) <- nameOrPlaceholder
10521052 t <- option Placeholder (do lchar ':'
10531053 expr syn)
1054− return (x,t))
1054+ return (x, fc, t))
10551055 (lchar ',')
10561056 <?> "type declaration list"
1057− where nameOrPlaceholder :: IdrisParser Name
1058− nameOrPlaceholder = fst <$> fnName
1057+ where nameOrPlaceholder :: IdrisParser (Name, FC)
1058+ nameOrPlaceholder = fnName
10591059 <|> do symbol "_"
1060− return (sMN 0 "underscore")
1060+ return (sMN 0 "underscore", NoFC)
10611061 <?> "name or placeholder"
10621062
10631063{- | 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
402402
403403{-* Syntax helpers-}
404404-- | Bind constraints to term
405−bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm
406−bindList b [] sc = sc
407−bindList b ((n, t):bs) sc = b n t (bindList b bs sc)
405+bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PTerm -> PTerm
406+bindList b [] sc = sc
407+bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)
408408
409409{- * Layout helpers -}
410410
src/Idris/Parser.hs+13−10
@@ -310,20 +310,20 @@ syntaxRule syn
310310 return $ PRef fc n'
311311 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =
312312 return $ PPatvar fc n'
313− fixBind rens (PLam fc n ty body)
314− | n `elem` userNames = liftM2 (PLam fc n) (fixBind rens ty) (fixBind rens body)
313+ fixBind rens (PLam fc n nfc ty body)
314+ | n `elem` userNames = liftM2 (PLam fc n nfc) (fixBind rens ty) (fixBind rens body)
315315 | otherwise =
316316 do ty' <- fixBind rens ty
317317 n' <- gensym n
318318 body' <- fixBind ((n,n'):rens) body
319− return $ PLam fc n' ty' body'
320− fixBind rens (PPi plic n argTy body)
321− | n `elem` userNames = liftM2 (PPi plic n) (fixBind rens argTy) (fixBind rens body)
319+ return $ PLam fc n' nfc ty' body'
320+ fixBind rens (PPi plic n nfc argTy body)
321+ | n `elem` userNames = liftM2 (PPi plic n nfc) (fixBind rens argTy) (fixBind rens body)
322322 | otherwise =
323323 do ty' <- fixBind rens argTy
324324 n' <- gensym n
325325 body' <- fixBind ((n,n'):rens) body
326− return $ (PPi plic n' ty' body')
326+ return $ (PPi plic n' nfc ty' body')
327327 fixBind rens (PLet fc n ty val body)
328328 | n `elem` userNames = liftM3 (PLet fc n)
329329 (fixBind rens ty)
@@ -555,12 +555,13 @@ Params ::=
555555params :: SyntaxInfo -> IdrisParser [PDecl]
556556params syn =
557557 do reserved "parameters"; lchar '('; ns <- typeDeclList syn; lchar ')'
558+ let ns' = [(n, ty) | (n, _, ty) <- ns]
558559 openBlock
559560 let pvars = syn_params syn
560− ds <- many (decl syn { syn_params = pvars ++ ns })
561+ ds <- many (decl syn { syn_params = pvars ++ ns' })
561562 closeBlock
562563 fc <- getFC
563− return [PParams fc ns (concat ds)]
564+ return [PParams fc ns' (concat ds)]
564565 <?> "parameters declaration"
565566
566567{- | Parses a mutual declaration (for mutually recursive functions)
@@ -659,13 +660,14 @@ class_ syn = do (doc, argDocs, acc)
659660 return (doc, argDocs, acc))
660661 fc <- getFC
661662 cons <- constraintList syn
663+ let cons' = [(c, ty) | (c, _, ty) <- cons]
662664 n_in <- fst <$> fnName
663665 let n = expandNS syn n_in
664666 cs <- many carg
665667 fds <- option (map fst cs) fundeps
666668 ds <- option [] (classBlock syn)
667669 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]
669671 <?> "type-class declaration"
670672 where
671673 fundeps :: IdrisParser [Name]
@@ -696,12 +698,13 @@ instance_ syn = do (doc, argDocs)
696698 fc <- getFC
697699 en <- optional instanceName
698700 cs <- constraintList syn
701+ let cs' = [(c, ty) | (c, _, ty) <- cs]
699702 cn <- fst <$> fnName
700703 args <- many (simpleExpr syn)
701704 let sc = PApp fc (PRef fc cn) (map pexp args)
702705 let t = bindList (PPi constraint) cs sc
703706 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]
705708 <?> "instance declaration"
706709 where instanceName :: IdrisParser Name
707710 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
128128mkPE_TyDecl ist args ty = mkty args ty
129129 where
130130 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)
132132 mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)
133133 | concreteClass ist t = mkty xs sc
134134 | classConstraint ist t
135− = PPi constraint n (delab ist (generaliseIn t)) (mkty xs sc)
136− | otherwise = PPi impl 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 NoFC (delab ist (generaliseIn t)) (mkty xs sc)
137137
138138 mkty (_ : xs) t
139139 = mkty xs t
src/Idris/REPL.hs+1−1
@@ -906,7 +906,7 @@ process fn (Check (PRef _ n))
906906 (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))
907907 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
908908 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)
910910 = let current = text " " <>
911911 (case n of
912912 MN _ _ -> text "_"