ec87a69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some effort at reporting line numbers of errors (top level of decl only)

commitec87a69abf71e58a4c7e5a12ebc480c303686844 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 22 Oct 2011, 23:43 (15 years ago) parent2c4ff83

10 files changed+148−93

compare with master

unifiedsplit

impl-paper/Makefile+2−1 impl-paper/impldtp.tex+2 impl-paper/syntax.tex+1 src/Core/Elaborate.hs+8 src/Core/TT.hs+13−1 src/Idris/AbsSyntax.hs+37−31 src/Idris/ElabDecls.hs+40−35 src/Idris/Error.hs+1 src/Idris/Parser.hs+43−24 src/Idris/Primitives.hs+1−1

impl-paper/Makefile+2−1

@@ -3,7 +3,8 @@ PAPER = impldtp

33all: ${PAPER}.pdf

55TEXFILES = ${PAPER}.tex intro.tex conclusions.tex overview.tex hll.tex\

6− typechecking.tex proofstate.tex elaboration.tex compiling.tex

6+ typechecking.tex proofstate.tex elaboration.tex compiling.tex\

7+ syntax.tex

89DIAGS =

910

impl-paper/impldtp.tex+2

@@ -93,6 +93,8 @@ KY16 9SX

9393

9494\input{compiling.tex}

9595

96+\input{syntax.tex}

97+

9698\input{conclusions.tex}

9799

98100\bibliographystyle{acmtrans}

impl-paper/syntax.texnew file+1

@@ -0,0 +1 @@

1+\section{Syntactic Sugar}

src/Core/Elaborate.hs+8

@@ -29,6 +29,14 @@ data Command = Theorem Name Raw

2929

3030type Elab a = StateT (ProofState, String) TC a

3131

32+erun :: FC -> Elab a -> Elab a

33+erun f elab = do s <- get

34+ case runStateT elab s of

35+ OK (a, s') -> do put s'

36+ return a

37+ Error (At f e) -> lift $ Error (At f e)

38+ Error e -> lift $ Error (At f e)

39+

3240runElab :: Elab a -> ProofState -> TC (a, (ProofState, String))

3341runElab e ps = runStateT e (ps, "")

3442

src/Core/TT.hs+13−1

@@ -23,8 +23,16 @@ data Option = SetInSet

2323 | CheckConv

2424 deriving Eq

2525

26+data FC = FC { fc_fname :: String,

27+ fc_line :: Int }

28+ deriving Eq

29+

30+instance Show FC where

31+ show (FC f l) = f ++ ":" ++ show l

32+

2633data Err = Msg String

2734 | CantUnify Term Term Err

35+ | At FC Err

2836 deriving Eq

2937

3038instance Show Err where

@@ -36,7 +44,7 @@ data TC a = OK a

3644

3745instance Show a => Show (TC a) where

3846 show (OK x) = show x

39− show (Error str) = "Error: " ++ (show str)

47+ show (Error str) = "Error: " ++ show str

4048

4149-- at some point, this instance should also carry type checking options

4250-- (e.g. Set:Set)

@@ -51,6 +59,10 @@ instance Monad TC where

5159tfail :: Err -> TC a

5260tfail e = Error e

5361

62+trun :: FC -> TC a -> TC a

63+trun fc (OK a) = OK a

64+trun fc (Error e) = Error (At fc e)

65+

5466instance MonadPlus TC where

5567 mzero = fail "Unknown error"

5668 (OK x) `mplus` _ = OK x

src/Idris/AbsSyntax.hs+37−31

@@ -56,11 +56,13 @@ getName = do i <- get;

5656 put (i { idris_name = idx + 1 })

5757 return idx

5858

59−checkUndefined :: Name -> Idris ()

60−checkUndefined n = do i <- getContext

61− case lookupCtxt n i of

62− Just _ -> fail $ show n ++ " already defined"

63− _ -> return ()

59+checkUndefined :: FC -> Name -> Idris ()

60+checkUndefined fc n

61+ = do i <- getContext

62+ case lookupCtxt n i of

63+ Just _ -> fail $ show fc ++ ":" ++

64+ show n ++ " already defined"

65+ _ -> return ()

6466

6567setContext :: Context -> Idris ()

6668setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )

@@ -130,12 +132,12 @@ instance Ord FixDecl where

130132

131133data Plicity = Imp | Exp deriving Show

132134

133−data PDecl' t = PFix Fixity [String] -- fixity declaration

134− | PTy Name t -- type declaration

135− | PClauses Name [PClause' t] -- pattern clause

136− | PData (PData' t) -- data declaration

137− | PParams [(Name, PTerm)] [PDecl' t] -- params block

138− | PSyntax Syntax

135+data PDecl' t = PFix FC Fixity [String] -- fixity declaration

136+ | PTy FC Name t -- type declaration

137+ | PClauses FC Name [PClause' t] -- pattern clause

138+ | PData FC (PData' t) -- data declaration

139+ | PParams FC [(Name, PTerm)] [PDecl' t] -- params block

140+ | PSyntax FC Syntax

139141 deriving Functor

140142

141143data PClause' t = PClause Name t t [PDecl]

@@ -143,7 +145,7 @@ data PClause' t = PClause Name t t [PDecl]

143145

144146data PData' t = PDatadecl { d_name :: Name,

145147 d_tcon :: t,

146− d_cons :: [(Name, t)] }

148+ d_cons :: [(Name, t, FC)] }

147149 deriving Functor

148150

149151-- Handy to get a free function for applying PTerm -> PTerm functions

@@ -156,11 +158,12 @@ type PClause = PClause' PTerm

156158-- get all the names declared in a decl

157159

158160declared :: PDecl -> [Name]

159−declared (PFix _ _) = []

160−declared (PTy n t) = [n]

161−declared (PClauses n _) = [] -- not a declaration

162−declared (PData (PDatadecl n _ ts)) = n : map fst ts

163−declared (PParams _ ds) = concatMap declared ds

161+declared (PFix _ _ _) = []

162+declared (PTy _ n t) = [n]

163+declared (PClauses _ n _) = [] -- not a declaration

164+declared (PData _ (PDatadecl n _ ts)) = n : map fstt ts

165+ where fstt (a, _, _) = a

166+declared (PParams _ _ ds) = concatMap declared ds

164167-- declared (PImport _) = []

165168

166169-- High level language terms

@@ -222,10 +225,10 @@ instance Show PTerm where

222225 show tm = showImp False tm

223226

224227instance Show PDecl where

225− show (PFix f ops) = show f ++ " " ++ showSep ", " ops

226− show (PTy n ty) = show n ++ " : " ++ show ty

227− show (PClauses n c) = showSep "\n" (map show c)

228− show (PData d) = show d

228+ show (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

229+ show (PTy _ n ty) = show n ++ " : " ++ show ty

230+ show (PClauses _ n c) = showSep "\n" (map show c)

231+ show (PData _ d) = show d

229232

230233instance Show PClause where

231234 show c = showCImp False c

@@ -240,7 +243,7 @@ showDImp :: Bool -> PData -> String

240243showDImp impl (PDatadecl n ty cons)

241244 = "data " ++ show n ++ " : " ++ showImp impl ty ++ " where\n\t"

242245 ++ showSep "\n\t| "

243− (map (\ (n, t) -> show n ++ " : " ++ showImp impl t) cons)

246+ (map (\ (n, t, _) -> show n ++ " : " ++ showImp impl t) cons)

244247

245248getImps :: [PArg] -> [(Name, PTerm)]

246249getImps [] = []

@@ -323,13 +326,15 @@ namesIn ist tm = nub $ ni [] tm

323326

324327-- For inferring types of things

325328

329+bi = FC "builtin" 0

330+

326331inferTy = MN 0 "__Infer"

327332inferCon = MN 0 "__infer"

328333inferDecl = PDatadecl inferTy

329334 PSet

330335 [(inferCon, PPi Imp (MN 0 "A") PSet (

331336 PPi Exp (MN 0 "a") (PRef (MN 0 "A"))

332− (PRef inferTy)))]

337+ (PRef inferTy)), bi)]

333338

334339infTerm t = PApp (PRef inferCon) [PImp (MN 0 "A") Placeholder, PExp t]

335340infP = P (TCon 0) inferTy (Set 0)

@@ -344,10 +349,11 @@ getInferType (App (App _ ty) _) = ty

344349

345350-- Handy primitives: Unit, False, Pair, MkPair, mkForeign

346351

352+

347353unitTy = MN 0 "__Unit"

348354unitCon = MN 0 "__II"

349355unitDecl = PDatadecl unitTy PSet

350− [(unitCon, PRef unitTy)]

356+ [(unitCon, PRef unitTy, bi)]

351357

352358falseTy = MN 0 "__False"

353359falseDecl = PDatadecl falseTy PSet []

@@ -360,7 +366,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

360366 PPi Exp (n "a") (PRef (n "A")) (

361367 PPi Exp (n "c") (PRef (n "B"))

362368 (PApp (PRef pairTy) [PExp (PRef (n "A")),

363− PExp (PRef (n "B"))])))))]

369+ PExp (PRef (n "B"))])))), bi)]

364370 where n a = MN 0 a

365371

366372piBind :: [(Name, PTerm)] -> PTerm -> PTerm

@@ -467,11 +473,11 @@ dumpDecls :: [PDecl] -> String

467473dumpDecls [] = ""

468474dumpDecls (d:ds) = dumpDecl d ++ "\n" ++ dumpDecls ds

469475

470−dumpDecl (PFix f ops) = show f ++ " " ++ showSep ", " ops

471−dumpDecl (PTy n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

472−dumpDecl (PClauses n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

473−dumpDecl (PData d) = showDImp True d

474−dumpDecl (PParams ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

475−dumpDecl (PSyntax syn) = "syntax " ++ show syn

476+dumpDecl (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

477+dumpDecl (PTy _ n t) = "tydecl " ++ show n ++ " : " ++ showImp True t

478+dumpDecl (PClauses _ n cs) = "pat\t" ++ showSep "\n\t" (map (showCImp True) cs)

479+dumpDecl (PData _ d) = showDImp True d

480+dumpDecl (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ dumpDecls ps ++ "}\n"

481+dumpDecl (PSyntax _ syn) = "syntax " ++ show syn

476482-- dumpDecl (PImport i) = "import " ++ i

477483

src/Idris/ElabDecls.hs+40−35

@@ -27,23 +27,26 @@ data ElabInfo = EInfo { params :: [(Name, PTerm)],

2727

2828toplevel = EInfo [] emptyContext id

2929

30−elabType :: ElabInfo -> Name -> PTerm -> Idris ()

31−elabType info n_in ty_in = let ty = piBind (params info) ty_in

32− n = liftname info n_in in

33− do checkUndefined n

30+elabType :: ElabInfo -> FC -> Name -> PTerm -> Idris ()

31+elabType info fc n_in ty_in = let ty = piBind (params info) ty_in

32+ n = liftname info n_in in

33+ do checkUndefined fc n

3434 ctxt <- getContext

3535 logLvl 2 $ "Type " ++ showImp True ty

36− ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False ty)

36+ ((ty', defer), log) <- tclift $ elaborate ctxt n (Set 0)

37+ (erun fc (build info False ty))

3738 (cty, _) <- tclift $ recheck ctxt [] ty'

3839 logLvl 2 $ "---> " ++ show cty

3940 let nty = normalise ctxt [] cty

4041 addDeferred ((n, nty):defer)

4142

42−elabData :: ElabInfo -> PData -> Idris ()

43−elabData info (PDatadecl n t dcons)

44− = do checkUndefined n

43+elabData :: ElabInfo -> FC -> PData -> Idris ()

44+elabData info fc (PDatadecl n t dcons)

45+ = do iLOG (show fc)

46+ checkUndefined fc n

4547 ctxt <- getContext

46− ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

48+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

49+ (erun fc (build info False t))

4750 addDeferred defer

4851 (cty, _) <- tclift $ recheck ctxt [] t'

4952 logLvl 2 $ "---> " ++ show cty

@@ -51,22 +54,23 @@ elabData info (PDatadecl n t dcons)

5154 cons <- mapM (elabCon info) dcons

5255 setContext (addDatatype (Data n cty cons) ctxt)

5356

54−elabCon :: ElabInfo -> (Name, PTerm) -> Idris (Name, Type)

55−elabCon info (n, t)

56− = do checkUndefined n

57+elabCon :: ElabInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

58+elabCon info (n, t, fc)

59+ = do checkUndefined fc n

5760 ctxt <- getContext

58− logLvl 2 $ "Constructor " ++ show n ++ " : " ++ showImp True t

59− ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0) (build info False t)

61+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp True t

62+ ((t', defer), log) <- tclift $ elaborate ctxt n (Set 0)

63+ (erun fc (build info False t))

6064 logLvl 2 $ "Rechecking " ++ show t'

6165 addDeferred defer

6266 (cty, _) <- tclift $ recheck ctxt [] t'

6367 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty

6468 return (n, cty)

6569

66−elabClauses :: ElabInfo -> Name -> [PClause] -> Idris ()

67−elabClauses info n_in cs = let n = liftname info n_in in

70+elabClauses :: ElabInfo -> FC -> Name -> [PClause] -> Idris ()

71+elabClauses info fc n_in cs = let n = liftname info n_in in

6872 do solveDeferred n

69− pats <- mapM (elabClause info) cs

73+ pats <- mapM (elabClause info fc) cs

7074 logLvl 3 (showSep "\n" (map (\ (l,r) ->

7175 show l ++ " = " ++

7276 show r) pats))

@@ -92,13 +96,13 @@ elabVal info tm

9296 logLvl 2 (show vtm)

9397 tclift $ recheck ctxt [] vtm

9498

95−elabClause :: ElabInfo -> PClause -> Idris (Term, Term)

96−elabClause info (PClause fname lhs rhs whereblock)

99+elabClause :: ElabInfo -> FC -> PClause -> Idris (Term, Term)

100+elabClause info fc (PClause fname lhs rhs whereblock)

97101 = do ctxt <- getContext

98102 -- Build the LHS as an "Infer", and pull out its type and

99103 -- pattern bindings

100104 ((lhs', dlhs), _) <- tclift $ elaborate ctxt (MN 0 "patLHS") infP

101− (build info True (infTerm lhs))

105+ (erun fc (build info True (infTerm lhs)))

102106 let lhs_tm = getInferTerm lhs'

103107 let lhs_ty = getInferType lhs'

104108 logLvl 3 (show lhs_tm)

@@ -114,7 +118,7 @@ elabClause info (PClause fname lhs rhs whereblock)

114118 ctxt <- getContext -- new context with where block added

115119 ((rhs', defer), _) <- tclift $ elaborate ctxt (MN 0 "patRHS") clhsty

116120 (do pbinds lhs_tm

117− (_, d) <- build winfo False rhs

121+ (_, d) <- erun fc (build winfo False rhs)

118122 psolve lhs_tm

119123 tt <- get_term

120124 return (tt, d))

@@ -152,15 +156,15 @@ elabClause info (PClause fname lhs rhs whereblock)

152156elabDecl :: ElabInfo -> PDecl -> Idris ()

153157elabDecl info d = idrisCatch (elabDecl' info d) (\e -> iputStrLn (report e))

154158

155−elabDecl' info (PFix _ _) = return () -- nothing to elaborate

156−elabDecl' info (PSyntax p) = return () -- nothing to elaborate

157−elabDecl' info (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n

158− elabType info n ty

159−elabDecl' info (PData d) = do iLOG $ "Elaborating " ++ show (d_name d)

160− elabData info d

161−elabDecl' info d@(PClauses n ps) = do iLOG $ "Elaborating clause " ++ show n

162− elabClauses info n ps

163−elabDecl' info (PParams ns ps) = mapM_ (elabDecl' pinfo) ps

159+elabDecl' info (PFix _ _ _) = return () -- nothing to elaborate

160+elabDecl' info (PSyntax _ p) = return () -- nothing to elaborate

161+elabDecl' info (PTy f n ty) = do iLOG $ "Elaborating type decl " ++ show n

162+ elabType info f n ty

163+elabDecl' info (PData f d) = do iLOG $ "Elaborating " ++ show (d_name d)

164+ elabData info f d

165+elabDecl' info d@(PClauses f n ps) = do iLOG $ "Elaborating clause " ++ show n

166+ elabClauses info f n ps

167+elabDecl' info (PParams f ns ps) = mapM_ (elabDecl' pinfo) ps

164168 where

165169 pinfo = let ds = concatMap declared ps

166170 newps = params info ++ ns

@@ -241,11 +245,12 @@ elab info pattern tm = do elab' tm

241245 = elabApp (liftname info f) (map (PExp . PRef) ps ++ args)

242246 | otherwise = elabApp f args

243247 where elabApp f args

244− = try (do ns <- apply (Var f) (map isph args)

245− solve

246− elabArgs ns (map getTm args))

247− (do apply_elab f (map toElab args)

248− solve)

248+ = -- erun (FC "FOO" 42) $

249+ try (do ns <- apply (Var f) (map isph args)

250+ solve

251+ elabArgs ns (map getTm args))

252+ (do apply_elab f (map toElab args)

253+ solve)

249254 elab' (PApp f [arg])

250255 = do simple_app (elab' f) (elab' (getTm arg))

251256 solve

src/Idris/Error.hs+1

@@ -28,6 +28,7 @@ pshow i (Msg s) = s

2828pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

2929 ++ " with " ++ show (delab i y)

3030 -- ++ "\n\t(" ++ pshow i e ++ ")"

31+pshow i (At f e) = show f ++ ":" ++ pshow i e

3132

3233tclift :: Show a => TC a -> Idris a

3334tclift tc = case tc of

src/Idris/Parser.hs+43−24

@@ -17,6 +17,7 @@ import Data.List

1717import Control.Monad.State

1818import Debug.Trace

1919import Data.Maybe

20+import System.FilePath

2021

2122type TokenParser a = PTok.TokenParser a

2223

@@ -82,6 +83,14 @@ parseImports fname input

8283 Right (x, i) -> do put i

8384 return x

8485

86+pfc :: IParser FC

87+pfc = do s <- getPosition

88+ let (dir, file) = splitFileName (sourceName s)

89+ let f = case dir of

90+ "./" -> file

91+ _ -> sourceName s

92+ return $ FC f (sourceLine s)

93+

8594pImport :: IParser String

8695pImport = do reserved "import"

8796 f <- identifier

@@ -103,11 +112,11 @@ parseProg syn fname input pos

103112

104113-- Collect PClauses with the same function name

105114collect :: [PDecl] -> [PDecl]

106−collect (c@(PClauses _ [PClause n l r w]) : ds) = clauses n [] (c:ds)

107− where clauses n acc (PClauses _ [PClause n' l r w] : ds)

115+collect (c@(PClauses fc _ [PClause n l r w]) : ds) = clauses n [] (c:ds)

116+ where clauses n acc (PClauses fc _ [PClause n' l r w] : ds)

108117 | n == n' = clauses n (PClause n' l r (collect w) : acc) ds

109− clauses n acc xs = PClauses n (reverse acc) : collect xs

110−collect (PParams ns ps : ds) = PParams ns (collect ps) : (collect ds)

118+ clauses n acc xs = PClauses fc n (reverse acc) : collect xs

119+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : (collect ds)

111120collect (d : ds) = d : collect ds

112121collect [] = []

113122

@@ -151,7 +160,8 @@ pSyntaxDecl syn

151160 = do s <- pSyntaxRule syn

152161 i <- getState

153162 setState (i { syntax_rules = s : syntax_rules i })

154− return (PSyntax s)

163+ fc <- pfc

164+ return (PSyntax fc s)

155165

156166pSyntaxRule :: SyntaxInfo -> IParser Syntax

157167pSyntaxRule syn

@@ -180,10 +190,11 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

180190 return (Symbol sym)

181191

182192pFunDecl' :: SyntaxInfo -> IParser PDecl

183−pFunDecl' syn = try (do n <- pfName; ty <- pTSig syn

193+pFunDecl' syn = try (do fc <- pfc

194+ n <- pfName; ty <- pTSig syn

184195 lchar ';'

185196 ty' <- implicit syn n ty

186− return (PTy n ty'))

197+ return (PTy fc n ty'))

187198 <|> try (pPattern syn)

188199

189200pUsing :: SyntaxInfo -> IParser [PDecl]

@@ -208,7 +219,8 @@ pParams syn =

208219 let pvars = syn_params syn

209220 ds <- many1 (pDecl syn { syn_params = pvars ++ ns })

210221 lchar '}'

211− return [PParams ns (concat ds)]

222+ fc <- pfc

223+ return [PParams fc ns (concat ds)]

212224

213225--------- Fixity ---------

214226

@@ -220,7 +232,8 @@ pFixity = do f <- fixity; i <- natural; ops <- sepBy1 operator (lchar ',')

220232 let fs = map (Fix (f prec)) ops

221233 setState (istate {

222234 idris_infixes = sort (fs ++ idris_infixes istate) })

223− return (PFix (f prec) ops)

235+ fc <- pfc

236+ return (PFix fc (f prec) ops)

224237

225238fixity :: IParser (Int -> Fixity)

226239fixity = try (do reserved "infixl"; return Infixl)

@@ -401,23 +414,26 @@ prefix name f = Prefix (do { reservedOp name; return f })

401414--------- Data declarations ---------

402415

403416pData :: SyntaxInfo -> IParser PDecl

404−pData syn = try (do reserved "data"; tyn <- pfName; ty <- pTSig syn

417+pData syn = try (do fc <- pfc

418+ reserved "data"; tyn <- pfName; ty <- pTSig syn

405419 reserved "where"

406420 ty' <- implicit syn tyn ty

407421 cons <- sepBy (pConstructor syn) (lchar '|')

408422 lchar ';'

409− return $ PData (PDatadecl tyn ty' cons))

410− <|> do reserved "data"; tyn <- pfName; args <- many pName

423+ return $ PData fc (PDatadecl tyn ty' cons))

424+ <|> do fc <- pfc

425+ reserved "data"; tyn <- pfName; args <- many pName

411426 lchar '='

412427 cons <- sepBy1 (pSimpleCon syn) (lchar '|')

413428 lchar ';'

414429 let conty = mkPApp (PRef tyn) (map PRef args)

415430 let ty = bindArgs (map (\a -> PSet) args) PSet

416431 ty' <- implicit syn tyn ty

417− cons' <- mapM (\ (x, cargs) -> do let cty = bindArgs cargs conty

418− cty' <- implicit syn x cty

419− return (x, cty')) cons

420− return $ PData (PDatadecl tyn ty' cons')

432+ cons' <- mapM (\ (x, cargs, cfc) ->

433+ do let cty = bindArgs cargs conty

434+ cty' <- implicit syn x cty

435+ return (x, cty', cfc)) cons

436+ return $ PData fc (PDatadecl tyn ty' cons')

421437

422438mkPApp t [] = t

423439mkPApp t xs = PApp t (map PExp xs)

@@ -426,23 +442,26 @@ bindArgs :: [PTerm] -> PTerm -> PTerm

426442bindArgs [] t = t

427443bindArgs (x:xs) t = PPi Exp (MN 0 "t") x (bindArgs xs t)

428444

429−pConstructor :: SyntaxInfo -> IParser (Name, PTerm)

445+pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

430446pConstructor syn

431− = do cn <- pfName; ty <- pTSig syn

447+ = do fc <- pfc

448+ cn <- pfName; ty <- pTSig syn

432449 ty' <- implicit syn cn ty

433− return (cn, ty')

450+ return (cn, ty', fc)

434451

435−pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm])

452+pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

436453pSimpleCon syn

437− = do cn <- pfName

454+ = do fc <- pfc

455+ cn <- pfName

438456 args <- many (pSimpleExpr syn)

439− return (cn, args)

457+ return (cn, args, fc)

440458

441459--------- Pattern match clauses ---------

442460

443461pPattern :: SyntaxInfo -> IParser PDecl

444−pPattern syn = do clause <- pClause syn

445− return (PClauses (MN 2 "_") [clause]) -- collect together later

462+pPattern syn = do fc <- pfc

463+ clause <- pClause syn

464+ return (PClauses fc (MN 2 "_") [clause]) -- collect together later

446465

447466pClause :: SyntaxInfo -> IParser PClause

448467pClause syn

src/Idris/Primitives.hs+1−1

@@ -94,7 +94,7 @@ elabPrim (Prim n ty i def epic)

9494

9595elabPrims :: Idris ()

9696elabPrims = do mapM_ (elabDecl toplevel)

97− (map PData

97+ (map (PData (FC "builtin" 0))

9898 [inferDecl, unitDecl, falseDecl, pairDecl])

9999 mapM_ elabPrim primitives

100100