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"];;
47 (* lista [meta n., goal; meta n., goal; ... ] *)
48 (* "item1#item2#...#" *)
51 let _,_,metasenv,subst,_ = s#obj in
52 let render_switch = function
53 | Stack.Open i -> "?" ^ (string_of_int i)
54 | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
56 let int_of_switch = function
57 | Stack.Open i | Stack.Closed i -> i
59 let sequent = function
61 let meta = List.assoc i metasenv in
62 snd (ApplyTransformation.ntxt_of_cic_sequent
63 ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
64 | Stack.Closed _ -> "This goal has already been closed."
66 let render_sequent is_loc acc depth tag (pos,sw) =
67 let metano = int_of_switch sw in
70 (match depth, pos with
71 | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B> "
73 Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
74 | 1, pos when Stack.head_tag s#stack = `BranchTag ->
75 Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
76 | _ -> render_switch sw)
79 let markup = Netencoding.Url.encode ~plus:false markup in
80 let txt0 = Netencoding.Url.encode ~plus:false (sequent sw) in
81 (string_of_int metano ^ "|" ^ markup ^ "|" ^ txt0 ^ "#" ^ acc)
84 ~env:(render_sequent true) ~cont:(render_sequent false)
85 ~todo:(render_sequent false) "" s#stack
88 (* let html_of_status s =
89 let _,_,metasenv,subst,_ = s#obj in
90 let txt = List.fold_left
91 (fun acc (nmeta,_ as meta) ->
92 let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
93 ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
95 prerr_endline ("### txt0 = " ^ txt0);
96 ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
99 String.concat "\n\n" txt
102 (* returns the length of the executed text and an html representation of the
104 let advance text (* (?bos=false) *) =
105 let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
107 eval_statement include_paths (*buffer*) !status (`Raw text)
108 (* with End_of_file -> raise Margin *)
111 history := st :: !history;
112 let txt = output_status !status in
113 parsed_len, new_unparsed, txt
116 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
119 let s = Pcre.replace ~rex:heading_nl_RE s in
121 let nl_pos = String.index s '\n' in
122 String.sub s 0 nl_pos
127 let rec aux parsed_len metasenv text =
129 prerr_endline ("evaluating: " ^ first_line text);
130 let plen,new_unparsed,cur_metasenv = advance text in
131 aux (parsed_len+plen) cur_metasenv new_unparsed
133 | End_of_file -> parsed_len, metasenv
135 prerr_endline ("goto bottom debug: metasenv = \n" ^ metasenv);
141 let new_history,new_status =
143 _::(status::_ as history) ->
145 | [_] -> (prerr_endline "singleton";failwith "retract")
146 | _ -> (prerr_endline "nil"; assert false) in
147 NCicLibrary.time_travel !status;
148 history := new_history;
149 status := new_status;
150 output_status !status
153 let read_file fname =
154 let chan = open_in fname in
155 let lines = ref [] in
158 lines := input_line chan :: !lines
160 with End_of_file -> close_in chan);
161 String.concat "\n" (List.rev !lines)
164 let load_index outchan =
165 let s = read_file "index.html" in
166 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
169 let load_doc filename outchan =
170 let s = read_file filename in
172 try String.sub filename (String.length filename - 4) 4 = ".png"
173 with Invalid_argument _ -> false
175 let contenttype = if is_png then "image/png" else "text/html" in
176 Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
179 let call_service outchan =
181 (ignore(MatitaEngine.assert_ng
182 ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
183 "/home/barolo/matitaB/matita/lib/basics/pts.ma");
184 prerr_endline "fatto";
185 let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
187 Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
190 e -> Http_daemon.respond ~code:(`Code 500) outchan
194 let callback req outchan =
196 (sprintf "request path = %s\n" req#path) ^
197 (sprintf "request GET params = %s\n"
199 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^
200 (sprintf "request POST params = %s\n"
202 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^
203 (sprintf "request ALL params = %s\n"
205 (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^
206 (sprintf "cookies = %s\n"
207 (match req#cookies with
210 ^ (if req#hasHeader ~name:"cookie"
211 then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')"
212 else "(No 'Cookie:' header received)")
215 (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^
216 (sprintf "request BODY = '%s'\n\n" req#body)
218 (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *)
223 | "/" -> load_index outchan
224 | "/matita" -> call_service outchan
226 prerr_endline "getting 'file' argument";
227 let filename = List.assoc "file" req#params_GET in
228 prerr_endline ("reading file " ^ filename);
229 let body = read_file filename in
231 Librarian.baseuri_of_script ~include_paths:[] filename
233 status := (!status)#set_baseuri baseuri;
234 Http_daemon.respond ~code:(`Code 200) ~body outchan
236 let script = req#body in
237 prerr_endline ("body length = " ^ (string_of_int (String.length script)));
238 let (parsed_len,_,txt), res, code =
239 try advance script, "OK", `Code 200
241 | HExtlib.Localized(_,e)
243 (prerr_endline ("exception: " ^ Printexc.to_string e);
245 NTacStatus.pp_tac_status !status
246 with e -> prerr_endline ("inner exception: " ^
247 Printexc.to_string e));
248 prerr_endline "end status";
249 let txt = output_status !status in
250 (0,"",txt), Printexc.to_string e, `Code 500)
252 (* prerr_endline ("server response:\n" ^ txt); *)
253 let body = (string_of_int parsed_len) ^ "@" ^ txt in
254 Http_daemon.respond ~code ~body outchan
256 let script = req#body in
257 prerr_endline ("body length = " ^ (string_of_int (String.length script)));
258 let (parsed_len,txt), res, code =
259 try gotoBottom script, "OK", `Code 200
261 | HExtlib.Localized(_,e)
263 (prerr_endline ("exception: " ^ Printexc.to_string e);
265 NTacStatus.pp_tac_status !status
266 with e -> prerr_endline ("inner exception: " ^
267 Printexc.to_string e));
268 prerr_endline "end status";
269 let txt = output_status !status in
270 (0,txt), Printexc.to_string e, `Code 500)
272 (* prerr_endline ("server response:\n" ^ txt); *)
273 let body = (string_of_int parsed_len) ^ "@" ^ txt in
274 Http_daemon.respond ~code ~body outchan
277 let body = retract () in
278 prerr_endline "retract OK";
279 Http_daemon.respond ~code:(`Code 200) ~body outchan
281 (prerr_endline (Printexc.to_string e);
282 Http_daemon.respond ~code:(`Code 500) outchan))
285 let url = String.sub url 1 (String.length url - 1) in
287 with _ -> Http_daemon.respond_not_found ~url outchan
291 { Http_daemon.default_spec with
299 MatitaInit.initialize_all ();
300 Http_daemon.main spec