matitaB/matita/matitadaemon.ml

   1 open Printf;;
   2 open Http_types;;
   3
   4 module Stack = Continuationals.Stack
   5
   6 (*** from matitaScript.ml ***)
   7 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
   8
   9 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
  10  statement
  11 =
  12   let ast,unparsed_text =
  13     match statement with
  14     | `Raw text ->
  15         (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
  16         let strm =
  17          GrafiteParser.parsable_statement status
  18           (Ulexing.from_utf8_string text) in
  19         let ast = MatitaEngine.get_ast status include_paths strm in
  20          ast, text
  21     | `Ast (st, text) -> st, text
  22   in
  23   let floc = match ast with
  24   | GrafiteAst.Executable (loc, _)
  25   | GrafiteAst.Comment (loc, _) -> loc in
  26
  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
  31   let status =
  32     MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
  33   in
  34   (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text
  35
  36
  37 let status = ref (new MatitaEngine.status "cic:/matita");;
  38 let history = ref [!status];;
  39
  40 let include_paths = ["/home/barolo/matitaB/matita/lib"];;
  41
  42 (* lista [meta n., goal; meta n., goal; ... ] *)
  43 (* "item1#item2#...#" *)
  44
  45 let output_status s =
  46   let _,_,metasenv,subst,_ = s#obj in
  47   let render_switch = function
  48   | Stack.Open i -> "?" ^ (string_of_int i)
  49   | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
  50   in
  51   let int_of_switch = function
  52   | Stack.Open i | Stack.Closed i -> i
  53   in
  54   let sequent = function
  55   | Stack.Open i ->
  56       let meta = List.assoc i metasenv in
  57       snd (ApplyTransformation.ntxt_of_cic_sequent
  58         ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
  59   | Stack.Closed _ -> "This goal has already been closed."
  60   in
  61   let render_sequent is_loc acc depth tag (pos,sw) =
  62     let metano = int_of_switch sw in
  63     let markup =
  64       if is_loc then
  65         (match depth, pos with
  66          | 0, 0 -> "<B>" ^ (render_switch sw) ^ "</B> "
  67          | 0, _ ->
  68             Printf.sprintf "<B>|<SUB>%d</SUB>: %s</B>" pos (render_switch sw)
  69          | 1, pos when Stack.head_tag s#stack = `BranchTag ->
  70              Printf.sprintf "|<SUB>%d</SUB> : %s" pos (render_switch sw)
  71          | _ -> render_switch sw)
  72       else render_switch sw
  73     in
  74     let markup = Netencoding.Url.encode ~plus:false markup in
  75     let txt0 = Netencoding.Url.encode ~plus:false (sequent sw) in
  76     (string_of_int metano ^ "|" ^ markup ^ "|" ^ txt0 ^ "#" ^ acc)
  77   in
  78   Stack.fold
  79     ~env:(render_sequent true) ~cont:(render_sequent false)
  80     ~todo:(render_sequent false) "" s#stack
  81 ;;
  82
  83 (* let html_of_status s =
  84   let _,_,metasenv,subst,_ = s#obj in
  85   let txt = List.fold_left
  86     (fun acc (nmeta,_ as meta) ->
  87        let txt0 = snd (ApplyTransformation.ntxt_of_cic_sequent
  88          ~metasenv ~subst ~map_unicode_to_tex:false 80 s meta)
  89        in
  90        prerr_endline ("### txt0 = " ^ txt0);
  91       ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
  92     [] metasenv
  93   in
  94   String.concat "\n\n" txt
  95 ;; *)
  96
  97 let advance text (* (?bos=false) *) =
  98      let (st,new_statements),(* newtext TODO *) _,parsed_len =
  99        (* try *)
 100          eval_statement include_paths (*buffer*) !status (`Raw text)
 101        (* with End_of_file -> raise Margin *)
 102      in
 103      status := st;
 104      history := st :: !history;
 105      let txt = output_status !status in
 106      parsed_len, txt
 107 ;;
 108
 109 let retract () =
 110   let new_history,new_status =
 111      match !history with
 112        _::(status::_ as history) ->
 113         history, status
 114     | [_] -> failwith "retract"
 115     | _ -> assert false in
 116   NCicLibrary.time_travel !status;
 117   history := new_history;
 118   status := new_status;
 119   output_status !status
 120 ;;
 121
 122 let read_file fname =
 123   let chan = open_in fname in
 124   let lines = ref [] in
 125   (try
 126      while true do
 127        lines := input_line chan :: !lines
 128      done;
 129    with End_of_file -> close_in chan);
 130   String.concat "\r\n" (List.rev !lines)
 131 ;;
 132
 133 let load_index outchan =
 134   let s = read_file "index.html" in
 135   Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 136 ;;
 137
 138 let load_doc filename outchan =
 139   let s = read_file filename in
 140   Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 141 ;;
 142
 143 let call_service outchan =
 144   try
 145    (ignore(MatitaEngine.assert_ng
 146      ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
 147     "/home/barolo/matitaB/matita/lib/basics/pts.ma");
 148     prerr_endline "fatto";
 149     let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
 150     in
 151     Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 152    )
 153   with
 154   e -> Http_daemon.respond ~code:(`Code 500) outchan
 155 ;;
 156
 157
 158 let callback req outchan =
 159   let str =
 160     (sprintf "request path = %s\n"  req#path) ^
 161     (sprintf "request GET params = %s\n"
 162       (String.concat ";"
 163         (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^
 164     (sprintf "request POST params = %s\n"
 165       (String.concat ";"
 166         (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^
 167     (sprintf "request ALL params = %s\n"
 168       (String.concat ";"
 169         (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^
 170     (sprintf "cookies = %s\n"
 171       (match req#cookies with
 172       | None ->
 173           "NO COOKIES "
 174           ^ (if req#hasHeader ~name:"cookie"
 175              then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')"
 176              else "(No 'Cookie:' header received)")
 177       | Some cookies ->
 178           (String.concat ";"
 179             (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^
 180     (sprintf "request BODY = '%s'\n\n" req#body)
 181   in
 182   (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *)
 183
 184   prerr_endline str;
 185
 186   match req#path with
 187   | "/" -> load_index outchan
 188   | "/matita" -> call_service outchan
 189   | "/open" ->
 190       prerr_endline "getting 'file' argument";
 191       let filename = List.assoc "file" req#params_GET in
 192       prerr_endline ("reading file " ^ filename);
 193       let body = read_file filename in
 194       let _,baseuri,_,_ =
 195         Librarian.baseuri_of_script ~include_paths:[] filename
 196       in
 197       status := (!status)#set_baseuri baseuri;
 198       Http_daemon.respond ~code:(`Code 200) ~body outchan
 199   | "/advance" ->
 200       let script = req#body in
 201       prerr_endline ("body length = " ^ (string_of_int (String.length script)));
 202       let (parsed_len,txt), res, code =
 203         try advance script, "OK", `Code 200
 204         with
 205         | HExtlib.Localized(_,e)
 206         | e ->
 207                 (prerr_endline ("exception: " ^ Printexc.to_string e);
 208                 (try
 209                   NTacStatus.pp_tac_status !status
 210                 with e -> prerr_endline ("inner exception: " ^
 211                   Printexc.to_string e));
 212                 prerr_endline "end status";
 213                 let txt = output_status !status in
 214                 (0,txt), Printexc.to_string e, `Code 500)
 215       in
 216       prerr_endline ("server response:\n" ^ txt);
 217       let body = (string_of_int parsed_len) ^ "@" ^ txt in
 218       Http_daemon.respond ~code ~body outchan
 219   | "/retract" ->
 220       (try
 221         let body = retract () in
 222         Http_daemon.respond ~code:(`Code 200) ~body outchan
 223        with e ->
 224         (prerr_endline (Printexc.to_string e);
 225          Http_daemon.respond ~code:(`Code 500) outchan))
 226   | url ->
 227      try
 228        let url = String.sub url 1 (String.length url - 1) in
 229        load_doc url outchan
 230      with _ -> Http_daemon.respond_not_found ~url outchan
 231 ;;
 232
 233 let spec =
 234   { Http_daemon.default_spec with
 235       callback = callback;
 236       port = 9999;
 237       mode = `Thread;
 238   }
 239 ;;
 240
 241 let _ =
 242   MatitaInit.initialize_all ();
 243   Http_daemon.main spec
 244 ;;