e9e7993 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Replace absurd syntax rule FCs

e9e7993David Raymond Christiansen11 years ago

idris.cabal+4

compare with master

unifiedsplit

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

641 test/sugar005/*.idr

642 test/sugar005/expected

643

644+ test/syntax001/run

645+ test/syntax001/*.idr

646+ test/syntax001/expected

647+

644 test/tactics001/run

648 test/tactics001/run

645 test/tactics001/*.idr

649 test/tactics001/*.idr

646 test/tactics001/expected

650 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

873 deriving (Eq, Data, Typeable)

874

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

876− | FirstSuccess

876+ | FirstSuccess

877 deriving (Eq, Data, Typeable)

878

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+

879{-!

931{-!

880−deriving instance Binary PTerm

932+dg instance Binary PTerm

881deriving instance NFData PTerm

933deriving instance NFData PTerm

882!-}

934!-}

883

935

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

968 size Skip = 1

1020 size Skip = 1

969 size (TFail ts) = 1 + size ts

1021 size (TFail ts) = 1 + size ts

970 size SourceFC = 1

1022 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

971

1031

972type PTactic = PTactic' PTerm

1032type PTactic = PTactic' PTerm

973

1033

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

1092highestFC (PQuasiquote _ _) = Nothing

1152highestFC (PQuasiquote _ _) = Nothing

1093highestFC (PUnquote tm) = highestFC tm

1153highestFC (PUnquote tm) = highestFC tm

1094highestFC (PQuoteName _) = Nothing

1154highestFC (PQuoteName _) = Nothing

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

1156+highestFC (PAppImpl t _) = highestFC t

1095

1157

1096-- Type class data

1158-- Type class data

1097

1159

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

1429consoleDecorate ist (AnnTerm _ _) = id

1491consoleDecorate ist (AnnTerm _ _) = id

1430consoleDecorate ist (AnnSearchResult _) = id

1492consoleDecorate ist (AnnSearchResult _) = id

1431consoleDecorate ist (AnnErr _) = id

1493consoleDecorate ist (AnnErr _) = id

1494+consoleDecorate ist (AnnNamespace _ _) = id

1432

1495

1433isPostulateName :: Name -> IState -> Bool

1496isPostulateName :: Name -> IState -> Bool

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

1497isPostulateName 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

107spanFC NoFC fc = fc

108spanFC fc NoFC = fc

109

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)

110

120

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

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

112instance Eq FC where

122instance Eq FC where

src/Idris/ParseExpr.hs+6−1

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

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

92externalExpr :: SyntaxInfo -> IdrisParser PTerm

93externalExpr syn = do i <- get

94+ (FC fn start _) <- getFC

94− extensions syn (syntaxRulesList $ syntax_rules i)

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

96+ (FC _ _ end) <- getFC

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

95 <?> "user-defined expression"

98 <?> "user-defined expression"

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

100+ | otherwise = FileFC fn

101

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

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

98simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

103simpleExternalExpr :: 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