5f7eed8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Propagate line numbers through applications and variables

5f7eed8Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+47−47

compare with master

unifiedsplit

@@ -169,26 +169,26 @@ declared (PParams _ _ ds) = concatMap declared ds

169-- High level language terms

170--

171data PTerm = PQuote Raw

172− | PRef Name

172+ | PRef FC Name

173 | PLam Name PTerm PTerm

174 | PPi Plicity Name PTerm PTerm

175 | PLet Name PTerm PTerm PTerm -- not implemented yet

176− | PApp PTerm [PArg]

176+ | PApp FC PTerm [PArg]

177− | PTrue

177+ | PTrue FC

178− | PFalse

178+ | PFalse FC

179− | PPair PTerm PTerm

179+ | PPair FC PTerm PTerm

180 | PHidden PTerm -- irrelevant or hidden pattern

181 | PSet

182 | PConstant Const

183 | Placeholder

184 | PDoBlock [PDo]

185− | PReturn

185+ | PReturn FC

186 | PMetavar Name

187 | PElabError String -- error to report on elaboration

188

189−data PDo = DoExp PTerm

189+data PDo = DoExp FC PTerm

190− | DoBind Name PTerm

190+ | DoBind FC Name PTerm

191− | DoLet Name PTerm

191+ | DoLet FC Name PTerm

192

193data PArg' t = PImp { pname :: Name, getTm :: t }

194 | PExp { getTm :: t }

@@ -261,7 +261,7 @@ getAll = map getTm

261showImp :: Bool -> PTerm -> String

262showImp impl tm = se 10 tm where

263 se p (PQuote r) = "![" ++ show r ++ "]"

264− se p (PRef n) = show n

264+ se p (PRef _ n) = show n

265 se p (PLam n ty sc) = bracket p 2 $ "\\ " ++ show n ++ " => " ++ show sc

266 se p (PPi Exp n ty sc)

267 | n `elem` allNamesIn sc = bracket p 2 $

@@ -272,20 +272,20 @@ showImp impl tm = se 10 tm where

272 | impl = bracket p 2 $ "{" ++ show n ++ " : " ++ se 10 ty ++

273 "} -> " ++ se 10 sc

274 | otherwise = se 10 sc

275− se p (PApp (PRef f) [])

275+ se p (PApp _ (PRef _ f) [])

276 | not impl = show f

277− se p (PApp (PRef op@(UN [f:_])) args)

277+ se p (PApp _ (PRef _ op@(UN [f:_])) args)

278 | length (getExps args) == 2 && not impl && not (isAlpha f)

279 = let [l, r] = getExps args in

280 bracket p 1 $ se 1 l ++ " " ++ show op ++ " " ++ se 0 r

281− se p (PApp f as)

281+ se p (PApp _ f as)

282 = let (imps, args) = (getImps as, getExps as) in

283 bracket p 1 $ se 1 f ++ (if impl then concatMap siArg imps else "")

284 ++ concatMap seArg args

285 se p (PHidden tm) = "." ++ se 0 tm

286− se p PTrue = "()"

286+ se p (PTrue _) = "()"

287− se p PFalse = "_|_"

287+ se p (PFalse _) = "_|_"

288− se p (PPair l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

288+ se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

289 se p PSet = "Set"

290 se p (PConstant c) = show c

291 se p (PMetavar n) = "?" ++ show n

@@ -300,27 +300,27 @@ showImp impl tm = se 10 tm where

300allNamesIn :: PTerm -> [Name]

301allNamesIn tm = nub $ ni [] tm

302 where

303− ni env (PRef n)

303+ ni env (PRef _ n)

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

305− ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

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

306 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

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

308 ni env (PHidden tm) = ni env tm

309− ni env (PPair l r) = ni env l ++ ni env r

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

310 ni env _ = []

311

312namesIn :: IState -> PTerm -> [Name]

313namesIn ist tm = nub $ ni [] tm

314 where

315− ni env (PRef n)

315+ ni env (PRef _ n)

316 | not (n `elem` env)

317 = case lookupCtxt n (idris_implicits ist) of

318 Nothing -> [n]

319 _ -> []

320− ni env (PApp f as) = ni env f ++ concatMap (ni env) (map getTm as)

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

321 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

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

323− ni env (PPair l r) = ni env l ++ ni env r

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

324 ni env (PHidden tm) = ni env tm

325 ni env _ = []

326

@@ -333,10 +333,10 @@ inferCon = MN 0 "__infer"

333inferDecl = PDatadecl inferTy

334 PSet

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

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

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

337− (PRef inferTy)), bi)]

337+ (PRef bi inferTy)), bi)]

338

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

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

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

341

342getInferTerm, getInferType :: Term -> Term

@@ -353,7 +353,7 @@ getInferType (App (App _ ty) _) = ty

353unitTy = MN 0 "__Unit"

354unitCon = MN 0 "__II"

355unitDecl = PDatadecl unitTy PSet

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

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

357

358falseTy = MN 0 "__False"

359falseDecl = PDatadecl falseTy PSet []

@@ -363,10 +363,10 @@ pairCon = UN ["MkPair"] -- MN 0 "__MkPair"

363pairDecl = PDatadecl pairTy (piBind [(n "A", PSet), (n "B", PSet)] PSet)

364 [(pairCon, PPi Imp (n "A") PSet (

365 PPi Imp (n "B") PSet (

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

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

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

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

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

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

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

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

370 where n a = MN 0 a

371

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

@@ -388,7 +388,7 @@ implicitise syn ist tm

388 then (tm, reverse declimps)

389 else implicitise syn ist (pibind uvars ns tm)

390 where

391− imps top env (PApp f as)

391+ imps top env (PApp _ f as)

392 = do (decls, ns) <- get

393 let isn = concatMap (namesIn ist) (map getTm as)

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

@@ -399,12 +399,12 @@ implicitise syn ist tm

399 imps True (n:env) sc

400 imps top env (PPi Exp n ty sc)

401 = do let isn = (namesIn ist ty ++ case sc of

402− (PRef x) -> namesIn ist sc

402+ (PRef _ x) -> namesIn ist sc

403 _ -> []) \\ [n]

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

405 put (PExp ty : decls, nub (ns ++ (isn \\ (env ++ map fst (getImps decls)))))

406 imps True (n:env) sc

407− imps top env (PPair l r)

407+ imps top env (PPair _ l r)

408 = do (decls, ns) <- get

409 put (decls, nub (ns ++ namesIn ist l ++ namesIn ist r))

410 imps top env (PLam n ty sc)

@@ -423,13 +423,13 @@ implicitise syn ist tm

423addImpl :: IState -> PTerm -> PTerm

424addImpl ist ptm = ai [] ptm

425 where

426− ai env (PRef f) = aiFn env (PRef f) []

426+ ai env (PRef fc f) = aiFn fc env (PRef fc f) []

427− ai env (PApp (PRef f) as)

427+ ai env (PApp fc (PRef _ f) as)

428 = let as' = map (fmap (ai env)) as in

429− aiFn env (PRef f) as'

429+ aiFn fc env (PRef fc f) as'

430− ai env (PApp f as) = let f' = ai env f

430+ ai env (PApp fc f as) = let f' = ai env f

431 as' = map (fmap (ai env)) as in

432− aiFn env f' as'

432+ aiFn fc env f' as'

433 ai env (PLam n ty sc) = let ty' = ai env ty

434 sc' = ai (n:env) sc in

435 PLam n ty' sc'

@@ -439,18 +439,18 @@ addImpl ist ptm = ai [] ptm

439 ai env (PHidden tm) = PHidden (ai env tm)

440 ai env tm = tm

441

442− aiFn env (PRef f) as | not (f `elem` env)

442+ aiFn _ env (PRef fc f) as | not (f `elem` env)

443 = case lookupCtxt f (idris_implicits ist) of

444− Just ns -> pApp (length ns) (PRef f) (insertImpl ns as)

444+ Just ns -> pApp fc (length ns) (PRef fc f) (insertImpl ns as)

445− Nothing -> pApp 1 (PRef f) as

445+ Nothing -> pApp fc 1 (PRef fc f) as

446− aiFn env f as = pApp 1 f as

446+ aiFn fc env f as = pApp fc 1 f as

447

448− pApp a f [] = f

448+ pApp fc a f [] = f

449− pApp a f as = let rest = drop a as in

449+ pApp fc a f as = let rest = drop a as in

450− appRest (PApp f (take a as)) rest

450+ appRest fc (PApp fc f (take a as)) rest

451

452− appRest f [] = f

452+ appRest fc f [] = f

453− appRest f (a : as) = appRest (PApp f [a]) as

453+ appRest fc f (a : as) = appRest fc (PApp fc f [a]) as

454

455 insertImpl :: [PArg] -> [PArg] -> [PArg]

456 insertImpl (PExp ty : ps) (PExp tm : given) =

src/Idris/Delaborate.hs+12−10

@@ -13,12 +13,14 @@ import Debug.Trace

13delab :: IState -> Term -> PTerm

14delab ist tm = de [] tm

15 where

16+ un = FC "(val)" 0

17+

16 de env (App f a) = deFn env f [a]

18 de env (App f a) = deFn env f [a]

17− de env (V i) = PRef (env!!i)

19+ de env (V i) = PRef un (env!!i)

18− de env (P _ n _) | n == unitTy = PTrue

20+ de env (P _ n _) | n == unitTy = PTrue un

19− | n == unitCon = PTrue

21+ | n == unitCon = PTrue un

20− | n == falseTy = PFalse

22+ | n == falseTy = PFalse un

21− | otherwise = PRef n

23+ | otherwise = PRef un n

22 de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)

24 de env (Bind n (Lam ty) sc) = PLam n (de env ty) (de (n:env) sc)

23 de env (Bind n (Pi ty) sc) = PPi Exp n (de env ty) (de (n:env) sc)

25 de env (Bind n (Pi ty) sc) = PPi Exp n (de env ty) (de (n:env) sc)

24 de env (Bind n (Let ty val) sc)

26 de env (Bind n (Let ty val) sc)

@@ -28,15 +30,15 @@ delab ist tm = de [] tm

28 de env (Set i) = PSet

30 de env (Set i) = PSet

30 deFn env (App f a) args = deFn env f (a:args)

32 deFn env (App f a) args = deFn env f (a:args)

31− deFn env (P _ n _) [l,r] | n == pairTy = PPair (de env l) (de env r)

33+ deFn env (P _ n _) [l,r] | n == pairTy = PPair un (de env l) (de env r)

32− deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair (de env l) (de env r)

34+ deFn env (P _ n _) [_,_,l,r] | n == pairCon = PPair un (de env l) (de env r)

33 deFn env (P _ n _) args = mkPApp n (map (de env) args)

35 deFn env (P _ n _) args = mkPApp n (map (de env) args)

34− deFn env f args = PApp (de env f) (map PExp (map (de env) args))

36+ deFn env f args = PApp un (de env f) (map PExp (map (de env) args))

36 mkPApp n args

38 mkPApp n args

37 | Just imps <- lookupCtxt n (idris_implicits ist)

39 | Just imps <- lookupCtxt n (idris_implicits ist)

38− = PApp (PRef n) (zipWith imp (imps ++ repeat (PExp undefined)) args)

40+ = PApp un (PRef un n) (zipWith imp (imps ++ repeat (PExp undefined)) args)

39− | otherwise = PApp (PRef n) (map PExp args)

41+ | otherwise = PApp un (PRef un n) (map PExp args)

41 imp (PImp n _) arg = PImp n arg

43 imp (PImp n _) arg = PImp n arg

42 imp (PExp _) arg = PExp arg

44 imp (PExp _) arg = PExp arg

src/Idris/ElabDecls.hs+20−17

@@ -209,25 +209,26 @@ elab info pattern tm = do elab' tm

209 elab' PSet = do fill (RSet 0); solve

210 elab' (PConstant c) = do apply (RConstant c) []; solve

211 elab' (PQuote r) = do fill r; solve

212− elab' PTrue = try (elab' (PRef unitCon))

212+ elab' (PTrue fc) = try (elab' (PRef fc unitCon))

213− (elab' (PRef unitTy))

213+ (elab' (PRef fc unitTy))

214− elab' PFalse = elab' (PRef falseTy)

214+ elab' (PFalse fc) = elab' (PRef fc falseTy)

215− elab' (PPair l r) = try (elab' (PApp (PRef pairTy)

215+ elab' (PPair fc l r) = try (elab' (PApp fc (PRef fc pairTy)

216 [PExp l,PExp r]))

217− (elab' (PApp (PRef pairCon)

217+ (elab' (PApp fc (PRef fc pairCon)

218 [PImp (MN 0 "a") Placeholder,

219 PImp (MN 0 "a") Placeholder,

220 PExp l, PExp r]))

221− elab' (PRef n) | pattern && not (inparamBlock n)

221+ elab' (PRef fc n) | pattern && not (inparamBlock n)

222+ = erun fc $

222− = try (do apply (Var n) []; solve)

223+ try (do apply (Var n) []; solve)

223− (patvar n)

224+ (patvar n)

224 where inparamBlock n = case lookupCtxt n (inblock info) of

225 where inparamBlock n = case lookupCtxt n (inblock info) of

225 Nothing -> False

226 Nothing -> False

226 _ -> True

227 _ -> True

227− elab' (PRef n)

228+ elab' (PRef fc n)

228 | Just ps <- lookupCtxt n (inblock info)

229 | Just ps <- lookupCtxt n (inblock info)

229− = elab' (PApp (PRef n) [])

230+ = elab' (PApp fc (PRef fc n) [])

230− | otherwise = do apply (Var n) []; solve

231+ | otherwise = erun fc $ do apply (Var n) []; solve

231 elab' (PLam n Placeholder sc)

232 elab' (PLam n Placeholder sc)

232 = do attack; intro n; elab' sc; solve

233 = do attack; intro n; elab' sc; solve

233 elab' (PPi _ n Placeholder sc)

234 elab' (PPi _ n Placeholder sc)

@@ -240,10 +241,11 @@ elab info pattern tm = do elab' tm

240 elab' ty

241 elab' ty

241 elab' sc

242 elab' sc

242 solve

243 solve

243− elab' (PApp (PRef f) args)

244+ elab' (PApp fc (PRef _ f) args)

244 | Just ps <- lookupCtxt f (inblock info)

245 | Just ps <- lookupCtxt f (inblock info)

246+ = erun fc $

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

247+ elabApp (liftname info f) (map (PExp . (PRef fc)) ps ++ args)

246− | otherwise = elabApp f args

248+ | otherwise = erun fc $ elabApp f args

247 where elabApp f args

249 where elabApp f args

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

250 = -- erun (FC "FOO" 42) $

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

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

@@ -251,9 +253,10 @@ elab info pattern tm = do elab' tm

251 elabArgs ns (map getTm args))

253 elabArgs ns (map getTm args))

252 (do apply_elab f (map toElab args)

254 (do apply_elab f (map toElab args)

253 solve)

255 solve)

254− elab' (PApp f [arg])

256+ elab' (PApp fc f [arg])

257+ = erun fc $

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

258+ do simple_app (elab' f) (elab' (getTm arg))

256− solve

259+ solve

257 elab' Placeholder = do (h : hs) <- get_holes

260 elab' Placeholder = do (h : hs) <- get_holes

258 movelast h

261 movelast h

259 elab' (PMetavar n) = do attack; defer n; solve

262 elab' (PMetavar n) = do attack; defer n; solve

src/Idris/Parser.hs+56−43

@@ -278,20 +278,20 @@ pExt syn (Rule (s:ssym) ptm)

278 dropn n ((x,t) : xs) | n == x = xs

279 | otherwise = (x,t):dropn n xs

280

281− update ns (PRef n) = case lookup n ns of

281+ update ns (PRef fc n) = case lookup n ns of

282− Just t -> t

282+ Just t -> t

283− _ -> PRef n

283+ _ -> PRef fc n

284 update ns (PLam n ty sc) = PLam n (update ns ty) (update (dropn n ns) sc)

285 update ns (PPi p n ty sc) = PPi p n (update ns ty) (update (dropn n ns) sc)

286 update ns (PLet n ty val sc) = PLet n (update ns ty) (update ns val)

287 (update (dropn n ns) sc)

288− update ns (PApp t args) = PApp (update ns t) (map (fmap (update ns)) args)

288+ update ns (PApp fc t args) = PApp fc (update ns t) (map (fmap (update ns)) args)

289− update ns (PPair l r) = PPair (update ns l) (update ns r)

289+ update ns (PPair fc l r) = PPair fc (update ns l) (update ns r)

290 update ns (PHidden t) = PHidden (update ns t)

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

292− where upd ns (DoExp t : ds) = DoExp (update ns t) : upd ns ds

292+ where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd ns ds

293− upd ns (DoBind n t : ds) = DoBind n (update ns t) : upd (dropn n ns) ds

293+ upd ns (DoBind fc n t : ds) = DoBind fc n (update ns t) : upd (dropn n ns) ds

294− upd ns (DoLet n t : ds) = DoLet n (update ns t) : upd (dropn n ns) ds

294+ upd ns (DoLet fc n t : ds) = DoLet fc n (update ns t) : upd (dropn n ns) ds

295 update ns t = t

296

297pName = do i <- getState

@@ -309,15 +309,16 @@ pSimpleExpr syn =

309 try (do symbol "!["; t <- pTerm; lchar ']'

310 return $ PQuote t)

311 <|> try (do lchar '?'; x <- pName; return (PMetavar x))

312− <|> try (do reserved "return"; return PReturn)

312+ <|> try (do fc <- pfc; reserved "return"; return (PReturn fc))

313− <|> try (do x <- pfName; return (PRef x))

313+ <|> try (do fc <- pfc; x <- pfName; return (PRef fc x))

314− <|> try (do lchar '('; l <- pExpr syn; lchar ','; r <- pExpr syn; lchar ')';

314+ <|> try (do lchar '('; l <- pExpr syn; lchar ','; fc <- pfc

315+ r <- pExpr syn; lchar ')';

315− return (PPair l r))

316+ return (PPair fc l r))

316 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

317 <|> try (do lchar '('; e <- pExpr syn; lchar ')'; return e)

317 <|> try (do c <- pConstant; return (PConstant c))

318 <|> try (do c <- pConstant; return (PConstant c))

318 <|> try (do reserved "Set"; return PSet)

319 <|> try (do reserved "Set"; return PSet)

319− <|> try (do symbol "()"; return PTrue)

320+ <|> try (do fc <- pfc; symbol "()"; return (PTrue fc))

320− <|> try (do symbol "_|_"; return PFalse)

321+ <|> try (do fc <- pfc; symbol "_|_"; return (PFalse fc))

321 <|> try (do lchar '_'; return Placeholder)

322 <|> try (do lchar '_'; return Placeholder)

322

323

323pHSimpleExpr syn

324pHSimpleExpr syn

@@ -327,8 +328,9 @@ pHSimpleExpr syn

327 return $ PHidden e

328 return $ PHidden e

328

329

329pApp syn = do f <- pSimpleExpr syn

330pApp syn = do f <- pSimpleExpr syn

331+ fc <- pfc

330 args <- many1 (pArg syn)

332 args <- many1 (pArg syn)

331− return (PApp f args)

333+ return (PApp fc f args)

332

334

333pArg :: SyntaxInfo -> IParser PArg

335pArg :: SyntaxInfo -> IParser PArg

334pArg syn = pImplicitArg syn

336pArg syn = pImplicitArg syn

@@ -336,7 +338,8 @@ pArg syn = pImplicitArg syn

336 return (PExp e)

338 return (PExp e)

337

339

338pImplicitArg syn = do lchar '{'; n <- pName

340pImplicitArg syn = do lchar '{'; n <- pName

341+ fc <- pfc

339− v <- option (PRef n) (do lchar '='; pExpr syn)

342+ v <- option (PRef fc n) (do lchar '='; pExpr syn)

340 lchar '}'

343 lchar '}'

341 return (PImp n v)

344 return (PImp n v)

342

345

@@ -375,11 +378,14 @@ pDoBlock syn

375 return (PDoBlock ds)

378 return (PDoBlock ds)

376

379

377pDo syn

380pDo syn

381+ = try (do fc <- pfc

378− = try (do i <- pName; symbol "<-"; e <- pExpr syn;

382+ i <- pName; symbol "<-"; e <- pExpr syn;

379− return (DoBind i e))

383+ return (DoBind fc i e))

384+ <|> try (do fc <- pfc

380− <|> try (do reserved "let"; i <- pName; reservedOp "="; e <- pExpr syn

385+ reserved "let"; i <- pName; reservedOp "="; e <- pExpr syn

381− return (DoLet i e))

386+ return (DoLet fc i e))

387+ <|> try (do fc <- pfc

382− <|> try (do e <- pExpr syn; return (DoExp e))

388+ e <- pExpr syn; return (DoExp fc e))

383

389

384pConstant :: IParser Const

390pConstant :: IParser Const

385pConstant = do reserved "Int"; return IType

391pConstant = do reserved "Int"; return IType

@@ -393,23 +399,25 @@ pConstant = do reserved "Int"; return IType

393 <|> try (do c <- chlit; return $ Ch c)

399 <|> try (do c <- chlit; return $ Ch c)

394

400

395table fixes

401table fixes

396− = [[prefix "-" (\x -> PApp (PRef (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

402+ = [[prefix "-" (\fc x -> PApp fc (PRef fc (UN ["-"])) [PExp (PConstant (I 0)), PExp x])]]

397 ++ toTable (reverse fixes) ++

403 ++ toTable (reverse fixes) ++

398− [[binary "=" (\x y -> PApp (PRef (UN ["="])) [PExp x,PExp y]) AssocLeft],

404+ [[binary "=" (\fc x y -> PApp fc (PRef fc (UN ["="])) [PExp x,PExp y]) AssocLeft],

399− [binary "->" (PPi Exp (MN 0 "X")) AssocRight]]

405+ [binary "->" (\fc x y -> PPi Exp (MN 0 "X") x y) AssocRight]]

400

406

401toTable fs = map (map toBin)

407toTable fs = map (map toBin)

402 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

408 (groupBy (\ (Fix x _) (Fix y _) -> prec x == prec y) fs)

403 where toBin (Fix (PrefixN _) op) = prefix op

409 where toBin (Fix (PrefixN _) op) = prefix op

404− (\x -> PApp (PRef (UN [op])) [PExp x])

410+ (\fc x -> PApp fc (PRef fc (UN [op])) [PExp x])

405− toBin (Fix f op) = binary op

411+ toBin (Fix f op)

406− (\x y -> PApp (PRef (UN [op])) [PExp x,PExp y]) (assoc f)

412+ = binary op (\fc x y -> PApp fc (PRef fc (UN [op])) [PExp x,PExp y]) (assoc f)

407 assoc (Infixl _) = AssocLeft

413 assoc (Infixl _) = AssocLeft

408 assoc (Infixr _) = AssocRight

414 assoc (Infixr _) = AssocRight

409 assoc (InfixN _) = AssocNone

415 assoc (InfixN _) = AssocNone

410

416

417+binary name f assoc = Infix (do { fc <- pfc;

411−binary name f assoc = Infix (do { reservedOp name; return f }) assoc

418+ reservedOp name; return (f fc) }) assoc

419+prefix name f = Prefix (do { fc <- pfc;

412−prefix name f = Prefix (do { reservedOp name; return f })

420+ reservedOp name; return (f fc) })

413

421

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

422--------- Data declarations ---------

415

423

@@ -426,7 +434,7 @@ pData syn = try (do fc <- pfc

426 lchar '='

434 lchar '='

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

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

428 lchar ';'

436 lchar ';'

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

437+ let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

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

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

431 ty' <- implicit syn tyn ty

439 ty' <- implicit syn tyn ty

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

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

@@ -435,8 +443,8 @@ pData syn = try (do fc <- pfc

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

443 return (x, cty', cfc)) cons

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

444 return $ PData fc (PDatadecl tyn ty' cons')

437

445

438−mkPApp t [] = t

446+mkPApp fc t [] = t

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

447+mkPApp fc t xs = PApp fc t (map PExp xs)

440

448

441bindArgs :: [PTerm] -> PTerm -> PTerm

449bindArgs :: [PTerm] -> PTerm -> PTerm

442bindArgs [] t = t

450bindArgs [] t = t

@@ -467,19 +475,22 @@ pClause :: SyntaxInfo -> IParser PClause

467pClause syn

475pClause syn

468 = try (do n <- pfName

476 = try (do n <- pfName

469 iargs <- many (pImplicitArg syn)

477 iargs <- many (pImplicitArg syn)

478+ fc <- pfc

470 args <- many (pHSimpleExpr syn)

479 args <- many (pHSimpleExpr syn)

471 lchar '='

480 lchar '='

472 rhs <- pExpr syn

481 rhs <- pExpr syn

473 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

482 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

483+ return $ PClause n (PApp fc (PRef fc n)

474− return $ PClause n (PApp (PRef n) (iargs ++ map PExp args)) rhs wheres)

484+ (iargs ++ map PExp args)) rhs wheres)

475 <|> do l <- pSimpleExpr syn

485 <|> do l <- pSimpleExpr syn

476 op <- operator

486 op <- operator

477 let n = UN [op]

487 let n = UN [op]

478 r <- pSimpleExpr syn

488 r <- pSimpleExpr syn

489+ fc <- pfc

479 lchar '='

490 lchar '='

480 rhs <- pExpr syn

491 rhs <- pExpr syn

481 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

492 wheres <- choice [pWhereblock syn, do lchar ';'; return []]

482− return $ PClause n (PApp (PRef n) [PExp l,PExp r]) rhs wheres

493+ return $ PClause n (PApp fc (PRef fc n) [PExp l,PExp r]) rhs wheres

483

494

484pWhereblock :: SyntaxInfo -> IParser [PDecl]

495pWhereblock :: SyntaxInfo -> IParser [PDecl]

485pWhereblock syn = do reserved "where"; lchar '{'

496pWhereblock syn = do reserved "where"; lchar '{'

@@ -503,19 +514,21 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in

503expandDo :: DSL -> PTerm -> PTerm

514expandDo :: DSL -> PTerm -> PTerm

504expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

515expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

505expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

516expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

506−expandDo dsl (PApp t args) = PApp (expandDo dsl t)

517+expandDo dsl (PApp fc t args) = PApp fc (expandDo dsl t)

507− (map (fmap (expandDo dsl)) args)

518+ (map (fmap (expandDo dsl)) args)

508−expandDo dsl (PPair l r) = PPair (expandDo dsl l) (expandDo dsl r)

519+expandDo dsl (PPair fc l r) = PPair fc (expandDo dsl l) (expandDo dsl r)

509expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

520expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

510−expandDo dsl PReturn = PRef (dsl_return dsl)

521+expandDo dsl (PReturn fc) = PRef fc (dsl_return dsl)

511expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

522expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

512 where

523 where

513− block b [DoExp tm] = tm

524+ block b [DoExp fc tm] = tm

514 block b [a] = PElabError "Last statement in do block must be an expression"

525 block b [a] = PElabError "Last statement in do block must be an expression"

515− block b (DoBind n tm : rest)

526+ block b (DoBind fc n tm : rest)

516− = PApp (PRef b) [PExp tm, PExp (PLam n Placeholder (block b rest))]

527+ = PApp fc (PRef fc b) [PExp tm, PExp (PLam n Placeholder (block b rest))]

517− block b (DoExp tm : rest)

528+ block b (DoExp fc tm : rest)

529+ = PApp fc (PRef fc b)

530+ [PExp tm,

518− = PApp (PRef b) [PExp tm, PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]

531+ PExp (PLam (MN 0 "bindx") Placeholder (block b rest))]

519expandDo dsl t = t

532expandDo dsl t = t

520

533

521

534