]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/matitaEngine.ml
minor additions to standard library
[helm.git] / matita / matita / matitaEngine.ml
1 (* Copyright (C) 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$ *)
27
28 module G = GrafiteAst
29 open Printf
30
31 class status baseuri =
32   object
33     inherit GrafiteTypes.status baseuri
34     inherit ApplyTransformation.status
35   end
36
37 exception TryingToAdd of string Lazy.t
38 exception EnrichedWithStatus of exn * status
39 exception AlreadyLoaded of string Lazy.t
40 exception FailureCompiling of string * exn
41 exception CircularDependency of string
42
43 let debug = false ;;
44 let debug_print = if debug then prerr_endline else ignore ;;
45
46 let slash_n_RE = Pcre.regexp "\\n" ;;
47
48 let first_line = ref true ;;
49
50 let cases_or_induction_context stack =
51     match stack with
52      [] -> false
53     | (_g,_t,_k,_tag,p)::_tl -> try
54                             let s = List.assoc "context" p in
55                             s = "cases" || s = "induction"
56                            with
57                             Not_found -> false
58 ;;
59
60 let has_focused_goal stack =
61     match stack with
62      [] -> false
63     | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
64 ;;
65
66 let get_indentation status _statement =
67   let base_ind =
68     match status#stack with
69       [] -> 0
70     | s -> List.length(s) * 2
71   in
72     if cases_or_induction_context status#stack then
73       (
74         if has_focused_goal status#stack then
75             base_ind + 2
76         else
77             base_ind
78       )
79     else
80       base_ind
81 ;;
82
83 let pp_ind s n =
84   let rec aux s n =
85     match n with
86       0 -> s
87     | n -> " " ^ (aux s (n-1))
88   in
89     aux s n
90
91 let write_ast_to_file status fname statement =
92   let indentation = get_indentation status statement in
93   let str = match statement with
94       G.Comment _ -> GrafiteAstPp.pp_statement status statement
95                        ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
96     | G.Executable (_,code) ->
97       (
98         match code with
99           G.NTactic _ -> GrafiteAstPp.pp_statement status statement
100                            ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
101         | G.NCommand (_,cmd) ->
102           (
103               match cmd with
104                 | G.NObj (_,obj,_) ->
105                         (
106                         match obj with
107                             NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
108                                    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
109                         |   _ -> ""
110                         )
111                 | G.NQed _ -> GrafiteAstPp.pp_statement status statement
112                                    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
113                 | _ -> ""
114           )
115         | _ -> ""
116       )
117   in
118     if str <> "" then
119       (
120         let s = pp_ind str indentation in
121         let flaglist = if !first_line = false then [Open_wronly; Open_append; Open_creat]
122           else (first_line := false; [Open_wronly; Open_trunc; Open_creat])
123         in
124         let out_channel =
125           open_out_gen flaglist 0o0644 fname in
126         let _ = output_string out_channel ((if str.[0] <> '\n' then s else str) ^ "\n") in
127         let _ = close_out out_channel in
128         str
129       )
130     else
131       str
132 ;;
133
134 let pp_ast_statement status stm ~fname =
135   let stm = write_ast_to_file status (fname ^ ".parsed.ma") stm in
136   if stm <> "" then
137   (
138     let stm = Pcre.replace ~rex:slash_n_RE stm in
139     let stm =
140       if String.length stm > 50 then String.sub stm 0 50 ^ " ..."
141       else stm
142     in
143     HLog.debug ("Executing: ``" ^ stm ^ "''")
144   )
145   else
146     HLog.debug ("Executing: `` Unprintable statement ''")
147 ;;
148
149 let clean_exit baseuri exn =
150   LibraryClean.clean_baseuris ~verbose:false [baseuri];
151   raise (FailureCompiling (baseuri,exn))
152 ;;
153
154 let cut prefix s =
155   let lenp = String.length prefix in
156   let lens = String.length s in
157   assert (lens > lenp);
158   assert (String.sub s 0 lenp = prefix);
159   String.sub s lenp (lens-lenp)
160 ;;
161
162 let print_string =
163   let indent = ref 0 in
164   let print_string ~right_justify s =
165     let ss =
166       match right_justify with
167         None -> ""
168       | Some (ss,len_ss) ->
169         let i = 80 - !indent - len_ss - String.length s in
170         if i > 0 then String.make i ' ' ^ ss else ss
171     in
172     assert (!indent >=0);
173     print_string (String.make !indent ' ' ^ s ^ ss) in
174   fun enter ?right_justify s ->
175     if enter then (print_string ~right_justify s; incr indent) else (decr indent; print_string ~right_justify s)
176 ;;
177
178 let pp_times ss fname rc big_bang big_bang_u big_bang_s =
179   if not (Helm_registry.get_bool "matita.verbose") then
180     let { Unix.tms_utime = u ; Unix.tms_stime = s} = Unix.times () in
181     let r = Unix.gettimeofday () -. big_bang in
182     let u = u -. big_bang_u in
183     let s = s -. big_bang_s in
184     let extra = try Sys.getenv "BENCH_EXTRA_TEXT" with Not_found -> "" in
185     let rc =
186       if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
187     let times =
188       let fmt t =
189         let seconds = int_of_float t in
190         let cents = int_of_float ((t -. floor t) *. 100.0) in
191         let minutes = seconds / 60 in
192         let seconds = seconds mod 60 in
193         Printf.sprintf "%dm%02d.%02ds" minutes seconds cents
194       in
195       Printf.sprintf "%s %s %s" (fmt r) (fmt u) (fmt s)
196     in
197     let s = Printf.sprintf "%-14s %s %s\n" rc times extra in
198     print_string false ~right_justify:(s,31) ss;
199     flush stdout;
200     HLog.message ("Compilation of "^Filename.basename fname^": "^rc)
201 ;;
202
203 let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
204   let baseuri = status#baseuri in
205   let new_aliases,new_status =
206     GrafiteDisambiguate.eval_with_new_aliases status
207       (fun status ->
208          let time0 = Unix.gettimeofday () in
209          let status =
210            GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
211              (text,prefix_len,ast) in
212          let time1 = Unix.gettimeofday () in
213          HLog.debug ("... grafite_engine done in " ^ string_of_float (time1 -. time0) ^ "s");
214          status
215       ) in
216   let _,intermediate_states =
217     List.fold_left
218       (fun (status,acc) (k,value) ->
219          let v = GrafiteAst.description_of_alias value in
220          let b =
221            try
222              let NReference.Ref (uri,_) = NReference.reference_of_string v in
223              NUri.baseuri_of_uri uri = baseuri
224            with
225              NReference.IllFormedReference _ ->
226              false (* v is a description, not a URI *)
227          in
228          if b then
229            status,acc
230          else
231            let status =
232              GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
233                GrafiteAst.WithPreferences [k,value]
234            in
235            status, (status ,Some (k,value))::acc
236       ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
237   in
238   (new_status,None)::intermediate_states
239 ;;
240
241 let baseuri_of_script ~include_paths fname =
242   try Librarian.baseuri_of_script ~include_paths fname
243   with
244     Librarian.NoRootFor _ ->
245     HLog.error ("The included file '"^fname^"' has no root file,");
246     HLog.error "please create it.";
247     raise (Failure ("No root file for "^fname))
248   | Librarian.FileNotFound _ ->
249     raise (Failure ("File not found: "^fname))
250 ;;
251
252 (* given a path to a ma file inside the include_paths, returns the
253    new include_paths associated to that file *)
254 let read_include_paths ~include_paths:_ file =
255  try 
256    let root, _buri, _fname, _tgt = 
257      Librarian.baseuri_of_script ~include_paths:[] file in 
258    let includes =
259     try
260      Str.split (Str.regexp " ") 
261       (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
262     with Not_found -> []
263    in
264    let rc = root :: includes in
265     List.iter (HLog.debug) rc; rc
266   with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
267     []
268 ;;
269
270 let rec get_ast status ~compiling ~asserted ~include_paths strm =
271   match GrafiteParser.parse_statement status strm with
272     (GrafiteAst.Executable
273        (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
274     ->
275     let already_included = NCicLibrary.get_transitively_included status in
276     let asserted,_ =
277       assert_ng ~already_included ~compiling ~asserted ~include_paths
278         mafilename
279     in
280     asserted,cmd
281   | cmd -> asserted,cmd
282
283 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
284   let matita_debug = Helm_registry.get_bool "matita.debug" in
285   let rec loop asserted status str =
286     let asserted,stop,status,str =
287       try
288         let cont =
289           try Some (get_ast status ~compiling ~asserted ~include_paths str)
290           with End_of_file -> None in
291         match cont with
292         | None -> asserted, true, status, str
293         | Some (asserted,ast) ->
294           cb status ast;
295           let new_statuses =
296             eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
297           let status =
298             match new_statuses with
299               [s,None] -> s
300             | _::(_,Some (_,value))::_ ->
301               raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
302             | _ -> assert false in
303           (* CSC: complex patch to re-build the lexer since the tokens may
304              have changed. Note: this way we loose look-ahead tokens.
305              Hence the "include" command must be terminated (no look-ahead) *)
306           let str =
307             match ast with
308               (GrafiteAst.Executable
309                  (_,GrafiteAst.NCommand
310                     (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
311               GrafiteParser.parsable_statement status
312                 (GrafiteParser.strm_of_parsable str)
313             | _ -> str
314           in
315           asserted, false, status, str
316       with exn when not matita_debug ->
317         raise (EnrichedWithStatus (exn, status))
318     in
319     if stop then asserted,status else loop asserted status str
320   in
321   loop asserted status str
322
323 and compile ~compiling ~asserted ~include_paths fname =
324   if List.mem fname compiling then raise (CircularDependency fname);
325   let compiling = fname::compiling in
326   let matita_debug = Helm_registry.get_bool "matita.debug" in
327   let root,baseuri,fname,_tgt =
328     Librarian.baseuri_of_script ~include_paths fname in
329   if Http_getter_storage.is_read_only baseuri then assert false;
330   (* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
331   let status = new status baseuri in
332   (*CSC: bad, one imperative bit is still there!
333          to be moved into functional status *)
334   NCicMetaSubst.pushmaxmeta ();
335   let ocamldirname = Filename.dirname fname in
336   let ocamlfname = Filename.chop_extension (Filename.basename fname) in
337   let status,ocamlfname =
338     Common.modname_of_filename status false ocamlfname in
339   let ocamlfname = ocamldirname ^ "/" ^ ocamlfname ^ ".ml" in
340   let status = OcamlExtraction.open_file status ~baseuri ocamlfname in
341   let big_bang = Unix.gettimeofday () in
342   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
343     Unix.times ()
344   in
345   let time = Unix.time () in
346   let cc =
347     let rex = Str.regexp ".*opt$" in
348     if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt"
349     else "matitac" in
350   let s = Printf.sprintf "%s %s" cc (cut (root^"/") fname) in
351   try
352     (* cleanup of previously compiled objects *)
353     if (not (Http_getter_storage.is_empty ~local:true baseuri))
354     then begin
355       HLog.message ("baseuri " ^ baseuri ^ " is not empty");
356       HLog.message ("cleaning baseuri " ^ baseuri);
357       LibraryClean.clean_baseuris [baseuri];
358     end;
359     HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri);
360     if not (Helm_registry.get_bool "matita.verbose") then
361       (print_string true (s ^ "\n"); flush stdout);
362     (* we dalay this error check until we print 'matitac file ' *)
363     assert (Http_getter_storage.is_empty ~local:true baseuri);
364     (* create dir for XML files *)
365     if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
366               ~default:false)
367     then
368       HExtlib.mkdir
369         (Filename.dirname
370            (Http_getter.filename ~local:true ~writable:true (baseuri ^
371                                                              "foo.con")));
372     let buf =
373       GrafiteParser.parsable_statement status
374         (Ulexing.from_utf8_channel (open_in fname))
375     in
376     let print_cb =
377       if not (Helm_registry.get_bool "matita.verbose") then fun _ _ -> ()
378       else pp_ast_statement ~fname
379     in
380     let asserted, status =
381       eval_from_stream ~compiling ~asserted ~include_paths status buf print_cb in
382     let status = OcamlExtraction.close_file status in
383     let elapsed = Unix.time () -. time in
384     (if Helm_registry.get_bool "matita.moo" then begin
385         GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
386           status
387       end;
388      let tm = Unix.gmtime elapsed in
389      let sec = string_of_int tm.Unix.tm_sec ^ "''" in
390      let min =
391        if tm.Unix.tm_min > 0 then (string_of_int tm.Unix.tm_min^"' ") else ""
392      in
393      let hou =
394        if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour^"h ") else ""
395      in
396      HLog.message
397        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
398      pp_times s fname true big_bang big_bang_u big_bang_s;
399      (*CSC: bad, one imperative bit is still there!
400             to be moved into functional status *)
401      NCicMetaSubst.pushmaxmeta ();
402      (* MATITA 1.0: debbo fare time_travel sulla ng_library?
403           LexiconSync.time_travel
404             ~present:lexicon_status ~past:initial_lexicon_status;
405      *)
406      asserted)
407   with
408   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
409   | exn when not matita_debug ->
410     (* MATITA 1.0: debbo fare time_travel sulla ng_library?
411            LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
412      *       *)
413     (*CSC: bad, one imperative bit is still there!
414            to be moved into functional status *)
415     NCicMetaSubst.pushmaxmeta ();
416     pp_times s fname false big_bang big_bang_u big_bang_s;
417     clean_exit baseuri exn
418
419 and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
420   let root,baseuri,fullmapath,_ =
421     Librarian.baseuri_of_script ~include_paths mapath in
422   if List.mem fullmapath asserted then asserted,false
423   else
424     begin
425       let include_paths =
426         let includes =
427           try
428             Str.split (Str.regexp " ")
429               (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
430           with Not_found -> []
431         in
432         root::includes @
433         Helm_registry.get_list Helm_registry.string "matita.includes" in
434       let baseuri = NUri.uri_of_string baseuri in
435       let ngtime_of baseuri =
436         let ngpath = NCicLibrary.ng_path_of_baseuri baseuri in
437         try
438           Some (Unix.stat ngpath).Unix.st_mtime
439         with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
440       let matime =
441         try (Unix.stat fullmapath).Unix.st_mtime
442         with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = fullmapath -> assert false
443       in
444       let ngtime = ngtime_of baseuri in
445       let asserted,to_be_compiled =
446         match ngtime with
447           Some ngtime ->
448           let preamble = GrafiteTypes.Serializer.dependencies_of baseuri in
449           let asserted,children_bad =
450             List.fold_left
451               (fun (asserted,b) mapath ->
452                  let asserted,b1 =
453                    try
454                      assert_ng ~already_included ~compiling ~asserted ~include_paths
455                        mapath
456                    with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
457                      asserted, true
458                  in
459                  asserted, b || b1
460                            || let _,baseuri,_,_ =
461                                 (*CSC: bug here? include_paths should be empty and
462                                        mapath should be absolute *)
463                                 Librarian.baseuri_of_script ~include_paths mapath in
464                            let baseuri = NUri.uri_of_string baseuri in
465                            (match ngtime_of baseuri with
466                               Some child_ngtime -> child_ngtime > ngtime
467                             | None -> assert false)
468               ) (asserted,false) preamble
469           in
470           asserted, children_bad || matime > ngtime
471         | None -> asserted,true
472       in
473       if not to_be_compiled then fullmapath::asserted,false
474       else
475       if List.mem baseuri already_included then
476         (* maybe recompiling it I would get the same... *)
477         raise (AlreadyLoaded (lazy mapath))
478       else
479         let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
480         fullmapath::asserted,true
481     end
482 ;;
483
484 let assert_ng ~include_paths mapath =
485   snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
486          mapath)
487 let get_ast status ~include_paths strm =
488   snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)