helm/software/matita/matitaWiki.ml

   1 (* Copyright (C) 2004-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (* $Id: matitacLib.ml 7090 2006-12-12 14:04:59Z fguidi $ *)
  27
  28 open Printf
  29
  30 open GrafiteTypes
  31
  32 exception AttemptToInsertAnAlias
  33
  34
  35 (** {2 Initialization} *)
  36
  37 let grafite_status = (ref [] : GrafiteTypes.status list ref)
  38
  39 let run_script is eval_function  =
  40   let grafite_status' =
  41     match !grafite_status with
  42     | s::_ -> s
  43     | _ -> assert false
  44   in
  45   let cb = fun _ _ -> () in
  46   let matita_debug = Helm_registry.get_bool "matita.debug" in
  47   try
  48    match eval_function grafite_status' is cb with
  49       [] -> raise End_of_file
  50     | (grafite_status'',None)::_ ->
  51        grafite_status := grafite_status''::!grafite_status
  52     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
  53   with
  54   | GrafiteEngine.Drop
  55   | End_of_file
  56   | CicNotationParser.Parse_error _
  57   | HExtlib.Localized _ as exn -> raise exn
  58   | exn ->
  59       if not matita_debug then
  60        HLog.error (snd (MatitaExcPp.to_string exn)) ;
  61       raise exn
  62
  63 let clean_exit n =
  64   match !grafite_status with
  65      [] -> exit n
  66    | grafite_status::_ ->
  67        let baseuri = grafite_status#baseuri in
  68        LibraryClean.clean_baseuris ~verbose:false [baseuri];
  69        exit n
  70
  71 let terminate n =
  72  let terminator = String.make 1 (Char.chr 249) in
  73  let prompt =
  74   (match n with
  75      None -> "-1"
  76    | Some n -> string_of_int n) ^ terminator
  77  in
  78   print_endline prompt;
  79   prerr_endline prompt
  80 ;;
  81
  82 let outer_syntax_parser () =
  83  let text = ref "" in
  84  let tag = ref `Do in
  85  let callbacks =
  86   { XmlPushParser.default_callbacks with
  87     XmlPushParser.start_element =
  88      (Some
  89        (fun name attrs ->
  90          match name with
  91             "pgip" -> ()
  92           | "doitem" -> tag := `Do
  93           | "undoitem" -> tag := `Undo
  94           | _ -> assert false)) ;
  95     XmlPushParser.character_data =
  96      (Some (fun s -> text := !text ^ s)) ;
  97     XmlPushParser.end_element =
  98      (Some
  99        (function
 100            "pgip" -> raise (XmlPushParser.Parse_error "EOC")
 101          | "doitem"
 102          | "undoitem" -> ()
 103          | _ -> assert false))
 104   }
 105  in
 106   let parse = XmlPushParser.create_parser callbacks in
 107     try
 108      XmlPushParser.parse parse (`Channel stdin) ;
 109      raise End_of_file
 110     with
 111        XmlPushParser.Parse_error "no element found" -> raise End_of_file
 112      | XmlPushParser.Parse_error "EOC" ->
 113         match !tag with
 114            `Do -> `Do !text
 115          | `Undo ->
 116              try
 117               `Undo (int_of_string !text)
 118              with
 119               Failure _ -> assert false
 120 ;;
 121
 122 let include_paths =
 123  lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
 124 ;;
 125
 126 let rec interactive_loop () =
 127   (* every loop is terminated by a terminator both on stdout and stderr *)
 128   let interactive_loop n = terminate n; interactive_loop () in
 129   try
 130    match outer_syntax_parser () with
 131       `Undo n ->
 132         let rec drop =
 133          function
 134             0,l -> l
 135           | n,_::l -> drop (n-1,l)
 136           | _,[] -> assert false
 137         in
 138          let to_be_dropped = List.length !grafite_status - n in
 139          let safe_hd = function [] -> assert false | he::_ -> he in
 140          let cur_grafite_status = safe_hd !grafite_status in
 141           grafite_status := drop (to_be_dropped, !grafite_status) ;
 142           let grafite_status = safe_hd !grafite_status in
 143            LexiconSync.time_travel
 144             ~present:cur_grafite_status ~past:grafite_status;
 145            GrafiteSync.time_travel
 146             ~present:cur_grafite_status ~past:grafite_status;
 147            interactive_loop (Some n)
 148     | `Do command ->
 149         let str = Ulexing.from_utf8_string command in
 150         let watch_statuses grafite_status =
 151          match grafite_status#proof_status with
 152             GrafiteTypes.Incomplete_proof
 153              {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
 154               GrafiteTypes.stack = stack } ->
 155               let open_goals = Continuationals.Stack.open_goals stack in
 156               print_endline
 157                (String.concat "\n"
 158                  (List.map
 159                    (fun i ->
 160                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
 161                       ~map_unicode_to_tex:(Helm_registry.get_bool
 162                         "matita.paste_unicode_as_tex")
 163                       (List.find (fun (j,_,_) -> j=i) metasenv)
 164                    ) open_goals))
 165           | _ -> ()
 166         in
 167          run_script str
 168            (MatitaEngine.eval_from_stream ~first_statement_only:true
 169            ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
 170          interactive_loop (Some (List.length !grafite_status))
 171   with
 172    | GrafiteEngine.Macro (floc,_) ->
 173       let x, y = HExtlib.loc_of_floc floc in
 174        HLog.error
 175         (sprintf "A macro has been found in a script at %d-%d" x y);
 176        interactive_loop None
 177    | Sys.Break -> HLog.error "user break!"; interactive_loop None
 178    | GrafiteTypes.Command_error _ -> interactive_loop None
 179    | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
 180       let x, y = HExtlib.loc_of_floc floc in
 181        HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
 182        interactive_loop None
 183    | End_of_file as exn -> raise exn
 184    | exn -> HLog.error (Printexc.to_string exn); interactive_loop None
 185
 186
 187 let main () =
 188   MatitaInit.initialize_all ();
 189   HLog.set_log_callback
 190    (fun tag msg ->
 191      let s =
 192       match tag with
 193          `Debug -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
 194        | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
 195        | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
 196        | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
 197      in
 198       output_string stderr s;
 199       flush stderr
 200    );
 201   (* must be called after init since args are set by cmdline parsing *)
 202   let system_mode =  Helm_registry.get_bool "matita.system" in
 203   let include_paths =
 204    Helm_registry.get_list Helm_registry.string "matita.includes" in
 205   grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
 206    (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
 207   Sys.catch_break true;
 208   let origcb = HLog.get_log_callback () in
 209   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
 210   let newcb tag s =
 211     match tag with
 212     | `Debug -> ()
 213     | `Message | `Warning | `Error -> origcb tag s
 214   in
 215   HLog.set_log_callback newcb;
 216   let matita_debug = Helm_registry.get_bool "matita.debug" in
 217   try
 218     (try
 219       interactive_loop ()
 220      with
 221       | End_of_file -> ()
 222       | GrafiteEngine.Drop -> clean_exit 1
 223     );
 224     let proof_status,moo_content_rev,lexicon_content_rev,dump =
 225       match !grafite_status with
 226       |  s::_ ->
 227          s#proof_status, s#moo_content_rev,
 228           s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
 229       | _ -> assert false
 230     in
 231     if proof_status <> GrafiteTypes.No_proof then
 232      begin
 233       HLog.error
 234        "there are still incomplete proofs at the end of the script";
 235       clean_exit 2
 236      end
 237     else
 238      begin
 239        let baseuri =
 240         (match !grafite_status with
 241            [] -> assert false
 242          | s::_ -> s)#baseuri
 243        in
 244        let moo_fname =
 245          LibraryMisc.obj_file_of_baseuri
 246            ~must_exist:false ~baseuri ~writable:true
 247        in
 248        let lexicon_fname=
 249          LibraryMisc.lexicon_file_of_baseuri
 250           ~must_exist:false ~baseuri ~writable:true
 251        in
 252        GrafiteMarshal.save_moo moo_fname moo_content_rev;
 253        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
 254        NRstatus.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
 255        exit 0
 256      end
 257   with
 258   | exn ->
 259       if matita_debug then raise exn;
 260       clean_exit 3