da3a26c · Idris-dev · git.iko.soy

src/Idris/DSL.hs+1−1

compare with master

unifiedsplit

@@ -72,7 +72,7 @@ expandSugar dsl (PAppBind fc t args) = PAppBind fc (expandSugar dsl t)

72expandSugar dsl (PCase fc s opts) = PCase fc (expandSugar dsl s)

73 (map (pmap (expandSugar dsl)) opts)

74expandSugar dsl (PIfThenElse fc c t f) =

75− PApp fc (PRef (FC (fc_fname fc) (fc_start fc) (fc_start fc)) (sUN "ifThenElse"))

75+ PApp fc (PRef NoFC (sUN "ifThenElse"))

76 [ PExp 0 [] (sMN 0 "condition") $ expandSugar dsl c

77 , PExp 0 [] (sMN 0 "whenTrue") $ expandSugar dsl t

78 , PExp 0 [] (sMN 0 "whenFalse") $ expandSugar dsl f

src/Idris/Elab/Term.hs+24−8

@@ -343,8 +343,7 @@ elab ist info emode opts fn tm

343 do hnf_compute

344 g <- goal

345 case g of

346− TType _ -> do highlightSource fc (AnnName unitTy Nothing Nothing Nothing)

347− elab' ina (Just fc) (PRef fc unitTy)

346+ TType _ -> elab' ina (Just fc) (PRef fc unitTy)

348 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

347 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

349 _ -> elab' ina (Just fc) (PRef fc unitCon)

348 _ -> elab' ina (Just fc) (PRef fc unitCon)

350 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

349 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

@@ -353,8 +352,9 @@ elab ist info emode opts fn tm

353 = do c <- getNameFrom (sMN 0 "class")

352 = do c <- getNameFrom (sMN 0 "class")

354 instanceArg c

353 instanceArg c

355 elab' ina _ (PRefl fc t)

354 elab' ina _ (PRefl fc t)

356− = elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

355+ = do elab' ina (Just fc) (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,

357− pimp (sMN 0 "x") t False])

356+ pimp (sMN 0 "x") t False])

357+ highlightSource fc (AnnName eqCon Nothing Nothing Nothing)

358 elab' ina _ (PEq fc Placeholder Placeholder l r)

359 = try (do tyn <- getNameFrom (sMN 0 "aqty")

360 claim tyn RType

@@ -427,7 +427,7 @@ elab ist info emode opts fn tm

427 [pimp (sMN 0 "a") t False,

428 pimp (sMN 0 "P") Placeholder True,

429 pexp l, pexp r])

430− elab' ina fc (PAlternative True as)

430+ elab' ina fc (PAlternative True as)

431 = do hnf_compute

432 ty <- goal

433 ctxt <- get_context

@@ -490,13 +490,17 @@ elab ist info emode opts fn tm

490 = lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

491 | pattern && not reflection && not (e_qq ina) && e_nomatching ina

492 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

493− | otherwise =

493+ | otherwise =

494 do fty <- get_type (Var n) -- check for implicits

495 ctxt <- get_context

496− env <- get_env

496+ env <- get_env

497 let a' = insertScopedImps fc (normalise ctxt env fty) []

498 if null a'

499+ then erun fc $

499− then erun fc $ do apply (Var n) []; solve

500+ do apply (Var n) []

501+ hl <- findHighlight n

502+ solve

503+ highlightSource fc hl

500 else elab' ina fc' (PApp fc tm [])

504 else elab' ina fc' (PApp fc tm [])

501 elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

505 elab' ina _ (PLam _ _ _ PImpossible) = lift . tfail . Msg $ "Only pattern-matching lambdas can be impossible"

502 elab' ina _ (PLam fc n Placeholder sc)

506 elab' ina _ (PLam fc n Placeholder sc)

@@ -1386,6 +1390,18 @@ pruneByType env (P _ n _) ctxt as

1386

1390

1387pruneByType _ t _ as = as

1391pruneByType _ t _ as = as

1388

1392

1393+-- | Use the local elab context to work out the highlighting for a name

1394+findHighlight :: Name -> ElabD OutputAnnotation

1395+findHighlight n = do ctxt <- get_context

1396+ env <- get_env

1397+ case lookup n env of

1398+ Just _ -> return $ AnnBoundName n False

1399+ Nothing -> case lookupTyExact n ctxt of

1400+ Just _ -> return $ AnnName n Nothing Nothing Nothing

1401+ Nothing -> lift . tfail . InternalMsg $

1402+ "Can't find name" ++ show n

1403+

1404+

1389findInstances :: IState -> Term -> [Name]

1405findInstances :: IState -> Term -> [Name]

1390findInstances ist t

1406findInstances ist t

1391 | (P _ n _, _) <- unApply (getRetTy t)

1407 | (P _ n _, _) <- unApply (getRetTy t)

src/Idris/Output.hs+3−3

@@ -41,9 +41,9 @@ iWarn fc err =

41 case idris_outputmode i of

42 RawOutput h ->

43 do err' <- iRender . fmap (fancifyAnnots i) $

44− if fc_fname fc /= ""

44+ case fc of

45− then text (show fc) <> colon <//> err

45+ FC fn _ _ | fn /= "" -> text (show fc) <> colon <//> err

46− else err

46+ _ -> err

47 runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

48 IdeMode n h ->

49 do err' <- iRender . fmap (fancifyAnnots i) $ err

src/Idris/ParseData.hs+1−1

@@ -56,7 +56,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

56 tyn_in <- fnName

57 let tyn = expandNS syn tyn_in

58 let rsyn = syn { syn_namespace = show (nsroot tyn) :

59− syn_namespace syn }

59+ syn_namespace syn }

60 params <- manyTill (recordParameter rsyn) (reserved "where")

61 (fields, cname, cdoc) <- indentedBlockS $ agdaStyleBody rsyn tyn

62 case cname of

src/Idris/ParseExpr.hs+13−10

@@ -1238,11 +1238,11 @@ constant :: IdrisParser (Idris.Core.TT.Const, FC)

1238constant = choice [ do fc <- reservedFC name; return (ty, fc)

1239 | (name, ty) <- constants

1240 ]

1241− <|> do f <- try float; return (Fl f, NoFC)

1241+ <|> do (f, fc) <- try float; return (Fl f, fc)

1242− <|> do i <- natural; return (BI i, NoFC)

1242+ <|> do (i, fc) <- natural; return (BI i, fc)

1243− <|> do s <- verbatimStringLiteral; return (Str s, NoFC)

1243+ <|> do (s, fc) <- verbatimStringLiteral; return (Str s, fc)

1244− <|> do s <- stringLiteral; return (Str s, NoFC)

1244+ <|> do (s, fc) <- stringLiteral; return (Str s, fc)

1245− <|> do c <- try charLiteral; return (Ch c, NoFC) --Currently ambigous with symbols

1245+ <|> do (c, fc) <- try charLiteral; return (Ch c, fc) --Currently ambigous with symbols

1246 <?> "constant or literal"

1247

1248{- | Parses a verbatim multi-line string literal (triple-quoted)

@@ -1253,9 +1253,12 @@ VerbatimString_t ::=

1253;

1254@

1255 -}

1256−verbatimStringLiteral :: MonadicParsing m => m String

1256+verbatimStringLiteral :: MonadicParsing m => m (String, FC)

1257−verbatimStringLiteral = token $ do try $ string "\"\"\""

1257+verbatimStringLiteral = token $ do (FC f start _) <- getFC

1258+ try $ string "\"\"\""

1258− manyTill anyChar $ try (string "\"\"\"")

1259+ str <- manyTill anyChar $ try (string "\"\"\"")

1260+ (FC _ _ end) <- getFC

1261+ return (str, FC f start end)

1259

1262

1260{- | Parses a static modifier

1263{- | Parses a static modifier

1261

1264

@@ -1370,7 +1373,7 @@ tactics =

1370 , noArgs ["trivial"] Trivial

1373 , noArgs ["trivial"] Trivial

1371 , noArgs ["unify"] DoUnify

1374 , noArgs ["unify"] DoUnify

1372 , (["search"], Nothing, const $

1375 , (["search"], Nothing, const $

1373− do depth <- option 10 natural

1376+ do depth <- option 10 $ fst <$> natural

1374 return (ProofSearch True True (fromInteger depth) Nothing []))

1377 return (ProofSearch True True (fromInteger depth) Nothing []))

1375 , noArgs ["instance"] TCInstance

1378 , noArgs ["instance"] TCInstance

1376 , noArgs ["solve"] Solve

1379 , noArgs ["solve"] Solve

@@ -1386,7 +1389,7 @@ tactics =

1386 , expressionTactic [":t", ":type"] TCheck

1389 , expressionTactic [":t", ":type"] TCheck

1387 , expressionTactic [":search"] TSearch

1390 , expressionTactic [":search"] TSearch

1388 , (["fail"], Just StringLitTArg, const $

1391 , (["fail"], Just StringLitTArg, const $

1389− do msg <- stringLiteral

1392+ do msg <- fst <$> stringLiteral

1390 return $ TFail [Idris.Core.TT.TextPart msg])

1393 return $ TFail [Idris.Core.TT.TextPart msg])

1391 , ([":doc"], Just ExprTArg, const $

1394 , ([":doc"], Just ExprTArg, const $

1392 do whiteSpace

1395 do whiteSpace

src/Idris/ParseHelpers.hs+17−18

@@ -194,24 +194,32 @@ whiteSpace :: MonadicParsing m => m ()

194whiteSpace = Tok.whiteSpace

195

196-- | Parses a string literal

197−stringLiteral :: MonadicParsing m => m String

197+stringLiteral :: IdrisParser (String, FC)

198−stringLiteral = Tok.stringLiteral

198+stringLiteral = do str <- Tok.stringLiteral

199+ fc <- lastTokenSpan <$> get

200+ return (str, fromMaybe NoFC fc)

199

201

200−-- | Parses a char literal

202+-- | Parses a char literal

201−charLiteral :: MonadicParsing m => m Char

203+charLiteral :: IdrisParser (Char, FC)

202−charLiteral = Tok.charLiteral

204+charLiteral = do ch <- Tok.charLiteral

205+ fc <- lastTokenSpan <$> get

206+ return (ch, fromMaybe NoFC fc)

203

207

204-- | Parses a natural number

208-- | Parses a natural number

205−natural :: MonadicParsing m => m Integer

209+natural :: IdrisParser (Integer, FC)

206−natural = Tok.natural

210+natural = do n <- Tok.natural

211+ fc <- lastTokenSpan <$> get

212+ return (n, fromMaybe NoFC fc)

207

213

208-- | Parses an integral number

214-- | Parses an integral number

209integer :: MonadicParsing m => m Integer

215integer :: MonadicParsing m => m Integer

210integer = Tok.integer

216integer = Tok.integer

211

217

212-- | Parses a floating point number

218-- | Parses a floating point number

213−float :: MonadicParsing m => m Double

219+float :: IdrisParser (Double, FC)

214−float = Tok.double

220+float = do f <- Tok.double

221+ fc <- lastTokenSpan <$> get

222+ return (f, fromMaybe NoFC fc)

215

223

216{- * Symbols, identifiers, names and operators -}

224{- * Symbols, identifiers, names and operators -}

217

225

@@ -367,15 +375,6 @@ getFC = do s <- position

367 -- Issue #1594 on the Issue Tracker.

375 -- Issue #1594 on the Issue Tracker.

368 -- https://github.com/idris-lang/Idris-dev/issues/1594

376 -- https://github.com/idris-lang/Idris-dev/issues/1594

369

377

370−{- | Get the span surrounding a parse -}

371−withSpan :: MonadicParsing m => m a -> m (a, FC)

372−withSpan p = do s <- position

373− let (dir, file) = splitFileName (fileName s)

374− let f = if dir == addTrailingPathSeparator "." then file else fileName s

375− res <- p

376− s' <- position

377− let fc = FC f (lineNum s, columnNum s) (lineNum s', columnNum s')

378− return (res, fc)

379

378

380{-* Syntax helpers-}

379{-* Syntax helpers-}

381-- | Bind constraints to term

380-- | Bind constraints to term

src/Idris/ParseOps.hs+4−1

@@ -29,6 +29,8 @@ import qualified Data.HashSet as HS

29import qualified Data.Text as T

30import qualified Data.ByteString.UTF8 as UTF8

31

32+import Debug.Trace

33+

32-- | Creates table for fixity declarations to build expression parser

34-- | Creates table for fixity declarations to build expression parser

33-- using pre-build and user-defined operator/fixity declarations

35-- using pre-build and user-defined operator/fixity declarations

34table :: [FixDecl] -> OperatorTable IdrisParser PTerm

36table :: [FixDecl] -> OperatorTable IdrisParser PTerm

@@ -121,7 +123,8 @@ Fixity ::=

121-}

123-}

122fixity :: IdrisParser PDecl

124fixity :: IdrisParser PDecl

123fixity = do pushIndent

125fixity = do pushIndent

126+ f <- fixityType; i <- fst <$> natural;

124− f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')

127+ ops <- sepBy1 operator (lchar ',')

125 terminator

128 terminator

126 let prec = fromInteger i

129 let prec = fromInteger i

127 istate <- get

130 istate <- get

src/Idris/Parser.hs+17−9

@@ -362,7 +362,7 @@ syntaxSym = try (do lchar '['; n <- name; lchar ']'

362 return (Binding n))

363 <|> do n <- iName []

364 return (Keyword n)

365− <|> do sym <- stringLiteral

365+ <|> do sym <- fmap fst stringLiteral

366 return (Symbol sym)

367 <?> "syntax symbol"

368

@@ -466,7 +466,7 @@ fnOpts opts

466 = do reserved "total"; fnOpts (TotalFn : opts)

467 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

468 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

469− <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

469+ <|> do try (lchar '%' *> reserved "export"); c <- fmap fst stringLiteral;

470 fnOpts (CExport c : opts)

471 <|> do try (lchar '%' *> reserved "no_implicit");

472 fnOpts (NoImplicit : opts)

@@ -490,7 +490,7 @@ fnOpts opts

490 <?> "function modifier"

491 where nameTimes :: IdrisParser (Name, Maybe Int)

492 nameTimes = do n <- fnName

493− t <- option Nothing (do reds <- natural

493+ t <- option Nothing (do reds <- fmap fst natural

494 return (Just (fromInteger reds)))

495 return (n, t)

496

@@ -1077,13 +1077,19 @@ Directive' ::= 'lib' CodeGen String_t

1077@

1078-}

1079directive :: SyntaxInfo -> IdrisParser [PDecl]

1080−directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;

1080+directive syn = do try (lchar '%' *> reserved "lib")

1081+ cgn <- codegen_

1082+ lib <- fmap fst stringLiteral

1081 return [PDirective (DLib cgn lib)]

1083 return [PDirective (DLib cgn lib)]

1084+ <|> do try (lchar '%' *> reserved "link")

1082− <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;

1085+ cgn <- codegen_; obj <- fst <$> stringLiteral

1083 return [PDirective (DLink cgn obj)]

1086 return [PDirective (DLink cgn obj)]

1087+ <|> do try (lchar '%' *> reserved "flag")

1084− <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_; flag <- stringLiteral

1088+ cgn <- codegen_; flag <- fst <$> stringLiteral

1085 return [PDirective (DFlag cgn flag)]

1089 return [PDirective (DFlag cgn flag)]

1086− <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;

1090+ <|> do try (lchar '%' *> reserved "include")

1091+ cgn <- codegen_

1092+ hdr <- fst <$> stringLiteral

1087 return [PDirective (DInclude cgn hdr)]

1093 return [PDirective (DInclude cgn hdr)]

1088 <|> do try (lchar '%' *> reserved "hide"); n <- fnName

1094 <|> do try (lchar '%' *> reserved "hide"); n <- fnName

1089 return [PDirective (DHide n)]

1095 return [PDirective (DHide n)]

@@ -1095,9 +1101,11 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

1095 i <- get

1101 i <- get

1096 put (i { default_total = tot } )

1102 put (i { default_total = tot } )

1097 return [PDirective (DDefault tot)]

1103 return [PDirective (DDefault tot)]

1098− <|> do try (lchar '%' *> reserved "logging"); i <- natural;

1104+ <|> do try (lchar '%' *> reserved "logging")

1105+ i <- fst <$> natural

1099 return [PDirective (DLogging i)]

1106 return [PDirective (DLogging i)]

1100− <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');

1107+ <|> do try (lchar '%' *> reserved "dynamic")

1108+ libs <- sepBy1 (fmap fst stringLiteral) (lchar ',')

1101 return [PDirective (DDynamicLibs libs)]

1109 return [PDirective (DDynamicLibs libs)]

1102 <|> do try (lchar '%' *> reserved "name")

1110 <|> do try (lchar '%' *> reserved "name")

1103 ty <- fnName

1111 ty <- fnName

src/Idris/REPLParser.hs+14−13

@@ -258,7 +258,7 @@ proofArg cmd name = do

258 upd <- option False $ do

259 P.lchar '!'

260 return True

261− l <- P.natural

261+ l <- fmap fst P.natural

262 n <- P.name;

263 return (Right (cmd upd (fromInteger l) n))

264

@@ -282,7 +282,8 @@ cmd_consolewidth name = do

282 pConsoleWidth :: P.IdrisParser ConsoleWidth

283 pConsoleWidth = do discard (P.symbol "auto"); return AutomaticWidth

284 <|> do discard (P.symbol "infinite"); return InfinitelyWide

285− <|> do n <- fmap fromInteger P.natural; return (ColsWide n)

285+ <|> do n <- fmap (fromInteger . fst) P.natural

286+ return (ColsWide n)

286

287

287cmd_execute :: String -> P.IdrisParser (Either String Command)

288cmd_execute :: String -> P.IdrisParser (Either String Command)

288cmd_execute name = do

289cmd_execute name = do

@@ -307,7 +308,7 @@ cmd_pprint :: String -> P.IdrisParser (Either String Command)

307cmd_pprint name = do

308cmd_pprint name = do

308 fmt <- ppFormat

309 fmt <- ppFormat

309 P.whiteSpace

310 P.whiteSpace

310− n <- fmap fromInteger P.natural

311+ n <- fmap (fromInteger . fst) P.natural

311 P.whiteSpace

312 P.whiteSpace

312 t <- P.fullExpr defaultSyntax

313 t <- P.fullExpr defaultSyntax

313 return (Right (PPrint fmt n t))

314 return (Right (PPrint fmt n t))

@@ -349,16 +350,16 @@ cmd_compile name = do

349cmd_addproof :: String -> P.IdrisParser (Either String Command)

350cmd_addproof :: String -> P.IdrisParser (Either String Command)

350cmd_addproof name = do

351cmd_addproof name = do

351 n <- option Nothing $ do

352 n <- option Nothing $ do

352− x <- P.name;

353+ x <- P.name

353 return (Just x)

354 return (Just x)

354 eof

355 eof

355 return (Right (AddProof n))

356 return (Right (AddProof n))

356

357

357cmd_log :: String -> P.IdrisParser (Either String Command)

358cmd_log :: String -> P.IdrisParser (Either String Command)

358cmd_log name = do

359cmd_log name = do

359− i <- P.natural

360+ i <- fmap (fromIntegral . fst) P.natural

360 eof

361 eof

361− return (Right (LogLvl (fromIntegral i)))

362+ return (Right (LogLvl i))

362

363

363cmd_let :: String -> P.IdrisParser (Either String Command)

364cmd_let :: String -> P.IdrisParser (Either String Command)

364cmd_let name = do

365cmd_let name = do

@@ -370,9 +371,9 @@ cmd_unlet name = (Right . Undefine) `fmap` many P.name

370

371

371cmd_loadto :: String -> P.IdrisParser (Either String Command)

372cmd_loadto :: String -> P.IdrisParser (Either String Command)

372cmd_loadto name = do

373cmd_loadto name = do

373− toline <- P.natural

374+ toline <- fmap (fromInteger . fst) P.natural

374 f <- many anyChar;

375 f <- many anyChar;

375− return (Right (Load f (Just (fromInteger toline))))

376+ return (Right (Load f (Just toline)))

376

377

377cmd_colour :: String -> P.IdrisParser (Either String Command)

378cmd_colour :: String -> P.IdrisParser (Either String Command)

378cmd_colour name = fmap Right pSetColourCmd

379cmd_colour name = fmap Right pSetColourCmd

@@ -452,19 +453,19 @@ packageBasedCmd valParser cmd name = do

452 return (Right (cmd pkgs val))

453 return (Right (cmd pkgs val))

453

454

454cmd_search :: String -> P.IdrisParser (Either String Command)

455cmd_search :: String -> P.IdrisParser (Either String Command)

455−cmd_search = packageBasedCmd

456+cmd_search = packageBasedCmd

456 (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search

457 (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search

457

458

458cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

459cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

459cmd_proofsearch name = do

460cmd_proofsearch name = do

460 upd <- option False (do P.lchar '!'; return True)

461 upd <- option False (do P.lchar '!'; return True)

461− l <- P.natural; n <- P.name;

462+ l <- fmap (fromInteger . fst) P.natural; n <- P.name

462 hints <- many P.fnName

463 hints <- many P.fnName

463− return (Right (DoProofSearch upd True (fromInteger l) n hints))

464+ return (Right (DoProofSearch upd True l n hints))

464

465

465cmd_refine :: String -> P.IdrisParser (Either String Command)

466cmd_refine :: String -> P.IdrisParser (Either String Command)

466cmd_refine name = do

467cmd_refine name = do

467 upd <- option False (do P.lchar '!'; return True)

468 upd <- option False (do P.lchar '!'; return True)

468− l <- P.natural; n <- P.name;

469+ l <- fmap (fromInteger . fst) P.natural; n <- P.name

469 hint <- P.fnName

470 hint <- P.fnName

470− return (Right (DoProofSearch upd False (fromInteger l) n [hint]))

471+ return (Right (DoProofSearch upd False l n [hint]))

src/Pkg/PParser.hs+2−2

@@ -5,12 +5,12 @@

5

6module Pkg.PParser where

7

8−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

8+import Text.Trifecta hiding (span, charLiteral, natural, symbol, char, string, whiteSpace)

9

10import Idris.Core.TT

11import Idris.REPL

12import Idris.AbsSyntaxTree

13−import Idris.ParseHelpers

13+import Idris.ParseHelpers hiding (stringLiteral)

14import Idris.CmdOptions

15

16import Control.Monad.State.Strict