4cd20b3 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Record update syntax

{ field = val } is a function which updates the field. So { field = val } rec update the field in record 'rec'. (This is backwards from Haskell, firstly because the other way round would conflict with implicit argument syntax, and secondly because it means record updates can be partially applied)

commit4cd20b3f3bfa9f337876bc0e4229cd159ca93bf5 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 27 Jan 2012, 15:12 (15 years ago) parent7826c0e

3 files changed+26−3

compare with master

unifiedsplit

lib/network/cgi.idr+2−2 src/Idris/ElabDecls.hs+1−1 src/Idris/Parser.hs+23

lib/network/cgi.idr+2−2

@@ -15,10 +15,10 @@ record CGIInfo : Set where

1515 (Output : String) -> CGIInfo

1616

1717add_Headers : String -> CGIInfo -> CGIInfo

18−add_Headers str st = set_Headers (Headers st ++ str) st

18+add_Headers str st = { Headers = Headers st ++ str } st

1919

2020add_Output : String -> CGIInfo -> CGIInfo

21−add_Output str st = set_Output (Output st ++ str) st

21+add_Output str st = { Output = Output st ++ str } st

2222

2323abstract

2424data CGI : Set -> Set where

src/Idris/ElabDecls.hs+1−1

@@ -133,7 +133,7 @@ elabRecord info syn fc tyn ty cn cty

133133

134134 mkSet (UN n) = UN ("set_" ++ n)

135135 mkSet (MN 0 n) = MN 0 ("set_" ++ n)

136− mkSet (NS n s) = NS (mkImp n) s

136+ mkSet (NS n s) = NS (mkSet n) s

137137

138138 mkProj recty substs cimp ((pn, pty), pos)

139139 = do let pfnTy = PTy defaultSyntax fc [] pn

src/Idris/Parser.hs+23

@@ -535,6 +535,7 @@ pSimpleExtExpr syn = do i <- getState

535535

536536pNoExtExpr syn =

537537 try (pApp syn)

538+ <|> pRecordSet syn

538539 <|> try (pSimpleExpr syn)

539540 <|> pLambda syn

540541 <|> pLet syn

@@ -761,6 +762,28 @@ pImplicitArg syn = do lchar '{'; n <- pName

761762pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"

762763 return (pconst e)

763764

765+pRecordSet syn

766+ = do lchar '{'

767+ fields <- sepBy1 pFieldSet (lchar ',')

768+ lchar '}'

769+ fc <- pfc

770+ rec <- option Nothing (do e <- pSimpleExpr syn; return (Just e))

771+ case rec of

772+ Nothing ->

773+ return (PLam (MN 0 "fldx") Placeholder

774+ (applyAll fc fields (PRef fc (MN 0 "fldx"))))

775+ Just v -> return (applyAll fc fields v)

776+ where pFieldSet = do n <- pfName; lchar '='

777+ e <- pExpr syn

778+ return (n, e)

779+ applyAll fc [] x = x

780+ applyAll fc ((n, e) : es) x

781+ = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])

782+

783+ mkSet (UN n) = UN ("set_" ++ n)

784+ mkSet (MN 0 n) = MN 0 ("set_" ++ n)

785+ mkSet (NS n s) = NS (mkSet n) s

786+

764787pTSig syn = do lchar ':'

765788 cs <- pConstList syn

766789 sc <- pExpr syn