X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=4504d2999e9f7b51646152dc316a1ac86c2cc6b6;hb=3bfc56cd9b5afe52c3abfbef886ce82efa3bb3a3;hp=66c6c33be85a2b53e16352a7c41b57e77ee2a8d0;hpb=55444711ececb62f0a93f2a064f64c3b27f744e2;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 66c6c33be..4504d2999 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -23,18 +23,21 @@ * http://cs.unibo.it/helm/. *) -module R = Helm_registry -module X = HExtlib -module T = Types -module G = Grafite +module R = Helm_registry +module X = HExtlib +module T = Types +module G = Grafite +module HG = Http_getter + +module O = Options type script = { - name: string; + name : string; + is_ma : bool; contents: T.items } type status = { - helm_dir: string; heading_path: string; heading_lines: int; input_package: string; @@ -43,7 +46,10 @@ type status = { output_base_uri: string; input_path: string; output_path: string; - script_ext: string; + input_type: T.input_kind; + output_type: T.output_kind; + input_ext: string; + includes: (string * string) list; coercions: (string * string) list; files: string list; requires: (string * string) list; @@ -51,7 +57,7 @@ type status = { } let default_script = { - name = ""; contents = [] + name = ""; is_ma = false; contents = [] } let default_scripts = 2 @@ -67,8 +73,8 @@ let load_registry registry = let set_files st = let eof ich = try Some (input_line ich) with End_of_file -> None in - let trim l = Filename.chop_extension (Str.string_after l 2) in - let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.script_ext in + let trim l = Filename.chop_extension (Str.string_after l 2) in + let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_ext in let ich = Unix.open_process_in cmd in let rec aux files = match eof ich with @@ -85,29 +91,57 @@ let set_requires st = {st with requires = requires} let init () = - let default_registry = "transcript" in - load_registry default_registry + let transcript_dir = Filename.dirname Sys.argv.(0) in + let default_registry = Filename.concat transcript_dir "transcript" in + let matita_registry = Filename.concat !O.cwd "matita" in + load_registry default_registry; + load_registry matita_registry; + HG.init () let make registry = let id x = x in - let get_coercions = R.get_list (R.pair id id) in + let get_pairs = R.get_list (R.pair id id) in + let get_input_type key = + match R.get_string key with + | "gallina8" -> T.Gallina8, ".v" + | "grafite" -> T.Grafite, ".ma" + | _ -> failwith "unknown input type" + in + let get_output_type key = + match R.get_string key with + | "procedural" -> T.Procedural + | "declarative" -> T.Declarative + | _ -> failwith "unknown output type" + in load_registry registry; + let input_type, input_ext = get_input_type "package.input_type" in + let heading_lines = match input_type with + | T.Grafite -> 0 + | _ -> R.get_int "transcript.heading_lines" + in let st = { - helm_dir = R.get_string "transcript.helm_dir"; heading_path = R.get_string "transcript.heading_path"; - heading_lines = R.get_int "transcript.heading_lines"; + heading_lines = heading_lines; input_package = R.get_string "package.input_name"; output_package = R.get_string "package.output_name"; input_base_uri = R.get_string "package.input_base_uri"; output_base_uri = R.get_string "package.output_base_uri"; input_path = R.get_string "package.input_path"; output_path = R.get_string "package.output_path"; - script_ext = R.get_string "package.script_type"; - coercions = get_coercions "package.coercion"; + input_type = input_type; + output_type = get_output_type "package.output_type"; + input_ext = input_ext; + includes = get_pairs "package.include"; + coercions = get_pairs "package.coercion"; files = []; requires = []; scripts = Array.make default_scripts default_script } in + let st = {st with + heading_path = Filename.concat !O.cwd st.heading_path; + input_path = Filename.concat !O.cwd st.input_path; + output_path = Filename.concat !O.cwd st.output_path + } in prerr_endline "reading file names ..."; let st = set_files st in let st = set_requires st in @@ -123,20 +157,21 @@ let get_index st name = | Some i, _ | _, Some i -> i | None, None -> failwith "not enought script entries" +let is_ma st name = + let i = get_index st name in + let script = st.scripts.(i) in + st.scripts.(i) <- {script with is_ma = true} + let set_items st name items = let i = get_index st name in let script = st.scripts.(i) in let contents = List.rev_append items script.contents in - st.scripts.(i) <- {name = name; contents = contents} + st.scripts.(i) <- {script with name = name; contents = contents} -let set_heading st name = - let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in +let set_heading st name = + let heading = st.heading_path, st.heading_lines in set_items st name [T.Heading heading] -let set_baseuri st name = - let baseuri = Filename.concat st.output_base_uri name in - set_items st name [T.BaseUri baseuri] - let require st name inc = set_items st name [T.Include inc] @@ -149,36 +184,44 @@ let make_path path = let make_prefix path = String.concat "__" (List.rev path) ^ "__" +let make_script_name st script name = + let ext = if script.is_ma then ".ma" else ".mma" in + Filename.concat st.output_path (name ^ ext) + let commit st name = let i = get_index st name in let script = st.scripts.(i) in let path = Filename.concat st.output_path (Filename.dirname name) in - let name = Filename.concat st.output_path (name ^ ".ma") in + let name = make_script_name st script name in let cmd = Printf.sprintf "mkdir -p %s" path in let _ = Sys.command cmd in let och = open_out name in - G.commit och script.contents; + G.commit st.output_type och script.contents; close_out och; - st.scripts.(i) <- default_script - + st.scripts.(i) <- default_script + let produce st = - let init name = set_heading st name; set_baseuri st name in + let init name = set_heading st name in let partition = function | T.Coercion (false, _) | T.Notation (false, _) -> false | _ -> true in + let get_items = match st.input_type with + | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token + | T.Grafite -> GrafiteParser.items GrafiteLexer.token + in let produce st name = let in_base_uri = Filename.concat st.input_base_uri name in let out_base_uri = Filename.concat st.output_base_uri name in let filter path = function - | T.Inline (b, k, obj, p) -> + | T.Inline (b, k, obj, p, f) -> let obj, p = if b then Filename.concat (make_path path) obj, make_prefix path else obj, p in let s = obj ^ G.string_of_inline_kind k in - path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p)) + path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p, f)) | T.Include s -> begin try path, Some (T.Include (List.assoc s st.requires)) @@ -195,24 +238,28 @@ let produce st = path, Some item | item -> path, Some item in + let set_includes st name = + try require st name (List.assoc name st.includes) + with Not_found -> () + in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path (name ^ st.script_ext) in + let file = Filename.concat st.input_path (name ^ st.input_ext) in let ich = open_in file in let lexbuf = Lexing.from_channel ich in try - let items = V8Parser.items V8Lexer.token lexbuf in - close_in ich; + let items = get_items lexbuf in close_in ich; let _, rev_items = X.list_rev_map_filter_fold filter [] items in let items = List.rev rev_items in let local_items, global_items = List.partition partition items in let comment = T.Line (Printf.sprintf "From %s" name) in if global_items <> [] then set_items st st.input_package (comment :: global_items); - init name; require st name st.input_package; + init name; require st name st.input_package; set_includes st name; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in + is_ma st st.input_package; init st.input_package; require st st.input_package "preamble"; List.iter (produce st) st.files; commit st st.input_package