ec87a69 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

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

ec87a69Edwin Brady15 years ago

impl-paper/Makefile+2−1

compare with master

unifiedsplit

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

3all: ${PAPER}.pdf

5TEXFILES = ${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

8DIAGS =

9DIAGS =

impl-paper/impldtp.tex+2

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

94\input{compiling.tex}

96+\input{syntax.tex}

97+

96\input{conclusions.tex}

98\input{conclusions.tex}

98\bibliographystyle{acmtrans}

100\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

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

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+

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

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

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

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

src/Core/TT.hs+13−1

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

23 | CheckConv

24 deriving Eq

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+

26data Err = Msg String

33data Err = Msg String

27 | CantUnify Term Term Err

34 | CantUnify Term Term Err

35+ | At FC Err

28 deriving Eq

36 deriving Eq

30instance Show Err where

38instance Show Err where

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

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

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

38 show (OK x) = show x

46 show (OK x) = show x

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

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

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

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

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

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

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

51tfail :: Err -> TC a

59tfail :: Err -> TC a

52tfail e = Error e

60tfail e = Error e

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

63+trun fc (OK a) = OK a

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

65+

54instance MonadPlus TC where

66instance MonadPlus TC where

55 mzero = fail "Unknown error"

67 mzero = fail "Unknown error"

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

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

src/Idris/AbsSyntax.hs+37−31

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

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

57 return idx

59−checkUndefined :: Name -> Idris ()

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

60−checkUndefined n = do i <- getContext

60+checkUndefined fc n

61+ = do i <- getContext

61− case lookupCtxt n i of

62+ case lookupCtxt n i of

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

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

64+ show n ++ " already defined"

63− _ -> return ()

65+ _ -> return ()

65setContext :: Context -> Idris ()

67setContext :: Context -> Idris ()

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

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

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

130

132

131data Plicity = Imp | Exp deriving Show

133data Plicity = Imp | Exp deriving Show

132

134

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

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

134− | PTy Name t -- type declaration

136+ | PTy FC Name t -- type declaration

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

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

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

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

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

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

138− | PSyntax Syntax

140+ | PSyntax FC Syntax

139 deriving Functor

141 deriving Functor

140

142

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

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

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

143

145

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

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

145 d_tcon :: t,

147 d_tcon :: t,

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

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

147 deriving Functor

149 deriving Functor

148

150

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

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

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

156-- get all the names declared in a decl

158-- get all the names declared in a decl

157

159

158declared :: PDecl -> [Name]

160declared :: PDecl -> [Name]

159−declared (PFix _ _) = []

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

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

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

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

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

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

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

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

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

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

164-- declared (PImport _) = []

167-- declared (PImport _) = []

165

168

166-- High level language terms

169-- High level language terms

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

222 show tm = showImp False tm

225 show tm = showImp False tm

223

226

224instance Show PDecl where

227instance Show PDecl where

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

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

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

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

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

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

228− show (PData d) = show d

231+ show (PData _ d) = show d

229

232

230instance Show PClause where

233instance Show PClause where

231 show c = showCImp False c

234 show c = showCImp False c

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

240showDImp impl (PDatadecl n ty cons)

243showDImp impl (PDatadecl n ty cons)

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

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

242 ++ showSep "\n\t| "

245 ++ showSep "\n\t| "

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

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

244

247

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

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

246getImps [] = []

249getImps [] = []

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

323

326

324-- For inferring types of things

327-- For inferring types of things

325

328

329+bi = FC "builtin" 0

330+

326inferTy = MN 0 "__Infer"

331inferTy = MN 0 "__Infer"

327inferCon = MN 0 "__infer"

332inferCon = MN 0 "__infer"

328inferDecl = PDatadecl inferTy

333inferDecl = PDatadecl inferTy

329 PSet

334 PSet

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

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

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

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

332− (PRef inferTy)))]

337+ (PRef inferTy)), bi)]

333

338

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

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

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

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

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

344

349

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

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

346

351

352+

347unitTy = MN 0 "__Unit"

353unitTy = MN 0 "__Unit"

348unitCon = MN 0 "__II"

354unitCon = MN 0 "__II"

349unitDecl = PDatadecl unitTy PSet

355unitDecl = PDatadecl unitTy PSet

350− [(unitCon, PRef unitTy)]

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

351

357

352falseTy = MN 0 "__False"

358falseTy = MN 0 "__False"

353falseDecl = PDatadecl falseTy PSet []

359falseDecl = PDatadecl falseTy PSet []

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

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

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

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

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

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

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

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

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

364 where n a = MN 0 a

370 where n a = MN 0 a

365

371

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

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

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

467dumpDecls [] = ""

473dumpDecls [] = ""

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

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

469

475

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

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

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

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

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

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

473−dumpDecl (PData d) = showDImp True d

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

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

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

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

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

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

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

477

483

src/Idris/ElabDecls.hs+40−35

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

28toplevel = EInfo [] emptyContext id

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

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

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

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

32− n = liftname info n_in in

32+ n = liftname info n_in in

33− do checkUndefined n

33+ do checkUndefined fc n

34 ctxt <- getContext

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

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

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

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

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

39 let nty = normalise ctxt [] cty

40 let nty = normalise ctxt [] cty

40 addDeferred ((n, nty):defer)

41 addDeferred ((n, nty):defer)

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

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

43−elabData info (PDatadecl n t dcons)

44+elabData info fc (PDatadecl n t dcons)

45+ = do iLOG (show fc)

44− = do checkUndefined n

46+ checkUndefined fc n

45 ctxt <- getContext

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

47 addDeferred defer

50 addDeferred defer

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

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

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

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

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

51 cons <- mapM (elabCon info) dcons

54 cons <- mapM (elabCon info) dcons

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

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

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

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

55−elabCon info (n, t)

58+elabCon info (n, t, fc)

56− = do checkUndefined n

59+ = do checkUndefined fc n

57 ctxt <- getContext

60 ctxt <- getContext

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

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

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

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

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

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

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

61 addDeferred defer

65 addDeferred defer

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

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

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

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

64 return (n, cty)

68 return (n, cty)

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

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

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

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

68 do solveDeferred n

72 do solveDeferred n

69− pats <- mapM (elabClause info) cs

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

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

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

71 show l ++ " = " ++

75 show l ++ " = " ++

72 show r) pats))

76 show r) pats))

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

92 logLvl 2 (show vtm)

96 logLvl 2 (show vtm)

93 tclift $ recheck ctxt [] vtm

97 tclift $ recheck ctxt [] vtm

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

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

96−elabClause info (PClause fname lhs rhs whereblock)

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

97 = do ctxt <- getContext

101 = do ctxt <- getContext

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

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

99 -- pattern bindings

103 -- pattern bindings

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

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

101− (build info True (infTerm lhs))

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

102 let lhs_tm = getInferTerm lhs'

106 let lhs_tm = getInferTerm lhs'

103 let lhs_ty = getInferType lhs'

107 let lhs_ty = getInferType lhs'

104 logLvl 3 (show lhs_tm)

108 logLvl 3 (show lhs_tm)

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

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

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

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

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

116 (do pbinds lhs_tm

120 (do pbinds lhs_tm

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

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

118 psolve lhs_tm

122 psolve lhs_tm

119 tt <- get_term

123 tt <- get_term

120 return (tt, d))

124 return (tt, d))

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

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

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

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

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

154

158

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

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

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

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

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

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

158− elabType info n ty

162+ elabType info f n ty

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

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

160− elabData info d

164+ elabData info f d

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

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

162− elabClauses info n ps

166+ elabClauses info f n ps

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

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

164 where

168 where

165 pinfo = let ds = concatMap declared ps

169 pinfo = let ds = concatMap declared ps

166 newps = params info ++ ns

170 newps = params info ++ ns

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

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

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

242 | otherwise = elabApp f args

246 | otherwise = elabApp f args

243 where elabApp f args

247 where elabApp f args

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

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

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

245− solve

250+ solve

246− elabArgs ns (map getTm args))

251+ elabArgs ns (map getTm args))

247− (do apply_elab f (map toElab args)

252+ (do apply_elab f (map toElab args)

248− solve)

253+ solve)

249 elab' (PApp f [arg])

254 elab' (PApp f [arg])

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

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

251 solve

256 solve

src/Idris/Error.hs+1

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

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

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

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

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

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

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

33tclift tc = case tc of

34tclift tc = case tc of

src/Idris/Parser.hs+43−24

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

17import Control.Monad.State

18import Debug.Trace

19import Data.Maybe

20+import System.FilePath

21type TokenParser a = PTok.TokenParser a

22type TokenParser a = PTok.TokenParser a

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

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

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

83 return x

84 return x

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+

85pImport :: IParser String

94pImport :: IParser String

86pImport = do reserved "import"

95pImport = do reserved "import"

87 f <- identifier

96 f <- identifier

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

103

112

104-- Collect PClauses with the same function name

113-- Collect PClauses with the same function name

105collect :: [PDecl] -> [PDecl]

114collect :: [PDecl] -> [PDecl]

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

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

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

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

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

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

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

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

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

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

111collect (d : ds) = d : collect ds

120collect (d : ds) = d : collect ds

112collect [] = []

121collect [] = []

113

122

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

151 = do s <- pSyntaxRule syn

160 = do s <- pSyntaxRule syn

152 i <- getState

161 i <- getState

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

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

163+ fc <- pfc

154− return (PSyntax s)

164+ return (PSyntax fc s)

155

165

156pSyntaxRule :: SyntaxInfo -> IParser Syntax

166pSyntaxRule :: SyntaxInfo -> IParser Syntax

157pSyntaxRule syn

167pSyntaxRule syn

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

180 return (Symbol sym)

190 return (Symbol sym)

181

191

182pFunDecl' :: SyntaxInfo -> IParser PDecl

192pFunDecl' :: SyntaxInfo -> IParser PDecl

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

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

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

184 lchar ';'

195 lchar ';'

185 ty' <- implicit syn n ty

196 ty' <- implicit syn n ty

186− return (PTy n ty'))

197+ return (PTy fc n ty'))

187 <|> try (pPattern syn)

198 <|> try (pPattern syn)

188

199

189pUsing :: SyntaxInfo -> IParser [PDecl]

200pUsing :: SyntaxInfo -> IParser [PDecl]

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

208 let pvars = syn_params syn

219 let pvars = syn_params syn

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

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

210 lchar '}'

221 lchar '}'

222+ fc <- pfc

211− return [PParams ns (concat ds)]

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

212

224

213--------- Fixity ---------

225--------- Fixity ---------

214

226

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

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

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

221 setState (istate {

233 setState (istate {

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

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

235+ fc <- pfc

223− return (PFix (f prec) ops)

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

224

237

225fixity :: IParser (Int -> Fixity)

238fixity :: IParser (Int -> Fixity)

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

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

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

401--------- Data declarations ---------

414--------- Data declarations ---------

402

415

403pData :: SyntaxInfo -> IParser PDecl

416pData :: SyntaxInfo -> IParser PDecl

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

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

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

405 reserved "where"

419 reserved "where"

406 ty' <- implicit syn tyn ty

420 ty' <- implicit syn tyn ty

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

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

408 lchar ';'

422 lchar ';'

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

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

424+ <|> do fc <- pfc

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

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

411 lchar '='

426 lchar '='

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

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

413 lchar ';'

428 lchar ';'

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

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

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

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

416 ty' <- implicit syn tyn ty

431 ty' <- implicit syn tyn ty

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

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

433+ do let cty = bindArgs cargs conty

418− cty' <- implicit syn x cty

434+ cty' <- implicit syn x cty

419− return (x, cty')) cons

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

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

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

421

437

422mkPApp t [] = t

438mkPApp t [] = t

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

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

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

426bindArgs [] t = t

442bindArgs [] t = t

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

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

428

444

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

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

430pConstructor syn

446pConstructor syn

447+ = do fc <- pfc

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

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

432 ty' <- implicit syn cn ty

449 ty' <- implicit syn cn ty

433− return (cn, ty')

450+ return (cn, ty', fc)

434

451

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

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

436pSimpleCon syn

453pSimpleCon syn

454+ = do fc <- pfc

437− = do cn <- pfName

455+ cn <- pfName

438 args <- many (pSimpleExpr syn)

456 args <- many (pSimpleExpr syn)

439− return (cn, args)

457+ return (cn, args, fc)

440

458

441--------- Pattern match clauses ---------

459--------- Pattern match clauses ---------

442

460

443pPattern :: SyntaxInfo -> IParser PDecl

461pPattern :: SyntaxInfo -> IParser PDecl

462+pPattern syn = do fc <- pfc

444−pPattern syn = do clause <- pClause syn

463+ clause <- pClause syn

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

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

446

465

447pClause :: SyntaxInfo -> IParser PClause

466pClause :: SyntaxInfo -> IParser PClause

448pClause syn

467pClause syn

src/Idris/Primitives.hs+1−1

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

95elabPrims :: Idris ()

96elabPrims = do mapM_ (elabDecl toplevel)

97− (map PData

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

98 [inferDecl, unitDecl, falseDecl, pairDecl])

99 mapM_ elabPrim primitives

100