af66f25 · Idris-dev · git.iko.soy

CHANGELOG+3

compare with master

unifiedsplit

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

4

5* Forward declarations of data allowed

6 - 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

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

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

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

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

9

12

src/Core/CoreParser.hs+11−9

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

19 opStart = iOpStart,

20 opLetter = iOpLetter,

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

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

22+ reservedOpNames

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

24+ reservedNames

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

31 }

33 }

32

34

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

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

src/Idris/AbsSyntaxTree.hs+1

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

296 [PDecl' t]

297 | PDSL Name (DSL' t)

298 | PSyntax FC Syntax

299+ | PMutual FC [PDecl' t]

299 | PDirective (Idris ())

300 | PDirective (Idris ())

300 deriving Functor

301 deriving Functor

301{-!

302{-!

src/Idris/ElabDecls.hs+7−1

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

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

953 elabType info s f o n ty

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

955− | what /= EDefns

955+ | what /= ETypes

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

957 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))

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

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

959 | what /= ETypes

962 | what /= ETypes

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

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

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

963 [fs] -> fs

966 [fs] -> fs

964 [] -> []

967 [] -> []

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

968 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

966elabDecl' what info (PParams f ns ps)

972elabDecl' what info (PParams f ns ps)

967 = do i <- get

973 = do i <- get

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

974 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

920 put x1

921 put x2

922 put x3

923+ PMutual x1 x2 -> do putWord8 11

924+ put x1

925+ put x2

923 get

926 get

924 = do i <- getWord8

927 = do i <- getWord8

925 case i of

928 case i of

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

980 x2 <- get

983 x2 <- get

981 x3 <- get

984 x3 <- get

982 return (PCAF x1 x2 x3)

985 return (PCAF x1 x2 x3)

986+ 11 -> do x1 <- get

987+ x2 <- get

988+ return (PMutual x1 x2)

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

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

984

990

985instance Binary SyntaxInfo where

991instance Binary SyntaxInfo where

src/Idris/Parser.hs+12

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

306 getfc (PClauses fc _ _ _) = fc

307

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

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

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

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

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

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

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

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

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

329 return [d']

330 return [d']

330 <|> pUsing syn

331 <|> pUsing syn

331 <|> pParams syn

332 <|> pParams syn

333+ <|> pMutual syn

332 <|> pNamespace syn

334 <|> pNamespace syn

333 <|> pClass syn

335 <|> pClass syn

334 <|> pInstance syn

336 <|> pInstance syn

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

454 fc <- pfc

456 fc <- pfc

455 return [PParams fc ns (concat ds)]

457 return [PParams fc ns (concat ds)]

456

458

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+

457pNamespace :: SyntaxInfo -> IParser [PDecl]

469pNamespace :: SyntaxInfo -> IParser [PDecl]

458pNamespace syn =

470pNamespace syn =

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

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