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

git.iko.soy/Idris-dev

Record data type info

commit3f18d02fb073ebf76bea0f777bf1db1eabdfbf6a authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 10 Jan 2012, 17:10 (15 years ago) parent38732d8

3 files changed+37−5

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+9−1 src/Idris/ElabDecls.hs+4 src/Idris/IBC.hs+24−4

src/Idris/AbsSyntax.hs+9−1

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

4040 idris_statics :: Ctxt [Bool],

4141 idris_classes :: Ctxt ClassInfo,

4242 idris_optimisation :: Ctxt OptInfo,

43+ idris_datatypes :: Ctxt TypeInfo,

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

4445 idris_log :: String,

4546 idris_options :: IOption,

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

6869 | IBCImp Name

6970 | IBCStatic Name

7071 | IBCClass Name

72+ | IBCData Name

7173 | IBCOpt Name

7274 | IBCSyntax Syntax

7375 | IBCKeyword String

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

8082 deriving Show

8183

8284idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

83− emptyContext emptyContext

85+ emptyContext emptyContext emptyContext

8486 "" defaultOpts 6 [] [] [] [] [] [] [] []

8587 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

8688

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

534536!-}

535537

536538

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

540+ deriving Show

541+{-!

542+deriving instance Binary TypeInfo

543+!-}

544+

537545-- Syntactic sugar info

538546

539547data DSL = DSL { dsl_bind :: PTerm,

src/Idris/ElabDecls.hs+4

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

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

7272 cons <- mapM (elabCon info syn) dcons

7373 ttag <- getName

74+ i <- get

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

76+ (idris_datatypes i) })

7477 addIBC (IBCDef n)

78+ addIBC (IBCData n)

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

7680

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

src/Idris/IBC.hs+24−4

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

2222import Paths_idris

2323

2424ibcVersion :: Word8

25−ibcVersion = 6

25+ibcVersion = 7

2626

2727data IBCFile = IBCFile { ver :: Word8,

2828 sourcefile :: FilePath,

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

3131 ibc_fixes :: [FixDecl],

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

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

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

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

3536 ibc_syntax :: [Syntax],

3637 ibc_keywords :: [String],

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

4445!-}

4546

4647initIBC :: IBCFile

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

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

4849

4950loadIBC :: FilePath -> Idris ()

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

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

8384 = case lookupCtxt Nothing n (idris_classes i) of

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

8586 _ -> 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"

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

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

8893 _ -> fail "IBC write failed"

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

111116 pFixes (ibc_fixes i)

112117 pStatics (ibc_statics i)

113118 pClasses (ibc_classes i)

119+ pDatatypes (ibc_datatypes i)

114120 pOptimise (ibc_optimise i)

115121 pSyntax (ibc_syntax i)

116122 pKeywords (ibc_keywords i)

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

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

169175 cs

170176

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+

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

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

173186 do i <- getIState

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

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

556569

557570instance 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)

559572 = do put x1

560573 put x2

561574 put x3

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

571584 put x13

572585 put x14

573586 put x15

587+ put x16

574588 get

575589 = do x1 <- get

576590 if x1 == ibcVersion then

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

588602 x13 <- get

589603 x14 <- get

590604 x15 <- get

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

605+ x16 <- get

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

592607 else return (initIBC { ver = x1 })

593608

594609instance Binary Fixity where

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

978993 x3 <- get

979994 return (Optimise x1 x2 x3)

980995

996+instance Binary TypeInfo where

997+ put (TI x1) = put x1

998+ get = do x1 <- get

999+ return (TI x1)

1000+

9811001instance Binary SynContext where

9821002 put x

9831003 = case x of