da3a26c · Idris-dev · git.iko.soy

src/Idris/DSL.hs+1−1

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

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

7373 (map (pmap (expandSugar dsl)) opts)

7474expandSugar 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"))

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

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

7878 , 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

343343 do hnf_compute

344344 g <- goal

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

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

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

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

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

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

354353 instanceArg c

355354 elab' ina _ (PRefl fc t)

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

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

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

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

357+ highlightSource fc (AnnName eqCon Nothing Nothing Nothing)

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

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

360360 claim tyn RType

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

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

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

429429 pexp l, pexp r])

430− elab' ina fc (PAlternative True as)

430+ elab' ina fc (PAlternative True as)

431431 = do hnf_compute

432432 ty <- goal

433433 ctxt <- get_context

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

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

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

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

493− | otherwise =

493+ | otherwise =

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

495495 ctxt <- get_context

496− env <- get_env

496+ env <- get_env

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

498498 if null a'

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

499+ then erun fc $

500+ do apply (Var n) []

501+ hl <- findHighlight n

502+ solve

503+ highlightSource fc hl

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

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

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

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

13861390

13871391pruneByType _ t _ as = as

13881392

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+

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

13901406findInstances ist t

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

src/Idris/Output.hs+3−3

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

4141 case idris_outputmode i of

4242 RawOutput h ->

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

44− if fc_fname fc /= ""

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

46− else err

44+ case fc of

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

46+ _ -> err

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

4848 IdeMode n h ->

4949 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

5656 tyn_in <- fnName

5757 let tyn = expandNS syn tyn_in

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

59− syn_namespace syn }

59+ syn_namespace syn }

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

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

6262 case cname of

src/Idris/ParseExpr.hs+13−10

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

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

12391239 | (name, ty) <- constants

12401240 ]

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

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

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

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

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

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

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

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

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

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

12461246 <?> "constant or literal"

12471247

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

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

12531253;

12541254@

12551255 -}

1256−verbatimStringLiteral :: MonadicParsing m => m String

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

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

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

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

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

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

1260+ (FC _ _ end) <- getFC

1261+ return (str, FC f start end)

12591262

12601263{- | Parses a static modifier

12611264

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

13701373 , noArgs ["trivial"] Trivial

13711374 , noArgs ["unify"] DoUnify

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

1373− do depth <- option 10 natural

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

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

13751378 , noArgs ["instance"] TCInstance

13761379 , noArgs ["solve"] Solve

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

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

13871390 , expressionTactic [":search"] TSearch

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

1389− do msg <- stringLiteral

1392+ do msg <- fst <$> stringLiteral

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

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

13921395 do whiteSpace

src/Idris/ParseHelpers.hs+17−18

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

194194whiteSpace = Tok.whiteSpace

195195

196196-- | Parses a string literal

197−stringLiteral :: MonadicParsing m => m String

198−stringLiteral = Tok.stringLiteral

197+stringLiteral :: IdrisParser (String, FC)

198+stringLiteral = do str <- Tok.stringLiteral

199+ fc <- lastTokenSpan <$> get

200+ return (str, fromMaybe NoFC fc)

199201

200−-- | Parses a char literal

201−charLiteral :: MonadicParsing m => m Char

202−charLiteral = Tok.charLiteral

202+-- | Parses a char literal

203+charLiteral :: IdrisParser (Char, FC)

204+charLiteral = do ch <- Tok.charLiteral

205+ fc <- lastTokenSpan <$> get

206+ return (ch, fromMaybe NoFC fc)

203207

204208-- | Parses a natural number

205−natural :: MonadicParsing m => m Integer

206−natural = Tok.natural

209+natural :: IdrisParser (Integer, FC)

210+natural = do n <- Tok.natural

211+ fc <- lastTokenSpan <$> get

212+ return (n, fromMaybe NoFC fc)

207213

208214-- | Parses an integral number

209215integer :: MonadicParsing m => m Integer

210216integer = Tok.integer

211217

212218-- | Parses a floating point number

213−float :: MonadicParsing m => m Double

214−float = Tok.double

219+float :: IdrisParser (Double, FC)

220+float = do f <- Tok.double

221+ fc <- lastTokenSpan <$> get

222+ return (f, fromMaybe NoFC fc)

215223

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

217225

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

367375 -- Issue #1594 on the Issue Tracker.

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

369377

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)

379378

380379{-* Syntax helpers-}

381380-- | Bind constraints to term

src/Idris/ParseOps.hs+4−1

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

2929import qualified Data.Text as T

3030import qualified Data.ByteString.UTF8 as UTF8

3131

32+import Debug.Trace

33+

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

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

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

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

121123-}

122124fixity :: IdrisParser PDecl

123125fixity = do pushIndent

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

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

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

125128 terminator

126129 let prec = fromInteger i

127130 istate <- get

src/Idris/Parser.hs+17−9

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

362362 return (Binding n))

363363 <|> do n <- iName []

364364 return (Keyword n)

365− <|> do sym <- stringLiteral

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

366366 return (Symbol sym)

367367 <?> "syntax symbol"

368368

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

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

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

468468 <|> 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;

470470 fnOpts (CExport c : opts)

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

472472 fnOpts (NoImplicit : opts)

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

490490 <?> "function modifier"

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

492492 nameTimes = do n <- fnName

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

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

494494 return (Just (fromInteger reds)))

495495 return (n, t)

496496

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

10771077@

10781078-}

10791079directive :: 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

10811083 return [PDirective (DLib cgn lib)]

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

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

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

10831086 return [PDirective (DLink cgn obj)]

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

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

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

10851089 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

10871093 return [PDirective (DInclude cgn hdr)]

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

10891095 return [PDirective (DHide n)]

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

10951101 i <- get

10961102 put (i { default_total = tot } )

10971103 return [PDirective (DDefault tot)]

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

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

1105+ i <- fst <$> natural

10991106 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 ',')

11011109 return [PDirective (DDynamicLibs libs)]

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

11031111 ty <- fnName

src/Idris/REPLParser.hs+14−13

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

258258 upd <- option False $ do

259259 P.lchar '!'

260260 return True

261− l <- P.natural

261+ l <- fmap fst P.natural

262262 n <- P.name;

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

264264

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

282282 pConsoleWidth :: P.IdrisParser ConsoleWidth

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

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

286287

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

288289cmd_execute name = do

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

307308cmd_pprint name = do

308309 fmt <- ppFormat

309310 P.whiteSpace

310− n <- fmap fromInteger P.natural

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

311312 P.whiteSpace

312313 t <- P.fullExpr defaultSyntax

313314 return (Right (PPrint fmt n t))

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

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

350351cmd_addproof name = do

351352 n <- option Nothing $ do

352− x <- P.name;

353+ x <- P.name

353354 return (Just x)

354355 eof

355356 return (Right (AddProof n))

356357

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

358359cmd_log name = do

359− i <- P.natural

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

360361 eof

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

362+ return (Right (LogLvl i))

362363

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

364365cmd_let name = do

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

370371

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

372373cmd_loadto name = do

373− toline <- P.natural

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

374375 f <- many anyChar;

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

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

376377

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

378379cmd_colour name = fmap Right pSetColourCmd

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

452453 return (Right (cmd pkgs val))

453454

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

455−cmd_search = packageBasedCmd

456+cmd_search = packageBasedCmd

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

457458

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

459460cmd_proofsearch name = do

460461 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

462463 hints <- many P.fnName

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

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

464465

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

466467cmd_refine name = do

467468 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

469470 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 @@

55

66module Pkg.PParser where

77

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)

99

1010import Idris.Core.TT

1111import Idris.REPL

1212import Idris.AbsSyntaxTree

13−import Idris.ParseHelpers

13+import Idris.ParseHelpers hiding (stringLiteral)

1414import Idris.CmdOptions

1515

1616import Control.Monad.State.Strict