c46243b · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

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

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

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

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

1151− pri (PConstant _) = 0

1151+ pri (PConstant _ _) = 0

1152 pri Placeholder = 1

1153 pri _ = 3

1154

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/AbsSyntaxTree.hs+21−16

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

670data EState = EState {

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

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

673− new_tyDecls :: [RDeclInstructions]

673+ new_tyDecls :: [RDeclInstructions],

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

674 }

675 }

675

676

676initEState :: EState

677initEState :: EState

677−initEState = EState [] [] []

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

678

679

679type ElabD a = Elab' EState a

680type ElabD a = Elab' EState a

680

681

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

683+highlightSource fc annot =

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

685+

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

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

682--

687--

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

688-- 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

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

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

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

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

827 | PHidden PTerm -- ^ Irrelevant or hidden pattern

832 | PHidden PTerm -- ^ Irrelevant or hidden pattern

828− | PType -- ^ 'Type' type

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

829 | PUniverse Universe -- ^ Some universe

834 | PUniverse Universe -- ^ Some universe

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

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

831− | PConstant Const -- ^ Builtin types

836+ | PConstant FC Const -- ^ Builtin types

832 | Placeholder -- ^ Underscore

837 | Placeholder -- ^ Underscore

833 | PDoBlock [PDo] -- ^ Do notation

838 | PDoBlock [PDo] -- ^ Do notation

834 | PIdiom FC PTerm -- ^ Idiom brackets

839 | PIdiom FC PTerm -- ^ Idiom brackets

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

1037 [] -> Nothing

1042 [] -> Nothing

1038 (fc:_) -> Just fc

1043 (fc:_) -> Just fc

1039highestFC (PHidden _) = Nothing

1044highestFC (PHidden _) = Nothing

1040−highestFC PType = Nothing

1045+highestFC (PType fc) = Just fc

1041highestFC (PUniverse _) = Nothing

1046highestFC (PUniverse _) = Nothing

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

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

1043−highestFC (PConstant _) = Nothing

1048+highestFC (PConstant fc _) = Just fc

1044highestFC Placeholder = Nothing

1049highestFC Placeholder = Nothing

1045highestFC (PDoBlock lines) =

1050highestFC (PDoBlock lines) =

1046 case map getDoFC lines of

1051 case map getDoFC lines of

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

1256inferTy = sMN 0 "__Infer"

1261inferTy = sMN 0 "__Infer"

1257inferCon = sMN 0 "__infer"

1262inferCon = sMN 0 "__infer"

1258inferDecl = PDatadecl inferTy

1263inferDecl = PDatadecl inferTy

1259− PType

1264+ (PType bi)

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

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

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

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

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

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

1263inferOpts = []

1268inferOpts = []

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

1312 "\n\n" ++

1317 "\n\n" ++

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

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

1314

1319

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

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

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

1317− PType))

1322+ (PType bi)))

1318 [(reflDoc, reflParamDoc,

1323 [(reflDoc, reflParamDoc,

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

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

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

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

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

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

1322 pimp (n "B") Placeholder False,

1327 pimp (n "B") Placeholder False,

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

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

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

1514 group (prettySe right bnd r)

1519 group (prettySe right bnd r)

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

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

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

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

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

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

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

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

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

1605 where

1610 where

1606 prettyAs =

1611 prettyAs =

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

1612 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"

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

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

1611 -- XXX: add pretty for tactics

1616 -- XXX: add pretty for tactics

1612 prettySe p bnd (PProof ts) =

1617 prettySe p bnd (PProof ts) =

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

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

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

1881 size (PUnifyLog tm) = size tm

1886 size (PUnifyLog tm) = size tm

1882 size (PDisamb _ tm) = size tm

1887 size (PDisamb _ tm) = size tm

1883 size (PNoImplicits tm) = size tm

1888 size (PNoImplicits tm) = size tm

1884− size PType = 1

1889+ size (PType _) = 1

1885 size (PUniverse _) = 1

1890 size (PUniverse _) = 1

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

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

1887 size Placeholder = 1

1892 size Placeholder = 1

1888 size (PDoBlock dos) = 1 + size dos

1893 size (PDoBlock dos) = 1 + size dos

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

1894 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

249----- Generated by 'derive'

250

251instance Binary FC where

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

252+ put x =

253+ case x of

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

253− = do put x1

255+ put x1

254− put (x2 * 65536 + x3)

256+ put (x2 * 65536 + x3)

255− put (x4 * 65536 + x5)

257+ put (x4 * 65536 + x5)

258+ NoFC -> putWord8 1

259+ FileFC x1 -> do putWord8 2

260+ put x1

256 get

261 get

262+ = do i <- getWord8

263+ case i of

257− = do x1 <- get

264+ 0 -> do x1 <- get

258− x2x3 <- get

265+ x2x3 <- get

259− x4x5 <- get

266+ x4x5 <- get

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

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"

261

272

262

273

263instance Binary Name where

274instance Binary Name where

src/Idris/Core/DeepSeq.hs+2

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

43

44instance NFData FC where

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

46+ rnf NoFC = ()

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

46

48

47instance NFData Provenance where

49instance NFData Provenance where

48 rnf ExpectedType = ()

50 rnf ExpectedType = ()

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

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

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

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

55 }

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

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

56− deriving (Data, Typeable, Ord)

58+ deriving (Data, Typeable, Ord)

57

59

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

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

59instance Eq FC where

61instance Eq FC where

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

65instance Eq FC' where

67instance Eq FC' where

66 FC' fc == FC' fc' = fcEq fc fc'

68 FC' fc == FC' fc' = fcEq fc fc'

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

69 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

68

73

69-- | Empty source location

74-- | Empty source location

70emptyFC :: FC

75emptyFC :: FC

71−emptyFC = fileFC ""

76+emptyFC = NoFC

72

77

73−-- | Source location with file only

78+-- | Source location with file only

74fileFC :: String -> FC

79fileFC :: String -> FC

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

80+fileFC s = FileFC s

76

81

77{-!

82{-!

78deriving instance Binary FC

83deriving instance Binary FC

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

81

86

82instance Sized FC where

87instance Sized FC where

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

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

89+ size NoFC = 1

90+ size (FileFC f) = length f

84

91

85instance Show FC where

92instance Show FC where

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

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

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

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

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

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

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

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

97+ show NoFC = "No location"

98+ show (FileFC f) = f

90

99

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

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

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

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

src/Idris/Coverage.hs+4−4

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

179 where

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

181 -- constants which are not explicitly handled are covered

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

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

183− where getConst (PConstant c) = Just c

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

184 getConst _ = Nothing

185 inventConsts xs = xs

186

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

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

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

228 [pexp t,pexp v]) o

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

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

230 otherPats arg = return Placeholder

231

232 ops fc n xs o

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

278

279 -- quick check for constructor equality

280 quickEq :: PTerm -> PTerm -> Bool

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

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

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

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

284 | length as == length as'

src/Idris/DSL.hs+2−2

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

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

34 [ pexp (stringC x)

35 , pexp (mkList fc xs)]

36− stringC = PConstant . Str . str

36+ stringC = PConstant fc . Str . str

37− intC = PConstant . I

37+ intC = PConstant fc . I

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

39 in case n of

40 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

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

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

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

227− rnf PType = ()

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

228 rnf (PUniverse _) = ()

229 rnf (PGoal x1 x2 x3 x4)

230 = 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` ()

232 rnf Placeholder = ()

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

234 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

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

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

92 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

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

95 de env _ Erased = Placeholder

96 de env _ Impossible = Placeholder

97− de env _ (TType i) = PType

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

98 de env _ (UType u) = PUniverse u

99

100 dens x | fullname = x

src/Idris/Docs.hs+6−6

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

296

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

298pprintConstDocs 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 <+>

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

301 nest 4 (line <> text str)

302

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

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

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

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

305− t (Str _) = PConstant StrType

305+ t (Str _) = PConstant NoFC StrType

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

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

307− t _ = PType

307+ t _ = PType NoFC

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

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

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

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

60 = 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)

62 let constraint = PApp fc (PRef fc tn)

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

64

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

110

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

112 -- uniqueness hierarchy

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

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

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

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

116 chkUniq _ t = t

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

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

16import Idris.PartialEval

17import Idris.Transforms

18import Idris.DeepSeq

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

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

20import IRTS.Lang

21

22import Idris.Elab.AsPat

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

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

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

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

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

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

457 do setContext ctxt'

458 processTacticDecls info newDecls

459+ sendHighlighting highlights

459 let lhs_tm = orderPats (getInferTerm lhs')

460 let lhs_tm = orderPats (getInferTerm lhs')

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

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

461 OK _ -> return True

462 OK _ -> return True

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

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

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

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

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

539

540

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

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

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

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

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

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

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

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

546 return (res, probs, inj))

547 return (res, probs, inj))

547 setContext ctxt'

548 setContext ctxt'

548 processTacticDecls info newDecls

549 processTacticDecls info newDecls

550+ sendHighlighting highlights

551+

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

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

550

553

551 let lhs_tm = orderPats (getInferTerm lhs')

554 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

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

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

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

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

614 logLvl 5 "STARTING CHECK"

617 logLvl 5 "STARTING CHECK"

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

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

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

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

617 (do pbinds ist lhs_tm

620 (do pbinds ist lhs_tm

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

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

619 setNextName

622 setNextName

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

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

621 errAt "right hand side of " fname

624 errAt "right hand side of " fname

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

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

623 errAt "right hand side of " fname

626 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

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

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

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

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

631 probs <- get_probs

634 probs <- get_probs

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

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

633 setContext ctxt'

636 setContext ctxt'

634 processTacticDecls info newDecls

637 processTacticDecls info newDecls

638+ sendHighlighting highlights

639+

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

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

636

641

637 logLvl 5 "DONE CHECK"

642 logLvl 5 "DONE CHECK"

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

774 let params = getParamsInType i [] fn_is fn_ty

779 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

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

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

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

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

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

781 setContext ctxt'

786 setContext ctxt'

782 processTacticDecls info newDecls

787 processTacticDecls info newDecls

788+ sendHighlighting highlights

789+

783 let lhs_tm = orderPats (getInferTerm lhs')

790 let lhs_tm = orderPats (getInferTerm lhs')

784 let lhs_ty = getInferType lhs'

791 let lhs_ty = getInferType lhs'

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

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

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

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

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

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

793 -- Elaborate wval in this context

800 -- Elaborate wval in this context

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

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

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

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

796 (bindTyArgs PVTy bargs infP) initEState

803 (bindTyArgs PVTy bargs infP) initEState

797 (do pbinds i lhs_tm

804 (do pbinds i lhs_tm

798 setNextName

805 setNextName

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

806 -- 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

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

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

802 erun fc $ psolve lhs_tm

809 erun fc $ psolve lhs_tm

803 tt <- get_term

810 tt <- get_term

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

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

805 setContext ctxt'

812 setContext ctxt'

806 processTacticDecls info newDecls

813 processTacticDecls info newDecls

814+ sendHighlighting highlights

815+

807 def' <- checkDef fc iderr defer

816 def' <- checkDef fc iderr defer

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

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

809 addDeferred def''

818 addDeferred def''

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

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

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

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

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

891 i <- getIState

900 i <- getIState

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

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

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

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

894 (do pbinds i lhs_tm

903 (do pbinds i lhs_tm

895 setNextName

904 setNextName

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

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

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

897 psolve lhs_tm

907 psolve lhs_tm

898 tt <- get_term

908 tt <- get_term

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

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

900 setContext ctxt'

910 setContext ctxt'

901 processTacticDecls info newDecls

911 processTacticDecls info newDecls

912+ sendHighlighting highlights

902

913

903 def' <- checkDef fc iderr defer

914 def' <- checkDef fc iderr defer

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

915 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

377 where keyOf :: PTerm -> String

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

379 keyOf (PApp _ tyf _) = keyOf tyf

380− keyOf PType = "ty__"

380+ keyOf (PType _) = "ty__"

381 keyOf _ = "carg__"

382 nameStart :: Name -> Char

383 nameStart n = nameStart' (simpleName n)

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

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

415 mkMotive n paramPos params indicies =

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

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

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

418

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

420 piConstr [] ty = ty

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

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

14import Idris.Inliner

15import Idris.PartialEval

16import Idris.DeepSeq

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

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

18import IRTS.Lang

19

20import Idris.Elab.Type

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

146

147 where

148 intInst = case ps of

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

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

150 _ -> False

151

152 mkiname n' ns ps' expn' =

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

176 ty' <- implicit info syn iname ty'

177 let ty = addImpl [] i ty'

178 ctxt <- getContext

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

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

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

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

182 setContext ctxt'

183 processTacticDecls info newDecls

184+ sendHighlighting highlights

184 ctxt <- getContext

185 ctxt <- getContext

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

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

186 let nty = normalise ctxt [] cty

187 let nty = normalise ctxt [] cty

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

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

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

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

68 ProvTerm ty p -> elabVal info ERHS ty

69− ProvPostulate _ -> elabVal info ERHS PType

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

70 unless (isTType typ) $

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

72

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

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

67 -- | Generates a type constructor.

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

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

70− generateTyConType [] = PType

70+ generateTyConType [] = (PType fc)

71

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

73 generateDConName :: Maybe Name -> Idris Name

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

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

48 -- ^ The potentially extended context from new definitions

49 , resultTyDecls :: [RDeclInstructions]

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

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

51 }

52 }

52

53

54

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

110 when tydecl (do mkPat

111 when tydecl (do mkPat

111 update_term liftPats

112 update_term liftPats

112 update_term orderPats)

113 update_term orderPats)

113− EState is _ impls <- getAux

114+ EState is _ impls highlights <- getAux

114 tt <- get_term

115 tt <- get_term

115 ctxt <- get_context

116 ctxt <- get_context

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

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

117 log <- getLog

118 log <- getLog

119+ if log /= ""

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

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

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

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

120 where pattern = emode == ELHS

122 where pattern = emode == ELHS

121 tydecl = emode == ETyDecl

123 tydecl = emode == ETyDecl

122

124

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

152 -- unification

154 -- unification

153 when (not (null dots)) $

155 when (not (null dots)) $

154 lift (Error (CantMatch (getInferTerm tm)))

156 lift (Error (CantMatch (getInferTerm tm)))

155− EState is _ impls <- getAux

157+ EState is _ impls highlights <- getAux

156 tt <- get_term

158 tt <- get_term

157 ctxt <- get_context

159 ctxt <- get_context

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

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

159 log <- getLog

161 log <- getLog

162+ if (log /= "")

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

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

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

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

162 where pattern = emode == ELHS

165 where pattern = emode == ELHS

163

166

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

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

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

318 -> PTerm -- ^ The term to elaborate

321 -> PTerm -- ^ The term to elaborate

319 -> ElabD ()

322 -> ElabD ()

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

323 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")

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

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

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

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

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

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

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

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

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

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

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

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

328 && isTypeConst c

334 && isTypeConst c

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

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

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

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

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

337 = 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)

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

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

334 elab' ina _ (PTrue fc _) =

342 elab' ina _ (PTrue fc _) =

335 do hnf_compute

343 do hnf_compute

336 g <- goal

344 g <- goal

337 case g of

345 case g of

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2281 -- want to run infinitely many times

2290 -- want to run infinitely many times

2282 let lhs_tm = orderPats (getInferTerm lhs')

2291 let lhs_tm = orderPats (getInferTerm lhs')

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

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

14import Idris.Inliner

15import Idris.PartialEval

16import Idris.DeepSeq

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

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

18import IRTS.Lang

19

20import Idris.Elab.Utils

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

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

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

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

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

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

59 (infTerm lhs)))

60 setContext ctxt'

61 processTacticDecls info newDecls

62+ sendHighlighting highlights

62 let lhs_tm = orderPats (getInferTerm lhs')

63 let lhs_tm = orderPats (getInferTerm lhs')

63 let lhs_ty = getInferType lhs'

64 let lhs_ty = getInferType lhs'

64 let newargs = pvars i lhs_tm

65 let newargs = pvars i lhs_tm

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

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

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

73 (do pbinds i lhs_tm

74 (do pbinds i lhs_tm

74 setNextName

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

76 erun fc $ psolve lhs_tm

77 erun fc $ psolve lhs_tm

77 tt <- get_term

78 tt <- get_term

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

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

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

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

80 setContext ctxt'

81 setContext ctxt'

81 processTacticDecls info newDecls

82 processTacticDecls info newDecls

83+ sendHighlighting highlights

82

84

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

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

84 let crhs_tm = renamepats pnames crhs_tm_in

86 let crhs_tm = renamepats pnames crhs_tm_in

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

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

16import Idris.Inliner

17import Idris.PartialEval

18import Idris.DeepSeq

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

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

20import IRTS.Lang

21

22import Idris.Elab.Utils

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

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

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

68

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

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

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

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

72 setContext ctxt'

73 processTacticDecls info newDecls

74+ sendHighlighting highlights

74

75

75 let tyT = patToImp tyT'

76 let tyT = patToImp tyT'

76

77

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

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

15import Idris.Inliner

16import Idris.PartialEval

17import Idris.DeepSeq

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

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

19import IRTS.Lang

20

21import Idris.Elab.Utils

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

63 -- * elaboration as a Type

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

65

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

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

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

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

69

70 -- Extend the context with new definitions created

71 setContext ctxt'

72 processTacticDecls info newDecls

73+ sendHighlighting highlights

73

74

74 let vtm = orderPats (getInferTerm tm')

75 let vtm = orderPats (getInferTerm tm')

75

76

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

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

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

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

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

120elabExec :: FC -> PTerm -> PTerm

121elabExec :: FC -> PTerm -> PTerm

121−elabExec fc tm = runtm (PAlternative False

122+elabExec fc tm = runtm (PAlternative False

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

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

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

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

124 tm,

125 tm,

125 printtm tm

126 printtm tm

126 ])

127 ])

127− where

128+ where

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

129 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"))

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

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

131

132

src/Idris/Error.hs+3−3

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

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

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

116warnDisamb ist (PHidden tm) = warnDisamb ist tm

117−warnDisamb ist PType = return ()

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

118warnDisamb ist (PUniverse _) = return ()

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

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

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

121warnDisamb ist Placeholder = return ()

122warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

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

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

125 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

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

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

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

src/Idris/IBC.hs+10−6

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

41import Util.Zlib (decompressEither)

42

43ibcVersion :: Word16

44−ibcVersion = 107

44+ibcVersion = 108

45

46data IBCFile = IBCFile { ver :: Word16,

47 sourcefile :: FilePath,

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

1570 put x2

1571 PHidden x1 -> do putWord8 21

1572 put x1

1573− PType -> putWord8 22

1573+ PType x1 -> do putWord8 22

1574+ put x1

1574 PGoal x1 x2 x3 x4 -> do putWord8 23

1575 PGoal x1 x2 x3 x4 -> do putWord8 23

1575 put x1

1576 put x1

1576 put x2

1577 put x2

1577 put x3

1578 put x3

1578 put x4

1579 put x4

1579− PConstant x1 -> do putWord8 24

1580+ PConstant x1 x2 -> do putWord8 24

1580− put x1

1581+ put x1

1582+ put x2

1581 Placeholder -> putWord8 25

1583 Placeholder -> putWord8 25

1582 PDoBlock x1 -> do putWord8 26

1584 PDoBlock x1 -> do putWord8 26

1583 put x1

1585 put x1

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

1709 return (PAlternative x1 x2)

1711 return (PAlternative x1 x2)

1710 21 -> do x1 <- get

1712 21 -> do x1 <- get

1711 return (PHidden x1)

1713 return (PHidden x1)

1714+ 22 -> do x1 <- get

1712− 22 -> return PType

1715+ return (PType x1)

1713 23 -> do x1 <- get

1716 23 -> do x1 <- get

1714 x2 <- get

1717 x2 <- get

1715 x3 <- get

1718 x3 <- get

1716 x4 <- get

1719 x4 <- get

1717 return (PGoal x1 x2 x3 x4)

1720 return (PGoal x1 x2 x3 x4)

1718 24 -> do x1 <- get

1721 24 -> do x1 <- get

1722+ x2 <- get

1719− return (PConstant x1)

1723+ return (PConstant x1 x2)

1720 25 -> return Placeholder

1724 25 -> return Placeholder

1721 26 -> do x1 <- get

1725 26 -> do x1 <- get

1722 return (PDoBlock x1)

1726 return (PDoBlock x1)

src/Idris/IdeMode.hs+2

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

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

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

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

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

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

172

174

173escape :: String -> String

175escape :: String -> String

174escape = concatMap escapeChar

176escape = concatMap escapeChar

src/Idris/Output.hs+14

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

194 where ppTm = pprintDelab ist

195 norm = normaliseAll (tt_ctxt ist) []

196

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+

197

211

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

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

199renderExternal fmt width doc

213renderExternal fmt width doc

src/Idris/ParseData.hs+3−2

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

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

138 onlyName syn =

139 do n <- fnName

140+ fc <- getFC

140− return (expandNS syn n, PType)

141+ return (expandNS syn n, PType fc)

141

142

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

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

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

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

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

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

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

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

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

203 args <- many name

204 args <- many name

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

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

205 let tyn = expandNS syn tyn_in

206 let tyn = expandNS syn tyn_in

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

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

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

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

src/Idris/ParseExpr.hs+26−25

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

335 <|> tacticsExpr syn

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

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

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

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

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

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

341− <|> do c <- constant

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

342 fc <- getFC

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

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

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

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

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

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

347 <|> do fc <- getFC

348 x <- fnName

349− if inPattern syn

349+ if inPattern syn

350 then option (PRef fc x)

351 (do reservedOp "@"

352 s <- simpleExpr syn

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

445-- name suggests, rather than Int

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

447modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

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

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

449 | not (inPattern syn)

450 = 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)))]

452 : consts)

453 | otherwise = PAlternative False consts

454 where

455− consts = [ PConstant (BI x)

455+ consts = [ PConstant inFC (BI x)

456− , PConstant (I (fromInteger x))

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

457− , PConstant (B8 (fromInteger x))

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

458− , PConstant (B16 (fromInteger x))

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

459− , PConstant (B32 (fromInteger x))

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

460− , PConstant (B64 (fromInteger x))

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

461 ]

462modifyConst syn fc x = x

463

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

1219-}

1220

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

1222−constants =

1222+constants =

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

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

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

1226 , ("Double", AType ATFloat)

1227 , ("String", StrType)

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

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

1230 , ("prim__WorldType", WorldType)

1228 , ("prim__WorldType", WorldType)

1231 , ("prim__TheWorld", TheWorld)

1229 , ("prim__TheWorld", TheWorld)

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

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

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

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

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

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

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

1236 ]

1234 ]

1237−

1235+

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

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

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

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

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

1239+ | (name, ty) <- constants

1240+ ]

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

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

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

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

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

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

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

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

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

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

1245 <?> "constant or literal"

1246 <?> "constant or literal"

1246

1247

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

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

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

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

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

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

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

1391 do whiteSpace

1392 do whiteSpace

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

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

1393 eof

1394 eof

1394 return (TDocStr doc))

1395 return (TDocStr doc))

1395 ]

1396 ]

src/Idris/ParseHelpers.hs+17

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

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

251reserved = Tok.reserve idrisStyle

252

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+

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

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

254-- | Parses a reserved operator

261-- | Parses a reserved operator

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

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

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

360 -- Issue #1594 on the Issue Tracker.

367 -- Issue #1594 on the Issue Tracker.

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

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

362

369

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+

363{-* Syntax helpers-}

380{-* Syntax helpers-}

364-- | Bind constraints to term

381-- | Bind constraints to term

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

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

src/Idris/Parser.hs+4−3

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

674 carg :: IdrisParser (Name, PTerm)

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

676 return (i, ty)

677− <|> do i <- name;

677+ <|> do i <- name

678+ fc <- getFC

678− return (i, PType)

679+ return (i, PType fc)

679

680

680{- | Parses a type class instance declaration

681{- | Parses a type class instance declaration

681

682

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

1187

1188

1188{- | Parses a constant form input -}

1189{- | Parses a constant form input -}

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

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

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

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

1191

1192

1192{- | Parses a tactic from input -}

1193{- | Parses a tactic from input -}

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

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

src/Idris/Prover.hs+1−1

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

297 infixes = idris_infixes ist

298 action = case tm of

299 TType _ ->

300− iPrintTermWithType (prettyImp ppo PType) type1Doc

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

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

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

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

src/Idris/REPL.hs+1−1

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

932 ty' = normaliseC ctxt [] ty

933 case tm of

934 TType _ ->

935− iPrintTermWithType (prettyIst ist PType) type1Doc

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

936 _ -> iPrintTermWithType (pprintDelab ist tm)

937 (pprintDelab ist ty)

938

src/Idris/REPLParser.hs+1−1

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

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

266cmd_doc name = do

267 let constant = do

268− c <- P.constant

268+ c <- fmap fst P.constant

269 eof

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

271