c46243b · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

@@ -1148,7 +1148,7 @@ getPriority i tm = 1 -- pri tm

11481148 pri (PPair _ _ l r) = max 1 (max (pri l) (pri r))

11491149 pri (PDPair _ _ l t r) = max 1 (max (pri l) (max (pri t) (pri r)))

11501150 pri (PAlternative a as) = maximum (map pri as)

1151− pri (PConstant _) = 0

1151+ pri (PConstant _ _) = 0

11521152 pri Placeholder = 1

11531153 pri _ = 3

11541154

@@ -1885,10 +1885,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

18851885 match' x y = match (fullApp x) (fullApp y)

18861886 match (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x]) x'

18871887 | fi == txt "fromInteger" && b == txt "builtins",

1888− PConstant (I _) <- getTm x = match (getTm x) x'

1888+ PConstant _ (I _) <- getTm x = match (getTm x) x'

18891889 match x' (PApp _ (PRef _ (NS (UN fi) [b])) [_,_,x])

18901890 | fi == txt "fromInteger" && b == txt "builtins",

1891− PConstant (I _) <- getTm x = match (getTm x) x'

1891+ PConstant _ (I _) <- getTm x = match (getTm x) x'

18921892 match (PApp _ (PRef _ (UN l)) [_,x]) x' | l == txt "lazy" = match (getTm x) x'

18931893 match x (PApp _ (PRef _ (UN l)) [_,x']) | l == txt "lazy" = match x (getTm x')

18941894 match (PApp _ f args) (PApp _ f' args')

src/Idris/AbsSyntaxTree.hs+21−16

@@ -670,14 +670,19 @@ data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

670670data EState = EState {

671671 case_decls :: [(Name, PDecl)],

672672 delayed_elab :: [Elab' EState ()],

673− new_tyDecls :: [RDeclInstructions]

673+ new_tyDecls :: [RDeclInstructions],

674+ highlighting :: [(FC, OutputAnnotation)]

674675 }

675676

676677initEState :: EState

677−initEState = EState [] [] []

678+initEState = EState [] [] [] []

678679

679680type ElabD a = Elab' EState a

680681

682+highlightSource :: FC -> OutputAnnotation -> ElabD ()

683+highlightSource fc annot =

684+ updateAux (\aux -> aux { highlighting = (fc, annot) : highlighting aux })

685+

681686-- | One clause of a top-level definition. Term arguments to constructors are:

682687--

683688-- 1. The whole application (missing for PClauseR and PWithR because they're within a "with" clause)

@@ -825,10 +830,10 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

825830 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

826831 | PAlternative Bool [PTerm] -- ^ True if only one may work. (| A, B, C|)

827832 | PHidden PTerm -- ^ Irrelevant or hidden pattern

828− | PType -- ^ 'Type' type

833+ | PType FC -- ^ 'Type' type

829834 | PUniverse Universe -- ^ Some universe

830835 | PGoal FC PTerm Name PTerm -- ^ quoteGoal, used for %reflection functions

831− | PConstant Const -- ^ Builtin types

836+ | PConstant FC Const -- ^ Builtin types

832837 | Placeholder -- ^ Underscore

833838 | PDoBlock [PDo] -- ^ Do notation

834839 | PIdiom FC PTerm -- ^ Idiom brackets

@@ -1037,10 +1042,10 @@ highestFC (PAlternative _ args) =

10371042 [] -> Nothing

10381043 (fc:_) -> Just fc

10391044highestFC (PHidden _) = Nothing

1040−highestFC PType = Nothing

1045+highestFC (PType fc) = Just fc

10411046highestFC (PUniverse _) = Nothing

10421047highestFC (PGoal fc _ _ _) = Just fc

1043−highestFC (PConstant _) = Nothing

1048+highestFC (PConstant fc _) = Just fc

10441049highestFC Placeholder = Nothing

10451050highestFC (PDoBlock lines) =

10461051 case map getDoFC lines of

@@ -1256,8 +1261,8 @@ bi = fileFC "builtin"

12561261inferTy = sMN 0 "__Infer"

12571262inferCon = sMN 0 "__infer"

12581263inferDecl = PDatadecl inferTy

1259− PType

1260− [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") PType (

1264+ (PType bi)

1265+ [(emptyDocstring, [], inferCon, PPi impl (sMN 0 "iType") (PType bi) (

12611266 PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))

12621267 (PRef bi inferTy)), bi, [])]

12631268inferOpts = []

@@ -1312,11 +1317,11 @@ eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

13121317 "\n\n" ++

13131318 "You may need to use `(~=~)` to explicitly request heterogeneous equality."

13141319

1315−eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1320+eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType bi), (n "B", PType bi)]

13161321 (piBind [(n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]

1317− PType))

1322+ (PType bi)))

13181323 [(reflDoc, reflParamDoc,

1319− eqCon, PPi impl (n "A") PType (

1324+ eqCon, PPi impl (n "A") (PType bi) (

13201325 PPi impl (n "x") (PRef bi (n "A"))

13211326 (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,

13221327 pimp (n "B") Placeholder False,

@@ -1513,7 +1518,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

15131518 (prettySe left bnd l <+> opName False) <$>

15141519 group (prettySe right bnd r)

15151520 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1516− | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1521+ | PConstant NoFC (Idris.Core.TT.Str str) <- getTm tm,

15171522 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

15181523 char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))

15191524 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

@@ -1605,9 +1610,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

16051610 where

16061611 prettyAs =

16071612 foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as

1608− prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1613+ prettySe p bnd (PType _) = annotate (AnnType "Type" "The type of types") $ text "Type"

16091614 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1610− prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1615+ prettySe p bnd (PConstant _ c) = annotate (AnnConst c) (text (show c))

16111616 -- XXX: add pretty for tactics

16121617 prettySe p bnd (PProof ts) =

16131618 text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

@@ -1881,9 +1886,9 @@ instance Sized PTerm where

18811886 size (PUnifyLog tm) = size tm

18821887 size (PDisamb _ tm) = size tm

18831888 size (PNoImplicits tm) = size tm

1884− size PType = 1

1889+ size (PType _) = 1

18851890 size (PUniverse _) = 1

1886− size (PConstant const) = 1 + size const

1891+ size (PConstant fc const) = 1 + size fc + size const

18871892 size Placeholder = 1

18881893 size (PDoBlock dos) = 1 + size dos

18891894 size (PIdiom fc term) = 1 + size term

src/Idris/Core/Binary.hs+19−8

@@ -249,15 +249,26 @@ instance Binary a => Binary (Err' a) where

249249----- Generated by 'derive'

250250

251251instance Binary FC where

252− put (FC x1 (x2, x3) (x4, x5))

253− = do put x1

254− put (x2 * 65536 + x3)

255− put (x4 * 65536 + x5)

252+ put x =

253+ case x of

254+ (FC x1 (x2, x3) (x4, x5)) -> do putWord8 0

255+ put x1

256+ put (x2 * 65536 + x3)

257+ put (x4 * 65536 + x5)

258+ NoFC -> putWord8 1

259+ FileFC x1 -> do putWord8 2

260+ put x1

256261 get

257− = do x1 <- get

258− x2x3 <- get

259− x4x5 <- get

260− return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

262+ = do i <- getWord8

263+ case i of

264+ 0 -> do x1 <- get

265+ x2x3 <- get

266+ x4x5 <- get

267+ return (FC x1 (x2x3 `div` 65536, x2x3 `mod` 65536) (x4x5 `div` 65536, x4x5 `mod` 65536))

268+ 1 -> return NoFC

269+ 2 -> do x1 <- get

270+ return (FileFC x1)

271+ _ -> error "Corrupted binary data for FC"

261272

262273

263274instance Binary Name where

src/Idris/Core/DeepSeq.hs+2

@@ -43,6 +43,8 @@ instance NFData Raw where

4343

4444instance NFData FC where

4545 rnf (FC x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

46+ rnf NoFC = ()

47+ rnf (FileFC f) = rnf f `seq` ()

4648

4749instance NFData Provenance where

4850 rnf ExpectedType = ()

src/Idris/Core/TT.hs+13−4

@@ -53,7 +53,9 @@ data FC = FC { fc_fname :: String, -- ^ Filename

5353 fc_start :: (Int, Int), -- ^ Line and column numbers for the start of the location span

5454 fc_end :: (Int, Int) -- ^ Line and column numbers for the end of the location span

5555 }

56− deriving (Data, Typeable, Ord)

56+ | NoFC -- ^ Locations for machine-generated terms

57+ | FileFC { fc_fname :: String } -- ^ Locations with file only

58+ deriving (Data, Typeable, Ord)

5759

5860-- | Ignore source location equality (so deriving classes do not compare FCs)

5961instance Eq FC where

@@ -65,14 +67,17 @@ newtype FC' = FC' { unwrapFC :: FC }

6567instance Eq FC' where

6668 FC' fc == FC' fc' = fcEq fc fc'

6769 where fcEq (FC n s e) (FC n' s' e') = n == n' && s == s' && e == e'

70+ fcEq NoFC NoFC = True

71+ fcEq (FileFC f) (FileFC f') = f == f'

72+ fcEq _ _ = False

6873

6974-- | Empty source location

7075emptyFC :: FC

71−emptyFC = fileFC ""

76+emptyFC = NoFC

7277

73−-- | Source location with file only

78+-- | Source location with file only

7479fileFC :: String -> FC

75−fileFC s = FC s (0, 0) (0, 0)

80+fileFC s = FileFC s

7681

7782{-!

7883deriving instance Binary FC

@@ -81,12 +86,16 @@ deriving instance NFData FC

8186

8287instance Sized FC where

8388 size (FC f s e) = 4 + length f

89+ size NoFC = 1

90+ size (FileFC f) = length f

8491

8592instance Show FC where

8693 show (FC f s e) = f ++ ":" ++ showLC s e

8794 where showLC (sl, sc) (el, ec) | sl == el && sc == ec = show sl ++ ":" ++ show sc

8895 | sl == el = show sl ++ ":" ++ show sc ++ "-" ++ show ec

8996 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

97+ show NoFC = "No location"

98+ show (FileFC f) = f

9099

91100-- | Output annotation for pretty-printed name - decides colour

92101data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput | PostulateOutput

src/Idris/Coverage.hs+4−4

@@ -179,8 +179,8 @@ genAll i args

179179 where

180180 -- if they're constants, invent a new one to make sure that

181181 -- constants which are not explicitly handled are covered

182− inventConsts cs@(PConstant c : _) = map PConstant (ic' (mapMaybe getConst cs))

183− where getConst (PConstant c) = Just c

182+ inventConsts cs@(PConstant fc c : _) = map (PConstant NoFC) (ic' (mapMaybe getConst cs))

183+ where getConst (PConstant _ c) = Just c

184184 getConst _ = Nothing

185185 inventConsts xs = xs

186186

@@ -226,7 +226,7 @@ genAll i args

226226 ([pimp (sUN "a") Placeholder True,

227227 pimp (sUN "P") Placeholder True] ++

228228 [pexp t,pexp v]) o

229− otherPats o@(PConstant c) = inventConsts [o] -- return o

229+ otherPats o@(PConstant _ c) = inventConsts [o] -- return o

230230 otherPats arg = return Placeholder

231231

232232 ops fc n xs o

@@ -278,7 +278,7 @@ genAll i args

278278

279279 -- quick check for constructor equality

280280 quickEq :: PTerm -> PTerm -> Bool

281− quickEq (PConstant n) (PConstant n') = n == n'

281+ quickEq (PConstant _ n) (PConstant _ n') = n == n'

282282 quickEq (PRef _ n) (PRef _ n') = n == n'

283283 quickEq (PApp _ t as) (PApp _ t' as')

284284 | length as == length as'

src/Idris/DSL.hs+2−2

@@ -33,8 +33,8 @@ mkTTName fc n =

3333 mkList fc (x:xs) = PApp fc (PRef fc (sNS (sUN "::") ["List", "Prelude"]))

3434 [ pexp (stringC x)

3535 , pexp (mkList fc xs)]

36− stringC = PConstant . Str . str

37− intC = PConstant . I

36+ stringC = PConstant fc . Str . str

37+ intC = PConstant fc . I

3838 reflm n = sNS (sUN n) ["Reflection", "Language"]

3939 in case n of

4040 UN nm -> PApp fc (PRef fc (reflm "UN")) [ pexp (stringC nm)]

src/Idris/DeepSeq.hs+2−2

@@ -224,11 +224,11 @@ instance NFData PTerm where

224224 rnf (PAs x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

225225 rnf (PAlternative x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

226226 rnf (PHidden x1) = rnf x1 `seq` ()

227− rnf PType = ()

227+ rnf (PType fc) = rnf fc `seq` ()

228228 rnf (PUniverse _) = ()

229229 rnf (PGoal x1 x2 x3 x4)

230230 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

231− rnf (PConstant x1) = x1 `seq` ()

231+ rnf (PConstant x1 x2) = x1 `seq` x2 `seq` ()

232232 rnf Placeholder = ()

233233 rnf (PDoBlock x1) = rnf x1 `seq` ()

234234 rnf (PIdiom x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Delaborate.hs+2−2

@@ -90,11 +90,11 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

9090 de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

9191 de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

9292 de env plic (Bind n bb sc) = de ((n,n):env) [] sc

93− de env _ (Constant i) = PConstant i

93+ de env _ (Constant i) = PConstant NoFC i

9494 de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

9595 de env _ Erased = Placeholder

9696 de env _ Impossible = Placeholder

97− de env _ (TType i) = PType

97+ de env _ (TType i) = PType un

9898 de env _ (UType u) = PUniverse u

9999

100100 dens x | fullname = x

src/Idris/Docs.hs+6−6

@@ -296,12 +296,12 @@ getPArgNames _ _ = []

296296

297297pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation

298298pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>

299− pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>

299+ pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+>

300300 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>

301301 nest 4 (line <> text str)

302302

303− where t (Fl _) = PConstant $ AType ATFloat

304− t (BI _) = PConstant $ AType (ATInt ITBig)

305− t (Str _) = PConstant StrType

306− t (Ch c) = PConstant $ AType (ATInt ITChar)

307− t _ = PType

303+ where t (Fl _) = PConstant NoFC $ AType ATFloat

304+ t (BI _) = PConstant NoFC $ AType (ATInt ITBig)

305+ t (Str _) = PConstant NoFC StrType

306+ t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)

307+ t _ = PType NoFC

src/Idris/Elab/Class.hs+2−2

@@ -58,7 +58,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

5858 [Name] -> [PDecl] -> Idris ()

5959elabClass info syn_in doc fc constraints tn ps pDocs fds ds

6060 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

61− let tty = pibind ps PType

61+ let tty = pibind ps (PType fc)

6262 let constraint = PApp fc (PRef fc tn)

6363 (map (pexp . PRef fc) (map fst ps))

6464

@@ -110,7 +110,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

110110

111111 -- To make sure the type constructor of the class is in the appropriate

112112 -- uniqueness hierarchy

113− chkUniq u@(PUniverse _) PType = u

113+ chkUniq u@(PUniverse _) (PType _) = u

114114 chkUniq (PUniverse l) (PUniverse r) = PUniverse (min l r)

115115 chkUniq (PPi _ _ _ sc) t = chkUniq sc t

116116 chkUniq _ t = t

src/Idris/Elab/Clause.hs+24−13

@@ -16,7 +16,7 @@ import Idris.Inliner

1616import Idris.PartialEval

1717import Idris.Transforms

1818import Idris.DeepSeq

19−import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult)

19+import Idris.Output (iputStrLn, pshow, iWarn, iRenderResult, sendHighlighting)

2020import IRTS.Lang

2121

2222import Idris.Elab.AsPat

@@ -453,9 +453,10 @@ checkPossible info fc tcgen fname lhs_in

453453 -- if the LHS type checks, it is possible

454454 case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

455455 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

456− OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->

456+ OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->

457457 do setContext ctxt'

458458 processTacticDecls info newDecls

459+ sendHighlighting highlights

459460 let lhs_tm = orderPats (getInferTerm lhs')

460461 case recheck ctxt [] (forget lhs_tm) lhs_tm of

461462 OK _ -> return True

@@ -537,7 +538,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

537538 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

538539 "\n" ++ show (fn_ty, fn_is))

539540

540− ((ElabResult lhs' dlhs [] ctxt' newDecls, probs, inj), _) <-

541+ ((ElabResult lhs' dlhs [] ctxt' newDecls highlights, probs, inj), _) <-

541542 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

542543 (do res <- errAt "left hand side of " fname

543544 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

@@ -546,6 +547,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

546547 return (res, probs, inj))

547548 setContext ctxt'

548549 processTacticDecls info newDecls

550+ sendHighlighting highlights

551+

549552 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

550553

551554 let lhs_tm = orderPats (getInferTerm lhs')

@@ -612,12 +615,12 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

612615 logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

613616 ctxt <- getContext -- new context with where block added

614617 logLvl 5 "STARTING CHECK"

615− ((rhs', defer, is, probs, ctxt', newDecls), _) <-

618+ ((rhs', defer, is, probs, ctxt', newDecls, highlights), _) <-

616619 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

617620 (do pbinds ist lhs_tm

618621 mapM_ setinj (nub (params ++ inj))

619622 setNextName

620− (ElabResult _ _ is ctxt' newDecls) <-

623+ (ElabResult _ _ is ctxt' newDecls highlights) <-

621624 errAt "right hand side of " fname

622625 (erun fc (build i winfo ERHS opts fname rhs))

623626 errAt "right hand side of " fname

@@ -629,9 +632,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

629632 let (tm, ds) = runState (collectDeferred (Just fname)

630633 (map fst $ case_decls aux) ctxt tt) []

631634 probs <- get_probs

632− return (tm, ds, is, probs, ctxt', newDecls))

635+ return (tm, ds, is, probs, ctxt', newDecls, highlights))

633636 setContext ctxt'

634637 processTacticDecls info newDecls

638+ sendHighlighting highlights

639+

635640 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

636641

637642 logLvl 5 "DONE CHECK"

@@ -774,12 +779,14 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

774779 let params = getParamsInType i [] fn_is fn_ty

775780 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

776781 logLvl 2 ("LHS: " ++ show lhs)

777− (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

782+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

778783 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

779784 (errAt "left hand side of with in " fname

780785 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

781786 setContext ctxt'

782787 processTacticDecls info newDecls

788+ sendHighlighting highlights

789+

783790 let lhs_tm = orderPats (getInferTerm lhs')

784791 let lhs_ty = getInferType lhs'

785792 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

@@ -791,19 +798,21 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

791798 let wval = addImplBound i (map fst bargs) wval_in

792799 logLvl 5 ("Checking " ++ showTmImpls wval)

793800 -- Elaborate wval in this context

794− ((wval', defer, is, ctxt', newDecls), _) <-

801+ ((wval', defer, is, ctxt', newDecls, highlights), _) <-

795802 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

796803 (bindTyArgs PVTy bargs infP) initEState

797804 (do pbinds i lhs_tm

798805 setNextName

799806 -- TODO: may want where here - see winfo abpve

800− (ElabResult _ d is ctxt' newDecls) <- errAt "with value in " fname

807+ (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname

801808 (erun fc (build i info ERHS opts fname (infTerm wval)))

802809 erun fc $ psolve lhs_tm

803810 tt <- get_term

804− return (tt, d, is, ctxt', newDecls))

811+ return (tt, d, is, ctxt', newDecls, highlights))

805812 setContext ctxt'

806813 processTacticDecls info newDecls

814+ sendHighlighting highlights

815+

807816 def' <- checkDef fc iderr defer

808817 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

809818 addDeferred def''

@@ -889,16 +898,18 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

889898 logLvl 5 ("New RHS " ++ showTmImpls rhs)

890899 ctxt <- getContext -- New context with block added

891900 i <- getIState

892− ((rhs', defer, is, ctxt', newDecls), _) <-

901+ ((rhs', defer, is, ctxt', newDecls, highlights), _) <-

893902 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "wpatRHS") clhsty initEState

894903 (do pbinds i lhs_tm

895904 setNextName

896− (ElabResult _ d is ctxt' newDecls) <- erun fc (build i info ERHS opts fname rhs)

905+ (ElabResult _ d is ctxt' newDecls highlights) <-

906+ erun fc (build i info ERHS opts fname rhs)

897907 psolve lhs_tm

898908 tt <- get_term

899− return (tt, d, is, ctxt', newDecls))

909+ return (tt, d, is, ctxt', newDecls, highlights))

900910 setContext ctxt'

901911 processTacticDecls info newDecls

912+ sendHighlighting highlights

902913

903914 def' <- checkDef fc iderr defer

904915 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

src/Idris/Elab/Data.hs+2−2

@@ -377,7 +377,7 @@ elabCaseFun ind paramPos n ty cons info = do

377377 where keyOf :: PTerm -> String

378378 keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"

379379 keyOf (PApp _ tyf _) = keyOf tyf

380− keyOf PType = "ty__"

380+ keyOf (PType _) = "ty__"

381381 keyOf _ = "carg__"

382382 nameStart :: Name -> Char

383383 nameStart n = nameStart' (simpleName n)

@@ -414,7 +414,7 @@ elabCaseFun ind paramPos n ty cons info = do

414414 mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm

415415 mkMotive n paramPos params indicies =

416416 let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))

417− in piConstr (indicies ++ [scrutineeTy]) PType

417+ in piConstr (indicies ++ [scrutineeTy]) (PType elimFC)

418418

419419 piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm

420420 piConstr [] ty = ty

src/Idris/Elab/Instance.hs+4−3

@@ -14,7 +14,7 @@ import Idris.Primitives

1414import Idris.Inliner

1515import Idris.PartialEval

1616import Idris.DeepSeq

17−import Idris.Output (iputStrLn, pshow, iWarn)

17+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

1818import IRTS.Lang

1919

2020import Idris.Elab.Type

@@ -146,7 +146,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

146146

147147 where

148148 intInst = case ps of

149− [PConstant (AType (ATInt ITNative))] -> True

149+ [PConstant NoFC (AType (ATInt ITNative))] -> True

150150 _ -> False

151151

152152 mkiname n' ns ps' expn' =

@@ -176,11 +176,12 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

176176 ty' <- implicit info syn iname ty'

177177 let ty = addImpl [] i ty'

178178 ctxt <- getContext

179− (ElabResult tyT _ _ ctxt' newDecls, _) <-

179+ (ElabResult tyT _ _ ctxt' newDecls highlights, _) <-

180180 tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState

181181 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

182182 setContext ctxt'

183183 processTacticDecls info newDecls

184+ sendHighlighting highlights

184185 ctxt <- getContext

185186 (cty, _) <- recheckC fc id [] tyT

186187 let nty = normalise ctxt [] cty

src/Idris/Elab/Provider.hs+1−1

@@ -66,7 +66,7 @@ elabProvider doc info syn fc what n

6666 -- The goal type for a postulate is always Type.

6767 (ty', typ) <- case what of

6868 ProvTerm ty p -> elabVal info ERHS ty

69− ProvPostulate _ -> elabVal info ERHS PType

69+ ProvPostulate _ -> elabVal info ERHS (PType fc)

7070 unless (isTType typ) $

7171 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

7272

src/Idris/Elab/Record.hs+1−1

@@ -67,7 +67,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn

6767 -- | Generates a type constructor.

6868 generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm

6969 generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)

70− generateTyConType [] = PType

70+ generateTyConType [] = (PType fc)

7171

7272 -- | Generates a name for the data constructor if none was specified.

7373 generateDConName :: Maybe Name -> Idris Name

src/Idris/Elab/Term.hs+20−11

@@ -48,6 +48,7 @@ data ElabResult =

4848 -- ^ The potentially extended context from new definitions

4949 , resultTyDecls :: [RDeclInstructions]

5050 -- ^ Meta-info about the new type declarations

51+ , resultHighlighting :: [(FC, OutputAnnotation)]

5152 }

5253

5354

@@ -110,13 +111,14 @@ build ist info emode opts fn tm

110111 when tydecl (do mkPat

111112 update_term liftPats

112113 update_term orderPats)

113− EState is _ impls <- getAux

114+ EState is _ impls highlights <- getAux

114115 tt <- get_term

115116 ctxt <- get_context

116117 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

117118 log <- getLog

118− if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)

119− else return (ElabResult tm ds (map snd is) ctxt impls)

119+ if log /= ""

120+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)

121+ else return (ElabResult tm ds (map snd is) ctxt impls highlights)

120122 where pattern = emode == ELHS

121123 tydecl = emode == ETyDecl

122124

@@ -152,13 +154,14 @@ buildTC ist info emode opts fn tm

152154 -- unification

153155 when (not (null dots)) $

154156 lift (Error (CantMatch (getInferTerm tm)))

155− EState is _ impls <- getAux

157+ EState is _ impls highlights <- getAux

156158 tt <- get_term

157159 ctxt <- get_context

158160 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

159161 log <- getLog

160− if (log /= "") then trace log $ return (ElabResult tm ds (map snd is) ctxt impls)

161− else return (ElabResult tm ds (map snd is) ctxt impls)

162+ if (log /= "")

163+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)

164+ else return (ElabResult tm ds (map snd is) ctxt impls highlights)

162165 where pattern = emode == ELHS

163166

164167-- return whether arguments of the given constructor name can be

@@ -318,24 +321,30 @@ elab ist info emode opts fn tm

318321 -> PTerm -- ^ The term to elaborate

319322 -> ElabD ()

320323 elab' ina fc (PNoImplicits t) = elab' ina fc t -- skip elabE step

321− elab' ina fc PType = do apply RType []; solve

324+ elab' ina fc (PType fc') =

325+ do apply RType []

326+ solve

327+ highlightSource fc' (AnnType "Type" "The type of types")

322328 elab' ina fc (PUniverse u) = do apply (RUType u) []; solve

323329-- elab' (_,_,inty) (PConstant c)

324330-- | constType c && pattern && not reflection && not inty

325331-- = lift $ tfail (Msg "Typecase is not allowed")

326− elab' ina fc tm@(PConstant c)

332+ elab' ina fc tm@(PConstant fc' c)

327333 | pattern && not reflection && not (e_qq ina) && not (e_intype ina)

328334 && isTypeConst c

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

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

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

332− | otherwise = do apply (RConstant c) []; solve

338+ | otherwise = do apply (RConstant c) []

339+ solve

340+ highlightSource fc' (AnnConst c)

333341 elab' ina fc (PQuote r) = do fill r; solve

334342 elab' ina _ (PTrue fc _) =

335343 do hnf_compute

336344 g <- goal

337345 case g of

338− TType _ -> elab' ina (Just fc) (PRef fc unitTy)

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

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

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

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

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

@@ -2276,7 +2285,7 @@ processTacticDecls info steps =

22762285 let tcgen = False -- TODO: later we may support dictionary generation

22772286 case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState

22782287 (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of

2279− OK (ElabResult lhs' _ _ _ _, _) ->

2288+ OK (ElabResult lhs' _ _ _ _ _, _) ->

22802289 do -- not recursively calling here, because we don't

22812290 -- want to run infinitely many times

22822291 let lhs_tm = orderPats (getInferTerm lhs')

src/Idris/Elab/Transform.hs+5−3

@@ -14,7 +14,7 @@ import Idris.Primitives

1414import Idris.Inliner

1515import Idris.PartialEval

1616import Idris.DeepSeq

17−import Idris.Output (iputStrLn, pshow, iWarn)

17+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

1818import IRTS.Lang

1919

2020import Idris.Elab.Utils

@@ -53,12 +53,13 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

56− (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

56+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

5757 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

5858 (erun fc (buildTC i info ELHS [] (sUN "transform")

5959 (infTerm lhs)))

6060 setContext ctxt'

6161 processTacticDecls info newDecls

62+ sendHighlighting highlights

6263 let lhs_tm = orderPats (getInferTerm lhs')

6364 let lhs_ty = getInferType lhs'

6465 let newargs = pvars i lhs_tm

@@ -72,13 +73,14 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

7273 tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

7374 (do pbinds i lhs_tm

7475 setNextName

75− (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

76+ (ElabResult _ _ _ ctxt' newDecls highlights) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

7677 erun fc $ psolve lhs_tm

7778 tt <- get_term

7879 let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []

7980 return (rhs', defer, ctxt', newDecls))

8081 setContext ctxt'

8182 processTacticDecls info newDecls

83+ sendHighlighting highlights

8284

8385 (crhs_tm_in, crhs_ty) <- recheckC fc id [] rhs'

8486 let crhs_tm = renamepats pnames crhs_tm_in

src/Idris/Elab/Type.hs+3−2

@@ -16,7 +16,7 @@ import Idris.Primitives

1616import Idris.Inliner

1717import Idris.PartialEval

1818import Idris.DeepSeq

19−import Idris.Output (iputStrLn, pshow, iWarn)

19+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

2020import IRTS.Lang

2121

2222import Idris.Elab.Utils

@@ -66,11 +66,12 @@ buildType info syn fc opts n ty' = do

6666 logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

6767 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6868

69− (ElabResult tyT' defer is ctxt' newDecls, log) <-

69+ (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

7070 tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

7171 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

7272 setContext ctxt'

7373 processTacticDecls info newDecls

74+ sendHighlighting highlights

7475

7576 let tyT = patToImp tyT'

7677

src/Idris/Elab/Value.hs+7−6

@@ -15,7 +15,7 @@ import Idris.Primitives

1515import Idris.Inliner

1616import Idris.PartialEval

1717import Idris.DeepSeq

18−import Idris.Output (iputStrLn, pshow, iWarn)

18+import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

1919import IRTS.Lang

2020

2121import Idris.Elab.Utils

@@ -63,13 +63,14 @@ elabValBind info aspat norm tm_in

6363 -- * elaboration as a Type

6464 -- * elaboration as a function a -> b

6565

66− (ElabResult tm' defer is ctxt' newDecls, _) <-

66+ (ElabResult tm' defer is ctxt' newDecls highlights, _) <-

6767 tclift (elaborate ctxt (idris_datatypes i) (sMN 0 "val") infP initEState

6868 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

6969

7070 -- Extend the context with new definitions created

7171 setContext ctxt'

7272 processTacticDecls info newDecls

73+ sendHighlighting highlights

7374

7475 let vtm = orderPats (getInferTerm tm')

7576

@@ -118,14 +119,14 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

118119-- Try running the term directly (as IO ()), then printing it as an Integer

119120-- (as a default numeric tye), then printing it as any Showable thing

120121elabExec :: FC -> PTerm -> PTerm

121−elabExec fc tm = runtm (PAlternative False

122+elabExec fc tm = runtm (PAlternative False

122123 [printtm (PApp fc (PRef fc (sUN "the"))

123− [pexp (PConstant (AType (ATInt ITBig))), pexp tm]),

124+ [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

124125 tm,

125126 printtm tm

126127 ])

127− where

128+ where

128129 runtm t = PApp fc (PRef fc (sUN "run__IO")) [pexp t]

129− printtm t = PApp fc (PRef fc (sUN "printLn"))

130+ printtm t = PApp fc (PRef fc (sUN "printLn"))

130131 [pimp (sUN "ffi") (PRef fc (sUN "FFI_C")) False, pexp t]

131132

src/Idris/Error.hs+3−3

@@ -114,16 +114,16 @@ warnDisamb ist (PPair _ _ x y) = warnDisamb ist x >> warnDisamb ist y

114114warnDisamb ist (PDPair _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

115115warnDisamb ist (PAlternative _ tms) = mapM_ (warnDisamb ist) tms

116116warnDisamb ist (PHidden tm) = warnDisamb ist tm

117−warnDisamb ist PType = return ()

117+warnDisamb ist (PType _) = return ()

118118warnDisamb ist (PUniverse _) = return ()

119119warnDisamb ist (PGoal _ x _ y) = warnDisamb ist x >> warnDisamb ist y

120−warnDisamb ist (PConstant _) = return ()

120+warnDisamb ist (PConstant _ _) = return ()

121121warnDisamb ist Placeholder = return ()

122122warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

123123 where wStep (DoExp _ x) = warnDisamb ist x

124124 wStep (DoBind _ _ x) = warnDisamb ist x

125125 wStep (DoBindP _ x y cs) = warnDisamb ist x >> warnDisamb ist y >>

126− mapM_ (\(x,y)-> warnDisamb ist x >> warnDisamb ist y) cs

126+ mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

127127 wStep (DoLet _ _ x y) = warnDisamb ist x >> warnDisamb ist y

128128 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

129129warnDisamb ist (PIdiom _ x) = warnDisamb ist x

src/Idris/IBC.hs+10−6

@@ -41,7 +41,7 @@ import Codec.Archive.Zip

4141import Util.Zlib (decompressEither)

4242

4343ibcVersion :: Word16

44−ibcVersion = 107

44+ibcVersion = 108

4545

4646data IBCFile = IBCFile { ver :: Word16,

4747 sourcefile :: FilePath,

@@ -1570,14 +1570,16 @@ instance Binary PTerm where

15701570 put x2

15711571 PHidden x1 -> do putWord8 21

15721572 put x1

1573− PType -> putWord8 22

1573+ PType x1 -> do putWord8 22

1574+ put x1

15741575 PGoal x1 x2 x3 x4 -> do putWord8 23

15751576 put x1

15761577 put x2

15771578 put x3

15781579 put x4

1579− PConstant x1 -> do putWord8 24

1580− put x1

1580+ PConstant x1 x2 -> do putWord8 24

1581+ put x1

1582+ put x2

15811583 Placeholder -> putWord8 25

15821584 PDoBlock x1 -> do putWord8 26

15831585 put x1

@@ -1709,14 +1711,16 @@ instance Binary PTerm where

17091711 return (PAlternative x1 x2)

17101712 21 -> do x1 <- get

17111713 return (PHidden x1)

1712− 22 -> return PType

1714+ 22 -> do x1 <- get

1715+ return (PType x1)

17131716 23 -> do x1 <- get

17141717 x2 <- get

17151718 x3 <- get

17161719 x4 <- get

17171720 return (PGoal x1 x2 x3 x4)

17181721 24 -> do x1 <- get

1719− return (PConstant x1)

1722+ x2 <- get

1723+ return (PConstant x1 x2)

17201724 25 -> return Placeholder

17211725 26 -> do x1 <- get

17221726 return (PDoBlock x1)

src/Idris/IdeMode.hs+2

@@ -169,6 +169,8 @@ instance SExpable FC where

169169 toSExp ((SymbolAtom "filename", StringAtom f),

170170 (SymbolAtom "start", IntegerAtom (toInteger sl), IntegerAtom (toInteger sc)),

171171 (SymbolAtom "end", IntegerAtom (toInteger el), IntegerAtom (toInteger ec)))

172+ toSExp NoFC = toSExp ([] :: [String])

173+ toSExp (FileFC f) = toSExp [(SymbolAtom "filename", StringAtom f)]

172174

173175escape :: String -> String

174176escape = concatMap escapeChar

src/Idris/Output.hs+14

@@ -194,6 +194,20 @@ prettyDocumentedIst ist (name, ty, docs) =

194194 where ppTm = pprintDelab ist

195195 norm = normaliseAll (tt_ctxt ist) []

196196

197+sendHighlighting :: [(FC, OutputAnnotation)] -> Idris ()

198+sendHighlighting [] = return ()

199+sendHighlighting highlights =

200+ do ist <- getIState

201+ case idris_outputmode ist of

202+ RawOutput _ -> return ()

203+ IdeMode n h ->

204+ let fancier = [toSExp (fc, fancifyAnnots ist annot) | (fc, annot) <- highlights]

205+ in runIO . hPutStrLn h $

206+ convSExp "output"

207+ (SymbolAtom "ok",

208+ (SymbolAtom "highlight-source", fancier)) n

209+

210+

197211

198212renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

199213renderExternal fmt width doc

src/Idris/ParseData.hs+3−2

@@ -137,7 +137,8 @@ recordParameter syn =

137137 onlyName :: SyntaxInfo -> IdrisParser (Name, PTerm)

138138 onlyName syn =

139139 do n <- fnName

140− return (expandNS syn n, PType)

140+ fc <- getFC

141+ return (expandNS syn n, PType fc)

141142

142143{- | Parses data declaration type (normal or codata)

143144DataI ::= 'data' | 'codata';

@@ -201,7 +202,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

201202 accData acc tyn (map (\ (_, _, n, _, _, _) -> n) cons)

202203 return $ PData doc argDocs syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

203204 args <- many name

204− let ty = bindArgs (map (const PType) args) PType

205+ let ty = bindArgs (map (const (PType fc)) args) (PType fc)

205206 let tyn = expandNS syn tyn_in

206207 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

207208 try (lchar '=') <|> do reserved "where"

src/Idris/ParseExpr.hs+26−25

@@ -335,18 +335,18 @@ simpleExpr syn =

335335 <|> tacticsExpr syn

336336 <|> try (do reserved "Type"; symbol "*"; return $ PUniverse AllTypes)

337337 <|> do reserved "AnyType"; return $ PUniverse AllTypes

338− <|> do reserved "Type"; return PType

338+ <|> PType <$> reservedFC "Type"

339339 <|> do reserved "UniqueType"; return $ PUniverse UniqueType

340340 <|> do reserved "NullType"; return $ PUniverse NullType

341− <|> do c <- constant

341+ <|> do (c, cfc) <- constant

342342 fc <- getFC

343− return (modifyConst syn fc (PConstant c))

343+ return (modifyConst syn fc (PConstant cfc c))

344344 <|> do symbol "'"; fc <- getFC; str <- name

345345 return (PApp fc (PRef fc (sUN "Symbol_"))

346− [pexp (PConstant (Str (show str)))])

346+ [pexp (PConstant NoFC (Str (show str)))])

347347 <|> do fc <- getFC

348348 x <- fnName

349− if inPattern syn

349+ if inPattern syn

350350 then option (PRef fc x)

351351 (do reservedOp "@"

352352 s <- simpleExpr syn

@@ -445,19 +445,19 @@ bracketedExpr syn e =

445445-- name suggests, rather than Int

446446{-| Finds optimal type for integer constant -}

447447modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

448−modifyConst syn fc (PConstant (BI x))

448+modifyConst syn fc (PConstant inFC (BI x))

449449 | not (inPattern syn)

450450 = PAlternative False

451− (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI (fromInteger x)))]

451+ (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant NoFC (BI (fromInteger x)))]

452452 : consts)

453453 | otherwise = PAlternative False consts

454454 where

455− consts = [ PConstant (BI x)

456− , PConstant (I (fromInteger x))

457− , PConstant (B8 (fromInteger x))

458− , PConstant (B16 (fromInteger x))

459− , PConstant (B32 (fromInteger x))

460− , PConstant (B64 (fromInteger x))

455+ consts = [ PConstant inFC (BI x)

456+ , PConstant inFC (I (fromInteger x))

457+ , PConstant inFC (B8 (fromInteger x))

458+ , PConstant inFC (B16 (fromInteger x))

459+ , PConstant inFC (B32 (fromInteger x))

460+ , PConstant inFC (B64 (fromInteger x))

461461 ]

462462modifyConst syn fc x = x

463463

@@ -1219,14 +1219,12 @@ Constant ::=

12191219-}

12201220

12211221constants :: [(String, Idris.Core.TT.Const)]

1222−constants =

1222+constants =

12231223 [ ("Integer", AType (ATInt ITBig))

12241224 , ("Int", AType (ATInt ITNative))

12251225 , ("Char", AType (ATInt ITChar))

12261226 , ("Double", AType ATFloat)

12271227 , ("String", StrType)

1228−-- , ("Ptr", PtrType)

1229−-- , ("ManagedPtr", ManagedPtrType)

12301228 , ("prim__WorldType", WorldType)

12311229 , ("prim__TheWorld", TheWorld)

12321230 , ("Bits8", AType (ATInt (ITFixed IT8)))

@@ -1234,14 +1232,17 @@ constants =

12341232 , ("Bits32", AType (ATInt (ITFixed IT32)))

12351233 , ("Bits64", AType (ATInt (ITFixed IT64)))

12361234 ]

1237−

1238−constant :: IdrisParser Idris.Core.TT.Const

1239−constant = choice [ do reserved name; return ty | (name, ty) <- constants ]

1240− <|> do f <- try float; return $ Fl f

1241− <|> do i <- natural; return $ BI i

1242− <|> do s <- verbatimStringLiteral; return $ Str s

1243− <|> do s <- stringLiteral; return $ Str s

1244− <|> do c <- try charLiteral; return $ Ch c --Currently ambigous with symbols

1235+

1236+-- | Parse a constant and its source span

1237+constant :: IdrisParser (Idris.Core.TT.Const, FC)

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

1239+ | (name, ty) <- constants

1240+ ]

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

12451246 <?> "constant or literal"

12461247

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

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

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

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

13911392 do whiteSpace

1392− doc <- (Right <$> constant) <|> (Left <$> fnName)

1393+ doc <- (Right . fst <$> constant) <|> (Left <$> fnName)

13931394 eof

13941395 return (TDocStr doc))

13951396 ]

src/Idris/ParseHelpers.hs+17

@@ -250,6 +250,13 @@ symbol = Tok.symbol

250250reserved :: MonadicParsing m => String -> m ()

251251reserved = Tok.reserve idrisStyle

252252

253+-- | Parses a reserved identifier, computing its span. Assumes that

254+-- reserved identifiers never contain line breaks.

255+reservedFC :: MonadicParsing m => String -> m FC

256+reservedFC str = do (FC file (l, c) _) <- getFC

257+ Tok.reserve idrisStyle str

258+ return $ FC file (l, c) (l, c + length str)

259+

253260-- Taken from Parsec (c) Daan Leijen 1999-2001, (c) Paolo Martini 2007

254261-- | Parses a reserved operator

255262reservedOp :: MonadicParsing m => String -> m ()

@@ -360,6 +367,16 @@ getFC = do s <- position

360367 -- Issue #1594 on the Issue Tracker.

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

362369

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+

363380{-* Syntax helpers-}

364381-- | Bind constraints to term

365382bindList :: (Name -> PTerm -> PTerm -> PTerm) -> [(Name, PTerm)] -> PTerm -> PTerm

src/Idris/Parser.hs+4−3

@@ -674,8 +674,9 @@ class_ syn = do (doc, argDocs, acc)

674674 carg :: IdrisParser (Name, PTerm)

675675 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

676676 return (i, ty)

677− <|> do i <- name;

678− return (i, PType)

677+ <|> do i <- name

678+ fc <- getFC

679+ return (i, PType fc)

679680

680681{- | Parses a type class instance declaration

681682

@@ -1187,7 +1188,7 @@ parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

11871188

11881189{- | Parses a constant form input -}

11891190parseConst :: IState -> String -> Result Const

1190−parseConst st = runparser constant st "(input)"

1191+parseConst st = runparser (fmap fst constant) st "(input)"

11911192

11921193{- | Parses a tactic from input -}

11931194parseTactic :: IState -> String -> Result PTactic

src/Idris/Prover.hs+1−1

@@ -297,7 +297,7 @@ ploop fn d prompt prf e h

297297 infixes = idris_infixes ist

298298 action = case tm of

299299 TType _ ->

300− iPrintTermWithType (prettyImp ppo PType) type1Doc

300+ iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc

301301 _ -> let bnd = map (\x -> (fst x, False)) env in

302302 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

303303 (pprintPTerm ppo bnd [] infixes (delab ist ty))

src/Idris/REPL.hs+1−1

@@ -932,7 +932,7 @@ process fn (Check t)

932932 ty' = normaliseC ctxt [] ty

933933 case tm of

934934 TType _ ->

935− iPrintTermWithType (prettyIst ist PType) type1Doc

935+ iPrintTermWithType (prettyIst ist (PType emptyFC)) type1Doc

936936 _ -> iPrintTermWithType (pprintDelab ist tm)

937937 (pprintDelab ist ty)

938938

src/Idris/REPLParser.hs+1−1

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

265265cmd_doc :: String -> P.IdrisParser (Either String Command)

266266cmd_doc name = do

267267 let constant = do

268− c <- P.constant

268+ c <- fmap fst P.constant

269269 eof

270270 return $ Right (DocStr (Right c) FullDocs)

271271