b5372b5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Removed argument customization for now.

b5372b5Sune Alkærsig12 years ago

src/Idris/Elab/Record.hs+2−2

compare with master

unifiedsplit

@@ -53,13 +53,13 @@ import Util.Pretty(pretty, text)

54elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> Name ->

55 PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Maybe Name -> [(Name, Plicity)] -> PTerm -> Idris ()

56−elabRecord info syn doc fc tyn ty opts cdoc mcn args cty_in'

56+elabRecord info syn doc fc tyn ty opts cdoc mcn args cty_in

57 = do cn <- liftM (expandNS syn) (case mcn of

58 Just cn' -> return (nsroot cn')

59 Nothing -> if isOp tyn

60 then generateConsNameOp

61 else generateConsName (sUN $ "Mk" ++ (show (nsroot tyn))))

62− cty_in <- customizeConstructor args cty_in'

62+

63 elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

64 -- TODO think: something more in info?

65 cty' <- implicit info syn cn cty_in

src/Idris/ParseData.hs+18−23

@@ -38,7 +38,7 @@ import qualified Data.ByteString.UTF8 as UTF8

38import Debug.Trace

40type Docs = Docstring (Either Err PTerm)

41−type RecordConstructor = (Docs, [(Name, Docs)], Maybe Name, PTerm, [(Name, Plicity)])

41+type RecordConstructor = (Docs, [(Name, Docs)], Maybe Name, PTerm)

43{- |Parses a record type declaration

44Record ::=

@@ -59,9 +59,8 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

59 tyn_in <- fnName

60 tys <- manyTill (recordTypeParameter syn) (reserved "where")

61 let ty = recordTypeConstructor tys

62− let ty' = withoutNames ty

63 let tyn = expandNS syn tyn_in

62 let tyn = expandNS syn tyn_in

64− (cdoc, cargDocs, cn, cty, args) <- indentedBlockS $ agdaStyleBody syn tyn ty

63+ (cdoc, cargDocs, cn, cty) <- indentedBlockS $ agdaStyleBody syn tyn ty

65 case cn of

64 case cn of

66 Just cn' -> accData acc tyn [cn']

65 Just cn' -> accData acc tyn [cn']

67 Nothing -> return ()

66 Nothing -> return ()

@@ -69,7 +68,7 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

69 syn_namespace syn }

68 syn_namespace syn }

70 let fns = getRecNames rsyn cty

69 let fns = getRecNames rsyn cty

71 mapM_ (\n -> addAcc n acc) fns

70 mapM_ (\n -> addAcc n acc) fns

72− return $ PRecord doc rsyn fc tyn ty' opts cdoc cn args cty

71+ return $ PRecord doc rsyn fc tyn ty opts cdoc cn [] cty

73 <?> "record type declaration"

72 <?> "record type declaration"

74 where

73 where

75 withoutNames :: PTerm -> PTerm

74 withoutNames :: PTerm -> PTerm

@@ -98,9 +97,8 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

98 fields <- many . indented $ field

97 fields <- many . indented $ field

100 let constructorDoc = parseDocstring . T.pack $ "Constructor of " ++ show tyn

99 let constructorDoc = parseDocstring . T.pack $ "Constructor of " ++ show tyn

101− (constructorName, args) <- do c <- optional constructor

100+ constructorName <- do n <- optional constructor

102− let (n, args) = maybePair c

103− return (n, mList args)

101+ return n

104

102

105 let constructorDoc' = annotate syn ist constructorDoc

103 let constructorDoc' = annotate syn ist constructorDoc

106 let fieldDocs = [(n, annotate syn ist doc) | (n, _, _, doc, _) <- fields]

104 let fieldDocs = [(n, annotate syn ist doc) | (n, _, _, doc, _) <- fields]

@@ -108,7 +106,7 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

108 constructorType = mkConstructorType [(n, t, p) | (n, t, p, _, _) <- fields] target

106 constructorType = mkConstructorType [(n, t, p) | (n, t, p, _, _) <- fields] target

109 constructorType' = replaceTarget constructorType (allImpl tyc)

107 constructorType' = replaceTarget constructorType (allImpl tyc)

110

108

111− return (constructorDoc', fieldDocs, constructorName, constructorType', args)

109+ return (constructorDoc', fieldDocs, constructorName, constructorType')

112 where

110 where

113 maybePair :: Maybe (a, b) -> (Maybe a, Maybe b)

111 maybePair :: Maybe (a, b) -> (Maybe a, Maybe b)

114 maybePair (Just(x, y)) = (Just x, Just y)

112 maybePair (Just(x, y)) = (Just x, Just y)

@@ -117,11 +115,6 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

117 mList :: Maybe [a] -> [a]

115 mList :: Maybe [a] -> [a]

118 mList (Just xs) = xs

116 mList (Just xs) = xs

119 mList Nothing = []

117 mList Nothing = []

120−

121− fieldsAndConstructor :: IdrisParser ([(Name, PTerm, Plicity, Docstring (), [(Name, Docstring ())])], (Maybe Name), [(Name, Plicity)])

122− fieldsAndConstructor = do fields <- (indented field) `manyTill` (reserved "constructor")

123− (cName, args) <- indented constructor

124− return (fields, Just cName, args)

125

118

126 allImpl :: PTerm -> PTerm

119 allImpl :: PTerm -> PTerm

127 allImpl (PPi _ n t t') = PPi impl n t (allImpl t')

120 allImpl (PPi _ n t t') = PPi impl n t (allImpl t')

@@ -129,21 +122,23 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

129

122

130 field :: IdrisParser (Name, PTerm, Plicity, Docstring (), [(Name, Docstring ())])

123 field :: IdrisParser (Name, PTerm, Plicity, Docstring (), [(Name, Docstring ())])

131 field = do (doc, argDocs) <- option noDocs docComment

124 field = do (doc, argDocs) <- option noDocs docComment

125+ c <- optional $ lchar '{'

132 n <- fnName

126 n <- fnName

133 lchar ':'

127 lchar ':'

134 t <- typeExpr (allowImp syn)

128 t <- typeExpr (allowImp syn)

129+ p <- endPlicity c

135− return (n, t, expl, doc, argDocs)

130+ return (n, t, p, doc, argDocs)

136

131

137− constructor :: IdrisParser (Name, [(Name, Plicity)])

132+ constructor :: IdrisParser Name -- (Name, [(Name, Plicity)])

138 constructor = do n <- (reserved "constructor") *> fnName

133 constructor = do n <- (reserved "constructor") *> fnName

139− args <- option [] (do lchar '('

134+ -- args <- option [] (do lchar '('

140− args <- many (do p <- optional $ lchar '{'

135+ -- args <- many (do p <- optional $ lchar '{'

141− argName <- fnName

136+ -- argName <- fnName

142− plicity <- endPlicity p

137+ -- plicity <- endPlicity p

143− return (argName, plicity))

138+ -- return (argName, plicity))

144− lchar ')'

139+ -- lchar ')'

145− return args)

140+ -- return args)

146− return (n, args)

141+ return n

147

142

148 endPlicity :: Maybe Char -> IdrisParser Plicity

143 endPlicity :: Maybe Char -> IdrisParser Plicity

149 endPlicity (Just _) = do lchar '}'

144 endPlicity (Just _) = do lchar '}'