3f18d02 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Record data type info

3f18d02Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+9−1

compare with master

unifiedsplit

@@ -40,6 +40,7 @@ data IState = IState { tt_ctxt :: Context,

40 idris_statics :: Ctxt [Bool],

41 idris_classes :: Ctxt ClassInfo,

42 idris_optimisation :: Ctxt OptInfo,

43+ idris_datatypes :: Ctxt TypeInfo,

43 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

44 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

44 idris_log :: String,

45 idris_log :: String,

45 idris_options :: IOption,

46 idris_options :: IOption,

@@ -68,6 +69,7 @@ data IBCWrite = IBCFix FixDecl

68 | IBCImp Name

69 | IBCImp Name

69 | IBCStatic Name

70 | IBCStatic Name

70 | IBCClass Name

71 | IBCClass Name

72+ | IBCData Name

71 | IBCOpt Name

73 | IBCOpt Name

72 | IBCSyntax Syntax

74 | IBCSyntax Syntax

73 | IBCKeyword String

75 | IBCKeyword String

@@ -80,7 +82,7 @@ data IBCWrite = IBCFix FixDecl

80 deriving Show

82 deriving Show

82idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

84idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

83− emptyContext emptyContext

85+ emptyContext emptyContext emptyContext

84 "" defaultOpts 6 [] [] [] [] [] [] [] []

86 "" defaultOpts 6 [] [] [] [] [] [] [] []

85 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

87 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

@@ -534,6 +536,12 @@ deriving instance Binary OptInfo

534!-}

536!-}

535

537

536

538

539+data TypeInfo = TI { con_names :: [Name] }

540+ deriving Show

541+{-!

542+deriving instance Binary TypeInfo

543+!-}

544+

537-- Syntactic sugar info

545-- Syntactic sugar info

538

546

539data DSL = DSL { dsl_bind :: PTerm,

547data DSL = DSL { dsl_bind :: PTerm,

src/Idris/ElabDecls.hs+4

@@ -71,7 +71,11 @@ elabData info syn fc (PDatadecl n t_in dcons)

71 updateContext (addTyDecl n cty) -- temporary, to check cons

72 cons <- mapM (elabCon info syn) dcons

73 ttag <- getName

74+ i <- get

75+ put (i { idris_datatypes = addDef n (TI (map fst cons))

76+ (idris_datatypes i) })

74 addIBC (IBCDef n)

77 addIBC (IBCDef n)

78+ addIBC (IBCData n)

75 updateContext (addDatatype (Data n ttag cty cons))

79 updateContext (addDatatype (Data n ttag cty cons))

77elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

81elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

src/Idris/IBC.hs+24−4

@@ -22,7 +22,7 @@ import System.Directory

22import Paths_idris

24ibcVersion :: Word8

25−ibcVersion = 6

25+ibcVersion = 7

27data IBCFile = IBCFile { ver :: Word8,

28 sourcefile :: FilePath,

@@ -31,6 +31,7 @@ data IBCFile = IBCFile { ver :: Word8,

31 ibc_fixes :: [FixDecl],

32 ibc_statics :: [(Name, [Bool])],

33 ibc_classes :: [(Name, ClassInfo)],

34+ ibc_datatypes :: [(Name, TypeInfo)],

34 ibc_optimise :: [(Name, OptInfo)],

35 ibc_optimise :: [(Name, OptInfo)],

35 ibc_syntax :: [Syntax],

36 ibc_syntax :: [Syntax],

36 ibc_keywords :: [String],

37 ibc_keywords :: [String],

@@ -44,7 +45,7 @@ deriving instance Binary IBCFile

44!-}

45!-}

46initIBC :: IBCFile

47initIBC :: IBCFile

47−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] []

48+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] []

49loadIBC :: FilePath -> Idris ()

50loadIBC :: FilePath -> Idris ()

50loadIBC fp = do iLOG $ "Loading ibc " ++ fp

51loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -83,6 +84,10 @@ ibc i (IBCClass n) f

83 = case lookupCtxt Nothing n (idris_classes i) of

84 = case lookupCtxt Nothing n (idris_classes i) of

84 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

85 [v] -> return f { ibc_classes = (n,v): ibc_classes f }

85 _ -> fail "IBC write failed"

86 _ -> fail "IBC write failed"

87+ibc i (IBCData n) f

88+ = case lookupCtxt Nothing n (idris_datatypes i) of

89+ [v] -> return f { ibc_datatypes = (n,v): ibc_datatypes f }

90+ _ -> fail "IBC write failed"

86ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of

91ibc i (IBCOpt n) f = case lookupCtxt Nothing n (idris_optimisation i) of

87 [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

92 [v] -> return f { ibc_optimise = (n,v): ibc_optimise f }

88 _ -> fail "IBC write failed"

93 _ -> fail "IBC write failed"

@@ -111,6 +116,7 @@ process i fn

111 pFixes (ibc_fixes i)

116 pFixes (ibc_fixes i)

112 pStatics (ibc_statics i)

117 pStatics (ibc_statics i)

113 pClasses (ibc_classes i)

118 pClasses (ibc_classes i)

119+ pDatatypes (ibc_datatypes i)

114 pOptimise (ibc_optimise i)

120 pOptimise (ibc_optimise i)

115 pSyntax (ibc_syntax i)

121 pSyntax (ibc_syntax i)

116 pKeywords (ibc_keywords i)

122 pKeywords (ibc_keywords i)

@@ -168,6 +174,13 @@ pClasses cs = mapM_ (\ (n, c) ->

168 = addDef n c (idris_classes i) }))

174 = addDef n c (idris_classes i) }))

169 cs

175 cs

170

176

177+pDatatypes :: [(Name, TypeInfo)] -> Idris ()

178+pDatatypes cs = mapM_ (\ (n, c) ->

179+ do i <- getIState

180+ putIState (i { idris_datatypes

181+ = addDef n c (idris_datatypes i) }))

182+ cs

183+

171pOptimise :: [(Name, OptInfo)] -> Idris ()

184pOptimise :: [(Name, OptInfo)] -> Idris ()

172pOptimise cs = mapM_ (\ (n, c) ->

185pOptimise cs = mapM_ (\ (n, c) ->

173 do i <- getIState

186 do i <- getIState

@@ -555,7 +568,7 @@ instance Binary Accessibility where

555 _ -> error "Corrupted binary data for Accessibility"

568 _ -> error "Corrupted binary data for Accessibility"

556

569

557instance Binary IBCFile where

570instance Binary IBCFile where

558− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

571+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)

559 = do put x1

572 = do put x1

560 put x2

573 put x2

561 put x3

574 put x3

@@ -571,6 +584,7 @@ instance Binary IBCFile where

571 put x13

584 put x13

572 put x14

585 put x14

573 put x15

586 put x15

587+ put x16

574 get

588 get

575 = do x1 <- get

589 = do x1 <- get

576 if x1 == ibcVersion then

590 if x1 == ibcVersion then

@@ -588,7 +602,8 @@ instance Binary IBCFile where

588 x13 <- get

602 x13 <- get

589 x14 <- get

603 x14 <- get

590 x15 <- get

604 x15 <- get

605+ x16 <- get

591− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15)

606+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16)

592 else return (initIBC { ver = x1 })

607 else return (initIBC { ver = x1 })

593

608

594instance Binary Fixity where

609instance Binary Fixity where

@@ -978,6 +993,11 @@ instance Binary OptInfo where

978 x3 <- get

993 x3 <- get

979 return (Optimise x1 x2 x3)

994 return (Optimise x1 x2 x3)

980

995

996+instance Binary TypeInfo where

997+ put (TI x1) = put x1

998+ get = do x1 <- get

999+ return (TI x1)

1000+

981instance Binary SynContext where

1001instance Binary SynContext where

982 put x

1002 put x

983 = case x of

1003 = case x of