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 = ref [];;
  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 retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 159   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 160   cgi # set_header
 161     ~cache:`No_cache
 162     ~content_type:"text/xml; charset=\"utf-8\""
 163     ();
 164   let filename = cgi # argument_value "file" in
 165   prerr_endline ("reading file " ^ filename);
 166   let body =
 167     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
 168       (read_file filename) in
 169   prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
 170   let body = "<file>" ^ body ^ "</file>" in
 171   let baseuri, incpaths =
 172     try
 173       let root, baseuri, _fname, _tgt =
 174         Librarian.baseuri_of_script ~include_paths:[] filename in
 175       let includes =
 176        try
 177         Str.split (Str.regexp " ")
 178          (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
 179        with Not_found -> []
 180       in
 181       let rc = root :: includes in
 182        List.iter (HLog.debug) rc; baseuri, rc
 183      with
 184        Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
 185   include_paths := incpaths;
 186   status := (!status)#set_baseuri baseuri;
 187   cgi#out_channel#output_string body;
 188   cgi#out_channel#commit_work()
 189 ;;
 190
 191 let advance0 text =
 192   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
 193        (* try *)
 194          eval_statement !include_paths (*buffer*) !status (`Raw text)
 195        (* with End_of_file -> raise Margin *)
 196      in
 197   status := st;
 198   history := st :: !history;
 199   parsed_len, new_unparsed
 200
 201
 202 (* returns the length of the executed text and an html representation of the
 203  * current metasenv*)
 204 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 205   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 206   cgi # set_header
 207     ~cache:`No_cache
 208     ~content_type:"text/xml; charset=\"utf-8\""
 209     ();
 210   let text = cgi#argument_value "body" in
 211   prerr_endline ("body =\n" ^ text);
 212   let parsed_len, new_unparsed = advance0 text in
 213   let txt = output_status !status in
 214   let body =
 215      "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 216      ^ "</response>"
 217   in
 218   prerr_endline ("sending advance response:\n" ^ body);
 219   cgi#out_channel#output_string body;
 220   cgi#out_channel#commit_work()
 221 ;;
 222
 223 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 224   let rec aux parsed_len text =
 225     try
 226       prerr_endline ("evaluating: " ^ first_line text);
 227       let plen,new_unparsed = advance0 text in
 228       aux (parsed_len+plen) new_unparsed
 229     with
 230     | _ -> parsed_len
 231   in
 232   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 233   cgi # set_header
 234     ~cache:`No_cache
 235     ~content_type:"text/xml; charset=\"utf-8\""
 236     ();
 237   let text = cgi#argument_value "body" in
 238   prerr_endline ("body =\n" ^ text);
 239   let parsed_len = aux 0 text in
 240   let txt = output_status !status in
 241   let body =
 242      "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 243      ^ "</response>"
 244   in
 245   prerr_endline ("sending goto bottom response:\n" ^ body);
 246   cgi#out_channel#output_string body;
 247   cgi#out_channel#commit_work()
 248 ;;
 249
 250 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 251   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 252   cgi # set_header
 253     ~cache:`No_cache
 254     ~content_type:"text/xml; charset=\"utf-8\""
 255     ();
 256   let new_history,new_status =
 257      match !history with
 258        _::(status::_ as history) ->
 259         history, status
 260     | [_] -> (prerr_endline "singleton";failwith "retract")
 261     | _ -> (prerr_endline "nil"; assert false) in
 262   NCicLibrary.time_travel !status;
 263   history := new_history;
 264   status := new_status;
 265   let body = output_status !status in
 266   cgi#out_channel#output_string body;
 267   cgi#out_channel#commit_work()
 268 ;;
 269
 270
 271 open Netcgi1_compat.Netcgi_types;;
 272
 273 (**********************************************************************)
 274 (* Create the webserver                                               *)
 275 (**********************************************************************)
 276
 277
 278 let start() =
 279   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 280
 281   let use_mt = ref true in
 282
 283   let opt_list' =
 284     [ "-mt", Arg.Set use_mt,
 285       "  Use multi-threading instead of multi-processing"
 286     ] @ opt_list in
 287
 288   Arg.parse
 289     opt_list'
 290     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 291     "usage: netplex [options]";
 292   let parallelizer =
 293     if !use_mt then
 294       Netplex_mt.mt()     (* multi-threading *)
 295     else
 296       Netplex_mp.mp() in  (* multi-processing *)
 297 (*
 298   let adder =
 299     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 300       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 301       dyn_uri = None;                 (* not needed *)
 302       dyn_translator = (fun _ -> ""); (* not needed *)
 303       dyn_accept_all_conditionals = false;
 304     } in
 305 *)
 306   let do_advance =
 307     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 308       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 309       dyn_uri = None;                 (* not needed *)
 310       dyn_translator = (fun _ -> ""); (* not needed *)
 311       dyn_accept_all_conditionals = false;
 312     } in
 313   let do_retract =
 314     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 315       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 316       dyn_uri = None;                 (* not needed *)
 317       dyn_translator = (fun _ -> ""); (* not needed *)
 318       dyn_accept_all_conditionals = false;
 319     } in
 320   let goto_bottom =
 321     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 322       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 323       dyn_uri = None;                 (* not needed *)
 324       dyn_translator = (fun _ -> ""); (* not needed *)
 325       dyn_accept_all_conditionals = false;
 326     } in
 327   let retrieve =
 328     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 329       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 330       dyn_uri = None;                 (* not needed *)
 331       dyn_translator = (fun _ -> ""); (* not needed *)
 332       dyn_accept_all_conditionals = false;
 333     } in
 334
 335   let nethttpd_factory =
 336     Nethttpd_plex.nethttpd_factory
 337       ~handlers:[ "advance", do_advance
 338                 ; "retract", do_retract
 339                 ; "bottom", goto_bottom
 340                 ; "open", retrieve ]
 341       () in
 342   MatitaInit.initialize_all ();
 343   Netplex_main.startup
 344     parallelizer
 345     Netplex_log.logger_factories   (* allow all built-in logging styles *)
 346     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
 347     [ nethttpd_factory ]           (* make this nethttpd available *)
 348     cmdline_cfg
 349 ;;
 350
 351 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
 352 start();;