c9c3bfa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Semantic highlighting of implicit fromInteger

Now, editors get highlighting information for integer literals according to the following rules: 1. If the constant elaborates to a constant (such as the fromInteger implementations for Integer, Int, Bits8, etc), then the constant itself is used for highlighting informating, as it would be in the pretty printer. 2. If the constant elaborates to an inductive datatype, the outermost constructor is used for highlighting (e.g., the Nat 4 highlights as S, and the Nat 0 highlights as Z) 3. Otherwise, no highlighting is performed.

commitc9c3bfa650c6cc7a4d72ec58e5781b3ab23071ed authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 19 Jul 2015, 19:50 (11 years ago) parentbc2915c

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

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

12261226 env <- get_env

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

12281228 solve

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

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

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

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

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

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

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

1236+ -- fromInteger get highlighted.

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

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

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

1240+ g <- forget <$> goal

1241+ claim n' g

1242+ movelast n'

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

1244+ -- let-bind it.

1245+ attack

1246+ letbind n g (Var n')

1247+ focus n'

1248+ elab' ina fc tm

1249+ env <- get_env

1250+ ctxt <- get_context

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

1252+ (lookup n env)

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

1254+ elab' ina fc tm

1255+ case v of

1256+ Just val -> highlightConst constFC val

1257+ Nothing -> return ()

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

1259+ highlightSource fc (AnnName n Nothing Nothing Nothing)

1260+ highlightConst fc (App _ f _) =

1261+ highlightConst fc f

1262+ highlightConst fc (Constant c) =

1263+ highlightSource fc (AnnConst c)

1264+ highlightConst _ _ = return ()

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

12301266

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