3b36802 · Idris-dev · git.iko.soy

src/Core/CoreParser.hs+1−1

compare with master

unifiedsplit

@@ -19,7 +19,7 @@ idrisDef = haskellDef {

19 opLetter = iOpLetter,

20 identLetter = identLetter haskellDef <|> lchar '.',

21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

22− reservedNames = ["let", "in", "data", "Set",

22+ reservedNames = ["let", "in", "data", "record", "Set",

23 "do", "dsl", "import", "impossible",

24 "case", "of",

25 "infix", "infixl", "infixr", "prefix",

src/Idris/AbsSyntax.hs+1

@@ -361,6 +361,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration

361 | PData SyntaxInfo FC (PData' t) -- data declaration

362 | PParams FC [(Name, t)] [PDecl' t] -- params block

363 | PNamespace String [PDecl' t] -- new namespace

364+ | PRecord SyntaxInfo FC Name t Name t -- record declaration

364 | PClass SyntaxInfo FC

365 | PClass SyntaxInfo FC

365 [t] -- constraints

366 [t] -- constraints

366 Name

367 Name

src/Idris/ElabDecls.hs+8

@@ -79,6 +79,11 @@ elabData info syn fc (PDatadecl n t_in dcons)

79 collapseCons n cons

80 updateContext (addDatatype (Data n ttag cty cons))

81

82+elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

83+ PTerm -> Name -> PTerm -> Idris ()

84+elabRecord info syn fc tyn ty cn cty

85+ = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

86+

82elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

87elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)

83elabCon info syn (n, t_in, fc)

88elabCon info syn (n, t_in, fc)

84 = do checkUndefined fc n

89 = do checkUndefined fc n

@@ -609,6 +614,9 @@ elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show

609elabDecl' info (PInstance s f cs n ps t ds)

614elabDecl' info (PInstance s f cs n ps t ds)

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

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

611 elabInstance info s f cs n ps t ds

616 elabInstance info s f cs n ps t ds

617+elabDecl' info (PRecord s f tyn ty cn cty)

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

619+ elabRecord info s f tyn ty cn cty

612elabDecl' info (PDirective i) = i

620elabDecl' info (PDirective i) = i

613

621

614elabCaseBlock info d@(PClauses f o n ps)

622elabCaseBlock info d@(PClauses f o n ps)

src/Idris/Parser.hs+12

@@ -330,6 +330,7 @@ pDecl' syn

330 = try pFixity

331 <|> pFunDecl' syn

332 <|> try (pData syn)

333+ <|> try (pRecord syn)

333 <|> pSyntaxDecl syn

334 <|> pSyntaxDecl syn

334

335

335pSyntaxDecl :: SyntaxInfo -> IParser PDecl

336pSyntaxDecl :: SyntaxInfo -> IParser PDecl

@@ -896,6 +897,17 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)

896 mapM_ (\n -> addAcc n (Just Hidden)) ns

897 mapM_ (\n -> addAcc n (Just Hidden)) ns

897accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

898accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

898

899

900+pRecord :: SyntaxInfo -> IParser PDecl

901+pRecord syn = try (do acc <- pAccessibility

902+ reserved "record"; fc <- pfc

903+ tyn_in <- pfName; ty <- pTSig syn

904+ let tyn = expandNS syn tyn_in

905+ reserved "where"

906+ (cn, cty, _) <- pConstructor syn

907+ pTerminator

908+ accData acc tyn [cn]

909+ return $ PRecord syn fc tyn ty cn cty)

910+

899pData :: SyntaxInfo -> IParser PDecl

911pData :: SyntaxInfo -> IParser PDecl

900pData syn = try (do acc <- pAccessibility

912pData syn = try (do acc <- pAccessibility

901 reserved "data"; fc <- pfc

913 reserved "data"; fc <- pfc