00cffbd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2449 from david-christiansen/parser-highlights

Semantic highlighting of implicit fromInteger

commit00cffbd7fccdb608d217e0c02b54fa540a47286f authorDavid Christiansen <david@davidchristiansen.dk> dateSun 19 Jul 2015, 21:15 (11 years ago) parent062b069 c9c3bfa

10 files changed+64−4

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+5 src/Idris/AbsSyntaxTree.hs+4 src/Idris/DSL.hs+2 src/Idris/DeepSeq.hs+1 src/Idris/Elab/Term.hs+36 src/Idris/ElabQuasiquote.hs+2 src/Idris/Error.hs+1 src/Idris/IBC.hs+6 src/Idris/IdrisDoc.hs+1 src/Idris/ParseExpr.hs+6−4

src/Idris/AbsSyntax.hs+5

@@ -1043,6 +1043,7 @@ expandParams dec ps ns infs tm = en tm

10431043 en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

10441044 en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

10451045 en (PRunElab fc tm ns) = PRunElab fc (en tm) ns

1046+ en (PConstSugar fc tm) = PConstSugar fc (en tm)

10461047 en t = t

10471048

10481049 nselem x [] = False

@@ -1510,6 +1511,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

15101511 imps top env (PUnifyLog tm) = imps False env tm

15111512 imps top env (PNoImplicits tm) = imps False env tm

15121513 imps top env (PRunElab fc tm ns) = imps False env tm

1514+ imps top env (PConstSugar fc tm) = imps top env tm -- ignore PConstSugar - it's for highlighting only!

15131515 imps top env _ = return ()

15141516

15151517 pibind using [] sc = sc

@@ -1637,6 +1639,7 @@ addImpl' inpat env infns imp_meths ist ptm

16371639 (fmap (ai True env ds) g)

16381640 ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

16391641 ai qq env ds (PRunElab fc tm ns) = PRunElab fc (ai False env ds tm) ns

1642+ ai qq env ds (PConstSugar fc tm) = PConstSugar fc (ai qq env ds tm)

16401643 ai qq env ds tm = tm

16411644

16421645 handleErr (Left err) = PElabError err

@@ -2065,6 +2068,7 @@ substMatchShadow n shs tm t = sm shs t where

20652068 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

20662069 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

20672070 sm xs (PRunElab fc script ns) = PRunElab fc (sm xs script) ns

2071+ sm xs (PConstSugar fc tm) = PConstSugar fc (sm xs tm)

20682072 sm xs x = x

20692073

20702074 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

@@ -2203,6 +2207,7 @@ mkUniqueNames env shadows tm

22032207 mkUniq nmap (PProof ts) = liftM PProof (mapM (mkUniqT nmap) ts)

22042208 mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

22052209 mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2210+ mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)

22062211 mkUniq nmap t = return (shadowAll (M.toList nmap) t)

22072212 where

22082213 shadowAll [] t = t

src/Idris/AbsSyntaxTree.hs+4

@@ -873,6 +873,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

873873 | PUnquote PTerm -- ^ ~Term

874874 | PQuoteName Name FC -- ^ `{n} where the FC is the precise highlighting for the name in particular

875875 | PRunElab FC PTerm [String] -- ^ %runElab tm - New-style proof script. Args are location, script, enclosing namespace.

876+ | PConstSugar FC PTerm -- ^ A desugared constant. The FC is a precise source location that will be used to highlight it later.

876877 deriving (Eq, Data, Typeable)

877878

878879data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

@@ -932,6 +933,7 @@ mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)

932933mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)

933934mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)

934935mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns

936+mapPTermFC f g (PConstSugar fc tm) = PConstSugar (g fc) (mapPTermFC f g tm)

935937mapPTermFC f g (PQuoteName n fc) = PQuoteName n (g fc)

936938

937939{-!

@@ -1159,6 +1161,7 @@ highestFC (PQuasiquote _ _) = Nothing

11591161highestFC (PUnquote tm) = highestFC tm

11601162highestFC (PQuoteName _ fc) = Just fc

11611163highestFC (PRunElab fc _ _) = Just fc

1164+highestFC (PConstSugar fc _) = Just fc

11621165highestFC (PAppImpl t _) = highestFC t

11631166

11641167-- Type class data

@@ -1750,6 +1753,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

17501753 bracket p funcAppPrec . group . align . hang 2 $

17511754 text "%runElab" <$>

17521755 prettySe (decD d) funcAppPrec bnd tm

1756+ prettySe d p bnd (PConstSugar fc tm) = prettySe d p bnd tm -- should never occur, but harmless

17531757

17541758 prettySe d p bnd _ = text "missing pretty-printer for term"

17551759

src/Idris/DSL.hs+2

@@ -113,6 +113,7 @@ expandSugar dsl (PDoBlock ds)

113113

114114expandSugar dsl (PIdiom fc e) = expandSugar dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

115115expandSugar dsl (PRunElab fc tm ns) = PRunElab fc (expandSugar dsl tm) ns

116+expandSugar dsl (PConstSugar fc tm) = PConstSugar fc (expandSugar dsl tm)

116117expandSugar dsl t = t

117118

118119-- | Replace DSL-bound variable in a term

@@ -199,6 +200,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

199200 r' <- db' r

200201 return (PDPair fc hls p l' t r')

201202 db' (PRunElab fc t ns) = fmap (\tm -> PRunElab fc tm ns) (db' t)

203+ db' (PConstSugar fc tm) = liftM (PConstSugar fc) (db' tm)

202204 db' t = return t

203205

204206 dbArg a = do t' <- db' (getTm a)

src/Idris/DeepSeq.hs+1

@@ -270,6 +270,7 @@ instance NFData PTerm where

270270 rnf (PUnquote x1) = rnf x1 `seq` ()

271271 rnf (PQuoteName x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

272272 rnf (PRunElab x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

273+ rnf (PConstSugar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

273274

274275instance NFData PAltType where

275276 rnf (ExactlyOne x1) = rnf x1 `seq` ()

src/Idris/Elab/Term.hs+36

@@ -1228,6 +1228,42 @@ elab ist info emode opts fn tm

12281228 env <- get_env

12291229 runElabAction ist (maybe fc' id fc) env (P Bound n' Erased) ns

12301230 solve

1231+ elab' ina fc (PConstSugar constFC tm) =

1232+ -- Here we elaborate the contained term, then calculate

1233+ -- highlighting for constFC. The highlighting is the

1234+ -- highlighting for the outermost constructor of the result of

1235+ -- evaluating the elaborated term, if one exists (it always

1236+ -- should, but better to fail gracefully for something silly

1237+ -- like highlighting info). This is how implicit applications of

1238+ -- fromInteger get highlighted.

1239+ do saveState -- so we don't pollute the elaborated term

1240+ n <- getNameFrom (sMN 0 "cstI")

1241+ n' <- getNameFrom (sMN 0 "cstIhole")

1242+ g <- forget <$> goal

1243+ claim n' g

1244+ movelast n'

1245+ -- In order to intercept the elaborated value, we need to

1246+ -- let-bind it.

1247+ attack

1248+ letbind n g (Var n')

1249+ focus n'

1250+ elab' ina fc tm

1251+ env <- get_env

1252+ ctxt <- get_context

1253+ let v = fmap (normaliseAll ctxt env . finalise . binderVal)

1254+ (lookup n env)

1255+ loadState -- we have the highlighting - re-elaborate the value

1256+ elab' ina fc tm

1257+ case v of

1258+ Just val -> highlightConst constFC val

1259+ Nothing -> return ()

1260+ where highlightConst fc (P _ n _) =

1261+ highlightSource fc (AnnName n Nothing Nothing Nothing)

1262+ highlightConst fc (App _ f _) =

1263+ highlightConst fc f

1264+ highlightConst fc (Constant c) =

1265+ highlightSource fc (AnnConst c)

1266+ highlightConst _ _ = return ()

12311267 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

12321268

12331269 -- delay elaboration of 't', with priority 'pri' until after everything

src/Idris/ElabQuasiquote.hs+2

@@ -168,6 +168,8 @@ extractUnquotes n (PUnquote tm)

168168 extractUnquotes (n-1) tm

169169extractUnquotes n (PRunElab fc tm ns)

170170 = fmap (\(tm', ex) -> (PRunElab fc tm' ns, ex)) $ extractUnquotes n tm

171+extractUnquotes n (PConstSugar fc tm)

172+ = extractUnquotes n tm

171173extractUnquotes n x = return (x, []) -- no subterms!

172174

173175

src/Idris/Error.hs+1

@@ -151,3 +151,4 @@ warnDisamb ist (PQuoteName _ _) = return ()

151151warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

152152warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

153153warnDisamb ist (PRunElab _ tm _) = warnDisamb ist tm

154+warnDisamb ist (PConstSugar _ tm) = warnDisamb ist tm

src/Idris/IBC.hs+6

@@ -1660,6 +1660,9 @@ instance Binary PTerm where

16601660 put x2

16611661 put x3

16621662 put x4

1663+ PConstSugar x1 x2 -> do putWord8 46

1664+ put x1

1665+ put x2

16631666

16641667 get

16651668 = do i <- getWord8

@@ -1803,6 +1806,9 @@ instance Binary PTerm where

18031806 x3 <- get

18041807 x4 <- get

18051808 return (PIfThenElse x1 x2 x3 x4)

1809+ 46 -> do x1 <- get

1810+ x2 <- get

1811+ return (PConstSugar x1 x2)

18061812 _ -> error "Corrupted binary data for PTerm"

18071813

18081814instance Binary PAltType where

src/Idris/IdrisDoc.hs+1

@@ -321,6 +321,7 @@ extractPTermNames (PDisamb _ p) = extract p

321321extractPTermNames (PUnifyLog p) = extract p

322322extractPTermNames (PNoImplicits p) = extract p

323323extractPTermNames (PRunElab _ p _) = extract p

324+extractPTermNames (PConstSugar _ tm) = extract tm

324325extractPTermNames _ = []

325326

326327-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+6−4

@@ -464,10 +464,12 @@ bracketedExpr syn openParenFC e =

464464modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

465465modifyConst syn fc (PConstant inFC (BI x))

466466 | not (inPattern syn)

467− = PAlternative [] FirstSuccess

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

469− : consts)

470− | otherwise = PAlternative [] FirstSuccess consts

467+ = PConstSugar inFC $ -- wrap in original location for highlighting

468+ PAlternative [] FirstSuccess

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

470+ : consts)

471+ | otherwise = PConstSugar inFC $

472+ PAlternative [] FirstSuccess consts

471473 where

472474 consts = [ PConstant inFC (BI x)

473475 , PConstant inFC (I (fromInteger x))