a54852b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Highlighting for pairs, lists and sigmas

a54852bDavid Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+43−43

compare with master

unifiedsplit

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

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

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

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

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

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

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

1006 en (PTyped l r) = PTyped (en l) (en r)

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

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

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

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

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

1010 en (PHidden t) = PHidden (en t)

1011 en (PUnifyLog t) = PUnifyLog (en t)

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

1105

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

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

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

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

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

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

1110 bnames _ = []

1111

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

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

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

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

1177 pri (PTyped l r) = pri l

1178− pri (PPair _ _ l r) = max 1 (max (pri l) (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)))

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)

1181 pri (PConstant _ _) = 0

1182 pri Placeholder = 1

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

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

1487 imps top env (PTyped l r)

1488 = imps top env l

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

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

1490 = do (decls, ns) <- get

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

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

1494 = do (decls, ns) <- get

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

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

1498 = do (decls, ns) <- get

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

1500 namesIn uvars ist r

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

1559 = let l' = ai qq env ds l

1560 r' = ai qq env ds r in

1561 PTyped l' r'

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

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

1563 = let l' = ai qq env ds l

1564 r' = ai qq env ds r in

1565− PPair fc p l' r'

1565+ PPair fc hls p l' r'

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

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

1567 = let l' = ai qq env ds l

1568 t' = ai qq env ds t

1569 r' = ai qq env ds r in

1570− PDPair fc p l' t' r'

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

1571 ai qq env ds (PAlternative a as)

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

1573 PAlternative a as'

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

1616 val' = ai qq env ds val

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

1618 PLet fc n nfc ty' val' sc'

1619+ defs ->

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

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

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

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

1621 = let ty' = ai qq env ds ty

1622 = let ty' = ai qq env ds ty

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

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

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

1803 as' <- slAlts ns as

1804 as' <- slAlts ns as

1804 return (a' : as')

1805 return (a' : as')

1805 slAlts ns [] = return []

1806 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 (PPair fc hls p l r) = do l' <- sl l; r' <- sl r; return (PPair fc hls p l' r')

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

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

1808− t' <- sl t

1809+ t' <- sl t

1809− r' <- sl r

1810+ r' <- sl r

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

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

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

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

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

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

1813 PRef _ _ _ -> return fn

1814 PRef _ _ _ -> return fn

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

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

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

1853 if null alts' then Placeholder

1854 if null alts' then Placeholder

1854 else PAlternative b alts'

1855 else PAlternative b alts'

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

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

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

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

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

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

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

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

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

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

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

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

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

1878

1879

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

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

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

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

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

1882− runState (pos ns ss tm) []

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

1883 where fs (PPi p n fc t sc)

1884 | Static <- pstatic p

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

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

1969 return (ml ++ mr)

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

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

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

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

1973− mr <- match' r r'

1973+ mr <- match' r r'

1974− return (ml ++ mr)

1974+ return (ml ++ mr)

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

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

1976− mt <- match' t t'

1976+ mt <- match' t t'

1977− mr <- match' r r'

1977+ mr <- match' r r'

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

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

1979 match (PAlternative a as) (PAlternative a' as')

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

1981 return (concat ms)

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

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

2059 (fmap (sm xs) tm)

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

2061+ sm xs (PPair f hls p x y) = PPair f hls 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)

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

2063 sm xs (PAlternative a as) = PAlternative a (map (sm xs) as)

2064 sm xs (PHidden x) = PHidden (sm xs x)

2065 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

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

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

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

2087 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

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

2090 sm (PAlternative a as) = PAlternative a (map sm as)

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

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

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

2167 return $! PCase fc t' alts'

2168 mkUniq (PIfThenElse fc c t f)

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

2170− mkUniq (PPair fc p l r)

2170+ mkUniq (PPair fc hls p l r)

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

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

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

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

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

2174 | t /= Placeholder

2175 = do env <- get

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

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

2180 put (S.insert n' env)

2181 t' <- mkUniq t

2182 sc'' <- mkUniq sc'

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

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

2184− mkUniq (PDPair fc p l t r)

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

2185 = 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'

2187 mkUniq (PAlternative b as)

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

2189 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

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

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

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

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

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.

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

853 | PAlternative PAltType [PTerm] -- ^ True if only one may work. (| A, B, C|)

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

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

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

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

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 info t1 t2 t3) = PDPair (f fc) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

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)

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

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

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

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

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

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

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

953+ mpt (PPair fc hls p l r) = PPair fc hls 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)

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

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

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

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

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

1119highestFC (PTrue fc _) = Just fc

1120highestFC (PResolveTC fc) = Just fc

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

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

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

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

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

1124highestFC (PAs fc _ _) = Just fc

1125highestFC (PAlternative _ args) =

1126 case mapMaybe highestFC args of

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

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

1678 prettySe d p bnd (PTyped l r) =

1679 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

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

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

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

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

1685 TypeOrTerm -> id

1686 IsType -> annName pairTy

1687 IsTerm -> annName pairCon

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

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

1689 depth d $

1690 annotated lparen <>

1691 left <+>

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

1809 slist _ _ _ _ = Nothing

1810

1811 pairElts :: PTerm -> Maybe [PTerm]

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

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

1813− | otherwise = Just [x, y]

1813+ | otherwise = Just [x, y]

1814 pairElts _ = Nothing

1815

1816 natns = "Prelude.Nat."

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

2006 size (PTrue fc _) = 1

2007 size (PResolveTC fc) = 1

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

2009− size (PPair 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

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

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

2012 size (PHidden hidden) = size hidden

2013 size (PUnifyLog tm) = size tm

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

2048 ni env (PHidden tm) = ni env tm

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

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

2051− ni env (PPair _ _ 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

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

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

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

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

2056 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

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

2078− ni set (PPair _ _ 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

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

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

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

2082 ni set (PHidden tm) = ni set tm

2083 ni set (PUnifyLog tm) = ni set tm

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

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

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

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

2117− ni env (PPair _ _ 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

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

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

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

2121 ni env (PHidden tm) = ni env tm

2122 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

2147− ni env (PPair _ _ 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

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

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

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

2151 ni env (PHidden tm) = ni env tm

2152 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

2178− ni env (PPair _ _ 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

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

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

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

2182 ni env (PHidden tm) = ni env tm

2183 ni env (PUnifyLog tm) = ni env tm

src/Idris/Coverage.hs+4−4

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

216 otherPats :: PTerm -> [PTerm]

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 _ l r)

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

220 = ops fc pairCon

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

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

223 [pexp l, pexp r]) o

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

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

225 = ops fc (sUN "Ex_intro")

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

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

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

245 -- put it back to its original form

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

247 | ei == txt "Ex_intro"

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

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

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

250 | n == pairCon

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

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

252 resugar t = t

253

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

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

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

79 ]

80−expandSugar dsl (PPair fc p l r) = PPair fc p (expandSugar dsl l) (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 p l t r) = PDPair fc p (expandSugar dsl l) (expandSugar dsl t)

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

82− (expandSugar dsl r)

82+ (expandSugar dsl r)

83expandSugar dsl (PAlternative a as) = PAlternative a (map (expandSugar dsl) as)

84expandSugar dsl (PHidden t) = PHidden (expandSugar dsl t)

85expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

@@ -137,8 +137,8 @@ var dsl n t i = v' i t where

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

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

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

140+ v' i (PPair f hls p l r) = PPair f hls 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)

141+ v' i (PDPair f hls p l t r) = PDPair f hls p (v' i l) (v' i t) (v' i r)

142 v' i (PAlternative a as) = PAlternative a $ map (v' i) as

143 v' i (PHidden t) = PHidden (v' i t)

144 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

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

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

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

195− db' (PPair fc p l r) = do l' <- db' l

195+ db' (PPair fc hls p l r) = do l' <- db' l

196− r' <- db' r

196+ r' <- db' r

197− return (PPair fc p l' r')

197+ return (PPair fc hls p l' r')

198− db' (PDPair fc p l t r) = do l' <- db' l

198+ db' (PDPair fc hls p l t r) = do l' <- db' l

199− r' <- db' r

199+ r' <- db' r

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

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

201 db' (PRunElab fc t ns) = fmap (\tm -> PRunElab fc tm ns) (db' t)

202 db' t = return t

203

src/Idris/DeepSeq.hs+3−3

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

242 rnf (PResolveTC x1) = rnf x1 `seq` ()

243 rnf (PRewrite x1 x2 x3 x4)

244 = 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` ()

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)

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

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

248 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

249 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

250 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

154

155 deFn env (App _ f a) args = deFn env f (a:args)

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

158 | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

159 deFn env (P _ n _) [ty, Bind x (Lam _) r]

160 | n == sigmaTy

161− = PDPair un IsType (PRef un [] x) (de env [] ty)

161+ = PDPair un [] IsType (PRef un [] x) (de env [] ty)

162 (de ((x,x):env) [] (instantiate (P Bound x ty) r))

163 deFn env (P _ n _) [lt,rt,l,r]

164− | n == pairCon = PPair un IsTerm (de env [] l) (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

165+ | n == sigmaCon = PDPair un [] IsTerm (de env [] l) Placeholder

166− (de env [] r)

166+ (de env [] r)

167 deFn env f@(P _ n _) args

168 | n `elem` map snd env

169 = PApp un (de env [] f) (map pexp (map (de env []) args))

@@ -553,15 +553,15 @@ addImplicitDiffs x y

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

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

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

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

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

559− (PPair fc pi a' b', PPair fc' pi' c' d')

559+ (PPair fc hls pi a' b', PPair fc' hls' pi' c' d')

560− addI (PDPair fc pi a t b) (PDPair fc' pi' c u d)

560+ addI (PDPair fc hls pi a t b) (PDPair fc' hls' pi' c u d)

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

562 (t', u') = addI t u

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

565 addI x y = (x, y)

566

567 -- Just the ones which appear desugared in errors

@@ -573,8 +573,8 @@ addImplicitDiffs x y

573 = n == n' && expLike s s' && expLike t t'

574 expLike (PLam _ n _ s t) (PLam _ n' _ s' t')

575 = n == n' && expLike s s' && expLike t t'

576− expLike (PPair _ _ x y) (PPair _ _ 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'

577+ expLike (PDPair _ _ _ x _ y) (PDPair _ _ _ x' _ y') = expLike x x' && expLike y y'

578 expLike x y = x == y

579

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

269 -- to the other methods in the class

270 constrainMeths :: [Name] -> Name -> PTerm -> PTerm

271 constrainMeths allM dictN tm = transform (addC allM dictN) tm

272− addC allM dictN m@(PRef fc [] n)

272+ addC allM dictN m@(PRef fc hls n)

273− | n `elem` allM = PApp NoFC m [pconst (PRef NoFC [] dictN)]

273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC hls dictN)]

274 | otherwise = m

275 addC _ _ tm = tm

276

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

@@ -446,8 +446,8 @@ projectInType :: [(Name, Name)] -> PTerm -> PTerm

446projectInType xs = mapPT st

447 where

448 st :: PTerm -> PTerm

449− st (PRef fc [] n)

449+ st (PRef fc hls n)

450− | Just pn <- lookup n xs = PApp fc (PRef fc [] pn) [pexp recRef]

450+ | Just pn <- lookup n xs = PApp fc (PRef fc hls pn) [pexp recRef]

451 st t = t

452

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

380 pimp (sUN "B") (PRef NoFC [] btyn) False,

381 pexp l, pexp r]))

382

383− elab' ina _ (PPair fc _ l r)

383+ elab' ina _ (PPair fc hls _ l r)

384 = do hnf_compute

385 g <- goal

386 let (tc, _) = unApply g

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

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

391 [pexp l,pexp r])

392 _ -> case tc of

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

395 [pimp (sUN "A") Placeholder False,

396 pimp (sUN "B") Placeholder False,

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

399 [pimp (sUN "A") Placeholder False,

400 pimp (sUN "B") Placeholder False,

401 pexp l, pexp r])

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

409-- pexp l, pexp r]))

410-- True

411

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)

413 = case t of

414 Placeholder ->

415 do hnf_compute

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

418 TType _ -> asType

419 _ -> asValue

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

422 [pexp t,

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

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

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

427 pexp l, pexp r])

428− elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc [] sigmaCon)

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,

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

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

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

431− pexp l, pexp r])

431+ pexp l, pexp r])

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

433 = do as' <- doPrune as

434 (h : hs) <- get_holes

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

594 elabE ec' fc sc

595 solve

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

598 = do attack

599 ivs <- get_instances

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

src/Idris/ElabQuasiquote.hs+4−4

@@ -116,15 +116,15 @@ extractUnquotes n (PRewrite fc x y z)

116 Just zz -> do (z', ex3) <- extractUnquotes n zz

117 return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)

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

120 = do (l', ex1) <- extractUnquotes n l

121 (r', ex2) <- extractUnquotes n r

122− return (PPair fc info l' r', ex1 ++ ex2)

122+ return (PPair fc hls info l' r', ex1 ++ ex2)

123−extractUnquotes n (PDPair fc info a b c)

123+extractUnquotes n (PDPair fc hls info a b c)

124 = do (a', ex1) <- extractUnquotes n a

125 (b', ex2) <- extractUnquotes n b

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

128extractUnquotes n (PAlternative b alts)

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

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

src/Idris/Error.hs+2−2

@@ -107,8 +107,8 @@ warnDisamb ist (PTrue _ _) = return ()

107warnDisamb ist (PResolveTC _) = return ()

108warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

109 Foldable.mapM_ (warnDisamb ist) z

110−warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y

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

111+warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

112warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms

113warnDisamb ist (PHidden tm) = warnDisamb ist tm

114warnDisamb ist (PType _) = return ()

src/Idris/IBC.hs+17−13

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

1581 put x2

1582 put x3

1583 put x4

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

1584+ PPair x1 x2 x3 x4 x5 -> do putWord8 18

1585− put x1

1585+ put x1

1586− put x2

1586+ put x2

1587− put x3

1587+ put x3

1588− put x4

1588+ put x4

1589+ put x5

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

1590+ PDPair x1 x2 x3 x4 x5 x6 -> do putWord8 19

1590− put x1

1591+ put x1

1591− put x2

1592+ put x2

1592− put x3

1593+ put x3

1593− put x4

1594+ put x4

1594− put x5

1595+ put x5

1596+ put x6

1595 PAlternative x1 x2 -> do putWord8 20

1597 PAlternative x1 x2 -> do putWord8 20

1596 put x1

1598 put x1

1597 put x2

1599 put x2

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

1725 x2 <- get

1727 x2 <- get

1726 x3 <- get

1728 x3 <- get

1727 x4 <- get

1729 x4 <- get

1730+ x5 <- get

1728− return (PPair x1 x2 x3 x4)

1731+ return (PPair x1 x2 x3 x4 x5)

1729 19 -> do x1 <- get

1732 19 -> do x1 <- get

1730 x2 <- get

1733 x2 <- get

1731 x3 <- get

1734 x3 <- get

1732 x4 <- get

1735 x4 <- get

1733 x5 <- get

1736 x5 <- get

1737+ x6 <- get

1734− return (PDPair x1 x2 x3 x4 x5)

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

1735 20 -> do x1 <- get

1739 20 -> do x1 <- get

1736 x2 <- get

1740 x2 <- get

1737 return (PAlternative x1 x2)

1741 return (PAlternative x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -306,8 +306,8 @@ extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

306extractPTermNames (PRewrite _ a b m) | Just c <- m =

307 concatMap extract [a, b, c]

308extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

309−extractPTermNames (PPair _ _ p1 p2) = concatMap extract [p1, p2]

309+extractPTermNames (PPair _ _ _ p1 p2) = concatMap extract [p1, p2]

310−extractPTermNames (PDPair _ _ a b c) = concatMap extract [a, b, c]

310+extractPTermNames (PDPair _ _ _ a b c) = concatMap extract [a, b, c]

311extractPTermNames (PAlternative _ l) = concatMap extract l

312extractPTermNames (PHidden p) = extract p

313extractPTermNames (PGoal _ p1 n p2) = n : concatMap extract [p1, p2]

src/Idris/ParseExpr.hs+26−26

@@ -193,9 +193,9 @@ extension syn ns rules =

193 = PCase fc (update ns c) (map (pmap (update ns)) opts)

194 update ns (PIfThenElse fc c t f)

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

196+ update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

197− update ns (PDPair fc p l t r)

197+ update ns (PDPair fc hls p l t r)

198− = PDPair fc p (update ns l) (update ns t) (update ns r)

198+ = PDPair fc hls p (update ns l) (update ns t) (update ns r)

199 update ns (PAlternative a as) = PAlternative a (map (update ns) as)

200 update ns (PHidden t) = PHidden (update ns t)

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

@@ -388,9 +388,9 @@ Bracketed ::= '(' Bracketed'

388@

389 -}

390bracketed :: SyntaxInfo -> IdrisParser PTerm

391−bracketed syn = do fc <- getFC

391+bracketed syn = do (FC fn (sl, sc) _) <- getFC

392 lchar '(' <?> "parenthesized expression"

393− bracketed' fc syn

393+ bracketed' (FC fn (sl, sc) (sl, sc+1)) syn

394{- |Parses the rest of an expression in braces

395@

396Bracketed' ::=

@@ -409,13 +409,14 @@ bracketed' open syn =

409 do (FC f start (l, c)) <- getFC

410 lchar ')'

411 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 ':'

413 lty <- expr syn

414 lty <- expr syn

414− reservedOp "**"

415+ starsFC <- reservedOpFC "**"

415 fc <- getFC

416 fc <- getFC

416 r <- expr syn

417 r <- expr syn

417− lchar ')'

418+ close <- lcharFC ')'

418− return (PDPair fc TypeOrTerm (PRef lnfc [] ln) lty r))

419+ return (PDPair fc [open, colonFC, starsFC, close] TypeOrTerm (PRef lnfc [] ln) lty r))

419 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

420 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

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

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

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

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

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

429 return (Just o))

430 return (Just o))

430 fc0 <- getFC

431 fc0 <- getFC

431 case op of

432 case op of

432− Nothing -> bracketedExpr syn l

433+ Nothing -> bracketedExpr syn open l

433 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

434 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

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

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

435 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

436 pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

436 <|> do l <- expr syn

437 <|> do l <- expr syn

437− bracketedExpr syn l

438+ bracketedExpr syn open l

438

439

440+-- | Parse the contents of parentheses, after an expression has been parsed.

439−bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm

441+bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

440−bracketedExpr syn e =

442+bracketedExpr syn openParenFC e =

441 do lchar ')'; return e

443 do lchar ')'; return e

442− <|> do fc <- do fc <- getFC

444+ <|> do exprs <- many (do comma <- lcharFC ','

443− lchar ','

445+ r <- expr syn

444− return fc

446+ return (r, comma))

445− rs <- sepBy1 (do fc' <- getFC; r <- expr syn; return (r, fc')) (lchar ',')

447+ closeParenFC <- lcharFC ')'

446− lchar ')'

448+ let hilite = [openParenFC, closeParenFC] ++ map snd exprs

447− return $ PPair fc TypeOrTerm e (mergePairs rs)

449+ return $ PPair openParenFC hilite TypeOrTerm e (mergePairs exprs)

448− <|> do fc <- do fc <- getFC

450+ <|> do starsFC <- reservedOpFC "**"

449− reservedOp "**"

450− return fc

451 r <- expr syn

452− lchar ')'

452+ closeParenFC <- lcharFC ')'

453− return (PDPair fc TypeOrTerm e Placeholder r)

453+ return (PDPair starsFC [openParenFC, starsFC, closeParenFC] TypeOrTerm e Placeholder r)

454 <?> "end of bracketed expression"

455 where mergePairs :: [(PTerm, FC)] -> PTerm

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

458

459-- bit of a hack here. If the integer doesn't fit in an Int, treat it as a

460-- big integer, otherwise try fromInteger and the constants as alternatives.

@@ -882,7 +882,7 @@ let_ syn = try (do kw <- reservedFC "let"

882 return (buildLets ls sc))

883 <?> "let binding"

884 where buildLets [] sc = sc

885− buildLets ((fc, PRef nfc [] n, ty, v, []) : ls) sc

885+ buildLets ((fc, PRef nfc _ n, ty, v, []) : ls) sc

886 = PLet fc n nfc ty v (buildLets ls sc)

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

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

src/Idris/ParseHelpers.hs+6

@@ -260,6 +260,12 @@ string = Chr.string

260lchar :: MonadicParsing m => Char -> m Char

261lchar = token . char

262

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+

263-- | Parses string as a token

269-- | Parses string as a token

264symbol :: MonadicParsing m => String -> m String

270symbol :: MonadicParsing m => String -> m String

265symbol = Tok.symbol

271symbol = Tok.symbol