173703d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added new (co)record syntax.

173703dSune Alkærsig12 years ago

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -1050,12 +1050,12 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

1050 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

1051 econ (doc, argDocs, n, t, fc, fs)

1052 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1053−expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn cty)

1053+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty opts cdoc cn args cty)

1054 = if tn `elem` ns

1055 then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1056− opts cdoc (dec cn) conty

1056+ opts cdoc (liftM dec cn) args conty

1057 else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1058− opts cdoc (dec cn) conty

1058+ opts cdoc (liftM dec cn) args conty

1059 where conty = piBindp expl ps (expandParams dec ps ns [] cty)

1060expandParamsD rhs ist dec ps ns (PParams f params pds)

1061 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

src/Idris/AbsSyntaxTree.hs+6−5

@@ -586,7 +586,7 @@ data PDecl' t

586 | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

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

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

589− | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration

589+ | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) (Maybe Name) [(Name, Plicity)] t -- ^ Record declaration

590 | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

591 [(Name, t)] -- constraints

592 Name

@@ -680,13 +680,14 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

680declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

681declared (PParams _ _ ds) = concatMap declared ds

682declared (PNamespace _ ds) = concatMap declared ds

683−declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

683+declared (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

684declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

685declared (PInstance _ _ _ _ _ _ _ _) = []

686declared (PDSL n _) = [n]

687declared (PSyntax _ _) = []

688declared (PMutual _ ds) = concatMap declared ds

689declared (PDirective _) = []

690+declared _ = []

690

691

691-- get the names declared, not counting nested parameter blocks

692-- get the names declared, not counting nested parameter blocks

692tldeclared :: PDecl -> [Name]

693tldeclared :: PDecl -> [Name]

@@ -694,7 +695,7 @@ tldeclared (PFix _ _ _) = []

694tldeclared (PTy _ _ _ _ _ n t) = [n]

695tldeclared (PTy _ _ _ _ _ n t) = [n]

695tldeclared (PPostulate _ _ _ _ n t) = [n]

696tldeclared (PPostulate _ _ _ _ n t) = [n]

696tldeclared (PClauses _ _ n _) = [] -- not a declaration

697tldeclared (PClauses _ _ n _) = [] -- not a declaration

697−tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]

698+tldeclared (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

698tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

699tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

699 where fstt (_, _, a, _, _, _) = a

700 where fstt (_, _, a, _, _, _) = a

700tldeclared (PParams _ _ ds) = []

701tldeclared (PParams _ _ ds) = []

@@ -715,14 +716,14 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

715defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

716defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

716defined (PParams _ _ ds) = concatMap defined ds

717defined (PParams _ _ ds) = concatMap defined ds

717defined (PNamespace _ ds) = concatMap defined ds

718defined (PNamespace _ ds) = concatMap defined ds

718−defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

719+defined (PRecord _ _ _ n _ _ _ (Just c) _ _) = [n, c]

719defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

720defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

720defined (PInstance _ _ _ _ _ _ _ _) = []

721defined (PInstance _ _ _ _ _ _ _ _) = []

721defined (PDSL n _) = [n]

722defined (PDSL n _) = [n]

722defined (PSyntax _ _) = []

723defined (PSyntax _ _) = []

723defined (PMutual _ ds) = concatMap defined ds

724defined (PMutual _ ds) = concatMap defined ds

724defined (PDirective _) = []

725defined (PDirective _) = []

725−--defined _ = []

726+defined _ = []

726

727

727updateN :: [(Name, Name)] -> Name -> Name

728updateN :: [(Name, Name)] -> Name -> Name

728updateN ns n | Just n' <- lookup n ns = n'

729updateN ns n | Just n' <- lookup n ns = n'

src/Idris/DeepSeq.hs+2−2

@@ -144,11 +144,11 @@ instance (NFData t) => NFData (PDecl' t) where

144 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

145 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

146 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

147− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

147+ rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

148 = rnf x1 `seq`

149 rnf x2 `seq`

150 rnf x3 `seq`

151− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

151+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` x10 `seq` ()

152 rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)

153 = rnf x1 `seq`

154 rnf x2 `seq`

src/Idris/Elab/Record.hs+53−14

@@ -17,6 +17,7 @@ import Idris.PartialEval

17import Idris.DeepSeq

18import Idris.Output (iputStrLn, pshow, iWarn)

19import IRTS.Lang

20+import Idris.ParseHelpers (opChars)

21import Idris.Elab.Type

22import Idris.Elab.Type

22import Idris.Elab.Data

23import Idris.Elab.Data

@@ -51,9 +52,15 @@ import Data.List.Split (splitOn)

51import Util.Pretty(pretty, text)

52import Util.Pretty(pretty, text)

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

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

54− PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Name -> PTerm -> Idris ()

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

55−elabRecord info syn doc fc tyn ty opts cdoc cn 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'

56− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

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

57 -- TODO think: something more in info?

64 -- TODO think: something more in info?

58 cty' <- implicit info syn cn cty_in

65 cty' <- implicit info syn cn cty_in

59 i <- getIState

66 i <- getIState

@@ -94,21 +101,53 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

94 ptys

101 ptys

102

96 -- Generate projection functions

103 -- Generate projection functions

97− proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

104+ proj_decls <- mapM (mkProj recty_in substs cimp cn) (zip ptys [0..])

98 logLvl 3 $ show proj_decls

105 logLvl 3 $ show proj_decls

99 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

106 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

100 let implBinds = getImplB id cty'

107 let implBinds = getImplB id cty'

101−

102− -- Generate update functions

103− update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls

104− (getFieldNames cty')

105− implBinds (length nonImp)) (zip nonImp [0..])

106 mapM_ (rec_elabDecl info EAll info) (concat proj_decls)

108 mapM_ (rec_elabDecl info EAll info) (concat proj_decls)

109+ -- Generate update functions

110+ when (Codata `notElem` opts)

111+ (do update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls

112+ (getFieldNames cty')

113+ implBinds (length nonImp) cn) (zip nonImp [0..])

107− logLvl 3 $ show update_decls

114+ logLvl 3 $ show update_decls

108− mapM_ (tryElabDecl info) (update_decls)

115+ mapM_ (tryElabDecl info) (update_decls))

109 where

116 where

110-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

117-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

111−

118+ customizeConstructor :: [(Name, Plicity)] -> PTerm -> Idris PTerm

119+ customizeConstructor [] t = return t

120+ customizeConstructor ns t = cc ns t

121+ where

122+ cc names (PPi _ n t t')

123+ | Just p <- lookup n names = do r <- cc (deleteAssoc n names) t'

124+ return $ PPi p n t r

125+ | otherwise = tclift $ tfail (At fc (Elaborating recString tyn (Msg ("Argument " ++ show n ++ " missing."))))

126+ where

127+ deleteAssoc :: Eq a => a -> [(a, b)] -> [(a, b)]

128+ deleteAssoc y (x@(z,_) : xs)

129+ | z == y = xs

130+ | otherwise = x : (deleteAssoc y xs)

131+ deleteAssoc _ [] = []

132+ cc [] t = return t

133+ cc _ _ = tclift $ tfail (At fc (Elaborating recString tyn (Msg ("Not the right of arguments to constructor. You must mention either all or none."))))

134+

135+ recString = (if Codata `elem` opts then "co" else "") ++ "record "

136+

137+ generateConsNameOp :: Idris Name

138+ generateConsNameOp = generateConsName $ sUN "Mk_Operator_Record0"

139+

140+ generateConsName :: Name -> Idris Name

141+ generateConsName n = do i <- getIState

142+ case lookupTyNameExact (expandNS syn n) (tt_ctxt i) of

143+ Just _ -> generateConsName (nextName n)

144+ Nothing -> return n

145+

146+ isOp :: Name -> Bool

147+ isOp (UN t) = foldr (||) False (map (\x -> x `elem` opChars) (str t))

148+ isOp (NS n _) = isOp n

149+ isOp _ = True

150+

112 isNonImp (PExp _ _ _ _, a) = Just a

151 isNonImp (PExp _ _ _ _, a) = Just a

113 isNonImp _ = Nothing

152 isNonImp _ = Nothing

114

153

@@ -182,7 +221,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

182 mkType (MN i n) = sMN i ("set_" ++ str n)

221 mkType (MN i n) = sMN i ("set_" ++ str n)

183 mkType (NS n s) = NS (mkType n) s

222 mkType (NS n s) = NS (mkType n) s

184

223

185− mkProj recty substs cimp ((pn_in, pty), pos)

224+ mkProj recty substs cimp cn ((pn_in, pty), pos)

186 = do let pn = expandNS syn pn_in -- projection name

225 = do let pn = expandNS syn pn_in -- projection name

187 -- use pn_in in the indices, consistently, to avoid clash

226 -- use pn_in in the indices, consistently, to avoid clash

188 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

227 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn

@@ -204,7 +243,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

204 -- If the 'pty' we're updating includes anything in 'substs', we're

243 -- If the 'pty' we're updating includes anything in 'substs', we're

205 -- updating the type as well, so use recty', otherwise just use

244 -- updating the type as well, so use recty', otherwise just use

206 -- recty

245 -- recty

207− mkUpdate recty inames extras fnames k num ((pn, pty), pos)

246+ mkUpdate recty inames extras fnames k num cn ((pn, pty), pos)

208 = do let setname = expandNS syn $ mkType pn

247 = do let setname = expandNS syn $ mkType pn

209 let valname = sMN 0 "updateval"

248 let valname = sMN 0 "updateval"

210 let pn_out = sMN 0 (show pn ++ "_out")

249 let pn_out = sMN 0 (show pn ++ "_out")

src/Idris/ElabDecls.hs+2−2

@@ -236,10 +236,10 @@ elabDecl' what info (PClass doc s f cs n ps pdocs ds)

236elabDecl' what info (PInstance s f cs n ps t expn ds)

237 = do iLOG $ "Elaborating instance " ++ show n

238 elabInstance info s what f cs n ps t expn ds

239−elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

239+elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn args cty)

240 | what /= ETypes

241 = do iLOG $ "Elaborating record " ++ show tyn

242− elabRecord info s doc f tyn ty opts cdoc cn cty

242+ elabRecord info s doc f tyn ty opts cdoc cn args cty

243 | otherwise

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

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

src/Idris/IBC.hs+4−2

@@ -1201,7 +1201,7 @@ instance (Binary t) => Binary (PDecl' t) where

1201 PNamespace x1 x2 -> do putWord8 5

1202 put x1

1203 put x2

1204− PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->

1204+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

1205 do putWord8 6

1206 put x1

1207 put x2

@@ -1212,6 +1212,7 @@ instance (Binary t) => Binary (PDecl' t) where

1212 put x7

1213 put x8

1214 put x9

1215+ put x10

1215 PClass x1 x2 x3 x4 x5 x6 x7 x8

1216 PClass x1 x2 x3 x4 x5 x6 x7 x8

1216 -> do putWord8 7

1217 -> do putWord8 7

1217 put x1

1218 put x1

@@ -1292,7 +1293,8 @@ instance (Binary t) => Binary (PDecl' t) where

1292 x7 <- get

1293 x7 <- get

1293 x8 <- get

1294 x8 <- get

1294 x9 <- get

1295 x9 <- get

1296+ x10 <- get

1295− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

1297+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

1296 7 -> do x1 <- get

1298 7 -> do x1 <- get

1297 x2 <- get

1299 x2 <- get

1298 x3 <- get

1300 x3 <- get

src/Idris/ParseData.hs+125−9

@@ -37,6 +37,9 @@ import qualified Data.ByteString.UTF8 as UTF8

38import Debug.Trace

40+type Docs = Docstring (Either Err PTerm)

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

42+

40{- |Parses a record type declaration

43{- |Parses a record type declaration

41Record ::=

44Record ::=

42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

45 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

@@ -50,23 +53,29 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

50 | (n, d) <- argDocs ]

53 | (n, d) <- argDocs ]

51 acc <- optional accessibility

54 acc <- optional accessibility

52 opts <- dataOpts []

55 opts <- dataOpts []

53− reserved "record"

56+ co <- recordI

54− return (doc', argDocs', acc, opts))

57+ return (doc', argDocs', acc, opts ++ co))

55 fc <- getFC

58 fc <- getFC

56− tyn_in <- fnName

59+ tyn_in <- fnName

57− lchar ':'

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

58− ty <- typeExpr (allowImp syn)

61+ let ty = recordTypeConstructor tys

62+ let ty' = withoutNames ty

59 let tyn = expandNS syn tyn_in

63 let tyn = expandNS syn tyn_in

60− reserved "where"

61− (cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)

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

65+ case cn of

62− accData acc tyn [cn]

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

67+ Nothing -> return ()

63 let rsyn = syn { syn_namespace = show (nsroot tyn) :

68 let rsyn = syn { syn_namespace = show (nsroot tyn) :

64 syn_namespace syn }

69 syn_namespace syn }

65 let fns = getRecNames rsyn cty

70 let fns = getRecNames rsyn cty

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

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

67− return $ PRecord doc rsyn fc tyn ty opts cdoc cn cty

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

68 <?> "record type declaration"

73 <?> "record type declaration"

69 where

74 where

75+ withoutNames :: PTerm -> PTerm

76+ withoutNames (PPi p _ t sc) = PPi p (sUN "__pi_arg") t (withoutNames sc)

77+ withoutNames t = t

78+

70 getRecNames :: SyntaxInfo -> PTerm -> [Name]

79 getRecNames :: SyntaxInfo -> PTerm -> [Name]

71 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

80 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

72 ++ getRecNames syn sc

81 ++ getRecNames syn sc

@@ -76,6 +85,109 @@ record syn = do (doc, argDocs, acc, opts) <- try (do

76 toFreeze (Just Frozen) = Just Hidden

85 toFreeze (Just Frozen) = Just Hidden

77 toFreeze x = x

86 toFreeze x = x

88+ recordTypeConstructor :: [(Name, Plicity, PTerm)] -> PTerm

89+ recordTypeConstructor ((n, p, t) : rest) = PPi p n t (recordTypeConstructor rest)

90+ recordTypeConstructor [] = PType

91+

92+ -- Greatly inspired by ziman (https://github.com/ziman)

93+ agdaStyleBody :: SyntaxInfo -> Name -> PTerm -> IdrisParser RecordConstructor

94+ agdaStyleBody syn tyn tyc = do

95+ ist <- get

96+ fc <- getFC

97+

98+ fields <- many . indented $ field

99+

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

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

102+ let (n, args) = maybePair c

103+ return (n, mList args)

104+

105+ let constructorDoc' = annotate syn ist constructorDoc

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

107+ target = PApp fc (PRef fc tyn) (getParams fc tyc)

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

109+ constructorType' = replaceTarget constructorType (allImpl tyc)

110+

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

112+ where

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

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

115+ maybePair Nothing = (Nothing, Nothing)

116+

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

118+ mList (Just xs) = xs

119+ 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+

126+ allImpl :: PTerm -> PTerm

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

128+ allImpl t = t

129+

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

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

132+ n <- fnName

133+ lchar ':'

134+ t <- typeExpr (allowImp syn)

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

136+

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

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

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

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

141+ argName <- fnName

142+ plicity <- endPlicity p

143+ return (argName, plicity))

144+ lchar ')'

145+ return args)

146+ return (n, args)

147+

148+ endPlicity :: Maybe Char -> IdrisParser Plicity

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

150+ return impl

151+ endPlicity Nothing = return expl

152+

153+ mkConstructorType :: [(Name, PTerm, Plicity)] -> PTerm -> PTerm

154+ mkConstructorType ((n, t, p) : rest) t' = PPi p (nsroot n) t (mkConstructorType rest t')

155+ mkConstructorType [] t = t

156+

157+ getParams :: FC -> PTerm -> [PArg]

158+ getParams fc (PPi (Exp os _ _) n t ts) = (PExp 0 os n $ PRef fc n) : getParams fc ts

159+ getParams fc (PPi (Imp os _ _ _) n t ts) = (PImp 0 False os n $ PRef fc n) : getParams fc ts

160+ getParams _ _ = []

161+

162+ annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

163+ annotate syn ist = annotCode $ tryFullExpr syn ist

164+

165+ replaceTarget :: PTerm -> PTerm -> PTerm

166+ replaceTarget trg (PPi p n t ts) = PPi p n t (replaceTarget trg ts)

167+ replaceTarget trg _ = trg

168+

169+recordTypeParameter :: SyntaxInfo -> IdrisParser (Name, Plicity, PTerm)

170+recordTypeParameter syn =

171+ (do lchar '('

172+ (n, pt) <- (namedTy syn <|> onlyName syn)

173+ lchar ')'

174+ return (n, expl, pt))

175+ <|>

176+ (do (n, pt) <- onlyName syn

177+ return (n, expl, pt))

178+

179+ where

180+ namedTy :: SyntaxInfo -> IdrisParser (Name, PTerm)

181+ namedTy syn =

182+ do tyn <- fnName

183+ lchar ':'

184+ ty <- typeExpr (allowImp syn)

185+ return (tyn, ty)

186+ onlyName :: SyntaxInfo -> IdrisParser (Name, PTerm)

187+ onlyName syn =

188+ do n <- fnName

189+ return (n, PType)

190+

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

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

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

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

81-}

193-}

@@ -83,6 +195,10 @@ dataI :: IdrisParser DataOpts

83dataI = do reserved "data"; return []

195dataI = do reserved "data"; return []

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

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

197

198+recordI :: IdrisParser DataOpts

199+recordI = do reserved "record"; return []

200+ <|> do reserved "corecord"; return [Codata]

201+

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

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

87DefaultEliminator ::= 'noelim'?

203DefaultEliminator ::= 'noelim'?

88 -}

204 -}

src/Idris/ParseHelpers.hs+2−2

@@ -226,14 +226,14 @@ idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved

226 where _styleName = "Idris"

227 _styleStart = satisfy isAlpha

228 _styleLetter = satisfy isAlphaNum <|> oneOf "_'."

229− _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "Type",

229+ _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "corecord", "Type",

230 "do", "dsl", "import", "impossible",

231 "case", "of", "total", "partial", "mutual",

232 "infix", "infixl", "infixr", "rewrite",

233 "where", "with", "syntax", "proof", "postulate",

234 "using", "namespace", "class", "instance", "parameters",

235 "public", "private", "abstract", "implicit",

236− "quoteGoal"]

236+ "quoteGoal", "constructor"]

237

238char :: MonadicParsing m => Char -> m Char

239char = Chr.char