ed72247 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Try to get line numbers better

commited722479bd828e045d1f7f671182264e86f32d69 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 2 Feb 2012, 10:57 (15 years ago) parentb04ea13

5 files changed+61−59

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+18−18 src/Idris/Coverage.hs+2−2 src/Idris/ElabDecls.hs+20−20 src/Idris/ElabTerm.hs+1−1 src/Idris/Parser.hs+20−18

src/Idris/AbsSyntax.hs+18−18

@@ -417,10 +417,10 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

417417 | PDirective (Idris ())

418418 deriving Functor

419419

420−data PClause' t = PClause Name t [t] t [PDecl' t]

421− | PWith Name t [t] t [PDecl' t]

422− | PClauseR [t] t [PDecl' t]

423− | PWithR [t] t [PDecl' t]

420+data PClause' t = PClause FC Name t [t] t [PDecl' t]

421+ | PWith FC Name t [t] t [PDecl' t]

422+ | PClauseR FC [t] t [PDecl' t]

423+ | PWithR FC [t] t [PDecl' t]

424424 deriving Functor

425425

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

@@ -691,13 +691,13 @@ showDeclImp _ (PClauses _ _ n c) = showSep "\n" (map show c)

691691showDeclImp _ (PData _ _ d) = show d

692692

693693showCImp :: Bool -> PClause -> String

694−showCImp impl (PClause n l ws r w)

694+showCImp impl (PClause _ n l ws r w)

695695 = showImp impl l ++ showWs ws ++ " = " ++ showImp impl r

696696 ++ " where " ++ show w

697697 where

698698 showWs [] = ""

699699 showWs (x : xs) = " | " ++ showImp impl x ++ showWs xs

700−showCImp impl (PWith n l ws r w)

700+showCImp impl (PWith _ n l ws r w)

701701 = showImp impl l ++ showWs ws ++ " with " ++ showImp impl r

702702 ++ " { " ++ show w ++ " } "

703703 where

@@ -732,8 +732,8 @@ getAll = map getTm

732732showImp :: Bool -> PTerm -> String

733733showImp impl tm = se 10 tm where

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

735− se p (PRef _ n) = if impl then show n

736− else showbasic n

735+ se p (PRef fc n) = if impl then show n ++ "[" ++ show fc ++ "]"

736+ else showbasic n

737737 where showbasic n@(UN _) = show n

738738 showbasic (MN _ s) = s

739739 showbasic (NS n s) = showSep "." (reverse s) ++ "." ++ showbasic n

@@ -982,22 +982,22 @@ expandParamsD ist dec ps ns (PClauses fc opts n cs)

982982 = let n' = if n `elem` ns then dec n else n in

983983 PClauses fc opts n' (map expandParamsC cs)

984984 where

985− expandParamsC (PClause n lhs ws rhs ds)

985+ expandParamsC (PClause fc n lhs ws rhs ds)

986986 = let -- ps' = updateps True (namesIn ist rhs) (zip ps [0..])

987987 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

988988 n' = if n `elem` ns then dec n else n in

989− PClause n' (expandParams dec ps'' ns lhs)

990− (map (expandParams dec ps'' ns) ws)

991− (expandParams dec ps'' ns rhs)

992− (map (expandParamsD ist dec ps'' ns) ds)

993− expandParamsC (PWith n lhs ws wval ds)

989+ PClause fc n' (expandParams dec ps'' ns lhs)

990+ (map (expandParams dec ps'' ns) ws)

991+ (expandParams dec ps'' ns rhs)

992+ (map (expandParamsD ist dec ps'' ns) ds)

993+ expandParamsC (PWith fc n lhs ws wval ds)

994994 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])

995995 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

996996 n' = if n `elem` ns then dec n else n in

997− PWith n' (expandParams dec ps'' ns lhs)

998− (map (expandParams dec ps'' ns) ws)

999− (expandParams dec ps'' ns wval)

1000− (map (expandParamsD ist dec ps'' ns) ds)

997+ PWith fc n' (expandParams dec ps'' ns lhs)

998+ (map (expandParams dec ps'' ns) ws)

999+ (expandParams dec ps'' ns wval)

1000+ (map (expandParamsD ist dec ps'' ns) ds)

10011001 updateps yn nm [] = []

10021002 updateps yn nm (((a, t), i):as)

10031003 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

src/Idris/Coverage.hs+2−2

@@ -44,8 +44,8 @@ genClauses fc n xs given

4444 | (f, args) <- unApply term = map (\t -> delab' i t True) args

4545 | otherwise = []

4646

47− lhsApp (PClause _ l _ _ _) = l

48− lhsApp (PWith _ l _ _ _) = l

47+ lhsApp (PClause _ _ l _ _ _) = l

48+ lhsApp (PWith _ _ l _ _ _) = l

4949

5050 mnub i [] = []

5151 mnub i (x : xs) =

src/Idris/ElabDecls.hs+20−20

@@ -159,7 +159,7 @@ elabRecord info syn fc tyn ty cn cty

159159 let lhs = PApp fc (PRef fc pn)

160160 [pexp (PApp fc (PRef fc cn) iargs)]

161161 let rhs = PRef fc (mkp pn)

162− let pclause = PClause pn lhs [] rhs []

162+ let pclause = PClause fc pn lhs [] rhs []

163163 return [pfnTy, PClauses fc [] pn [pclause]]

164164

165165 implicitise (pa, t) = pa { getTm = t }

@@ -175,7 +175,7 @@ elabRecord info syn fc tyn ty cn cty

175175 let rhsArgs = take pos pls ++ (PRef fc valname) :

176176 drop (pos + 1) pls

177177 let before = pos

178− let pclause = PClause setname (PApp fc (PRef fc setname)

178+ let pclause = PClause fc setname (PApp fc (PRef fc setname)

179179 [pexp (PRef fc valname),

180180 pexp (PApp fc (PRef fc cn)

181181 (map pexp lhsArgs))])

@@ -214,7 +214,7 @@ elabCon info syn tn (n, t_in, fc)

214214

215215elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

216216elabClauses info fc opts n_in cs = let n = liftname info n_in in

217− do pats_in <- mapM (elabClause info fc (TCGen `elem` opts)) cs

217+ do pats_in <- mapM (elabClause info (TCGen `elem` opts)) cs

218218 solveDeferred n

219219 let pats = mapMaybe id pats_in

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

@@ -340,19 +340,19 @@ checkPossible info fc tcgen fname lhs_in

340340-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

341341 Error _ -> return False

342342

343−elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

344−elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

343+elabClause :: ElabInfo -> Bool -> PClause -> Idris (Maybe (Term, Term))

344+elabClause info tcgen (PClause fc fname lhs_in [] PImpossible [])

345345 = do b <- checkPossible info fc tcgen fname lhs_in

346346 case b of

347347 True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

348348 False -> return Nothing

349−elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

349+elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

350350 = do ctxt <- getContext

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

352352 -- pattern bindings

353353 i <- get

354354 let lhs = addImplPat i lhs_in

355− logLvl 5 ("LHS: " ++ showImp True lhs)

355+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp True lhs)

356356 ((lhs', dlhs, []), _) <-

357357 tclift $ elaborate ctxt (MN 0 "patLHS") infP []

358358 (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

@@ -411,7 +411,7 @@ elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

411411 -- _ -> MN i (show n)) . l

412412 }

413413

414−elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

414+elabClause info tcgen (PWith fc fname lhs_in withs wval_in withblock)

415415 = do ctxt <- getContext

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

417417 -- pattern bindings

@@ -491,7 +491,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

491491 | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n

492492 mkAuxC wname lhs ns d = return $ d

493493

494− mkAux wname toplhs ns (PClause n tm_in (w:ws) rhs wheres)

494+ mkAux wname toplhs ns (PClause fc n tm_in (w:ws) rhs wheres)

495495 = do i <- get

496496 let tm = addImpl i tm_in

497497 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

@@ -500,8 +500,8 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

500500 Left _ -> fail $ show fc ++ "with clause does not match top level"

501501 Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

502502 lhs <- updateLHS n wname mvars ns (fullApp tm) w

503− return $ PClause wname lhs ws rhs wheres

504− mkAux wname toplhs ns (PWith n tm_in (w:ws) wval withs)

503+ return $ PClause fc wname lhs ws rhs wheres

504+ mkAux wname toplhs ns (PWith fc n tm_in (w:ws) wval withs)

505505 = do i <- get

506506 let tm = addImpl i tm_in

507507 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

@@ -510,7 +510,7 @@ elabClause info fc tcgen (PWith fname lhs_in withs wval_in withblock)

510510 case matchClause i toplhs tm of

511511 Left _ -> fail $ show fc ++ "with clause does not match top level"

512512 Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

513− return $ PWith wname lhs ws wval withs'

513+ return $ PWith fc wname lhs ws wval withs'

514514

515515 updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

516516 = return $ substMatches mvars $

@@ -597,7 +597,7 @@ elabClass info syn fc constraints tn ps ds

597597 iLOG (showImp True ty)

598598 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

599599 return [PTy syn fc [] cfn ty,

600− PClauses fc [Inlinable,TCGen] cfn [PClause cfn lhs [] rhs []]]

600+ PClauses fc [Inlinable,TCGen] cfn [PClause fc cfn lhs [] rhs []]]

601601

602602 tfun cn c syn all (m, (o, ty))

603603 = do let ty' = insertConstraint c ty

@@ -611,7 +611,7 @@ elabClass info syn fc constraints tn ps ds

611611 iLOG (show (m, ty', capp, margs))

612612 iLOG (showImp True lhs ++ " = " ++ showImp True rhs)

613613 return [PTy syn fc o m ty',

614− PClauses fc [Inlinable,TCGen] m [PClause m lhs [] rhs []]]

614+ PClauses fc [Inlinable,TCGen] m [PClause fc m lhs [] rhs []]]

615615

616616 getMArgs (PPi (Imp _ _) n ty sc) = IA : getMArgs sc

617617 getMArgs (PPi (Exp _ _) n ty sc) = EA : getMArgs sc

@@ -649,7 +649,7 @@ elabInstance info syn fc cs n ps t ds

649649 = do i <- get

650650 (n, ci) <- case lookupCtxtName (namespace info) n (idris_classes i) of

651651 [c] -> return c

652− _ -> fail $ show n ++ " is not a type class"

652+ _ -> fail $ show fc ++ ":" ++ show n ++ " is not a type class"

653653 let iname = UN ('@':show n ++ "$" ++ show ps)

654654 elabType info syn fc [] iname t

655655 let ips = zip (class_params ci) ps

@@ -678,7 +678,7 @@ elabInstance info syn fc cs n ps t ds

678678 let rhs = PApp fc (PRef fc (instanceName ci))

679679 (map (pexp . mkMethApp) mtys)

680680 let idecl = PClauses fc [Inlinable, TCGen] iname

681− [PClause iname lhs [] rhs wb]

681+ [PClause fc iname lhs [] rhs wb]

682682 iLOG (show idecl)

683683 elabDecl info idecl

684684 where

@@ -727,8 +727,8 @@ elabInstance info syn fc cs n ps t ds

727727 insertDef meth def ns decls

728728 | null $ filter (clauseFor meth ns) decls

729729 = decls ++ [PClauses fc [Inlinable,TCGen] meth

730− [PClause meth (PApp fc (PRef fc meth) []) []

731− (PApp fc (PRef fc def) []) []]]

730+ [PClause fc meth (PApp fc (PRef fc meth) []) []

731+ (PApp fc (PRef fc def) []) []]]

732732 | otherwise = decls

733733

734734 warnMissing decls ns meth

@@ -742,8 +742,8 @@ elabInstance info syn fc cs n ps t ds

742742decorateid decorate (PTy s f o n t) = PTy s f o (decorate n) t

743743decorateid decorate (PClauses f o n cs)

744744 = PClauses f o (decorate n) (map dc cs)

745− where dc (PClause n t as w ds) = PClause (decorate n) (dappname t) as w ds

746− dc (PWith n t as w ds) = PWith (decorate n) (dappname t) as w

745+ where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

746+ dc (PWith fc n t as w ds) = PWith fc (decorate n) (dappname t) as w

747747 (map (decorateid decorate) ds)

748748 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

749749 dappname t = t

src/Idris/ElabTerm.hs+1−1

@@ -291,7 +291,7 @@ elab ist info pattern tcgen fn tm

291291 where -- mkarg (MN _ _) = Placeholder

292292 mkarg n = PRef fc n

293293 mkClause args (l, r)

294− = PClause n (PApp fc (PRef fc n)

294+ = PClause fc n (PApp fc (PRef fc n)

295295 (map pexp args ++ [pexp l])) [] r []

296296

297297 elabArgs ina failed retry [] _

src/Idris/Parser.hs+20−18

@@ -280,14 +280,14 @@ parseProg syn fname input pos

280280collect :: [PDecl] -> [PDecl]

281281collect (c@(PClauses _ o _ _) : ds)

282282 = clauses (cname c) [] (c : ds)

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

284− | n == n' = clauses n (PClause n' l ws r (collect w) : acc) ds

285− clauses n acc (PClauses fc _ _ [PWith n' l ws r w] : ds)

286− | n == n' = clauses n (PWith n' l ws r (collect w) : acc) ds

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

284+ | n == n' = clauses n (PClause fc' n' l ws r (collect w) : acc) ds

285+ clauses n acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)

286+ | n == n' = clauses n (PWith fc' n' l ws r (collect w) : acc) ds

287287 clauses n acc xs = PClauses (getfc c) o n (reverse acc) : collect xs

288288

289− cname (PClauses fc _ _ [PClause n _ _ _ _]) = n

290− cname (PClauses fc _ _ [PWith n _ _ _ _]) = n

289+ cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = n

290+ cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = n

291291 getfc (PClauses fc _ _ _) = fc

292292

293293collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

@@ -1087,8 +1087,8 @@ pOverload syn = do o <- identifier <|> do reserved "let"; return "let"

10871087--------- Pattern match clauses ---------

10881088

10891089pPattern :: SyntaxInfo -> IParser PDecl

1090−pPattern syn = do clause <- pClause syn

1091− fc <- pfc

1090+pPattern syn = do fc <- pfc

1091+ clause <- pClause syn

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

10931093

10941094pArgExpr syn = let syn' = syn { inPattern = True } in

@@ -1125,13 +1125,14 @@ pClause syn

11251125 (iargs ++ cargs ++ map pexp args)

11261126 ist <- getState

11271127 setState (ist { lastParse = Just n })

1128− return $ PClause n capp wargs rhs wheres)

1128+ return $ PClause fc n capp wargs rhs wheres)

11291129 <|> try (do push_indent

11301130 wargs <- many1 (pWExpr syn)

11311131 ist <- getState

11321132 n <- case lastParse ist of

11331133 Just t -> return t

11341134 Nothing -> fail "Invalid clause"

1135+ fc <- pfc

11351136 rhs <- pRHS syn n

11361137 let ctxt = tt_ctxt ist

11371138 let wsyn = syn { syn_namespace = [] }

@@ -1140,7 +1141,7 @@ pClause syn

11401141 return x,

11411142 do pTerminator

11421143 return ([], [])]

1143− return $ PClauseR wargs rhs wheres)

1144+ return $ PClauseR fc wargs rhs wheres)

11441145

11451146 <|> try (do push_indent

11461147 n_in <- pfName; let n = expandNS syn n_in

@@ -1160,16 +1161,17 @@ pClause syn

11601161 ist <- getState

11611162 setState (ist { lastParse = Just n })

11621163 pop_indent

1163− return $ PWith n capp wargs wval withs)

1164+ return $ PWith fc n capp wargs wval withs)

11641165

11651166 <|> try (do wargs <- many1 (pWExpr syn)

1167+ fc <- pfc

11661168 reserved "with"

11671169 wval <- pSimpleExpr syn

11681170 open_block

11691171 ds <- many1 $ pFunDecl syn

11701172 let withs = concat ds

11711173 close_block

1172− return $ PWithR wargs wval withs)

1174+ return $ PWithR fc wargs wval withs)

11731175

11741176 <|> do push_indent

11751177 l <- pArgExpr syn

@@ -1188,7 +1190,7 @@ pClause syn

11881190 ist <- getState

11891191 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

11901192 setState (ist { lastParse = Just n })

1191− return $ PClause n capp wargs rhs wheres

1193+ return $ PClause fc n capp wargs rhs wheres

11921194

11931195 <|> do l <- pArgExpr syn

11941196 op <- operator

@@ -1205,12 +1207,12 @@ pClause syn

12051207 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

12061208 let withs = map (fillLHSD n capp wargs) $ concat ds

12071209 setState (ist { lastParse = Just n })

1208− return $ PWith n capp wargs wval withs

1210+ return $ PWith fc n capp wargs wval withs

12091211 where

1210− fillLHS n capp owargs (PClauseR wargs v ws)

1211− = PClause n capp (owargs ++ wargs) v ws

1212− fillLHS n capp owargs (PWithR wargs v ws)

1213− = PWith n capp (owargs ++ wargs) v

1212+ fillLHS n capp owargs (PClauseR fc wargs v ws)

1213+ = PClause fc n capp (owargs ++ wargs) v ws

1214+ fillLHS n capp owargs (PWithR fc wargs v ws)

1215+ = PWith fc n capp (owargs ++ wargs) v

12141216 (map (fillLHSD n capp (owargs ++ wargs)) ws)

12151217 fillLHS _ _ _ c = c

12161218