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 let lexicon_status = (ref [] : LexiconEngine.status list ref)
  39
  40 let run_script is eval_function  =
  41   let lexicon_status',grafite_status' =
  42     match !lexicon_status,!grafite_status with
  43     | ss::_, s::_ -> ss,s
  44     | _,_ -> assert false
  45   in
  46   let cb = fun _ _ -> () in
  47   let matita_debug = Helm_registry.get_bool "matita.debug" in
  48   try
  49    match eval_function lexicon_status' grafite_status' is cb with
  50       [] -> raise End_of_file
  51     | ((grafite_status'',lexicon_status''),None)::_ ->
  52        lexicon_status := lexicon_status''::!lexicon_status;
  53        grafite_status := grafite_status''::!grafite_status
  54     | (s,Some _)::_ -> raise AttemptToInsertAnAlias
  55   with
  56   | GrafiteEngine.Drop
  57   | End_of_file
  58   | CicNotationParser.Parse_error _
  59   | HExtlib.Localized _ as exn -> raise exn
  60   | exn ->
  61       if not matita_debug then
  62        HLog.error (snd (MatitaExcPp.to_string exn)) ;
  63       raise exn
  64
  65 let clean_exit n =
  66   match !grafite_status with
  67      [] -> exit n
  68    | grafite_status::_ ->
  69       try
  70        let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
  71        LibraryClean.clean_baseuris ~verbose:false [baseuri];
  72        exit n
  73       with GrafiteTypes.Option_error("baseuri", "not found") ->
  74        (* no baseuri ==> nothing to clean yet *)
  75        exit n
  76
  77 let terminate n =
  78  let terminator = String.make 1 (Char.chr 249) in
  79  let prompt =
  80   (match n with
  81      None -> "-1"
  82    | Some n -> string_of_int n) ^ terminator
  83  in
  84   print_endline prompt;
  85   prerr_endline prompt
  86 ;;
  87
  88 let outer_syntax_parser () =
  89  let text = ref "" in
  90  let tag = ref `Do in
  91  let callbacks =
  92   { XmlPushParser.default_callbacks with
  93     XmlPushParser.start_element =
  94      (Some
  95        (fun name attrs ->
  96          match name with
  97             "pgip" -> ()
  98           | "doitem" -> tag := `Do
  99           | "undoitem" -> tag := `Undo
 100           | _ -> assert false)) ;
 101     XmlPushParser.character_data =
 102      (Some (fun s -> text := !text ^ s)) ;
 103     XmlPushParser.end_element =
 104      (Some
 105        (function
 106            "pgip" -> raise (XmlPushParser.Parse_error "EOC")
 107          | "doitem"
 108          | "undoitem" -> ()
 109          | _ -> assert false))
 110   }
 111  in
 112   let parse = XmlPushParser.create_parser callbacks in
 113     try
 114      XmlPushParser.parse parse (`Channel stdin) ;
 115      raise End_of_file
 116     with
 117        XmlPushParser.Parse_error "no element found" -> raise End_of_file
 118      | XmlPushParser.Parse_error "EOC" ->
 119         match !tag with
 120            `Do -> `Do !text
 121          | `Undo ->
 122              try
 123               `Undo (int_of_string !text)
 124              with
 125               Failure _ -> assert false
 126 ;;
 127
 128 let rec interactive_loop () =
 129   (* every loop is terminated by a terminator both on stdout and stderr *)
 130   let interactive_loop n = terminate n; interactive_loop () in
 131   try
 132    match outer_syntax_parser () with
 133       `Undo n ->
 134         let rec drop =
 135          function
 136             0,l -> l
 137           | n,_::l -> drop (n-1,l)
 138           | _,[] -> assert false
 139         in
 140          let to_be_dropped = List.length !lexicon_status - n in
 141          let safe_hd = function [] -> assert false | he::_ -> he in
 142          let cur_lexicon_status = safe_hd !lexicon_status in
 143          let cur_grafite_status = safe_hd !grafite_status in
 144           lexicon_status := drop (to_be_dropped, !lexicon_status) ;
 145           grafite_status := drop (to_be_dropped, !grafite_status) ;
 146           let lexicon_status = safe_hd !lexicon_status in
 147           let grafite_status = safe_hd !grafite_status in
 148            LexiconSync.time_travel
 149             ~present:cur_lexicon_status ~past:lexicon_status;
 150            GrafiteSync.time_travel
 151             ~present:cur_grafite_status ~past:grafite_status;
 152            interactive_loop (Some n)
 153     | `Do command ->
 154         let str = Ulexing.from_utf8_string command in
 155         let watch_statuses lexicon_status grafite_status =
 156          match grafite_status.GrafiteTypes.proof_status with
 157             GrafiteTypes.Incomplete_proof
 158              {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
 159               GrafiteTypes.stack = stack } ->
 160               let open_goals = Continuationals.Stack.open_goals stack in
 161               print_endline
 162                (String.concat "\n"
 163                  (List.map
 164                    (fun i ->
 165                      ApplyTransformation.txt_of_cic_sequent 80 metasenv
 166                       (List.find (fun (j,_,_) -> j=i) metasenv)
 167                    ) open_goals))
 168           | _ -> ()
 169         in
 170         let include_paths =
 171          Helm_registry.get_list Helm_registry.string "matita.includes"
 172         in
 173          run_script str
 174            (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
 175            ~include_paths ~watch_statuses) ;
 176          interactive_loop (Some (List.length !lexicon_status))
 177   with
 178    | GrafiteEngine.Macro (floc,_) ->
 179       let x, y = HExtlib.loc_of_floc floc in
 180        HLog.error
 181         (sprintf "A macro has been found in a script at %d-%d" x y);
 182        interactive_loop None
 183    | Sys.Break -> HLog.error "user break!"; interactive_loop None
 184    | GrafiteTypes.Command_error _ -> interactive_loop None
 185    | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
 186       let x, y = HExtlib.loc_of_floc floc in
 187        HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
 188        interactive_loop None
 189    | End_of_file as exn -> raise exn
 190    | exn -> HLog.error (Printexc.to_string exn); interactive_loop None
 191
 192
 193 let main () =
 194   MatitaInit.initialize_all ();
 195   HLog.set_log_callback
 196    (fun tag msg ->
 197      let s =
 198       match tag with
 199          `Debug -> "<div style='color:blue'>Debug: " ^ msg ^ "</div><br/>\n"
 200        | `Message -> "<div style='color:green'>Info: " ^ msg ^ "</div><br/>\n"
 201        | `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
 202        | `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
 203      in
 204       output_string stderr s;
 205       flush stderr
 206    );
 207   (* must be called after init since args are set by cmdline parsing *)
 208   let system_mode =  Helm_registry.get_bool "matita.system" in
 209   Helm_registry.set_int "matita.verbosity" 0;
 210   let include_paths =
 211    Helm_registry.get_list Helm_registry.string "matita.includes" in
 212   grafite_status := [GrafiteSync.init ()];
 213   lexicon_status :=
 214    [CicNotation2.load_notation ~include_paths
 215      BuildTimeConf.core_notation_script] ;
 216   Sys.catch_break true;
 217   let origcb = HLog.get_log_callback () in
 218   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
 219   let newcb tag s =
 220     match tag with
 221     | `Debug -> ()
 222     | `Message | `Warning | `Error -> origcb tag s
 223   in
 224   HLog.set_log_callback newcb;
 225   let matita_debug = Helm_registry.get_bool "matita.debug" in
 226   try
 227     (try
 228       interactive_loop ()
 229      with
 230       | End_of_file -> ()
 231       | GrafiteEngine.Drop -> clean_exit 1
 232     );
 233     let proof_status,moo_content_rev,metadata,lexicon_content_rev =
 234       match !lexicon_status,!grafite_status with
 235       | ss::_, s::_ ->
 236          s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
 237           ss.LexiconEngine.lexicon_content_rev
 238       | _,_ -> assert false
 239     in
 240     if proof_status <> GrafiteTypes.No_proof then
 241      begin
 242       HLog.error
 243        "there are still incomplete proofs at the end of the script";
 244       clean_exit 2
 245      end
 246     else
 247      begin
 248        let baseuri =
 249         GrafiteTypes.get_string_option
 250          (match !grafite_status with
 251              [] -> assert false
 252            | s::_ -> s) "baseuri" in
 253        let moo_fname =
 254          LibraryMisc.obj_file_of_baseuri
 255            ~must_exist:false ~baseuri ~writable:true
 256        in
 257        let lexicon_fname=
 258          LibraryMisc.lexicon_file_of_baseuri
 259           ~must_exist:false ~baseuri ~writable:true
 260        in
 261        let metadata_fname =
 262         LibraryMisc.metadata_file_of_baseuri
 263           ~must_exist:false ~baseuri ~writable:true
 264        in
 265        GrafiteMarshal.save_moo moo_fname moo_content_rev;
 266        LibraryNoDb.save_metadata metadata_fname metadata;
 267        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
 268        exit 0
 269      end
 270   with
 271   | exn ->
 272       if matita_debug then raise exn;
 273       clean_exit 3