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 None : GrafiteTypes.status option ref)
  38 let lexicon_status = (ref None : LexiconEngine.status option ref)
  39
  40 let run_script is eval_function  =
  41   let lexicon_status',grafite_status' =
  42     match !lexicon_status,!grafite_status with
  43     | Some ss, Some 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 := Some lexicon_status'';
  53        grafite_status := Some 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  let opt_exit =
  67   function
  68      None -> ()
  69    | Some n -> exit n
  70  in
  71   match !grafite_status with
  72      None -> opt_exit n
  73    | Some grafite_status ->
  74       try
  75        let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
  76        LibraryClean.clean_baseuris ~verbose:false [baseuri];
  77        opt_exit n
  78       with GrafiteTypes.Option_error("baseuri", "not found") ->
  79        (* no baseuri ==> nothing to clean yet *)
  80        opt_exit n
  81
  82 let terminate () =
  83  let terminator = String.make 1 (Char.chr 249) in
  84   print_endline terminator;
  85   prerr_endline terminator
  86 ;;
  87
  88 let rec interactive_loop () =
  89   (* every loop is terminated by a terminator both on stdout and stderr *)
  90   let interactive_loop () = terminate(); interactive_loop () in
  91   let str = Ulexing.from_utf8_channel stdin in
  92   let watch_statuses lexicon_status grafite_status =
  93    match grafite_status.GrafiteTypes.proof_status with
  94       GrafiteTypes.Incomplete_proof
  95        {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
  96         GrafiteTypes.stack = stack } ->
  97         let open_goals = Continuationals.Stack.open_goals stack in
  98         print_endline
  99          (String.concat "\n"
 100            (List.map
 101              (fun i ->
 102                ApplyTransformation.txt_of_cic_sequent 80 metasenv
 103                 (List.find (fun (j,_,_) -> j=i) metasenv)
 104              ) open_goals))
 105     | _ -> ()
 106   in
 107   let include_paths =
 108    Helm_registry.get_list Helm_registry.string "matita.includes" in
 109   try
 110     run_script str
 111       (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
 112       ~include_paths ~watch_statuses) ;
 113     interactive_loop ()
 114   with
 115   | GrafiteEngine.Macro (floc,_) ->
 116      let x, y = HExtlib.loc_of_floc floc in
 117       HLog.error
 118        (sprintf "A macro has been found in a script at %d-%d" x y);
 119       interactive_loop ()
 120   | Sys.Break -> HLog.error "user break!"; interactive_loop ()
 121   | GrafiteTypes.Command_error _ -> interactive_loop ()
 122   | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
 123      let x, y = HExtlib.loc_of_floc floc in
 124       HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
 125       interactive_loop ()
 126   | End_of_file as exn -> raise exn
 127   | exn -> HLog.error (Printexc.to_string exn); interactive_loop ()
 128
 129
 130 let main () =
 131   MatitaInit.initialize_all ();
 132   (* must be called after init since args are set by cmdline parsing *)
 133   let system_mode =  Helm_registry.get_bool "matita.system" in
 134   Helm_registry.set_int "matita.verbosity" 0;
 135   let include_paths =
 136    Helm_registry.get_list Helm_registry.string "matita.includes" in
 137   grafite_status := Some (GrafiteSync.init ());
 138   lexicon_status :=
 139    Some (CicNotation2.load_notation ~include_paths
 140     BuildTimeConf.core_notation_script);
 141   Sys.catch_break true;
 142   let origcb = HLog.get_log_callback () in
 143   let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
 144   let newcb tag s =
 145     match tag with
 146     | `Debug -> ()
 147     | `Message | `Warning | `Error -> origcb tag s
 148   in
 149   HLog.set_log_callback newcb;
 150   let matita_debug = Helm_registry.get_bool "matita.debug" in
 151   try
 152     (try
 153       interactive_loop ()
 154      with
 155       | End_of_file -> ()
 156       | GrafiteEngine.Drop -> clean_exit (Some 1)
 157     );
 158     let proof_status,moo_content_rev,metadata,lexicon_content_rev =
 159       match !lexicon_status,!grafite_status with
 160       | Some ss, Some s ->
 161          s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
 162           ss.LexiconEngine.lexicon_content_rev
 163       | _,_ -> assert false
 164     in
 165     if proof_status <> GrafiteTypes.No_proof then
 166      begin
 167       HLog.error
 168        "there are still incomplete proofs at the end of the script";
 169       clean_exit (Some 2)
 170      end
 171     else
 172      begin
 173        let baseuri =
 174         GrafiteTypes.get_string_option
 175          (match !grafite_status with
 176              None -> assert false
 177            | Some s -> s) "baseuri" in
 178        let moo_fname =
 179          LibraryMisc.obj_file_of_baseuri
 180            ~must_exist:false ~baseuri ~writable:true
 181        in
 182        let lexicon_fname=
 183          LibraryMisc.lexicon_file_of_baseuri
 184           ~must_exist:false ~baseuri ~writable:true
 185        in
 186        let metadata_fname =
 187         LibraryMisc.metadata_file_of_baseuri
 188           ~must_exist:false ~baseuri ~writable:true
 189        in
 190        GrafiteMarshal.save_moo moo_fname moo_content_rev;
 191        LibraryNoDb.save_metadata metadata_fname metadata;
 192        LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
 193        exit 0
 194      end
 195   with
 196   | exn ->
 197       if matita_debug then raise exn;
 198       clean_exit (Some 3)