d215440 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2257 from david-christiansen/name-highlights

Tracking and highlighting of metavariables

commitd2154408797018e55cd0350f04a44db5b9e71c5d authorDavid Christiansen <david@davidchristiansen.dk> dateWed 13 May 2015, 07:40 (11 years ago) parent6ecd591 64ab360

10 files changed+21−17

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+4−4 src/Idris/DeepSeq.hs+1−1 src/Idris/Delaborate.hs+2−2 src/Idris/Elab/Term.hs+3−2 src/Idris/Error.hs+1−1 src/Idris/IBC.hs+5−3 src/Idris/IdrisDoc.hs+1−1 src/Idris/ParseExpr.hs+2−1 src/Idris/Parser.hs+1−1

src/Idris/AbsSyntax.hs+1−1

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

19301930 (x: _) -> return x

19311931 _ -> LeftErr (a, b)

19321932 match (PCase _ _ _) _ = return [] -- lifted out

1933− match (PMetavar _) _ = return [] -- modified

1933+ match (PMetavar _ _) _ = return [] -- modified

19341934 match (PInferRef _ _) _ = return [] -- modified

19351935 match (PQuote _) _ = return []

19361936 match (PProof _) _ = return []

src/Idris/AbsSyntaxTree.hs+4−4

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

844844 | PDoBlock [PDo] -- ^ Do notation

845845 | PIdiom FC PTerm -- ^ Idiom brackets

846846 | PReturn FC

847− | PMetavar Name -- ^ A metavariable, ?name

847+ | PMetavar FC Name -- ^ A metavariable, ?name, and its precise location

848848 | PProof [PTactic] -- ^ Proof script

849849 | PTactics [PTactic] -- ^ As PProof, but no auto solving

850850 | PElabError Err -- ^ Error to report on elaboration

@@ -1063,7 +1063,7 @@ highestFC (PDoBlock lines) =

10631063

10641064highestFC (PIdiom fc _) = Just fc

10651065highestFC (PReturn fc) = Just fc

1066−highestFC (PMetavar _) = Nothing

1066+highestFC (PMetavar fc _) = Just fc

10671067highestFC (PProof _) = Nothing

10681068highestFC (PTactics _) = Nothing

10691069highestFC (PElabError _) = Nothing

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

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

16211621 prettySe p bnd (PTactics ts) =

16221622 text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1623− prettySe p bnd (PMetavar n) = text "?" <> pretty n

1623+ prettySe p bnd (PMetavar _ n) = annotate (AnnName n (Just MetavarOutput) Nothing Nothing) $ text "?" <> pretty n

16241624 prettySe p bnd (PReturn f) = kwd "return"

16251625 prettySe p bnd PImpossible = kwd "impossible"

16261626 prettySe p bnd Placeholder = text "_"

@@ -1893,7 +1893,7 @@ instance Sized PTerm where

18931893 size (PDoBlock dos) = 1 + size dos

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

18951895 size (PReturn fc) = 1

1896− size (PMetavar name) = 1

1896+ size (PMetavar _ name) = 1

18971897 size (PProof tactics) = size tactics

18981898 size (PElabError err) = size err

18991899 size PImpossible = 1

src/Idris/DeepSeq.hs+1−1

@@ -249,7 +249,7 @@ instance NFData PTerm where

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

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

251251 rnf (PReturn x1) = rnf x1 `seq` ()

252− rnf (PMetavar x1) = rnf x1 `seq` ()

252+ rnf (PMetavar x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

253253 rnf (PProof x1) = rnf x1 `seq` ()

254254 rnf (PTactics x1) = rnf x1 `seq` ()

255255 rnf (PElabError x1) = rnf x1 `seq` ()

src/Idris/Delaborate.hs+2−2

@@ -128,9 +128,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

128128 deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

129129

130130 mkMVApp n []

131− = PMetavar n

131+ = PMetavar NoFC n

132132 mkMVApp n args

133− = PApp un (PMetavar n) (map pexp args)

133+ = PApp un (PMetavar NoFC n) (map pexp args)

134134 mkPApp n args

135135 | Just imps <- lookupCtxtExact n (idris_implicits ist)

136136 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

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

@@ -879,10 +879,10 @@ elab ist info emode opts fn tm

879879 (appImpl es)

880880 (elab' ina fc Placeholder)

881881 (show f)

882− elab' ina fc Placeholder

882+ elab' ina fc Placeholder

883883 = do (h : hs) <- get_holes

884884 movelast h

885− elab' ina fc (PMetavar n) =

885+ elab' ina fc (PMetavar nfc n) =

886886 do ptm <- get_term

887887 -- When building the metavar application, leave out the unique

888888 -- names which have been used elsewhere in the term, since we

@@ -892,6 +892,7 @@ elab ist info emode opts fn tm

892892 attack

893893 defer unique_used n'

894894 solve

895+ highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

895896 where mkN n@(NS _ _) = n

896897 mkN n = case namespace info of

897898 Just xs@(_:_) -> sNS n xs

src/Idris/Error.hs+1−1

@@ -125,7 +125,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

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

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

127127warnDisamb ist (PReturn _) = return ()

128−warnDisamb ist (PMetavar _) = return ()

128+warnDisamb ist (PMetavar _ _) = return ()

129129warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs

130130warnDisamb ist (PTactics tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs

131131warnDisamb ist (PElabError _) = return ()

src/Idris/IBC.hs+5−3

@@ -1600,8 +1600,9 @@ instance Binary PTerm where

16001600 put x2

16011601 PReturn x1 -> do putWord8 28

16021602 put x1

1603− PMetavar x1 -> do putWord8 29

1604− put x1

1603+ PMetavar x1 x2 -> do putWord8 29

1604+ put x1

1605+ put x2

16051606 PProof x1 -> do putWord8 30

16061607 put x1

16071608 PTactics x1 -> do putWord8 31

@@ -1736,7 +1737,8 @@ instance Binary PTerm where

17361737 28 -> do x1 <- get

17371738 return (PReturn x1)

17381739 29 -> do x1 <- get

1739− return (PMetavar x1)

1740+ x2 <- get

1741+ return (PMetavar x1 x2)

17401742 30 -> do x1 <- get

17411743 return (PProof x1)

17421744 31 -> do x1 <- get

src/Idris/IdrisDoc.hs+1−1

@@ -313,7 +313,7 @@ extractPTermNames (PHidden p) = extract p

313313extractPTermNames (PGoal _ p1 n p2) = n : concatMap extract [p1, p2]

314314extractPTermNames (PDoBlock pdos) = concatMap extractPDo pdos

315315extractPTermNames (PIdiom _ p) = extract p

316−extractPTermNames (PMetavar n) = [n]

316+extractPTermNames (PMetavar _ n) = [n]

317317extractPTermNames (PProof tacts) = concatMap extractPTactic tacts

318318extractPTermNames (PTactics tacts) = concatMap extractPTactic tacts

319319extractPTermNames (PCoerced p) = extract p

src/Idris/ParseExpr.hs+2−1

@@ -324,7 +324,8 @@ SimpleExpr ::=

324324simpleExpr :: SyntaxInfo -> IdrisParser PTerm

325325simpleExpr syn =

326326 try (simpleExternalExpr syn)

327− <|> do x <- try (lchar '?' *> (fst <$> name)); return (PMetavar x)

327+ <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

328+ return (PMetavar (FC f (l, c-1) end) x)

328329 <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

329330 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc (SN $ ElimN t))

330331 <|> proofExpr syn

src/Idris/Parser.hs+1−1

@@ -879,7 +879,7 @@ rhs syn n = do lchar '='; expr syn

879879 addLet fc nm (PLet fc' n nfc ty val r) = PLet fc' n nfc ty val (addLet fc nm r)

880880 addLet fc nm (PCase fc' t cs) = PCase fc' t (map addLetC cs)

881881 where addLetC (l, r) = (l, addLet fc nm r)

882− addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar nm))

882+ addLet fc nm r = (PLet fc (sUN "value") NoFC Placeholder r (PMetavar NoFC nm))

883883

884884{- |Parses a function clause

885885