3cd25e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add extra HL information to PRef

3cd25e6David Raymond Christiansen11 years ago

src/Idris/AbsSyntax.hs+73−73

compare with master

unifiedsplit

@@ -998,10 +998,10 @@ 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' n) t r)

1001+ en (PDPair f 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' n') (en t) (en (shadow n n' r))

1004+ PDPair f 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)

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

1017

1018 en (PQuote (Var n))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1033− en (PRef fc n)

1033+ en (PRef fc hl n)

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

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

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

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

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

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

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

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

1038− en (PInferRef fc n)

1038+ en (PInferRef fc hl n)

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

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

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

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

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

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

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

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

1103

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

1105

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

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

1107 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

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

1162getPriority :: IState -> PTerm -> Int

1163getPriority i tm = 1 -- pri tm

1164 where

1165− pri (PRef _ n) =

1165+ pri (PRef _ _ n) =

1166 case lookupP n (tt_ctxt i) of

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

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

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

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

1289 | otherwise = doAdd cs ns t

1290

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

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

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

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

1293

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

1295 = getcapp c ++ getConstraints sc

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

1297 getConstraints _ = []

1298

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

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

1300 = do ns <- mapM getName args

1301 return (UConstraint c ns)

1302 getcapp _ = []

1303

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

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

1305 getName _ = []

1306

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

1458 imps True (n:env) sc

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

1460 = 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]

1462 _ -> [])

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

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

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

1466 imps True (n:env) sc

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

1468 = 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]

1470 _ -> [])

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

1472 put (PConstraint 10 l n Placeholder : decls,

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

1474 imps True (n:env) sc

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

1476 = 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]

1478 _ -> [])

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

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

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

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

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

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

1546 where

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

1548− ai qq env ds (PRef fc f)

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

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

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

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

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

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

1554 = let l' = ai qq env ds l

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

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

1573 PAlternative a as'

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

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

1577− PApp fc (PInferRef ffc f) as'

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

1578− ai qq env ds (PApp fc ftm@(PRef ffc 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 f) as)

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

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

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

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

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

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

1609 PLam fc n nfc ty' sc'

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

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

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

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

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

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

1614 = case lookupDef n (tt_ctxt ist) of

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

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− _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

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

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

1621 = let ty' = ai qq env ds ty

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

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

1674 vname _ = False

1675

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

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

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

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

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

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

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

1683 [] -> nh

1684 x -> x

1685 case ns' of

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

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

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

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

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

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

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

1690 alts -> Right $

1691 PAlternative (ExactlyOne True) $

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

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

1693 (insertImpl ns as)) alts

1694 where

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

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

1737 case find n imps [] of

1738 Just (tm, imps') ->

1739 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

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

1741 PImp p True l n ph :

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

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

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

1780stripLinear :: IState -> PTerm -> PTerm

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

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

1783− sl (PRef fc f)

1783+ sl (PRef fc hl f)

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

1785− = return $ PRef fc f

1785+ = return $ PRef fc hl f

1786 | otherwise = do ns <- get

1787 if (f `elem` ns)

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

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

1789 else do put (f : ns)

1790− return (PRef fc f)

1790+ return (PRef fc hl f)

1791 sl (PPatvar fc f)

1792 = do ns <- get

1793 if (f `elem` ns)

@@ -1810,7 +1810,7 @@ stripLinear i tm = evalState (sl tm) [] where

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

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

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

1813− PRef _ _ -> return fn

1813+ PRef _ _ _ -> return fn

1814 t -> sl t

1815 args' <- mapM slA args

1816 return $ PApp fc fn' args'

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

1832stripUnmatchable :: IState -> PTerm -> PTerm

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

1834 su :: PTerm -> PTerm

1835− su tm@(PRef fc f)

1835+ su tm@(PRef fc hl f)

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

1837 = Placeholder

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

1839 = PHidden tm

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

1841 = PHidden tm

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

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

1843 -- here we use canBeDConName because the impossible pattern

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

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

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

1930 fullApp x = x

1931

1932 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'

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

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

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

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

1939− match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = 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')

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

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

1942 | length args == length args'

1943 = do mf <- match' f f'

1944 ms <- zipWithM matchArg args args'

1945 return (mf ++ concat ms)

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

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

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

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

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

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

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

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

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

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

1951 | n == n' && not names &&

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

1953 || tm == Placeholder)

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

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

1957 where dropNS (NS n _) = n

1958 dropNS n = n

1959− match (PRef _ n) tm

1959+ match (PRef _ _ n) tm

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

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

1962 = return [(n, tm)]

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

1986 _ -> LeftErr (a, b)

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

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

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

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

1990 match (PQuote _) _ = return []

1991 match (PProof _) _ = return []

1992 match (PTactics _) _ = return []

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

2044

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

2046substMatchShadow n shs tm t = sm shs t where

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

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

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

2049 sm xs (PPi p x fc t sc)

2050 | x `elem` xs

2051 = let x' = nextName x in

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

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

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

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

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

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

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

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

2072

2073shadow :: Name -> Name -> PTerm -> PTerm

2074shadow 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'

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

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

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

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

2170 mkUniq (PPair fc p l r)

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

2172 return $! PPair fc p l' r'

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

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

2174 | t /= Placeholder

2175 = do env <- get

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

@@ -2180,7 +2180,7 @@ 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' n') t' sc''

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

2184 mkUniq (PDPair fc p l t r)

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

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

src/Idris/AbsSyntaxTree.hs+45−45

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

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

814updateNs [] t = t

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

817 updateRef t = t

818

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

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

831

832-- | High level language terms

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

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

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 Name -- ^ A name to be defined later

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

836 | PPatvar FC Name -- ^ A pattern variable

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

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

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

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

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

886mapPTermFC f g (PQuote q) = PQuote q

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

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

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

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

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

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

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

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

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

1105highestFC :: PTerm -> Maybe FC

1106highestFC (PQuote _) = Nothing

1107−highestFC (PRef fc _) = Just fc

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

1108−highestFC (PInferRef fc _) = Just fc

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

1109highestFC (PPatvar fc _) = Just fc

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

1111highestFC (PPi _ _ _ _ _) = Nothing

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

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

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

1294

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

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

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

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

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

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

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

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

1299 Nothing

1300 Nothing

1301 Nothing

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

1350inferDecl = PDatadecl inferTy NoFC

1351 (PType bi)

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

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

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

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

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

1355inferOpts = []

1356

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

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

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

1359

1360getInferTerm, getInferType :: Term -> Term

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

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

1406

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

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

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

1409 (PType bi)))

1410 [(reflDoc, reflParamDoc,

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

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

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

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

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

1414 pimp (n "B") Placeholder False,

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

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

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

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

1417 where n a = sUN a

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

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

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

1534 prettySe d p bnd e

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

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

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

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

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

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

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

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

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

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

1583 -- operators in general is improved.

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

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

1585 | n == eqTy, ppopt_impl ppo =

1586 depth d . bracket p eqPrec $

1587 enclose lparen rparen eq <+>

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

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

1594 eqPrec = startPrec

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

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

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

1597 | UN nm <- basename f

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

1599 prettyName True (ppopt_impl ppo) bnd f

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

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

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

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

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

1603 | UN nm <- basename op

1604 , not (tnull nm) &&

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

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

1626 inFix l r = align . group $

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

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

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

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

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

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

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

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

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

1634 let args = getShowArgs as

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

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

1697 IsTerm -> annName sigmaCon

1698 TypeOrTerm -> id

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

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

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

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

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

1702 prettySe d p bnd (PAlternative a as) =

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

1704 where

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

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

1782 slist' d _ _ e

1783 | containsHole e = Nothing

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

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

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

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

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

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

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

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

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

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

1791 all isImp imps,

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

1817

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

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

1820− snat d p (PRef _ z)

1820+ snat d p (PRef _ _ z)

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

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

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

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

1857

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

1859containsHole :: PTerm -> Bool

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

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

1861

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

1863prettyName

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

1994

1995instance Sized PTerm where

1996 size (PQuote rawTerm) = size rawTerm

1997− size (PRef fc name) = size name

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

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

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

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

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

2035allNamesIn :: PTerm -> [Name]

2036allNamesIn tm = nub $ ni [] tm

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

2038− ni env (PRef _ n)

2038+ ni env (PRef _ _ n)

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

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

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

@@ -2049,8 +2049,8 @@ allNamesIn tm = nub $ ni [] 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

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

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

2056 ni env (PUnifyLog tm) = ni env tm

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

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

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

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

2082 ni set (PHidden tm) = ni set tm

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

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

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

2097 where

2098− ni env (PRef _ n)

2098+ ni env (PRef _ _ n)

2099 | not (n `elem` env)

2100 = case lookupTy n (tt_ctxt ist) of

2101 [] -> [n]

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

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

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

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

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

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

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

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

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

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

2121 ni env (PHidden tm) = ni env tm

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

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

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

2130 where

2131− ni env (PRef _ n)

2131+ ni env (PRef _ _ n)

2132 | not (n `elem` env)

2133 = case lookupTy n (tt_ctxt ist) of

2134 [] -> [n]

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

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

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

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

2151 ni env (PHidden tm) = ni env tm

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

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

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

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

2165− ni env (PRef _ n)

2165+ ni env (PRef _ _ n)

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

2167 = case lookupDefExact n (tt_ctxt ist) of

2168 Nothing -> [n]

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

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

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

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

2182 ni env (PHidden tm) = ni env tm

src/Idris/CaseSplit.hs+24−24

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

127

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

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

131 dens t = t

132

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

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

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

138 ps' = mergeAllPats ist cv t ps in

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

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

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

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

142 patvars (PPatvar _ n) = [n]

143 patvars _ = []

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

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

147-- user provided name (first pattern)

148mergePat ist (PPatvar fc n) new t

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

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

150mergePat ist old (PPatvar fc n) t

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

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

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

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

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

154 return new

155 | otherwise

156 = do ms <- get

157 case lookup n' (namemap ms) of

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

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

159− return (PRef fc x)

159+ return (PRef fc [] x)

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

161− return (PRef fc n)

161+ return (PRef fc [] n)

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

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

164 return (PApp fc f newArgs)

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

169 return (y { machine_inf = machine_inf x,

170 getTm = tm' })

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

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

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

173− addUpdate n tm

173+ addUpdate n tm

174− return tm

174+ return tm

175mergePat ist x y t = return y

176

177mergeUserImpl :: PTerm -> PTerm -> PTerm

178mergeUserImpl x y = x

179

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

181−argTys ist (PRef fc n)

181+argTys ist (PRef fc hls n)

182 = case lookupTy n (tt_ctxt ist) of

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

184 _ -> repeat Nothing

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

188argTys _ _ = repeat Nothing

189

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

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

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

192 = do ms <- get

193 case lookup n (namemap ms) of

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

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

195 Nothing -> case n of

196 (UN _) -> return orig

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

198− return (PRef fc n')

198+ return (PRef fc [] n')

199tidy ist (PApp fc f args) ty

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

201 return (PApp fc f args')

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

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

223 _ -> [Placeholder]

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

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

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

226 (map toPlaceholder args)

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

228 toPlaceholder tm = tm { getTm = Placeholder }

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

233 where subst :: PTerm -> PTerm

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

235 | otherwise = Placeholder

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

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

237− | isDConName v ctxt = orig

237+ | isDConName v ctxt = orig

238− subst (PRef _ _) = Placeholder

238+ subst (PRef _ _ _) = Placeholder

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

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

240 | isTConName t ctxt = Placeholder -- infer types

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

242 subst x = x

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

281

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

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

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

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

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

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

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

287 nshow t = show t

288

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

359 getNameFrom i used (PPi _ _ _ _ _)

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

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

363 = case getNameHints i f of

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

365 ns -> uniqueNameFrom (mkSupply ns) used

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

415 newPats

416 return (map fst newPats')

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

419 base t = t

420

421 nm ptm = do mptm <- elabNewPat ptm

src/Idris/Coverage.hs+13−13

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

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

29 evalStateT (toTT (mapPT deNS timp)) 0

30 where

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

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

32− case lookupNameDef n (tt_ctxt i) of

32+ case lookupNameDef n (tt_ctxt i) of

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

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

34− _ -> return $ P Ref n Erased

34+ _ -> return $ P Ref n Erased

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

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

37 return $ mkApp t' args'

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

42 put (v + 1)

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

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

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

46 deNS t = t

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

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

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

113 mkClauses parg args

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

116 return tm

117 where

118 mkArg :: [[PTerm]] -> [[PTerm]]

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

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

215

216 otherPats :: PTerm -> [PTerm]

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

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

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

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

219 otherPats o@(PPair fc _ l r)

220 = ops fc pairCon

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

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

232 ops fc n xs o

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

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

236 let tyn = getTy n (tt_ctxt i)

237 case lookupCtxt tyn (idris_datatypes i) of

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

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

243 getExpTm t = getTm t

244

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

247 | ei == txt "Ex_intro"

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

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

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

250 | n == pairCon

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

252 resugar t = t

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

265

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

267 (pargs : _)

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

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

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

270

271 fnub :: [PTerm] -> [PTerm]

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

279 -- quick check for constructor equality

280 quickEq :: PTerm -> PTerm -> Bool

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

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

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

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

284 | length as == length as'

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

src/Idris/DSL.hs+14−14

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

18dslify :: SyntaxInfo -> IState -> PTerm -> PTerm

19dslify syn i = transform dslifyApp

20 where

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

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

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

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

24 dslifyApp t = t

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

30mkTTName :: FC -> Name -> PTerm

31mkTTName fc n =

32− let mkList fc [] = PRef fc (sNS (sUN "Nil") ["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"]))

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

34 [ pexp (stringC x)

35 , pexp (mkList fc xs)]

36 stringC = PConstant fc . Str . str

37 intC = PConstant fc . I

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

39 in case n of

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

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)

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

42− , pexp (mkList fc ns)]

42+ , pexp (mkList fc ns)]

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

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

44− , pexp (stringC nm)]

44+ , pexp (stringC nm)]

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

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

47expandSugar :: DSL -> PTerm -> PTerm

48expandSugar dsl (PLam fc n nfc ty tm)

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

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

73 (map (pmap (expandSugar dsl)) opts)

74expandSugar dsl (PIfThenElse fc c t f) =

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

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

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

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

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

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

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

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

101 = 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"))

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

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

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

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

118-- | Replace DSL-bound variable in a term

119var :: DSL -> Name -> PTerm -> Int -> PTerm

120var 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 =

122 case dsl_var dsl of

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

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

@@ -153,7 +153,7 @@ var dsl n t i = v' i t where

153 Nothing -> PElabError (Msg "No index_next defined")

154 Just f -> PApp fc f [pexp (mkVar fc (n-1))]

155

156− setFC fc (PRef _ n) = PRef fc n

156+ setFC fc (PRef _ _ n) = PRef fc [] n

157 setFC fc (PApp _ f xs) = PApp fc (setFC fc f) (map (fmap (setFC fc)) xs)

158 setFC fc t = t

159

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

182 (bs, n) <- get

183 let nm = sUN ("_bindApp" ++ show n)

184 put ((nm, fc, PApp fc t args') : bs, n+1)

185− return (PRef fc nm)

185+ return (PRef fc [] nm)

186 db' (PApp fc t args)

187 = do t' <- db' t

188 args' <- mapM dbArg args

src/Idris/DeepSeq.hs+2−2

@@ -223,8 +223,8 @@ instance (NFData t) => NFData (PData' t) where

223

224instance NFData PTerm where

225 rnf (PQuote x1) = rnf x1 `seq` ()

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

227+ rnf (PInferRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

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

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

230 rnf (PPi x1 x2 x3 x4 x5)

src/Idris/Delaborate.hs+12−12

@@ -30,11 +30,11 @@ bugaddr = "https://github.com/idris-lang/Idris-dev/issues"

30resugar :: IState -> PTerm -> PTerm

31resugar ist = transform flattenDoLet . transform resugarApp

32 where

33− resugarApp (PApp fc (PRef _ n) args)

33+ resugarApp (PApp fc (PRef _ _ n) args)

34 | [c, t, f] <- mapMaybe explicitTerm args

35 , basename n == sUN "ifThenElse"

36 = PIfThenElse fc c (dedelay t) (dedelay f)

37− resugarApp (PApp fc (PRef _ n) args)

37+ resugarApp (PApp fc (PRef _ _ n) args)

38 | [v, PLam _ bn _ _ next] <- mapMaybe explicitTerm args

39 , basename n == sUN ">>="

40 = let step = if bn `elem` namesIn [] ist next

@@ -43,7 +43,7 @@ resugar ist = transform flattenDoLet . transform resugarApp

43 in case resugarApp next of

44 PDoBlock dos -> PDoBlock (step : dos)

45 expr -> PDoBlock [step, DoExp NoFC expr]

46− resugarApp (PApp fc (PRef _ n) args)

46+ resugarApp (PApp fc (PRef _ _ n) args)

47 | [PConstant fc (BI i)] <- mapMaybe explicitTerm args

48 , basename n == sUN "fromInteger"

49 = PConstant fc (BI i)

@@ -59,7 +59,7 @@ resugar ist = transform flattenDoLet . transform resugarApp

59 fixExp d = [d]

60 flattenDoLet tm = tm

62− dedelay (PApp _ (PRef _ delay) [_, _, obj])

62+ dedelay (PApp _ (PRef _ _ delay) [_, _, obj])

63 | delay == sUN "Delay" = getTm obj

64 dedelay x = x

@@ -99,15 +99,15 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

99 un = fileFC "(val)"

100

101 de env _ (App _ f a) = deFn env f [a]

102− de env _ (V i) | i < length env = PRef un (snd (env!!i))

102+ de env _ (V i) | i < length env = PRef un [] (snd (env!!i))

103− | otherwise = PRef un (sUN ("v" ++ show i ++ ""))

103+ | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))

104 de env _ (P _ n _) | n == unitTy = PTrue un IsType

105 | n == unitCon = PTrue un IsTerm

106− | Just n' <- lookup n env = PRef un n'

106+ | Just n' <- lookup n env = PRef un [] n'

107 | otherwise

108 = case lookup n (idris_metavars ist) of

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

110− _ -> PRef un n

110+ _ -> PRef un [] n

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

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

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

@@ -158,7 +158,7 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

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)

@@ -181,8 +181,8 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

181 = PApp un (PMetavar NoFC n) (map pexp args)

182 mkPApp n args

183 | Just imps <- lookupCtxtExact n (idris_implicits ist)

184− = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

184+ = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

185− | otherwise = PApp un (PRef un n) (map pexp args)

185+ | otherwise = PApp un (PRef un [] n) (map pexp args)

186

187 imp (PImp p m l n _) arg = PImp p m l n arg

188 imp (PExp p l n _) arg = PExp p l n arg

@@ -565,7 +565,7 @@ addImplicitDiffs x y

565 addI x y = (x, y)

566

567 -- Just the ones which appear desugared in errors

568− expLike (PRef _ n) (PRef _ n') = n == n'

568+ expLike (PRef _ _ n) (PRef _ _ n') = n == n'

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

570 = expLike f f' && length as == length as' &&

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

src/Idris/Docs.hs+5−5

@@ -197,12 +197,12 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

197 updateArgs ps (a:as) = a : updateArgs ps as

198 updateArgs _ _ = []

199

200− updateRef nm (PRef fc _) = PRef fc nm

200+ updateRef nm (PRef fc _ _) = PRef fc [] nm

201 updateRef _ pt = pt

202

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

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

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

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

205− isSubclass _ = False

205+ isSubclass _ = False

206

207 prettyParameters =

208 if any (isJust . snd) params

@@ -289,7 +289,7 @@ docClass n ci

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

290 getDInst _ = Nothing

291

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

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

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

294 isSubclass (PPi _ _ _ _ pt)

295 = isSubclass pt

src/Idris/Elab/AsPat.hs+1−1

@@ -44,5 +44,5 @@ replaceUnderscore tm = evalState (transformM (underAs replaceUnderscore') tm) 0

46 replaceUnderscore' :: PTerm -> State Int PTerm

47− replaceUnderscore' Placeholder = PRef emptyFC <$> fresh

47+ replaceUnderscore' Placeholder = PRef emptyFC [] <$> fresh

48 replaceUnderscore' tm = return tm

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

@@ -65,8 +65,8 @@ elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

65elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

66 = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

67 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

68− let constraint = PApp fc (PRef fc tn)

68+ let constraint = PApp fc (PRef fc [] tn)

69− (map (pexp . PRef fc) (map (\(n, _, _) -> n) ps))

69+ (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

71 let syn =

72 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

142 = do when (not $ null cs) . tclift

143 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

144 i <- getIState

145− let t = PApp fc (PRef fc n) (map pexp ps)

145+ let t = PApp fc (PRef fc [] n) (map pexp ps)

146 let isConstrained = any (== t) (map snd constraints)

147 when (not isConstrained) . tclift

148 $ 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

195 = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

196 -- SN (ParentN cn (show con))

197 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

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

198+ let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

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

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

200 let rhs = PResolveTC (fileFC "HACK")

201 let ty = PPi constraint cnm NoFC c con

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

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

204 i <- getIState

205 let conn = case con of

206− PRef _ n -> n

206+ PRef _ _ n -> n

207− PApp _ (PRef _ n) _ -> n

207+ PApp _ (PRef _ _ n) _ -> n

208 let conn' = case lookupCtxtName conn (idris_classes i) of

209 [(n, _)] -> n

210 _ -> conn

@@ -225,10 +225,10 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

225 tfun cn c syn all (m, (mfc, doc, o, ty))

226 = do let ty' = expandMethNS syn (insertConstraint c all ty)

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

229 let margs = getMArgs ty

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

232 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

233 logLvl 2 ("Top level type: " ++ showTmImpls ty')

234 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

242 getMArgs _ = []

243

244 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

246 | otherwise = getMeth ms as x

247

248 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

250 lhsArgs (CA : xs) ns = lhsArgs xs ns

251 lhsArgs [] _ = []

252

253 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

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

256 rhsArgs [] _ = []

257

@@ -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 [] n)

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

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

274 | otherwise = m

275 addC _ _ tm = tm

276

@@ -303,7 +303,7 @@ expandMethNS :: SyntaxInfo

303 -> PTerm -> PTerm

304expandMethNS syn = mapPT expand

305 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

307 expand t = t

308

309-- | Find the determining parameter locations

src/Idris/Elab/Clause.hs+17−17

@@ -482,20 +482,20 @@ checkPossible info fc tcgen fname lhs_in

482

483

484propagateParams :: IState -> [Name] -> Type -> PTerm -> PTerm

485−propagateParams i ps t tm@(PApp _ (PRef fc n) args)

485+propagateParams i ps t tm@(PApp _ (PRef fc hls n) args)

486− = PApp fc (PRef fc n) (addP t args)

486+ = PApp fc (PRef fc hls n) (addP t args)

487 where addP (Bind n _ sc) (t : ts)

488 | Placeholder <- getTm t,

489 n `elem` ps,

490 not (n `elem` allNamesIn tm)

491− = t { getTm = PRef NoFC n } : addP sc ts

491+ = t { getTm = PRef NoFC [] n } : addP sc ts

492 addP (Bind n _ sc) (t : ts) = t : addP sc ts

493 addP _ ts = ts

494−propagateParams i ps t (PRef fc n)

494+propagateParams i ps t (PRef fc hls n)

495 = case lookupCtxt n (idris_implicits i) of

496 [is] -> let ps' = filter (isImplicit is) ps in

497− PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps')

497+ PApp fc (PRef fc hls n) (map (\x -> pimp x (PRef fc [] x) True) ps')

498− _ -> PRef fc n

498+ _ -> PRef fc hls n

499 where isImplicit [] n = False

500 isImplicit (PImp _ _ _ x _ : is) n | x == n = True

501 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

734 borrowedB b = borrowedNames env (binderTy b)

735 borrowedNames _ _ = []

736

737− mkLHSapp t@(PRef _ _) = PApp fc t []

737+ mkLHSapp t@(PRef _ _ _) = PApp fc t []

738 mkLHSapp t = t

739

740 decorate (NS x ns)

@@ -772,7 +772,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

772 where

773 isArg' (PClause _ _ (PApp _ _ args) _ _ _)

774 = any (\x -> case x of

775− PRef _ n' -> n == n'

775+ PRef _ _ n' -> n == n'

776 _ -> False) (map getTm args)

777 isArg' _ = False

778 isArg _ _ = False

@@ -905,13 +905,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

905 mapM_ (rec_elabDecl info EAll info) wb

906

907 -- rhs becomes: fname' ps_pre wval ps_post Refl

908− let rhs = PApp fc (PRef fc wname)

908+ let rhs = PApp fc (PRef fc [] wname)

909− (map (pexp . (PRef fc) . fst) bargs_pre ++

909+ (map (pexp . (PRef fc []) . fst) bargs_pre ++

910 pexp wval :

911− (map (pexp . (PRef fc) . fst) bargs_post) ++

911+ (map (pexp . (PRef fc []) . fst) bargs_post) ++

912 case mpn of

913 Nothing -> []

914− Just _ -> [pexp (PApp NoFC (PRef NoFC eqCon)

914+ Just _ -> [pexp (PApp NoFC (PRef NoFC [] eqCon)

915 [ pimp (sUN "A") Placeholder False

916 , pimp (sUN "x") Placeholder False

917 ])])

@@ -974,21 +974,21 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

974 = ifail $ show fc ++ ":badly formed with clause"

975

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

978

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

980 = let ns = map (keepMvar (map fst mvars) fc') ns_in

981 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

982 return $ substMatches mvars $

983− PApp fc (PRef fc' wname)

983+ PApp fc (PRef fc' [] wname)

984 (map pexp ns ++ pexp w : (map pexp ns') ++

985 case pn of

986 Nothing -> []

987− Just pnm -> [pexp (PRef fc pnm)])

987+ Just pnm -> [pexp (PRef fc [] pnm)])

988 updateLHS n pn wname mvars ns_in ns_in' tm w

989 = updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w

990

991− keepMvar mvs fc v | v `elem` mvs = PRef fc v

991+ keepMvar mvs fc v | v `elem` mvs = PRef fc [] v

992 | otherwise = Placeholder

993

994 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

259

260 mkLazy (PPi pl n nfc ty sc)

261 = let ty' = if getTyName ty

262− then PApp fc (PRef fc (sUN "Lazy'"))

262+ then PApp fc (PRef fc [] (sUN "Lazy'"))

263− [pexp (PRef fc (sUN "LazyCodata")),

263+ [pexp (PRef fc [] (sUN "LazyCodata")),

264 pexp ty]

265 else ty in

266 PPi pl n nfc ty' (mkLazy sc)

267 mkLazy t = t

268

269− getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

269+ getTyName (PApp _ (PRef _ _ n) _) = n == nsroot tn

270− getTyName (PRef _ n) = n == nsroot tn

270+ getTyName (PRef _ _ n) = n == nsroot tn

271 getTyName _ = False

272

273

@@ -326,11 +326,11 @@ elabCaseFun ind paramPos n ty cons info = do

326 scrutineeIdxs <- namePis False idxs

327 let motiveConstr = [(motiveName, expl, motive)]

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

330 let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName NoFC eliminatorTy

331 let clauseConsElimArgs = map getPiName consTerms

332 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'

334 let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

335 elimLog elimSig

336 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

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

381 mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg

382 return (oldName, (name, pl, piarg))

383 where keyOf :: PTerm -> String

384− keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

384+ keyOf (PRef _ _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

385 keyOf (PApp _ tyf _) = keyOf tyf

386 keyOf (PType _) = "ty__"

387 keyOf _ = "carg__"

@@ -446,10 +446,10 @@ elabCaseFun ind paramPos n ty cons info = do

446 case findIndex (== n) oldParams of

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

448 Just i -> (removeParamPis oldParams params tyr)

449− removeParamPis oldParams params (PRef _ n) =

449+ removeParamPis oldParams params (PRef _ _ n) =

450 case findIndex (== n) oldParams of

451− Nothing -> (PRef elimFC n)

451+ Nothing -> (PRef elimFC [] n)

452− Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))

452+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC [] (newname))

453 removeParamPis oldParams params (PApp _ cns args) =

454 PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args

455 where replaceParamArgs :: [PArg] -> [PArg]

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

460 [n] ->

461 case findIndex (== n) oldParams of

462 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

464 removeParamPis oldParams params t = t

465

466 paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]

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

468 paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args

469

470 extractName :: PTerm -> [Name]

471− extractName (PRef _ n) = [n]

471+ extractName (PRef _ _ n) = [n]

472− extractName _ = []

472+ extractName _ = []

473

474 splitArgPms :: PTerm -> ([PTerm], [PTerm])

475 splitArgPms (PApp _ f args) = splitArgPms' args

@@ -505,23 +505,23 @@ elabCaseFun ind paramPos n ty cons info = do

505 let (_, consIdxs) = splitArgPms resTy

506 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

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

509 where (_, idxs) = splitArgPms ty

510

511 findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]

512 findRecArgs [] = []

513− findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty: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

514+ findRecArgs (ty@(_,_,PApp _ (PRef _ _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

515− findRecArgs (ty:rs) = findRecArgs rs

515+ findRecArgs (ty:rs) = findRecArgs rs

516

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

519

520 convertArg :: (Name, Plicity, PTerm) -> PArg

521− convertArg (n, _, _) = pexp (PRef elimFC n)

521+ convertArg (n, _, _) = pexp (PRef elimFC [] n)

522

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

525

526 getPiName :: (Name, Plicity, PTerm) -> Name

527 getPiName (name,_,_) = name

@@ -539,11 +539,11 @@ elabCaseFun ind paramPos n ty cons info = do

539 let (_, generalIdxs') = splitArgPms resTy

540 let generalIdxs = map pexp generalIdxs'

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

543 let recArgs = findRecArgs consArgs

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

546 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

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

549 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

68 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"

69 cs -> tclift $ tfail $ At fc

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

72 let iname = mkiname n (namespace info) ps expn

73 let emptyclass = null (class_methods ci)

74 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

89 -- where block

90 wparams <- mapM (\p -> case p of

91 PApp _ _ args -> getWParams (map getTm args)

92− a@(PRef fc f) -> getWParams [a]

92+ a@(PRef fc _ f) -> getWParams [a]

93 _ -> return []) ps

94 ist <- getIState

95 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

100 let all_meths = map (nsroot . fst) (class_methods ci)

101 let mtys = map (\ (n, (op, t)) ->

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

104 all_meths

105 t' = substMatchesShadow mnamemap pnames t_in in

106 (decorate ns iname n,

@@ -123,15 +123,15 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

123

124 -- Bring variables in instance head into scope

125 let headVars = nub $ mapMaybe (\p -> case p of

126− PRef _ n ->

126+ PRef _ _ n ->

127 case lookupTy n (tt_ctxt ist) of

128 [] -> Just n

129 _ -> Nothing

130 _ -> Nothing) ps

131-- let lhs = PRef fc iname

132− let lhs = PApp fc (PRef fc iname)

132+ let lhs = PApp fc (PRef fc [] iname)

133− (map (\n -> pimp n (PRef fc n) True) headVars)

133+ (map (\n -> pimp n (PRef fc [] n) True) headVars)

134− let rhs = PApp fc (PRef fc (instanceCtorName ci))

134+ let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

135 (map (pexp . mkMethApp) mtys)

136

137 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

218 keepDets dets t = t

219

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

222 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

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

224 lamBind i (PPi _ n _ ty sc) sc'

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

226 lamBind i _ sc = sc

227 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

229 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

231 methArgs i (PPi (Constraint _ _) n _ ty sc)

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

233 methArgs i _ = []

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

237

238 getWParams [] = return []

239 getWParams (p : ps)

240− | PRef _ n <- p

240+ | PRef _ _ n <- p

241 = do ps' <- getWParams ps

242 ctxt <- getContext

243 case lookupP n ctxt of

244− [] -> return (pimp n (PRef fc n) True : ps')

244+ [] -> return (pimp n (PRef fc [] n) True : ps')

245 _ -> return ps'

246 getWParams (_ : ps) = getWParams ps

247

src/Idris/Elab/Provider.hs+1−1

@@ -94,7 +94,7 @@ elabProvider doc info syn fc nfc what n

94 | ProvTerm ty _ <- what ->

95 do -- Finally add a top-level definition of the provided term

96 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) []]

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

100 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

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

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

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

101 paramsAndDoc = pad params paramDocs

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

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

328 generateLhs :: PTerm

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

331 where

332 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

334 lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)

335 lhsArgs _ [] = []

336

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

343

344 -- | The right hand side of the projection function.

345 generateRhs :: PTerm

346− generateRhs = PRef fc pname_in

346+ generateRhs = PRef fc [] pname_in

347

348-- | Creates and elaborates an update function.

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

387 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

388 PPi expl (nsroot pname) NoFC pty $

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

391

392 -- | The "_set" name.

393 set_pname :: Name

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

401

402 -- | The left-hand side of the update function.

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

405 where

406 constructorPattern :: PTerm

407− constructorPattern = PApp fc (PRef fc cn) args

407+ constructorPattern = PApp fc (PRef fc [] cn) args

408

409 -- | The "_in" name.

410 pname_in :: Name

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

415

416 -- | The right-hand side of the update function.

417 generateRhs :: PTerm

418− generateRhs = PApp fc (PRef fc cn) (newArgs i args)

418+ generateRhs = PApp fc (PRef fc [] cn) (newArgs i args)

419 where

420 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

422 newArgs i (x : rest) = x : (newArgs (i-1) rest)

423 newArgs _ [] = []

424

@@ -440,17 +440,17 @@ asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t

440recName :: Name

441recName = sMN 0 "rec"

442

443−recRef = PRef emptyFC recName

443+recRef = PRef emptyFC [] recName

444

445projectInType :: [(Name, Name)] -> PTerm -> PTerm

446projectInType xs = mapPT st

447 where

448 st :: PTerm -> PTerm

449− st (PRef fc n)

449+ st (PRef fc [] n)

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

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

451 st t = t

452

453-- | Creates an PArg from a plicity and a name where the term is a PRef.

454asPRefArg :: 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)

456

src/Idris/Elab/Term.hs+58−55

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

289 env <- get_env

290 handleError (forceErr t' env)

291 (elab' ina fc' t')

292− (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

292+ (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

293 [pimp (sUN "t") Placeholder True,

294 pimp (sUN "a") Placeholder True,

295 pexp ct]))

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

308 forceErr orig env (At _ t) = forceErr orig env t

309 forceErr orig env t = False

310

311− notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

311+ notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

312 notDelay _ = True

313

314 local f = do e <- get_env

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

350 do hnf_compute

351 g <- goal

352 case g of

353− TType _ -> elab' ina (Just fc) (PRef fc unitTy)

353+ TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

354− UType _ -> elab' ina (Just fc) (PRef fc unitTy)

354+ UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

355− _ -> elab' ina (Just fc) (PRef fc unitCon)

355+ _ -> elab' ina (Just fc) (PRef fc [] unitCon)

356 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

357 = do g <- goal; resolveTC False False 5 g fn ist

358 elab' ina fc (PResolveTC fc')

@@ -360,14 +360,14 @@ elab ist info emode opts fn tm

360 instanceArg c

361 -- Elaborate the equality type first homogeneously, then

362 -- heterogeneously as a fallback

363− elab' ina _ (PApp fc (PRef _ n) args)

363+ elab' ina _ (PApp fc (PRef _ _ n) args)

364 | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

365 = try (do tyn <- getNameFrom (sMN 0 "aqty")

366 claim tyn RType

367 movelast tyn

368− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

368+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

369− [pimp (sUN "A") (PRef NoFC tyn) True,

369+ [pimp (sUN "A") (PRef NoFC [] tyn) True,

370− pimp (sUN "B") (PRef NoFC tyn) False,

370+ pimp (sUN "B") (PRef NoFC [] tyn) False,

371 pexp l, pexp r]))

372 (do atyn <- getNameFrom (sMN 0 "aqty")

373 btyn <- getNameFrom (sMN 0 "bqty")

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

375 movelast atyn

376 claim btyn RType

377 movelast btyn

378− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

378+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

379− [pimp (sUN "A") (PRef NoFC atyn) True,

379+ [pimp (sUN "A") (PRef NoFC [] atyn) True,

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

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

381 pexp l, pexp r]))

382

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

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

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 [] 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 [] 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 [] 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 [] 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 n) t r)

412+ elab' ina _ (PDPair fc p l@(PRef nfc hl n) t r)

413 = case t of

414 Placeholder ->

415 do hnf_compute

@@ -418,14 +418,14 @@ 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 [] 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 [] 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 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])

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

449 [x] -> elab' ina fc x

450 _ -> tryAll (zip (map (elab' ina fc) as'')

451 (map showHd as'')))

452− where showHd (PApp _ (PRef _ n) _) = n

452+ where showHd (PApp _ (PRef _ _ n) _) = n

453− showHd (PRef _ n) = n

453+ showHd (PRef _ _ n) = n

454 showHd (PApp _ h _) = showHd h

455 showHd x = NErased -- We probably should do something better than this here

456

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

486-- elab' (_, _, inty) (PRef fc f)

487-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

488-- = lift $ tfail (Msg "Typecase is not allowed")

489− elab' ec _ tm@(PRef fc n)

489+ elab' ec _ tm@(PRef fc hl n)

490 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

491 && isTConName n (tt_ctxt ist)

492 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

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

526 bindable (NS _ _) = False

527 bindable (UN xs) = True

528 bindable n = implicitable n

529− elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp NoFC f [])

529+ elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

530− elab' ina fc' tm@(PRef fc n)

530+ elab' ina fc' tm@(PRef fc hls n)

531 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

532 && isTConName n (tt_ctxt ist)

533 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -541,9 +541,10 @@ elab ist info emode opts fn tm

541 if null a'

542 then erun fc $

543 do apply (Var n) []

544− hl <- findHighlight n

544+ hilite <- findHighlight n

545 solve

546− highlightSource fc hl

546+ mapM_ (uncurry highlightSource) $

547+ (fc, hilite) : map (\f -> (f, hilite)) hls

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

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

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

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

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

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

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

646 solve

647 solve

647-- elab' ina fc (PLet n Placeholder

648-- elab' ina fc (PLet n Placeholder

648-- (PApp fc r [pexp (delab ist rty)]) sc)

649-- (PApp fc r [pexp (delab ist rty)]) sc)

649− elab' ina _ tm@(PApp fc (PInferRef _ f) args) = do

650+ elab' ina _ tm@(PApp fc (PInferRef _ _ f) args) = do

650 rty <- goal

651 rty <- goal

651 ds <- get_deferred

652 ds <- get_deferred

652 ctxt <- get_context

653 ctxt <- get_context

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

677 fnTy [] ret = forget ret

678 fnTy [] ret = forget ret

678 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

679 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

679

680

680− localVar env (PRef _ x)

681+ localVar env (PRef _ _ x)

681 = case lookup x env of

682 = case lookup x env of

682 Just _ -> Just x

683 Just _ -> Just x

683 _ -> Nothing

684 _ -> Nothing

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

701 solve

702 solve

702 -- if f is local, just do a simple_app

703 -- if f is local, just do a simple_app

703 -- FIXME: Anyone feel like refactoring this mess? - EB

704 -- FIXME: Anyone feel like refactoring this mess? - EB

704− elab' ina topfc tm@(PApp fc (PRef ffc f) args_in)

705+ elab' ina topfc tm@(PApp fc (PRef ffc hls f) args_in)

705 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

706 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

706 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

707 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

707 | otherwise = implicitApp $

708 | otherwise = implicitApp $

@@ -723,11 +724,12 @@ elab ist info emode opts fn tm

723 if (f `elem` map fst env && length args == 1 && length args_in == 1)

724 if (f `elem` map fst env && length args == 1 && length args_in == 1)

724 then -- simple app, as below

725 then -- simple app, as below

725 do simple_app False

726 do simple_app False

726− (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc f))

727+ (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))

727 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

728 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

728 (show tm)

729 (show tm)

729 solve

730 solve

730− highlightSource ffc annot

731+ mapM (uncurry highlightSource) $

732+ (ffc, annot) : map (\f -> (f, annot)) hls

731 return []

733 return []

732 else

734 else

733 do ivs <- get_instances

735 do ivs <- get_instances

@@ -753,7 +755,8 @@ elab ist info emode opts fn tm

753 ulog <- getUnifyLog

755 ulog <- getUnifyLog

754

756

755 annot <- findHighlight f

757 annot <- findHighlight f

756− highlightSource ffc annot

758+ mapM (uncurry highlightSource) $

759+ (ffc, annot) : map (\f -> (f, annot)) hls

757

760

758 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

761 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

759 [] fc False f

762 [] fc False f

@@ -851,8 +854,8 @@ elab ist info emode opts fn tm

851 tacTm (PProof _) = True

854 tacTm (PProof _) = True

852 tacTm _ = False

855 tacTm _ = False

853

856

854− setInjective (PRef _ n) = setinj n

857+ setInjective (PRef _ _ n) = setinj n

855− setInjective (PApp _ (PRef _ n) _) = setinj n

858+ setInjective (PApp _ (PRef _ _ n) _) = setinj n

856 setInjective _ = return ()

859 setInjective _ = return ()

857

860

858 elab' ina _ tm@(PApp fc f [arg]) =

861 elab' ina _ tm@(PApp fc f [arg]) =

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

862 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

865 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

863 (show tm)

866 (show tm)

864 solve

867 solve

865− where headRef (PRef _ _) = True

868+ where headRef (PRef _ _ _) = True

866 headRef (PApp _ f _) = headRef f

869 headRef (PApp _ f _) = headRef f

867 headRef (PAlternative _ as) = all headRef as

870 headRef (PAlternative _ as) = all headRef as

868 headRef _ = False

871 headRef _ = False

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

924 elab' ina (Just fc) t

927 elab' ina (Just fc) t

925 focus valn

928 focus valn

926 elab' ina (Just fc) sc

929 elab' ina (Just fc) sc

927− elab' ina (Just fc) (PRef fc letn)

930+ elab' ina (Just fc) (PRef fc [] letn)

928 solve

931 solve

929 elab' ina _ c@(PCase fc scr opts)

932 elab' ina _ c@(PCase fc scr opts)

930 = do attack

933 = do attack

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

1163 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1166 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1164

1167

1165 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1168 isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1166− isScr (PRef _ n) (n', b) = (n', (n == n', b))

1169+ isScr (PRef _ _ n) (n', b) = (n', (n == n', b))

1167 isScr _ (n', b) = (n', (False, b))

1170 isScr _ (n', b) = (n', (False, b))

1168

1171

1169 caseBlock :: FC -> Name

1172 caseBlock :: FC -> Name

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

1192

1195

1193 getNmScr (n, (s, _)) = (n, s)

1196 getNmScr (n, (s, _)) = (n, s)

1194

1197

1195− mkarg (n, s) = (PRef fc n, s)

1198+ mkarg (n, s) = (PRef fc [] n, s)

1196 -- may be shadowed names in the new pattern - so replace the

1199 -- may be shadowed names in the new pattern - so replace the

1197 -- old ones with an _

1200 -- old ones with an _

1198 -- Also, names which don't appear on the rhs should not be

1201 -- Also, names which don't appear on the rhs should not be

@@ -1202,34 +1205,34 @@ elab ist info emode opts fn tm

1202 = let args' = map (shadowed (allNamesIn l)) args

1205 = let args' = map (shadowed (allNamesIn l)) args

1203 args'' = map (implicitable (allNamesIn r ++

1206 args'' = map (implicitable (allNamesIn r ++

1204 keepscrName scr)) args'

1207 keepscrName scr)) args'

1205− lhs = PApp (getFC fc l) (PRef NoFC n)

1208+ lhs = PApp (getFC fc l) (PRef NoFC [] n)

1206 (map (mkLHSarg l) args'') in

1209 (map (mkLHSarg l) args'') in

1207 PClause (getFC fc l) n lhs [] r []

1210 PClause (getFC fc l) n lhs [] r []

1208

1211

1209 -- Keep scrutinee available if it's just a name (this makes

1212 -- Keep scrutinee available if it's just a name (this makes

1210 -- the names in scope look better when looking at a hole on

1213 -- the names in scope look better when looking at a hole on

1211 -- the rhs of a case)

1214 -- the rhs of a case)

1212− keepscrName (PRef _ n) = [n]

1215+ keepscrName (PRef _ _ n) = [n]

1213 keepscrName _ = []

1216 keepscrName _ = []

1214

1217

1215 mkLHSarg l (tm, True) = pexp l

1218 mkLHSarg l (tm, True) = pexp l

1216 mkLHSarg l (tm, False) = pexp tm

1219 mkLHSarg l (tm, False) = pexp tm

1217

1220

1218− shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)

1221+ shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)

1219 shadowed new t = t

1222 shadowed new t = t

1220

1223

1221− implicitable rhs (PRef _ n, s) | n `notElem` rhs = (Placeholder, s)

1224+ implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)

1222 implicitable rhs t = t

1225 implicitable rhs t = t

1223

1226

1224

1227

1225 getFC d (PApp fc _ _) = fc

1228 getFC d (PApp fc _ _) = fc

1226− getFC d (PRef fc _) = fc

1229+ getFC d (PRef fc _ _) = fc

1227 getFC d (PAlternative _ (x:_)) = getFC d x

1230 getFC d (PAlternative _ (x:_)) = getFC d x

1228 getFC d x = d

1231 getFC d x = d

1229

1232

1230 insertLazy :: PTerm -> ElabD PTerm

1233 insertLazy :: PTerm -> ElabD PTerm

1231− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

1234+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1232− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

1235+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

1233 insertLazy (PCoerced t) = return t

1236 insertLazy (PCoerced t) = return t

1234 insertLazy t =

1237 insertLazy t =

1235 do ty <- goal

1238 do ty <- goal

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

1244 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

1247 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

1245 mkDelay env t

1248 mkDelay env t

1246 = let fc = fileFC "Delay" in

1249 = let fc = fileFC "Delay" in

1247− addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

1250+ addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))

1248 [pexp t])

1251 [pexp t])

1249

1252

1250

1253

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

1253 -- blowup especially where there are errors deep in large expressions.

1256 -- blowup especially where there are errors deep in large expressions.

1254 notImplicitable (PApp _ f _) = notImplicitable f

1257 notImplicitable (PApp _ f _) = notImplicitable f

1255 -- TMP HACK no coercing on bind (make this configurable)

1258 -- TMP HACK no coercing on bind (make this configurable)

1256− notImplicitable (PRef _ n)

1259+ notImplicitable (PRef _ _ n)

1257 | [opts] <- lookupCtxt n (idris_flags ist)

1260 | [opts] <- lookupCtxt n (idris_flags ist)

1258 = NoImplicit `elem` opts

1261 = NoImplicit `elem` opts

1259 notImplicitable (PAlternative (ExactlyOne _) as) = any notImplicitable as

1262 notImplicitable (PAlternative (ExactlyOne _) as) = any notImplicitable as

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

1306 where

1309 where

1307 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1310 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1308 addImplBound ist (map fst env)

1311 addImplBound ist (map fst env)

1309− (PApp fc (PRef fc n) [pexp (PCoerced t)])

1312+ (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1310

1313

1311 -- | Elaborate the arguments to a function

1314 -- | Elaborate the arguments to a function

1312 elabArgs :: IState -- ^ The current Idris state

1315 elabArgs :: IState -- ^ The current Idris state

@@ -1369,8 +1372,8 @@ elab ist info emode opts fn tm

1369pruneAlt :: [PTerm] -> [PTerm]

1372pruneAlt :: [PTerm] -> [PTerm]

1370pruneAlt xs = map prune xs

1373pruneAlt xs = map prune xs

1371 where

1374 where

1372− prune (PApp fc1 (PRef fc2 f) as)

1375+ prune (PApp fc1 (PRef fc2 hls f) as)

1373− = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1376+ = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

1374 prune t = t

1377 prune t = t

1375

1378

1376 choose f (PAlternative a as)

1379 choose f (PAlternative a as)

@@ -1383,7 +1386,7 @@ pruneAlt xs = map prune xs

1383 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

1386 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

1384 choose f t = t

1387 choose f t = t

1385

1388

1386− headIs f (PApp _ (PRef _ f') _) = f == f'

1389+ headIs f (PApp _ (PRef _ _ f') _) = f == f'

1387 headIs f (PApp _ f' _) = headIs f f'

1390 headIs f (PApp _ f' _) = headIs f f'

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

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

1389

1392

@@ -1400,7 +1403,7 @@ pruneByType env t c as

1400 | Just n <- getName t,

1403 | Just n <- getName t,

1401 n `elem` env = Just t

1404 n `elem` env = Just t

1402 | otherwise = locallyBound ts

1405 | otherwise = locallyBound ts

1403− getName (PRef _ n) = Just n

1406+ getName (PRef _ _ n) = Just n

1404 getName (PApp _ f _) = getName f

1407 getName (PApp _ f _) = getName f

1405 getName (PHidden t) = getName t

1408 getName (PHidden t) = getName t

1406 getName _ = Nothing

1409 getName _ = Nothing

@@ -1417,8 +1420,8 @@ pruneByType env (P _ n _) ctxt as

1417 _ -> asV

1420 _ -> asV

1418 _ -> as'

1421 _ -> as'

1419 where

1422 where

1420− headIs var f (PRef _ f') = typeHead var f f'

1423+ headIs var f (PRef _ _ f') = typeHead var f f'

1421− headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1424+ headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

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

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

1423 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1426 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

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

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

49import Util.Pretty(pretty, text)

51elabTransform :: 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

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

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

@@ -129,7 +129,7 @@ decorateid decorate (PClauses f o n cs)

129 dc (PWith fc n t as w pn ds)

130 = PWith fc (decorate n) (dappname t) as w pn

131 (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

133 dappname t = t

134

135

src/Idris/Elab/Value.hs+4−4

@@ -121,15 +121,15 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

121-- (as a default numeric tye), then printing it as any Showable thing

122elabExec :: FC -> PTerm -> PTerm

123elabExec fc tm = runtm (PAlternative FirstSuccess

124− [printtm (PApp fc (PRef fc (sUN "the"))

124+ [printtm (PApp fc (PRef fc [] (sUN "the"))

125 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

126 tm,

127 printtm tm

128 ])

129 where

130− runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]

131− printtm t = PApp fc (PRef fc (sUN "printLn"))

131+ printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132− [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

132+ [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133

134elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

135elabREPL info aspat tm

src/Idris/ElabDecls.hs+2−2

@@ -68,8 +68,8 @@ recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'

68-- | Return the elaborated term which calls 'main'

69elabMain :: Idris Term

70elabMain = do (m, _) <- elabVal recinfo ERHS

71− (PApp fc (PRef fc (sUN "run__IO"))

71+ (PApp fc (PRef fc [] (sUN "run__IO"))

72− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

72+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

73 return m

74 where fc = fileFC "toplevel"

src/Idris/ElabQuasiquote.hs+1−1

@@ -163,7 +163,7 @@ extractUnquotes n (PQuasiquote tm goal)

163 = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm

164extractUnquotes n (PUnquote tm)

165 | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")

166− return (PRef (fileFC "(unquote)") n, [(n, tm)])

166+ return (PRef (fileFC "(unquote)") [] n, [(n, tm)])

167 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

168 extractUnquotes (n-1) tm

169extractUnquotes n (PRunElab fc tm ns)

src/Idris/Error.hs+2−2

@@ -88,8 +88,8 @@ getErrSpan _ = emptyFC

88-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent

89warnDisamb :: IState -> PTerm -> Idris ()

90warnDisamb ist (PQuote _) = return ()

91−warnDisamb ist (PRef _ _) = return ()

91+warnDisamb ist (PRef _ _ _) = return ()

92−warnDisamb ist (PInferRef _ _) = return ()

92+warnDisamb ist (PInferRef _ _ _) = return ()

93warnDisamb ist (PPatvar _ _) = return ()

94warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

95warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

src/Idris/IBC.hs+13−9

@@ -40,7 +40,7 @@ import System.Directory

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 114

43+ibcVersion = 115

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

@@ -1522,12 +1522,14 @@ instance Binary PTerm where

1522 = case x of

1523 PQuote x1 -> do putWord8 0

1524 put x1

1525− PRef x1 x2 -> do putWord8 1

1525+ PRef x1 x2 x3 -> do putWord8 1

1526− put x1

1526+ put x1

1527− put x2

1527+ put x2

1528+ put x3

1528− PInferRef x1 x2 -> do putWord8 2

1529+ PInferRef x1 x2 x3 -> do putWord8 2

1529− put x1

1530+ put x1

1530− put x2

1531+ put x2

1532+ put x3

1531 PPatvar x1 x2 -> do putWord8 3

1533 PPatvar x1 x2 -> do putWord8 3

1532 put x1

1534 put x1

1533 put x2

1535 put x2

@@ -1663,10 +1665,12 @@ instance Binary PTerm where

1663 return (PQuote x1)

1665 return (PQuote x1)

1664 1 -> do x1 <- get

1666 1 -> do x1 <- get

1665 x2 <- get

1667 x2 <- get

1668+ x3 <- get

1666− return (PRef x1 x2)

1669+ return (PRef x1 x2 x3)

1667 2 -> do x1 <- get

1670 2 -> do x1 <- get

1668 x2 <- get

1671 x2 <- get

1672+ x3 <- get

1669− return (PInferRef x1 x2)

1673+ return (PInferRef x1 x2 x3)

1670 3 -> do x1 <- get

1674 3 -> do x1 <- get

1671 x2 <- get

1675 x2 <- get

1672 return (PPatvar x1 x2)

1676 return (PPatvar x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -288,8 +288,8 @@ loadDocs ist n

288-- TODO: Remove unnecessary cases

289extractPTermNames :: PTerm -- ^ Where to extract names from

290 -> [Name] -- ^ Extracted names

291−extractPTermNames (PRef _ n) = [n]

291+extractPTermNames (PRef _ _ n) = [n]

292−extractPTermNames (PInferRef _ n) = [n]

292+extractPTermNames (PInferRef _ _ n) = [n]

293extractPTermNames (PPatvar _ n) = [n]

294extractPTermNames (PLam _ n _ p1 p2) = n : concatMap extract [p1, p2]

295extractPTermNames (PPi _ n _ p1 p2) = n : concatMap extract [p1, p2]

src/Idris/Interactive.hs+5−5

@@ -112,7 +112,7 @@ addMissing fn updatefile l n

112 else iPrintResult extras

113 where showPat = show . stripNS

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

116 dens t = t

117

118 nsroot (NS n _) = nsroot n

@@ -120,7 +120,7 @@ addMissing fn updatefile l n

120 nsroot n = n

121

122 getAppName (PApp _ r _) = getAppName r

123− getAppName (PRef _ r) = r

123+ getAppName (PRef _ _ r) = r

124 getAppName _ = n

125

126 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

@@ -178,10 +178,10 @@ doProofSearch fn updatefile rec l n hints (Just depth)

178 let fc = fileFC fn

179 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

180 (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) []

182 newmv <- idrisCatch

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

185 ctxt <- getContext

186 i <- getIState

187 return . flip displayS "" . renderPretty 1.0 80 $

@@ -204,7 +204,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

204 dropCtxt _ t = t

205

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

208 dens t = t

209

210 nsroot (NS n _) = nsroot n

src/Idris/ParseData.hs+1−1

@@ -218,7 +218,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

218 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

219 cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

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

222 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

223 do let cty = bindArgs cargs conty

224 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

src/Idris/ParseExpr.hs+47−41

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

174 _ -> n

175

176 update :: [(Name, SynMatch)] -> PTerm -> PTerm

177− update ns (PRef fc n) = case lookup n ns of

177+ update ns (PRef fc hls n) = case lookup n ns of

178− Just (SynTm t) -> t

178+ Just (SynTm t) -> t

179− _ -> PRef fc n

179+ _ -> PRef fc hls n

180 update ns (PLam fc n nfc ty sc)

181 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)

182 update ns (PPi p n fc ty sc)

@@ -346,7 +346,7 @@ simpleExpr syn =

346 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

347 return (PMetavar (FC f (l, c-1) end) x)

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

350 <|> proofExpr syn

351 <|> tacticsExpr syn

352 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

@@ -358,16 +358,16 @@ simpleExpr syn =

358 fc <- getFC

359 return (modifyConst syn fc (PConstant cfc c))

360 <|> do symbol "'"; fc <- getFC; str <- fst <$> name

361− return (PApp fc (PRef fc (sUN "Symbol_"))

361+ return (PApp fc (PRef fc [] (sUN "Symbol_"))

362 [pexp (PConstant NoFC (Str (show str)))])

363 <|> do (x, fc) <- fnName

364 if inPattern syn

365− then option (PRef fc x)

365+ then option (PRef fc [fc] x)

366 (do reservedOp "@"

367 s <- simpleExpr syn

368 fcIn <- getFC

369 return (PAs fcIn x s))

370− else return (PRef fc x)

370+ else return (PRef fc [fc] x)

371 <|> idiom syn

372 <|> listExpr syn

373 <|> alt syn

@@ -415,14 +415,14 @@ bracketed' open syn =

415 fc <- getFC

416 r <- expr syn

417 lchar ')'

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

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

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

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

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

422 then fail "minus not allowed in section"

423 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

424− (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

424+ (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),

425− pexp e]))

425+ pexp e]))

426 <|> try (do l <- simpleExpr syn

427 op <- option Nothing (do o <- operator

428 lchar ')'

@@ -431,8 +431,8 @@ bracketed' open syn =

431 case op of

432 Nothing -> bracketedExpr syn l

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

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

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

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

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

436 <|> do l <- expr syn

437 bracketedExpr syn l

438

@@ -465,7 +465,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

465modifyConst syn fc (PConstant inFC (BI x))

466 | not (inPattern syn)

467 = 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)))]

469 : consts)

470 | otherwise = PAlternative FirstSuccess consts

471 where

@@ -580,7 +580,7 @@ app syn = do f <- simpleExpr syn

580 return (PLet fc (sMN 0 "match") NoFC

581 f

582 (PMatchApp fc ff)

583− (PRef fc (sMN 0 "match")))

583+ (PRef fc [] (sMN 0 "match")))

584 <?> "matching application expression") <|> (do

585 fc <- getFC

586 i <- get

@@ -589,17 +589,17 @@ app syn = do f <- simpleExpr syn

589 [] -> return f

590 _ -> return (flattenFromInt fc f args))

591 <?> "function application"

592− where

592+ where

593 -- bit of a hack to deal with the situation where we're applying a

594 -- literal to an argument, which we may want for obscure applications

595 -- of fromInteger, and this will help disambiguate better.

596 -- We know, at least, it won't be one of the constants!

597 flattenFromInt fc (PAlternative x alts) args

598 | Just i <- getFromInt alts

599− = PApp fc (PRef fc (sUN "fromInteger")) (i : args)

599+ = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

600 flattenFromInt fc f args = PApp fc f args

601

602− getFromInt ((PApp _ (PRef _ n) [a]) : _) | n == sUN "fromInteger" = Just a

602+ getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a

603 getFromInt (_ : xs) = getFromInt xs

604 getFromInt _ = Nothing

605

@@ -628,10 +628,10 @@ ImplicitArg ::=

628-}

629implicitArg :: SyntaxInfo -> IdrisParser PArg

630implicitArg syn = do lchar '{'

631− n <- fst <$> name

631+ (n, nfc) <- name

632 fc <- getFC

633− v <- option (PRef fc n) (do lchar '='

633+ v <- option (PRef nfc [nfc] n) (do lchar '='

634− expr syn)

634+ expr syn)

635 lchar '}'

636 return (pimp n v True)

637 <?> "implicit function argument"

@@ -735,14 +735,14 @@ recordType syn =

735 case rec of

736 Nothing ->

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

739 Just v -> return (applyAll fc fields v)

740 Right fields ->

741 case rec of

742 Nothing ->

743 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

744− (getAll fc (reverse fields)

744+ (getAll fc (reverse fields)

745− (PRef fc (sMN 0 "fldx"))))

745+ (PRef fc [] (sMN 0 "fldx"))))

746 Just v -> return (getAll fc (reverse fields) v)

747

748 <?> "record setting expression"

@@ -766,17 +766,17 @@ recordType syn =

766 applyAll fc [] x = x

767 applyAll fc ((ns, e) : es) x

768 = applyAll fc es (doUpdate fc ns e x)

769−

769+

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

772 doUpdate fc (n : ns) e get

773− = PApp fc (PRef fc (mkType n))

773+ = PApp fc (PRef fc [] (mkType n))

774− [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),

774+ [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),

775 pexp get]

776

777 getAll :: FC -> [Name] -> PTerm -> PTerm

778− getAll fc [n] e = PApp fc (PRef fc n) [pexp 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)]

779+ getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]

780

781

782-- | Creates setters for record types on necessary functions

@@ -838,7 +838,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"

838 pmList [] sc = sc

839 pmList ((i, (fc, x)) : xs) sc

840 = PLam fc (sMN i "lamp") NoFC Placeholder

841− (PCase fc (PRef fc (sMN i "lamp"))

841+ (PCase fc (PRef fc [] (sMN i "lamp"))

842 [(x, pmList xs sc)])

843 lambdaTail :: IdrisParser PTerm

844 lambdaTail = impossible <|> symbol "=>" *> expr syn

@@ -859,7 +859,7 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"

859 highlightP kw AnnKeyword

860 highlightP kw' AnnKeyword

861 return (PRewrite fc

862− (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

862+ (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc

863 giving)

864 <?> "term rewrite expression"

865

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

@@ -1144,20 +1144,26 @@ listExpr syn = do (FC f (l, c) _) <- getFC

1144 qs <- sepBy1 (do_ syn) (lchar ',')

1145 lchar ']'

1146 return (PDoBlock (map addGuard qs ++

1147− [DoExp fc (PApp fc (PRef fc (sUN "return"))

1147+ [DoExp fc (PApp fc (PRef fc [] (sUN "return"))

1148 [pexp x])]))) <|>

1149+ (do xs <- many (do (FC fn (sl, sc) _) <- getFC

1149− (do xs <- many ((lchar ',' <?> "list element") *> expr syn)

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

1150 lchar ']' <?> "end of list expression"

1155 lchar ']' <?> "end of list expression"

1156+ let rbrackFC = FC fn (sl, sc) (sl, sc+1)

1151− return (mkList fc (x:xs))))

1157+ return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))

1152 <?> "list expression"

1158 <?> "list expression"

1153 where

1159 where

1154 mkNil :: FC -> PTerm

1160 mkNil :: FC -> PTerm

1155− mkNil fc = PRef fc (sUN "Nil")

1161+ mkNil fc = PRef fc [fc] (sUN "Nil")

1156− mkList :: FC -> [PTerm] -> PTerm

1162+ mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm

1157− mkList fc [] = PRef NoFC (sUN "Nil")

1163+ mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")

1158− mkList fc (x : xs) = PApp fc (PRef NoFC (sUN "::")) [pexp x, pexp (mkList fc xs)]

1164+ mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]

1159 addGuard :: PDo -> PDo

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

1161 [pexp e])

1167 [pexp e])

1162 addGuard x = x

1168 addGuard x = x

1163

1169

@@ -1216,7 +1222,7 @@ do_ syn

1216 option (DoBind fc i ifc e)

1222 option (DoBind fc i ifc e)

1217 (do lchar '|'

1223 (do lchar '|'

1218 ts <- sepBy1 (do_alt syn) (lchar '|')

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

1220 <|> try (do i <- expr' syn

1226 <|> try (do i <- expr' syn

1221 symbol "<-"

1227 symbol "<-"

1222 fc <- getFC

1228 fc <- getFC

src/Idris/ParseOps.hs+5−5

@@ -35,11 +35,11 @@ import Debug.Trace

35-- using pre-build and user-defined operator/fixity declarations

36table :: [FixDecl] -> OperatorTable IdrisParser PTerm

37table 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])]] ++

39 toTable (reverse fixes) ++

40 [[backtick],

41 [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],

43 [nofixityoperator]]

44 where

45 flatten :: PTerm -> PTerm -- flatten application

@@ -52,9 +52,9 @@ toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

52toTable fs = map (map toBin)

53 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

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

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

58 assoc (Infixl _) = AssocLeft

59 assoc (Infixr _) = AssocRight

60 assoc (InfixN _) = AssocNone

@@ -79,7 +79,7 @@ backtick = Infix (do indentPropHolds gtProp

79 lchar '`'; (n, fc) <- fnName

80 lchar '`'

81 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

84-- | Operator without fixity (throws an error)

85nofixityoperator :: Operator IdrisParser PTerm

src/Idris/Parser.hs+7−7

@@ -324,8 +324,8 @@ syntaxRule syn

324 uniquifyBinders userNames = fixBind []

325 where

326 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm

327− fixBind rens (PRef fc n) | Just n' <- lookup n rens =

327+ fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =

328− return $ PRef fc n'

328+ return $ PRef fc hls n'

329 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =

330 return $ PPatvar fc n'

331 fixBind rens (PLam fc n nfc ty body)

@@ -735,7 +735,7 @@ instance_ syn = do (doc, argDocs)

735 let cs' = [(c, ty) | (c, _, ty) <- cs]

736 (cn, cnfc) <- fnName

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

739 let t = bindList (PPi constraint) cs sc

740 ds <- option [] (instanceBlock syn)

741 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]

@@ -953,7 +953,7 @@ clause syn

953 let capp = PLet fc (sMN 0 "match") NoFC

954 ty

955 (PMatchApp fc n)

956− (PRef fc (sMN 0 "match"))

956+ (PRef fc [] (sMN 0 "match"))

957 ist <- get

958 put (ist { lastParse = Just n })

959 return $ PClause fc n capp [] r wheres

@@ -976,7 +976,7 @@ clause syn

976 do terminator

977 return ([], [])]

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

980 put (ist { lastParse = Just n })

981 return $ PClause fc n capp wargs rs wheres) <|> (do

982 popIndent

@@ -987,7 +987,7 @@ clause syn

987 ds <- some $ fnDecl syn

988 closeBlock

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

991 let withs = map (fillLHSD n capp wargs) $ concat ds

992 put (ist { lastParse = Just n })

993 return $ PWith fc n capp wargs wval pn withs)

@@ -998,7 +998,7 @@ clause syn

998 args <- many (try (implicitArg (syn { inPattern = True } ))

999 <|> (fmap pexp (argExpr syn)))

1000 wargs <- many (wExpr syn)

1001− let capp = PApp fc (PRef nfc n)

1001+ let capp = PApp fc (PRef nfc [nfc] n)

1002 (cargs ++ args)

1003 (do r <- rhs syn n

1004 ist <- get

src/Idris/PartialEval.hs+3−3

@@ -206,8 +206,8 @@ mkNewPats ist d ns newname sname lhs rhs =

206 mkClause (oldlhs, oldrhs)

207 = let (_, as) = unApply oldlhs

208 lhsargs = mkLHSargs [] ns as

209− lhs = PApp emptyFC (PRef emptyFC newname) lhsargs

209+ lhs = PApp emptyFC (PRef emptyFC [] newname) lhsargs

210− rhs = PApp emptyFC (PRef emptyFC sname)

210+ rhs = PApp emptyFC (PRef emptyFC [] sname)

211 (mkRHSargs ns lhsargs) in

212 (lhs, rhs)

213

@@ -245,7 +245,7 @@ mkNewPats ist d ns newname sname lhs rhs =

245mkPE_TermDecl :: IState -> Name -> Name ->

246 [(PEArgType, Term)] -> PEDecl

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

249 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

250 patdef = lookupCtxtExact sname (idris_patdefs ist)

251 newpats = case patdef of

src/Idris/ProofSearch.hs+4−4

@@ -25,8 +25,8 @@ trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

25trivial = trivialHoles []

27trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

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

29+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

30 return ())

31 (do env <- get_env

32 g <- goal

@@ -42,7 +42,7 @@ trivialHoles ok elab ist

42 -- anywhere but the top is okay for a hole, if holesOK set

43 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

44 holesOK hs (binderTy b)

45− then try' (elab (PRef (fileFC "prf") x))

45+ then try' (elab (PRef (fileFC "prf") [] x))

46 (tryAll xs) True

47 else tryAll xs

@@ -227,7 +227,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

227 = do let a = getPArity (delab ist (binderTy t))

228 tryLocalArg d locs tys n a

229

230− tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)

230+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)

231 tryLocalArg d locs tys n i

232 = simple_app False (tryLocalArg d locs tys n (i - 1))

233 (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

310 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))

311 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm

312 return (d', prev, st', done, prf', env, go)

313− ECheck (PRef _ n) ->

313+ ECheck (PRef _ _ n) ->

314 do (d', st', done, prf', go) <- checkNameType e prf n

315 return (d', prev, st', done, prf', env, go)

316 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

331 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

332 DoLet fc i ifc ty expr ->

333 do (tm, ty) <- elabVal recinfo ERHS

334− (PApp NoFC (PRef NoFC (sUN "the"))

334+ (PApp NoFC (PRef NoFC [] (sUN "the"))

335 [ pexp (inLets ist env ty)

336 , pexp (inLets ist env expr)

337 ])

@@ -417,7 +417,7 @@ ploop fn d prompt prf e h

417 when (not (null hs)) $ ifail "Incomplete proof"

418 iputStrLn "Proof completed!"

419 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

421 Success (TCheck t) -> checkType e prf t

422 Success (TEval t) -> evalTerm e prf t

423 Success (TDocStr x) -> docStr e prf x

src/Idris/Providers.hs+1−1

@@ -10,7 +10,7 @@ import Idris.Error

10-- | Wrap a type provider in the type of type providers

11providerTy :: FC -> PTerm -> PTerm

12providerTy 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]

15ioret :: Name

16ioret = sUN "prim_io_return"

src/Idris/REPL.hs+6−6

@@ -345,7 +345,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

345 case splitName name of

346 Left err -> iPrintError err

347 Right n -> process "(idemode)"

348− (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

348+ (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

349runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

350 case parseConst orig name of

351 Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

@@ -581,7 +581,7 @@ idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)

581 iPrintResult "defined"

582idemodeProcess fn (Undefine n) = process fn (Undefine n)

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

585idemodeProcess fn (Check t) = process fn (Check t)

586idemodeProcess fn (Core t) = process fn (Core t)

587idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

@@ -893,7 +893,7 @@ process fn (ExecVal t)

893 prettyIst ist (delab ist ty'))

894 iPrintTermWithType resOut tyOut

895

896−process fn (Check (PRef _ n))

896+process fn (Check (PRef _ _ n))

897 = do ctxt <- getContext

898 ist <- getIState

899 let ppo = ppOptionIst ist

@@ -1173,8 +1173,8 @@ process fn (Compile codegen f)

1173 let iface = Interface `elem` opts

1174 m <- if iface then return Nothing else

1175 do (m', _) <- elabVal recinfo ERHS

1176− (PApp fc (PRef fc (sUN "run__IO"))

1176+ (PApp fc (PRef fc [] (sUN "run__IO"))

1177− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1177+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

1178 return (Just m')

1179 ir <- compile codegen f m

1180 i <- getIState

@@ -1345,7 +1345,7 @@ process fn (TransformInfo n)

1345-- iputStrLn "---------------"

1346-- showTrans i ts

1347

1348−process fn (PPrint fmt width (PRef _ n))

1348+process fn (PPrint fmt width (PRef _ _ n))

1349 = do outs <- pprintDef n

1350 iPrintResult =<< renderExternal fmt width (vsep outs)

1351

src/Idris/REPLParser.hs+1−1

@@ -304,7 +304,7 @@ cmd_execute name = do

304 tm <- option maintm (P.fullExpr defaultSyntax)

305 return (Right (Execute tm))

306 where

307− maintm = PRef (fileFC "(repl)") (sNS (sUN "main") ["Main"])

307+ maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

308

309

310cmd_dynamic :: String -> P.IdrisParser (Either String Command)