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

src/Idris/AbsSyntax.hs+5

compare with master

unifiedsplit

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

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

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

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

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

1046 en t = t

1047 en t = t

1047

1048

1048 nselem x [] = False

1049 nselem x [] = False

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

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

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

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

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

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

1513 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!

1513 imps top env _ = return ()

1515 imps top env _ = return ()

1514

1516

1515 pibind using [] sc = sc

1517 pibind using [] sc = sc

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

1637 (fmap (ai True env ds) g)

1639 (fmap (ai True env ds) g)

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

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

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

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

1640 ai qq env ds tm = tm

1643 ai qq env ds tm = tm

1641

1644

1642 handleErr (Left err) = PElabError err

1645 handleErr (Left err) = PElabError err

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

2065 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2068 sm xs (PUnifyLog x) = PUnifyLog (sm xs x)

2066 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

2069 sm xs (PNoImplicits x) = PNoImplicits (sm xs x)

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

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

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

2068 sm xs x = x

2072 sm xs x = x

2069

2073

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

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

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

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

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

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

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

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

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

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

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

2207 where

2212 where

2208 shadowAll [] t = t

2213 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

873 | PUnquote PTerm -- ^ ~Term

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

875 | 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.

876 deriving (Eq, Data, Typeable)

877 deriving (Eq, Data, Typeable)

877

878

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

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

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

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

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

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

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

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

935mapPTermFC 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)

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

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

936

938

937{-!

939{-!

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

1159highestFC (PUnquote tm) = highestFC tm

1161highestFC (PUnquote tm) = highestFC tm

1160highestFC (PQuoteName _ fc) = Just fc

1162highestFC (PQuoteName _ fc) = Just fc

1161highestFC (PRunElab fc _ _) = Just fc

1163highestFC (PRunElab fc _ _) = Just fc

1164+highestFC (PConstSugar fc _) = Just fc

1162highestFC (PAppImpl t _) = highestFC t

1165highestFC (PAppImpl t _) = highestFC t

1163

1166

1164-- Type class data

1167-- Type class data

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

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

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

1751 text "%runElab" <$>

1754 text "%runElab" <$>

1752 prettySe (decD d) funcAppPrec bnd tm

1755 prettySe (decD d) funcAppPrec bnd tm

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

1753

1757

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

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

1755

1759

src/Idris/DSL.hs+2

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

113

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

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

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

116expandSugar dsl t = t

117expandSugar dsl t = t

117

118

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

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

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

199 r' <- db' r

200 r' <- db' r

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

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

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

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

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

202 db' t = return t

204 db' t = return t

203

205

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

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

src/Idris/DeepSeq.hs+1

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

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

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

272 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` ()

273

274

274instance NFData PAltType where

275instance NFData PAltType where

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

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

src/Idris/Elab/Term.hs+36

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

1228 env <- get_env

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

1230 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 ()

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

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

1232

1268

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

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

src/Idris/ElabQuasiquote.hs+2

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

168 extractUnquotes (n-1) tm

169extractUnquotes n (PRunElab fc tm ns)

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

171+extractUnquotes n (PConstSugar fc tm)

172+ = extractUnquotes n tm

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

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

172

174

173

175

src/Idris/Error.hs+1

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

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

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

153warnDisamb 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

1660 put x2

1661 put x3

1662 put x4

1663+ PConstSugar x1 x2 -> do putWord8 46

1664+ put x1

1665+ put x2

1663

1666

1664 get

1667 get

1665 = do i <- getWord8

1668 = do i <- getWord8

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

1803 x3 <- get

1806 x3 <- get

1804 x4 <- get

1807 x4 <- get

1805 return (PIfThenElse x1 x2 x3 x4)

1808 return (PIfThenElse x1 x2 x3 x4)

1809+ 46 -> do x1 <- get

1810+ x2 <- get

1811+ return (PConstSugar x1 x2)

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

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

1807

1813

1808instance Binary PAltType where

1814instance Binary PAltType where

src/Idris/IdrisDoc.hs+1

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

321extractPTermNames (PUnifyLog p) = extract p

322extractPTermNames (PNoImplicits p) = extract p

323extractPTermNames (PRunElab _ p _) = extract p

324+extractPTermNames (PConstSugar _ tm) = extract tm

324extractPTermNames _ = []

325extractPTermNames _ = []

325

326

326-- | Shorter name for extractPTermNames

327-- | Shorter name for extractPTermNames

src/Idris/ParseExpr.hs+6−4

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

464modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

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

466 | not (inPattern syn)

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

467− = PAlternative [] FirstSuccess

468+ PAlternative [] FirstSuccess

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

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

469− : consts)

470+ : consts)

471+ | otherwise = PConstSugar inFC $

470− | otherwise = PAlternative [] FirstSuccess consts

472+ PAlternative [] FirstSuccess consts

471 where

473 where

472 consts = [ PConstant inFC (BI x)

474 consts = [ PConstant inFC (BI x)

473 , PConstant inFC (I (fromInteger x))

475 , PConstant inFC (I (fromInteger x))