git.iko.soy/Idris-dev
on master help sign in
Record update functions
7826c0eEdwin Brady
lib/network/cgi.idr+20−37
compare with master
unifiedsplit
@@ -6,36 +6,19 @@ public
6Vars : Set
6Vars : Set
7Vars = List (String, String)
7Vars = List (String, String)
8
8
9+record CGIInfo : Set where
9−data CGIInfo = CGISt Vars -- GET
10+ CGISt : (GET : Vars) ->
10− Vars -- POST
11+ (POST : Vars) ->
11− Vars -- Cookies
12+ (Cookies : Vars) ->
12− String -- User agent
13+ (UserAgent : String) ->
13− String -- headers
14+ (Headers : String) ->
14− String -- output
15+ (Output : String) -> CGIInfo
15−
16−get_GET : CGIInfo -> Vars
17−get_GET (CGISt g _ _ _ _ _) = g
18−
19−get_POST : CGIInfo -> Vars
20−get_POST (CGISt _ p _ _ _ _) = p
21−
22−get_Cookies : CGIInfo -> Vars
23−get_Cookies (CGISt _ _ c _ _ _) = c
24−
25−get_UAgent : CGIInfo -> String
26−get_UAgent (CGISt _ _ _ a _ _) = a
27−
28−get_Headers : CGIInfo -> String
29−get_Headers (CGISt _ _ _ _ h _) = h
30−
31−get_Output : CGIInfo -> String
32−get_Output (CGISt _ _ _ _ _ o) = o
33
16
34add_Headers : String -> CGIInfo -> CGIInfo
17add_Headers : String -> CGIInfo -> CGIInfo
35−add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o
18+add_Headers str st = set_Headers (Headers st ++ str) st
36
19
37add_Output : String -> CGIInfo -> CGIInfo
20add_Output : String -> CGIInfo -> CGIInfo
38−add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str)
21+add_Output str st = set_Output (Output st ++ str) st
39
22
40abstract
23abstract
41data CGI : Set -> Set where
24data CGI : Set -> Set where
@@ -70,17 +53,17 @@ output s = do i <- getInfo
70abstract
53abstract
71queryVars : CGI Vars
54queryVars : CGI Vars
72queryVars = do i <- getInfo
55queryVars = do i <- getInfo
73− return (get_GET i)
56+ return (GET i)
74
57
75abstract
58abstract
76postVars : CGI Vars
59postVars : CGI Vars
77postVars = do i <- getInfo
60postVars = do i <- getInfo
78− return (get_POST i)
61+ return (POST i)
79
62
80abstract
63abstract
81cookieVars : CGI Vars
64cookieVars : CGI Vars
82cookieVars = do i <- getInfo
65cookieVars = do i <- getInfo
83− return (get_Cookies i)
66+ return (Cookies i)
84
67
85abstract
68abstract
86queryVar : String -> CGI (Maybe String)
69queryVar : String -> CGI (Maybe String)
@@ -89,11 +72,11 @@ queryVar x = do vs <- queryVars
89
72
90getOutput : CGI String
73getOutput : CGI String
91getOutput = do i <- getInfo
74getOutput = do i <- getInfo
92− return (get_Output i)
75+ return (Output i)
93
76
94getHeaders : CGI String
77getHeaders : CGI String
95getHeaders = do i <- getInfo
78getHeaders = do i <- getInfo
96− return (get_Headers i)
79+ return (Headers i)
97
80
98abstract
81abstract
99flushHeaders : CGI ()
82flushHeaders : CGI ()
@@ -134,11 +117,11 @@ runCGI prog = do
134 let post_vars = getVars ['&'] content
117 let post_vars = getVars ['&'] content
135 let cookies = getVars [';'] cookie
118 let cookies = getVars [';'] cookie
136
119
137− p <- getAction prog (CGISt get_vars post_vars cookies agent
120+ (v, st) <- getAction prog (CGISt get_vars post_vars cookies agent
138− "Content-type: text/html\n"
121+ "Content-type: text/html\n"
139− "")
122+ "")
140− putStrLn (get_Headers (snd p))
123+ putStrLn (Headers st)
141− putStr (get_Output (snd p))
124+ putStr (Output st)
142− return (fst p)
125+ return v
143
126
144
127
src/Idris/ElabDecls.hs+32−3
@@ -96,15 +96,20 @@ elabRecord info syn fc tyn ty cn cty
96 cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
96 cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
97 [imps] -> return imps
97 [imps] -> return imps
98 let ptys = getProjs [] (renameBs cimp cty)
98 let ptys = getProjs [] (renameBs cimp cty)
99+ let ptys_u = getProjs [] cty
99 let recty = getRecTy cty
100 let recty = getRecTy cty
100 logLvl 6 $ show (recty, ptys)
101 logLvl 6 $ show (recty, ptys)
101 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
102 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
102 [pexp (PRef fc rec)])) ptys
103 [pexp (PRef fc rec)])) ptys
103− let ptpos = zip ptys [0..]
104+ proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
104− decls <- mapM (mkProj recty substs cimp) ptpos
105+ let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
106+ update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])
105− mapM_ (elabDecl info) (concat decls)
107+ mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))
106 where
108 where
107
109
110+ isNonImp (PExp _ _ _, a) = Just a
111+ isNonImp _ = Nothing
112+
108 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
113 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
109 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
114 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
110 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
115 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
@@ -126,6 +131,10 @@ elabRecord info syn fc tyn ty cn cty
126 mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
131 mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
127 mkImp (NS n s) = NS (mkImp n) s
132 mkImp (NS n s) = NS (mkImp n) s
128
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
137+
129 mkProj recty substs cimp ((pn, pty), pos)
138 mkProj recty substs cimp ((pn, pty), pos)
130 = do let pfnTy = PTy defaultSyntax fc [] pn
139 = do let pfnTy = PTy defaultSyntax fc [] pn
131 (PPi expl rec recty
140 (PPi expl rec recty
@@ -143,6 +152,26 @@ elabRecord info syn fc tyn ty cn cty
143
152
144 implicitise (pa, t) = pa { getTm = t }
153 implicitise (pa, t) = pa { getTm = t }
145
154
155+ mkUpdate recty num ((pn, pty), pos)
156+ = do let setname = mkSet pn
157+ let valname = MN 0 "updateval"
158+ let pfnTy = PTy defaultSyntax fc [] setname
159+ (PPi expl pn pty
160+ (PPi expl rec recty recty))
161+ let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
162+ let lhsArgs = pls
163+ let rhsArgs = take pos pls ++ (PRef fc valname) :
164+ drop (pos + 1) pls
165+ let before = pos
166+ let pclause = PClause setname (PApp fc (PRef fc setname)
167+ [pexp (PRef fc valname),
168+ pexp (PApp fc (PRef fc cn)
169+ (map pexp lhsArgs))])
170+ []
171+ (PApp fc (PRef fc cn)
172+ (map pexp rhsArgs)) []
173+ return [pfnTy, PClauses fc [] setname [pclause]]
174+
146elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)
175elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)
147elabCon info syn tn (n, t_in, fc)
176elabCon info syn tn (n, t_in, fc)
148 = do checkUndefined fc n
177 = do checkUndefined fc n