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

lib/network/cgi.idr+2−2

compare with master

unifiedsplit

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

15 (Output : String) -> CGIInfo

16

17add_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

19

20add_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

22

23abstract

24data CGI : Set -> Set where

src/Idris/ElabDecls.hs+1−1

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

133

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

135 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

137

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

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

src/Idris/Parser.hs+23

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

535

536pNoExtExpr syn =

537 try (pApp syn)

538+ <|> pRecordSet syn

538 <|> try (pSimpleExpr syn)

539 <|> try (pSimpleExpr syn)

539 <|> pLambda syn

540 <|> pLambda syn

540 <|> pLet syn

541 <|> pLet syn

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

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

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

762 return (pconst e)

763 return (pconst e)

763

764

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+

764pTSig syn = do lchar ':'

787pTSig syn = do lchar ':'

765 cs <- pConstList syn

788 cs <- pConstList syn

766 sc <- pExpr syn

789 sc <- pExpr syn