From 7b995596c8b11be95c430646227d01928cc71219 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Dec 2005 14:09:29 +0000 Subject: [PATCH] 1. Several files in grafite that should be in grafite_parser moved there. 2. grafiteEngine is now generalized over the function baseuri_of_script (that associates the baseuri to a .ma file). This function is used to execute the Include statement. However, it seems to me that this shows a problem in the architecture (since the only possible implementation of the function involves using the grafie_parser right now). Modified Files in ocaml: METAS/meta.helm-grafite_parser.src grafite/.depend grafite/Makefile grafite/cicNotation.ml grafite/cicNotation.mli grafite2/disambiguatePp.ml grafite2/disambiguatePp.mli grafite2/grafiteEngine.ml grafite2/grafiteEngine.mli grafite2/grafiteMisc.ml grafite2/grafiteMisc.mli grafite_parser/.depend grafite_parser/Makefile Modified Files in matita: matitaEngine.ml matitaEngine.mli matitaGui.ml matitaInit.ml matitaScript.ml matitacLib.ml matitaclean.ml matitadep.ml Added Files in ocaml: grafite_parser/cicNotation2.ml grafite_parser/cicNotation2.mli grafite_parser/grafiteParser.ml grafite_parser/grafiteParser.mli grafite_parser/grafiteParserMisc.ml grafite_parser/grafiteParserMisc.mli grafite_parser/print_grammar.ml grafite_parser/test_dep.ml grafite_parser/test_parser.ml Removed Files in ocaml: grafite/grafiteParser.ml grafite/grafiteParser.mli grafite/print_grammar.ml grafite/test_dep.ml grafite/test_parser.ml --- helm/matita/matitaEngine.ml | 14 +++++---- helm/matita/matitaEngine.mli | 6 ++-- helm/matita/matitaGui.ml | 8 ++--- helm/matita/matitaInit.ml | 2 +- helm/matita/matitaScript.ml | 14 +++++---- helm/matita/matitacLib.ml | 15 ++++----- helm/matita/matitaclean.ml | 24 ++++++-------- helm/matita/matitadep.ml | 61 ++++++++++++++---------------------- 8 files changed, 65 insertions(+), 79 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index c0f74962d..cfbf74798 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -31,7 +31,7 @@ let debug = false ;; let debug_print = if debug then prerr_endline else ignore ;; let eval_from_stream - ?do_heavy_checks ?include_paths ?clean_baseuri status str cb + ?do_heavy_checks ~include_paths ?clean_baseuri status str cb = try while true do @@ -39,14 +39,15 @@ let eval_from_stream cb !status ast; status := GrafiteEngine.eval_ast + ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths) ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - ?do_heavy_checks ?include_paths ?clean_baseuri !status ast + ?do_heavy_checks ?clean_baseuri !status ast done with End_of_file -> () let eval_from_stream_greedy - ?do_heavy_checks ?include_paths ?clean_baseuri status str cb + ?do_heavy_checks ~include_paths ?clean_baseuri status str cb = while true do print_string "matita> "; @@ -55,15 +56,16 @@ let eval_from_stream_greedy cb !status ast; status := GrafiteEngine.eval_ast + ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths) ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - ?do_heavy_checks ?include_paths ?clean_baseuri !status ast + ?do_heavy_checks ?clean_baseuri !status ast done ;; -let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = +let eval_string ?do_heavy_checks ~include_paths ?clean_baseuri status str = eval_from_stream - ?do_heavy_checks ?include_paths ?clean_baseuri status + ?do_heavy_checks ~include_paths ?clean_baseuri status (Ulexing.from_utf8_string str) (fun _ _ -> ()) let default_options () = no_options diff --git a/helm/matita/matitaEngine.mli b/helm/matita/matitaEngine.mli index 9f8cb44a6..b97361979 100644 --- a/helm/matita/matitaEngine.mli +++ b/helm/matita/matitaEngine.mli @@ -27,13 +27,13 @@ * infos like if the theorem is a duplicate *) val eval_string: ?do_heavy_checks:bool -> - ?include_paths:string list -> + include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status ref -> string -> unit val eval_from_stream: ?do_heavy_checks:bool -> - ?include_paths:string list -> + include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status ref -> Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> @@ -41,7 +41,7 @@ val eval_from_stream: val eval_from_stream_greedy: ?do_heavy_checks:bool -> - ?include_paths:string list -> + include_paths:string list -> ?clean_baseuri:bool -> GrafiteTypes.status ref-> Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteParser.statement -> unit) -> diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 74913dbe6..641ac4c9a 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -70,9 +70,10 @@ let clean_current_baseuri status = let ask_and_save_moo_if_needed parent fname status = let basedir = Helm_registry.get "matita.basedir" in + let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in + let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in let save () = - let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in - let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in + let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev; LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata in @@ -80,13 +81,12 @@ let ask_and_save_moo_if_needed parent fname status = status.GrafiteTypes.proof_status = GrafiteTypes.No_proof then begin - let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in let rc = MatitaGtkMisc.ask_confirmation ~title:"A .moo can be generated" ~message:(Printf.sprintf "%s can be generated for %s.\nShould I generate it?" - (Filename.basename mooname) (Filename.basename fname)) + (Filename.basename moo_fname) (Filename.basename fname)) ~parent () in let b = diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml index 134e00e7c..44f668183 100644 --- a/helm/matita/matitaInit.ml +++ b/helm/matita/matitaInit.ml @@ -85,7 +85,7 @@ let initialize_notation init_status = wants [ConfigurationFile] init_status; if not (already_configured [Notation] init_status) then begin - CicNotation.load_notation BuildTimeConf.core_notation_script; + CicNotation2.load_notation BuildTimeConf.core_notation_script; Notation::init_status end else diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c35fb9307..75773e3fe 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -98,7 +98,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = (* | Incomplete_proof { stack = stack } when not (List.mem user_goal (Continuationals.head_goals stack)) -> let status = - MatitaEngine.eval_ast ~include_paths:include_ + MatitaEngine.eval_ast ~do_heavy_checks:true status (goal_ast user_goal) in let initial_space = if initial_space = "" then "\n" else initial_space @@ -109,9 +109,10 @@ let eval_with_engine guistuff status user_goal parsed_text st = | _ -> initial_space,status,[] in let new_status = GrafiteEngine.eval_ast + ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_) ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic ~disambiguate_command:GrafiteDisambiguate.disambiguate_command - ~include_paths:include_ ~do_heavy_checks:true new_status st + ~do_heavy_checks:true new_status st in let new_aliases = match ex with @@ -163,7 +164,7 @@ let eval_with_engine guistuff status user_goal parsed_text st = try eval_with_engine guistuff status user_goal parsed_text st with - | GrafiteEngine.UnableToInclude what + | GrafiteParserMisc.UnableToInclude what | GrafiteEngine.IncludedFileNotCompiled what as exc -> let compile_needed_and_go_on d = let target = what in @@ -294,6 +295,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac = in let new_status = GrafiteEngine.eval_ast + ~baseuri_of_script:(fun _ -> assert false) ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic ~disambiguate_command:GrafiteDisambiguate.disambiguate_command status ast in @@ -356,7 +358,7 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script match ex with | TA.Command (loc, _) | TA.Tactical (loc, _, _) -> (try - (match GrafiteMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with + (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with | None -> () | Some u -> if not (GrafiteMisc.is_empty u) then @@ -373,8 +375,8 @@ let eval_executable guistuff status user_goal unparsed_text parsed_text script LibraryClean.clean_baseuris ~basedir [u] | `NO -> () | `CANCEL -> raise MatitaTypes.Cancel); - eval_with_engine - guistuff status user_goal parsed_text (TA.Executable (loc, ex)) + eval_with_engine + guistuff status user_goal parsed_text (TA.Executable (loc, ex)) with MatitaTypes.Cancel -> [], 0) | TA.Macro (_,mac) -> eval_macro guistuff status user_goal unparsed_text parsed_text script mac diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index b90190820..b2c3e9a32 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -116,7 +116,7 @@ let rec interactive_loop () = let go () = Helm_registry.load_from BuildTimeConf.matita_conf; - CicNotation.load_notation BuildTimeConf.core_notation_script; + CicNotation2.load_notation BuildTimeConf.core_notation_script; Http_getter.init (); MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); LibraryDb.create_owner_environment (); @@ -152,12 +152,12 @@ let main ~mode = Ulexing.from_utf8_channel (match fname with | "stdin" -> stdin - | fname -> open_in fname) + | fname -> open_in fname) in + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in run_script is - (MatitaEngine.eval_from_stream - ~include_paths:(Helm_registry.get_list Helm_registry.string - "matita.includes") + (MatitaEngine.eval_from_stream ~include_paths ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve"))); let elapsed = Unix.time () -. time in let tm = Unix.gmtime elapsed in @@ -184,8 +184,9 @@ let main ~mode = else begin let basedir = Helm_registry.get "matita.basedir" in - let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in - let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in + let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in + let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in GrafiteMarshal.save_moo moo_fname moo_content_rev; LibraryNoDb.save_metadata metadata_fname metadata; HLog.message diff --git a/helm/matita/matitaclean.ml b/helm/matita/matitaclean.ml index b8c2bb4c2..a5669d2e6 100644 --- a/helm/matita/matitaclean.ml +++ b/helm/matita/matitaclean.ml @@ -30,10 +30,8 @@ module TA = GrafiteAst let main () = let _ = MatitaInit.initialize_all () in - let uris_to_remove = ref [] in - let files_to_remove = ref [] in let basedir = Helm_registry.get "matita.basedir" in - (match Helm_registry.get_list Helm_registry.string "matita.args" with + match Helm_registry.get_list Helm_registry.string "matita.args" with | [ "all" ] -> LibraryDb.clean_owner_environment (); let xmldir = basedir ^ "/xml" in @@ -48,14 +46,15 @@ let main () = exit 0 | [] -> MatitaInit.die_usage () | files -> - List.iter - (fun suri -> + let uris_to_remove = + List.fold_left + (fun uris_to_remove suri -> let uri = try UM.buri_of_uri (UM.uri_of_string suri) with UM.IllFormedUri _ -> - files_to_remove := suri :: !files_to_remove; - let u = GrafiteMisc.baseuri_of_file suri in + let u = + GrafiteParserMisc.baseuri_of_script ~include_paths:[] suri in if String.length u < 5 || String.sub u 0 5 <> "cic:/" then begin HLog.error (sprintf "File %s defines a bad baseuri: %s" suri u); @@ -63,11 +62,6 @@ let main () = end else u in - uris_to_remove := uri :: !uris_to_remove) - files); - LibraryClean.clean_baseuris ~basedir !uris_to_remove; - let moos = - List.map (GrafiteMisc.obj_file_of_script ~basedir) !files_to_remove - in - List.iter HExtlib.safe_remove moos - + uri::uris_to_remove) [] files + in + LibraryClean.clean_baseuris ~basedir uris_to_remove diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml index c40f1636d..c845954ed 100644 --- a/helm/matita/matitadep.ml +++ b/helm/matita/matitadep.ml @@ -34,51 +34,37 @@ let main () = let buri alias = U.buri_of_uri (U.uri_of_string alias) in let resolve alias current_buri = let buri = buri alias in - if buri <> current_buri then Some buri else None - in - let find path = - let rec aux = function - | [] -> close_in (open_in path); path - | p :: tl -> - try - close_in (open_in (p ^ "/" ^ path)); p ^ "/" ^ path - with Sys_error _ -> aux tl - in - let paths = Helm_registry.get_list Helm_registry.string "matita.includes" in - try - aux paths - with Sys_error _ as exc -> - HLog.error ("Unable to read " ^ path); - HLog.error ("opts.include_paths was " ^ String.concat ":" paths); - raise exc - in + if buri <> current_buri then Some buri else None in + let include_paths = + Helm_registry.get_list Helm_registry.string "matita.includes" in MatitaInit.load_configuration_file (); MatitaInit.parse_cmdline (); let basedir = Helm_registry.get "matita.basedir" in List.iter - (fun file -> - let ic = open_in file in + (fun ma_file -> + let ic = open_in ma_file in let istream = Ulexing.from_utf8_channel ic in let dependencies = GrafiteParser.parse_dependencies istream in close_in ic; List.iter - (function - | GrafiteAst.UriDep uri -> + (function + | GrafiteAst.UriDep uri -> let uri = UriManager.string_of_uri uri in - Hashtbl.add uri_deps file uri - | GrafiteAst.BaseuriDep uri -> + Hashtbl.add uri_deps ma_file uri + | GrafiteAst.BaseuriDep uri -> let uri = Http_getter_misc.strip_trailing_slash uri in - Hashtbl.add baseuri_of file uri - | GrafiteAst.IncludeDep path -> + Hashtbl.add baseuri_of ma_file uri + | GrafiteAst.IncludeDep path -> try - let ma_file = if path <> "coq.ma" then find path else path in - let moo_file = GrafiteMisc.obj_file_of_script ~basedir ma_file in - Hashtbl.add include_deps file moo_file + let baseuri = + GrafiteParserMisc.baseuri_of_script ~include_paths path in + let moo_file = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in + Hashtbl.add include_deps ma_file moo_file with Sys_error _ -> HLog.warn - ("Unable to find " ^ path ^ " that is included in " ^ file)) - dependencies) - (Helm_registry.get_list Helm_registry.string "matita.args"); + ("Unable to find " ^ path ^ " that is included in " ^ ma_file) + ) dependencies + ) (Helm_registry.get_list Helm_registry.string "matita.args"); Hashtbl.iter (fun file alias -> let dep = resolve alias (Hashtbl.find baseuri_of file) in @@ -89,13 +75,14 @@ let main () = (LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri:u)) uri_deps; List.iter - (fun file -> - let deps = Hashtbl.find_all include_deps file in + (fun ma_file -> + let deps = Hashtbl.find_all include_deps ma_file in let deps = List.fast_sort Pervasives.compare deps in let deps = HExtlib.list_uniq deps in - let deps = file :: deps in - let moo = GrafiteMisc.obj_file_of_script ~basedir file in + let deps = ma_file :: deps in + let baseuri = Hashtbl.find baseuri_of ma_file in + let moo = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in Printf.printf "%s: %s\n" moo (String.concat " " deps); - Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" file) moo) + Printf.printf "%s: %s\n" (Pcre.replace ~pat:"ma$" ~templ:"mo" ma_file) moo) (Helm_registry.get_list Helm_registry.string "matita.args") -- 2.39.2