5c4ee75 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Make load to line work with mutual blocks

Now reads entire block before stopping loading (otherwise we might not get all the declarations we need for the block to type check)

commit5c4ee75e9de281034d64a943bc3cf072476869af authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 May 2014, 23:43 (12 years ago) parentdb05606

4 files changed+8−7

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/DeepSeq.hs+2−2 src/Idris/IBC.hs+2−2 src/Idris/Parser.hs+2−2

src/Idris/AbsSyntaxTree.hs+2−1

@@ -964,6 +964,7 @@ data SyntaxInfo = Syn { using :: [Using],

964964 inPattern :: Bool,

965965 implicitAllowed :: Bool,

966966 maxline :: Maybe Int,

967+ mut_nesting :: Int,

967968 dsl_info :: DSL }

968969 deriving Show

969970{-!

@@ -971,7 +972,7 @@ deriving instance NFData SyntaxInfo

971972deriving instance Binary SyntaxInfo

972973!-}

973974

974−defaultSyntax = Syn [] [] [] [] id False False Nothing initDSL

975+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL

975976

976977expandNS :: SyntaxInfo -> Name -> Name

977978expandNS syn n@(NS _ _) = n

src/Idris/DeepSeq.hs+2−2

@@ -321,11 +321,11 @@ instance NFData Using where

321321

322322

323323instance NFData SyntaxInfo where

324− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

325325 = rnf x1 `seq`

326326 rnf x2 `seq`

327327 rnf x3 `seq`

328− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

328+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

329329

330330

331331

src/Idris/IBC.hs+2−2

@@ -1582,7 +1582,7 @@ instance Binary Using where

15821582 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

15831583

15841584instance Binary SyntaxInfo where

1585− put (Syn x1 x2 x3 x4 _ x5 x6 _ x7)

1585+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)

15861586 = do put x1

15871587 put x2

15881588 put x3

@@ -1598,7 +1598,7 @@ instance Binary SyntaxInfo where

15981598 x5 <- get

15991599 x6 <- get

16001600 x7 <- get

1601− return (Syn x1 x2 x3 x4 id x5 x6 Nothing x7)

1601+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7)

16021602

16031603instance (Binary t) => Binary (PClause' t) where

16041604 put x

src/Idris/Parser.hs+2−2

@@ -163,7 +163,7 @@ decl syn = do fc <- getFC

163163 let continue = case maxline syn of

164164 Nothing -> True

165165 Just l -> if fst (fc_end fc) > l

166− then False

166+ then mut_nesting syn /= 0

167167 else True

168168 if continue then do notEndBlock

169169 declBody

@@ -502,7 +502,7 @@ mutual syn =

502502 do reserved "mutual"

503503 openBlock

504504 let pvars = syn_params syn

505− ds <- many (decl syn)

505+ ds <- many (decl (syn { mut_nesting = mut_nesting syn + 1 } ))

506506 closeBlock

507507 fc <- getFC

508508 return [PMutual fc (concat ds)]