a10e866 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added data options

commita10e86672dc9d2d3457ecd33c2178852964a44ed authorAhmad Salim Al-Sibahi <asal@itu.dk> dateTue 26 Nov 2013, 13:31 (13 years ago) parent16847d5

6 files changed+65−24

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+9−1 src/Idris/DeepSeq.hs+4 src/Idris/ElabDecls.hs+14−10 src/Idris/IBC.hs+10−1 src/Idris/ParseData.hs+22−12

src/Idris/AbsSyntax.hs+6

@@ -606,6 +606,7 @@ inferDecl = PDatadecl inferTy

606606 [("", inferCon, PPi impl (MN 0 "A") PType (

607607 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

608608 (PRef bi inferTy)), bi)]

609+inferOpts = []

609610

610611infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

611612infP = P (TCon 6 0) inferTy (TType (UVal 0))

@@ -628,9 +629,11 @@ unitTy = MN 0 "__Unit"

628629unitCon = MN 0 "__II"

629630unitDecl = PDatadecl unitTy PType

630631 [("", unitCon, PRef bi unitTy, bi)]

632+unitOpts = [DefaultEliminator]

631633

632634falseTy = MN 0 "__False"

633635falseDecl = PDatadecl falseTy PType []

636+falseOpts = []

634637

635638pairTy = MN 0 "__Pair"

636639pairCon = MN 0 "__MkPair"

@@ -642,6 +645,7 @@ pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)

642645 (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),

643646 pexp (PRef bi (n "B"))])))), bi)]

644647 where n a = MN 0 a

648+pairOpts = [DefaultEliminator]

645649

646650eqTy = UN "="

647651eqCon = UN "refl"

@@ -655,6 +659,8 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

655659 pexp (PRef bi (n "x")),

656660 pexp (PRef bi (n "x"))])), bi)]

657661 where n a = MN 0 a

662+eqOpts = []

663+

658664

659665-- Defined in builtins.idr

660666sigmaTy = UN "Exists"

src/Idris/AbsSyntaxTree.hs+9−1

@@ -388,6 +388,14 @@ inlinable = elem Inlinable

388388dictionary :: FnOpts -> Bool

389389dictionary = elem Dictionary

390390

391+

392+-- | Data declaration options

393+data DataOpt = Codata -- Set if the the data-type is coinductive

394+ | DefaultEliminator -- Set if an eliminator should be generated for data type

395+ deriving (Show, Eq)

396+

397+type DataOpts = [DataOpt]

398+

391399-- | Top-level declarations such as compiler directives, definitions,

392400-- datatypes and typeclasses.

393401data PDecl' t

@@ -396,7 +404,7 @@ data PDecl' t

396404 | PPostulate String SyntaxInfo FC FnOpts Name t -- ^ Postulate

397405 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

398406 | PCAF FC Name t -- ^ Top level constant

399− | PData String SyntaxInfo FC Bool (PData' t) -- ^ Data declaration. The Bool argument is True for codata.

407+ | PData String SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

400408 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

401409 | PNamespace String [PDecl' t] -- ^ New namespace

402410 | PRecord String SyntaxInfo FC Name t String Name t -- ^ Record declaration

src/Idris/DeepSeq.hs+4

@@ -164,6 +164,10 @@ instance NFData FnOpt where

164164 rnf Reflection = ()

165165 rnf (Specialise x1) = rnf x1 `seq` ()

166166

167+instance NFData DataOpt where

168+ rnf Codata = ()

169+ rnf DefaultEliminator = ()

170+

167171instance (NFData t) => NFData (PDecl' t) where

168172 rnf (PFix x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

169173 rnf (PTy x1 x2 x3 x4 x5 x6)

src/Idris/ElabDecls.hs+14−10

@@ -143,9 +143,10 @@ elabPostulate info syn doc fc opts n ty

143143 -- remove it from the deferred definitions list

144144 solveDeferred n

145145

146−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()

147−elabData info syn doc fc codata (PLaterdecl n t_in)

148− = do iLOG (show (fc, doc))

146+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

147+elabData info syn doc fc opts (PLaterdecl n t_in)

148+ = do let codata = Codata `elem` opts

149+ iLOG (show (fc, doc))

149150 checkUndefined fc n

150151 ctxt <- getContext

151152 i <- getIState

@@ -161,8 +162,9 @@ elabData info syn doc fc codata (PLaterdecl n t_in)

161162 logLvl 2 $ "---> " ++ show cty

162163 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons

163164

164−elabData info syn doc fc codata (PDatadecl n t_in dcons)

165− = do iLOG (show fc)

165+elabData info syn doc fc opts (PDatadecl n t_in dcons)

166+ = do let codata = Codata `elem` opts

167+ iLOG (show fc)

166168 undef <- isUndefined fc n

167169 ctxt <- getContext

168170 i <- getIState

@@ -249,8 +251,10 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

249251

250252elabPrims :: Idris ()

251253elabPrims = do mapM_ (elabDecl EAll toplevel)

252− (map (PData "" defaultSyntax (fileFC "builtin") False)

253− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

254+ (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)

255+ (zip

256+ [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]

257+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))

254258 mapM_ elabPrim primitives

255259 -- Special case prim__believe_me because it doesn't work on just constants

256260 elabBelieveMe

@@ -400,7 +404,7 @@ elabTransform info fc safe lhs_in rhs_in

400404elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

401405 PTerm -> String -> Name -> PTerm -> Idris ()

402406elabRecord info syn doc fc tyn ty cdoc cn cty

403− = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

407+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])

404408 cty' <- implicit syn cn cty

405409 i <- getIState

406410 cty <- case lookupTy cn (tt_ctxt i) of

@@ -1274,7 +1278,7 @@ elabClass info syn doc fc constraints tn ps ds

12741278 let cons = [("", cn, cty, fc)]

12751279 let ddecl = PDatadecl tn tty cons

12761280 logLvl 5 $ "Class data " ++ showDImp True ddecl

1277− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl

1281+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

12781282 -- for each constraint, build a top level function to chase it

12791283 logLvl 5 $ "Building functions"

12801284 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -1697,7 +1701,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

16971701 elabRecord info s doc f tyn ty cdoc cn cty

16981702 | otherwise

16991703 = do iLOG $ "Elaborating [type of] " ++ show tyn

1700− elabData info s doc f False (PLaterdecl tyn ty)

1704+ elabData info s doc f [] (PLaterdecl tyn ty)

17011705elabDecl' _ info (PDSL n dsl)

17021706 = do i <- getIState

17031707 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })

src/Idris/IBC.hs+10−1

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 44

26+ibcVersion = 45

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -931,6 +931,15 @@ instance Binary IBCFile where

931931 return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27)

932932 else return (initIBC { ver = x1 })

933933

934+instance Binary DataOpt where

935+ put x = case x of

936+ Codata -> putWord8 0

937+ DefaultEliminator -> putWord8 1

938+ get = do i <- getWord8

939+ case i of

940+ 0 -> return Codata

941+ 1 -> return DefaultEliminator

942+

934943instance Binary FnOpt where

935944 put x

936945 = case x of

src/Idris/ParseData.hs+22−12

@@ -70,13 +70,19 @@ record syn = do (doc, acc) <- try (do

7070{- | Parses data declaration type (normal or codata)

7171DataI ::= 'data' | 'codata';

7272-}

73−dataI :: IdrisParser Bool

74−dataI = do reserved "data"; return False

75− <|> do reserved "codata"; return True

73+dataI :: IdrisParser DataOpts

74+dataI = do reserved "data"; return []

75+ <|> do reserved "codata"; return [Codata]

76+

77+{- | Parses if a data should not have a default eliminator

78+DefaultEliminator ::= 'noelim'?

79+ -}

80+defaultEliminator :: IdrisParser DataOpts

81+defaultEliminator = do option [DefaultEliminator] (do reserved "%noelim"; return [])

7682

7783{- | Parses a data type declaration

78−Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?

79− | DocComment? Accessibility? DataI FnName Name* DataRest?

84+Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest?

85+ | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest?

8086 ;

8187Constructor' ::= Constructor KeepTerminator;

8288ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

@@ -90,29 +96,31 @@ SimpleConstructorList ::=

9096 ;

9197-}

9298data_ :: SyntaxInfo -> IdrisParser PDecl

93−data_ syn = do (doc, acc, co) <- try (do

99+data_ syn = do (doc, acc, dataOpts) <- try (do

94100 doc <- option "" (docComment '|')

95101 pushIndent

96102 acc <- optional accessibility

103+ elim <- defaultEliminator

97104 co <- dataI

98− return (doc, acc, co))

105+ let dataOpts = combineDataOpts(elim ++ co)

106+ return (doc, acc, dataOpts))

99107 fc <- getFC

100108 tyn_in <- fnName

101109 (do try (lchar ':')

102110 popIndent

103111 ty <- typeExpr (allowImp syn)

104112 let tyn = expandNS syn tyn_in

105− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

113+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

106114 reserved "where"

107115 cons <- indentedBlock (constructor syn)

108116 accData acc tyn (map (\ (_, n, _, _) -> n) cons)

109− return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do

117+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons))) <|> (do

110118 args <- many name

111119 let ty = bindArgs (map (const PType) args) PType

112120 let tyn = expandNS syn tyn_in

113− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

121+ option (PData doc syn fc dataOpts (PLaterdecl tyn ty)) (do

114122 try (lchar '=') <|> do reserved "where"

115− let kw = (if co then "co" else "") ++ "data "

123+ let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

116124 let n = show tyn_in ++ " "

117125 let s = kw ++ n

118126 let as = concat (intersperse " " $ map show args) ++ " "

@@ -129,7 +137,7 @@ data_ syn = do (doc, acc, co) <- try (do

129137 do let cty = bindArgs cargs conty

130138 return (doc, x, cty, cfc)) cons

131139 accData acc tyn (map (\ (_, n, _, _) -> n) cons')

132− return $ PData doc syn fc co (PDatadecl tyn ty cons')))

140+ return $ PData doc syn fc dataOpts (PDatadecl tyn ty cons')))

133141 <?> "data type declaration"

134142 where

135143 mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

@@ -137,6 +145,8 @@ data_ syn = do (doc, acc, co) <- try (do

137145 mkPApp fc t xs = PApp fc t (map pexp xs)

138146 bindArgs :: [PTerm] -> PTerm -> PTerm

139147 bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

148+ combineDataOpts :: DataOpts -> DataOpts

149+ combineDataOpts opts = if Codata `elem` opts then delete DefaultEliminator opts else opts

140150

141151

142152{- | Parses a type constructor declaration