a54852b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Highlighting for pairs, lists and sigmas

Now, the elaborator supports highlighting of pairs, lists, and sigmas in their sugared for, revealing the underlying names in the highlight. This means that tooltips in Emacs and any other editor supporting highlighting can now show how a particular notation was disambiguated - Vects and Lists give different tooltips, and pair types have blue parentheses and commas while pair values have red ones. Likewise for dependent pairs.

commita54852bb11631b5933caee6c8c5a1d7b4df04e0e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 17 Jul 2015, 20:54 (11 years ago) parent3cd25e6

15 files changed+176−166

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+43−43 src/Idris/AbsSyntaxTree.hs+30−30 src/Idris/Coverage.hs+4−4 src/Idris/DSL.hs+11−11 src/Idris/DeepSeq.hs+3−3 src/Idris/Delaborate.hs+11−11 src/Idris/Elab/Class.hs+2−2 src/Idris/Elab/Record.hs+2−2 src/Idris/Elab/Term.hs+13−13 src/Idris/ElabQuasiquote.hs+4−4 src/Idris/Error.hs+2−2 src/Idris/IBC.hs+17−13 src/Idris/IdrisDoc.hs+2−2 src/Idris/ParseExpr.hs+26−26 src/Idris/ParseHelpers.hs+6

src/Idris/AbsSyntax.hs+43−43

@@ -998,14 +998,14 @@ 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' fcs 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' fcs 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)

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)

10091009 en (PAlternative a as) = PAlternative a (map en as)

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

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

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

11051105

11061106 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

@@ -1175,8 +1175,8 @@ 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)))

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

11801180 pri (PAlternative a as) = maximum (map pri as)

11811181 pri (PConstant _ _) = 0

11821182 pri Placeholder = 1

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

@@ -1559,15 +1559,15 @@ 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 a as)

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

15731573 PAlternative a as'

@@ -1616,7 +1616,8 @@ addImpl' inpat env infns imp_meths ist ptm

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

@@ -1803,11 +1804,11 @@ 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

18131814 PRef _ _ _ -> return fn

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

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

@@ -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 a as) = PAlternative a (map (sm xs) as)

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

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

@@ -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 a as) = PAlternative a (map sm as)

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

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

@@ -2167,10 +2167,10 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

21672167 return $! PCase fc t' alts'

21682168 mkUniq (PIfThenElse fc c t f)

21692169 = liftM3 (PIfThenElse fc) (mkUniq c) (mkUniq t) (mkUniq f)

2170− mkUniq (PPair fc p l r)

2170+ mkUniq (PPair fc hls p l r)

21712171 = do l' <- mkUniq l; r' <- mkUniq r

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

2173− mkUniq (PDPair fc p (PRef fc' hl n) t sc)

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

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

21742174 | t /= Placeholder

21752175 = do env <- get

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

@@ -2180,10 +2180,10 @@ mkUniqueNames env tm = evalState (mkUniq tm) (S.fromList env) where

21802180 put (S.insert n' env)

21812181 t' <- mkUniq t

21822182 sc'' <- mkUniq sc'

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

2184− mkUniq (PDPair fc p l t r)

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

2184+ mkUniq (PDPair fc hls p l t r)

21852185 = do l' <- mkUniq l; t' <- mkUniq t; r' <- mkUniq r

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

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

21872187 mkUniq (PAlternative b as)

21882188 = liftM (PAlternative b) (mapM mkUniq as)

21892189 mkUniq (PHidden t) = liftM PHidden (mkUniq t)

src/Idris/AbsSyntaxTree.hs+30−30

@@ -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 PAltType [PTerm] -- ^ True if only one may work. (| A, B, C|)

854854 | PHidden PTerm -- ^ Irrelevant or hidden pattern

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

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

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

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

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

904−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)

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

904+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)

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

906906mapPTermFC f g (PAlternative ty ts) = PAlternative ty (map (mapPTermFC f g) ts)

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

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

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

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

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

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

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

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

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

955955 mpt (PAlternative a as) = PAlternative a (map (mapPT f) as)

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

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

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

11191119highestFC (PTrue fc _) = Just fc

11201120highestFC (PResolveTC fc) = Just fc

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

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

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

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

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

11241124highestFC (PAs fc _ _) = Just fc

11251125highestFC (PAlternative _ args) =

11261126 case mapMaybe highestFC args of

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

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

16781678 prettySe d p bnd (PTyped l r) =

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

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

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

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

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

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

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

16851685 TypeOrTerm -> id

16861686 IsType -> annName pairTy

16871687 IsTerm -> annName pairCon

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

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

16891689 depth d $

16901690 annotated lparen <>

16911691 left <+>

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

18091809 slist _ _ _ _ = Nothing

18101810

18111811 pairElts :: PTerm -> Maybe [PTerm]

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

1813− | otherwise = Just [x, y]

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

1813+ | otherwise = Just [x, y]

18141814 pairElts _ = Nothing

18151815

18161816 natns = "Prelude.Nat."

@@ -2006,8 +2006,8 @@ instance Sized PTerm where

20062006 size (PTrue fc _) = 1

20072007 size (PResolveTC fc) = 1

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

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

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

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

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

20112011 size (PAlternative a alts) = 1 + size alts

20122012 size (PHidden hidden) = size hidden

20132013 size (PUnifyLog tm) = size tm

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

20482048 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

20552055 ni env (PAlternative a ls) = concatMap (ni env) ls

20562056 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

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

20812081 ni set (PAlternative a as) = niTms set as

20822082 ni set (PHidden tm) = ni set tm

20832083 ni set (PUnifyLog tm) = ni set tm

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

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

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

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

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

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

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

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

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

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

21202120 ni env (PAlternative a as) = concatMap (ni env) as

21212121 ni env (PHidden tm) = ni env tm

21222122 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

21502150 ni env (PAlternative a as) = concatMap (ni env) as

21512151 ni env (PHidden tm) = ni env tm

21522152 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

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

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

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

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

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

21812181 ni env (PAlternative a as) = concatMap (ni env) as

21822182 ni env (PHidden tm) = ni env tm

21832183 ni env (PUnifyLog tm) = ni env tm

src/Idris/Coverage.hs+4−4

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

216216 otherPats :: PTerm -> [PTerm]

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

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

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

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

@@ -245,10 +245,10 @@ genAll i args

245245 -- put it back to its original form

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

247247 | ei == txt "Ex_intro"

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

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

249249 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

src/Idris/DSL.hs+11−11

@@ -77,9 +77,9 @@ expandSugar dsl (PIfThenElse fc c t f) =

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 a as) = PAlternative a (map (expandSugar dsl) as)

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

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

@@ -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 a as) = PAlternative 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)

@@ -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+3−3

@@ -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) = rnf x1 `seq` rnf x2 `seq` ()

250250 rnf (PHidden x1) = rnf x1 `seq` ()

src/Idris/Delaborate.hs+11−11

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

@@ -553,15 +553,15 @@ 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

@@ -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/Elab/Class.hs+2−2

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

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

@@ -446,8 +446,8 @@ projectInType :: [(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.

src/Idris/Elab/Term.hs+13−13

@@ -380,22 +380,22 @@ elab ist info emode opts fn tm

380380 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 hl 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,17 @@ 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+ elab' ina _ (PDPair fc hls p l t r) = elab' ina (Just fc) (PApp fc (PRef fc hls sigmaCon)

429+ [pimp (sMN 0 "a") t False,

430+ pimp (sMN 0 "P") Placeholder True,

431+ pexp l, pexp r])

432432 elab' ina fc (PAlternative (ExactlyOne delayok) as)

433433 = do as' <- doPrune as

434434 (h : hs) <- get_holes

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

594594 elabE ec' fc sc

595595 solve

596596 highlightSource nfc (AnnBoundName n False)

597− elab' ina _ (PLet fc n nfc ty val sc)

597+ elab' ina _ tm@(PLet fc n nfc ty val sc)

598598 = do attack

599599 ivs <- get_instances

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

src/Idris/ElabQuasiquote.hs+4−4

@@ -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 b alts)

129129 = do alts' <- mapM (extractUnquotes n) alts

130130 let (alts'', exs) = unzip alts'

src/Idris/Error.hs+2−2

@@ -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+17−13

@@ -1581,17 +1581,19 @@ instance Binary PTerm where

15811581 put x2

15821582 put x3

15831583 put x4

1584− PPair x1 x2 x3 x4 -> do putWord8 18

1585− put x1

1586− put x2

1587− put x3

1588− put x4

1589− PDPair x1 x2 x3 x4 x5 -> do putWord8 19

1590− put x1

1591− put x2

1592− put x3

1593− put x4

1594− 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

15951597 PAlternative x1 x2 -> do putWord8 20

15961598 put x1

15971599 put x2

@@ -1725,13 +1727,15 @@ instance Binary PTerm where

17251727 x2 <- get

17261728 x3 <- get

17271729 x4 <- get

1728− return (PPair x1 x2 x3 x4)

1730+ x5 <- get

1731+ return (PPair x1 x2 x3 x4 x5)

17291732 19 -> do x1 <- get

17301733 x2 <- get

17311734 x3 <- get

17321735 x4 <- get

17331736 x5 <- get

1734− return (PDPair x1 x2 x3 x4 x5)

1737+ x6 <- get

1738+ return (PDPair x1 x2 x3 x4 x5 x6)

17351739 20 -> do x1 <- get

17361740 x2 <- get

17371741 return (PAlternative x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -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/ParseExpr.hs+26−26

@@ -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 a as) = PAlternative a (map (update ns) as)

200200 update ns (PHidden t) = PHidden (update ns t)

201201 update ns (PDoBlock ds) = PDoBlock $ upd ns ds

@@ -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,13 +409,14 @@ 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 == "!")

@@ -429,32 +430,31 @@ bracketed' open syn =

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

434435 (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

435436 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.

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

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