c48561f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Better approximation of syntax rule errors

External syntax is now properly used in error locations. Processing of highlighting and non-highlighting FCs has been separated.

commitc48561f5a5945902692d01b5fcdf8e6b4e6e2e6e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 18 Jun 2015, 22:51 (11 years ago) parente9e7993

5 files changed+64−59

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+53−51 src/Idris/ParseExpr.hs+8−3 test/syntax001/Syntax.idr+1−1 test/syntax001/SyntaxOk.idr−2 test/syntax001/expected+2−2

src/Idris/AbsSyntaxTree.hs+53−51

@@ -876,57 +876,59 @@ data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

876876 | FirstSuccess

877877 deriving (Eq, Data, Typeable)

878878

879−

880−mapPTermFC :: (FC -> FC) -> PTerm -> PTerm

881−mapPTermFC f (PQuote q) = PQuote q

882−mapPTermFC f (PRef fc n) = PRef (f fc) n

883−mapPTermFC f (PInferRef fc n) = PInferRef (f fc) n

884−mapPTermFC f (PPatvar fc n) = PPatvar (f fc) n

885−mapPTermFC f (PLam fc n fc' t1 t2) = PLam (f fc) n (f fc') (mapPTermFC f t1) (mapPTermFC f t2)

886−mapPTermFC f (PPi plic n fc t1 t2) = PPi plic n (f fc) (mapPTermFC f t1) (mapPTermFC f t2)

887−mapPTermFC f (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (f fc') (mapPTermFC f t1) (mapPTermFC f t2) (mapPTermFC f t3)

888−mapPTermFC f (PTyped t1 t2) = PTyped (mapPTermFC f t1) (mapPTermFC f t2)

889−mapPTermFC f (PApp fc t args) = PApp (f fc) (mapPTermFC f t) (map (fmap (mapPTermFC f)) args)

890−mapPTermFC f (PAppImpl t1 impls) = PAppImpl (mapPTermFC f t1) impls

891−mapPTermFC f (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f t) (map (fmap (mapPTermFC f)) args)

892−mapPTermFC f (PMatchApp fc n) = PMatchApp (f fc) n

893−mapPTermFC f (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f t1) (mapPTermFC f t2) (mapPTermFC f t3)

894−mapPTermFC f (PCase fc t cases) = PCase (f fc) (mapPTermFC f t) (map (\(l,r) -> (mapPTermFC f l, mapPTermFC f r)) cases)

895−mapPTermFC f (PTrue fc info) = PTrue (f fc) info

896−mapPTermFC f (PResolveTC fc) = PResolveTC (f fc)

897−mapPTermFC f (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f t1) (mapPTermFC f t2) (fmap (mapPTermFC f) t3)

898−mapPTermFC f (PPair fc info t1 t2) = PPair (f fc) info (mapPTermFC f t1) (mapPTermFC f t2)

899−mapPTermFC f (PDPair fc info t1 t2 t3) = PDPair (f fc) info (mapPTermFC f t1) (mapPTermFC f t2) (mapPTermFC f t3)

900−mapPTermFC f (PAs fc n t) = PAs (f fc) n (mapPTermFC f t)

901−mapPTermFC f (PAlternative ty ts) = PAlternative ty (map (mapPTermFC f) ts)

902−mapPTermFC f (PHidden t) = PHidden (mapPTermFC f t)

903−mapPTermFC f (PType fc) = PType (f fc)

904−mapPTermFC f (PUniverse u) = PUniverse u

905−mapPTermFC f (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f t1) n (mapPTermFC f t2)

906−mapPTermFC f (PConstant fc c) = PConstant (f fc) c

907−mapPTermFC f Placeholder = Placeholder

908−mapPTermFC f (PDoBlock dos) = PDoBlock (map (mapPDoFC f) dos)

909− where mapPDoFC f (DoExp fc t) = DoExp (f fc) (mapPTermFC f t)

910− mapPDoFC f (DoBind fc n nfc t) = DoBind (f fc) n (f nfc) (mapPTermFC f t)

911− mapPDoFC f (DoBindP fc t1 t2 alts) =

912− DoBindP (f fc) (mapPTermFC f t1) (mapPTermFC f t2) (map (\(l,r)-> (mapPTermFC f l, mapPTermFC f r)) alts)

913− mapPDoFC f (DoLet fc n nfc t1 t2) = DoLet (f fc) n (f nfc) (mapPTermFC f t1) (mapPTermFC f t2)

914− mapPDoFC f (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f t1) (mapPTermFC f t2)

915−mapPTermFC f (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f t)

916−mapPTermFC f (PReturn fc) = PReturn (f fc)

917−mapPTermFC f (PMetavar fc n) = PMetavar (f fc) n

918−mapPTermFC f (PProof tacs) = PProof (map (fmap (mapPTermFC f)) tacs)

919−mapPTermFC f (PTactics tacs) = PTactics (map (fmap (mapPTermFC f)) tacs)

920−mapPTermFC f (PElabError err) = PElabError err

921−mapPTermFC f PImpossible = PImpossible

922−mapPTermFC f (PCoerced t) = PCoerced (mapPTermFC f t)

923−mapPTermFC f (PDisamb msg t) = PDisamb msg (mapPTermFC f t)

924−mapPTermFC f (PUnifyLog t) = PUnifyLog (mapPTermFC f t)

925−mapPTermFC f (PNoImplicits t) = PNoImplicits (mapPTermFC f t)

926−mapPTermFC f (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f t1) (fmap (mapPTermFC f) t2)

927−mapPTermFC f (PUnquote t) = PUnquote (mapPTermFC f t)

928−mapPTermFC f (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f tm) ns

929−mapPTermFC f (PQuoteName n) = PQuoteName n

879+-- | Transform the FCs in a PTerm. The first function transforms the

880+-- general-purpose FCs, and the second transforms those that are used

881+-- for semantic source highlighting, so they can be treated specially.

882+mapPTermFC :: (FC -> FC) -> (FC -> FC) -> PTerm -> PTerm

883+mapPTermFC f g (PQuote q) = PQuote q

884+mapPTermFC f g (PRef fc n) = PRef (g fc) n

885+mapPTermFC f g (PInferRef fc n) = PInferRef (g fc) n

886+mapPTermFC f g (PPatvar fc n) = PPatvar (g fc) n

887+mapPTermFC f g (PLam fc n fc' t1 t2) = PLam (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2)

888+mapPTermFC f g (PPi plic n fc t1 t2) = PPi plic n (g fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

889+mapPTermFC f g (PLet fc n fc' t1 t2 t3) = PLet (f fc) n (g fc') (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

890+mapPTermFC f g (PTyped t1 t2) = PTyped (mapPTermFC f g t1) (mapPTermFC f g t2)

891+mapPTermFC f g (PApp fc t args) = PApp (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

892+mapPTermFC f g (PAppImpl t1 impls) = PAppImpl (mapPTermFC f g t1) impls

893+mapPTermFC f g (PAppBind fc t args) = PAppBind (f fc) (mapPTermFC f g t) (map (fmap (mapPTermFC f g)) args)

894+mapPTermFC f g (PMatchApp fc n) = PMatchApp (f fc) n

895+mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

896+mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)

897+mapPTermFC f g (PTrue fc info) = PTrue (f fc) info

898+mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)

899+mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)

900+mapPTermFC f g (PPair fc info t1 t2) = PPair (f fc) info (mapPTermFC f g t1) (mapPTermFC f g t2)

901+mapPTermFC f g (PDPair fc info t1 t2 t3) = PDPair (f fc) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

902+mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

903+mapPTermFC f g (PAlternative ty ts) = PAlternative ty (map (mapPTermFC f g) ts)

904+mapPTermFC f g (PHidden t) = PHidden (mapPTermFC f g t)

905+mapPTermFC f g (PType fc) = PType (f fc)

906+mapPTermFC f g (PUniverse u) = PUniverse u

907+mapPTermFC f g (PGoal fc t1 n t2) = PGoal (f fc) (mapPTermFC f g t1) n (mapPTermFC f g t2)

908+mapPTermFC f g (PConstant fc c) = PConstant (f fc) c

909+mapPTermFC f g Placeholder = Placeholder

910+mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

911+ where mapPDoFC (DoExp fc t) = DoExp (f fc) (mapPTermFC f g t)

912+ mapPDoFC (DoBind fc n nfc t) = DoBind (f fc) n (g nfc) (mapPTermFC f g t)

913+ mapPDoFC (DoBindP fc t1 t2 alts) =

914+ DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

915+ mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

916+ mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

917+mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

918+mapPTermFC f g (PReturn fc) = PReturn (f fc)

919+mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n

920+mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)

921+mapPTermFC f g (PTactics tacs) = PTactics (map (fmap (mapPTermFC f g)) tacs)

922+mapPTermFC f g (PElabError err) = PElabError err

923+mapPTermFC f g PImpossible = PImpossible

924+mapPTermFC f g (PCoerced t) = PCoerced (mapPTermFC f g t)

925+mapPTermFC f g (PDisamb msg t) = PDisamb msg (mapPTermFC f g t)

926+mapPTermFC f g (PUnifyLog t) = PUnifyLog (mapPTermFC f g t)

927+mapPTermFC f g (PNoImplicits t) = PNoImplicits (mapPTermFC f g t)

928+mapPTermFC f g (PQuasiquote t1 t2) = PQuasiquote (mapPTermFC f g t1) (fmap (mapPTermFC f g) t2)

929+mapPTermFC f g (PUnquote t) = PUnquote (mapPTermFC f g t)

930+mapPTermFC f g (PRunElab fc tm ns) = PRunElab (f fc) (mapPTermFC f g tm) ns

931+mapPTermFC f g (PQuoteName n) = PQuoteName n

930932

931933{-!

932934dg instance Binary PTerm

src/Idris/ParseExpr.hs+8−3

@@ -94,10 +94,15 @@ externalExpr syn = do i <- get

9494 (FC fn start _) <- getFC

9595 expr <- extensions syn (syntaxRulesList $ syntax_rules i)

9696 (FC _ _ end) <- getFC

97− return (mapPTermFC (fixFC fn (FC fn start end)) expr)

97+ let outerFC = FC fn start end

98+ return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)

9899 <?> "user-defined expression"

99− where fixFC fn outer inner | inner `fcIn` outer = inner

100− | otherwise = FileFC fn

100+ where -- Fix non-highlighting FCs by approximating with the span of the syntax application

101+ fixFC outer inner | inner `fcIn` outer = inner

102+ | otherwise = outer

103+ -- Fix highlighting FCs by making them useless, to avoid spurious highlights

104+ fixFCH fn outer inner | inner `fcIn` outer = inner

105+ | otherwise = FileFC fn

101106

102107{- | Parses a simple user-defined expression -}

103108simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

test/syntax001/Syntax.idr+1−1

@@ -1,4 +1,4 @@

1− module Syntax

1+module Syntax

33syntax "fnord" [y] = y + y + y

test/syntax001/SyntaxOk.idr−2

@@ -2,7 +2,5 @@ module SyntaxOk

33syntax "fnord" [y] = y + y + y

5−foo : Nat

6−foo = fnord "argh"

test/syntax001/expected+2−2

@@ -1,10 +1,10 @@

1−When checking right hand side of foo:

1+Syntax.idr:6:7-9:1:When checking right hand side of foo:

22When checking an application of function Prelude.Classes.+:

33 Type mismatch between

44 String (Type of "argh")

55 and

66 Nat (Expected type)

7−When checking right hand side of foo:

7+SyntaxTest.idr:5:7-6:1:When checking right hand side of foo:

88When checking an application of function Prelude.Classes.+:

99 Type mismatch between

1010 String (Type of "argh")