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

src/Idris/AbsSyntax.hs+73−73

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

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

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

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

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

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

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

10031003 = let n' = mkShadow n in

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

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

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

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

10071007 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

10171017

10181018 en (PQuote (Var n))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1033− en (PRef fc n)

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

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

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

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

1038− en (PInferRef fc n)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1033+ en (PRef fc hl n)

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

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

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

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

1038+ en (PInferRef fc hl n)

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

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

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

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

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

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

11031103

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

11051105

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

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

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

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

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

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

11621162getPriority :: IState -> PTerm -> Int

11631163getPriority i tm = 1 -- pri tm

11641164 where

1165− pri (PRef _ n) =

1165+ pri (PRef _ _ n) =

11661166 case lookupP n (tt_ctxt i) of

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

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

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

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

12891289 | otherwise = doAdd cs ns t

12901290

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

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

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

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

12931293

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

12951295 = getcapp c ++ getConstraints sc

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

12971297 getConstraints _ = []

12981298

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

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

13001300 = do ns <- mapM getName args

13011301 return (UConstraint c ns)

13021302 getcapp _ = []

13031303

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

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

13051305 getName _ = []

13061306

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

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

14581458 imps True (n:env) sc

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

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

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

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

14621462 _ -> [])

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

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

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

14661466 imps True (n:env) sc

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

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

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

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

14701470 _ -> [])

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

14721472 put (PConstraint 10 l n Placeholder : decls,

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

14741474 imps True (n:env) sc

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

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

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

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

14781478 _ -> [])

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

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

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

14901490 = do (decls, ns) <- get

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

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

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

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

14941494 = do (decls, ns) <- get

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

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

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

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

15461546 where

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

1548− ai qq env ds (PRef fc f)

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

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

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

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

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

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

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

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

15541554 = let l' = ai qq env ds l

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

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

15731573 PAlternative a as'

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

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

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

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

1577− PApp fc (PInferRef ffc f) as'

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

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

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

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

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

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

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

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

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

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

16091609 PLam fc n nfc ty' sc'

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

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

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

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

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

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

16141614 = case lookupDef n (tt_ctxt ist) of

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

16161616 val' = ai qq env ds val

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

16181618 PLet fc n nfc ty' val' sc'

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

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

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

16211621 = let ty' = ai qq env ds ty

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

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

16741674 vname _ = False

16751675

16761676aiFn 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

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

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

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

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

16831683 [] -> nh

16841684 x -> x

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

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

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

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

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

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

16901690 alts -> Right $

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

16931693 (insertImpl ns as)) alts

16941694 where

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

17371737 case find n imps [] of

17381738 Just (tm, imps') ->

17391739 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

17411741 PImp p True l n ph :

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

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

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

17801780stripLinear :: IState -> PTerm -> PTerm

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

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

1783− sl (PRef fc f)

1783+ sl (PRef fc hl f)

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

1785− = return $ PRef fc f

1785+ = return $ PRef fc hl f

17861786 | otherwise = do ns <- get

17871787 if (f `elem` ns)

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

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

17891789 else do put (f : ns)

1790− return (PRef fc f)

1790+ return (PRef fc hl f)

17911791 sl (PPatvar fc f)

17921792 = do ns <- get

17931793 if (f `elem` ns)

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

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

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

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

1813− PRef _ _ -> return fn

1813+ PRef _ _ _ -> return fn

18141814 t -> sl t

18151815 args' <- mapM slA args

18161816 return $ PApp fc fn' args'

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

18321832stripUnmatchable :: IState -> PTerm -> PTerm

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

18341834 su :: PTerm -> PTerm

1835− su tm@(PRef fc f)

1835+ su tm@(PRef fc hl f)

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

18371837 = Placeholder

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

18391839 = PHidden tm

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

18411841 = PHidden tm

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

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

18431843 -- here we use canBeDConName because the impossible pattern

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

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

19301930 fullApp x = x

19311931

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

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

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

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

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

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

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

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

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

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

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

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

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

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

19421942 | length args == length args'

19431943 = do mf <- match' f f'

19441944 ms <- zipWithM matchArg args args'

19451945 return (mf ++ concat ms)

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

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

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

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

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

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

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

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

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

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

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

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

19531953 || tm == Placeholder)

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

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

19571957 where dropNS (NS n _) = n

19581958 dropNS n = n

1959− match (PRef _ n) tm

1959+ match (PRef _ _ n) tm

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

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

19621962 = return [(n, tm)]

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

19861986 _ -> LeftErr (a, b)

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

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

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

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

19901990 match (PQuote _) _ = return []

19911991 match (PProof _) _ = return []

19921992 match (PTactics _) _ = return []

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

20442044

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

20462046substMatchShadow n shs tm t = sm shs t where

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

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

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

20492049 sm xs (PPi p x fc t sc)

20502050 | x `elem` xs

20512051 = let x' = nextName x in

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

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

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

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

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

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

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

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

20722072

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

20742074shadow n n' t = sm t where

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

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

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

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

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

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

21702170 mkUniq (PPair fc p l r)

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

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

21742174 | t /= Placeholder

21752175 = do env <- get

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

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

21802180 put (S.insert n' env)

21812181 t' <- mkUniq t

21822182 sc'' <- mkUniq sc'

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

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

21842184 mkUniq (PDPair fc p l t r)

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

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

src/Idris/AbsSyntaxTree.hs+45−45

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

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

814814updateNs [] t = t

815815updateNs ns t = mapPT updateRef t

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

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

817817 updateRef t = t

818818

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

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

831831

832832-- | High level language terms

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

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

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

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

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

836836 | PPatvar FC Name -- ^ A pattern variable

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

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

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

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

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

886886mapPTermFC f g (PQuote q) = PQuote q

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

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

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

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

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

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

891891mapPTermFC 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

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

11051105highestFC :: PTerm -> Maybe FC

11061106highestFC (PQuote _) = Nothing

1107−highestFC (PRef fc _) = Just fc

1108−highestFC (PInferRef fc _) = Just fc

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

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

11091109highestFC (PPatvar fc _) = Just fc

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

11111111highestFC (PPi _ _ _ _ _) = Nothing

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

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

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

12941294

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

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

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

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

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

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

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

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

12991299 Nothing

13001300 Nothing

13011301 Nothing

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

13501350inferDecl = PDatadecl inferTy NoFC

13511351 (PType bi)

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

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

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

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

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

13551355inferOpts = []

13561356

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]

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

13591359

13601360getInferTerm, getInferType :: Term -> Term

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

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

14061406

14071407eqDecl = 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"))]

14091409 (PType bi)))

14101410 [(reflDoc, reflParamDoc,

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

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

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

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

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

14141414 pimp (n "B") Placeholder False,

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

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

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

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

14171417 where n a = sUN a

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

14191419 "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

15341534 prettySe d p bnd e

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

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

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

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

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

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

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

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

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

15851585 | n == eqTy, ppopt_impl ppo =

15861586 depth d . bracket p eqPrec $

15871587 enclose lparen rparen eq <+>

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

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

15941594 eqPrec = startPrec

15951595 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

15971597 | UN nm <- basename f

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

15991599 prettyName True (ppopt_impl ppo) bnd f

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

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

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

16031603 | UN nm <- basename op

16041604 , not (tnull nm) &&

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

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

16261626 inFix l r = align . group $

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

16281628 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

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

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

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

16341634 let args = getShowArgs as

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

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

16971697 IsTerm -> annName sigmaCon

16981698 TypeOrTerm -> id

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

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

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

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

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

17021702 prettySe d p bnd (PAlternative a as) =

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

17041704 where

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

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

17821782 slist' d _ _ e

17831783 | containsHole e = Nothing

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

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

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

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

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

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

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

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

17911791 all isImp imps,

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

18171817

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

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

1820− snat d p (PRef _ z)

1820+ snat d p (PRef _ _ z)

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

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

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

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

18571857

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

18591859containsHole :: 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]

18611861

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

18631863prettyName

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

19941994

19951995instance Sized PTerm where

19961996 size (PQuote rawTerm) = size rawTerm

1997− size (PRef fc name) = size name

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

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

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

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

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

20352035allNamesIn :: PTerm -> [Name]

20362036allNamesIn tm = nub $ ni [] tm

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

2038− ni env (PRef _ n)

2038+ ni env (PRef _ _ n)

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

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

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

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

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

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

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

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

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

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

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

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

20562056 ni env (PUnifyLog tm) = ni env tm

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

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

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

20782078 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

20802080 ni set (PDPair _ _ l t r) = ni (ni (ni set l) t) r

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

20822082 ni set (PHidden tm) = ni set tm

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

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

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

20972097 where

2098− ni env (PRef _ n)

2098+ ni env (PRef _ _ n)

20992099 | not (n `elem` env)

21002100 = case lookupTy n (tt_ctxt ist) of

21012101 [] -> [n]

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

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

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

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

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

21062106 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

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

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

21172117 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

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

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

21212121 ni env (PHidden tm) = ni env tm

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

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

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

21302130 where

2131− ni env (PRef _ n)

2131+ ni env (PRef _ _ n)

21322132 | not (n `elem` env)

21332133 = case lookupTy n (tt_ctxt ist) of

21342134 [] -> [n]

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

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

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

21472147 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

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

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

21512151 ni env (PHidden tm) = ni env tm

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

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

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

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

2165− ni env (PRef _ n)

2165+ ni env (PRef _ _ n)

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

21672167 = case lookupDefExact n (tt_ctxt ist) of

21682168 Nothing -> [n]

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

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

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

21782178 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

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

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

21822182 ni env (PHidden tm) = ni env tm

src/Idris/CaseSplit.hs+24−24

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

127127

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

129129stripNS tm = mapPT dens tm where

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

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

131131 dens t = t

132132

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

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

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

138138 ps' = mergeAllPats ist cv t ps in

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

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

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

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

142142 patvars (PPatvar _ n) = [n]

143143 patvars _ = []

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

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

147147-- user provided name (first pattern)

148148mergePat ist (PPatvar fc n) new t

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

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

150150mergePat ist old (PPatvar fc n) t

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

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

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

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

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

154154 return new

155155 | otherwise

156156 = do ms <- get

157157 case lookup n' (namemap ms) of

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

159− return (PRef fc x)

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

159+ return (PRef fc [] x)

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

161− return (PRef fc n)

161+ return (PRef fc [] n)

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

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

164164 return (PApp fc f newArgs)

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

169169 return (y { machine_inf = machine_inf x,

170170 getTm = tm' })

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

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

173− addUpdate n tm

174− return tm

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

173+ addUpdate n tm

174+ return tm

175175mergePat ist x y t = return y

176176

177177mergeUserImpl :: PTerm -> PTerm -> PTerm

178178mergeUserImpl x y = x

179179

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

181−argTys ist (PRef fc n)

181+argTys ist (PRef fc hls n)

182182 = case lookupTy n (tt_ctxt ist) of

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

184184 _ -> repeat Nothing

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

188188argTys _ _ = repeat Nothing

189189

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

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

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

192192 = do ms <- get

193193 case lookup n (namemap ms) of

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

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

195195 Nothing -> case n of

196196 (UN _) -> return orig

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

198− return (PRef fc n')

198+ return (PRef fc [] n')

199199tidy ist (PApp fc f args) ty

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

201201 return (PApp fc f args')

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

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

223223 _ -> [Placeholder]

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

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

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

226226 (map toPlaceholder args)

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

228228 toPlaceholder tm = tm { getTm = Placeholder }

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

233233 where subst :: PTerm -> PTerm

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

235235 | otherwise = Placeholder

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

237− | isDConName v ctxt = orig

238− subst (PRef _ _) = Placeholder

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

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

237+ | isDConName v ctxt = orig

238+ subst (PRef _ _ _) = Placeholder

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

240240 | isTConName t ctxt = Placeholder -- infer types

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

242242 subst x = x

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

281281

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

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

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

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

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

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

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

287287 nshow t = show t

288288

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

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

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

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

362− getNameFrom i used (PRef fc f)

362+ getNameFrom i used (PRef fc _ f)

363363 = case getNameHints i f of

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

365365 ns -> uniqueNameFrom (mkSupply ns) used

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

415415 newPats

416416 return (map fst newPats')

417417 where

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

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

419419 base t = t

420420

421421 nm ptm = do mptm <- elabNewPat ptm

src/Idris/Coverage.hs+13−13

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

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

2929 evalStateT (toTT (mapPT deNS timp)) 0

3030 where

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

32− case lookupNameDef n (tt_ctxt i) of

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

34− _ -> return $ P Ref n Erased

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

32+ case lookupNameDef n (tt_ctxt i) of

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

34+ _ -> return $ P Ref n Erased

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

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

3737 return $ mkApp t' args'

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

4242 put (v + 1)

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

4444

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

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

4646 deNS t = t

4747

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

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

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

113113 mkClauses parg args

114114 = do args' <- mkArg args

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

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

116116 return tm

117117 where

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

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

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

215215

216216 otherPats :: PTerm -> [PTerm]

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

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

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

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

219219 otherPats o@(PPair fc _ l r)

220220 = ops fc pairCon

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

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

232232 ops fc n xs o

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

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

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

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

236236 let tyn = getTy n (tt_ctxt i)

237237 case lookupCtxt tyn (idris_datatypes i) of

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

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

243243 getExpTm t = getTm t

244244

245245 -- put it back to its original form

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

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

247247 | ei == txt "Ex_intro"

248248 = 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])

250250 | n == pairCon

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

252252 resugar t = t

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

265265

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

267267 (pargs : _)

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

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

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

270270

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

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

279279 -- quick check for constructor equality

280280 quickEq :: PTerm -> PTerm -> Bool

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

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

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

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

284284 | length as == length as'

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

src/Idris/DSL.hs+14−14

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

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

1919dslify syn i = transform dslifyApp

2020 where

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

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

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

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

2424 dslifyApp t = t

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

2929

3030mkTTName :: FC -> Name -> PTerm

3131mkTTName fc n =

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

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

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

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

3434 [ pexp (stringC x)

3535 , pexp (mkList fc xs)]

3636 stringC = PConstant fc . Str . str

3737 intC = PConstant fc . I

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

3939 in case n of

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

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

42− , pexp (mkList fc ns)]

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

44− , pexp (stringC nm)]

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

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

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

42+ , pexp (mkList fc ns)]

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

44+ , pexp (stringC nm)]

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

4646

4747expandSugar :: DSL -> PTerm -> PTerm

4848expandSugar dsl (PLam fc n nfc ty tm)

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

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

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

7474expandSugar dsl (PIfThenElse fc c t f) =

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

120120var dsl n t i = v' i t where

121− v' i (PRef fc x) | x == n =

121+ v' i (PRef fc hl x) | x == n =

122122 case dsl_var dsl of

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

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

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

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

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

155155

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

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

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

158158 setFC fc t = t

159159

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

182182 (bs, n) <- get

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

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

185− return (PRef fc nm)

185+ return (PRef fc [] nm)

186186 db' (PApp fc t args)

187187 = do t' <- db' t

188188 args' <- mapM dbArg args

src/Idris/DeepSeq.hs+2−2

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

223223

224224instance NFData PTerm where

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

226− rnf (PRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

227− rnf (PInferRef x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

226+ rnf (PRef x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` x3 `seq` ()

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

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

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

230230 rnf (PPi x1 x2 x3 x4 x5)

src/Idris/Delaborate.hs+12−12

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

3030resugar :: IState -> PTerm -> PTerm

3131resugar ist = transform flattenDoLet . transform resugarApp

3232 where

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

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

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

3535 , basename n == sUN "ifThenElse"

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

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

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

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

3939 , basename n == sUN ">>="

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

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

4343 in case resugarApp next of

4444 PDoBlock dos -> PDoBlock (step : dos)

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

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

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

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

4848 , basename n == sUN "fromInteger"

4949 = PConstant fc (BI i)

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

5959 fixExp d = [d]

6060 flattenDoLet tm = tm

6161

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

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

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

6464 dedelay x = x

6565

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

9999 un = fileFC "(val)"

100100

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

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

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

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

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

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

105105 | n == unitCon = PTrue un IsTerm

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

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

107107 | otherwise

108108 = case lookup n (idris_metavars ist) of

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

110− _ -> PRef un n

110+ _ -> PRef un [] n

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

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

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

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

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

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

160160 | n == sigmaTy

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

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

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

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

164164 | n == pairCon = PPair un IsTerm (de env [] l) (de env [] r)

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

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

182182 mkPApp n args

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

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

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

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

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

186186

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

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

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

565565 addI x y = (x, y)

566566

567567 -- Just the ones which appear desugared in errors

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

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

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

570570 = expLike f f' && length as == length as' &&

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

src/Idris/Docs.hs+5−5

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

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

198198 updateArgs _ _ = []

199199

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

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

201201 updateRef _ pt = pt

202202

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

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

205− isSubclass _ = False

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

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

205+ isSubclass _ = False

206206

207207 prettyParameters =

208208 if any (isJust . snd) params

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

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

290290 getDInst _ = Nothing

291291

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

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

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

294294 isSubclass (PPi _ _ _ _ pt)

295295 = isSubclass pt

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

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

4444

4545

4646 replaceUnderscore' :: PTerm -> State Int PTerm

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

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

4848 replaceUnderscore' tm = return tm

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

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

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

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

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

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

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

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

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

7070

7171 let syn =

7272 syn_in { using = addToUsing (using syn_in)

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

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

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

144144 i <- getIState

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

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

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

147147 when (not isConstrained) . tclift

148148 $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))

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

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

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

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

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

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

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

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

200200 let rhs = PResolveTC (fileFC "HACK")

201201 let ty = PPi constraint cnm NoFC c con

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

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

204204 i <- getIState

205205 let conn = case con of

206− PRef _ n -> n

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

206+ PRef _ _ n -> n

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

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

209209 [(n, _)] -> n

210210 _ -> conn

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

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

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

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

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

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

229229 let margs = getMArgs ty

230230 let anames = map (\x -> sMN x "arg") [0..]

231− let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

231+ let lhs = PApp fc (PRef fc [] m) (pconst capp : lhsArgs margs anames)

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

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

234234 logLvl 1 (show (m, ty', capp, margs))

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

242242 getMArgs _ = []

243243

244244 getMeth :: [Name] -> [Name] -> Name -> PTerm

245− getMeth (m:ms) (a:as) x | x == a = PRef fc m

245+ getMeth (m:ms) (a:as) x | x == a = PRef fc [] m

246246 | otherwise = getMeth ms as x

247247

248248 lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

249− lhsArgs (IA n : xs) ns = pimp n (PRef fc n) False : lhsArgs xs ns

249+ lhsArgs (IA n : xs) ns = pimp n (PRef fc [] n) False : lhsArgs xs ns

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

251251 lhsArgs [] _ = []

252252

253253 rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

254− rhsArgs (IA n : xs) ns = pexp (PRef fc n) : rhsArgs xs ns

254+ rhsArgs (IA n : xs) ns = pexp (PRef fc [] n) : rhsArgs xs ns

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

256256 rhsArgs [] _ = []

257257

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

269269 -- to the other methods in the class

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

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

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

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

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

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

274274 | otherwise = m

275275 addC _ _ tm = tm

276276

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

303303 -> PTerm -> PTerm

304304expandMethNS syn = mapPT expand

305305 where

306− expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

306+ expand (PRef fc hls n) | n `elem` imp_methods syn = PRef fc hls $ expandNS syn n

307307 expand t = t

308308

309309-- | Find the determining parameter locations

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

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

482482

483483

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

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

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

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

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

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

488488 | Placeholder <- getTm t,

489489 n `elem` ps,

490490 not (n `elem` allNamesIn tm)

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

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

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

493493 addP _ ts = ts

494−propagateParams i ps t (PRef fc n)

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

495495 = case lookupCtxt n (idris_implicits i) of

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

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

498− _ -> PRef fc n

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

498+ _ -> PRef fc hls n

499499 where isImplicit [] n = False

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

501501 isImplicit (_ : is) n = isImplicit is n

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

734734 borrowedB b = borrowedNames env (binderTy b)

735735 borrowedNames _ _ = []

736736

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

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

738738 mkLHSapp t = t

739739

740740 decorate (NS x ns)

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

772772 where

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

774774 = any (\x -> case x of

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

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

776776 _ -> False) (map getTm args)

777777 isArg' _ = False

778778 isArg _ _ = False

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

905905 mapM_ (rec_elabDecl info EAll info) wb

906906

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

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

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

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

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

910910 pexp wval :

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

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

912912 case mpn of

913913 Nothing -> []

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

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

915915 [ pimp (sUN "A") Placeholder False

916916 , pimp (sUN "x") Placeholder False

917917 ])])

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

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

975975

976976 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

977− addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

977+ addArg (PRef fc hls f) w = PApp fc (PRef fc hls f) [pexp w]

978978

979− updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

979+ updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' hls' n') args) w

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

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

982982 return $ substMatches mvars $

983− PApp fc (PRef fc' wname)

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

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

985985 case pn of

986986 Nothing -> []

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

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

988988 updateLHS n pn wname mvars ns_in ns_in' tm w

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

990990

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

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

992992 | otherwise = Placeholder

993993

994994 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

src/Idris/Elab/Data.hs+23−23

@@ -259,15 +259,15 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

259259

260260 mkLazy (PPi pl n nfc ty sc)

261261 = let ty' = if getTyName ty

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

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

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

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

264264 pexp ty]

265265 else ty in

266266 PPi pl n nfc ty' (mkLazy sc)

267267 mkLazy t = t

268268

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

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

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

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

271271 getTyName _ = False

272272

273273

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

326326 scrutineeIdxs <- namePis False idxs

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

328328 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

329− let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

329+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC [] n) scrutineeIdxs) (PRef elimFC [] scrutineeName))

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

331331 let clauseConsElimArgs = map getPiName consTerms

332332 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

333− let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

333+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC [] arg)) clauseGeneralArgs'

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

335335 elimLog elimSig

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

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

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

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

383383 where keyOf :: PTerm -> String

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

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

385385 keyOf (PApp _ tyf _) = keyOf tyf

386386 keyOf (PType _) = "ty__"

387387 keyOf _ = "carg__"

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

446446 case findIndex (== n) oldParams of

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

448448 Just i -> (removeParamPis oldParams params tyr)

449− removeParamPis oldParams params (PRef _ n) =

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

450450 case findIndex (== n) oldParams of

451− Nothing -> (PRef elimFC n)

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

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

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

453453 removeParamPis oldParams params (PApp _ cns args) =

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

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

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

460460 [n] ->

461461 case findIndex (== n) oldParams of

462462 Nothing -> arg:replaceParamArgs args

463− Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args

463+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC [] newname}:replaceParamArgs args

464464 removeParamPis oldParams params t = t

465465

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

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

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

469469

470470 extractName :: PTerm -> [Name]

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

472− extractName _ = []

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

472+ extractName _ = []

473473

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

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

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

505505 let (_, consIdxs) = splitArgPms resTy

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

507507 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

508− applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))

508+ applyRecMotive (n,_,ty) = (sUN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC [] n))

509509 where (_, idxs) = splitArgPms ty

510510

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

512512 findRecArgs [] = []

513− findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs

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

515− findRecArgs (ty:rs) = findRecArgs rs

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

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

515+ findRecArgs (ty:rs) = findRecArgs rs

516516

517517 applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm

518− applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)

518+ applyCons tn targs = PApp elimFC (PRef elimFC [] tn) (map convertArg targs)

519519

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

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

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

522522

523523 applyMotive :: [PTerm] -> PTerm -> PTerm

524− applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])

524+ applyMotive idxs t = PApp elimFC (PRef elimFC [] motiveName) (map pexp idxs ++ [pexp t])

525525

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

527527 getPiName (name,_,_) = name

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

539539 let (_, generalIdxs') = splitArgPms resTy

540540 let generalIdxs = map pexp generalIdxs'

541541 consArgs <- namePis False args

542− let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

542+ let lhsPattern = PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

543543 let recArgs = findRecArgs consArgs

544544 let recElims = if ind then map applyRecElim recArgs else []

545− let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

545+ let rhsExpr = PApp elimFC (PRef elimFC [] cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

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

547547 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

548− applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])

548+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC [] elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC [] recCnm])

549549 where (_, idxs) = splitArgPms recTy

src/Idris/Elab/Instance.hs+12−12

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

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

6969 cs -> tclift $ tfail $ At fc

7070 (CantResolveAlts (map fst cs))

71− let constraint = PApp fc (PRef fc n) (map pexp ps)

71+ let constraint = PApp fc (PRef fc [] n) (map pexp ps)

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

7373 let emptyclass = null (class_methods ci)

7474 when (what /= EDefns || (null ds && not emptyclass)) $ do

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

8989 -- where block

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

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

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

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

9393 _ -> return []) ps

9494 ist <- getIState

9595 let pnames = nub $ map pname (concat (nub wparams)) ++

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

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

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

102102 let t_in = substMatchesShadow ips pnames t

103− mnamemap = map (\n -> (n, PRef fc (decorate ns iname n)))

103+ mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))

104104 all_meths

105105 t' = substMatchesShadow mnamemap pnames t_in in

106106 (decorate ns iname n,

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

123123

124124 -- Bring variables in instance head into scope

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

126− PRef _ n ->

126+ PRef _ _ n ->

127127 case lookupTy n (tt_ctxt ist) of

128128 [] -> Just n

129129 _ -> Nothing

130130 _ -> Nothing) ps

131131-- let lhs = PRef fc iname

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

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

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

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

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

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

135135 (map (pexp . mkMethApp) mtys)

136136

137137 logLvl 5 $ "Instance LHS " ++ show lhs ++ " " ++ show headVars

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

218218 keepDets dets t = t

219219

220220 mkMethApp (n, _, _, ty)

221− = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

221+ = lamBind 0 ty (papp fc (PRef fc [] n) (methArgs 0 ty))

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

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

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

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

226226 lamBind i _ sc = sc

227227 methArgs i (PPi (Imp _ _ _ _) n _ ty sc)

228− = PImp 0 True [] n (PRef fc (sMN i "meth")) : methArgs (i+1) sc

228+ = PImp 0 True [] n (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc

229229 methArgs i (PPi (Exp _ _ _) n _ ty sc)

230− = PExp 0 [] (sMN 0 "marg") (PRef fc (sMN i "meth")) : methArgs (i+1) sc

230+ = PExp 0 [] (sMN 0 "marg") (PRef fc [] (sMN i "meth")) : methArgs (i+1) sc

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

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

233233 methArgs i _ = []

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

237237

238238 getWParams [] = return []

239239 getWParams (p : ps)

240− | PRef _ n <- p

240+ | PRef _ _ n <- p

241241 = do ps' <- getWParams ps

242242 ctxt <- getContext

243243 case lookupP n ctxt of

244− [] -> return (pimp n (PRef fc n) True : ps')

244+ [] -> return (pimp n (PRef fc [] n) True : ps')

245245 _ -> return ps'

246246 getWParams (_ : ps) = getWParams ps

247247

src/Idris/Elab/Provider.hs+1−1

@@ -94,7 +94,7 @@ elabProvider doc info syn fc nfc what n

9494 | ProvTerm ty _ <- what ->

9595 do -- Finally add a top-level definition of the provided term

9696 elabType info syn doc [] fc [] n NoFC ty

97− elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

97+ elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc [] n) []) [] (delab i tm) []]

9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

9999 | ProvPostulate _ <- what ->

100100 do -- Add the postulate

src/Idris/Elab/Record.hs+13−13

@@ -95,7 +95,7 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

9595

9696 -- | The target for the constructor and projection functions. Also the source of the update functions.

9797 target :: PTerm

98− target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, _, p, _) <- params]

98+ target = PApp fc (PRef fc [] tyn) $ map (uncurry asPRefArg) [(p, n) | (n, _, p, _) <- params]

9999

100100 paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]

101101 paramsAndDoc = pad params paramDocs

@@ -327,10 +327,10 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

327327 -- | The left hand side of the projection function.

328328 generateLhs :: PTerm

329329 generateLhs = let args = lhsArgs index phArgs

330− in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]

330+ in PApp fc (PRef fc [] pname) [pexp (PApp fc (PRef fc [] cn) args)]

331331 where

332332 lhsArgs :: Int -> [PArg] -> [PArg]

333− lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest

333+ lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest

334334 lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)

335335 lhsArgs _ [] = []

336336

@@ -343,7 +343,7 @@ elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs f

343343

344344 -- | The right hand side of the projection function.

345345 generateRhs :: PTerm

346− generateRhs = PRef fc pname_in

346+ generateRhs = PRef fc [] pname_in

347347

348348-- | Creates and elaborates an update function.

349349-- If 'optional' is true, we will not fail if we can't elaborate the update function.

@@ -387,7 +387,7 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

387387 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $

388388 PPi expl (nsroot pname) NoFC pty $

389389 PPi expl recName NoFC sty (substInput sty)

390− where substInput = substMatches [(cname, PRef fc (nsroot pname))]

390+ where substInput = substMatches [(cname, PRef fc [] (nsroot pname))]

391391

392392 -- | The "_set" name.

393393 set_pname :: Name

@@ -401,10 +401,10 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

401401

402402 -- | The left-hand side of the update function.

403403 generateLhs :: PTerm

404− generateLhs = PApp fc (PRef fc set_pname) [pexp $ PRef fc pname_in, pexp constructorPattern]

404+ generateLhs = PApp fc (PRef fc [] set_pname) [pexp $ PRef fc [] pname_in, pexp constructorPattern]

405405 where

406406 constructorPattern :: PTerm

407− constructorPattern = PApp fc (PRef fc cn) args

407+ constructorPattern = PApp fc (PRef fc [] cn) args

408408

409409 -- | The "_in" name.

410410 pname_in :: Name

@@ -415,10 +415,10 @@ elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i option

415415

416416 -- | The right-hand side of the update function.

417417 generateRhs :: PTerm

418− generateRhs = PApp fc (PRef fc cn) (newArgs i args)

418+ generateRhs = PApp fc (PRef fc [] cn) (newArgs i args)

419419 where

420420 newArgs :: Int -> [PArg] -> [PArg]

421− newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest

421+ newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest

422422 newArgs i (x : rest) = x : (newArgs (i-1) rest)

423423 newArgs _ [] = []

424424

@@ -440,17 +440,17 @@ asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t

440440recName :: Name

441441recName = sMN 0 "rec"

442442

443−recRef = PRef emptyFC recName

443+recRef = PRef emptyFC [] recName

444444

445445projectInType :: [(Name, Name)] -> PTerm -> PTerm

446446projectInType xs = mapPT st

447447 where

448448 st :: PTerm -> PTerm

449− st (PRef fc n)

450− | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]

449+ st (PRef fc [] n)

450+ | Just pn <- lookup n xs = PApp fc (PRef fc [] pn) [pexp recRef]

451451 st t = t

452452

453453-- | Creates an PArg from a plicity and a name where the term is a PRef.

454454asPRefArg :: Plicity -> Name -> PArg

455−asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)

455+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC [] (nsroot n)

456456

src/Idris/Elab/Term.hs+58−55

@@ -289,7 +289,7 @@ elab ist info emode opts fn tm

289289 env <- get_env

290290 handleError (forceErr t' env)

291291 (elab' ina fc' t')

292− (elab' ina fc' (PApp fc (PRef fc (sUN "Force"))

292+ (elab' ina fc' (PApp fc (PRef fc [] (sUN "Force"))

293293 [pimp (sUN "t") Placeholder True,

294294 pimp (sUN "a") Placeholder True,

295295 pexp ct]))

@@ -308,7 +308,7 @@ elab ist info emode opts fn tm

308308 forceErr orig env (At _ t) = forceErr orig env t

309309 forceErr orig env t = False

310310

311− notDelay t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = False

311+ notDelay t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = False

312312 notDelay _ = True

313313

314314 local f = do e <- get_env

@@ -350,9 +350,9 @@ elab ist info emode opts fn tm

350350 do hnf_compute

351351 g <- goal

352352 case g of

353− TType _ -> elab' ina (Just fc) (PRef fc unitTy)

354− UType _ -> elab' ina (Just fc) (PRef fc unitTy)

355− _ -> elab' ina (Just fc) (PRef fc unitCon)

353+ TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

354+ UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

355+ _ -> elab' ina (Just fc) (PRef fc [] unitCon)

356356 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

357357 = do g <- goal; resolveTC False False 5 g fn ist

358358 elab' ina fc (PResolveTC fc')

@@ -360,14 +360,14 @@ elab ist info emode opts fn tm

360360 instanceArg c

361361 -- Elaborate the equality type first homogeneously, then

362362 -- heterogeneously as a fallback

363− elab' ina _ (PApp fc (PRef _ n) args)

363+ elab' ina _ (PApp fc (PRef _ _ n) args)

364364 | n == eqTy, [Placeholder, Placeholder, l, r] <- map getTm args

365365 = try (do tyn <- getNameFrom (sMN 0 "aqty")

366366 claim tyn RType

367367 movelast tyn

368− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

369− [pimp (sUN "A") (PRef NoFC tyn) True,

370− pimp (sUN "B") (PRef NoFC tyn) False,

368+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

369+ [pimp (sUN "A") (PRef NoFC [] tyn) True,

370+ pimp (sUN "B") (PRef NoFC [] tyn) False,

371371 pexp l, pexp r]))

372372 (do atyn <- getNameFrom (sMN 0 "aqty")

373373 btyn <- getNameFrom (sMN 0 "bqty")

@@ -375,9 +375,9 @@ elab ist info emode opts fn tm

375375 movelast atyn

376376 claim btyn RType

377377 movelast btyn

378− elab' ina (Just fc) (PApp fc (PRef fc eqTy)

379− [pimp (sUN "A") (PRef NoFC atyn) True,

380− pimp (sUN "B") (PRef NoFC btyn) False,

378+ elab' ina (Just fc) (PApp fc (PRef fc [] eqTy)

379+ [pimp (sUN "A") (PRef NoFC [] atyn) True,

380+ pimp (sUN "B") (PRef NoFC [] btyn) False,

381381 pexp l, pexp r]))

382382

383383 elab' ina _ (PPair fc _ l r)

@@ -385,17 +385,17 @@ elab ist info emode opts fn tm

385385 g <- goal

386386 let (tc, _) = unApply g

387387 case g of

388− TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)

388+ TType _ -> elab' ina (Just fc) (PApp fc (PRef fc [] pairTy)

389389 [pexp l,pexp r])

390− UType _ -> elab' ina (Just fc) (PApp fc (PRef fc upairTy)

390+ UType _ -> elab' ina (Just fc) (PApp fc (PRef fc [] upairTy)

391391 [pexp l,pexp r])

392392 _ -> case tc of

393393 P _ n _ | n == upairTy

394− -> elab' ina (Just fc) (PApp fc (PRef fc upairCon)

394+ -> elab' ina (Just fc) (PApp fc (PRef fc [] upairCon)

395395 [pimp (sUN "A") Placeholder False,

396396 pimp (sUN "B") Placeholder False,

397397 pexp l, pexp r])

398− _ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)

398+ _ -> elab' ina (Just fc) (PApp fc (PRef fc [] pairCon)

399399 [pimp (sUN "A") Placeholder False,

400400 pimp (sUN "B") Placeholder False,

401401 pexp l, pexp r])

@@ -409,7 +409,7 @@ elab ist info emode opts fn tm

409409-- pexp l, pexp r]))

410410-- True

411411

412− elab' ina _ (PDPair fc p l@(PRef nfc n) t r)

412+ elab' ina _ (PDPair fc p l@(PRef nfc hl n) t r)

413413 = case t of

414414 Placeholder ->

415415 do hnf_compute

@@ -418,14 +418,14 @@ elab ist info emode opts fn tm

418418 TType _ -> asType

419419 _ -> asValue

420420 _ -> asType

421− where asType = elab' ina (Just fc) (PApp fc (PRef NoFC sigmaTy)

421+ where asType = elab' ina (Just fc) (PApp fc (PRef NoFC [] sigmaTy)

422422 [pexp t,

423423 pexp (PLam fc n nfc Placeholder r)])

424− asValue = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

424+ asValue = elab' ina (Just fc) (PApp fc (PRef fc [] sigmaCon)

425425 [pimp (sMN 0 "a") t False,

426426 pimp (sMN 0 "P") Placeholder True,

427427 pexp l, pexp r])

428− elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc sigmaCon)

428+ elab' ina _ (PDPair fc p l t r) = elab' ina (Just fc) (PApp fc (PRef fc [] sigmaCon)

429429 [pimp (sMN 0 "a") t False,

430430 pimp (sMN 0 "P") Placeholder True,

431431 pexp l, pexp r])

@@ -449,8 +449,8 @@ elab ist info emode opts fn tm

449449 [x] -> elab' ina fc x

450450 _ -> tryAll (zip (map (elab' ina fc) as'')

451451 (map showHd as'')))

452− where showHd (PApp _ (PRef _ n) _) = n

453− showHd (PRef _ n) = n

452+ where showHd (PApp _ (PRef _ _ n) _) = n

453+ showHd (PRef _ _ n) = n

454454 showHd (PApp _ h _) = showHd h

455455 showHd x = NErased -- We probably should do something better than this here

456456

@@ -486,7 +486,7 @@ elab ist info emode opts fn tm

486486-- elab' (_, _, inty) (PRef fc f)

487487-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

488488-- = lift $ tfail (Msg "Typecase is not allowed")

489− elab' ec _ tm@(PRef fc n)

489+ elab' ec _ tm@(PRef fc hl n)

490490 | pattern && not reflection && not (e_qq ec) && not (e_intype ec)

491491 && isTConName n (tt_ctxt ist)

492492 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -526,8 +526,8 @@ elab ist info emode opts fn tm

526526 bindable (NS _ _) = False

527527 bindable (UN xs) = True

528528 bindable n = implicitable n

529− elab' ina _ f@(PInferRef fc n) = elab' ina (Just fc) (PApp NoFC f [])

530− elab' ina fc' tm@(PRef fc n)

529+ elab' ina _ f@(PInferRef fc hls n) = elab' ina (Just fc) (PApp NoFC f [])

530+ elab' ina fc' tm@(PRef fc hls n)

531531 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

532532 && isTConName n (tt_ctxt ist)

533533 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

@@ -541,9 +541,10 @@ elab ist info emode opts fn tm

541541 if null a'

542542 then erun fc $

543543 do apply (Var n) []

544− hl <- findHighlight n

544+ hilite <- findHighlight n

545545 solve

546− highlightSource fc hl

546+ mapM_ (uncurry highlightSource) $

547+ (fc, hilite) : map (\f -> (f, hilite)) hls

547548 else elab' ina fc' (PApp fc tm [])

548549 elab' ina _ (PLam _ _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

549550 elab' ina _ (PLam fc n nfc Placeholder sc)

@@ -646,7 +647,7 @@ elab ist info emode opts fn tm

646647 solve

647648-- elab' ina fc (PLet n Placeholder

648649-- (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

650651 rty <- goal

651652 ds <- get_deferred

652653 ctxt <- get_context

@@ -677,7 +678,7 @@ elab ist info emode opts fn tm

677678 fnTy [] ret = forget ret

678679 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

679680

680− localVar env (PRef _ x)

681+ localVar env (PRef _ _ x)

681682 = case lookup x env of

682683 Just _ -> Just x

683684 _ -> Nothing

@@ -701,7 +702,7 @@ elab ist info emode opts fn tm

701702 solve

702703 -- if f is local, just do a simple_app

703704 -- 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)

705706 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

706707 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

707708 | otherwise = implicitApp $

@@ -723,11 +724,12 @@ elab ist info emode opts fn tm

723724 if (f `elem` map fst env && length args == 1 && length args_in == 1)

724725 then -- simple app, as below

725726 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))

727728 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

728729 (show tm)

729730 solve

730− highlightSource ffc annot

731+ mapM (uncurry highlightSource) $

732+ (ffc, annot) : map (\f -> (f, annot)) hls

731733 return []

732734 else

733735 do ivs <- get_instances

@@ -753,7 +755,8 @@ elab ist info emode opts fn tm

753755 ulog <- getUnifyLog

754756

755757 annot <- findHighlight f

756− highlightSource ffc annot

758+ mapM (uncurry highlightSource) $

759+ (ffc, annot) : map (\f -> (f, annot)) hls

757760

758761 elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })

759762 [] fc False f

@@ -851,8 +854,8 @@ elab ist info emode opts fn tm

851854 tacTm (PProof _) = True

852855 tacTm _ = False

853856

854− setInjective (PRef _ n) = setinj n

855− setInjective (PApp _ (PRef _ n) _) = setinj n

857+ setInjective (PRef _ _ n) = setinj n

858+ setInjective (PApp _ (PRef _ _ n) _) = setinj n

856859 setInjective _ = return ()

857860

858861 elab' ina _ tm@(PApp fc f [arg]) =

@@ -862,7 +865,7 @@ elab ist info emode opts fn tm

862865 (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

863866 (show tm)

864867 solve

865− where headRef (PRef _ _) = True

868+ where headRef (PRef _ _ _) = True

866869 headRef (PApp _ f _) = headRef f

867870 headRef (PAlternative _ as) = all headRef as

868871 headRef _ = False

@@ -924,7 +927,7 @@ elab ist info emode opts fn tm

924927 elab' ina (Just fc) t

925928 focus valn

926929 elab' ina (Just fc) sc

927− elab' ina (Just fc) (PRef fc letn)

930+ elab' ina (Just fc) (PRef fc [] letn)

928931 solve

929932 elab' ina _ c@(PCase fc scr opts)

930933 = do attack

@@ -1163,7 +1166,7 @@ elab ist info emode opts fn tm

11631166 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

11641167

11651168 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))

11671170 isScr _ (n', b) = (n', (False, b))

11681171

11691172 caseBlock :: FC -> Name

@@ -1192,7 +1195,7 @@ elab ist info emode opts fn tm

11921195

11931196 getNmScr (n, (s, _)) = (n, s)

11941197

1195− mkarg (n, s) = (PRef fc n, s)

1198+ mkarg (n, s) = (PRef fc [] n, s)

11961199 -- may be shadowed names in the new pattern - so replace the

11971200 -- old ones with an _

11981201 -- Also, names which don't appear on the rhs should not be

@@ -1202,34 +1205,34 @@ elab ist info emode opts fn tm

12021205 = let args' = map (shadowed (allNamesIn l)) args

12031206 args'' = map (implicitable (allNamesIn r ++

12041207 keepscrName scr)) args'

1205− lhs = PApp (getFC fc l) (PRef NoFC n)

1208+ lhs = PApp (getFC fc l) (PRef NoFC [] n)

12061209 (map (mkLHSarg l) args'') in

12071210 PClause (getFC fc l) n lhs [] r []

12081211

12091212 -- Keep scrutinee available if it's just a name (this makes

12101213 -- the names in scope look better when looking at a hole on

12111214 -- the rhs of a case)

1212− keepscrName (PRef _ n) = [n]

1215+ keepscrName (PRef _ _ n) = [n]

12131216 keepscrName _ = []

12141217

12151218 mkLHSarg l (tm, True) = pexp l

12161219 mkLHSarg l (tm, False) = pexp tm

12171220

1218− shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)

1221+ shadowed new (PRef _ _ n, s) | n `elem` new = (Placeholder, s)

12191222 shadowed new t = t

12201223

1221− implicitable rhs (PRef _ n, s) | n `notElem` rhs = (Placeholder, s)

1224+ implicitable rhs (PRef _ _ n, s) | n `notElem` rhs = (Placeholder, s)

12221225 implicitable rhs t = t

12231226

12241227

12251228 getFC d (PApp fc _ _) = fc

1226− getFC d (PRef fc _) = fc

1229+ getFC d (PRef fc _ _) = fc

12271230 getFC d (PAlternative _ (x:_)) = getFC d x

12281231 getFC d x = d

12291232

12301233 insertLazy :: PTerm -> ElabD PTerm

1231− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

1232− insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

1234+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Delay" = return t

1235+ insertLazy t@(PApp _ (PRef _ _ (UN l)) _) | l == txt "Force" = return t

12331236 insertLazy (PCoerced t) = return t

12341237 insertLazy t =

12351238 do ty <- goal

@@ -1244,7 +1247,7 @@ elab ist info emode opts fn tm

12441247 mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)

12451248 mkDelay env t

12461249 = 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"))

12481251 [pexp t])

12491252

12501253

@@ -1253,7 +1256,7 @@ elab ist info emode opts fn tm

12531256 -- blowup especially where there are errors deep in large expressions.

12541257 notImplicitable (PApp _ f _) = notImplicitable f

12551258 -- TMP HACK no coercing on bind (make this configurable)

1256− notImplicitable (PRef _ n)

1259+ notImplicitable (PRef _ _ n)

12571260 | [opts] <- lookupCtxt n (idris_flags ist)

12581261 = NoImplicit `elem` opts

12591262 notImplicitable (PAlternative (ExactlyOne _) as) = any notImplicitable as

@@ -1306,7 +1309,7 @@ elab ist info emode opts fn tm

13061309 where

13071310 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

13081311 addImplBound ist (map fst env)

1309− (PApp fc (PRef fc n) [pexp (PCoerced t)])

1312+ (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

13101313

13111314 -- | Elaborate the arguments to a function

13121315 elabArgs :: IState -- ^ The current Idris state

@@ -1369,8 +1372,8 @@ elab ist info emode opts fn tm

13691372pruneAlt :: [PTerm] -> [PTerm]

13701373pruneAlt xs = map prune xs

13711374 where

1372− prune (PApp fc1 (PRef fc2 f) as)

1373− = PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)

1375+ prune (PApp fc1 (PRef fc2 hls f) as)

1376+ = PApp fc1 (PRef fc2 hls f) (fmap (fmap (choose f)) as)

13741377 prune t = t

13751378

13761379 choose f (PAlternative a as)

@@ -1383,7 +1386,7 @@ pruneAlt xs = map prune xs

13831386 choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)

13841387 choose f t = t

13851388

1386− headIs f (PApp _ (PRef _ f') _) = f == f'

1389+ headIs f (PApp _ (PRef _ _ f') _) = f == f'

13871390 headIs f (PApp _ f' _) = headIs f f'

13881391 headIs f _ = True -- keep if it's not an application

13891392

@@ -1400,7 +1403,7 @@ pruneByType env t c as

14001403 | Just n <- getName t,

14011404 n `elem` env = Just t

14021405 | otherwise = locallyBound ts

1403− getName (PRef _ n) = Just n

1406+ getName (PRef _ _ n) = Just n

14041407 getName (PApp _ f _) = getName f

14051408 getName (PHidden t) = getName t

14061409 getName _ = Nothing

@@ -1417,8 +1420,8 @@ pruneByType env (P _ n _) ctxt as

14171420 _ -> asV

14181421 _ -> as'

14191422 where

1420− headIs var f (PRef _ f') = typeHead var f f'

1421− headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'

1423+ headIs var f (PRef _ _ f') = typeHead var f f'

1424+ headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

14221425 headIs var f (PApp _ f' _) = headIs var f f'

14231426 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

14241427 headIs var f (PHidden t) = headIs var f t

src/Idris/Elab/Transform.hs+1−1

@@ -49,7 +49,7 @@ import Data.List.Split (splitOn)

4949import Util.Pretty(pretty, text)

5050

5151elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)

52−elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

52+elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

src/Idris/Elab/Utils.hs+1−1

@@ -129,7 +129,7 @@ decorateid decorate (PClauses f o n cs)

129129 dc (PWith fc n t as w pn ds)

130130 = PWith fc (decorate n) (dappname t) as w pn

131131 (map (decorateid decorate) ds)

132− dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

132+ dappname (PApp fc (PRef fc' hl n) as) = PApp fc (PRef fc' hl (decorate n)) as

133133 dappname t = t

134134

135135

src/Idris/Elab/Value.hs+4−4

@@ -121,15 +121,15 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

121121-- (as a default numeric tye), then printing it as any Showable thing

122122elabExec :: FC -> PTerm -> PTerm

123123elabExec fc tm = runtm (PAlternative FirstSuccess

124− [printtm (PApp fc (PRef fc (sUN "the"))

124+ [printtm (PApp fc (PRef fc [] (sUN "the"))

125125 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

126126 tm,

127127 printtm tm

128128 ])

129129 where

130− runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

131− printtm t = PApp fc (PRef fc (sUN "printLn"))

132− [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

130+ runtm t = PApp fc (PRef fc [] (sUN "run__IO")) [pexp t]

131+ printtm t = PApp fc (PRef fc [] (sUN "printLn"))

132+ [pimp (sUN "ffi") (PRef fc [] (sUN "FFI_C")) False, pexp t]

133133

134134elabREPL :: ElabInfo -> ElabMode -> PTerm -> Idris (Term, Type)

135135elabREPL info aspat tm

src/Idris/ElabDecls.hs+2−2

@@ -68,8 +68,8 @@ recinfo = EInfo [] emptyContext id Nothing Nothing elabDecl'

6868-- | Return the elaborated term which calls 'main'

6969elabMain :: Idris Term

7070elabMain = do (m, _) <- elabVal recinfo ERHS

71− (PApp fc (PRef fc (sUN "run__IO"))

72− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

71+ (PApp fc (PRef fc [] (sUN "run__IO"))

72+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

7373 return m

7474 where fc = fileFC "toplevel"

7575

src/Idris/ElabQuasiquote.hs+1−1

@@ -163,7 +163,7 @@ extractUnquotes n (PQuasiquote tm goal)

163163 = fmap (\(tm', ex) -> (PQuasiquote tm' goal, ex)) $ extractUnquotes (n+1) tm

164164extractUnquotes n (PUnquote tm)

165165 | n == 0 = do n <- getNameFrom (sMN 0 "unquotation")

166− return (PRef (fileFC "(unquote)") n, [(n, tm)])

166+ return (PRef (fileFC "(unquote)") [] n, [(n, tm)])

167167 | otherwise = fmap (\(tm', ex) -> (PUnquote tm', ex)) $

168168 extractUnquotes (n-1) tm

169169extractUnquotes n (PRunElab fc tm ns)

src/Idris/Error.hs+2−2

@@ -88,8 +88,8 @@ getErrSpan _ = emptyFC

8888-- | Issue a warning on "with"-terms whose namespace is empty or nonexistent

8989warnDisamb :: IState -> PTerm -> Idris ()

9090warnDisamb ist (PQuote _) = return ()

91−warnDisamb ist (PRef _ _) = return ()

92−warnDisamb ist (PInferRef _ _) = return ()

91+warnDisamb ist (PRef _ _ _) = return ()

92+warnDisamb ist (PInferRef _ _ _) = return ()

9393warnDisamb ist (PPatvar _ _) = return ()

9494warnDisamb ist (PLam _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

9595warnDisamb ist (PPi _ _ _ t b) = warnDisamb ist t >> warnDisamb ist b

src/Idris/IBC.hs+13−9

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 114

43+ibcVersion = 115

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -1522,12 +1522,14 @@ instance Binary PTerm where

15221522 = case x of

15231523 PQuote x1 -> do putWord8 0

15241524 put x1

1525− PRef x1 x2 -> do putWord8 1

1526− put x1

1527− put x2

1528− PInferRef x1 x2 -> do putWord8 2

1529− put x1

1530− put x2

1525+ PRef x1 x2 x3 -> do putWord8 1

1526+ put x1

1527+ put x2

1528+ put x3

1529+ PInferRef x1 x2 x3 -> do putWord8 2

1530+ put x1

1531+ put x2

1532+ put x3

15311533 PPatvar x1 x2 -> do putWord8 3

15321534 put x1

15331535 put x2

@@ -1663,10 +1665,12 @@ instance Binary PTerm where

16631665 return (PQuote x1)

16641666 1 -> do x1 <- get

16651667 x2 <- get

1666− return (PRef x1 x2)

1668+ x3 <- get

1669+ return (PRef x1 x2 x3)

16671670 2 -> do x1 <- get

16681671 x2 <- get

1669− return (PInferRef x1 x2)

1672+ x3 <- get

1673+ return (PInferRef x1 x2 x3)

16701674 3 -> do x1 <- get

16711675 x2 <- get

16721676 return (PPatvar x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -288,8 +288,8 @@ loadDocs ist n

288288-- TODO: Remove unnecessary cases

289289extractPTermNames :: PTerm -- ^ Where to extract names from

290290 -> [Name] -- ^ Extracted names

291−extractPTermNames (PRef _ n) = [n]

292−extractPTermNames (PInferRef _ n) = [n]

291+extractPTermNames (PRef _ _ n) = [n]

292+extractPTermNames (PInferRef _ _ n) = [n]

293293extractPTermNames (PPatvar _ n) = [n]

294294extractPTermNames (PLam _ n _ p1 p2) = n : concatMap extract [p1, p2]

295295extractPTermNames (PPi _ n _ p1 p2) = n : concatMap extract [p1, p2]

src/Idris/Interactive.hs+5−5

@@ -112,7 +112,7 @@ addMissing fn updatefile l n

112112 else iPrintResult extras

113113 where showPat = show . stripNS

114114 stripNS tm = mapPT dens tm where

115− dens (PRef fc n) = PRef fc (nsroot n)

115+ dens (PRef fc hls n) = PRef fc hls (nsroot n)

116116 dens t = t

117117

118118 nsroot (NS n _) = nsroot n

@@ -120,7 +120,7 @@ addMissing fn updatefile l n

120120 nsroot n = n

121121

122122 getAppName (PApp _ r _) = getAppName r

123− getAppName (PRef _ r) = r

123+ getAppName (PRef _ _ r) = r

124124 getAppName _ = n

125125

126126 makeIndent ind | ".lidr" `isSuffixOf` fn = '>' : ' ' : replicate (ind-2) ' '

@@ -178,10 +178,10 @@ doProofSearch fn updatefile rec l n hints (Just depth)

178178 let fc = fileFC fn

179179 let body t = PProof [Try (TSeq Intros (ProofSearch rec False depth t hints))

180180 (ProofSearch rec False depth t hints)]

181− let def = PClause fc mn (PRef fc mn) [] (body top) []

181+ let def = PClause fc mn (PRef fc [] mn) [] (body top) []

182182 newmv <- idrisCatch

183183 (do elabDecl' EAll recinfo (PClauses fc [] mn [def])

184− (tm, ty) <- elabVal recinfo ERHS (PRef fc mn)

184+ (tm, ty) <- elabVal recinfo ERHS (PRef fc [] mn)

185185 ctxt <- getContext

186186 i <- getIState

187187 return . flip displayS "" . renderPretty 1.0 80 $

@@ -204,7 +204,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

204204 dropCtxt _ t = t

205205

206206 stripNS tm = mapPT dens tm where

207− dens (PRef fc n) = PRef fc (nsroot n)

207+ dens (PRef fc hls n) = PRef fc hls (nsroot n)

208208 dens t = t

209209

210210 nsroot (NS n _) = nsroot n

src/Idris/ParseData.hs+1−1

@@ -218,7 +218,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

218218 fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

219219 cons <- sepBy1 (simpleConstructor syn) (reservedOp "|")

220220 terminator

221− let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

221+ let conty = mkPApp fc (PRef fc [] tyn) (map (PRef fc []) args)

222222 cons' <- mapM (\ (doc, argDocs, x, xfc, cargs, cfc, fs) ->

223223 do let cty = bindArgs cargs conty

224224 return (doc, argDocs, x, xfc, cty, cfc, fs)) cons

src/Idris/ParseExpr.hs+47−41

@@ -174,9 +174,9 @@ extension syn ns rules =

174174 _ -> n

175175

176176 update :: [(Name, SynMatch)] -> PTerm -> PTerm

177− update ns (PRef fc n) = case lookup n ns of

178− Just (SynTm t) -> t

179− _ -> PRef fc n

177+ update ns (PRef fc hls n) = case lookup n ns of

178+ Just (SynTm t) -> t

179+ _ -> PRef fc hls n

180180 update ns (PLam fc n nfc ty sc)

181181 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)

182182 update ns (PPi p n fc ty sc)

@@ -346,7 +346,7 @@ simpleExpr syn =

346346 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

347347 return (PMetavar (FC f (l, c-1) end) x)

348348 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

349− <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc (SN $ ElimN t))

349+ <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

350350 <|> proofExpr syn

351351 <|> tacticsExpr syn

352352 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

@@ -358,16 +358,16 @@ simpleExpr syn =

358358 fc <- getFC

359359 return (modifyConst syn fc (PConstant cfc c))

360360 <|> do symbol "'"; fc <- getFC; str <- fst <$> name

361− return (PApp fc (PRef fc (sUN "Symbol_"))

361+ return (PApp fc (PRef fc [] (sUN "Symbol_"))

362362 [pexp (PConstant NoFC (Str (show str)))])

363363 <|> do (x, fc) <- fnName

364364 if inPattern syn

365− then option (PRef fc x)

365+ then option (PRef fc [fc] x)

366366 (do reservedOp "@"

367367 s <- simpleExpr syn

368368 fcIn <- getFC

369369 return (PAs fcIn x s))

370− else return (PRef fc x)

370+ else return (PRef fc [fc] x)

371371 <|> idiom syn

372372 <|> listExpr syn

373373 <|> alt syn

@@ -415,14 +415,14 @@ bracketed' open syn =

415415 fc <- getFC

416416 r <- expr syn

417417 lchar ')'

418− return (PDPair fc TypeOrTerm (PRef lnfc ln) lty r))

418+ return (PDPair fc TypeOrTerm (PRef lnfc [] ln) lty r))

419419 <|> try (do fc <- getFC; o <- operator; e <- expr syn; lchar ')'

420420 -- No prefix operators! (bit of a hack here...)

421421 if (o == "-" || o == "!")

422422 then fail "minus not allowed in section"

423423 else return $ PLam fc (sMN 1000 "ARG") NoFC Placeholder

424− (PApp fc (PRef fc (sUN o)) [pexp (PRef fc (sMN 1000 "ARG")),

425− pexp e]))

424+ (PApp fc (PRef fc [] (sUN o)) [pexp (PRef fc [] (sMN 1000 "ARG")),

425+ pexp e]))

426426 <|> try (do l <- simpleExpr syn

427427 op <- option Nothing (do o <- operator

428428 lchar ')'

@@ -431,8 +431,8 @@ bracketed' open syn =

431431 case op of

432432 Nothing -> bracketedExpr syn l

433433 Just o -> return $ PLam fc0 (sMN 1000 "ARG") NoFC Placeholder

434− (PApp fc0 (PRef fc0 (sUN o)) [pexp l,

435− pexp (PRef fc0 (sMN 1000 "ARG"))]))

434+ (PApp fc0 (PRef fc0 [] (sUN o)) [pexp l,

435+ pexp (PRef fc0 [] (sMN 1000 "ARG"))]))

436436 <|> do l <- expr syn

437437 bracketedExpr syn l

438438

@@ -465,7 +465,7 @@ modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

465465modifyConst syn fc (PConstant inFC (BI x))

466466 | not (inPattern syn)

467467 = PAlternative FirstSuccess

468− (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

468+ (PApp fc (PRef fc [] (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

469469 : consts)

470470 | otherwise = PAlternative FirstSuccess consts

471471 where

@@ -580,7 +580,7 @@ app syn = do f <- simpleExpr syn

580580 return (PLet fc (sMN 0 "match") NoFC

581581 f

582582 (PMatchApp fc ff)

583− (PRef fc (sMN 0 "match")))

583+ (PRef fc [] (sMN 0 "match")))

584584 <?> "matching application expression") <|> (do

585585 fc <- getFC

586586 i <- get

@@ -589,17 +589,17 @@ app syn = do f <- simpleExpr syn

589589 [] -> return f

590590 _ -> return (flattenFromInt fc f args))

591591 <?> "function application"

592− where

592+ where

593593 -- bit of a hack to deal with the situation where we're applying a

594594 -- literal to an argument, which we may want for obscure applications

595595 -- of fromInteger, and this will help disambiguate better.

596596 -- We know, at least, it won't be one of the constants!

597597 flattenFromInt fc (PAlternative x alts) args

598598 | Just i <- getFromInt alts

599− = PApp fc (PRef fc (sUN "fromInteger")) (i : args)

599+ = PApp fc (PRef fc [] (sUN "fromInteger")) (i : args)

600600 flattenFromInt fc f args = PApp fc f args

601601

602− getFromInt ((PApp _ (PRef _ n) [a]) : _) | n == sUN "fromInteger" = Just a

602+ getFromInt ((PApp _ (PRef _ _ n) [a]) : _) | n == sUN "fromInteger" = Just a

603603 getFromInt (_ : xs) = getFromInt xs

604604 getFromInt _ = Nothing

605605

@@ -628,10 +628,10 @@ ImplicitArg ::=

628628-}

629629implicitArg :: SyntaxInfo -> IdrisParser PArg

630630implicitArg syn = do lchar '{'

631− n <- fst <$> name

631+ (n, nfc) <- name

632632 fc <- getFC

633− v <- option (PRef fc n) (do lchar '='

634− expr syn)

633+ v <- option (PRef nfc [nfc] n) (do lchar '='

634+ expr syn)

635635 lchar '}'

636636 return (pimp n v True)

637637 <?> "implicit function argument"

@@ -735,14 +735,14 @@ recordType syn =

735735 case rec of

736736 Nothing ->

737737 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

738− (applyAll fc fields (PRef fc (sMN 0 "fldx"))))

738+ (applyAll fc fields (PRef fc [] (sMN 0 "fldx"))))

739739 Just v -> return (applyAll fc fields v)

740740 Right fields ->

741741 case rec of

742742 Nothing ->

743743 return (PLam fc (sMN 0 "fldx") NoFC Placeholder

744− (getAll fc (reverse fields)

745− (PRef fc (sMN 0 "fldx"))))

744+ (getAll fc (reverse fields)

745+ (PRef fc [] (sMN 0 "fldx"))))

746746 Just v -> return (getAll fc (reverse fields) v)

747747

748748 <?> "record setting expression"

@@ -766,17 +766,17 @@ recordType syn =

766766 applyAll fc [] x = x

767767 applyAll fc ((ns, e) : es) x

768768 = applyAll fc es (doUpdate fc ns e x)

769−

769+

770770 doUpdate fc [n] e get

771− = PApp fc (PRef fc (mkType n)) [pexp e, pexp get]

771+ = PApp fc (PRef fc [] (mkType n)) [pexp e, pexp get]

772772 doUpdate fc (n : ns) e get

773− = PApp fc (PRef fc (mkType n))

774− [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),

773+ = PApp fc (PRef fc [] (mkType n))

774+ [pexp (doUpdate fc ns e (PApp fc (PRef fc [] n) [pexp get])),

775775 pexp get]

776776

777777 getAll :: FC -> [Name] -> PTerm -> PTerm

778− getAll fc [n] e = PApp fc (PRef fc n) [pexp e]

779− getAll fc (n:ns) e = PApp fc (PRef fc n) [pexp (getAll fc ns e)]

778+ getAll fc [n] e = PApp fc (PRef fc [] n) [pexp e]

779+ getAll fc (n:ns) e = PApp fc (PRef fc [] n) [pexp (getAll fc ns e)]

780780

781781

782782-- | Creates setters for record types on necessary functions

@@ -838,7 +838,7 @@ lambda syn = do lchar '\\' <?> "lambda expression"

838838 pmList [] sc = sc

839839 pmList ((i, (fc, x)) : xs) sc

840840 = PLam fc (sMN i "lamp") NoFC Placeholder

841− (PCase fc (PRef fc (sMN i "lamp"))

841+ (PCase fc (PRef fc [] (sMN i "lamp"))

842842 [(x, pmList xs sc)])

843843 lambdaTail :: IdrisParser PTerm

844844 lambdaTail = impossible <|> symbol "=>" *> expr syn

@@ -859,7 +859,7 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"

859859 highlightP kw AnnKeyword

860860 highlightP kw' AnnKeyword

861861 return (PRewrite fc

862− (PApp fc (PRef fc (sUN "sym")) [pexp prf]) sc

862+ (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc

863863 giving)

864864 <?> "term rewrite expression"

865865

@@ -882,7 +882,7 @@ let_ syn = try (do kw <- reservedFC "let"

882882 return (buildLets ls sc))

883883 <?> "let binding"

884884 where buildLets [] sc = sc

885− buildLets ((fc, PRef nfc n, ty, v, []) : ls) sc

885+ buildLets ((fc, PRef nfc [] n, ty, v, []) : ls) sc

886886 = PLet fc n nfc ty v (buildLets ls sc)

887887 buildLets ((fc, pat, ty, v, alts) : ls) sc

888888 = PCase fc v ((pat, buildLets ls sc) : alts)

@@ -1144,20 +1144,26 @@ listExpr syn = do (FC f (l, c) _) <- getFC

11441144 qs <- sepBy1 (do_ syn) (lchar ',')

11451145 lchar ']'

11461146 return (PDoBlock (map addGuard qs ++

1147− [DoExp fc (PApp fc (PRef fc (sUN "return"))

1147+ [DoExp fc (PApp fc (PRef fc [] (sUN "return"))

11481148 [pexp x])]))) <|>

1149− (do xs <- many ((lchar ',' <?> "list element") *> expr syn)

1149+ (do xs <- many (do (FC fn (sl, sc) _) <- getFC

1150+ lchar ',' <?> "list element"

1151+ let commaFC = FC fn (sl, sc) (sl, sc + 1)

1152+ elt <- expr syn

1153+ return (elt, commaFC))

1154+ (FC fn (sl, sc) _) <- getFC

11501155 lchar ']' <?> "end of list expression"

1151− return (mkList fc (x:xs))))

1156+ let rbrackFC = FC fn (sl, sc) (sl, sc+1)

1157+ return (mkList fc rbrackFC ((x, (FC f (l, c) (l, c+1))) : xs))))

11521158 <?> "list expression"

11531159 where

11541160 mkNil :: FC -> PTerm

1155− mkNil fc = PRef fc (sUN "Nil")

1156− mkList :: FC -> [PTerm] -> PTerm

1157− mkList fc [] = PRef NoFC (sUN "Nil")

1158− mkList fc (x : xs) = PApp fc (PRef NoFC (sUN "::")) [pexp x, pexp (mkList fc xs)]

1161+ mkNil fc = PRef fc [fc] (sUN "Nil")

1162+ mkList :: FC -> FC -> [(PTerm, FC)] -> PTerm

1163+ mkList errFC nilFC [] = PRef nilFC [nilFC] (sUN "Nil")

1164+ mkList errFC nilFC ((x, fc) : xs) = PApp errFC (PRef fc [fc] (sUN "::")) [pexp x, pexp (mkList errFC nilFC xs)]

11591165 addGuard :: PDo -> PDo

1160− addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc (sUN "guard"))

1166+ addGuard (DoExp fc e) = DoExp fc (PApp fc (PRef fc [] (sUN "guard"))

11611167 [pexp e])

11621168 addGuard x = x

11631169

@@ -1216,7 +1222,7 @@ do_ syn

12161222 option (DoBind fc i ifc e)

12171223 (do lchar '|'

12181224 ts <- sepBy1 (do_alt syn) (lchar '|')

1219− return (DoBindP fc (PRef ifc i) e ts)))

1225+ return (DoBindP fc (PRef ifc [ifc] i) e ts)))

12201226 <|> try (do i <- expr' syn

12211227 symbol "<-"

12221228 fc <- getFC

src/Idris/ParseOps.hs+5−5

@@ -35,11 +35,11 @@ import Debug.Trace

3535-- using pre-build and user-defined operator/fixity declarations

3636table :: [FixDecl] -> OperatorTable IdrisParser PTerm

3737table fixes

38− = [[prefix "-" (\fc x -> PApp fc (PRef fc (sUN "negate")) [pexp x])]] ++

38+ = [[prefix "-" (\fc x -> PApp fc (PRef fc [fc] (sUN "negate")) [pexp x])]] ++

3939 toTable (reverse fixes) ++

4040 [[backtick],

4141 [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

42− [binary "=" (\fc x y -> PApp fc (PRef fc eqTy) [pexp x, pexp y]) AssocLeft],

42+ [binary "=" (\fc x y -> PApp fc (PRef fc [fc] eqTy) [pexp x, pexp y]) AssocLeft],

4343 [nofixityoperator]]

4444 where

4545 flatten :: PTerm -> PTerm -- flatten application

@@ -52,9 +52,9 @@ toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

5252toTable fs = map (map toBin)

5353 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

5454 where toBin (Fix (PrefixN _) op) = prefix op

55− (\fc x -> PApp fc (PRef fc (sUN op)) [pexp x])

55+ (\fc x -> PApp fc (PRef fc [] (sUN op)) [pexp x])

5656 toBin (Fix f op)

57− = binary op (\fc x y -> PApp fc (PRef fc (sUN op)) [pexp x,pexp y]) (assoc f)

57+ = binary op (\fc x y -> PApp fc (PRef fc [] (sUN op)) [pexp x,pexp y]) (assoc f)

5858 assoc (Infixl _) = AssocLeft

5959 assoc (Infixr _) = AssocRight

6060 assoc (InfixN _) = AssocNone

@@ -79,7 +79,7 @@ backtick = Infix (do indentPropHolds gtProp

7979 lchar '`'; (n, fc) <- fnName

8080 lchar '`'

8181 indentPropHolds gtProp

82− return (\x y -> PApp fc (PRef fc n) [pexp x, pexp y])) AssocNone

82+ return (\x y -> PApp fc (PRef fc [fc] n) [pexp x, pexp y])) AssocNone

8383

8484-- | Operator without fixity (throws an error)

8585nofixityoperator :: Operator IdrisParser PTerm

src/Idris/Parser.hs+7−7

@@ -324,8 +324,8 @@ syntaxRule syn

324324 uniquifyBinders userNames = fixBind []

325325 where

326326 fixBind :: [(Name, Name)] -> PTerm -> IdrisParser PTerm

327− fixBind rens (PRef fc n) | Just n' <- lookup n rens =

328− return $ PRef fc n'

327+ fixBind rens (PRef fc hls n) | Just n' <- lookup n rens =

328+ return $ PRef fc hls n'

329329 fixBind rens (PPatvar fc n) | Just n' <- lookup n rens =

330330 return $ PPatvar fc n'

331331 fixBind rens (PLam fc n nfc ty body)

@@ -735,7 +735,7 @@ instance_ syn = do (doc, argDocs)

735735 let cs' = [(c, ty) | (c, _, ty) <- cs]

736736 (cn, cnfc) <- fnName

737737 args <- many (simpleExpr syn)

738− let sc = PApp fc (PRef cnfc cn) (map pexp args)

738+ let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

739739 let t = bindList (PPi constraint) cs sc

740740 ds <- option [] (instanceBlock syn)

741741 return [PInstance doc argDocs syn fc cs' cn cnfc args t en ds]

@@ -953,7 +953,7 @@ clause syn

953953 let capp = PLet fc (sMN 0 "match") NoFC

954954 ty

955955 (PMatchApp fc n)

956− (PRef fc (sMN 0 "match"))

956+ (PRef fc [] (sMN 0 "match"))

957957 ist <- get

958958 put (ist { lastParse = Just n })

959959 return $ PClause fc n capp [] r wheres

@@ -976,7 +976,7 @@ clause syn

976976 do terminator

977977 return ([], [])]

978978 ist <- get

979− let capp = PApp fc (PRef nfc n) [pexp l, pexp r]

979+ let capp = PApp fc (PRef nfc [nfc] n) [pexp l, pexp r]

980980 put (ist { lastParse = Just n })

981981 return $ PClause fc n capp wargs rs wheres) <|> (do

982982 popIndent

@@ -987,7 +987,7 @@ clause syn

987987 ds <- some $ fnDecl syn

988988 closeBlock

989989 ist <- get

990− let capp = PApp fc (PRef fc n) [pexp l, pexp r]

990+ let capp = PApp fc (PRef fc [] n) [pexp l, pexp r]

991991 let withs = map (fillLHSD n capp wargs) $ concat ds

992992 put (ist { lastParse = Just n })

993993 return $ PWith fc n capp wargs wval pn withs)

@@ -998,7 +998,7 @@ clause syn

998998 args <- many (try (implicitArg (syn { inPattern = True } ))

999999 <|> (fmap pexp (argExpr syn)))

10001000 wargs <- many (wExpr syn)

1001− let capp = PApp fc (PRef nfc n)

1001+ let capp = PApp fc (PRef nfc [nfc] n)

10021002 (cargs ++ args)

10031003 (do r <- rhs syn n

10041004 ist <- get

src/Idris/PartialEval.hs+3−3

@@ -206,8 +206,8 @@ mkNewPats ist d ns newname sname lhs rhs =

206206 mkClause (oldlhs, oldrhs)

207207 = let (_, as) = unApply oldlhs

208208 lhsargs = mkLHSargs [] ns as

209− lhs = PApp emptyFC (PRef emptyFC newname) lhsargs

210− rhs = PApp emptyFC (PRef emptyFC sname)

209+ lhs = PApp emptyFC (PRef emptyFC [] newname) lhsargs

210+ rhs = PApp emptyFC (PRef emptyFC [] sname)

211211 (mkRHSargs ns lhsargs) in

212212 (lhs, rhs)

213213

@@ -245,7 +245,7 @@ mkNewPats ist d ns newname sname lhs rhs =

245245mkPE_TermDecl :: IState -> Name -> Name ->

246246 [(PEArgType, Term)] -> PEDecl

247247mkPE_TermDecl ist newname sname ns

248− = let lhs = PApp emptyFC (PRef emptyFC newname) (map pexp (mkp ns))

248+ = let lhs = PApp emptyFC (PRef emptyFC [] newname) (map pexp (mkp ns))

249249 rhs = eraseImps $ delab ist (mkApp (P Ref sname Erased) (map snd ns))

250250 patdef = lookupCtxtExact sname (idris_patdefs ist)

251251 newpats = case patdef of

src/Idris/ProofSearch.hs+4−4

@@ -25,8 +25,8 @@ trivial :: (PTerm -> ElabD ()) -> IState -> ElabD ()

2525trivial = trivialHoles []

2626

2727trivialHoles :: [(Name, Int)] -> (PTerm -> ElabD ()) -> IState -> ElabD ()

28−trivialHoles ok elab ist

29− = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

28+trivialHoles ok elab ist

29+ = try' (do elab (PApp (fileFC "prf") (PRef (fileFC "prf") [] eqCon) [pimp (sUN "A") Placeholder False, pimp (sUN "x") Placeholder False])

3030 return ())

3131 (do env <- get_env

3232 g <- goal

@@ -42,7 +42,7 @@ trivialHoles ok elab ist

4242 -- anywhere but the top is okay for a hole, if holesOK set

4343 if -- all (\n -> not (n `elem` badhs)) (freeNames (binderTy b))

4444 holesOK hs (binderTy b)

45− then try' (elab (PRef (fileFC "prf") x))

45+ then try' (elab (PRef (fileFC "prf") [] x))

4646 (tryAll xs) True

4747 else tryAll xs

4848

@@ -227,7 +227,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist

227227 = do let a = getPArity (delab ist (binderTy t))

228228 tryLocalArg d locs tys n a

229229

230− tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") n)

230+ tryLocalArg d locs tys n 0 = elab (PRef (fileFC "prf") [] n)

231231 tryLocalArg d locs tys n i

232232 = simple_app False (tryLocalArg d locs tys n (i - 1))

233233 (psRec True d locs tys) "proof search local apply"

src/Idris/Prover.hs+3−3

@@ -310,7 +310,7 @@ elabloop fn d prompt prf e prev h env

310310 return (False, prev, e, False, prf, env, Right $ iRenderResult (text "TT:" <+> pprintTT [] tm))

311311 EEval tm -> do (d', st', done, prf', go) <- evalTerm e prf tm

312312 return (d', prev, st', done, prf', env, go)

313− ECheck (PRef _ n) ->

313+ ECheck (PRef _ _ n) ->

314314 do (d', st', done, prf', go) <- checkNameType e prf n

315315 return (d', prev, st', done, prf', env, go)

316316 ECheck tm -> do (d', st', done, prf', go) <- checkType e prf tm

@@ -331,7 +331,7 @@ elabloop fn d prompt prf e prev h env

331331 return (True, LetStep:prev, e, False, prf ++ [step], (i, ty', tm' ) : env, Right (iPrintResult ""))

332332 DoLet fc i ifc ty expr ->

333333 do (tm, ty) <- elabVal recinfo ERHS

334− (PApp NoFC (PRef NoFC (sUN "the"))

334+ (PApp NoFC (PRef NoFC [] (sUN "the"))

335335 [ pexp (inLets ist env ty)

336336 , pexp (inLets ist env expr)

337337 ])

@@ -417,7 +417,7 @@ ploop fn d prompt prf e h

417417 when (not (null hs)) $ ifail "Incomplete proof"

418418 iputStrLn "Proof completed!"

419419 return (False, e, True, prf, Right $ iPrintResult "")

420− Success (TCheck (PRef _ n)) -> checkNameType e prf n

420+ Success (TCheck (PRef _ _ n)) -> checkNameType e prf n

421421 Success (TCheck t) -> checkType e prf t

422422 Success (TEval t) -> evalTerm e prf t

423423 Success (TDocStr x) -> docStr e prf x

src/Idris/Providers.hs+1−1

@@ -10,7 +10,7 @@ import Idris.Error

1010-- | Wrap a type provider in the type of type providers

1111providerTy :: FC -> PTerm -> PTerm

1212providerTy fc tm

13− = PApp fc (PRef fc $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]

13+ = PApp fc (PRef fc [] $ sNS (sUN "Provider" ) ["Providers", "Prelude"]) [PExp 0 [] (sMN 0 "pvarg") tm]

1414

1515ioret :: Name

1616ioret = sUN "prim_io_return"

src/Idris/REPL.hs+6−6

@@ -345,7 +345,7 @@ runIdeModeCommand h id orig fn mods (IdeMode.TypeOf name) =

345345 case splitName name of

346346 Left err -> iPrintError err

347347 Right n -> process "(idemode)"

348− (Check (PRef (FC "(idemode)" (0,0) (0,0)) n))

348+ (Check (PRef (FC "(idemode)" (0,0) (0,0)) [] n))

349349runIdeModeCommand h id orig fn mods (IdeMode.DocsFor name w) =

350350 case parseConst orig name of

351351 Success c -> process "(idemode)" (DocStr (Right c) (howMuch w))

@@ -581,7 +581,7 @@ idemodeProcess fn (NewDefn decls) = do process fn (NewDefn decls)

581581 iPrintResult "defined"

582582idemodeProcess fn (Undefine n) = process fn (Undefine n)

583583idemodeProcess fn (ExecVal t) = process fn (ExecVal t)

584−idemodeProcess fn (Check (PRef x n)) = process fn (Check (PRef x n))

584+idemodeProcess fn (Check (PRef x hls n)) = process fn (Check (PRef x hls n))

585585idemodeProcess fn (Check t) = process fn (Check t)

586586idemodeProcess fn (Core t) = process fn (Core t)

587587idemodeProcess fn (DocStr n w) = process fn (DocStr n w)

@@ -893,7 +893,7 @@ process fn (ExecVal t)

893893 prettyIst ist (delab ist ty'))

894894 iPrintTermWithType resOut tyOut

895895

896−process fn (Check (PRef _ n))

896+process fn (Check (PRef _ _ n))

897897 = do ctxt <- getContext

898898 ist <- getIState

899899 let ppo = ppOptionIst ist

@@ -1173,8 +1173,8 @@ process fn (Compile codegen f)

11731173 let iface = Interface `elem` opts

11741174 m <- if iface then return Nothing else

11751175 do (m', _) <- elabVal recinfo ERHS

1176− (PApp fc (PRef fc (sUN "run__IO"))

1177− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1176+ (PApp fc (PRef fc [] (sUN "run__IO"))

1177+ [pexp $ PRef fc [] (sNS (sUN "main") ["Main"])])

11781178 return (Just m')

11791179 ir <- compile codegen f m

11801180 i <- getIState

@@ -1345,7 +1345,7 @@ process fn (TransformInfo n)

13451345-- iputStrLn "---------------"

13461346-- showTrans i ts

13471347

1348−process fn (PPrint fmt width (PRef _ n))

1348+process fn (PPrint fmt width (PRef _ _ n))

13491349 = do outs <- pprintDef n

13501350 iPrintResult =<< renderExternal fmt width (vsep outs)

13511351

src/Idris/REPLParser.hs+1−1

@@ -304,7 +304,7 @@ cmd_execute name = do

304304 tm <- option maintm (P.fullExpr defaultSyntax)

305305 return (Right (Execute tm))

306306 where

307− maintm = PRef (fileFC "(repl)") (sNS (sUN "main") ["Main"])

307+ maintm = PRef (fileFC "(repl)") [] (sNS (sUN "main") ["Main"])

308308

309309

310310cmd_dynamic :: String -> P.IdrisParser (Either String Command)