git.iko.soy/Idris-dev
on master help sign in
Added lib/network directory, and network.cgi module
2a50169Edwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -18,7 +18,7 @@ Description: Idris is a general purpose language with full dependent types.
18Cabal-Version: >= 1.6
18Cabal-Version: >= 1.6
19Build-type: Custom
19Build-type: Custom
20
20
21−Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr
21+Extra-source-files: lib/Makefile lib/*.idr lib/prelude/*.idr lib/network/*.idr
22 tutorial/examples/*.idr
22 tutorial/examples/*.idr
23
23
24Executable idris
24Executable idris
lib/Makefile+7
@@ -4,16 +4,23 @@ check: .PHONY
4 echo "Checking $$x"; \
4 echo "Checking $$x"; \
5 idris --noprelude --check $$x; \
5 idris --noprelude --check $$x; \
6 done
6 done
7+ for x in network/*.idr ; do \
8+ echo "Checking $$x"; \
9+ idris --noprelude --check $$x; \
10+ done
7
11
8recheck: clean check
12recheck: clean check
9
13
10install: recheck
14install: recheck
11 mkdir -p $(TARGET)/prelude
15 mkdir -p $(TARGET)/prelude
16+ mkdir -p $(TARGET)/network
12 install *.ibc $(TARGET)
17 install *.ibc $(TARGET)
13 install prelude/*.ibc $(TARGET)/prelude
18 install prelude/*.ibc $(TARGET)/prelude
19+ install network/*.ibc $(TARGET)/network
14
20
15clean: .PHONY
21clean: .PHONY
16 rm -f *.ibc
22 rm -f *.ibc
17 rm -f prelude/*.ibc
23 rm -f prelude/*.ibc
24+ rm -f network/*.ibc
18
25
19.PHONY:
26.PHONY:
lib/network/cgi.idrnew file+153
@@ -0,0 +1,153 @@
1+module network.cgi;
2+
3+import system;
4+
5+public
6+Vars : Set;
7+Vars = List (String, String);
8+
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;
33+
34+add_Headers : String -> CGIInfo -> CGIInfo;
35+add_Headers str (CGISt g p c a h o) = CGISt g p c a (h ++ str) o;
36+
37+add_Output : String -> CGIInfo -> CGIInfo;
38+add_Output str (CGISt g p c a h o) = CGISt g p c a h (o ++ str);
39+
40+abstract
41+data CGI : Set -> Set where
42+ MkCGI : (CGIInfo -> IO (a, CGIInfo)) -> CGI a;
43+
44+getAction : CGI a -> CGIInfo -> IO (a, CGIInfo);
45+getAction (MkCGI act) = act;
46+
47+instance Monad CGI where {
48+ (>>=) (MkCGI f) k = MkCGI (\s => do { v <- f s;
49+ getAction (k (fst v)) (snd v); });
50+
51+ return v = MkCGI (\s => return (v, s));
52+}
53+
54+setInfo : CGIInfo -> CGI ();
55+setInfo i = MkCGI (\s => return ((), i));
56+
57+getInfo : CGI CGIInfo;
58+getInfo = MkCGI (\s => return (s, s));
59+
60+abstract
61+lift : IO a -> CGI a ;
62+lift op = MkCGI (\st => do { x <- op;
63+ return (x, st); } );
64+
65+abstract
66+output : String -> CGI ();
67+output s = do { i <- getInfo;
68+ setInfo (add_Output s i); };
69+
70+abstract
71+queryVars : CGI Vars;
72+queryVars = do { i <- getInfo;
73+ return (get_GET i); };
74+
75+abstract
76+postVars : CGI Vars;
77+postVars = do { i <- getInfo;
78+ return (get_POST i); };
79+
80+abstract
81+cookieVars : CGI Vars;
82+cookieVars = do { i <- getInfo;
83+ return (get_Cookies i); };
84+
85+abstract
86+queryVar : String -> CGI (Maybe String);
87+queryVar x = do { vs <- queryVars;
88+ return (lookup x vs); };
89+
90+getOutput : CGI String;
91+getOutput = do { i <- getInfo;
92+ return (get_Output i); };
93+
94+getHeaders : CGI String;
95+getHeaders = do { i <- getInfo;
96+ return (get_Headers i); };
97+
98+abstract
99+flushHeaders : CGI ();
100+flushHeaders = do { o <- getHeaders;
101+ lift (putStrLn o);
102+ };
103+
104+abstract
105+flush : CGI ();
106+flush = do { o <- getOutput;
107+ lift (putStr o);
108+ };
109+
110+getVars : List Char -> String -> List (String, String);
111+getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
112+ where {
113+ readVar : String -> Maybe (String, String);
114+ readVar xs with split (\x => x == '=') xs {
115+ | [k, v] = Just (trim k, trim v);
116+ | _ = Nothing;
117+ }
118+ }
119+
120+getContent : Int -> IO String;
121+getContent x = getC x "" where {
122+ getC : Int -> String -> IO String;
123+ getC 0 acc = return $ rev acc;
124+ getC n acc = do { x <- getChar;
125+ getC (n-1) (strCons x acc); };
126+}
127+
128+abstract
129+runCGI : CGI a -> IO a;
130+runCGI prog = do {
131+ clen_in <- getEnv "CONTENT_LENGTH";
132+ let clen = prim__strToInt clen_in;
133+ content <- getContent clen;
134+ query <- getEnv "QUERY_STRING";
135+ cookie <- getEnv "HTTP_COOKIE";
136+ agent <- getEnv "HTTP_USER_AGENT";
137+
138+ let get_vars = getVars ['&',';'] query;
139+ let post_vars = getVars ['&'] content;
140+ let cookies = getVars [';'] cookie;
141+
142+ p <- getAction prog (CGISt get_vars post_vars cookies agent
143+ "Content-type: text/html\n"
144+ "");
145+ putStrLn (get_Headers (snd p));
146+ putStr (get_Output (snd p));
147+ return (fst p);
148+};
149+
150+
151+
152+
153+