@@ -38,7 +38,7 @@ import qualified Data.ByteString.UTF8 as UTF8
3838import Debug.Trace
3939
4040type 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)
4242
4343{- |Parses a record type declaration
4444Record ::=
@@ -59,9 +59,8 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
5959 tyn_in <- fnName
6060 tys <- manyTill (recordTypeParameter syn) (reserved "where")
6161 let ty = recordTypeConstructor tys
62− let ty' = withoutNames ty
6362 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
6564 case cn of
6665 Just cn' -> accData acc tyn [cn']
6766 Nothing -> return ()
@@ -69,7 +68,7 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
6968 syn_namespace syn }
7069 let fns = getRecNames rsyn cty
7170 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
7372 <?> "record type declaration"
7473 where
7574 withoutNames :: PTerm -> PTerm
@@ -98,9 +97,8 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
9897 fields <- many . indented $ field
9998
10099 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)
100+ constructorName <- do n <- optional constructor
101+ return n
104102
105103 let constructorDoc' = annotate syn ist constructorDoc
106104 let fieldDocs = [(n, annotate syn ist doc) | (n, _, _, doc, _) <- fields]
@@ -108,7 +106,7 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
108106 constructorType = mkConstructorType [(n, t, p) | (n, t, p, _, _) <- fields] target
109107 constructorType' = replaceTarget constructorType (allImpl tyc)
110108
111− return (constructorDoc', fieldDocs, constructorName, constructorType', args)
109+ return (constructorDoc', fieldDocs, constructorName, constructorType')
112110 where
113111 maybePair :: Maybe (a, b) -> (Maybe a, Maybe b)
114112 maybePair (Just(x, y)) = (Just x, Just y)
@@ -117,11 +115,6 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
117115 mList :: Maybe [a] -> [a]
118116 mList (Just xs) = xs
119117 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)
125118
126119 allImpl :: PTerm -> PTerm
127120 allImpl (PPi _ n t t') = PPi impl n t (allImpl t')
@@ -129,21 +122,23 @@ record syn = do (doc, argDocs, acc, opts) <- try (do
129122
130123 field :: IdrisParser (Name, PTerm, Plicity, Docstring (), [(Name, Docstring ())])
131124 field = do (doc, argDocs) <- option noDocs docComment
125+ c <- optional $ lchar '{'
132126 n <- fnName
133127 lchar ':'
134128 t <- typeExpr (allowImp syn)
135− return (n, t, expl, doc, argDocs)
129+ p <- endPlicity c
130+ return (n, t, p, doc, argDocs)
136131
137− constructor :: IdrisParser (Name, [(Name, Plicity)])
132+ constructor :: IdrisParser Name -- (Name, [(Name, Plicity)])
138133 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)
134+ -- args <- option [] (do lchar '('
135+ -- args <- many (do p <- optional $ lchar '{'
136+ -- argName <- fnName
137+ -- plicity <- endPlicity p
138+ -- return (argName, plicity))
139+ -- lchar ')'
140+ -- return args)
141+ return n
147142
148143 endPlicity :: Maybe Char -> IdrisParser Plicity
149144 endPlicity (Just _) = do lchar '}'