@@ -618,16 +618,23 @@ recordType syn
618 (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
618 (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
619 Just v -> return (applyAll fc fields v)
619 Just v -> return (applyAll fc fields v)
620 <?> "record setting expression"
620 <?> "record setting expression"
621− where fieldType :: IdrisParser (Name, PTerm)
621+ where fieldType :: IdrisParser ([Name], PTerm)
622− fieldType = do n <- fnName
622+ fieldType = do n <- sepBy1 fnName (symbol "->")
623 lchar '='
623 lchar '='
624 e <- expr syn
624 e <- expr syn
625 return (n, e)
625 return (n, e)
626 <?> "field setter"
626 <?> "field setter"
627− applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
627+ applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm
628 applyAll fc [] x = x
628 applyAll fc [] x = x
629− applyAll fc ((n, e) : es) x
629+ applyAll fc ((ns, e) : es) x
630+ = applyAll fc es (doUpdate fc ns e x)
632+ doUpdate fc [n] e get
630− = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
633+ = PApp fc (PRef fc (mkType n)) [pexp e, pexp get]
634+ doUpdate fc (n : ns) e get
635+ = PApp fc (PRef fc (mkType n))
636+ [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),
632-- | Creates setters for record types on necessary functions
639-- | Creates setters for record types on necessary functions
633mkType :: Name -> Name
640mkType :: Name -> Name