d215440 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

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

1930 (x: _) -> return x

1931 _ -> LeftErr (a, b)

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

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

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

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

1935 match (PQuote _) _ = return []

1936 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

844 | PDoBlock [PDo] -- ^ Do notation

845 | PIdiom FC PTerm -- ^ Idiom brackets

846 | PReturn FC

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

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

848 | PProof [PTactic] -- ^ Proof script

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

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

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

1063

1064highestFC (PIdiom fc _) = Just fc

1065highestFC (PReturn fc) = Just fc

1066−highestFC (PMetavar _) = Nothing

1066+highestFC (PMetavar fc _) = Just fc

1067highestFC (PProof _) = Nothing

1068highestFC (PTactics _) = Nothing

1069highestFC (PElabError _) = Nothing

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

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

1621 prettySe p bnd (PTactics ts) =

1622 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

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

1625 prettySe p bnd PImpossible = kwd "impossible"

1626 prettySe p bnd Placeholder = text "_"

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

1893 size (PDoBlock dos) = 1 + size dos

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

1895 size (PReturn fc) = 1

1896− size (PMetavar name) = 1

1896+ size (PMetavar _ name) = 1

1897 size (PProof tactics) = size tactics

1898 size (PElabError err) = size err

1899 size PImpossible = 1

src/Idris/DeepSeq.hs+1−1

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

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

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

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

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

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

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

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

255 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

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

129

130 mkMVApp n []

131− = PMetavar n

131+ = PMetavar NoFC n

132 mkMVApp n args

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

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

134 mkPApp n args

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

136 = 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

879 (appImpl es)

880 (elab' ina fc Placeholder)

881 (show f)

882− elab' ina fc Placeholder

882+ elab' ina fc Placeholder

883 = do (h : hs) <- get_holes

884 movelast h

885− elab' ina fc (PMetavar n) =

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

886 do ptm <- get_term

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

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

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

892 attack

893 defer unique_used n'

894 solve

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

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

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

896 mkN n = case namespace info of

897 mkN n = case namespace info of

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

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

src/Idris/Error.hs+1−1

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

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

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

127warnDisamb ist (PReturn _) = return ()

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

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

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

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

131warnDisamb ist (PElabError _) = return ()

src/Idris/IBC.hs+5−3

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

1600 put x2

1601 PReturn x1 -> do putWord8 28

1602 put x1

1603− PMetavar x1 -> do putWord8 29

1603+ PMetavar x1 x2 -> do putWord8 29

1604− put x1

1604+ put x1

1605+ put x2

1605 PProof x1 -> do putWord8 30

1606 PProof x1 -> do putWord8 30

1606 put x1

1607 put x1

1607 PTactics x1 -> do putWord8 31

1608 PTactics x1 -> do putWord8 31

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

1736 28 -> do x1 <- get

1737 28 -> do x1 <- get

1737 return (PReturn x1)

1738 return (PReturn x1)

1738 29 -> do x1 <- get

1739 29 -> do x1 <- get

1740+ x2 <- get

1739− return (PMetavar x1)

1741+ return (PMetavar x1 x2)

1740 30 -> do x1 <- get

1742 30 -> do x1 <- get

1741 return (PProof x1)

1743 return (PProof x1)

1742 31 -> do x1 <- get

1744 31 -> do x1 <- get

src/Idris/IdrisDoc.hs+1−1

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

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

314extractPTermNames (PDoBlock pdos) = concatMap extractPDo pdos

315extractPTermNames (PIdiom _ p) = extract p

316−extractPTermNames (PMetavar n) = [n]

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

317extractPTermNames (PProof tacts) = concatMap extractPTactic tacts

318extractPTermNames (PTactics tacts) = concatMap extractPTactic tacts

319extractPTermNames (PCoerced p) = extract p

src/Idris/ParseExpr.hs+2−1

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

324simpleExpr :: SyntaxInfo -> IdrisParser PTerm

325simpleExpr syn =

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

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

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

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

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

330 <|> proofExpr syn

331 <|> proofExpr syn

src/Idris/Parser.hs+1−1

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

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

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

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

883

884{- |Parses a function clause

885