02501ef · 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 = { Headers = Headers st ++ str } st

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

19

20add_Output : String -> CGIInfo -> CGIInfo

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

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

22

23abstract

24data CGI : Set -> Set where

src/Idris/AbsSyntax.hs+7

@@ -652,6 +652,13 @@ data SyntaxInfo = Syn { using :: [(Name, PTerm)],

652

653defaultSyntax = Syn [] [] [] [] id False initDSL

654

655+expandNS :: SyntaxInfo -> Name -> Name

656+expandNS syn n@(NS _ _) = n

657+expandNS syn n = case syn_namespace syn of

658+ [] -> n

659+ xs -> NS n xs

660+

661+

655--- Pretty printing declarations and terms

662--- Pretty printing declarations and terms

656

663

657instance Show PTerm where

664instance Show PTerm where

src/Idris/ElabDecls.hs+6−4

@@ -86,7 +86,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

86

87elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

88 PTerm -> Name -> PTerm -> Idris ()

89−elabRecord info syn fc tyn ty cn cty

89+elabRecord info syn_in fc tyn ty cn cty

90 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

91 cty <- implicit syn cn cty

92 i <- get

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

106 update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])

107 mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))

108 where

109+ syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

109

110

110 isNonImp (PExp _ _ _, a) = Just a

111 isNonImp (PExp _ _ _, a) = Just a

111 isNonImp _ = Nothing

112 isNonImp _ = Nothing

@@ -135,8 +136,9 @@ elabRecord info syn fc tyn ty cn cty

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

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

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

137 mkSet (NS n s) = NS (mkSet n) s

137

138

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

139+ mkProj recty substs cimp ((pn_in, pty), pos)

140+ = do let pn = expandNS syn pn_in

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

141+ let pfnTy = PTy defaultSyntax fc [] pn

140 (PPi expl rec recty

142 (PPi expl rec recty

141 (substMatches substs pty))

143 (substMatches substs pty))

142 let pls = repeat Placeholder

144 let pls = repeat Placeholder

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

153 implicitise (pa, t) = pa { getTm = t }

155 implicitise (pa, t) = pa { getTm = t }

154

156

155 mkUpdate recty num ((pn, pty), pos)

157 mkUpdate recty num ((pn, pty), pos)

156− = do let setname = mkSet pn

158+ = do let setname = expandNS syn $ mkSet pn

157 let valname = MN 0 "updateval"

159 let valname = MN 0 "updateval"

158 let pfnTy = PTy defaultSyntax fc [] setname

160 let pfnTy = PTy defaultSyntax fc [] setname

159 (PPi expl pn pty

161 (PPi expl pn pty

src/Idris/Parser.hs+4−8

@@ -444,12 +444,6 @@ pNamespace syn =

444 close_block

445 return [PNamespace n (concat ds)]

446

447−expandNS :: SyntaxInfo -> Name -> Name

448−expandNS syn n@(NS _ _) = n

449−expandNS syn n = case syn_namespace syn of

450− [] -> n

451− xs -> NS n xs

452−

453--------- Fixity ---------

447--------- Fixity ---------

454

448

455pFixity :: IParser PDecl

449pFixity :: IParser PDecl

@@ -763,7 +757,8 @@ pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"

763 return (pconst e)

757 return (pconst e)

764

758

765pRecordSet syn

759pRecordSet syn

760+ = do reserved "record"

766− = do lchar '{'

761+ lchar '{'

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

762 fields <- sepBy1 pFieldSet (lchar ',')

768 lchar '}'

763 lchar '}'

769 fc <- pfc

764 fc <- pfc

@@ -1017,12 +1012,13 @@ bindArgs [] t = t

1017bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)

1012bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)

1018

1013

1019pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1014pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)

1020−pConstructor syn

1015+pConstructor syn

1021 = do cn_in <- pfName; fc <- pfc

1016 = do cn_in <- pfName; fc <- pfc

1022 let cn = expandNS syn cn_in

1017 let cn = expandNS syn cn_in

1023 ty <- pTSig syn

1018 ty <- pTSig syn

1024-- ty' <- implicit syn cn ty

1019-- ty' <- implicit syn cn ty

1025 return (cn, ty, fc)

1020 return (cn, ty, fc)

1021+

1026

1022

1027pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

1023pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)

1028pSimpleCon syn

1024pSimpleCon syn