af66f25 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'mutual' blocks

Effect is to elaborate all types in the block before elaborating definitions

commitaf66f2553110d697d1196bcf8982b3ad6587ded4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Oct 2012, 08:38 (14 years ago) parent264b67f

6 files changed+40−10

compare with master

unifiedsplit

CHANGELOG+3 src/Core/CoreParser.hs+11−9 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabDecls.hs+7−1 src/Idris/IBC.hs+6 src/Idris/Parser.hs+12

CHANGELOG+3

@@ -4,6 +4,9 @@ User visible changes:

55* Forward declarations of data allowed

66 - supporting induction recursion and mutually recursive data

7+* 'mutual' blocks added

8+ - effect is to elaborate all types of declarations in the block before

9+ elaborating their definitions

710* Implicit arguments will be added automatically only if their initial

811 letter is lower case, or they are in a using declaration

912

src/Core/CoreParser.hs+11−9

@@ -19,15 +19,17 @@ idrisDef = haskellDef {

1919 opStart = iOpStart,

2020 opLetter = iOpLetter,

2121 identLetter = identLetter haskellDef <|> lchar '.',

22− reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

23− reservedNames = ["let", "in", "data", "codata", "record", "Set",

24− "do", "dsl", "import", "impossible",

25− "case", "of", "total", "partial",

26− "infix", "infixl", "infixr",

27− "where", "with", "syntax", "proof", "postulate",

28− "using", "namespace", "class", "instance",

29− "public", "private", "abstract",

30− "Int", "Integer", "Float", "Char", "String", "Ptr"]

22+ reservedOpNames

23+ = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

24+ reservedNames

25+ = ["let", "in", "data", "codata", "record", "Set",

26+ "do", "dsl", "import", "impossible",

27+ "case", "of", "total", "partial", "mutual",

28+ "infix", "infixl", "infixr",

29+ "where", "with", "syntax", "proof", "postulate",

30+ "using", "namespace", "class", "instance",

31+ "public", "private", "abstract",

32+ "Int", "Integer", "Float", "Char", "String", "Ptr"]

3133 }

3234

3335iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

src/Idris/AbsSyntaxTree.hs+1

@@ -296,6 +296,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

296296 [PDecl' t]

297297 | PDSL Name (DSL' t)

298298 | PSyntax FC Syntax

299+ | PMutual FC [PDecl' t]

299300 | PDirective (Idris ())

300301 deriving Functor

301302{-!

src/Idris/ElabDecls.hs+7−1

@@ -952,9 +952,12 @@ elabDecl' what info (PTy s f o n ty)

952952 = do iLOG $ "Elaborating type decl " ++ show n ++ show o

953953 elabType info s f o n ty

954954elabDecl' what info (PData s f co d)

955− | what /= EDefns

955+ | what /= ETypes

956956 = do iLOG $ "Elaborating " ++ show (d_name d)

957957 elabData info s f co d

958+ | otherwise

959+ = do iLOG $ "Elaborating [type of] " ++ show (d_name d)

960+ elabData info s f co (PLaterdecl (d_name d) (d_tcon d))

958961elabDecl' what info d@(PClauses f o n ps)

959962 | what /= ETypes

960963 = do iLOG $ "Elaborating clause " ++ show n

@@ -963,6 +966,9 @@ elabDecl' what info d@(PClauses f o n ps)

963966 [fs] -> fs

964967 [] -> []

965968 elabClauses info f (o ++ o') n ps

969+elabDecl' what info (PMutual f ps)

970+ = do mapM_ (elabDecl ETypes info) ps

971+ mapM_ (elabDecl EDefns info) ps

966972elabDecl' what info (PParams f ns ps)

967973 = do i <- get

968974 iLOG $ "Expanding params block with " ++ show (concatMap declared ps)

src/Idris/IBC.hs+6

@@ -920,6 +920,9 @@ instance (Binary t) => Binary (PDecl' t) where

920920 put x1

921921 put x2

922922 put x3

923+ PMutual x1 x2 -> do putWord8 11

924+ put x1

925+ put x2

923926 get

924927 = do i <- getWord8

925928 case i of

@@ -980,6 +983,9 @@ instance (Binary t) => Binary (PDecl' t) where

980983 x2 <- get

981984 x3 <- get

982985 return (PCAF x1 x2 x3)

986+ 11 -> do x1 <- get

987+ x2 <- get

988+ return (PMutual x1 x2)

983989 _ -> error "Corrupted binary data for PDecl'"

984990

985991instance Binary SyntaxInfo where

src/Idris/Parser.hs+12

@@ -306,6 +306,7 @@ collect (c@(PClauses _ o _ _) : ds)

306306 getfc (PClauses fc _ _ _) = fc

307307

308308collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

309+collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

309310collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

310311collect (PClass f s cs n ps ds : ds') = PClass f s cs n ps (collect ds) : collect ds'

311312collect (PInstance f s cs n ps t en ds : ds')

@@ -329,6 +330,7 @@ pDecl syn = do notEndBlock

329330 return [d']

330331 <|> pUsing syn

331332 <|> pParams syn

333+ <|> pMutual syn

332334 <|> pNamespace syn

333335 <|> pClass syn

334336 <|> pInstance syn

@@ -454,6 +456,16 @@ pParams syn =

454456 fc <- pfc

455457 return [PParams fc ns (concat ds)]

456458

459+pMutual :: SyntaxInfo -> IParser [PDecl]

460+pMutual syn =

461+ do reserved "mutual"

462+ openBlock

463+ let pvars = syn_params syn

464+ ds <- many1 (pDecl syn)

465+ closeBlock

466+ fc <- pfc

467+ return [PMutual fc (concat ds)]

468+

457469pNamespace :: SyntaxInfo -> IParser [PDecl]

458470pNamespace syn =

459471 do reserved "namespace"; n <- identifier;