ed72247 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Try to get line numbers better

ed72247Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+18−18

compare with master

unifiedsplit

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

417 | PDirective (Idris ())

418 deriving Functor

419

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

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

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

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

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

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

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

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

424 deriving Functor

425

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

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

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

692

693showCImp :: Bool -> PClause -> String

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

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

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

696 ++ " where " ++ show w

697 where

698 showWs [] = ""

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

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

702 ++ " { " ++ show w ++ " } "

703 where

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

732showImp :: Bool -> PTerm -> String

733showImp impl tm = se 10 tm where

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

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

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

736− else showbasic n

736+ else showbasic n

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

738 showbasic (MN _ s) = s

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

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

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

983 PClauses fc opts n' (map expandParamsC cs)

984 where

985− expandParamsC (PClause n lhs ws rhs ds)

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

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

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

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

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

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

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

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

991− (expandParams dec ps'' ns rhs)

991+ (expandParams dec ps'' ns rhs)

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

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

993− expandParamsC (PWith n lhs ws wval ds)

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

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

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

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

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

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

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

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

999− (expandParams dec ps'' ns wval)

999+ (expandParams dec ps'' ns wval)

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

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

1001 updateps yn nm [] = []

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

1003 | (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

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

45 | otherwise = []

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

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

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

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

50 mnub i [] = []

51 mnub i (x : xs) =

src/Idris/ElabDecls.hs+20−20

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

159 let lhs = PApp fc (PRef fc pn)

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

161 let rhs = PRef fc (mkp pn)

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

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

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

164

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

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

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

176 drop (pos + 1) pls

177 let before = pos

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

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

179 [pexp (PRef fc valname),

180 pexp (PApp fc (PRef fc cn)

181 (map pexp lhsArgs))])

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

214

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

216elabClauses 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

218 solveDeferred n

219 let pats = mapMaybe id pats_in

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

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

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

341 Error _ -> return False

342

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

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

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

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

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

346 case b of

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

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

350 = do ctxt <- getContext

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

352 -- pattern bindings

353 i <- get

354 let lhs = addImplPat i lhs_in

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

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

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

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

358 (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)

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

412 }

413

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)

415 = do ctxt <- getContext

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

417 -- pattern bindings

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

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

492 mkAuxC wname lhs ns d = return $ d

493

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)

495 = do i <- get

496 let tm = addImpl i tm_in

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

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

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

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

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

503− return $ PClause wname lhs ws rhs wheres

503+ return $ PClause fc wname lhs ws rhs wheres

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

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

505 = do i <- get

506 let tm = addImpl i tm_in

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

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

510 case matchClause i toplhs tm of

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

512 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'

514

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

516 = return $ substMatches mvars $

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

597 iLOG (showImp True ty)

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

599 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 []]]

601

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

603 = do let ty' = insertConstraint c ty

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

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

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

613 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 []]]

615

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

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

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

649 = do i <- get

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

651 [c] -> return c

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

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

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

654 elabType info syn fc [] iname t

655 let ips = zip (class_params ci) ps

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

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

679 (map (pexp . mkMethApp) mtys)

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

681− [PClause iname lhs [] rhs wb]

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

682 iLOG (show idecl)

683 elabDecl info idecl

684 where

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

727 insertDef meth def ns decls

728 | null $ filter (clauseFor meth ns) decls

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

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

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

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

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

732 | otherwise = decls

733

734 warnMissing decls ns meth

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

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

743decorateid decorate (PClauses f o n cs)

744 = 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

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

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

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

747 (map (decorateid decorate) ds)

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

749 dappname t = t

src/Idris/ElabTerm.hs+1−1

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

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

292 mkarg n = PRef fc n

293 mkClause args (l, r)

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

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

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

296

297 elabArgs ina failed retry [] _

src/Idris/Parser.hs+20−18

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

280collect :: [PDecl] -> [PDecl]

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

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

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

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

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

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

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

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

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

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

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

288

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

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

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

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

291 getfc (PClauses fc _ _ _) = fc

292

293collect (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"

1087--------- Pattern match clauses ---------

1088

1089pPattern :: SyntaxInfo -> IParser PDecl

1090+pPattern syn = do fc <- pfc

1090−pPattern syn = do clause <- pClause syn

1091+ clause <- pClause syn

1091− fc <- pfc

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

1093

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

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

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

1126 ist <- getState

1127 setState (ist { lastParse = Just n })

1128− return $ PClause n capp wargs rhs wheres)

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

1129 <|> try (do push_indent

1130 wargs <- many1 (pWExpr syn)

1131 ist <- getState

1132 n <- case lastParse ist of

1133 Just t -> return t

1134 Nothing -> fail "Invalid clause"

1135+ fc <- pfc

1135 rhs <- pRHS syn n

1136 rhs <- pRHS syn n

1136 let ctxt = tt_ctxt ist

1137 let ctxt = tt_ctxt ist

1137 let wsyn = syn { syn_namespace = [] }

1138 let wsyn = syn { syn_namespace = [] }

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

1140 return x,

1141 return x,

1141 do pTerminator

1142 do pTerminator

1142 return ([], [])]

1143 return ([], [])]

1143− return $ PClauseR wargs rhs wheres)

1144+ return $ PClauseR fc wargs rhs wheres)

1144

1145

1145 <|> try (do push_indent

1146 <|> try (do push_indent

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

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

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

1160 ist <- getState

1161 ist <- getState

1161 setState (ist { lastParse = Just n })

1162 setState (ist { lastParse = Just n })

1162 pop_indent

1163 pop_indent

1163− return $ PWith n capp wargs wval withs)

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

1164

1165

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

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

1167+ fc <- pfc

1166 reserved "with"

1168 reserved "with"

1167 wval <- pSimpleExpr syn

1169 wval <- pSimpleExpr syn

1168 open_block

1170 open_block

1169 ds <- many1 $ pFunDecl syn

1171 ds <- many1 $ pFunDecl syn

1170 let withs = concat ds

1172 let withs = concat ds

1171 close_block

1173 close_block

1172− return $ PWithR wargs wval withs)

1174+ return $ PWithR fc wargs wval withs)

1173

1175

1174 <|> do push_indent

1176 <|> do push_indent

1175 l <- pArgExpr syn

1177 l <- pArgExpr syn

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

1188 ist <- getState

1190 ist <- getState

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

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

1190 setState (ist { lastParse = Just n })

1192 setState (ist { lastParse = Just n })

1191− return $ PClause n capp wargs rhs wheres

1193+ return $ PClause fc n capp wargs rhs wheres

1192

1194

1193 <|> do l <- pArgExpr syn

1195 <|> do l <- pArgExpr syn

1194 op <- operator

1196 op <- operator

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

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

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

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

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

1207 setState (ist { lastParse = Just n })

1209 setState (ist { lastParse = Just n })

1208− return $ PWith n capp wargs wval withs

1210+ return $ PWith fc n capp wargs wval withs

1209 where

1211 where

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

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

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

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

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

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

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

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

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

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

1215 fillLHS _ _ _ c = c

1217 fillLHS _ _ _ c = c

1216

1218