a10e866 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added data options

a10e866Ahmad Salim Al-Sibahi13 years ago

src/Idris/AbsSyntax.hs+6

compare with master

unifiedsplit

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

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

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

608 (PRef bi inferTy)), bi)]

609+inferOpts = []

609

610

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

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

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

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

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

628unitCon = MN 0 "__II"

629unitCon = MN 0 "__II"

629unitDecl = PDatadecl unitTy PType

630unitDecl = PDatadecl unitTy PType

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

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

632+unitOpts = [DefaultEliminator]

631

633

632falseTy = MN 0 "__False"

634falseTy = MN 0 "__False"

633falseDecl = PDatadecl falseTy PType []

635falseDecl = PDatadecl falseTy PType []

636+falseOpts = []

634

637

635pairTy = MN 0 "__Pair"

638pairTy = MN 0 "__Pair"

636pairCon = MN 0 "__MkPair"

639pairCon = MN 0 "__MkPair"

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

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

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

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

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

644 where n a = MN 0 a

647 where n a = MN 0 a

648+pairOpts = [DefaultEliminator]

645

649

646eqTy = UN "="

650eqTy = UN "="

647eqCon = UN "refl"

651eqCon = UN "refl"

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

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

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

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

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

657 where n a = MN 0 a

661 where n a = MN 0 a

662+eqOpts = []

663+

658

664

659-- Defined in builtins.idr

665-- Defined in builtins.idr

660sigmaTy = UN "Exists"

666sigmaTy = UN "Exists"

src/Idris/AbsSyntaxTree.hs+9−1

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

388dictionary :: FnOpts -> Bool

389dictionary = elem Dictionary

390

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+

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

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

392-- datatypes and typeclasses.

400-- datatypes and typeclasses.

393data PDecl' t

401data PDecl' t

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

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

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

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

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

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

406 | 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.

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

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

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

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

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

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

src/Idris/DeepSeq.hs+4

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

164 rnf Reflection = ()

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

166

167+instance NFData DataOpt where

168+ rnf Codata = ()

169+ rnf DefaultEliminator = ()

170+

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

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

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

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

169 rnf (PTy x1 x2 x3 x4 x5 x6)

173 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

143 -- remove it from the deferred definitions list

144 solveDeferred n

145

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

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

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

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

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

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

149+ iLOG (show (fc, doc))

149 checkUndefined fc n

150 checkUndefined fc n

150 ctxt <- getContext

151 ctxt <- getContext

151 i <- getIState

152 i <- getIState

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

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

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

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

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

163

164

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

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

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

165− = do iLOG (show fc)

167+ iLOG (show fc)

166 undef <- isUndefined fc n

168 undef <- isUndefined fc n

167 ctxt <- getContext

169 ctxt <- getContext

168 i <- getIState

170 i <- getIState

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

249

251

250elabPrims :: Idris ()

252elabPrims :: Idris ()

251elabPrims = do mapM_ (elabDecl EAll toplevel)

253elabPrims = do mapM_ (elabDecl EAll toplevel)

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

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

255+ (zip

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

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

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

254 mapM_ elabPrim primitives

258 mapM_ elabPrim primitives

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

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

256 elabBelieveMe

260 elabBelieveMe

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

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

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

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

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

402elabRecord info syn doc fc tyn ty cdoc cn cty

406elabRecord 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)])

404 cty' <- implicit syn cn cty

408 cty' <- implicit syn cn cty

405 i <- getIState

409 i <- getIState

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

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

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

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

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

1275 let ddecl = PDatadecl tn tty cons

1279 let ddecl = PDatadecl tn tty cons

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

1280 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

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

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

1279 logLvl 5 $ "Building functions"

1283 logLvl 5 $ "Building functions"

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

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

1697 elabRecord info s doc f tyn ty cdoc cn cty

1701 elabRecord info s doc f tyn ty cdoc cn cty

1698 | otherwise

1702 | otherwise

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

1703 = 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)

1701elabDecl' _ info (PDSL n dsl)

1705elabDecl' _ info (PDSL n dsl)

1702 = do i <- getIState

1706 = do i <- getIState

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

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

src/Idris/IBC.hs+10−1

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

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 44

26+ibcVersion = 45

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

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

932 else return (initIBC { ver = x1 })

933

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+

934instance Binary FnOpt where

943instance Binary FnOpt where

935 put x

944 put x

936 = case x of

945 = case x of

src/Idris/ParseData.hs+22−12

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

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

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

72-}

73−dataI :: IdrisParser Bool

73+dataI :: IdrisParser DataOpts

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

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

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

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 [])

77{- | Parses a data type declaration

83{- | Parses a data type declaration

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

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

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

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

80 ;

86 ;

81Constructor' ::= Constructor KeepTerminator;

87Constructor' ::= Constructor KeepTerminator;

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

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

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

90 ;

96 ;

91-}

97-}

92data_ :: SyntaxInfo -> IdrisParser PDecl

98data_ :: SyntaxInfo -> IdrisParser PDecl

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

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

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

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

95 pushIndent

101 pushIndent

96 acc <- optional accessibility

102 acc <- optional accessibility

103+ elim <- defaultEliminator

97 co <- dataI

104 co <- dataI

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

98− return (doc, acc, co))

106+ return (doc, acc, dataOpts))

99 fc <- getFC

107 fc <- getFC

100 tyn_in <- fnName

108 tyn_in <- fnName

101 (do try (lchar ':')

109 (do try (lchar ':')

102 popIndent

110 popIndent

103 ty <- typeExpr (allowImp syn)

111 ty <- typeExpr (allowImp syn)

104 let tyn = expandNS syn tyn_in

112 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

106 reserved "where"

114 reserved "where"

107 cons <- indentedBlock (constructor syn)

115 cons <- indentedBlock (constructor syn)

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

116 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

110 args <- many name

118 args <- many name

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

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

112 let tyn = expandNS syn tyn_in

120 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

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

122 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 "

116 let n = show tyn_in ++ " "

124 let n = show tyn_in ++ " "

117 let s = kw ++ n

125 let s = kw ++ n

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

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

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

129 do let cty = bindArgs cargs conty

137 do let cty = bindArgs cargs conty

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

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

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

139 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')))

133 <?> "data type declaration"

141 <?> "data type declaration"

134 where

142 where

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

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

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

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

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

138 bindArgs :: [PTerm] -> PTerm -> PTerm

146 bindArgs :: [PTerm] -> PTerm -> PTerm

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

147 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

140

150

141

151

142{- | Parses a type constructor declaration

152{- | Parses a type constructor declaration