matitaB/matita/matitadaemon.ml

   1 open Printf;;
   2 open Http_types;;
   3
   4 module Stack = Continuationals.Stack
   5
   6 let utf8_length = Netconversion.ustring_length `Enc_utf8
   7
   8 (*** from matitaScript.ml ***)
   9 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
  10
  11 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
  12  statement
  13 =
  14   let ast,unparsed_text =
  15     match statement with
  16     | `Raw text ->
  17         (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
  18         let strm =
  19          GrafiteParser.parsable_statement status
  20           (Ulexing.from_utf8_string text) in
  21         let ast = MatitaEngine.get_ast status include_paths strm in
  22          ast, text
  23     | `Ast (st, text) -> st, text
  24   in
  25   let floc = match ast with
  26   | GrafiteAst.Executable (loc, _)
  27   | GrafiteAst.Comment (loc, _) -> loc in
  28
  29   let _,lend = HExtlib.loc_of_floc floc in
  30   let parsed_text, parsed_text_len =
  31     MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
  32   let byte_parsed_text_len = String.length parsed_text in
  33   let unparsed_txt' =
  34     String.sub unparsed_text byte_parsed_text_len
  35       (String.length unparsed_text - byte_parsed_text_len)
  36   in
  37
  38   let status =
  39     MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
  40   in
  41   (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
  42     utf8_length parsed_text
  43
  44
  45 let status = ref (new MatitaEngine.status "cic:/matita");;
  46 let history = ref [!status];;
  47
  48 let include_paths = ["/home/barolo/matitaB/matita/lib"];;
  49
  50 (* <metasenv>
  51  *   <meta number="...">
  52  *     <metaname>...</metaname>
  53  *     <goal>...</goal>
  54  *   </meta>
  55  *
  56  *   ...
  57  * </metasenv> *)
  58 let output_status s =
  59   let _,_,metasenv,subst,_ = s#obj in
  60   let render_switch = function
  61   | Stack.Open i -> "?" ^ (string_of_int i)
  62   | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
  63   in
  64   let int_of_switch = function
  65   | Stack.Open i | Stack.Closed i -> i
  66   in
  67   let sequent = function
  68   | Stack.Open i ->
  69       let meta = List.assoc i metasenv in
  70       snd (ApplyTransformation.ntxt_of_cic_sequent
  71         ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
  72   | Stack.Closed _ -> "This goal has already been closed."
  73   in
  74   let render_sequent is_loc acc depth tag (pos,sw) =
  75     let metano = int_of_switch sw in
  76     let markup =
  77       if is_loc then
  78         (match depth, pos with
  79          | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B>"
  80          | 0, _ ->
  81             Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
  82          | 1, pos when Stack.head_tag s#stack = `BranchTag ->
  83              Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
  84          | _ -> render_switch sw)
  85       else render_switch sw
  86     in
  87     prerr_endline "pippo1";
  88     let markup =
  89       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
  90     let markup = "<metaname>" ^ markup ^ "</metaname>" in
  91     prerr_endline "pippo2";
  92     let sequent =
  93       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
  94     in
  95     let txt0 = "<goal>" ^ sequent ^ "</goal>" in
  96     "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
  97     txt0 ^ "</meta>" ^ acc
  98   in
  99   let res = "<metasenv>" ^
 100     (Stack.fold
 101       ~env:(render_sequent true) ~cont:(render_sequent false)
 102       ~todo:(render_sequent false) "" s#stack) ^
 103     "</metasenv>"
 104   in
 105   prerr_endline ("sending metasenv:\n" ^ res); res
 106 ;;
 107
 108 (* let html_of_status s =
 109   let _,_,metasenv,subst,_ = s#obj in
 110   let txt = List.fold_left
 111     (fun acc (nmeta,_ as meta) ->
 112        let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
 113          ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
 114        in
 115        prerr_endline ("### txt0 = " ^ txt0);
 116       ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
 117     [] metasenv
 118   in
 119   String.concat "\n\n" txt
 120 ;; *)
 121
 122 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
 123
 124 let first_line s =
 125   let s = Pcre.replace ~rex:heading_nl_RE s in
 126   try
 127     let nl_pos = String.index s '\n' in
 128     String.sub s 0 nl_pos
 129   with Not_found -> s
 130 ;;
 131
 132 let read_file fname =
 133   let chan = open_in fname in
 134   let lines = ref [] in
 135   (try
 136      while true do
 137        lines := input_line chan :: !lines
 138      done;
 139    with End_of_file -> close_in chan);
 140   String.concat "\n" (List.rev !lines)
 141 ;;
 142
 143 let load_index outchan =
 144   let s = read_file "index.html" in
 145   Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 146 ;;
 147
 148 let load_doc filename outchan =
 149   let s = read_file filename in
 150   let is_png =
 151     try String.sub filename (String.length filename - 4) 4 = ".png"
 152     with Invalid_argument _ -> false
 153   in
 154   let contenttype = if is_png then "image/png" else "text/html" in
 155   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 156 ;;
 157
 158 let call_service outchan =
 159   try
 160    (ignore(MatitaEngine.assert_ng
 161      ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
 162     "/home/barolo/matitaB/matita/lib/basics/pts.ma");
 163     prerr_endline "fatto";
 164     let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
 165     in
 166     Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 167    )
 168   with
 169   e -> Http_daemon.respond ~code:(`Code 500) outchan
 170 ;;
 171
 172 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 173   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 174   cgi # set_header
 175     ~cache:`No_cache
 176     ~content_type:"text/xml; charset=\"utf-8\""
 177     ();
 178   let filename = cgi # argument_value "file" in
 179   prerr_endline ("reading file " ^ filename);
 180   let body =
 181     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
 182       (read_file filename) in
 183   prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
 184   let body = "<file>" ^ body ^ "</file>" in
 185   let _,baseuri,_,_ =
 186     Librarian.baseuri_of_script ~include_paths:[] filename
 187   in
 188   status := (!status)#set_baseuri baseuri;
 189   cgi#out_channel#output_string body;
 190   cgi#out_channel#commit_work()
 191 ;;
 192
 193 let advance0 text =
 194   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
 195        (* try *)
 196          eval_statement include_paths (*buffer*) !status (`Raw text)
 197        (* with End_of_file -> raise Margin *)
 198      in
 199   status := st;
 200   history := st :: !history;
 201   parsed_len, new_unparsed
 202
 203
 204 (* returns the length of the executed text and an html representation of the
 205  * current metasenv*)
 206 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 207   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 208   cgi # set_header
 209     ~cache:`No_cache
 210     ~content_type:"text/xml; charset=\"utf-8\""
 211     ();
 212   let text = cgi#argument_value "body" in
 213   prerr_endline ("body =\n" ^ text);
 214   let parsed_len, new_unparsed = advance0 text in
 215   let txt = output_status !status in
 216   let body =
 217      "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 218      ^ "</response>"
 219   in
 220   prerr_endline ("sending advance response:\n" ^ body);
 221   cgi#out_channel#output_string body;
 222   cgi#out_channel#commit_work()
 223 ;;
 224
 225 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 226   let rec aux parsed_len text =
 227     try
 228       prerr_endline ("evaluating: " ^ first_line text);
 229       let plen,new_unparsed = advance0 text in
 230       aux (parsed_len+plen) new_unparsed
 231     with
 232     | _ -> parsed_len
 233   in
 234   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 235   cgi # set_header
 236     ~cache:`No_cache
 237     ~content_type:"text/xml; charset=\"utf-8\""
 238     ();
 239   let text = cgi#argument_value "body" in
 240   prerr_endline ("body =\n" ^ text);
 241   let parsed_len = aux 0 text in
 242   let txt = output_status !status in
 243   let body =
 244      "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 245      ^ "</response>"
 246   in
 247   prerr_endline ("sending goto bottom response:\n" ^ body);
 248   cgi#out_channel#output_string body;
 249   cgi#out_channel#commit_work()
 250 ;;
 251
 252 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 253   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 254   cgi # set_header
 255     ~cache:`No_cache
 256     ~content_type:"text/xml; charset=\"utf-8\""
 257     ();
 258   let new_history,new_status =
 259      match !history with
 260        _::(status::_ as history) ->
 261         history, status
 262     | [_] -> (prerr_endline "singleton";failwith "retract")
 263     | _ -> (prerr_endline "nil"; assert false) in
 264   NCicLibrary.time_travel !status;
 265   history := new_history;
 266   status := new_status;
 267   let body = output_status !status in
 268   cgi#out_channel#output_string body;
 269   cgi#out_channel#commit_work()
 270 ;;
 271
 272
 273 open Netcgi1_compat.Netcgi_types;;
 274
 275 (**********************************************************************)
 276 (* Create the webserver                                               *)
 277 (**********************************************************************)
 278
 279
 280 let start() =
 281   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 282
 283   let use_mt = ref true in
 284
 285   let opt_list' =
 286     [ "-mt", Arg.Set use_mt,
 287       "  Use multi-threading instead of multi-processing"
 288     ] @ opt_list in
 289
 290   Arg.parse
 291     opt_list'
 292     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 293     "usage: netplex [options]";
 294   let parallelizer =
 295     if !use_mt then
 296       Netplex_mt.mt()     (* multi-threading *)
 297     else
 298       Netplex_mp.mp() in  (* multi-processing *)
 299 (*
 300   let adder =
 301     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 302       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 303       dyn_uri = None;                 (* not needed *)
 304       dyn_translator = (fun _ -> ""); (* not needed *)
 305       dyn_accept_all_conditionals = false;
 306     } in
 307 *)
 308   let do_advance =
 309     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 310       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 311       dyn_uri = None;                 (* not needed *)
 312       dyn_translator = (fun _ -> ""); (* not needed *)
 313       dyn_accept_all_conditionals = false;
 314     } in
 315   let do_retract =
 316     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 317       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 318       dyn_uri = None;                 (* not needed *)
 319       dyn_translator = (fun _ -> ""); (* not needed *)
 320       dyn_accept_all_conditionals = false;
 321     } in
 322   let goto_bottom =
 323     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 324       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 325       dyn_uri = None;                 (* not needed *)
 326       dyn_translator = (fun _ -> ""); (* not needed *)
 327       dyn_accept_all_conditionals = false;
 328     } in
 329   let retrieve =
 330     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 331       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 332       dyn_uri = None;                 (* not needed *)
 333       dyn_translator = (fun _ -> ""); (* not needed *)
 334       dyn_accept_all_conditionals = false;
 335     } in
 336
 337   let nethttpd_factory =
 338     Nethttpd_plex.nethttpd_factory
 339       ~handlers:[ "advance", do_advance
 340                 ; "retract", do_retract
 341                 ; "bottom", goto_bottom
 342                 ; "open", retrieve ]
 343       () in
 344   MatitaInit.initialize_all ();
 345   Netplex_main.startup
 346     parallelizer
 347     Netplex_log.logger_factories   (* allow all built-in logging styles *)
 348     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
 349     [ nethttpd_factory ]           (* make this nethttpd available *)
 350     cmdline_cfg
 351 ;;
 352
 353 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
 354 start();;