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

git.iko.soy/Idris-dev

Propagate line numbers through applications and variables

commit5f7eed8804c5472af78faa817ba18ee8dcd25b9a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSun 23 Oct 2011, 21:23 (15 years ago) parentec87a69

4 files changed+135−117

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+47−47 src/Idris/Delaborate.hs+12−10 src/Idris/ElabDecls.hs+20−17 src/Idris/Parser.hs+56−43

src/Idris/AbsSyntax.hs+47−47

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

169169-- High level language terms

170170--

171171data PTerm = PQuote Raw

172− | PRef Name

172+ | PRef FC Name

173173 | PLam Name PTerm PTerm

174174 | PPi Plicity Name PTerm PTerm

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

176− | PApp PTerm [PArg]

177− | PTrue

178− | PFalse

179− | PPair PTerm PTerm

176+ | PApp FC PTerm [PArg]

177+ | PTrue FC

178+ | PFalse FC

179+ | PPair FC PTerm PTerm

180180 | PHidden PTerm -- irrelevant or hidden pattern

181181 | PSet

182182 | PConstant Const

183183 | Placeholder

184184 | PDoBlock [PDo]

185− | PReturn

185+ | PReturn FC

186186 | PMetavar Name

187187 | PElabError String -- error to report on elaboration

188188

189−data PDo = DoExp PTerm

190− | DoBind Name PTerm

191− | DoLet Name PTerm

189+data PDo = DoExp FC PTerm

190+ | DoBind FC Name PTerm

191+ | DoLet FC Name PTerm

192192

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

194194 | PExp { getTm :: t }

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

261261showImp :: Bool -> PTerm -> String

262262showImp impl tm = se 10 tm where

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

264− se p (PRef n) = show n

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

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

266266 se p (PPi Exp n ty sc)

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

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

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

273273 "} -> " ++ se 10 sc

274274 | otherwise = se 10 sc

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

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

276276 | not impl = show f

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

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

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

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

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

281− se p (PApp f as)

281+ se p (PApp _ f as)

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

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

284284 ++ concatMap seArg args

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

286− se p PTrue = "()"

287− se p PFalse = "_|_"

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

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

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

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

289289 se p PSet = "Set"

290290 se p (PConstant c) = show c

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

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

300300allNamesIn :: PTerm -> [Name]

301301allNamesIn tm = nub $ ni [] tm

302302 where

303− ni env (PRef n)

303+ ni env (PRef _ n)

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

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

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

308308 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

310310 ni env _ = []

311311

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

313313namesIn ist tm = nub $ ni [] tm

314314 where

315− ni env (PRef n)

315+ ni env (PRef _ n)

316316 | not (n `elem` env)

317317 = case lookupCtxt n (idris_implicits ist) of

318318 Nothing -> [n]

319319 _ -> []

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)

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

322322 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

324324 ni env (PHidden tm) = ni env tm

325325 ni env _ = []

326326

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

333333inferDecl = PDatadecl inferTy

334334 PSet

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

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

337− (PRef inferTy)), bi)]

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

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

338338

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]

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

341341

342342getInferTerm, getInferType :: Term -> Term

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

353353unitTy = MN 0 "__Unit"

354354unitCon = MN 0 "__II"

355355unitDecl = PDatadecl unitTy PSet

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

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

357357

358358falseTy = MN 0 "__False"

359359falseDecl = PDatadecl falseTy PSet []

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

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

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

365365 PPi Imp (n "B") PSet (

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

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

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

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

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

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

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

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

370370 where n a = MN 0 a

371371

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

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

388388 then (tm, reverse declimps)

389389 else implicitise syn ist (pibind uvars ns tm)

390390 where

391− imps top env (PApp f as)

391+ imps top env (PApp _ f as)

392392 = do (decls, ns) <- get

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

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

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

399399 imps True (n:env) sc

400400 imps top env (PPi Exp n ty sc)

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

402− (PRef x) -> namesIn ist sc

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

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

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

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

406406 imps True (n:env) sc

407− imps top env (PPair l r)

407+ imps top env (PPair _ l r)

408408 = do (decls, ns) <- get

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

410410 imps top env (PLam n ty sc)

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

423423addImpl :: IState -> PTerm -> PTerm

424424addImpl ist ptm = ai [] ptm

425425 where

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

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

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

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

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

429− aiFn env (PRef f) as'

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

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

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

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

432− aiFn env f' as'

432+ aiFn fc env f' as'

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

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

435435 PLam n ty' sc'

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

439439 ai env (PHidden tm) = PHidden (ai env tm)

440440 ai env tm = tm

441441

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

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

443443 = case lookupCtxt f (idris_implicits ist) of

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

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

446− aiFn env f as = pApp 1 f as

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

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

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

447447

448− pApp a f [] = f

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

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

448+ pApp fc a f [] = f

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

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

451451

452− appRest f [] = f

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

452+ appRest fc f [] = f

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

454454

455455 insertImpl :: [PArg] -> [PArg] -> [PArg]

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

src/Idris/Delaborate.hs+12−10

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

1313delab :: IState -> Term -> PTerm

1414delab ist tm = de [] tm

1515 where

16+ un = FC "(val)" 0

17+

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

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

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

19− | n == unitCon = PTrue

20− | n == falseTy = PFalse

21− | otherwise = PRef n

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

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

21+ | n == unitCon = PTrue un

22+ | n == falseTy = PFalse un

23+ | otherwise = PRef un n

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

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

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

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

2830 de env (Set i) = PSet

2931

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

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

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

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

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

3537

3638 mkPApp n args

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

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

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

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

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

4042

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

4244 imp (PExp _) arg = PExp arg

src/Idris/ElabDecls.hs+20−17

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

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

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

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

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

213− (elab' (PRef unitTy))

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

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

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

213+ (elab' (PRef fc unitTy))

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

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

216216 [PExp l,PExp r]))

217− (elab' (PApp (PRef pairCon)

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

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

219219 PImp (MN 0 "a") Placeholder,

220220 PExp l, PExp r]))

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

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

223− (patvar n)

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

222+ = erun fc $

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

224+ (patvar n)

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

225226 Nothing -> False

226227 _ -> True

227− elab' (PRef n)

228+ elab' (PRef fc n)

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

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

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

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

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

231232 elab' (PLam n Placeholder sc)

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

233234 elab' (PPi _ n Placeholder sc)

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

240241 elab' ty

241242 elab' sc

242243 solve

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

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

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

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

246− | otherwise = elabApp f args

246+ = erun fc $

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

248+ | otherwise = erun fc $ elabApp f args

247249 where elabApp f args

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

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

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

251253 elabArgs ns (map getTm args))

252254 (do apply_elab f (map toElab args)

253255 solve)

254− elab' (PApp f [arg])

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

256− solve

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

257+ = erun fc $

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

259+ solve

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

258261 movelast h

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

src/Idris/Parser.hs+56−43

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

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

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

280280

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

282− Just t -> t

283− _ -> PRef n

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

282+ Just t -> t

283+ _ -> PRef fc n

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

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

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

287287 (update (dropn n ns) sc)

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

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

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

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

290290 update ns (PHidden t) = PHidden (update ns t)

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

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

293− upd ns (DoBind n t : ds) = DoBind 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

292+ where upd ns (DoExp fc t : ds) = DoExp fc (update ns t) : upd 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 fc n t : ds) = DoLet fc n (update ns t) : upd (dropn n ns) ds

295295 update ns t = t

296296

297297pName = do i <- getState

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

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

310310 return $ PQuote t)

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

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

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

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

315− return (PPair l r))

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

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

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

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

316+ return (PPair fc l r))

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

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

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

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

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

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

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

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

322323

323324pHSimpleExpr syn

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

327328 return $ PHidden e

328329

329330pApp syn = do f <- pSimpleExpr syn

331+ fc <- pfc

330332 args <- many1 (pArg syn)

331− return (PApp f args)

333+ return (PApp fc f args)

332334

333335pArg :: SyntaxInfo -> IParser PArg

334336pArg syn = pImplicitArg syn

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

336338 return (PExp e)

337339

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

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

341+ fc <- pfc

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

340343 lchar '}'

341344 return (PImp n v)

342345

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

375378 return (PDoBlock ds)

376379

377380pDo syn

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

379− return (DoBind i e))

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

381− return (DoLet i e))

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

381+ = try (do fc <- pfc

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

383+ return (DoBind fc i e))

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

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

386+ return (DoLet fc i e))

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

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

383389

384390pConstant :: IParser Const

385391pConstant = do reserved "Int"; return IType

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

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

394400

395401table 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])]]

397403 ++ toTable (reverse fixes) ++

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

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

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

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

400406

401407toTable fs = map (map toBin)

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

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

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

405− toBin (Fix f op) = binary op

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

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

411+ toBin (Fix f op)

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

407413 assoc (Infixl _) = AssocLeft

408414 assoc (Infixr _) = AssocRight

409415 assoc (InfixN _) = AssocNone

410416

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

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

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

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

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

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

413421

414422--------- Data declarations ---------

415423

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

426434 lchar '='

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

428436 lchar ';'

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

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

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

431439 ty' <- implicit syn tyn ty

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

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

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

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

437445

438−mkPApp t [] = t

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

446+mkPApp fc t [] = t

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

440448

441449bindArgs :: [PTerm] -> PTerm -> PTerm

442450bindArgs [] t = t

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

467475pClause syn

468476 = try (do n <- pfName

469477 iargs <- many (pImplicitArg syn)

478+ fc <- pfc

470479 args <- many (pHSimpleExpr syn)

471480 lchar '='

472481 rhs <- pExpr syn

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

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

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

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

475485 <|> do l <- pSimpleExpr syn

476486 op <- operator

477487 let n = UN [op]

478488 r <- pSimpleExpr syn

489+ fc <- pfc

479490 lchar '='

480491 rhs <- pExpr syn

481492 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

483494

484495pWhereblock :: SyntaxInfo -> IParser [PDecl]

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

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

503514expandDo :: DSL -> PTerm -> PTerm

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

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

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

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

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

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

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

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

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

512523 where

513− block b [DoExp tm] = tm

524+ block b [DoExp fc tm] = tm

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

515− block b (DoBind n tm : rest)

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

517− block b (DoExp tm : rest)

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

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

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

528+ block b (DoExp fc tm : rest)

529+ = PApp fc (PRef fc b)

530+ [PExp tm,

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

519532expandDo dsl t = t

520533

521534