X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=027b03575589bbd6ce3a1a747698b854798ddf3f;hb=916c558005ed665c62699a7a4c5347870c8a3efb;hp=120d31fdd3ffa2da105e152a96a7cd81c62c608d;hpb=f620bf94af6c347926ed1c2328462efab7018b21;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 120d31fdd..027b03575 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -27,7 +27,7 @@ module R = Helm_registry module X = HExtlib module T = Types module G = Grafite -module HP = Http_getter +module HG = Http_getter module O = Options @@ -46,8 +46,11 @@ type status = { output_base_uri: string; input_path: string; output_path: string; - input_type: string; + input_type: T.input_kind; output_type: T.output_kind; + input_ext: string; + remove_lines: int; + includes: (string * string) list; coercions: (string * string) list; files: string list; requires: (string * string) list; @@ -71,8 +74,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.input_type 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 @@ -94,11 +97,17 @@ let init () = let matita_registry = Filename.concat !O.cwd "matita" in load_registry default_registry; load_registry matita_registry; - HP.init () + 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 @@ -106,6 +115,7 @@ let make registry = | _ -> failwith "unknown output type" in load_registry registry; + let input_type, input_ext = get_input_type "package.input_type" in let st = { heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; @@ -115,16 +125,20 @@ let make registry = 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"; - input_type = R.get_string "package.input_type"; + input_type = input_type; output_type = get_output_type "package.output_type"; - coercions = get_coercions "package.coercion"; + input_ext = input_ext; + remove_lines = R.get_int "package.heading_lines"; + 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; - output_path = Filename.concat !O.cwd st.output_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 @@ -152,7 +166,7 @@ let set_items st name items = let contents = List.rev_append items script.contents in st.scripts.(i) <- {script with name = name; contents = contents} -let set_heading st name = +let set_heading st name = let heading = st.heading_path, st.heading_lines in set_items st name [T.Heading heading] @@ -191,6 +205,10 @@ let produce st = | 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 @@ -216,22 +234,32 @@ let produce st = | T.Section (b, id, _) as item -> let path = if b then id :: path else List.tl path in path, Some item + | T.Verbatim s -> + let pat, templ = st.input_base_uri, st.output_base_uri in + path, Some (T.Verbatim (Pcre.replace ~pat ~templ s)) | item -> path, Some item in + let set_includes st name = + try require st name (List.assoc name st.includes) + with Not_found -> () + in + let rec remove_lines ich n = + if n > 0 then let _ = input_line ich in remove_lines ich (pred n) + in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path (name ^ st.input_type) in + let file = Filename.concat st.input_path (name ^ st.input_ext) in let ich = open_in file in + begin try remove_lines ich st.remove_lines with End_of_file -> () end; 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