4 module Stack = Continuationals.Stack
6 (*** from matitaScript.ml ***)
7 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
9 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
12 let ast,unparsed_text =
15 (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
17 GrafiteParser.parsable_statement status
18 (Ulexing.from_utf8_string text) in
19 let ast = MatitaEngine.get_ast status include_paths strm in
21 | `Ast (st, text) -> st, text
23 let floc = match ast with
24 | GrafiteAst.Executable (loc, _)
25 | GrafiteAst.Comment (loc, _) -> loc in
27 let _,lend = HExtlib.loc_of_floc floc in
28 let parsed_text, parsed_text_len =
29 MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
30 let byte_parsed_text_len = String.length parsed_text in
32 String.sub unparsed_text byte_parsed_text_len
33 (String.length unparsed_text - byte_parsed_text_len)
37 MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
39 (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) Glib.Utf8.length parsed_text
42 let status = ref (new MatitaEngine.status "cic:/matita");;
43 let history = ref [!status];;
45 let include_paths = ["/home/barolo/matitaB/matita/lib"];;
49 * <metaname>...</metaname>
56 let _,_,metasenv,subst,_ = s#obj in
57 let render_switch = function
58 | Stack.Open i -> "?" ^ (string_of_int i)
59 | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
61 let int_of_switch = function
62 | Stack.Open i | Stack.Closed i -> i
64 let sequent = function
66 let meta = List.assoc i metasenv in
67 snd (ApplyTransformation.ntxt_of_cic_sequent
68 ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
69 | Stack.Closed _ -> "This goal has already been closed."
71 let render_sequent is_loc acc depth tag (pos,sw) =
72 let metano = int_of_switch sw in
75 (match depth, pos with
76 | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
78 Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
79 | 1, pos when Stack.head_tag s#stack = `BranchTag ->
80 Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
81 | _ -> render_switch sw)
85 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
86 let markup = "<metaname>" ^ markup ^ "</metaname>" in
88 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
90 let txt0 = "<goal>" ^ sequent ^ "</goal>" in
91 "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
92 txt0 ^ "</meta>" ^ acc
94 let res = "<metasenv>" ^
96 ~env:(render_sequent true) ~cont:(render_sequent false)
97 ~todo:(render_sequent false) "" s#stack) ^
100 prerr_endline ("sending metasenv:\n" ^ res); res
103 (* let html_of_status s =
104 let _,_,metasenv,subst,_ = s#obj in
105 let txt = List.fold_left
106 (fun acc (nmeta,_ as meta) ->
107 let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
108 ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
110 prerr_endline ("### txt0 = " ^ txt0);
111 ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
114 String.concat "\n\n" txt
117 (* returns the length of the executed text and an html representation of the
119 let advance text (* (?bos=false) *) =
120 let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
122 eval_statement include_paths (*buffer*) !status (`Raw text)
123 (* with End_of_file -> raise Margin *)
126 history := st :: !history;
127 let txt = output_status !status in
128 parsed_len, new_unparsed, txt
131 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
134 let s = Pcre.replace ~rex:heading_nl_RE s in
136 let nl_pos = String.index s '\n' in
137 String.sub s 0 nl_pos
142 let rec aux parsed_len metasenv text =
144 prerr_endline ("evaluating: " ^ first_line text);
145 let plen,new_unparsed,cur_metasenv = advance text in
146 aux (parsed_len+plen) cur_metasenv new_unparsed
148 | End_of_file -> parsed_len, metasenv
150 prerr_endline ("goto bottom debug: metasenv = \n" ^ metasenv);
156 let new_history,new_status =
158 _::(status::_ as history) ->
160 | [_] -> (prerr_endline "singleton";failwith "retract")
161 | _ -> (prerr_endline "nil"; assert false) in
162 NCicLibrary.time_travel !status;
163 history := new_history;
164 status := new_status;
165 output_status !status
168 let read_file fname =
169 let chan = open_in fname in
170 let lines = ref [] in
173 lines := input_line chan :: !lines
175 with End_of_file -> close_in chan);
176 String.concat "\n" (List.rev !lines)
179 let load_index outchan =
180 let s = read_file "index.html" in
181 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
184 let load_doc filename outchan =
185 let s = read_file filename in
187 try String.sub filename (String.length filename - 4) 4 = ".png"
188 with Invalid_argument _ -> false
190 let contenttype = if is_png then "image/png" else "text/html" in
191 Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
194 let call_service outchan =
196 (ignore(MatitaEngine.assert_ng
197 ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
198 "/home/barolo/matitaB/matita/lib/basics/pts.ma");
199 prerr_endline "fatto";
200 let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
202 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
205 e -> Http_daemon.respond ~code:(`Code 500) outchan
209 let callback req outchan =
211 (sprintf "request path = %s\n" req#path) ^
212 (sprintf "request GET params = %s\n"
214 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^
215 (sprintf "request POST params = %s\n"
217 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^
218 (sprintf "request ALL params = %s\n"
220 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^
221 (sprintf "cookies = %s\n"
222 (match req#cookies with
225 ^ (if req#hasHeader ~name:"cookie"
226 then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')"
227 else "(No 'Cookie:' header received)")
230 (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^
231 (sprintf "request BODY = '%s'\n\n" req#body)
233 (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *)
238 | "/" -> load_index outchan
239 | "/matita" -> call_service outchan
241 prerr_endline "getting 'file' argument";
242 let filename = List.assoc "file" req#params_GET in
243 prerr_endline ("reading file " ^ filename);
245 Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
246 (read_file filename) in
247 prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
248 let body = "<file>" ^ body ^ "</file>" in
250 Librarian.baseuri_of_script ~include_paths:[] filename
252 status := (!status)#set_baseuri baseuri;
253 Http_daemon.respond ~code:(`Code 200) ~body outchan
255 let script = req#body in
256 prerr_endline ("body length = " ^ (string_of_int (String.length script)));
257 let (parsed_len,_,txt), res, code =
258 try advance script, "OK", `Code 200
260 | HExtlib.Localized(_,e)
262 (prerr_endline ("exception: " ^ Printexc.to_string e);
264 NTacStatus.pp_tac_status !status
265 with e -> prerr_endline ("inner exception: " ^
266 Printexc.to_string e));
267 prerr_endline "end status";
268 let txt = output_status !status in
269 (0,"",txt), Printexc.to_string e, `Code 500)
271 (* prerr_endline ("server response:\n" ^ txt); *)
273 "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
275 in (prerr_endline ("sending advance response:\n" ^ body);
276 Http_daemon.respond ~code ~body outchan)
278 let script = req#body in
279 prerr_endline ("body length = " ^ (string_of_int (String.length script)));
280 let (parsed_len,txt), res, code =
281 try gotoBottom script, "OK", `Code 200
283 | HExtlib.Localized(_,e)
285 (prerr_endline ("exception: " ^ Printexc.to_string e);
287 NTacStatus.pp_tac_status !status
288 with e -> prerr_endline ("inner exception: " ^
289 Printexc.to_string e));
290 prerr_endline "end status";
291 let txt = output_status !status in
292 (0,txt), Printexc.to_string e, `Code 500)
294 (* prerr_endline ("server response:\n" ^ txt); *)
296 "<parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
297 in Http_daemon.respond ~code ~body outchan
300 let body = retract () in
301 prerr_endline "retract OK";
302 Http_daemon.respond ~code:(`Code 200) ~body outchan
304 (prerr_endline (Printexc.to_string e);
305 Http_daemon.respond ~code:(`Code 500) outchan))
308 let url = String.sub url 1 (String.length url - 1) in
310 with _ -> Http_daemon.respond_not_found ~url outchan
314 { Http_daemon.default_spec with
317 mode = `Single (*`Thread *) ;
322 MatitaInit.initialize_all ();
323 Http_daemon.main spec