452b3c6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2445 from david-christiansen/parser-highlights

Highlighting for pairs, lists and sigmas

commit452b3c627fa2ebff9ca333395f7181779f5a920d authorDavid Christiansen <david@davidchristiansen.dk> dateSat 18 Jul 2015, 00:36 (11 years ago) parent5da0d60 bc2915c

36 files changed+593−568

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+113−112 src/Idris/AbsSyntaxTree.hs+70−70 src/Idris/CaseSplit.hs+24−24 src/Idris/Coverage.hs+17−17 src/Idris/DSL.hs+25−25 src/Idris/DeepSeq.hs+5−5 src/Idris/Delaborate.hs+22−22 src/Idris/Docs.hs+5−5 src/Idris/Elab/AsPat.hs+1−1 src/Idris/Elab/Class.hs+15−15 src/Idris/Elab/Clause.hs+17−17 src/Idris/Elab/Data.hs+23−23 src/Idris/Elab/Instance.hs+12−12 src/Idris/Elab/Provider.hs+1−1 src/Idris/Elab/Record.hs+13−13 src/Idris/Elab/Term.hs+66−62 src/Idris/Elab/Transform.hs+1−1 src/Idris/Elab/Utils.hs+1−1 src/Idris/Elab/Value.hs+4−4 src/Idris/ElabDecls.hs+2−2 src/Idris/ElabQuasiquote.hs+5−5 src/Idris/Error.hs+4−4 src/Idris/IBC.hs+30−22 src/Idris/IdrisDoc.hs+4−4 src/Idris/Interactive.hs+5−5 src/Idris/ParseData.hs+1−1 src/Idris/ParseExpr.hs+71−65 src/Idris/ParseHelpers.hs+6 src/Idris/ParseOps.hs+5−5 src/Idris/Parser.hs+7−7 src/Idris/PartialEval.hs+3−3 src/Idris/ProofSearch.hs+4−4 src/Idris/Prover.hs+3−3 src/Idris/Providers.hs+1−1 src/Idris/REPL.hs+6−6 src/Idris/REPLParser.hs+1−1

src/Idris/AbsSyntax.hs+113−112

@@ -998,15 +998,15 @@ expandParams dec ps ns infs tm = en tm

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

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

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

1001− en (PDPair f p (PRef f' n) t r)

1001+ en (PDPair f hls p (PRef f' fcs n) t r)

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

10031003 = let n' = mkShadow n in

1004− PDPair f p (PRef f' n') (en t) (en (shadow n n' r))

1004+ PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))

10051005 en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

10061006 en (PTyped l r) = PTyped (en l) (en r)

1007− en (PPair f p l r) = PPair f p (en l) (en r)

1008− en (PDPair f p l t r) = PDPair f p (en l) (en t) (en r)

1009− en (PAlternative ms a as) = PAlternative ms a (map en as)

1007+ en (PPair f hls p l r) = PPair f hls p (en l) (en r)

1008+ en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)

1009+ en (PAlternative ns a as) = PAlternative ns a (map en as)

10101010 en (PHidden t) = PHidden (en t)

10111011 en (PUnifyLog t) = PUnifyLog (en t)

10121012 en (PDisamb ds t) = PDisamb ds (en t)

@@ -1017,27 +1017,27 @@ expandParams dec ps ns infs tm = en tm

10171017

10181018 en (PQuote (Var n))

10191019 | n `nselem` ns = PQuote (Var (dec n))

1020− en (PApp fc (PInferRef fc' n) as)

1021− | n `nselem` ns = PApp fc (PInferRef fc' (dec n))

1022− (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

1023− en (PApp fc (PRef fc' n) as)

1024− | n `elem` infs = PApp fc (PInferRef fc' (dec n))

1025− (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

1026− | n `nselem` ns = PApp fc (PRef fc' (dec n))

1027− (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

1028− en (PAppBind fc (PRef fc' n) as)

1029− | n `elem` infs = PAppBind fc (PInferRef fc' (dec n))

1030− (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

1031− | n `nselem` ns = PAppBind fc (PRef fc' (dec n))

1032− (map (pexp . (PRef fc)) (map fst ps) ++ (map (fmap en) as))

1033− en (PRef fc n)

1034− | n `elem` infs = PApp fc (PInferRef fc (dec n))

1035− (map (pexp . (PRef fc)) (map fst ps))

1036− | n `nselem` ns = PApp fc (PRef fc (dec n))

1037− (map (pexp . (PRef fc)) (map fst ps))

1038− en (PInferRef fc n)

1039− | n `nselem` ns = PApp fc (PInferRef fc (dec n))

1040− (map (pexp . (PRef fc)) (map fst ps))

1020+ en (PApp fc (PInferRef fc' hl n) as)

1021+ | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1022+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1023+ en (PApp fc (PRef fc' hl n) as)

1024+ | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1025+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1026+ | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1027+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1028+ en (PAppBind fc (PRef fc' hl n) as)

1029+ | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1030+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1031+ | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1032+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1033+ en (PRef fc hl n)

1034+ | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1035+ (map (pexp . (PRef fc hl)) (map fst ps))

1036+ | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1037+ (map (pexp . (PRef fc hl)) (map fst ps))

1038+ en (PInferRef fc hl n)

1039+ | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1040+ (map (pexp . (PRef fc hl)) (map fst ps))

10411041 en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

10421042 en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

10431043 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

@@ -1103,10 +1103,10 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

11031103

11041104 removeBound lhs ns = ns \\ nub (bnames lhs)

11051105

1106− bnames (PRef _ n) = [n]

1106+ bnames (PRef _ _ n) = [n]

11071107 bnames (PApp _ _ args) = concatMap bnames (map getTm args)

1108− bnames (PPair _ _ l r) = bnames l ++ bnames r

1109− bnames (PDPair _ _ l Placeholder r) = bnames l ++ bnames r

1108+ bnames (PPair _ _ _ l r) = bnames l ++ bnames r

1109+ bnames (PDPair _ _ _ l Placeholder r) = bnames l ++ bnames r

11101110 bnames _ = []

11111111

11121112-- | Expands parameters defined in parameter and where blocks inside of declarations

@@ -1162,7 +1162,7 @@ mapsnd f (x, t) = (x, f t)

11621162getPriority :: IState -> PTerm -> Int

11631163getPriority i tm = 1 -- pri tm

11641164 where

1165− pri (PRef _ n) =

1165+ pri (PRef _ _ n) =

11661166 case lookupP n (tt_ctxt i) of

11671167 ((P (DCon _ _ _) _ _):_) -> 1

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

@@ -1175,9 +1175,9 @@ getPriority i tm = 1 -- pri tm

11751175 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

11761176 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

11771177 pri (PTyped l r) = pri l

1178− pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))

1179− pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1180− pri (PAlternative ms a as) = maximum (map pri as)

1178+ pri (PPair _ _ _ l r) = max 1 (max (pri l) (pri r))

1179+ pri (PDPair _ _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

1180+ pri (PAlternative _ a as) = maximum (map pri as)

11811181 pri (PConstant _ _) = 0

11821182 pri Placeholder = 1

11831183 pri _ = 3

@@ -1288,20 +1288,20 @@ addUsingConstraints syn fc t

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

12891289 | otherwise = doAdd cs ns t

12901290

1291− mkConst c args = PApp fc (PRef fc c)

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

1291+ mkConst c args = PApp fc (PRef fc [] c)

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

12931293

12941294 getConstraints (PPi (Constraint _ _) _ _ c sc)

12951295 = getcapp c ++ getConstraints sc

12961296 getConstraints (PPi _ _ _ c sc) = getConstraints sc

12971297 getConstraints _ = []

12981298

1299− getcapp (PApp _ (PRef _ c) args)

1299+ getcapp (PApp _ (PRef _ _ c) args)

13001300 = do ns <- mapM getName args

13011301 return (UConstraint c ns)

13021302 getcapp _ = []

13031303

1304− getName (PExp _ _ _ (PRef _ n)) = return n

1304+ getName (PExp _ _ _ (PRef _ _ n)) = return n

13051305 getName _ = []

13061306

13071307-- Add implicit bindings from using block, and bind any missing names

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

14581458 imps True (n:env) sc

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

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

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

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

14621462 _ -> [])

14631463 (decls, ns) <- get -- ignore decls in HO types

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

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

14661466 imps True (n:env) sc

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

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

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

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

14701470 _ -> [])

14711471 (decls, ns) <- get -- ignore decls in HO types

14721472 put (PConstraint 10 l n Placeholder : decls,

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

14741474 imps True (n:env) sc

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

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

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

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

14781478 _ -> [])

14791479 (decls, ns) <- get -- ignore decls in HO types

14801480 put (PTacImplicit 10 l n scr Placeholder : decls,

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

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

14871487 imps top env (PTyped l r)

14881488 = imps top env l

1489− imps top env (PPair _ _ l r)

1489+ imps top env (PPair _ _ _ l r)

14901490 = do (decls, ns) <- get

14911491 let isn = namesIn uvars ist l ++ namesIn uvars ist r

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

1493− imps top env (PDPair _ _ (PRef _ n) t r)

1493+ imps top env (PDPair _ _ _ (PRef _ _ n) t r)

14941494 = do (decls, ns) <- get

14951495 let isn = nub (namesIn uvars ist t ++ namesIn uvars ist r) \\ [n]

14961496 put (decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

1497− imps top env (PDPair _ _ l t r)

1497+ imps top env (PDPair _ _ _ l t r)

14981498 = do (decls, ns) <- get

14991499 let isn = namesIn uvars ist l ++ namesIn uvars ist t ++

15001500 namesIn uvars ist r

@@ -1545,10 +1545,10 @@ addImpl' inpat env infns imp_meths ist ptm

15451545 = mkUniqueNames env [] (ai False (zip env (repeat Nothing)) [] ptm)

15461546 where

15471547 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1548− ai qq env ds (PRef fc f)

1549− | f `elem` infns = PInferRef fc f

1548+ ai qq env ds (PRef fc fcs f)

1549+ | f `elem` infns = PInferRef fc fcs f

15501550 | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f fc ds []

1551− ai qq env ds (PHidden (PRef fc f))

1551+ ai qq env ds (PHidden (PRef fc hl f))

15521552 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f fc ds [])

15531553 ai qq env ds (PRewrite fc l r g)

15541554 = let l' = ai qq env ds l

@@ -1559,24 +1559,24 @@ addImpl' inpat env infns imp_meths ist ptm

15591559 = let l' = ai qq env ds l

15601560 r' = ai qq env ds r in

15611561 PTyped l' r'

1562− ai qq env ds (PPair fc p l r)

1562+ ai qq env ds (PPair fc hls p l r)

15631563 = let l' = ai qq env ds l

15641564 r' = ai qq env ds r in

1565− PPair fc p l' r'

1566− ai qq env ds (PDPair fc p l t r)

1565+ PPair fc hls p l' r'

1566+ ai qq env ds (PDPair fc hls p l t r)

15671567 = let l' = ai qq env ds l

15681568 t' = ai qq env ds t

15691569 r' = ai qq env ds r in

1570− PDPair fc p l' t' r'

1570+ PDPair fc hls p l' t' r'

15711571 ai qq env ds (PAlternative ms a as)

15721572 = let as' = map (ai qq env ds) as in

15731573 PAlternative ms a as'

15741574 ai qq env _ (PDisamb ds' as) = ai qq env ds' as

1575− ai qq env ds (PApp fc (PInferRef ffc f) as)

1575+ ai qq env ds (PApp fc (PInferRef ffc hl f) as)

15761576 = let as' = map (fmap (ai qq env ds)) as in

1577− PApp fc (PInferRef ffc f) as'

1578− ai qq env ds (PApp fc ftm@(PRef ffc f) as)

1579− | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc f) as)

1577+ PApp fc (PInferRef ffc hl f) as'

1578+ ai qq env ds (PApp fc ftm@(PRef ffc hl f) as)

1579+ | f `elem` infns = ai qq env ds (PApp fc (PInferRef ffc hl f) as)

15801580 | not (f `elem` map fst env)

15811581 = let as' = map (fmap (ai qq env ds)) as in

15821582 handleErr $ aiFn inpat False qq imp_meths ist fc f ffc ds as'

@@ -1608,15 +1608,16 @@ addImpl' inpat env infns imp_meths ist ptm

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

16091609 PLam fc n nfc ty' sc'

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

1611− (PCase fc (PRef fc (sMN 0 "lamp") )

1612− [(PRef fc n, sc)]))

1611+ (PCase fc (PRef fc [] (sMN 0 "lamp") )

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

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

16141614 = case lookupDef n (tt_ctxt ist) of

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

16161616 val' = ai qq env ds val

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

16181618 PLet fc n nfc ty' val' sc'

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

1619+ defs ->

1620+ ai qq env ds (PCase fc val [(PRef fc [] n, sc)])

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

16211622 = let ty' = ai qq env ds ty

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

@@ -1674,7 +1675,7 @@ aiFn inpat True qq imp_meths ist fc f ffc ds []

16741675 vname _ = False

16751676

16761677aiFn inpat expat qq imp_meths ist fc f ffc ds as

1677− | f `elem` primNames = Right $ PApp fc (PRef ffc f) as

1678+ | f `elem` primNames = Right $ PApp fc (PRef ffc [ffc] f) as

16781679aiFn inpat expat qq imp_meths ist fc f ffc ds as

16791680 -- This is where namespaces get resolved by adding PAlternative

16801681 = do let ns = lookupCtxtName f (idris_implicits ist)

@@ -1683,13 +1684,13 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

16831684 [] -> nh

16841685 x -> x

16851686 case ns' of

1686− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc (isImpName f f')) (insertImpl ns as)

1687+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f')) (insertImpl ns as)

16871688 [] -> if f `elem` (map fst (idris_metavars ist))

1688− then Right $ PApp fc (PRef ffc f) as

1689− else Right $ mkPApp fc (length as) (PRef ffc f) as

1689+ then Right $ PApp fc (PRef ffc [ffc] f) as

1690+ else Right $ mkPApp fc (length as) (PRef ffc [ffc] f) as

16901691 alts -> Right $

16911692 PAlternative [] (ExactlyOne True) $

1692− map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc (isImpName f f'))

1693+ map (\(f', ns) -> mkPApp fc (length ns) (PRef ffc [ffc] (isImpName f f'))

16931694 (insertImpl ns as)) alts

16941695 where

16951696 -- if the name is in imp_meths, we should actually refer to the bound

@@ -1737,7 +1738,7 @@ aiFn inpat expat qq imp_meths ist fc f ffc ds as

17371738 case find n imps [] of

17381739 Just (tm, imps') ->

17391740 PImp p False l n tm : insImpAcc (M.insert n tm pnas) ps given imps'

1740− Nothing -> let ph = if f `elem` imp_meths then PRef fc n else Placeholder in

1741+ Nothing -> let ph = if f `elem` imp_meths then PRef fc [] n else Placeholder in

17411742 PImp p True l n ph :

17421743 insImpAcc (M.insert n ph pnas) ps given imps

17431744 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

@@ -1780,14 +1781,14 @@ expArg _ = False

17801781stripLinear :: IState -> PTerm -> PTerm

17811782stripLinear i tm = evalState (sl tm) [] where

17821783 sl :: PTerm -> State [Name] PTerm

1783− sl (PRef fc f)

1784+ sl (PRef fc hl f)

17841785 | (_:_) <- lookupTy f (tt_ctxt i)

1785− = return $ PRef fc f

1786+ = return $ PRef fc hl f

17861787 | otherwise = do ns <- get

17871788 if (f `elem` ns)

1788− then return $ PHidden (PRef fc f) -- Placeholder

1789+ then return $ PHidden (PRef fc hl f) -- Placeholder

17891790 else do put (f : ns)

1790− return (PRef fc f)

1791+ return (PRef fc hl f)

17911792 sl (PPatvar fc f)

17921793 = do ns <- get

17931794 if (f `elem` ns)

@@ -1803,14 +1804,14 @@ stripLinear i tm = evalState (sl tm) [] where

18031804 as' <- slAlts ns as

18041805 return (a' : as')

18051806 slAlts ns [] = return []

1806− sl (PPair fc p l r) = do l' <- sl l; r' <- sl r; return (PPair fc p l' r')

1807− sl (PDPair fc p l t r) = do l' <- sl l

1808− t' <- sl t

1809− r' <- sl r

1810− return (PDPair fc p l' t' r')

1807+ sl (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')

1808+ sl (PDPair fc hls p l t r) = do l' <- sl l

1809+ t' <- sl t

1810+ r' <- sl r

1811+ return (PDPair fc hls p l' t' r')

18111812 sl (PApp fc fn args) = do fn' <- case fn of

18121813 -- Just the args, fn isn't matchable as a var

1813− PRef _ _ -> return fn

1814+ PRef _ _ _ -> return fn

18141815 t -> sl t

18151816 args' <- mapM slA args

18161817 return $ PApp fc fn' args'

@@ -1832,14 +1833,14 @@ stripLinear i tm = evalState (sl tm) [] where

18321833stripUnmatchable :: IState -> PTerm -> PTerm

18331834stripUnmatchable i (PApp fc fn args) = PApp fc fn (fmap (fmap su) args) where

18341835 su :: PTerm -> PTerm

1835− su tm@(PRef fc f)

1836+ su tm@(PRef fc hl f)

18361837 | (Bind n (Pi _ t _) sc :_) <- lookupTy f (tt_ctxt i)

18371838 = Placeholder

18381839 | (TType _ : _) <- lookupTy f (tt_ctxt i)

18391840 = PHidden tm

18401841 | (UType _ : _) <- lookupTy f (tt_ctxt i)

18411842 = PHidden tm

1842− su (PApp fc f@(PRef _ fn) args)

1843+ su (PApp fc f@(PRef _ _ fn) args)

18431844 -- here we use canBeDConName because the impossible pattern

18441845 -- check will not necessarily fully resolve constructor names,

18451846 -- and these bare names will otherwise get in the way of

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

18521853 = let alts' = filter (/= Placeholder) (map su alts) in

18531854 if null alts' then Placeholder

18541855 else PAlternative ms b alts'

1855− su (PPair fc p l r) = PPair fc p (su l) (su r)

1856− su (PDPair fc p l t r) = PDPair fc p (su l) (su t) (su r)

1856+ su (PPair fc hls p l r) = PPair fc hls p (su l) (su r)

1857+ su (PDPair fc hls p l t r) = PDPair fc hls p (su l) (su t) (su r)

18571858 su t@(PLam fc _ _ _ _) = PHidden t

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

18591860 su t@(PConstant _ c) | isTypeConst c = PHidden t

@@ -1877,9 +1878,8 @@ mkPApp fc a f as = let rest = drop a as in

18771878-- FIXME: It's possible that this really has to happen after elaboration

18781879

18791880findStatics :: IState -> PTerm -> (PTerm, [Bool])

1880−findStatics ist tm = trace (show tm) $

1881− let (ns, ss) = fs tm in

1882− runState (pos ns ss tm) []

1881+findStatics ist tm = let (ns, ss) = fs tm

1882+ in runState (pos ns ss tm) []

18831883 where fs (PPi p n fc t sc)

18841884 | Static <- pstatic p

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

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

19301930 fullApp x = x

19311931

19321932 match' x y = match (fullApp x) (fullApp y)

1933− match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'

1933+ match (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x]) x'

19341934 | fi == txt "fromInteger" && b == txt "builtins",

19351935 PConstant _ (I _) <- getTm x = match (getTm x) x'

1936− match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])

1936+ match x' (PApp _ (PRef _ _ (NS (UN fi) [b])) [_,_,x])

19371937 | fi == txt "fromInteger" && b == txt "builtins",

19381938 PConstant _ (I _) <- getTm x = match (getTm x) x'

1939− match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'

1940− match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')

1939+ match (PApp _ (PRef _ _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'

1940+ match x (PApp _ (PRef _ _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')

19411941 match (PApp _ f args) (PApp _ f' args')

19421942 | length args == length args'

19431943 = do mf <- match' f f'

19441944 ms <- zipWithM matchArg args args'

19451945 return (mf ++ concat ms)

1946− match (PRef f n) (PApp _ x []) = match (PRef f n) x

1947− match (PPatvar f n) xr = match (PRef f n) xr

1948− match xr (PPatvar f n) = match xr (PRef f n)

1949− match (PApp _ x []) (PRef f n) = match x (PRef f n)

1950− match (PRef _ n) tm@(PRef _ n')

1946+ match (PRef f hl n) (PApp _ x []) = match (PRef f hl n) x

1947+ match (PPatvar f n) xr = match (PRef f [f] n) xr

1948+ match xr (PPatvar f n) = match xr (PRef f [f] n)

1949+ match (PApp _ x []) (PRef f hl n) = match x (PRef f hl n)

1950+ match (PRef _ _ n) tm@(PRef _ _ n')

19511951 | n == n' && not names &&

19521952 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

19531953 || tm == Placeholder)

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

19561956 | n == n' || n == dropNS n' || dropNS n == n' = return []

19571957 where dropNS (NS n _) = n

19581958 dropNS n = n

1959− match (PRef _ n) tm

1959+ match (PRef _ _ n) tm

19601960 | not names && (not (isConName n (tt_ctxt i) ||

19611961 isFnName n (tt_ctxt i)) || tm == Placeholder)

19621962 = return [(n, tm)]

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

19691969 return (ml ++ mr)

19701970 match (PTyped l r) x = match l x

19711971 match x (PTyped l r) = match x l

1972− match (PPair _ _ l r) (PPair _ _ l' r') = do ml <- match' l l'

1973− mr <- match' r r'

1974− return (ml ++ mr)

1975− match (PDPair _ _ l t r) (PDPair _ _ l' t' r') = do ml <- match' l l'

1976− mt <- match' t t'

1977− mr <- match' r r'

1978− return (ml ++ mt ++ mr)

1972+ match (PPair _ _ _ l r) (PPair _ _ _ l' r') = do ml <- match' l l'

1973+ mr <- match' r r'

1974+ return (ml ++ mr)

1975+ match (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r') = do ml <- match' l l'

1976+ mt <- match' t t'

1977+ mr <- match' r r'

1978+ return (ml ++ mt ++ mr)

19791979 match (PAlternative _ a as) (PAlternative _ a' as')

19801980 = do ms <- zipWithM match' as as'

19811981 return (concat ms)

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

19861986 _ -> LeftErr (a, b)

19871987 match (PCase _ _ _) _ = return [] -- lifted out

19881988 match (PMetavar _ _) _ = return [] -- modified

1989− match (PInferRef _ _) _ = return [] -- modified

1989+ match (PInferRef _ _ _) _ = return [] -- modified

19901990 match (PQuote _) _ = return []

19911991 match (PProof _) _ = return []

19921992 match (PTactics _) _ = return []

@@ -2044,13 +2044,13 @@ substMatch n = substMatchShadow n []

20442044

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

20462046substMatchShadow n shs tm t = sm shs t where

2047− sm xs (PRef _ n') | n == n' = tm

2047+ sm xs (PRef _ _ n') | n == n' = tm

20482048 sm xs (PLam fc x xfc t sc) = PLam fc x xfc (sm xs t) (sm xs sc)

20492049 sm xs (PPi p x fc t sc)

20502050 | x `elem` xs

20512051 = let x' = nextName x in

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

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

2052+ PPi p x' fc (sm (x':xs) (substMatch x (PRef emptyFC [] x') t))

2053+ (sm (x':xs) (substMatch x (PRef emptyFC [] x') sc))

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

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

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

@@ -2058,8 +2058,8 @@ substMatchShadow n shs tm t = sm shs t where

20582058 sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

20592059 (fmap (sm xs) tm)

20602060 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

2061− sm xs (PPair f p x y) = PPair f p (sm xs x) (sm xs y)

2062− sm xs (PDPair f p x t y) = PDPair f p (sm xs x) (sm xs t) (sm xs y)

2061+ sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)

2062+ sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)

20632063 sm xs (PAlternative ms a as) = PAlternative ms a (map (sm xs) as)

20642064 sm xs (PHidden x) = PHidden (sm xs x)

20652065 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

@@ -2072,7 +2072,7 @@ substMatchShadow n shs tm t = sm shs t where

20722072

20732073shadow :: Name -> Name -> PTerm -> PTerm

20742074shadow n n' t = sm t where

2075− sm (PRef fc x) | n == x = PRef fc n'

2075+ sm (PRef fc hl x) | n == x = PRef fc hl n'

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

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

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

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

20852085 sm (PIfThenElse fc c t f) = PIfThenElse fc (sm c) (sm t) (sm f)

20862086 sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

20872087 sm (PTyped x y) = PTyped (sm x) (sm y)

2088− sm (PPair f p x y) = PPair f p (sm x) (sm y)

2089− sm (PDPair f p x t y) = PDPair f p (sm x) (sm t) (sm y)

2088+ sm (PPair f hls p x y) = PPair f hls p (sm x) (sm y)

2089+ sm (PDPair f hls p x t y) = PDPair f hls p (sm x) (sm t) (sm y)

20902090 sm (PAlternative ms a as) = PAlternative ms a (map sm as)

20912091 sm (PTactics ts) = PTactics (map (fmap sm) ts)

20922092 sm (PProof ts) = PProof (map (fmap sm) ts)

@@ -2174,10 +2174,10 @@ mkUniqueNames env shadows tm

21742174 return $! PCase fc t' alts'

21752175 mkUniq nmap (PIfThenElse fc c t f)

21762176 = liftM3 (PIfThenElse fc) (mkUniq nmap c) (mkUniq nmap t) (mkUniq nmap f)

2177− mkUniq nmap (PPair fc p l r)

2177+ mkUniq nmap (PPair fc hls p l r)

21782178 = do l' <- mkUniq nmap l; r' <- mkUniq nmap r

2179− return $! PPair fc p l' r'

2180− mkUniq nmap (PDPair fc p (PRef fc' n) t sc)

2179+ return $! PPair fc hls p l' r'

2180+ mkUniq nmap (PDPair fc hls p (PRef fc' hls' n) t sc)

21812181 | t /= Placeholder

21822182 = do env <- get

21832183 (n', sc') <- if n `S.member` env

@@ -2188,10 +2188,10 @@ mkUniqueNames env shadows tm

21882188 let nmap' = M.insert n n' nmap

21892189 t' <- mkUniq nmap t

21902190 sc'' <- mkUniq nmap' sc'

2191− return $! PDPair fc p (PRef fc' n') t' sc''

2192− mkUniq nmap (PDPair fc p l t r)

2191+ return $! PDPair fc hls p (PRef fc' hls' n') t' sc''

2192+ mkUniq nmap (PDPair fc hls p l t r)

21932193 = do l' <- mkUniq nmap l; t' <- mkUniq nmap t; r' <- mkUniq nmap r

2194− return $! PDPair fc p l' t' r'

2194+ return $! PDPair fc hls p l' t' r'

21952195 mkUniq nmap (PAlternative ns b as)

21962196 -- store the nmap and defer the rest until we've pruned the set

21972197 -- during elaboration

@@ -2207,3 +2207,4 @@ mkUniqueNames env shadows tm

22072207 where

22082208 shadowAll [] t = t

22092209 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2210+

src/Idris/AbsSyntaxTree.hs+70−70

@@ -813,7 +813,7 @@ updateN _ n = n

813813updateNs :: [(Name, Name)] -> PTerm -> PTerm

814814updateNs [] t = t

815815updateNs ns t = mapPT updateRef t

816− where updateRef (PRef fc f) = PRef fc (updateN ns f)

816+ where updateRef (PRef fc fcs f) = PRef fc fcs (updateN ns f)

817817 updateRef t = t

818818

819819-- updateDNs :: [(Name, Name)] -> PDecl -> PDecl

@@ -831,8 +831,8 @@ data PunInfo = IsType | IsTerm | TypeOrTerm deriving (Eq, Show, Data, Typeable)

831831

832832-- | High level language terms

833833data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level language

834− | PRef FC Name -- ^ A reference to a variable

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

834+ | PRef FC [FC] Name -- ^ A reference to a variable. The FC is its precise source location for highlighting. The list of FCs is a collection of additional highlighting locations.

835+ | PInferRef FC [FC] Name -- ^ A name to be defined later

836836 | PPatvar FC Name -- ^ A pattern variable

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

838838 | PPi Plicity Name FC PTerm PTerm -- ^ (n : t1) -> t2, where the FC is for the precise location of the variable

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

847847 | PTrue FC PunInfo -- ^ Unit type..?

848848 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

849849 | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

850− | PPair FC PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration)

851− | PDPair FC PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration)

850+ | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

851+ | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

852852 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

853853 | PAlternative [(Name, Name)] PAltType [PTerm] -- ^ (| A, B, C|). Includes unapplied unique name mappings for mkUniqueNames.

854854 | PHidden PTerm -- ^ Irrelevant or hidden pattern

@@ -885,8 +885,8 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

885885-- for semantic source highlighting, so they can be treated specially.

886886mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm

887887mapPTermFC f g (PQuote q) = PQuote q

888−mapPTermFC f g (PRef fc n) = PRef (g fc) n

889−mapPTermFC f g (PInferRef fc n) = PInferRef (g fc) n

888+mapPTermFC f g (PRef fc fcs n) = PRef (g fc) (map g fcs) n

889+mapPTermFC f g (PInferRef fc fcs n) = PInferRef (g fc) (map g fcs) n

890890mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n

891891mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)

892892mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

@@ -901,8 +901,8 @@ mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r)

901901mapPTermFC f g (PTrue fc info) = PTrue (f fc) info

902902mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)

903903mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)

904−mapPTermFC f g (PPair fc info t1 t2) = PPair (f fc) info (mapPTermFC f g t1) (mapPTermFC f g t2)

905−mapPTermFC f g (PDPair fc info t1 t2 t3) = PDPair (f fc) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

904+mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)

905+mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

906906mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

907907mapPTermFC f g (PAlternative ns ty ts) = PAlternative ns ty (map (mapPTermFC f g) ts)

908908mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

@@ -951,8 +951,8 @@ mapPT f t = f (mpt t) where

951951 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

952952 mpt (PIfThenElse fc c t e) = PIfThenElse fc (mapPT f c) (mapPT f t) (mapPT f e)

953953 mpt (PTyped l r) = PTyped (mapPT f l) (mapPT f r)

954− mpt (PPair fc p l r) = PPair fc p (mapPT f l) (mapPT f r)

955− mpt (PDPair fc p l t r) = PDPair fc p (mapPT f l) (mapPT f t) (mapPT f r)

954+ mpt (PPair fc hls p l r) = PPair fc hls p (mapPT f l) (mapPT f r)

955+ mpt (PDPair fc hls p l t r) = PDPair fc hls p (mapPT f l) (mapPT f t) (mapPT f r)

956956 mpt (PAlternative ns a as) = PAlternative ns a (map (mapPT f) as)

957957 mpt (PHidden t) = PHidden (mapPT f t)

958958 mpt (PDoBlock ds) = PDoBlock (map (fmap (mapPT f)) ds)

@@ -1105,8 +1105,8 @@ type PArg = PArg' PTerm

11051105-- | Get the highest FC in a term, if one exists

11061106highestFC :: PTerm -> Maybe FC

11071107highestFC (PQuote _) = Nothing

1108−highestFC (PRef fc _) = Just fc

1109−highestFC (PInferRef fc _) = Just fc

1108+highestFC (PRef fc _ _) = Just fc

1109+highestFC (PInferRef fc _ _) = Just fc

11101110highestFC (PPatvar fc _) = Just fc

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

11121112highestFC (PPi _ _ _ _ _) = Nothing

@@ -1120,8 +1120,8 @@ highestFC (PIfThenElse fc _ _ _) = Just fc

11201120highestFC (PTrue fc _) = Just fc

11211121highestFC (PResolveTC fc) = Just fc

11221122highestFC (PRewrite fc _ _ _) = Just fc

1123−highestFC (PPair fc _ _ _) = Just fc

1124−highestFC (PDPair fc _ _ _ _) = Just fc

1123+highestFC (PPair fc _ _ _ _) = Just fc

1124+highestFC (PDPair fc _ _ _ _ _) = Just fc

11251125highestFC (PAs fc _ _) = Just fc

11261126highestFC (PAlternative _ _ args) =

11271127 case mapMaybe highestFC args of

@@ -1293,10 +1293,10 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

12931293 symCompare (SimpleExpr _) (Expr _) = GT

12941294 symCompare (SimpleExpr e1) (SimpleExpr e2) = compare e1 e2

12951295

1296−initDSL = DSL (PRef f (sUN ">>="))

1297− (PRef f (sUN "return"))

1298− (PRef f (sUN "<*>"))

1299− (PRef f (sUN "pure"))

1296+initDSL = DSL (PRef f [] (sUN ">>="))

1297+ (PRef f [] (sUN "return"))

1298+ (PRef f [] (sUN "<*>"))

1299+ (PRef f [] (sUN "pure"))

13001300 Nothing

13011301 Nothing

13021302 Nothing

@@ -1351,11 +1351,11 @@ inferCon = sMN 0 "__infer"

13511351inferDecl = PDatadecl inferTy NoFC

13521352 (PType bi)

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

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

1355− (PRef bi inferTy)), bi, [])]

1354+ PPi expl (sMN 0 "ival") NoFC (PRef bi [] (sMN 0 "iType"))

1355+ (PRef bi [] inferTy)), bi, [])]

13561356inferOpts = []

13571357

1358−infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

1358+infTerm t = PApp bi (PRef bi [] inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]

13591359infP = P (TCon 6 0) inferTy (TType (UVal 0))

13601360

13611361getInferTerm, getInferType :: Term -> Term

@@ -1406,15 +1406,15 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

14061406 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

14071407

14081408eqDecl = PDatadecl eqTy NoFC (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

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

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

14101410 (PType bi)))

14111411 [(reflDoc, reflParamDoc,

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

1413− PPi impl (n "x") NoFC (PRef bi (n "A"))

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

1413+ PPi impl (n "x") NoFC (PRef bi [] (n "A"))

1414+ (PApp bi (PRef bi [] eqTy) [pimp (n "A") Placeholder False,

14151415 pimp (n "B") Placeholder False,

1416− pexp (PRef bi (n "x")),

1417− pexp (PRef bi (n "x"))])), bi, [])]

1416+ pexp (PRef bi [] (n "x")),

1417+ pexp (PRef bi [] (n "x"))])), bi, [])]

14181418 where n a = sUN a

14191419 reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $

14201420 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

@@ -1535,7 +1535,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

15351535 prettySe d p bnd e

15361536 | Just str <- slist d p bnd e = depth d $ str

15371537 | Just n <- snat d p e = depth d $ annotate (AnnData "Nat" "") (text (show n))

1538− prettySe d p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1538+ prettySe d p bnd (PRef fc _ n) = prettyName True (ppopt_impl ppo) bnd n

15391539 prettySe d p bnd (PLam fc n nfc ty sc) =

15401540 depth d . bracket p startPrec . group . align . hang 2 $

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

@@ -1582,7 +1582,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

15821582 -- This case preserves the behavior of the former constructor PEq.

15831583 -- It should be removed if feasible when the pretty-printing of infix

15841584 -- operators in general is improved.

1585− prettySe d p bnd (PApp _ (PRef _ n) [lt, rt, l, r])

1585+ prettySe d p bnd (PApp _ (PRef _ _ n) [lt, rt, l, r])

15861586 | n == eqTy, ppopt_impl ppo =

15871587 depth d . bracket p eqPrec $

15881588 enclose lparen rparen eq <+>

@@ -1594,13 +1594,13 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

15941594 where eq = annName eqTy (text "=")

15951595 eqPrec = startPrec

15961596 prettyTerm = prettySe (decD d) (eqPrec + 1) bnd

1597− prettySe d p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1597+ prettySe d p bnd (PApp _ (PRef _ _ f) args) -- normal names, no explicit args

15981598 | UN nm <- basename f

15991599 , not (ppopt_impl ppo) && null (getShowArgs args) =

16001600 prettyName True (ppopt_impl ppo) bnd f

1601− prettySe d p bnd (PAppBind _ (PRef _ f) [])

1601+ prettySe d p bnd (PAppBind _ (PRef _ _ f) [])

16021602 | not (ppopt_impl ppo) = text "!" <> prettyName True (ppopt_impl ppo) bnd f

1603− prettySe d p bnd (PApp _ (PRef _ op) args) -- infix operators

1603+ prettySe d p bnd (PApp _ (PRef _ _ op) args) -- infix operators

16041604 | UN nm <- basename op

16051605 , not (tnull nm) &&

16061606 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

@@ -1627,10 +1627,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16271627 inFix l r = align . group $

16281628 (prettySe (decD d) left bnd l <+> opName False) <$>

16291629 group (prettySe (decD d) right bnd r)

1630− prettySe d p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1630+ prettySe d p bnd (PApp _ hd@(PRef fc _ f) [tm]) -- symbols, like 'foo

16311631 | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,

16321632 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1633− char '\'' <> prettySe (decD d) startPrec bnd (PRef fc (sUN str))

1633+ char '\'' <> prettySe (decD d) startPrec bnd (PRef fc [] (sUN str))

16341634 prettySe d p bnd (PApp _ f as) = -- Normal prefix applications

16351635 let args = getShowArgs as

16361636 fp = prettySe (decD d) (startPrec + 1) bnd f

@@ -1678,7 +1678,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16781678 text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r

16791679 prettySe d p bnd (PTyped l r) =

16801680 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen

1681− prettySe d p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

1681+ prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser

16821682 | Just elts <- pairElts pair = depth d . enclose (ann lparen) (ann rparen) .

16831683 align . group . vsep . punctuate (ann comma) $

16841684 map (prettySe (decD d) startPrec bnd) elts

@@ -1686,7 +1686,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16861686 TypeOrTerm -> id

16871687 IsType -> annName pairTy

16881688 IsTerm -> annName pairCon

1689− prettySe d p bnd (PDPair _ pun l t r) =

1689+ prettySe d p bnd (PDPair _ _ pun l t r) =

16901690 depth d $

16911691 annotated lparen <>

16921692 left <+>

@@ -1698,8 +1698,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

16981698 IsTerm -> annName sigmaCon

16991699 TypeOrTerm -> id

17001700 (left, addBinding) = case (l, pun) of

1701− (PRef _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1702− _ -> (prettySe (decD d) startPrec bnd l, id )

1701+ (PRef _ _ n, IsType) -> (bindingOf n False <+> text ":" <+> prettySe (decD d) startPrec bnd t, ((n, False) :))

1702+ _ -> (prettySe (decD d) startPrec bnd l, id)

17031703 prettySe d p bnd (PAlternative ns a as) =

17041704 lparen <> text "|" <> prettyAs <> text "|" <> rparen

17051705 where

@@ -1782,11 +1782,11 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17821782 slist' (Just d) _ _ _ | d <= 0 = Nothing

17831783 slist' d _ _ e

17841784 | containsHole e = Nothing

1785− slist' d p bnd (PApp _ (PRef _ nil) _)

1785+ slist' d p bnd (PApp _ (PRef _ _ nil) _)

17861786 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1787− slist' d p bnd (PRef _ nil)

1787+ slist' d p bnd (PRef _ _ nil)

17881788 | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

1789− slist' d p bnd (PApp _ (PRef _ cons) args)

1789+ slist' d p bnd (PApp _ (PRef _ _ cons) args)

17901790 | nsroot cons == sUN "::",

17911791 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

17921792 all isImp imps,

@@ -1810,15 +1810,15 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18101810 slist _ _ _ _ = Nothing

18111811

18121812 pairElts :: PTerm -> Maybe [PTerm]

1813− pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)

1814− | otherwise = Just [x, y]

1813+ pairElts (PPair _ _ _ x y) | Just elts <- pairElts y = Just (x:elts)

1814+ | otherwise = Just [x, y]

18151815 pairElts _ = Nothing

18161816

18171817 natns = "Prelude.Nat."

18181818

18191819 snat :: Maybe Int -> Int -> PTerm -> Maybe Integer

18201820 snat (Just x) _ _ | x <= 0 = Nothing

1821− snat d p (PRef _ z)

1821+ snat d p (PRef _ _ z)

18221822 | show z == (natns++"Z") || show z == "Z" = Just 0

18231823 snat d p (PApp _ s [PExp {getTm=n}])

18241824 | show s == (natns++"S") || show s == "S",

@@ -1858,7 +1858,7 @@ isHoleName _ = False

18581858

18591859-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess

18601860containsHole :: PTerm -> Bool

1861−containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]

1861+containsHole pterm = or [isHoleName n | PRef _ _ n <- take 1000 $ universe pterm]

18621862

18631863-- | Pretty-printer helper for names that attaches the correct annotations

18641864prettyName

@@ -1995,7 +1995,7 @@ showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

19951995

19961996instance Sized PTerm where

19971997 size (PQuote rawTerm) = size rawTerm

1998− size (PRef fc name) = size name

1998+ size (PRef fc _ name) = size name

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

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

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

@@ -2007,9 +2007,9 @@ instance Sized PTerm where

20072007 size (PTrue fc _) = 1

20082008 size (PResolveTC fc) = 1

20092009 size (PRewrite fc left right _) = 1 + size left + size right

2010− size (PPair fc _ left right) = 1 + size left + size right

2011− size (PDPair fs _ left ty right) = 1 + size left + size ty + size right

2012− size (PAlternative ns a alts) = 1 + size alts

2010+ size (PPair fc _ _ left right) = 1 + size left + size right

2011+ size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

2012+ size (PAlternative _ a alts) = 1 + size alts

20132013 size (PHidden hidden) = size hidden

20142014 size (PUnifyLog tm) = size tm

20152015 size (PDisamb _ tm) = size tm

@@ -2036,7 +2036,7 @@ getPArity _ = 0

20362036allNamesIn :: PTerm -> [Name]

20372037allNamesIn tm = nub $ ni [] tm

20382038 where -- TODO THINK added niTacImp, but is it right?

2039− ni env (PRef _ n)

2039+ ni env (PRef _ _ n)

20402040 | not (n `elem` env) = [n]

20412041 ni env (PPatvar _ n) = [n]

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

@@ -2049,10 +2049,10 @@ allNamesIn tm = nub $ ni [] tm

20492049 ni env (PHidden tm) = ni env tm

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

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

2052− ni env (PPair _ _ l r) = ni env l ++ ni env r

2053− ni env (PDPair _ _ (PRef _ n) Placeholder r) = n : ni env r

2054− ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

2055− ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

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

2053+ ni env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni env r

2054+ ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2055+ ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

20562056 ni env (PAlternative ns a ls) = concatMap (ni env) ls

20572057 ni env (PUnifyLog tm) = ni env tm

20582058 ni env (PDisamb _ tm) = ni env tm

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

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

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

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

2079− ni set (PPair _ _ l r) = ni (ni set l) r

2080− ni set (PDPair _ _ (PRef _ n) t r) = ni (ni set t) r

2081− ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r

2079+ ni set (PPair _ _ _ l r) = ni (ni set l) r

2080+ ni set (PDPair _ _ _ (PRef _ _ n) t r) = ni (ni set t) r

2081+ ni set (PDPair _ _ _ l t r) = ni (ni (ni set l) t) r

20822082 ni set (PAlternative ns a as) = niTms set as

20832083 ni set (PHidden tm) = ni set tm

20842084 ni set (PUnifyLog tm) = ni set tm

@@ -2096,12 +2096,12 @@ boundNamesIn tm = S.toList (ni S.empty tm)

20962096implicitNamesIn :: [Name] -> IState -> PTerm -> [Name]

20972097implicitNamesIn uvars ist tm = nub $ ni [] tm

20982098 where

2099− ni env (PRef _ n)

2099+ ni env (PRef _ _ n)

21002100 | not (n `elem` env)

21012101 = case lookupTy n (tt_ctxt ist) of

21022102 [] -> [n]

21032103 _ -> if n `elem` uvars then [n] else []

2104− ni env (PApp _ f@(PRef _ n) as)

2104+ ni env (PApp _ f@(PRef _ _ n) as)

21052105 | n `elem` uvars = ni env f ++ concatMap (ni env) (map getTm as)

21062106 | otherwise = concatMap (ni env) (map getTm as)

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

@@ -2115,9 +2115,9 @@ implicitNamesIn uvars ist tm = nub $ ni [] tm

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

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

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

2118− ni env (PPair _ _ l r) = ni env l ++ ni env r

2119− ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

2120− ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

2118+ ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2119+ ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2120+ ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

21212121 ni env (PAlternative ns a as) = concatMap (ni env) as

21222122 ni env (PHidden tm) = ni env tm

21232123 ni env (PUnifyLog tm) = ni env tm

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

21292129namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

21302130namesIn uvars ist tm = nub $ ni [] tm

21312131 where

2132− ni env (PRef _ n)

2132+ ni env (PRef _ _ n)

21332133 | not (n `elem` env)

21342134 = case lookupTy n (tt_ctxt ist) of

21352135 [] -> [n]

@@ -2145,9 +2145,9 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

2148− ni env (PPair _ _ l r) = ni env l ++ ni env r

2149− ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

2150− ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

2148+ ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2149+ ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2150+ ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

21512151 ni env (PAlternative ns a as) = concatMap (ni env) as

21522152 ni env (PHidden tm) = ni env tm

21532153 ni env (PUnifyLog tm) = ni env tm

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

21632163usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

21642164usedNamesIn vars ist tm = nub $ ni [] tm

21652165 where -- TODO THINK added niTacImp, but is it right?

2166− ni env (PRef _ n)

2166+ ni env (PRef _ _ n)

21672167 | n `elem` vars && not (n `elem` env)

21682168 = case lookupDefExact n (tt_ctxt ist) of

21692169 Nothing -> [n]

@@ -2176,9 +2176,9 @@ usedNamesIn vars ist tm = nub $ ni [] tm

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

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

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

2179− ni env (PPair _ _ l r) = ni env l ++ ni env r

2180− ni env (PDPair _ _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

2181− ni env (PDPair _ _ l t r) = ni env l ++ ni env t ++ ni env r

2179+ ni env (PPair _ _ _ l r) = ni env l ++ ni env r

2180+ ni env (PDPair _ _ _ (PRef _ _ n) t r) = ni env t ++ ni (n:env) r

2181+ ni env (PDPair _ _ _ l t r) = ni env l ++ ni env t ++ ni env r

21822182 ni env (PAlternative ns a as) = concatMap (ni env) as

21832183 ni env (PHidden tm) = ni env tm

21842184 ni env (PUnifyLog tm) = ni env tm

src/Idris/CaseSplit.hs+24−24

@@ -127,7 +127,7 @@ varlist = map (sUN . (:[])) "xyzwstuv" -- EB's personal preference :)

127127

128128stripNS :: Idris.AbsSyntaxTree.PTerm -> Idris.AbsSyntaxTree.PTerm

129129stripNS tm = mapPT dens tm where

130− dens (PRef fc n) = PRef fc (nsroot n)

130+ dens (PRef fc hls n) = PRef fc hls (nsroot n)

131131 dens t = t

132132

133133mergeAllPats :: IState -> Name -> PTerm -> [PTerm] -> [(PTerm, [(Name, PTerm)])]

@@ -137,7 +137,7 @@ mergeAllPats ist cv t (p : ps)

137137 (MS [] [] (filter (/=cv) (patvars t)) [])

138138 ps' = mergeAllPats ist cv t ps in

139139 ((p', u) : ps')

140− where patvars (PRef _ n) = [n]

140+ where patvars (PRef _ _ n) = [n]

141141 patvars (PApp _ _ as) = concatMap (patvars . getTm) as

142142 patvars (PPatvar _ n) = [n]

143143 patvars _ = []

@@ -146,19 +146,19 @@ mergePat :: IState -> PTerm -> PTerm -> Maybe Name -> State MergeState PTerm

146146-- If any names are unified, make sure they stay unified. Always prefer

147147-- user provided name (first pattern)

148148mergePat ist (PPatvar fc n) new t

149− = mergePat ist (PRef fc n) new t

149+ = mergePat ist (PRef fc [] n) new t

150150mergePat ist old (PPatvar fc n) t

151− = mergePat ist old (PRef fc n) t

152−mergePat ist orig@(PRef fc n) new@(PRef _ n') t

151+ = mergePat ist old (PRef fc [] n) t

152+mergePat ist orig@(PRef fc _ n) new@(PRef _ _ n') t

153153 | isDConName n' (tt_ctxt ist) = do addUpdate n new

154154 return new

155155 | otherwise

156156 = do ms <- get

157157 case lookup n' (namemap ms) of

158− Just x -> do addUpdate n (PRef fc x)

159− return (PRef fc x)

158+ Just x -> do addUpdate n (PRef fc [] x)

159+ return (PRef fc [] x)

160160 Nothing -> do put (ms { namemap = ((n', n) : namemap ms) })

161− return (PRef fc n)

161+ return (PRef fc [] n)

162162mergePat ist (PApp _ _ args) (PApp fc f args') t

163163 = do newArgs <- zipWithM mergeArg args (zip args' (argTys ist f))

164164 return (PApp fc f newArgs)

@@ -169,16 +169,16 @@ mergePat ist (PApp _ _ args) (PApp fc f args') t

169169 return (y { machine_inf = machine_inf x,

170170 getTm = tm' })

171171 _ -> return (y { getTm = tm' })

172−mergePat ist (PRef fc n) tm ty = do tm <- tidy ist tm ty

173− addUpdate n tm

174− return tm

172+mergePat ist (PRef fc _ n) tm ty = do tm <- tidy ist tm ty

173+ addUpdate n tm

174+ return tm

175175mergePat ist x y t = return y

176176

177177mergeUserImpl :: PTerm -> PTerm -> PTerm

178178mergeUserImpl x y = x

179179

180180argTys :: IState -> PTerm -> [Maybe Name]

181−argTys ist (PRef fc n)

181+argTys ist (PRef fc hls n)

182182 = case lookupTy n (tt_ctxt ist) of

183183 [ty] -> map (tyName . snd) (getArgTys ty) ++ repeat Nothing

184184 _ -> repeat Nothing

@@ -188,14 +188,14 @@ argTys ist (PRef fc n)

188188argTys _ _ = repeat Nothing

189189

190190tidy :: IState -> PTerm -> Maybe Name -> State MergeState PTerm

191−tidy ist orig@(PRef fc n) ty

191+tidy ist orig@(PRef fc hls n) ty

192192 = do ms <- get

193193 case lookup n (namemap ms) of

194− Just x -> return (PRef fc x)

194+ Just x -> return (PRef fc [] x)

195195 Nothing -> case n of

196196 (UN _) -> return orig

197197 _ -> do n' <- inventName ist ty n

198− return (PRef fc n')

198+ return (PRef fc [] n')

199199tidy ist (PApp fc f args) ty

200200 = do args' <- zipWithM tidyArg args (argTys ist f)

201201 return (PApp fc f args')

@@ -222,7 +222,7 @@ findPats ist t | (P _ n _, _) <- unApply t

222222 [ti] -> map genPat (con_names ti)

223223 _ -> [Placeholder]

224224 where genPat n = case lookupCtxt n (idris_implicits ist) of

225− [args] -> PApp emptyFC (PRef emptyFC n)

225+ [args] -> PApp emptyFC (PRef emptyFC [] n)

226226 (map toPlaceholder args)

227227 _ -> error $ "Can't happen (genPat) " ++ show n

228228 toPlaceholder tm = tm { getTm = Placeholder }

@@ -233,10 +233,10 @@ replaceVar ctxt n t (PApp fc f pats) = PApp fc f (map substArg pats)

233233 where subst :: PTerm -> PTerm

234234 subst orig@(PPatvar _ v) | v == n = t

235235 | otherwise = Placeholder

236− subst orig@(PRef _ v) | v == n = t

237− | isDConName v ctxt = orig

238− subst (PRef _ _) = Placeholder

239− subst (PApp fc (PRef _ t) pats)

236+ subst orig@(PRef _ _ v) | v == n = t

237+ | isDConName v ctxt = orig

238+ subst (PRef _ _ _) = Placeholder

239+ subst (PApp fc (PRef _ _ t) pats)

240240 | isTConName t ctxt = Placeholder -- infer types

241241 subst (PApp fc f pats) = PApp fc f (map substArg pats)

242242 subst x = x

@@ -281,8 +281,8 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

281281

282282 -- TMP HACK: If there are Nats, we don't want to show as numerals since

283283 -- this isn't supported in a pattern, so special case here

284− nshow (PRef _ (UN z)) | z == txt "Z" = "Z"

285− nshow (PApp _ (PRef _ (UN s)) [x]) | s == txt "S" =

284+ nshow (PRef _ _ (UN z)) | z == txt "Z" = "Z"

285+ nshow (PApp _ (PRef _ _ (UN s)) [x]) | s == txt "S" =

286286 "(S " ++ addBrackets (nshow (getTm x)) ++ ")"

287287 nshow t = show t

288288

@@ -359,7 +359,7 @@ getClause l fn fp

359359 getNameFrom i used (PPi _ _ _ _ _)

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

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

362− getNameFrom i used (PRef fc f)

362+ getNameFrom i used (PRef fc _ f)

363363 = case getNameHints i f of

364364 [] -> uniqueName (sUN "x") used

365365 ns -> uniqueNameFrom (mkSupply ns) used

@@ -415,7 +415,7 @@ nameMissing ps = do ist <- get

415415 newPats

416416 return (map fst newPats')

417417 where

418− base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc (sUN "_")))) args)

418+ base (PApp fc f args) = PApp fc f (map (fmap (const (PRef fc [] (sUN "_")))) args)

419419 base t = t

420420

421421 nm ptm = do mptm <- elabNewPat ptm

src/Idris/Coverage.hs+17−17

@@ -28,10 +28,10 @@ mkPatTm t = do i <- getIState

2828 let timp = addImpl' True [] [] [] i t

2929 evalStateT (toTT (mapPT deNS timp)) 0

3030 where

31− toTT (PRef _ n) = do i <- lift getIState

32− case lookupNameDef n (tt_ctxt i) of

33− [(n', TyDecl nt _)] -> return $ P nt n' Erased

34− _ -> return $ P Ref n Erased

31+ toTT (PRef _ _ n) = do i <- lift getIState

32+ case lookupNameDef n (tt_ctxt i) of

33+ [(n', TyDecl nt _)] -> return $ P nt n' Erased

34+ _ -> return $ P Ref n Erased

3535 toTT (PApp _ t args) = do t' <- toTT t

3636 args' <- mapM (toTT . getTm) args

3737 return $ mkApp t' args'

@@ -42,7 +42,7 @@ mkPatTm t = do i <- getIState

4242 put (v + 1)

4343 return (P Bound (sMN v "imp") Erased)

4444

45− deNS (PRef f (NS n _)) = PRef f n

45+ deNS (PRef f hl (NS n _)) = PRef f hl n

4646 deNS t = t

4747

4848-- | Given a list of LHSs, generate a extra clauses which cover the remaining

@@ -112,7 +112,7 @@ genClauses fc n xs given

112112 | all (== [Placeholder]) args = []

113113 mkClauses parg args

114114 = do args' <- mkArg args

115− let tm = PApp fc (PRef fc n) (zipWith upd args' parg)

115+ let tm = PApp fc (PRef fc [] n) (zipWith upd args' parg)

116116 return tm

117117 where

118118 mkArg :: [[PTerm]] -> [[PTerm]]

@@ -214,14 +214,14 @@ genAll i args

214214 nubMap f acc (x : xs) = nubMap f (fnub' acc (f x)) xs

215215

216216 otherPats :: PTerm -> [PTerm]

217− otherPats o@(PRef fc n) = ops fc n [] o

218− otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

219− otherPats o@(PPair fc _ l r)

217+ otherPats o@(PRef fc hl n) = ops fc n [] o

218+ otherPats o@(PApp _ (PRef fc hl n) xs) = ops fc n xs o

219+ otherPats o@(PPair fc hls _ l r)

220220 = ops fc pairCon

221221 ([pimp (sUN "A") Placeholder True,

222222 pimp (sUN "B") Placeholder True] ++

223223 [pexp l, pexp r]) o

224− otherPats o@(PDPair fc p t _ v)

224+ otherPats o@(PDPair fc hls p t _ v)

225225 = ops fc (sUN "Ex_intro")

226226 ([pimp (sUN "a") Placeholder True,

227227 pimp (sUN "P") Placeholder True] ++

@@ -232,7 +232,7 @@ genAll i args

232232 ops fc n xs o

233233 | (TyDecl c@(DCon _ arity _) ty : _) <- lookupDef n (tt_ctxt i)

234234 = do xs' <- mapM otherPats (map getExpTm xs)

235− let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

235+ let p = resugar (PApp fc (PRef fc [] n) (zipWith upd xs' xs))

236236 let tyn = getTy n (tt_ctxt i)

237237 case lookupCtxt tyn (idris_datatypes i) of

238238 (TI ns _ _ _ _ : _) -> p : map (mkPat fc) (ns \\ [n])

@@ -243,12 +243,12 @@ genAll i args

243243 getExpTm t = getTm t

244244

245245 -- put it back to its original form

246− resugar (PApp _ (PRef fc (UN ei)) [_,_,t,v])

246+ resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v])

247247 | ei == txt "Ex_intro"

248− = PDPair fc TypeOrTerm (getTm t) Placeholder (getTm v)

249− resugar (PApp _ (PRef fc n) [_,_,l,r])

248+ = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)

249+ resugar (PApp _ (PRef fc hl n) [_,_,l,r])

250250 | n == pairCon

251− = PPair fc IsTerm (getTm l) (getTm r)

251+ = PPair fc [] IsTerm (getTm l) (getTm r)

252252 resugar t = t

253253

254254 dropForce force (x : xs) i | i `elem` force

@@ -265,7 +265,7 @@ genAll i args

265265

266266 mkPat fc x = case lookupCtxt x (idris_implicits i) of

267267 (pargs : _)

268− -> PApp fc (PRef fc x) (map (upd Placeholder) pargs)

268+ -> PApp fc (PRef fc [] x) (map (upd Placeholder) pargs)

269269 _ -> error "Can't happen - genAll"

270270

271271 fnub :: [PTerm] -> [PTerm]

@@ -279,7 +279,7 @@ genAll i args

279279 -- quick check for constructor equality

280280 quickEq :: PTerm -> PTerm -> Bool

281281 quickEq (PConstant _ n) (PConstant _ n') = n == n'

282− quickEq (PRef _ n) (PRef _ n') = n == n'

282+ quickEq (PRef _ _ n) (PRef _ _ n') = n == n'

283283 quickEq (PApp _ t as) (PApp _ t' as')

284284 | length as == length as'

285285 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))

src/Idris/DSL.hs+25−25

@@ -18,7 +18,7 @@ debindApp syn t = debind (dsl_bind (dsl_info syn)) t

1818dslify :: SyntaxInfo -> IState -> PTerm -> PTerm

1919dslify syn i = transform dslifyApp

2020 where

21− dslifyApp (PApp fc (PRef _ f) [a])

21+ dslifyApp (PApp fc (PRef _ _ f) [a])

2222 | [d] <- lookupCtxt f (idris_dsls i)

2323 = desugar (syn { dsl_info = d }) i (getTm a)

2424 dslifyApp t = t

@@ -29,20 +29,20 @@ desugar syn i t = let t' = expandSugar (dsl_info syn) t

2929

3030mkTTName :: FC -> Name -> PTerm

3131mkTTName fc n =

32− let mkList fc [] = PRef fc (sNS (sUN "Nil") ["List", "Prelude"])

33− mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))

32+ let mkList fc [] = PRef fc [] (sNS (sUN "Nil") ["List", "Prelude"])

33+ mkList fc (x:xs) = PApp fc (PRef fc [] (sNS (sUN "::") ["List", "Prelude"]))

3434 [ pexp (stringC x)

3535 , pexp (mkList fc xs)]

3636 stringC = PConstant fc . Str . str

3737 intC = PConstant fc . I

3838 reflm n = sNS (sUN n) ["Reflection", "Language"]

3939 in case n of

40− UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]

41− NS nm ns -> PApp fc (PRef fc (reflm "NS")) [ pexp (mkTTName fc nm)

42− , pexp (mkList fc ns)]

43− MN i nm -> PApp fc (PRef fc (reflm "MN")) [ pexp (intC i)

44− , pexp (stringC nm)]

45− otherwise -> PRef fc $ reflm "NErased"

40+ UN nm -> PApp fc (PRef fc [] (reflm "UN")) [ pexp (stringC nm)]

41+ NS nm ns -> PApp fc (PRef fc [] (reflm "NS")) [ pexp (mkTTName fc nm)

42+ , pexp (mkList fc ns)]

43+ MN i nm -> PApp fc (PRef fc [] (reflm "MN")) [ pexp (intC i)

44+ , pexp (stringC nm)]

45+ otherwise -> PRef fc [] $ reflm "NErased"

4646

4747expandSugar :: DSL -> PTerm -> PTerm

4848expandSugar dsl (PLam fc n nfc ty tm)

@@ -72,14 +72,14 @@ expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)

7272expandSugar dsl (PCase fc s opts) = PCase fc (expandSugar dsl s)

7373 (map (pmap (expandSugar dsl)) opts)

7474expandSugar dsl (PIfThenElse fc c t f) =

75− PApp fc (PRef NoFC (sUN "ifThenElse"))

75+ PApp fc (PRef NoFC [] (sUN "ifThenElse"))

7676 [ PExp 0 [] (sMN 0 "condition") $ expandSugar dsl c

7777 , PExp 0 [] (sMN 0 "whenTrue") $ expandSugar dsl t

7878 , PExp 0 [] (sMN 0 "whenFalse") $ expandSugar dsl f

7979 ]

80−expandSugar dsl (PPair fc p l r) = PPair fc p (expandSugar dsl l) (expandSugar dsl r)

81−expandSugar dsl (PDPair fc p l t r) = PDPair fc p (expandSugar dsl l) (expandSugar dsl t)

82− (expandSugar dsl r)

80+expandSugar dsl (PPair fc hls p l r) = PPair fc hls p (expandSugar dsl l) (expandSugar dsl r)

81+expandSugar dsl (PDPair fc hls p l t r) = PDPair fc hls p (expandSugar dsl l) (expandSugar dsl t)

82+ (expandSugar dsl r)

8383expandSugar dsl (PAlternative ms a as) = PAlternative ms a (map (expandSugar dsl) as)

8484expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

8585expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

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

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

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

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

102− (PCase fc (PRef fc (sMN 0 "bpat"))

102+ (PCase fc (PRef fc [] (sMN 0 "bpat"))

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

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

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

@@ -118,7 +118,7 @@ expandSugar dsl t = t

118118-- | Replace DSL-bound variable in a term

119119var :: DSL -> Name -> PTerm -> Int -> PTerm

120120var dsl n t i = v' i t where

121− v' i (PRef fc x) | x == n =

121+ v' i (PRef fc hl x) | x == n =

122122 case dsl_var dsl of

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

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

@@ -137,8 +137,8 @@ var dsl n t i = v' i t where

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

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

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

140− v' i (PPair f p l r) = PPair f p (v' i l) (v' i r)

141− v' i (PDPair f p l t r) = PDPair f p (v' i l) (v' i t) (v' i r)

140+ v' i (PPair f hls p l r) = PPair f hls p (v' i l) (v' i r)

141+ v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)

142142 v' i (PAlternative ms a as) = PAlternative ms a $ map (v' i) as

143143 v' i (PHidden t) = PHidden (v' i t)

144144 v' i (PIdiom f t) = PIdiom f (v' i t)

@@ -153,7 +153,7 @@ var dsl n t i = v' i t where

153153 Nothing -> PElabError (Msg "No index_next defined")

154154 Just f -> PApp fc f [pexp (mkVar fc (n-1))]

155155

156− setFC fc (PRef _ n) = PRef fc n

156+ setFC fc (PRef _ _ n) = PRef fc [] n

157157 setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)

158158 setFC fc t = t

159159

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

182182 (bs, n) <- get

183183 let nm = sUN ("_bindApp" ++ show n)

184184 put ((nm, fc, PApp fc t args') : bs, n+1)

185− return (PRef fc nm)

185+ return (PRef fc [] nm)

186186 db' (PApp fc t args)

187187 = do t' <- db' t

188188 args' <- mapM dbArg args

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

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

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

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

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

196− r' <- db' r

197− return (PPair fc p l' r')

198− db' (PDPair fc p l t r) = do l' <- db' l

199− r' <- db' r

200− return (PDPair fc p l' t r')

195+ db' (PPair fc hls p l r) = do l' <- db' l

196+ r' <- db' r

197+ return (PPair fc hls p l' r')

198+ db' (PDPair fc hls p l t r) = do l' <- db' l

199+ r' <- db' r

200+ return (PDPair fc hls p l' t r')

201201 db' (PRunElab fc t ns) = fmap (\tm -> PRunElab fc tm ns) (db' t)

202202 db' t = return t

203203

src/Idris/DeepSeq.hs+5−5

@@ -223,8 +223,8 @@ instance (NFData t) => NFData (PData' t) where

223223

224224instance NFData PTerm where

225225 rnf (PQuote x1) = rnf x1 `seq` ()

226− rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

227− rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

226+ rnf (PRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

227+ rnf (PInferRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

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

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

230230 rnf (PPi x1 x2 x3 x4 x5)

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

242242 rnf (PResolveTC x1) = rnf x1 `seq` ()

243243 rnf (PRewrite x1 x2 x3 x4)

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

245− rnf (PPair x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

246− rnf (PDPair x1 x2 x3 x4 x5)

247− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

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

246+ rnf (PDPair x1 x2 x3 x4 x5 x6)

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

248248 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

249249 rnf (PAlternative x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

250250 rnf (PHidden x1) = rnf x1 `seq` ()

src/Idris/Delaborate.hs+22−22

@@ -30,11 +30,11 @@ bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

3030resugar :: IState -> PTerm -> PTerm

3131resugar ist = transform flattenDoLet . transform resugarApp

3232 where

33− resugarApp (PApp fc (PRef _ n) args)

33+ resugarApp (PApp fc (PRef _ _ n) args)

3434 | [c, t, f] <- mapMaybe explicitTerm args

3535 , basename n == sUN "ifThenElse"

3636 = PIfThenElse fc c (dedelay t) (dedelay f)

37− resugarApp (PApp fc (PRef _ n) args)

37+ resugarApp (PApp fc (PRef _ _ n) args)

3838 | [v, PLam _ bn _ _ next] <- mapMaybe explicitTerm args

3939 , basename n == sUN ">>="

4040 = let step = if bn `elem` namesIn [] ist next

@@ -43,7 +43,7 @@ resugar ist = transform flattenDoLet . transform resugarApp

4343 in case resugarApp next of

4444 PDoBlock dos -> PDoBlock (step : dos)

4545 expr -> PDoBlock [step, DoExp NoFC expr]

46− resugarApp (PApp fc (PRef _ n) args)

46+ resugarApp (PApp fc (PRef _ _ n) args)

4747 | [PConstant fc (BI i)] <- mapMaybe explicitTerm args

4848 , basename n == sUN "fromInteger"

4949 = PConstant fc (BI i)

@@ -59,7 +59,7 @@ resugar ist = transform flattenDoLet . transform resugarApp

5959 fixExp d = [d]

6060 flattenDoLet tm = tm

6161

62− dedelay (PApp _ (PRef _ delay) [_, _, obj])

62+ dedelay (PApp _ (PRef _ _ delay) [_, _, obj])

6363 | delay == sUN "Delay" = getTm obj

6464 dedelay x = x

6565

@@ -99,15 +99,15 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

9999 un = fileFC "(val)"

100100

101101 de env _ (App _ f a) = deFn env f [a]

102− de env _ (V i) | i < length env = PRef un (snd (env!!i))

103− | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

102+ de env _ (V i) | i < length env = PRef un [] (snd (env!!i))

103+ | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))

104104 de env _ (P _ n _) | n == unitTy = PTrue un IsType

105105 | n == unitCon = PTrue un IsTerm

106− | Just n' <- lookup n env = PRef un n'

106+ | Just n' <- lookup n env = PRef un [] n'

107107 | otherwise

108108 = case lookup n (idris_metavars ist) of

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

110− _ -> PRef un n

110+ _ -> PRef un [] n

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

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

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

@@ -154,16 +154,16 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

154154

155155 deFn env (App _ f a) args = deFn env f (a:args)

156156 deFn env (P _ n _) [l,r]

157− | n == pairTy = PPair un IsType (de env [] l) (de env [] r)

157+ | n == pairTy = PPair un [] IsType (de env [] l) (de env [] r)

158158 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

159159 deFn env (P _ n _) [ty, Bind x (Lam _) r]

160160 | n == sigmaTy

161− = PDPair un IsType (PRef un x) (de env [] ty)

161+ = PDPair un [] IsType (PRef un [] x) (de env [] ty)

162162 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

163163 deFn env (P _ n _) [lt,rt,l,r]

164− | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

165− | n == sigmaCon = PDPair un IsTerm (de env [] l) Placeholder

166− (de env [] r)

164+ | n == pairCon = PPair un [] IsTerm (de env [] l) (de env [] r)

165+ | n == sigmaCon = PDPair un [] IsTerm (de env [] l) Placeholder

166+ (de env [] r)

167167 deFn env f@(P _ n _) args

168168 | n `elem` map snd env

169169 = PApp un (de env [] f) (map pexp (map (de env []) args))

@@ -181,8 +181,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

181181 = PApp un (PMetavar NoFC n) (map pexp args)

182182 mkPApp n args

183183 | Just imps <- lookupCtxtExact n (idris_implicits ist)

184− = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

185− | otherwise = PApp un (PRef un n) (map pexp args)

184+ = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

185+ | otherwise = PApp un (PRef un [] n) (map pexp args)

186186

187187 imp (PImp p m l n _) arg = PImp p m l n arg

188188 imp (PExp p l n _) arg = PExp p l n arg

@@ -553,19 +553,19 @@ addImplicitDiffs x y

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

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

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

556− addI (PPair fc pi a b) (PPair fc' pi' c d)

556+ addI (PPair fc hls pi a b) (PPair fc' hls' pi' c d)

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

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

559− (PPair fc pi a' b', PPair fc' pi' c' d')

560− addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)

559+ (PPair fc hls pi a' b', PPair fc' hls' pi' c' d')

560+ addI (PDPair fc hls pi a t b) (PDPair fc' hls' pi' c u d)

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

562562 (t', u') = addI t u

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

564− (PDPair fc pi a' t' b', PDPair fc' pi' c' u' d')

564+ (PDPair fc hls pi a' t' b', PDPair fc' hls' pi' c' u' d')

565565 addI x y = (x, y)

566566

567567 -- Just the ones which appear desugared in errors

568− expLike (PRef _ n) (PRef _ n') = n == n'

568+ expLike (PRef _ _ n) (PRef _ _ n') = n == n'

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

570570 = expLike f f' && length as == length as' &&

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

@@ -573,8 +573,8 @@ addImplicitDiffs x y

573573 = n == n' && expLike s s' && expLike t t'

574574 expLike (PLam _ n _ s t) (PLam _ n' _ s' t')

575575 = n == n' && expLike s s' && expLike t t'

576− expLike (PPair _ _ x y) (PPair _ _ x' y') = expLike x x' && expLike y y'

577− expLike (PDPair _ _ x _ y) (PDPair _ _ x' _ y') = expLike x x' && expLike y y'

576+ expLike (PPair _ _ _ x y) (PPair _ _ _ x' y') = expLike x x' && expLike y y'

577+ expLike (PDPair _ _ _ x _ y) (PDPair _ _ _ x' _ y') = expLike x x' && expLike y y'

578578 expLike x y = x == y

579579

580580-- Issue #1589 on the issue tracker

src/Idris/Docs.hs+5−5

@@ -197,12 +197,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

197197 updateArgs ps (a:as) = a : updateArgs ps as

198198 updateArgs _ _ = []

199199

200− updateRef nm (PRef fc _) = PRef fc nm

200+ updateRef nm (PRef fc _ _) = PRef fc [] nm

201201 updateRef _ pt = pt

202202

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

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

205− isSubclass _ = False

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

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

205+ isSubclass _ = False

206206

207207 prettyParameters =

208208 if any (isJust . snd) params

@@ -289,7 +289,7 @@ docClass n ci

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

290290 getDInst _ = Nothing

291291

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

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

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

294294 isSubclass (PPi _ _ _ _ pt)

295295 = isSubclass pt

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

@@ -44,5 +44,5 @@ replaceUnderscore tm = evalState (transformM (underAs replaceUnderscore') tm) 0

4444

4545

4646 replaceUnderscore' :: PTerm -> State Int PTerm

47− replaceUnderscore' Placeholder = PRef emptyFC <$> fresh

47+ replaceUnderscore' Placeholder = PRef emptyFC [] <$> fresh

4848 replaceUnderscore' tm = return tm

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

@@ -65,8 +65,8 @@ elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

6565elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

6666 = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

6767 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

68− let constraint = PApp fc (PRef fc tn)

69− (map (pexp . PRef fc) (map (\(n, _, _) -> n) ps))

68+ let constraint = PApp fc (PRef fc [] tn)

69+ (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

7070

7171 let syn =

7272 syn_in { using = addToUsing (using syn_in)

@@ -142,7 +142,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

142142 = do when (not $ null cs) . tclift

143143 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

144144 i <- getIState

145− let t = PApp fc (PRef fc n) (map pexp ps)

145+ let t = PApp fc (PRef fc [] n) (map pexp ps)

146146 let isConstrained = any (== t) (map snd constraints)

147147 when (not isConstrained) . tclift

148148 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

@@ -195,16 +195,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

195195 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

196196 -- SN (ParentN cn (show con))

197197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

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

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

198+ let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

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

200200 let rhs = PResolveTC (fileFC "HACK")

201201 let ty = PPi constraint cnm NoFC c con

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

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

204204 i <- getIState

205205 let conn = case con of

206− PRef _ n -> n

207− PApp _ (PRef _ n) _ -> n

206+ PRef _ _ n -> n

207+ PApp _ (PRef _ _ n) _ -> n

208208 let conn' = case lookupCtxtName conn (idris_classes i) of

209209 [(n, _)] -> n

210210 _ -> conn

@@ -225,10 +225,10 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

225225 tfun cn c syn all (m, (mfc, doc, o, ty))

226226 = do let ty' = expandMethNS syn (insertConstraint c all ty)

227227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

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

228+ let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

229229 let margs = getMArgs ty

230230 let anames = map (\x -> sMN x "arg") [0..]

231− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

231+ let lhs = PApp fc (PRef fc [] m) (pconst capp : lhsArgs margs anames)

232232 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

233233 logLvl 2 ("Top level type: " ++ showTmImpls ty')

234234 logLvl 1 (show (m, ty', capp, margs))

@@ -242,16 +242,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

242242 getMArgs _ = []

243243

244244 getMeth :: [Name] -> [Name] -> Name -> PTerm

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

245+ getMeth (m:ms) (a:as) x | x == a = PRef fc [] m

246246 | otherwise = getMeth ms as x

247247

248248 lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

249− lhsArgs (IA n : xs) ns = pimp n (PRef fc n) False : lhsArgs xs ns

249+ lhsArgs (IA n : xs) ns = pimp n (PRef fc [] n) False : lhsArgs xs ns

250250 lhsArgs (CA : xs) ns = lhsArgs xs ns

251251 lhsArgs [] _ = []

252252

253253 rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

254− rhsArgs (IA n : xs) ns = pexp (PRef fc n) : rhsArgs xs ns

254+ rhsArgs (IA n : xs) ns = pexp (PRef fc [] n) : rhsArgs xs ns

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

256256 rhsArgs [] _ = []

257257

@@ -269,8 +269,8 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

269269 -- to the other methods in the class

270270 constrainMeths :: [Name] -> Name -> PTerm -> PTerm

271271 constrainMeths allM dictN tm = transform (addC allM dictN) tm

272− addC allM dictN m@(PRef fc n)

273− | n `elem` allM = PApp NoFC m [pconst (PRef NoFC dictN)]

272+ addC allM dictN m@(PRef fc hls n)

273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]

274274 | otherwise = m

275275 addC _ _ tm = tm

276276

@@ -303,7 +303,7 @@ expandMethNS :: SyntaxInfo

303303 -> PTerm -> PTerm

304304expandMethNS syn = mapPT expand

305305 where

306− expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

306+ expand (PRef fc hls n) | n `elem` imp_methods syn = PRef fc hls $ expandNS syn n

307307 expand t = t

308308

309309-- | Find the determining parameter locations

src/Idris/Elab/Clause.hs+17−17

@@ -482,20 +482,20 @@ checkPossible info fc tcgen fname lhs_in

482482

483483

484484propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

485−propagateParams i ps t tm@(PApp _ (PRef fc n) args)

486− = PApp fc (PRef fc n) (addP t args)

485+propagateParams i ps t tm@(PApp _ (PRef fc hls n) args)

486+ = PApp fc (PRef fc hls n) (addP t args)

487487 where addP (Bind n _ sc) (t : ts)

488488 | Placeholder <- getTm t,

489489 n `elem` ps,

490490 not (n `elem` allNamesIn tm)

491− = t { getTm = PRef NoFC n } : addP sc ts

491+ = t { getTm = PRef NoFC [] n } : addP sc ts

492492 addP (Bind n _ sc) (t : ts) = t : addP sc ts

493493 addP _ ts = ts

494−propagateParams i ps t (PRef fc n)

494+propagateParams i ps t (PRef fc hls n)

495495 = case lookupCtxt n (idris_implicits i) of

496496 [is] -> let ps' = filter (isImplicit is) ps in

497− PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')

498− _ -> PRef fc n

497+ PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')

498+ _ -> PRef fc hls n

499499 where isImplicit [] n = False

500500 isImplicit (PImp _ _ _ x _ : is) n | x == n = True

501501 isImplicit (_ : is) n = isImplicit is n

@@ -734,7 +734,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

734734 borrowedB b = borrowedNames env (binderTy b)

735735 borrowedNames _ _ = []

736736

737− mkLHSapp t@(PRef _ _) = PApp fc t []

737+ mkLHSapp t@(PRef _ _ _) = PApp fc t []

738738 mkLHSapp t = t

739739

740740 decorate (NS x ns)

@@ -772,7 +772,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

772772 where

773773 isArg' (PClause _ _ (PApp _ _ args) _ _ _)

774774 = any (\x -> case x of

775− PRef _ n' -> n == n'

775+ PRef _ _ n' -> n == n'

776776 _ -> False) (map getTm args)

777777 isArg' _ = False

778778 isArg _ _ = False

@@ -905,13 +905,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

905905 mapM_ (rec_elabDecl info EAll info) wb

906906

907907 -- rhs becomes: fname' ps_pre wval ps_post Refl

908− let rhs = PApp fc (PRef fc wname)

909− (map (pexp . (PRef fc) . fst) bargs_pre ++

908+ let rhs = PApp fc (PRef fc [] wname)

909+ (map (pexp . (PRef fc []) . fst) bargs_pre ++

910910 pexp wval :

911− (map (pexp . (PRef fc) . fst) bargs_post) ++

911+ (map (pexp . (PRef fc []) . fst) bargs_post) ++

912912 case mpn of

913913 Nothing -> []

914− Just _ -> [pexp (PApp NoFC (PRef NoFC eqCon)

914+ Just _ -> [pexp (PApp NoFC (PRef NoFC [] eqCon)

915915 [ pimp (sUN "A") Placeholder False

916916 , pimp (sUN "x") Placeholder False

917917 ])])

@@ -974,21 +974,21 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

974974 = ifail $ show fc ++ ":badly formed with clause"

975975

976976 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

977− addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

977+ addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]

978978

979− updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

979+ updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

980980 = let ns = map (keepMvar (map fst mvars) fc') ns_in

981981 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

982982 return $ substMatches mvars $

983− PApp fc (PRef fc' wname)

983+ PApp fc (PRef fc' [] wname)

984984 (map pexp ns ++ pexp w : (map pexp ns') ++

985985 case pn of

986986 Nothing -> []

987− Just pnm -> [pexp (PRef fc pnm)])

987+ Just pnm -> [pexp (PRef fc [] pnm)])

988988 updateLHS n pn wname mvars ns_in ns_in' tm w

989989 = updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w

990990

991− keepMvar mvs fc v | v `elem` mvs = PRef fc v

991+ keepMvar mvs fc v | v `elem` mvs = PRef fc [] v

992992 | otherwise = Placeholder

993993

994994 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

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

@@ -259,15 +259,15 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

259259

260260 mkLazy (PPi pl n nfc ty sc)

261261 = let ty' = if getTyName ty

262− then PApp fc (PRef fc (sUN "Lazy'"))

263− [pexp (PRef fc (sUN "LazyCodata")),

262+ then PApp fc (PRef fc [] (sUN "Lazy'"))

263+ [pexp (PRef fc [] (sUN "LazyCodata")),

264264 pexp ty]

265265 else ty in

266266 PPi pl n nfc ty' (mkLazy sc)

267267 mkLazy t = t

268268

269− getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

270− getTyName (PRef _ n) = n == nsroot tn

269+ getTyName (PApp _ (PRef _ _ n) _) = n == nsroot tn

270+ getTyName (PRef _ _ n) = n == nsroot tn

271271 getTyName _ = False

272272

273273

@@ -326,11 +326,11 @@ elabCaseFun ind paramPos n ty cons info = do

326326 scrutineeIdxs <- namePis False idxs

327327 let motiveConstr = [(motiveName, expl, motive)]

328328 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

329− let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

329+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

330330 let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

331331 let clauseConsElimArgs = map getPiName consTerms

332332 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

333− let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

333+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

334334 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

335335 elimLog elimSig

336336 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

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

381381 mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg

382382 return (oldName, (name, pl, piarg))

383383 where keyOf :: PTerm -> String

384− keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

384+ keyOf (PRef _ _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

385385 keyOf (PApp _ tyf _) = keyOf tyf

386386 keyOf (PType _) = "ty__"

387387 keyOf _ = "carg__"

@@ -446,10 +446,10 @@ elabCaseFun ind paramPos n ty cons info = do

446446 case findIndex (== n) oldParams of

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

448448 Just i -> (removeParamPis oldParams params tyr)

449− removeParamPis oldParams params (PRef _ n) =

449+ removeParamPis oldParams params (PRef _ _ n) =

450450 case findIndex (== n) oldParams of

451− Nothing -> (PRef elimFC n)

452− Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))

451+ Nothing -> (PRef elimFC [] n)

452+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC [] (newname))

453453 removeParamPis oldParams params (PApp _ cns args) =

454454 PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args

455455 where replaceParamArgs :: [PArg] -> [PArg]

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

460460 [n] ->

461461 case findIndex (== n) oldParams of

462462 Nothing -> arg:replaceParamArgs args

463− Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args

463+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC [] newname}:replaceParamArgs args

464464 removeParamPis oldParams params t = t

465465

466466 paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]

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

468468 paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args

469469

470470 extractName :: PTerm -> [Name]

471− extractName (PRef _ n) = [n]

472− extractName _ = []

471+ extractName (PRef _ _ n) = [n]

472+ extractName _ = []

473473

474474 splitArgPms :: PTerm -> ([PTerm], [PTerm])

475475 splitArgPms (PApp _ f args) = splitArgPms' args

@@ -505,23 +505,23 @@ elabCaseFun ind paramPos n ty cons info = do

505505 let (_, consIdxs) = splitArgPms resTy

506506 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

507507 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

508− applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

508+ applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC [] n))

509509 where (_, idxs) = splitArgPms ty

510510

511511 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

512512 findRecArgs [] = []

513− findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

514− findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

515− findRecArgs (ty:rs) = findRecArgs rs

513+ findRecArgs (ty@(_,_,PRef _ _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

514+ findRecArgs (ty@(_,_,PApp _ (PRef _ _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

515+ findRecArgs (ty:rs) = findRecArgs rs

516516

517517 applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm

518− applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)

518+ applyCons tn targs = PApp elimFC (PRef elimFC [] tn) (map convertArg targs)

519519

520520 convertArg :: (Name, Plicity, PTerm) -> PArg

521− convertArg (n, _, _) = pexp (PRef elimFC n)

521+ convertArg (n, _, _) = pexp (PRef elimFC [] n)

522522

523523 applyMotive :: [PTerm] -> PTerm -> PTerm

524− applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])

524+ applyMotive idxs t = PApp elimFC (PRef elimFC [] motiveName) (map pexp idxs ++ [pexp t])

525525

526526 getPiName :: (Name, Plicity, PTerm) -> Name

527527 getPiName (name,_,_) = name

@@ -539,11 +539,11 @@ elabCaseFun ind paramPos n ty cons info = do

539539 let (_, generalIdxs') = splitArgPms resTy

540540 let generalIdxs = map pexp generalIdxs'

541541 consArgs <- namePis False args

542− let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

542+ let lhsPattern = PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

543543 let recArgs = findRecArgs consArgs

544544 let recElims = if ind then map applyRecElim recArgs else []

545− let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

545+ let rhsExpr = PApp elimFC (PRef elimFC [] cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

546546 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

547547 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

548− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

548+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC [] recCnm])

549549 where (_, idxs) = splitArgPms recTy

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

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

6868 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

6969 cs -> tclift $ tfail $ At fc

7070 (CantResolveAlts (map fst cs))

71− let constraint = PApp fc (PRef fc n) (map pexp ps)

71+ let constraint = PApp fc (PRef fc [] n) (map pexp ps)

7272 let iname = mkiname n (namespace info) ps expn

7373 let emptyclass = null (class_methods ci)

7474 when (what /= EDefns || (null ds && not emptyclass)) $ do

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

8989 -- where block

9090 wparams <- mapM (\p -> case p of

9191 PApp _ _ args -> getWParams (map getTm args)

92− a@(PRef fc f) -> getWParams [a]

92+ a@(PRef fc _ f) -> getWParams [a]

9393 _ -> return []) ps

9494 ist <- getIState

9595 let pnames = nub $ map pname (concat (nub wparams)) ++

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

100100 let all_meths = map (nsroot . fst) (class_methods ci)

101101 let mtys = map (\ (n, (op, t)) ->

102102 let t_in = substMatchesShadow ips pnames t

103− mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))

103+ mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))

104104 all_meths

105105 t' = substMatchesShadow mnamemap pnames t_in in

106106 (decorate ns iname n,

@@ -123,15 +123,15 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

123123

124124 -- Bring variables in instance head into scope

125125 let headVars = nub $ mapMaybe (\p -> case p of

126− PRef _ n ->

126+ PRef _ _ n ->

127127 case lookupTy n (tt_ctxt ist) of

128128 [] -> Just n

129129 _ -> Nothing

130130 _ -> Nothing) ps

131131-- let lhs = PRef fc iname

132− let lhs = PApp fc (PRef fc iname)

133− (map (\n -> pimp n (PRef fc n) True) headVars)

134− let rhs = PApp fc (PRef fc (instanceCtorName ci))

132+ let lhs = PApp fc (PRef fc [] iname)

133+ (map (\n -> pimp n (PRef fc [] n) True) headVars)

134+ let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

135135 (map (pexp . mkMethApp) mtys)

136136

137137 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

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

218218 keepDets dets t = t

219219

220220 mkMethApp (n, _, _, ty)

221− = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

221+ = lamBind 0 ty (papp fc (PRef fc [] n) (methArgs 0 ty))

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

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

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

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

226226 lamBind i _ sc = sc

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

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

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

229229 methArgs i (PPi (Exp _ _ _) n _ ty sc)

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

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

231231 methArgs i (PPi (Constraint _ _) n _ ty sc)

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

233233 methArgs i _ = []

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

237237

238238 getWParams [] = return []

239239 getWParams (p : ps)

240− | PRef _ n <- p

240+ | PRef _ _ n <- p

241241 = do ps' <- getWParams ps

242242 ctxt <- getContext

243243 case lookupP n ctxt of

244− [] -> return (pimp n (PRef fc n) True : ps')

244+ [] -> return (pimp n (PRef fc [] n) True : ps')

245245 _ -> return ps'

246246 getWParams (_ : ps) = getWParams ps

247247

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

@@ -94,7 +94,7 @@ elabProvider doc info syn fc nfc what n

9494 | ProvTerm ty _ <- what ->

9595 do -- Finally add a top-level definition of the provided term

9696 elabType info syn doc [] fc [] n NoFC ty

97− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

97+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc [] n) []) [] (delab i tm) []]

9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

9999 | ProvPostulate _ <- what ->

100100 do -- Add the postulate

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

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

9595

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

9797 target :: PTerm

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

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

9999

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

101101 paramsAndDoc = pad params paramDocs

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

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

328328 generateLhs :: PTerm

329329 generateLhs = let args = lhsArgs index phArgs

330− in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]

330+ in PApp fc (PRef fc [] pname) [pexp (PApp fc (PRef fc [] cn) args)]

331331 where

332332 lhsArgs :: Int -> [PArg] -> [PArg]

333− lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest

333+ lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest

334334 lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)

335335 lhsArgs _ [] = []

336336

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

343343

344344 -- | The right hand side of the projection function.

345345 generateRhs :: PTerm

346− generateRhs = PRef fc pname_in

346+ generateRhs = PRef fc [] pname_in

347347

348348-- | Creates and elaborates an update function.

349349-- If 'optional' is true, we will not fail if we can't elaborate the update function.

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

387387 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

388388 PPi expl (nsroot pname) NoFC pty $

389389 PPi expl recName NoFC sty (substInput sty)

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

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

391391

392392 -- | The "_set" name.

393393 set_pname :: Name

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

401401

402402 -- | The left-hand side of the update function.

403403 generateLhs :: PTerm

404− generateLhs = PApp fc (PRef fc set_pname) [pexp $ PRef fc pname_in, pexp constructorPattern]

404+ generateLhs = PApp fc (PRef fc [] set_pname) [pexp $ PRef fc [] pname_in, pexp constructorPattern]

405405 where

406406 constructorPattern :: PTerm

407− constructorPattern = PApp fc (PRef fc cn) args

407+ constructorPattern = PApp fc (PRef fc [] cn) args

408408

409409 -- | The "_in" name.

410410 pname_in :: Name

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

415415

416416 -- | The right-hand side of the update function.

417417 generateRhs :: PTerm

418− generateRhs = PApp fc (PRef fc cn) (newArgs i args)

418+ generateRhs = PApp fc (PRef fc [] cn) (newArgs i args)

419419 where

420420 newArgs :: Int -> [PArg] -> [PArg]

421− newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest

421+ newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest

422422 newArgs i (x : rest) = x : (newArgs (i-1) rest)

423423 newArgs _ [] = []

424424

@@ -440,17 +440,17 @@ asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t

440440recName :: Name

441441recName = sMN 0 "rec"

442442

443−recRef = PRef emptyFC recName

443+recRef = PRef emptyFC [] recName

444444

445445projectInType :: [(Name, Name)] -> PTerm -> PTerm

446446projectInType xs = mapPT st

447447 where

448448 st :: PTerm -> PTerm

449− st (PRef fc n)

450− | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

449+ st (PRef fc hls n)

450+ | Just pn <- lookup n xs = PApp fc (PRef fc hls pn) [pexp recRef]

451451 st t = t

452452

453453-- | Creates an PArg from a plicity and a name where the term is a PRef.

454454asPRefArg :: Plicity -> Name -> PArg

455−asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)

455+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC [] (nsroot n)

456456

src/Idris/Elab/Term.hs+66−62

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

289289 env <- get_env

290290 handleError (forceErr t' env)

291291 (elab' ina fc' t')

292− (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

292+ (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

293293 [pimp (sUN "t") Placeholder True,

294294 pimp (sUN "a") Placeholder True,

295295 pexp ct]))

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

308308 forceErr orig env (At _ t) = forceErr orig env t

309309 forceErr orig env t = False

310310

311− notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

311+ notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

312312 notDelay _ = True

313313

314314 local f = do e <- get_env

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

350350 do hnf_compute

351351 g <- goal

352352 case g of

353− TType _ -> elab' ina (Just fc) (PRef fc unitTy)

354− UType _ -> elab' ina (Just fc) (PRef fc unitTy)

355− _ -> elab' ina (Just fc) (PRef fc unitCon)

353+ TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

354+ UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

355+ _ -> elab' ina (Just fc) (PRef fc [] unitCon)

356356 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

357357 = do g <- goal; resolveTC False False 5 g fn ist

358358 elab' ina fc (PResolveTC fc')

@@ -360,14 +360,14 @@ elab ist info emode opts fn tm

360360 instanceArg c

361361 -- Elaborate the equality type first homogeneously, then

362362 -- heterogeneously as a fallback

363− elab' ina _ (PApp fc (PRef _ n) args)

363+ elab' ina _ (PApp fc (PRef _ _ n) args)

364364 | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

365365 = try (do tyn <- getNameFrom (sMN 0 "aqty")

366366 claim tyn RType

367367 movelast tyn

368− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

369− [pimp (sUN "A") (PRef NoFC tyn) True,

370− pimp (sUN "B") (PRef NoFC tyn) False,

368+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

369+ [pimp (sUN "A") (PRef NoFC [] tyn) True,

370+ pimp (sUN "B") (PRef NoFC [] tyn) False,

371371 pexp l, pexp r]))

372372 (do atyn <- getNameFrom (sMN 0 "aqty")

373373 btyn <- getNameFrom (sMN 0 "bqty")

@@ -375,27 +375,27 @@ elab ist info emode opts fn tm

375375 movelast atyn

376376 claim btyn RType

377377 movelast btyn

378− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

379− [pimp (sUN "A") (PRef NoFC atyn) True,

380− pimp (sUN "B") (PRef NoFC btyn) False,

378+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

379+ [pimp (sUN "A") (PRef NoFC [] atyn) True,

380+ pimp (sUN "B") (PRef NoFC [] btyn) False,

381381 pexp l, pexp r]))

382382

383− elab' ina _ (PPair fc _ l r)

383+ elab' ina _ (PPair fc hls _ l r)

384384 = do hnf_compute

385385 g <- goal

386386 let (tc, _) = unApply g

387387 case g of

388− TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)

388+ TType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairTy)

389389 [pexp l,pexp r])

390− UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)

390+ UType _ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairTy)

391391 [pexp l,pexp r])

392392 _ -> case tc of

393393 P _ n _ | n == upairTy

394− -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)

394+ -> elab' ina (Just fc) (PApp fc (PRef fc hls upairCon)

395395 [pimp (sUN "A") Placeholder False,

396396 pimp (sUN "B") Placeholder False,

397397 pexp l, pexp r])

398− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)

398+ _ -> elab' ina (Just fc) (PApp fc (PRef fc hls pairCon)

399399 [pimp (sUN "A") Placeholder False,

400400 pimp (sUN "B") Placeholder False,

401401 pexp l, pexp r])

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

409409-- pexp l, pexp r]))

410410-- True

411411

412− elab' ina _ (PDPair fc p l@(PRef nfc n) t r)

412+ elab' ina _ (PDPair fc hls p l@(PRef nfc hl n) t r)

413413 = case t of

414414 Placeholder ->

415415 do hnf_compute

@@ -418,17 +418,18 @@ elab ist info emode opts fn tm

418418 TType _ -> asType

419419 _ -> asValue

420420 _ -> asType

421− where asType = elab' ina (Just fc) (PApp fc (PRef NoFC sigmaTy)

421+ where asType = elab' ina (Just fc) (PApp fc (PRef NoFC hls sigmaTy)

422422 [pexp t,

423423 pexp (PLam fc n nfc Placeholder r)])

424− asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

424+ asValue = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

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

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

427427 pexp l, pexp r])

428− elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

429− [pimp (sMN 0 "a") t False,

430− pimp (sMN 0 "P") Placeholder True,

431− pexp l, pexp r])

428+

429+ elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

430+ [pimp (sMN 0 "a") t False,

431+ pimp (sMN 0 "P") Placeholder True,

432+ pexp l, pexp r])

432433 elab' ina fc (PAlternative ms (ExactlyOne delayok) as)

433434 = do as_pruned <- doPrune as

434435 -- Finish the mkUniqueNames job with the pruned set, rather than

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

455456 [x] -> elab' ina fc x

456457 _ -> tryAll (zip (map (elab' ina fc) as'')

457458 (map showHd as'')))

458− where showHd (PApp _ (PRef _ n) _) = n

459− showHd (PRef _ n) = n

459+ where showHd (PApp _ (PRef _ _ n) _) = n

460+ showHd (PRef _ _ n) = n

460461 showHd (PApp _ h _) = showHd h

461462 showHd x = NErased -- We probably should do something better than this here

462463

@@ -528,14 +529,14 @@ elab ist info emode opts fn tm

528529 pruneAlts _ alts _ = filter isLend alts

529530

530531 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

531− hasArg n env (PApp _ (PRef _ a) _)

532+ hasArg n env (PApp _ (PRef _ _ a) _)

532533 = case lookupTyExact a (tt_ctxt ist) of

533534 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

534535 any (fnIs n) args

535536 Nothing -> False

536537 hasArg n _ _ = False

537538

538− isLend (PApp _ (PRef _ l) _) = l == sNS (sUN "lend") ["Ownership"]

539+ isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]

539540 isLend _ = False

540541

541542 fnIs n ty = case unApply ty of

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

556557-- elab' (_, _, inty) (PRef fc f)

557558-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

558559-- = lift $ tfail (Msg "Typecase is not allowed")

559− elab' ec _ tm@(PRef fc n)

560+ elab' ec _ tm@(PRef fc hl n)

560561 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

561562 && isTConName n (tt_ctxt ist)

562563 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

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

596597 bindable (NS _ _) = False

597598 bindable (UN xs) = True

598599 bindable n = implicitable n

599− elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp NoFC f [])

600− elab' ina fc' tm@(PRef fc n)

600+ elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

601+ elab' ina fc' tm@(PRef fc hls n)

601602 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

602603 && isTConName n (tt_ctxt ist)

603604 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -611,9 +612,10 @@ elab ist info emode opts fn tm

611612 if null a'

612613 then erun fc $

613614 do apply (Var n) []

614− hl <- findHighlight n

615+ hilite <- findHighlight n

615616 solve

616− highlightSource fc hl

617+ mapM_ (uncurry highlightSource) $

618+ (fc, hilite) : map (\f -> (f, hilite)) hls

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

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

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

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

663665 elabE ec' fc sc

664666 solve

665667 highlightSource nfc (AnnBoundName n False)

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

668+ elab' ina _ tm@(PLet fc n nfc ty val sc)

667669 = do attack

668670 ivs <- get_instances

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

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

716718 solve

717719-- elab' ina fc (PLet n Placeholder

718720-- (PApp fc r [pexp (delab ist rty)]) sc)

719− elab' ina _ tm@(PApp fc (PInferRef _ f) args) = do

721+ elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do

720722 rty <- goal

721723 ds <- get_deferred

722724 ctxt <- get_context

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

747749 fnTy [] ret = forget ret

748750 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

749751

750− localVar env (PRef _ x)

752+ localVar env (PRef _ _ x)

751753 = case lookup x env of

752754 Just _ -> Just x

753755 _ -> Nothing

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

771773 solve

772774 -- if f is local, just do a simple_app

773775 -- FIXME: Anyone feel like refactoring this mess? - EB

774− elab' ina topfc tm@(PApp fc (PRef ffc f) args_in)

776+ elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in)

775777 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

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

777779 | otherwise = implicitApp $

@@ -793,11 +795,12 @@ elab ist info emode opts fn tm

793795 if (f `elem` map fst env && length args == 1 && length args_in == 1)

794796 then -- simple app, as below

795797 do simple_app False

796− (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc f))

798+ (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))

797799 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

798800 (show tm)

799801 solve

800− highlightSource ffc annot

802+ mapM (uncurry highlightSource) $

803+ (ffc, annot) : map (\f -> (f, annot)) hls

801804 return []

802805 else

803806 do ivs <- get_instances

@@ -823,7 +826,8 @@ elab ist info emode opts fn tm

823826 ulog <- getUnifyLog

824827

825828 annot <- findHighlight f

826− highlightSource ffc annot

829+ mapM (uncurry highlightSource) $

830+ (ffc, annot) : map (\f -> (f, annot)) hls

827831

828832 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

829833 [] fc False f

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

921925 tacTm (PProof _) = True

922926 tacTm _ = False

923927

924− setInjective (PRef _ n) = setinj n

925− setInjective (PApp _ (PRef _ n) _) = setinj n

928+ setInjective (PRef _ _ n) = setinj n

929+ setInjective (PApp _ (PRef _ _ n) _) = setinj n

926930 setInjective _ = return ()

927931

928932 elab' ina _ tm@(PApp fc f [arg]) =

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

932936 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

933937 (show tm)

934938 solve

935− where headRef (PRef _ _) = True

939+ where headRef (PRef _ _ _) = True

936940 headRef (PApp _ f _) = headRef f

937941 headRef (PAlternative _ _ as) = all headRef as

938942 headRef _ = False

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

994998 elab' ina (Just fc) t

995999 focus valn

9961000 elab' ina (Just fc) sc

997− elab' ina (Just fc) (PRef fc letn)

1001+ elab' ina (Just fc) (PRef fc [] letn)

9981002 solve

9991003 elab' ina _ c@(PCase fc scr opts)

10001004 = do attack

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

12331237 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

12341238

12351239 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1236− isScr (PRef _ n) (n', b) = (n', (n == n', b))

1240+ isScr (PRef _ _ n) (n', b) = (n', (n == n', b))

12371241 isScr _ (n', b) = (n', (False, b))

12381242

12391243 caseBlock :: FC -> Name

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

12621266

12631267 getNmScr (n, (s, _)) = (n, s)

12641268

1265− mkarg (n, s) = (PRef fc n, s)

1269+ mkarg (n, s) = (PRef fc [] n, s)

12661270 -- may be shadowed names in the new pattern - so replace the

12671271 -- old ones with an _

12681272 -- Also, names which don't appear on the rhs should not be

@@ -1272,34 +1276,34 @@ elab ist info emode opts fn tm

12721276 = let args' = map (shadowed (allNamesIn l)) args

12731277 args'' = map (implicitable (allNamesIn r ++

12741278 keepscrName scr)) args'

1275− lhs = PApp (getFC fc l) (PRef NoFC n)

1279+ lhs = PApp (getFC fc l) (PRef NoFC [] n)

12761280 (map (mkLHSarg l) args'') in

12771281 PClause (getFC fc l) n lhs [] r []

12781282

12791283 -- Keep scrutinee available if it's just a name (this makes

12801284 -- the names in scope look better when looking at a hole on

12811285 -- the rhs of a case)

1282− keepscrName (PRef _ n) = [n]

1286+ keepscrName (PRef _ _ n) = [n]

12831287 keepscrName _ = []

12841288

12851289 mkLHSarg l (tm, True) = pexp l

12861290 mkLHSarg l (tm, False) = pexp tm

12871291

1288− shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)

1292+ shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)

12891293 shadowed new t = t

12901294

1291− implicitable rhs (PRef _ n, s) | n `notElem` rhs = (Placeholder, s)

1295+ implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)

12921296 implicitable rhs t = t

12931297

12941298

12951299 getFC d (PApp fc _ _) = fc

1296− getFC d (PRef fc _) = fc

1300+ getFC d (PRef fc _ _) = fc

12971301 getFC d (PAlternative _ _ (x:_)) = getFC d x

12981302 getFC d x = d

12991303

13001304 insertLazy :: PTerm -> ElabD PTerm

1301− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

1302− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

1305+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1306+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

13031307 insertLazy (PCoerced t) = return t

13041308 insertLazy t =

13051309 do ty <- goal

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

13141318 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)

13151319 mkDelay env t

13161320 = let fc = fileFC "Delay" in

1317− addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

1321+ addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))

13181322 [pexp t])

13191323

13201324

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

13231327 -- blowup especially where there are errors deep in large expressions.

13241328 notImplicitable (PApp _ f _) = notImplicitable f

13251329 -- TMP HACK no coercing on bind (make this configurable)

1326− notImplicitable (PRef _ n)

1330+ notImplicitable (PRef _ _ n)

13271331 | [opts] <- lookupCtxt n (idris_flags ist)

13281332 = NoImplicit `elem` opts

13291333 notImplicitable (PAlternative _ (ExactlyOne _) as) = any notImplicitable as

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

13751379 where

13761380 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

13771381 addImplBound ist (map fst env)

1378− (PApp fc (PRef fc n) [pexp (PCoerced t)])

1382+ (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

13791383

13801384 -- | Elaborate the arguments to a function

13811385 elabArgs :: IState -- ^ The current Idris state

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

14381442pruneAlt :: [PTerm] -> [PTerm]

14391443pruneAlt xs = map prune xs

14401444 where

1441− prune (PApp fc1 (PRef fc2 f) as)

1442− = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1445+ prune (PApp fc1 (PRef fc2 hls f) as)

1446+ = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

14431447 prune t = t

14441448

14451449 choose f (PAlternative ms a as)

@@ -1452,7 +1456,7 @@ pruneAlt xs = map prune xs

14521456 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

14531457 choose f t = t

14541458

1455− headIs f (PApp _ (PRef _ f') _) = f == f'

1459+ headIs f (PApp _ (PRef _ _ f') _) = f == f'

14561460 headIs f (PApp _ f' _) = headIs f f'

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

14581462

@@ -1469,7 +1473,7 @@ pruneByType env t c as

14691473 | Just n <- getName t,

14701474 n `elem` map fst env = Just t

14711475 | otherwise = locallyBound ts

1472− getName (PRef _ n) = Just n

1476+ getName (PRef _ _ n) = Just n

14731477 getName (PApp _ f _) = getName f

14741478 getName (PHidden t) = getName t

14751479 getName _ = Nothing

@@ -1489,8 +1493,8 @@ pruneByType env (P _ n _) ist as

14891493 where

14901494 ctxt = tt_ctxt ist

14911495

1492− headIs var f (PRef _ f') = typeHead var f f'

1493− headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1496+ headIs var f (PRef _ _ f') = typeHead var f f'

1497+ headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

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

14951499 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

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

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

@@ -49,7 +49,7 @@ import Data.List.Split (splitOn)

4949import Util.Pretty(pretty, text)

5050

5151elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

52−elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

52+elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

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

@@ -129,7 +129,7 @@ decorateid decorate (PClauses f o n cs)

129129 dc (PWith fc n t as w pn ds)

130130 = PWith fc (decorate n) (dappname t) as w pn

131131 (map (decorateid decorate) ds)

132− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

132+ dappname (PApp fc (PRef fc' hl n) as) = PApp fc (PRef fc' hl (decorate n)) as

133133 dappname t = t

134134

135135

src/Idris/Elab/Value.hs+4−4

@@ -121,15 +121,15 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

121121-- (as a default numeric tye), then printing it as any Showable thing

122122elabExec :: FC -> PTerm -> PTerm

123123elabExec fc tm = runtm (PAlternative [] FirstSuccess

124− [printtm (PApp fc (PRef fc (sUN "the"))

124+ [printtm (PApp fc (PRef fc [] (sUN "the"))

125125 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

126126 tm,

127127 printtm tm

128128 ])

129129 where

130− runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

131− printtm t = PApp fc (PRef fc (sUN "printLn"))

132− [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]

131+ printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132+ [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133133

134134elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

135135elabREPL info aspat tm

src/Idris/ElabDecls.hs+2−2

@@ -68,8 +68,8 @@ recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'

6868-- | Return the elaborated term which calls 'main'

6969elabMain :: Idris Term

7070elabMain = do (m, _) <- elabVal recinfo ERHS

71− (PApp fc (PRef fc (sUN "run__IO"))

72− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

71+ (PApp fc (PRef fc [] (sUN "run__IO"))

72+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

7373 return m

7474 where fc = fileFC "toplevel"

7575

src/Idris/ElabQuasiquote.hs+5−5

@@ -116,15 +116,15 @@ extractUnquotes n (PRewrite fc x y z)

116116 Just zz -> do (z', ex3) <- extractUnquotes n zz

117117 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)

118118 Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)

119−extractUnquotes n (PPair fc info l r)

119+extractUnquotes n (PPair fc hls info l r)

120120 = do (l', ex1) <- extractUnquotes n l

121121 (r', ex2) <- extractUnquotes n r

122− return (PPair fc info l' r', ex1 ++ ex2)

123−extractUnquotes n (PDPair fc info a b c)

122+ return (PPair fc hls info l' r', ex1 ++ ex2)

123+extractUnquotes n (PDPair fc hls info a b c)

124124 = do (a', ex1) <- extractUnquotes n a

125125 (b', ex2) <- extractUnquotes n b

126126 (c', ex3) <- extractUnquotes n c

127− return (PDPair fc info a' b' c', ex1 ++ ex2 ++ ex3)

127+ return (PDPair fc hls info a' b' c', ex1 ++ ex2 ++ ex3)

128128extractUnquotes n (PAlternative ms b alts)

129129 = do alts' <- mapM (extractUnquotes n) alts

130130 let (alts'', exs) = unzip alts'

@@ -163,7 +163,7 @@ extractUnquotes n (PQuasiquote tm goal)

163163 = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm

164164extractUnquotes n (PUnquote tm)

165165 | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")

166− return (PRef (fileFC "(unquote)") n, [(n, tm)])

166+ return (PRef (fileFC "(unquote)") [] n, [(n, tm)])

167167 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

168168 extractUnquotes (n-1) tm

169169extractUnquotes n (PRunElab fc tm ns)

src/Idris/Error.hs+4−4

@@ -88,8 +88,8 @@ getErrSpan _ = emptyFC

8888-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent

8989warnDisamb :: IState -> PTerm -> Idris ()

9090warnDisamb ist (PQuote _) = return ()

91−warnDisamb ist (PRef _ _) = return ()

92−warnDisamb ist (PInferRef _ _) = return ()

91+warnDisamb ist (PRef _ _ _) = return ()

92+warnDisamb ist (PInferRef _ _ _) = return ()

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

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

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

@@ -107,8 +107,8 @@ warnDisamb ist (PTrue _ _) = return ()

107107warnDisamb ist (PResolveTC _) = return ()

108108warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

109109 Foldable.mapM_ (warnDisamb ist) z

110−warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y

111−warnDisamb ist (PDPair _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

110+warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

111+warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

112112warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms

113113warnDisamb ist (PHidden tm) = warnDisamb ist tm

114114warnDisamb ist (PType _) = return ()

src/Idris/IBC.hs+30−22

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 115

43+ibcVersion = 116

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -1522,12 +1522,14 @@ instance Binary PTerm where

15221522 = case x of

15231523 PQuote x1 -> do putWord8 0

15241524 put x1

1525− PRef x1 x2 -> do putWord8 1

1526− put x1

1527− put x2

1528− PInferRef x1 x2 -> do putWord8 2

1529− put x1

1530− put x2

1525+ PRef x1 x2 x3 -> do putWord8 1

1526+ put x1

1527+ put x2

1528+ put x3

1529+ PInferRef x1 x2 x3 -> do putWord8 2

1530+ put x1

1531+ put x2

1532+ put x3

15311533 PPatvar x1 x2 -> do putWord8 3

15321534 put x1

15331535 put x2

@@ -1579,17 +1581,19 @@ instance Binary PTerm where

15791581 put x2

15801582 put x3

15811583 put x4

1582− PPair x1 x2 x3 x4 -> do putWord8 18

1583− put x1

1584− put x2

1585− put x3

1586− put x4

1587− PDPair x1 x2 x3 x4 x5 -> do putWord8 19

1588− put x1

1589− put x2

1590− put x3

1591− put x4

1592− put x5

1584+ PPair x1 x2 x3 x4 x5 -> do putWord8 18

1585+ put x1

1586+ put x2

1587+ put x3

1588+ put x4

1589+ put x5

1590+ PDPair x1 x2 x3 x4 x5 x6 -> do putWord8 19

1591+ put x1

1592+ put x2

1593+ put x3

1594+ put x4

1595+ put x5

1596+ put x6

15931597 PAlternative x1 x2 x3 -> do putWord8 20

15941598 put x1

15951599 put x2

@@ -1664,10 +1668,12 @@ instance Binary PTerm where

16641668 return (PQuote x1)

16651669 1 -> do x1 <- get

16661670 x2 <- get

1667− return (PRef x1 x2)

1671+ x3 <- get

1672+ return (PRef x1 x2 x3)

16681673 2 -> do x1 <- get

16691674 x2 <- get

1670− return (PInferRef x1 x2)

1675+ x3 <- get

1676+ return (PInferRef x1 x2 x3)

16711677 3 -> do x1 <- get

16721678 x2 <- get

16731679 return (PPatvar x1 x2)

@@ -1722,13 +1728,15 @@ instance Binary PTerm where

17221728 x2 <- get

17231729 x3 <- get

17241730 x4 <- get

1725− return (PPair x1 x2 x3 x4)

1731+ x5 <- get

1732+ return (PPair x1 x2 x3 x4 x5)

17261733 19 -> do x1 <- get

17271734 x2 <- get

17281735 x3 <- get

17291736 x4 <- get

17301737 x5 <- get

1731− return (PDPair x1 x2 x3 x4 x5)

1738+ x6 <- get

1739+ return (PDPair x1 x2 x3 x4 x5 x6)

17321740 20 -> do x1 <- get

17331741 x2 <- get

17341742 x3 <- get

src/Idris/IdrisDoc.hs+4−4

@@ -288,8 +288,8 @@ loadDocs ist n

288288-- TODO: Remove unnecessary cases

289289extractPTermNames :: PTerm -- ^ Where to extract names from

290290 -> [Name] -- ^ Extracted names

291−extractPTermNames (PRef _ n) = [n]

292−extractPTermNames (PInferRef _ n) = [n]

291+extractPTermNames (PRef _ _ n) = [n]

292+extractPTermNames (PInferRef _ _ n) = [n]

293293extractPTermNames (PPatvar _ n) = [n]

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

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

@@ -306,8 +306,8 @@ extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

306306extractPTermNames (PRewrite _ a b m) | Just c <- m =

307307 concatMap extract [a, b, c]

308308extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

309−extractPTermNames (PPair _ _ p1 p2) = concatMap extract [p1, p2]

310−extractPTermNames (PDPair _ _ a b c) = concatMap extract [a, b, c]

309+extractPTermNames (PPair _ _ _ p1 p2) = concatMap extract [p1, p2]

310+extractPTermNames (PDPair _ _ _ a b c) = concatMap extract [a, b, c]

311311extractPTermNames (PAlternative _ _ l) = concatMap extract l

312312extractPTermNames (PHidden p) = extract p

313313extractPTermNames (PGoal _ p1 n p2) = n : concatMap extract [p1, p2]

src/Idris/Interactive.hs+5−5

@@ -112,7 +112,7 @@ addMissing fn updatefile l n

112112 else iPrintResult extras

113113 where showPat = show . stripNS

114114 stripNS tm = mapPT dens tm where

115− dens (PRef fc n) = PRef fc (nsroot n)

115+ dens (PRef fc hls n) = PRef fc hls (nsroot n)

116116 dens t = t

117117

118118 nsroot (NS n _) = nsroot n

@@ -120,7 +120,7 @@ addMissing fn updatefile l n

120120 nsroot n = n

121121

122122 getAppName (PApp _ r _) = getAppName r

123− getAppName (PRef _ r) = r

123+ getAppName (PRef _ _ r) = r

124124 getAppName _ = n

125125

126126 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

@@ -178,10 +178,10 @@ doProofSearch fn updatefile rec l n hints (Just depth)

178178 let fc = fileFC fn

179179 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

180180 (ProofSearch rec False depth t hints)]

181− let def = PClause fc mn (PRef fc mn) [] (body top) []

181+ let def = PClause fc mn (PRef fc [] mn) [] (body top) []

182182 newmv <- idrisCatch

183183 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

184− (tm, ty) <- elabVal recinfo ERHS (PRef fc mn)

184+ (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)

185185 ctxt <- getContext

186186 i <- getIState

187187 return . flip displayS "" . renderPretty 1.0 80 $

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

204204 dropCtxt _ t = t

205205

206206 stripNS tm = mapPT dens tm where

207− dens (PRef fc n) = PRef fc (nsroot n)

207+ dens (PRef fc hls n) = PRef fc hls (nsroot n)

208208 dens t = t

209209

210210 nsroot (NS n _) = nsroot n

src/Idris/ParseData.hs+1−1

@@ -218,7 +218,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

218218 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

219219 cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

220220 terminator

221− let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

221+ let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

222222 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

223223 do let cty = bindArgs cargs conty

224224 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

src/Idris/ParseExpr.hs+71−65

@@ -174,9 +174,9 @@ extension syn ns rules =

174174 _ -> n

175175

176176 update :: [(Name, SynMatch)] -> PTerm -> PTerm

177− update ns (PRef fc n) = case lookup n ns of

178− Just (SynTm t) -> t

179− _ -> PRef fc n

177+ update ns (PRef fc hls n) = case lookup n ns of

178+ Just (SynTm t) -> t

179+ _ -> PRef fc hls n

180180 update ns (PLam fc n nfc ty sc)

181181 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)

182182 update ns (PPi p n fc ty sc)

@@ -193,9 +193,9 @@ extension syn ns rules =

193193 = PCase fc (update ns c) (map (pmap (update ns)) opts)

194194 update ns (PIfThenElse fc c t f)

195195 = PIfThenElse fc (update ns c) (update ns t) (update ns f)

196− update ns (PPair fc p l r) = PPair fc p (update ns l) (update ns r)

197− update ns (PDPair fc p l t r)

198− = PDPair fc p (update ns l) (update ns t) (update ns r)

196+ update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

197+ update ns (PDPair fc hls p l t r)

198+ = PDPair fc hls p (update ns l) (update ns t) (update ns r)

199199 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)

200200 update ns (PHidden t) = PHidden (update ns t)

201201 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -346,7 +346,7 @@ simpleExpr syn =

346346 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

347347 return (PMetavar (FC f (l, c-1) end) x)

348348 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

349− <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc (SN $ ElimN t))

349+ <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

350350 <|> proofExpr syn

351351 <|> tacticsExpr syn

352352 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

@@ -358,16 +358,16 @@ simpleExpr syn =

358358 fc <- getFC

359359 return (modifyConst syn fc (PConstant cfc c))

360360 <|> do symbol "'"; fc <- getFC; str <- fst <$> name

361− return (PApp fc (PRef fc (sUN "Symbol_"))

361+ return (PApp fc (PRef fc [] (sUN "Symbol_"))

362362 [pexp (PConstant NoFC (Str (show str)))])

363363 <|> do (x, fc) <- fnName

364364 if inPattern syn

365− then option (PRef fc x)

365+ then option (PRef fc [fc] x)

366366 (do reservedOp "@"

367367 s <- simpleExpr syn

368368 fcIn <- getFC

369369 return (PAs fcIn x s))

370− else return (PRef fc x)

370+ else return (PRef fc [fc] x)

371371 <|> idiom syn

372372 <|> listExpr syn

373373 <|> alt syn

@@ -388,9 +388,9 @@ Bracketed ::= '(' Bracketed'

388388@

389389 -}

390390bracketed :: SyntaxInfo -> IdrisParser PTerm

391−bracketed syn = do fc <- getFC

391+bracketed syn = do (FC fn (sl, sc) _) <- getFC

392392 lchar '(' <?> "parenthesized expression"

393− bracketed' fc syn

393+ bracketed' (FC fn (sl, sc) (sl, sc+1)) syn

394394{- |Parses the rest of an expression in braces

395395@

396396Bracketed' ::=

@@ -409,52 +409,52 @@ bracketed' open syn =

409409 do (FC f start (l, c)) <- getFC

410410 lchar ')'

411411 return $ PTrue (spanFC open (FC f start (l, c+1))) TypeOrTerm

412− <|> try (do (ln, lnfc) <- name; lchar ':';

412+ <|> try (do (ln, lnfc) <- name

413+ colonFC <- lcharFC ':'

413414 lty <- expr syn

414− reservedOp "**"

415+ starsFC <- reservedOpFC "**"

415416 fc <- getFC

416417 r <- expr syn

417− lchar ')'

418− return (PDPair fc TypeOrTerm (PRef lnfc ln) lty r))

418+ close <- lcharFC ')'

419+ return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))

419420 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

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

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

422423 then fail "minus not allowed in section"

423424 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

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

425− pexp e]))

425+ (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),

426+ pexp e]))

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

427428 op <- option Nothing (do o <- operator

428429 lchar ')'

429430 return (Just o))

430431 fc0 <- getFC

431432 case op of

432− Nothing -> bracketedExpr syn l

433+ Nothing -> bracketedExpr syn open l

433434 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

434− (PApp fc0 (PRef fc0 (sUN o)) [pexp l,

435− pexp (PRef fc0 (sMN 1000 "ARG"))]))

435+ (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

436+ pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

436437 <|> do l <- expr syn

437− bracketedExpr syn l

438+ bracketedExpr syn open l

438439

439−bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm

440−bracketedExpr syn e =

440+-- | Parse the contents of parentheses, after an expression has been parsed.

441+bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

442+bracketedExpr syn openParenFC e =

441443 do lchar ')'; return e

442− <|> do fc <- do fc <- getFC

443− lchar ','

444− return fc

445− rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')

446− lchar ')'

447− return $ PPair fc TypeOrTerm e (mergePairs rs)

448− <|> do fc <- do fc <- getFC

449− reservedOp "**"

450− return fc

444+ <|> do exprs <- many (do comma <- lcharFC ','

445+ r <- expr syn

446+ return (r, comma))

447+ closeParenFC <- lcharFC ')'

448+ let hilite = [openParenFC, closeParenFC] ++ map snd exprs

449+ return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

450+ <|> do starsFC <- reservedOpFC "**"

451451 r <- expr syn

452− lchar ')'

453− return (PDPair fc TypeOrTerm e Placeholder r)

452+ closeParenFC <- lcharFC ')'

453+ return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)

454454 <?> "end of bracketed expression"

455455 where mergePairs :: [(PTerm, FC)] -> PTerm

456456 mergePairs [(t, fc)] = t

457− mergePairs ((t, fc):rs) = PPair fc TypeOrTerm t (mergePairs rs)

457+ mergePairs ((t, fc):rs) = PPair fc [] TypeOrTerm t (mergePairs rs)

458458

459459-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

460460-- big integer, otherwise try fromInteger and the constants as alternatives.

@@ -465,7 +465,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

465465modifyConst syn fc (PConstant inFC (BI x))

466466 | not (inPattern syn)

467467 = PAlternative [] FirstSuccess

468− (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

468+ (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

469469 : consts)

470470 | otherwise = PAlternative [] FirstSuccess consts

471471 where

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

580580 return (PLet fc (sMN 0 "match") NoFC

581581 f

582582 (PMatchApp fc ff)

583− (PRef fc (sMN 0 "match")))

583+ (PRef fc [] (sMN 0 "match")))

584584 <?> "matching application expression") <|> (do

585585 fc <- getFC

586586 i <- get

@@ -589,17 +589,17 @@ app syn = do f <- simpleExpr syn

589589 [] -> return f

590590 _ -> return (flattenFromInt fc f args))

591591 <?> "function application"

592− where

592+ where

593593 -- bit of a hack to deal with the situation where we're applying a

594594 -- literal to an argument, which we may want for obscure applications

595595 -- of fromInteger, and this will help disambiguate better.

596596 -- We know, at least, it won't be one of the constants!

597597 flattenFromInt fc (PAlternative _ x alts) args

598598 | Just i <- getFromInt alts

599− = PApp fc (PRef fc (sUN "fromInteger")) (i : args)

599+ = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

600600 flattenFromInt fc f args = PApp fc f args

601601

602− getFromInt ((PApp _ (PRef _ n) [a]) : _) | n == sUN "fromInteger" = Just a

602+ getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a

603603 getFromInt (_ : xs) = getFromInt xs

604604 getFromInt _ = Nothing

605605

@@ -628,10 +628,10 @@ ImplicitArg ::=

628628-}

629629implicitArg :: SyntaxInfo -> IdrisParser PArg

630630implicitArg syn = do lchar '{'

631− n <- fst <$> name

631+ (n, nfc) <- name

632632 fc <- getFC

633− v <- option (PRef fc n) (do lchar '='

634− expr syn)

633+ v <- option (PRef nfc [nfc] n) (do lchar '='

634+ expr syn)

635635 lchar '}'

636636 return (pimp n v True)

637637 <?> "implicit function argument"

@@ -735,14 +735,14 @@ recordType syn =

735735 case rec of

736736 Nothing ->

737737 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

738− (applyAll fc fields (PRef fc (sMN 0 "fldx"))))

738+ (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))

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

740740 Right fields ->

741741 case rec of

742742 Nothing ->

743743 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

744− (getAll fc (reverse fields)

745− (PRef fc (sMN 0 "fldx"))))

744+ (getAll fc (reverse fields)

745+ (PRef fc [] (sMN 0 "fldx"))))

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

747747

748748 <?> "record setting expression"

@@ -766,17 +766,17 @@ recordType syn =

766766 applyAll fc [] x = x

767767 applyAll fc ((ns, e) : es) x

768768 = applyAll fc es (doUpdate fc ns e x)

769−

769+

770770 doUpdate fc [n] e get

771− = PApp fc (PRef fc (mkType n)) [pexp e, pexp get]

771+ = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]

772772 doUpdate fc (n : ns) e get

773− = PApp fc (PRef fc (mkType n))

774− [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),

773+ = PApp fc (PRef fc [] (mkType n))

774+ [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),

775775 pexp get]

776776

777777 getAll :: FC -> [Name] -> PTerm -> PTerm

778− getAll fc [n] e = PApp fc (PRef fc n) [pexp e]

779− getAll fc (n:ns) e = PApp fc (PRef fc n) [pexp (getAll fc ns e)]

778+ getAll fc [n] e = PApp fc (PRef fc [] n) [pexp e]

779+ getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]

780780

781781

782782-- | Creates setters for record types on necessary functions

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

838838 pmList [] sc = sc

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

840840 = PLam fc (sMN i "lamp") NoFC Placeholder

841− (PCase fc (PRef fc (sMN i "lamp"))

841+ (PCase fc (PRef fc [] (sMN i "lamp"))

842842 [(x, pmList xs sc)])

843843 lambdaTail :: IdrisParser PTerm

844844 lambdaTail = impossible <|> symbol "=>" *> expr syn

@@ -859,7 +859,7 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"

859859 highlightP kw AnnKeyword

860860 highlightP kw' AnnKeyword

861861 return (PRewrite fc

862− (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

862+ (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc

863863 giving)

864864 <?> "term rewrite expression"

865865

@@ -882,7 +882,7 @@ let_ syn = try (do kw <- reservedFC "let"

882882 return (buildLets ls sc))

883883 <?> "let binding"

884884 where buildLets [] sc = sc

885− buildLets ((fc, PRef nfc n, ty, v, []) : ls) sc

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

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

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

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

@@ -1144,20 +1144,26 @@ listExpr syn = do (FC f (l, c) _) <- getFC

11441144 qs <- sepBy1 (do_ syn) (lchar ',')

11451145 lchar ']'

11461146 return (PDoBlock (map addGuard qs ++

1147− [DoExp fc (PApp fc (PRef fc (sUN "return"))

1147+ [DoExp fc (PApp fc (PRef fc [] (sUN "return"))

11481148 [pexp x])]))) <|>

1149− (do xs <- many ((lchar ',' <?> "list element") *> expr syn)

1149+ (do xs <- many (do (FC fn (sl, sc) _) <- getFC

1150+ lchar ',' <?> "list element"

1151+ let commaFC = FC fn (sl, sc) (sl, sc + 1)

1152+ elt <- expr syn

1153+ return (elt, commaFC))

1154+ (FC fn (sl, sc) _) <- getFC

11501155 lchar ']' <?> "end of list expression"

1151− return (mkList fc (x:xs))))

1156+ let rbrackFC = FC fn (sl, sc) (sl, sc+1)

1157+ return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))

11521158 <?> "list expression"

11531159 where

11541160 mkNil :: FC -> PTerm

1155− mkNil fc = PRef fc (sUN "Nil")

1156− mkList :: FC -> [PTerm] -> PTerm

1157− mkList fc [] = PRef NoFC (sUN "Nil")

1158− mkList fc (x : xs) = PApp fc (PRef NoFC (sUN "::")) [pexp x, pexp (mkList fc xs)]

1161+ mkNil fc = PRef fc [fc] (sUN "Nil")

1162+ mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm

1163+ mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")

1164+ mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]

11591165 addGuard :: PDo -> PDo

1160− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

1166+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc [] (sUN "guard"))

11611167 [pexp e])

11621168 addGuard x = x

11631169

@@ -1216,7 +1222,7 @@ do_ syn

12161222 option (DoBind fc i ifc e)

12171223 (do lchar '|'

12181224 ts <- sepBy1 (do_alt syn) (lchar '|')

1219− return (DoBindP fc (PRef ifc i) e ts)))

1225+ return (DoBindP fc (PRef ifc [ifc] i) e ts)))

12201226 <|> try (do i <- expr' syn

12211227 symbol "<-"

12221228 fc <- getFC

src/Idris/ParseHelpers.hs+6

@@ -260,6 +260,12 @@ string = Chr.string

260260lchar :: MonadicParsing m => Char -> m Char

261261lchar = token . char

262262

263+-- | Parses a character as a token, returning the source span of the character

264+lcharFC :: MonadicParsing m => Char -> m FC

265+lcharFC ch = do (FC file (l, c) _) <- getFC

266+ _ <- token (char ch)

267+ return $ FC file (l, c) (l, c+1)

268+

263269-- | Parses string as a token

264270symbol :: MonadicParsing m => String -> m String

265271symbol = Tok.symbol

src/Idris/ParseOps.hs+5−5

@@ -35,11 +35,11 @@ import Debug.Trace

3535-- using pre-build and user-defined operator/fixity declarations

3636table :: [FixDecl] -> OperatorTable IdrisParser PTerm

3737table fixes

38− = [[prefix "-" (\fc x -> PApp fc (PRef fc (sUN "negate")) [pexp x])]] ++

38+ = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

3939 toTable (reverse fixes) ++

4040 [[backtick],

4141 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

42− [binary "=" (\fc x y -> PApp fc (PRef fc eqTy) [pexp x, pexp y]) AssocLeft],

42+ [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],

4343 [nofixityoperator]]

4444 where

4545 flatten :: PTerm -> PTerm -- flatten application

@@ -52,9 +52,9 @@ toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

5252toTable fs = map (map toBin)

5353 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

5454 where toBin (Fix (PrefixN _) op) = prefix op

55− (\fc x -> PApp fc (PRef fc (sUN op)) [pexp x])

55+ (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])

5656 toBin (Fix f op)

57− = binary op (\fc x y -> PApp fc (PRef fc (sUN op)) [pexp x,pexp y]) (assoc f)

57+ = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)

5858 assoc (Infixl _) = AssocLeft

5959 assoc (Infixr _) = AssocRight

6060 assoc (InfixN _) = AssocNone

@@ -79,7 +79,7 @@ backtick = Infix (do indentPropHolds gtProp

7979 lchar '`'; (n, fc) <- fnName

8080 lchar '`'

8181 indentPropHolds gtProp

82− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82+ return (\x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y])) AssocNone

8383

8484-- | Operator without fixity (throws an error)

8585nofixityoperator :: Operator IdrisParser PTerm

src/Idris/Parser.hs+7−7

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

324324 uniquifyBinders userNames = fixBind []

325325 where

326326 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm

327− fixBind rens (PRef fc n) | Just n' <- lookup n rens =

328− return $ PRef fc n'

327+ fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =

328+ return $ PRef fc hls n'

329329 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =

330330 return $ PPatvar fc n'

331331 fixBind rens (PLam fc n nfc ty body)

@@ -735,7 +735,7 @@ instance_ syn = do (doc, argDocs)

735735 let cs' = [(c, ty) | (c, _, ty) <- cs]

736736 (cn, cnfc) <- fnName

737737 args <- many (simpleExpr syn)

738− let sc = PApp fc (PRef cnfc cn) (map pexp args)

738+ let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

739739 let t = bindList (PPi constraint) cs sc

740740 ds <- option [] (instanceBlock syn)

741741 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]

@@ -953,7 +953,7 @@ clause syn

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

954954 ty

955955 (PMatchApp fc n)

956− (PRef fc (sMN 0 "match"))

956+ (PRef fc [] (sMN 0 "match"))

957957 ist <- get

958958 put (ist { lastParse = Just n })

959959 return $ PClause fc n capp [] r wheres

@@ -976,7 +976,7 @@ clause syn

976976 do terminator

977977 return ([], [])]

978978 ist <- get

979− let capp = PApp fc (PRef nfc n) [pexp l, pexp r]

979+ let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

980980 put (ist { lastParse = Just n })

981981 return $ PClause fc n capp wargs rs wheres) <|> (do

982982 popIndent

@@ -987,7 +987,7 @@ clause syn

987987 ds <- some $ fnDecl syn

988988 closeBlock

989989 ist <- get

990− let capp = PApp fc (PRef fc n) [pexp l, pexp r]

990+ let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]

991991 let withs = map (fillLHSD n capp wargs) $ concat ds

992992 put (ist { lastParse = Just n })

993993 return $ PWith fc n capp wargs wval pn withs)

@@ -998,7 +998,7 @@ clause syn

998998 args <- many (try (implicitArg (syn { inPattern = True } ))

999999 <|> (fmap pexp (argExpr syn)))

10001000 wargs <- many (wExpr syn)

1001− let capp = PApp fc (PRef nfc n)

1001+ let capp = PApp fc (PRef nfc [nfc] n)

10021002 (cargs ++ args)

10031003 (do r <- rhs syn n

10041004 ist <- get

src/Idris/PartialEval.hs+3−3

@@ -206,8 +206,8 @@ mkNewPats ist d ns newname sname lhs rhs =

206206 mkClause (oldlhs, oldrhs)

207207 = let (_, as) = unApply oldlhs

208208 lhsargs = mkLHSargs [] ns as

209− lhs = PApp emptyFC (PRef emptyFC newname) lhsargs

210− rhs = PApp emptyFC (PRef emptyFC sname)

209+ lhs = PApp emptyFC (PRef emptyFC [] newname) lhsargs

210+ rhs = PApp emptyFC (PRef emptyFC [] sname)

211211 (mkRHSargs ns lhsargs) in

212212 (lhs, rhs)

213213

@@ -245,7 +245,7 @@ mkNewPats ist d ns newname sname lhs rhs =

245245mkPE_TermDecl :: IState -> Name -> Name ->

246246 [(PEArgType, Term)] -> PEDecl

247247mkPE_TermDecl ist newname sname ns

248− = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))

248+ = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))

249249 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

250250 patdef = lookupCtxtExact sname (idris_patdefs ist)

251251 newpats = case patdef of

src/Idris/ProofSearch.hs+4−4

@@ -25,8 +25,8 @@ trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

2525trivial = trivialHoles []

2626

2727trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

29− = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

28+trivialHoles ok elab ist

29+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

3030 return ())

3131 (do env <- get_env

3232 g <- goal

@@ -42,7 +42,7 @@ trivialHoles ok elab ist

4242 -- anywhere but the top is okay for a hole, if holesOK set

4343 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

4444 holesOK hs (binderTy b)

45− then try' (elab (PRef (fileFC "prf") x))

45+ then try' (elab (PRef (fileFC "prf") [] x))

4646 (tryAll xs) True

4747 else tryAll xs

4848

@@ -227,7 +227,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

227227 = do let a = getPArity (delab ist (binderTy t))

228228 tryLocalArg d locs tys n a

229229

230− tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)

230+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)

231231 tryLocalArg d locs tys n i

232232 = simple_app False (tryLocalArg d locs tys n (i - 1))

233233 (psRec True d locs tys) "proof search local apply"

src/Idris/Prover.hs+3−3

@@ -310,7 +310,7 @@ elabloop fn d prompt prf e prev h env

310310 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))

311311 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm

312312 return (d', prev, st', done, prf', env, go)

313− ECheck (PRef _ n) ->

313+ ECheck (PRef _ _ n) ->

314314 do (d', st', done, prf', go) <- checkNameType e prf n

315315 return (d', prev, st', done, prf', env, go)

316316 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm

@@ -331,7 +331,7 @@ elabloop fn d prompt prf e prev h env

331331 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

332332 DoLet fc i ifc ty expr ->

333333 do (tm, ty) <- elabVal recinfo ERHS

334− (PApp NoFC (PRef NoFC (sUN "the"))

334+ (PApp NoFC (PRef NoFC [] (sUN "the"))

335335 [ pexp (inLets ist env ty)

336336 , pexp (inLets ist env expr)

337337 ])

@@ -417,7 +417,7 @@ ploop fn d prompt prf e h

417417 when (not (null hs)) $ ifail "Incomplete proof"

418418 iputStrLn "Proof completed!"

419419 return (False, e, True, prf, Right $ iPrintResult "")

420− Success (TCheck (PRef _ n)) -> checkNameType e prf n

420+ Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

421421 Success (TCheck t) -> checkType e prf t

422422 Success (TEval t) -> evalTerm e prf t

423423 Success (TDocStr x) -> docStr e prf x

src/Idris/Providers.hs+1−1

@@ -10,7 +10,7 @@ import Idris.Error

1010-- | Wrap a type provider in the type of type providers

1111providerTy :: FC -> PTerm -> PTerm

1212providerTy fc tm

13− = PApp fc (PRef fc $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]

13+ = PApp fc (PRef fc [] $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]

1414

1515ioret :: Name

1616ioret = sUN "prim_io_return"

src/Idris/REPL.hs+6−6

@@ -345,7 +345,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

345345 case splitName name of

346346 Left err -> iPrintError err

347347 Right n -> process "(idemode)"

348− (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

348+ (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

349349runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

350350 case parseConst orig name of

351351 Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

@@ -581,7 +581,7 @@ idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)

581581 iPrintResult "defined"

582582idemodeProcess fn (Undefine n) = process fn (Undefine n)

583583idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

584−idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

584+idemodeProcess fn (Check (PRef x hls n)) = process fn (Check (PRef x hls n))

585585idemodeProcess fn (Check t) = process fn (Check t)

586586idemodeProcess fn (Core t) = process fn (Core t)

587587idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

@@ -893,7 +893,7 @@ process fn (ExecVal t)

893893 prettyIst ist (delab ist ty'))

894894 iPrintTermWithType resOut tyOut

895895

896−process fn (Check (PRef _ n))

896+process fn (Check (PRef _ _ n))

897897 = do ctxt <- getContext

898898 ist <- getIState

899899 let ppo = ppOptionIst ist

@@ -1173,8 +1173,8 @@ process fn (Compile codegen f)

11731173 let iface = Interface `elem` opts

11741174 m <- if iface then return Nothing else

11751175 do (m', _) <- elabVal recinfo ERHS

1176− (PApp fc (PRef fc (sUN "run__IO"))

1177− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1176+ (PApp fc (PRef fc [] (sUN "run__IO"))

1177+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

11781178 return (Just m')

11791179 ir <- compile codegen f m

11801180 i <- getIState

@@ -1345,7 +1345,7 @@ process fn (TransformInfo n)

13451345-- iputStrLn "---------------"

13461346-- showTrans i ts

13471347

1348−process fn (PPrint fmt width (PRef _ n))

1348+process fn (PPrint fmt width (PRef _ _ n))

13491349 = do outs <- pprintDef n

13501350 iPrintResult =<< renderExternal fmt width (vsep outs)

13511351

src/Idris/REPLParser.hs+1−1

@@ -304,7 +304,7 @@ cmd_execute name = do

304304 tm <- option maintm (P.fullExpr defaultSyntax)

305305 return (Right (Execute tm))

306306 where

307− maintm = PRef (fileFC "(repl)") (sNS (sUN "main") ["Main"])

307+ maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

308308

309309

310310cmd_dynamic :: String -> P.IdrisParser (Either String Command)