git.iko.soy/Idris-dev
on master help sign in
Record syntax (but no magic yet...)
commit3b36802743ec641eb66298a2818833e3ea11c326 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateWed 18 Jan 2012, 14:35 (15 years ago) parent3b13341
4 files changed+22−1
compare with master
unifiedsplit
src/Core/CoreParser.hs+1−1 src/Idris/AbsSyntax.hs+1 src/Idris/ElabDecls.hs+8 src/Idris/Parser.hs+12
src/Core/CoreParser.hs+1−1
@@ -19,7 +19,7 @@ idrisDef = haskellDef {
1919 opLetter = iOpLetter,
2020 identLetter = identLetter haskellDef <|> lchar '.',
2121 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],
22− reservedNames = ["let", "in", "data", "Set",
22+ reservedNames = ["let", "in", "data", "record", "Set",
2323 "do", "dsl", "import", "impossible",
2424 "case", "of",
2525 "infix", "infixl", "infixr", "prefix",
src/Idris/AbsSyntax.hs+1
@@ -361,6 +361,7 @@ data PDecl' t = PFix FC Fixity [String] -- fixity declaration
361361 | PData SyntaxInfo FC (PData' t) -- data declaration
362362 | PParams FC [(Name, t)] [PDecl' t] -- params block
363363 | PNamespace String [PDecl' t] -- new namespace
364+ | PRecord SyntaxInfo FC Name t Name t -- record declaration
364365 | PClass SyntaxInfo FC
365366 [t] -- constraints
366367 Name
src/Idris/ElabDecls.hs+8
@@ -79,6 +79,11 @@ elabData info syn fc (PDatadecl n t_in dcons)
7979 collapseCons n cons
8080 updateContext (addDatatype (Data n ttag cty cons))
8181
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+
8287elabCon :: ElabInfo -> SyntaxInfo -> (Name, PTerm, FC) -> Idris (Name, Type)
8388elabCon info syn (n, t_in, fc)
8489 = do checkUndefined fc n
@@ -609,6 +614,9 @@ elabDecl' info (PClass s f cs n ps ds) = do iLOG $ "Elaborating class " ++ show
609614elabDecl' info (PInstance s f cs n ps t ds)
610615 = do iLOG $ "Elaborating instance " ++ show n
611616 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
612620elabDecl' info (PDirective i) = i
613621
614622elabCaseBlock info d@(PClauses f o n ps)
src/Idris/Parser.hs+12
@@ -330,6 +330,7 @@ pDecl' syn
330330 = try pFixity
331331 <|> pFunDecl' syn
332332 <|> try (pData syn)
333+ <|> try (pRecord syn)
333334 <|> pSyntaxDecl syn
334335
335336pSyntaxDecl :: SyntaxInfo -> IParser PDecl
@@ -896,6 +897,17 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)
896897 mapM_ (\n -> addAcc n (Just Hidden)) ns
897898accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns
898899
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+
899911pData :: SyntaxInfo -> IParser PDecl
900912pData syn = try (do acc <- pAccessibility
901913 reserved "data"; fc <- pfc