e9e7993 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Replace absurd syntax rule FCs

Previously, FCs coming from syntax rules would keep the FCs of their definition context. Now, after expanding a syntax rule, the FCs that aren't contained in the region in which the syntax was expanded are replaced by a reference to the present file. This does not give a precise source location - that runs the risk of generating false highlighting information - but this solution at least places the error in the right file, and the "While elaborating ..." bit can be used to find the error. We should probably get better at separating the highlighting-relevant FCs from the highlighting-irrelevant FCs in the future.

commite9e7993e4791564d427ce83cabe8e39b656eb3af authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 18 Jun 2015, 22:27 (11 years ago) parent6d7da92

9 files changed+122−3

compare with master

unifiedsplit

idris.cabal+4 src/Idris/AbsSyntaxTree.hs+65−2 src/Idris/Core/TT.hs+10 src/Idris/ParseExpr.hs+6−1 test/syntax001/Syntax.idr+8 test/syntax001/SyntaxOk.idr+8 test/syntax001/SyntaxTest.idr+5 test/syntax001/expected+12 test/syntax001/run+4

idris.cabal+4

@@ -641,6 +641,10 @@ Extra-source-files:

641641 test/sugar005/*.idr

642642 test/sugar005/expected

643643

644+ test/syntax001/run

645+ test/syntax001/*.idr

646+ test/syntax001/expected

647+

644648 test/tactics001/run

645649 test/tactics001/*.idr

646650 test/tactics001/expected

src/Idris/AbsSyntaxTree.hs+65−2

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

873873 deriving (Eq, Data, Typeable)

874874

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

876− | FirstSuccess

876+ | 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

930+

879931{-!

880−deriving instance Binary PTerm

932+dg instance Binary PTerm

881933deriving instance NFData PTerm

882934!-}

883935

@@ -968,6 +1020,14 @@ instance Sized a => Sized (PTactic' a) where

9681020 size Skip = 1

9691021 size (TFail ts) = 1 + size ts

9701022 size SourceFC = 1

1023+ size DoUnify = 1

1024+ size (CaseTac x) = 1 + size x

1025+ size (Equiv t) = 1 + size t

1026+ size (Claim x y) = 1 + size x + size y

1027+ size Unfocus = 1

1028+ size (MatchRefine x) = 1 + size x

1029+ size (LetTacTy x y z) = 1 + size x + size y + size z

1030+ size TCInstance = 1

9711031

9721032type PTactic = PTactic' PTerm

9731033

@@ -1092,6 +1152,8 @@ highestFC (PNoImplicits tm) = highestFC tm

10921152highestFC (PQuasiquote _ _) = Nothing

10931153highestFC (PUnquote tm) = highestFC tm

10941154highestFC (PQuoteName _) = Nothing

1155+highestFC (PRunElab fc _ _) = Just fc

1156+highestFC (PAppImpl t _) = highestFC t

10951157

10961158-- Type class data

10971159

@@ -1429,6 +1491,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

14291491consoleDecorate ist (AnnTerm _ _) = id

14301492consoleDecorate ist (AnnSearchResult _) = id

14311493consoleDecorate ist (AnnErr _) = id

1494+consoleDecorate ist (AnnNamespace _ _) = id

14321495

14331496isPostulateName :: Name -> IState -> Bool

14341497isPostulateName n ist = S.member n (idris_postulates ist)

src/Idris/Core/TT.hs+10

@@ -107,6 +107,16 @@ spanFC (FileFC f) (FileFC f') | f == f' = FileFC f

107107spanFC NoFC fc = fc

108108spanFC fc NoFC = fc

109109

110+-- | Determine whether the first argument is completely contained in the second

111+fcIn :: FC -> FC -> Bool

112+fcIn NoFC _ = False

113+fcIn (FileFC _) _ = False

114+fcIn (FC {}) NoFC = False

115+fcIn (FC {}) (FileFC _) = False

116+fcIn (FC fn1 (sl1, sc1) (el1, ec1)) (FC fn2 (sl2, sc2) (el2, ec2)) =

117+ fn1 == fn2 &&

118+ (sl1 == sl2 && sc1 > sc2 || sl1 > sl2) &&

119+ (el1 == el2 && ec1 < ec2 || el1 < el2)

110120

111121-- | Ignore source location equality (so deriving classes do not compare FCs)

112122instance Eq FC where

src/Idris/ParseExpr.hs+6−1

@@ -91,8 +91,13 @@ expr' syn = try (externalExpr syn)

9191{- | Parses a user-defined expression -}

9292externalExpr :: SyntaxInfo -> IdrisParser PTerm

9393externalExpr syn = do i <- get

94− extensions syn (syntaxRulesList $ syntax_rules i)

94+ (FC fn start _) <- getFC

95+ expr <- extensions syn (syntaxRulesList $ syntax_rules i)

96+ (FC _ _ end) <- getFC

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

9598 <?> "user-defined expression"

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

100+ | otherwise = FileFC fn

96101

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

98103simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

test/syntax001/Syntax.idrnew file+8

@@ -0,0 +1,8 @@

1+ module Syntax

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

5+foo : Nat

6+foo = fnord "argh"

test/syntax001/SyntaxOk.idrnew file+8

@@ -0,0 +1,8 @@

1+module SyntaxOk

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

5+foo : Nat

6+foo = fnord "argh"

test/syntax001/SyntaxTest.idrnew file+5

@@ -0,0 +1,5 @@

1+module SyntaxTest

2+import SyntaxOk

4+foo : Nat

5+foo = fnord "argh"

test/syntax001/expectednew file+12

@@ -0,0 +1,12 @@

1+When checking right hand side of foo:

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

3+ Type mismatch between

4+ String (Type of "argh")

5+ and

6+ Nat (Expected type)

7+When checking right hand side of foo:

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

9+ Type mismatch between

10+ String (Type of "argh")

11+ and

12+ Nat (Expected type)

test/syntax001/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ Syntax.idr --nocolour --consolewidth 80 --check

3+idris $@ SyntaxTest.idr --nocolour --consolewidth 80 --check

4+rm -f *.ibc