@@ -37,6 +37,9 @@ import qualified Data.ByteString.UTF8 as UTF8
3737
3838import Debug.Trace
3939
40+type Docs = Docstring (Either Err PTerm)
41+type RecordConstructor = (Docs, [(Name, Docs)], Maybe Name, PTerm, [(Name, Plicity)])
42+
4043{- |Parses a record type declaration
4144Record ::=
4245 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
@@ -50,23 +53,29 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
5053 | (n, d) <- argDocs ]
5154 acc <- optional accessibility
5255 opts <- dataOpts []
53− reserved "record"
54− return (doc', argDocs', acc, opts))
56+ co <- recordI
57+ return (doc', argDocs', acc, opts ++ co))
5558 fc <- getFC
56− tyn_in <- fnName
57− lchar ':'
58− ty <- typeExpr (allowImp syn)
59+ tyn_in <- fnName
60+ tys <- manyTill (recordTypeParameter syn) (reserved "where")
61+ let ty = recordTypeConstructor tys
62+ let ty' = withoutNames ty
5963 let tyn = expandNS syn tyn_in
60− reserved "where"
61− (cdoc, cargDocs, cn, cty, _, _) <- indentedBlockS (constructor syn)
62− accData acc tyn [cn]
64+ (cdoc, cargDocs, cn, cty, args) <- indentedBlockS $ agdaStyleBody syn tyn ty
65+ case cn of
66+ Just cn' -> accData acc tyn [cn']
67+ Nothing -> return ()
6368 let rsyn = syn { syn_namespace = show (nsroot tyn) :
6469 syn_namespace syn }
6570 let fns = getRecNames rsyn cty
6671 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
6873 <?> "record type declaration"
6974 where
75+ withoutNames :: PTerm -> PTerm
76+ withoutNames (PPi p _ t sc) = PPi p (sUN "__pi_arg") t (withoutNames sc)
77+ withoutNames t = t
78+
7079 getRecNames :: SyntaxInfo -> PTerm -> [Name]
7180 getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]
7281 ++ getRecNames syn sc
@@ -76,6 +85,109 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
7685 toFreeze (Just Frozen) = Just Hidden
7786 toFreeze x = x
7887
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+
79191{- | Parses data declaration type (normal or codata)
80192DataI ::= 'data' | 'codata';
81193-}
@@ -83,6 +195,10 @@ dataI :: IdrisParser DataOpts
83195dataI = do reserved "data"; return []
84196 <|> do reserved "codata"; return [Codata]
85197
198+recordI :: IdrisParser DataOpts
199+recordI = do reserved "record"; return []
200+ <|> do reserved "corecord"; return [Codata]
201+
86202{- | Parses if a data should not have a default eliminator
87203DefaultEliminator ::= 'noelim'?
88204 -}