git.iko.soy/Idris-dev
on master help sign in
Record update functions

set_field val record -- updates the field name 'field' to 'val' in 'record'

commit7826c0e2004de5fe3124b5ce1a3f0be95d12af89 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 27 Jan 2012, 14:48 (15 years ago) parent3a4a26b
2 files changed+52−40
compare with master
unifiedsplit
lib/network/cgi.idr+20−37 src/Idris/ElabDecls.hs+32−3
lib/network/cgi.idr+20−37
@@ -6,36 +6,19 @@ public
66Vars : Set
77Vars = List (String, String)
88
9−data CGIInfo = CGISt Vars -- GET
10− Vars -- POST
11− Vars -- Cookies
12− String -- User agent
13− String -- headers
14− String -- output
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
9+record CGIInfo : Set where
10+ CGISt : (GET : Vars) ->
11+ (POST : Vars) ->
12+ (Cookies : Vars) ->
13+ (UserAgent : String) ->
14+ (Headers : String) ->
15+ (Output : String) -> CGIInfo
3316
3417add_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
3619
3720add_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
3922
4023abstract
4124data CGI : Set -> Set where
@@ -70,17 +53,17 @@ output s = do i <- getInfo
7053abstract
7154queryVars : CGI Vars
7255queryVars = do i <- getInfo
73− return (get_GET i)
56+ return (GET i)
7457
7558abstract
7659postVars : CGI Vars
7760postVars = do i <- getInfo
78− return (get_POST i)
61+ return (POST i)
7962
8063abstract
8164cookieVars : CGI Vars
8265cookieVars = do i <- getInfo
83− return (get_Cookies i)
66+ return (Cookies i)
8467
8568abstract
8669queryVar : String -> CGI (Maybe String)
@@ -89,11 +72,11 @@ queryVar x = do vs <- queryVars
8972
9073getOutput : CGI String
9174getOutput = do i <- getInfo
92− return (get_Output i)
75+ return (Output i)
9376
9477getHeaders : CGI String
9578getHeaders = do i <- getInfo
96− return (get_Headers i)
79+ return (Headers i)
9780
9881abstract
9982flushHeaders : CGI ()
@@ -134,11 +117,11 @@ runCGI prog = do
134117 let post_vars = getVars ['&'] content
135118 let cookies = getVars [';'] cookie
136119
137− p <- getAction prog (CGISt get_vars post_vars cookies agent
138− "Content-type: text/html\n"
139− "")
140− putStrLn (get_Headers (snd p))
141− putStr (get_Output (snd p))
142− return (fst p)
120+ (v, st) <- getAction prog (CGISt get_vars post_vars cookies agent
121+ "Content-type: text/html\n"
122+ "")
123+ putStrLn (Headers st)
124+ putStr (Output st)
125+ return v
143126
144127
src/Idris/ElabDecls.hs+32−3
@@ -96,15 +96,20 @@ elabRecord info syn fc tyn ty cn cty
9696 cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
9797 [imps] -> return imps
9898 let ptys = getProjs [] (renameBs cimp cty)
99+ let ptys_u = getProjs [] cty
99100 let recty = getRecTy cty
100101 logLvl 6 $ show (recty, ptys)
101102 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
102103 [pexp (PRef fc rec)])) ptys
103− let ptpos = zip ptys [0..]
104− decls <- mapM (mkProj recty substs cimp) ptpos
105− mapM_ (elabDecl info) (concat decls)
104+ proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
105+ let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
106+ update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])
107+ mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))
106108 where
107109
110+ isNonImp (PExp _ _ _, a) = Just a
111+ isNonImp _ = Nothing
112+
108113 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
109114 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
110115 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
126131 mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
127132 mkImp (NS n s) = NS (mkImp n) s
128133
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+
129138 mkProj recty substs cimp ((pn, pty), pos)
130139 = do let pfnTy = PTy defaultSyntax fc [] pn
131140 (PPi expl rec recty
@@ -143,6 +152,26 @@ elabRecord info syn fc tyn ty cn cty
143152
144153 implicitise (pa, t) = pa { getTm = t }
145154
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+
146175elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)
147176elabCon info syn tn (n, t_in, fc)
148177 = do checkUndefined fc n