git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2384 from david-christiansen/syntax-fc

Replace absurd syntax rule FCs

commit5457da9934bf4bf561e7786ab0da812026bd6ec0 authorDavid Christiansen <david@davidchristiansen.dk> dateFri 19 Jun 2015, 00:58 (11 years ago) parent9107357e1fce3f
10 files changed+128−4
compare with master
unifiedsplit
idris.cabal+4 src/Idris/AbsSyntaxTree.hs+67−2 src/Idris/Core/TT.hs+10 src/Idris/ParseExpr.hs+11−1 test/proof002/expected+1−1 test/syntax001/Syntax.idr+8 test/syntax001/SyntaxOk.idr+6 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+67−2
@@ -873,11 +873,65 @@ 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+-- | 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
932+
879933{-!
880−deriving instance Binary PTerm
934+dg instance Binary PTerm
881935deriving instance NFData PTerm
882936!-}
883937
@@ -968,6 +1022,14 @@ instance Sized a => Sized (PTactic' a) where
9681022 size Skip = 1
9691023 size (TFail ts) = 1 + size ts
9701024 size SourceFC = 1
1025+ size DoUnify = 1
1026+ size (CaseTac x) = 1 + size x
1027+ size (Equiv t) = 1 + size t
1028+ size (Claim x y) = 1 + size x + size y
1029+ size Unfocus = 1
1030+ size (MatchRefine x) = 1 + size x
1031+ size (LetTacTy x y z) = 1 + size x + size y + size z
1032+ size TCInstance = 1
9711033
9721034type PTactic = PTactic' PTerm
9731035
@@ -1092,6 +1154,8 @@ highestFC (PNoImplicits tm) = highestFC tm
10921154highestFC (PQuasiquote _ _) = Nothing
10931155highestFC (PUnquote tm) = highestFC tm
10941156highestFC (PQuoteName _) = Nothing
1157+highestFC (PRunElab fc _ _) = Just fc
1158+highestFC (PAppImpl t _) = highestFC t
10951159
10961160-- Type class data
10971161
@@ -1429,6 +1493,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
14291493consoleDecorate ist (AnnTerm _ _) = id
14301494consoleDecorate ist (AnnSearchResult _) = id
14311495consoleDecorate ist (AnnErr _) = id
1496+consoleDecorate ist (AnnNamespace _ _) = id
14321497
14331498isPostulateName :: Name -> IState -> Bool
14341499isPostulateName 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+11−1
@@ -91,8 +91,18 @@ 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+ let outerFC = FC fn start end
98+ return (mapPTermFC (fixFC outerFC) (fixFCH fn outerFC) expr)
9599 <?> "user-defined expression"
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
96106
97107{- | Parses a simple user-defined expression -}
98108simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
test/proof002/expected+1−1
@@ -1,4 +1,4 @@
1−Reflect.idr:208:38:
1+test030a.idr:12:26-14:1:
22When checking right hand side of testReflect1:
33When checking an application of function Reflect.getJust:
44 Type mismatch between
test/syntax001/Syntax.idrnew file+8
@@ -0,0 +1,8 @@
1+module Syntax
2+
3+syntax "fnord" [y] = y + y + y
4+
5+foo : Nat
6+foo = fnord "argh"
7+
8+
test/syntax001/SyntaxOk.idrnew file+6
@@ -0,0 +1,6 @@
1+module SyntaxOk
2+
3+syntax "fnord" [y] = y + y + y
4+
5+
6+
test/syntax001/SyntaxTest.idrnew file+5
@@ -0,0 +1,5 @@
1+module SyntaxTest
2+import SyntaxOk
3+
4+foo : Nat
5+foo = fnord "argh"
test/syntax001/expectednew file+12
@@ -0,0 +1,12 @@
1+Syntax.idr:6:7-9: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+SyntaxTest.idr:5:7-6:1: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