]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaWiki.ml
...
[helm.git] / 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        NCicLibrary.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