@@ -605,25 +605,45 @@ FieldType ::=
605605@
606606-}
607607recordType :: SyntaxInfo -> IdrisParser PTerm
608−recordType syn
609− = do reserved "record"
608+recordType syn =
609+ do reserved "record"
610610 lchar '{'
611− fields <- sepBy1 fieldType (lchar ',')
611+ fgs <- fieldGetOrSet
612612 lchar '}'
613613 fc <- getFC
614614 rec <- optional (simpleExpr syn)
615− case rec of
616− Nothing ->
617− return (PLam (sMN 0 "fldx") Placeholder
618− (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
619− Just v -> return (applyAll fc fields v)
615+ case fgs of
616+ Left fields ->
617+ case rec of
618+ Nothing ->
619+ return (PLam (sMN 0 "fldx") Placeholder
620+ (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
621+ Just v -> return (applyAll fc fields v)
622+ Right fields ->
623+ case rec of
624+ Nothing ->
625+ return (PLam (sMN 0 "fldx") Placeholder
626+ (getAll fc (reverse fields)
627+ (PRef fc (sMN 0 "fldx"))))
628+ Just v -> return (getAll fc (reverse fields) v)
629+
620630 <?> "record setting expression"
621− where fieldType :: IdrisParser ([Name], PTerm)
622− fieldType = do n <- sepBy1 fnName (symbol "->")
623− lchar '='
624− e <- expr syn
625− return (n, e)
626− <?> "field setter"
631+ where fieldSet :: IdrisParser ([Name], PTerm)
632+ fieldSet = do ns <- fieldGet
633+ lchar '='
634+ e <- expr syn
635+ return (ns, e)
636+ <?> "field setter"
637+
638+ fieldGet :: IdrisParser [Name]
639+ fieldGet = sepBy1 fnName (symbol "->")
640+
641+ fieldGetOrSet :: IdrisParser (Either [([Name], PTerm)] [Name])
642+ fieldGetOrSet = try (do fs <- sepBy1 fieldSet (lchar ',')
643+ return (Left fs))
644+ <|> do f <- fieldGet
645+ return (Right f)
646+
627647 applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm
628648 applyAll fc [] x = x
629649 applyAll fc ((ns, e) : es) x
@@ -636,6 +656,11 @@ recordType syn
636656 [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),
637657 pexp get]
638658
659+ getAll :: FC -> [Name] -> PTerm -> PTerm
660+ getAll fc [n] e = PApp fc (PRef fc n) [pexp e]
661+ getAll fc (n:ns) e = PApp fc (PRef fc n) [pexp (getAll fc ns e)]
662+
663+
639664-- | Creates setters for record types on necessary functions
640665mkType :: Name -> Name
641666mkType (UN n) = sUN ("set_" ++ str n)