X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=2e81186ea7e91c75e7a51016ea94b20a8ca20eba;hb=93cc2a2254a2620000377dfc99a7aaedf2b8ec63;hp=92c3c73b469c8b9138e0aebf8cd2d3cec29cb43b;hpb=c5e25191f05bb2662fc738bfb2742eb03b941510;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 92c3c73b4..2e81186ea 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -23,29 +23,43 @@ * http://cs.unibo.it/helm/. *) -module R = Helm_registry +module R = Helm_registry +module X = HExtlib +module T = Types +module G = Grafite +module HG = Http_getter + +module O = Options type script = { - name: string; - contents: Types.items + name : string; + is_ma : bool; + contents: T.items } type status = { - helm_dir: string; heading_path: string; heading_lines: int; - package: string; - base_uri: string; + input_package: string; + output_package: string; + input_base_uri: string; + 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; + remove_lines: int; + excludes: string list; + includes: (string * string) list; + coercions: (string * string) list; files: string list; requires: (string * string) list; scripts: script array } let default_script = { - name = ""; contents = [] + name = ""; is_ma = false; contents = [] } let default_scripts = 2 @@ -61,13 +75,14 @@ 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 - | None -> List.rev files - | Some l -> aux (trim l :: files) + let rec aux files = match eof ich with + | None -> List.rev files + | Some l -> + let l = trim l in + if List.mem l st.excludes then aux files else aux (l :: files) in let files = aux [] in let _ = Unix.close_process_in ich in @@ -79,24 +94,59 @@ 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_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 excludes = match input_type with + | T.Grafite -> ["theory"] + | T.Gallina8 -> [] + 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"; - package = R.get_string "package.name"; - base_uri = R.get_string "package.base_uri"; + 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"; + input_type = input_type; + output_type = get_output_type "package.output_type"; + input_ext = input_ext; + remove_lines = R.get_int "package.heading_lines"; + excludes = excludes; + 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 @@ -112,44 +162,116 @@ 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} - -let set_heading st name = - let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in - set_items st name [Types.Heading heading] + st.scripts.(i) <- {script with name = name; contents = contents} -let set_baseuri st name = - let baseuri = Filename.concat st.base_uri name in - set_items st name [Types.BaseUri baseuri] +let set_heading st name = + let heading = st.heading_path, st.heading_lines in + set_items st name [T.Heading heading] +let require st name inc = + set_items st name [T.Include inc] + +let get_coercion st str = + try List.assoc str st.coercions with Not_found -> "" + +let make_path path = + List.fold_left Filename.concat "" (List.rev 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 - Grafite.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, 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, f)) + | T.Include s -> + begin + try path, Some (T.Include (List.assoc s st.requires)) + with Not_found -> path, None + end + | T.Coercion (b, obj) -> + let str = get_coercion st obj in + if str <> "" then path, Some (T.Coercion (b, str)) else + let base_uri = if b then out_base_uri else in_base_uri in + let s = obj ^ G.string_of_inline_kind T.Con in + path, Some (T.Coercion (b, Filename.concat base_uri s)) + | 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.script_ext) 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; - init name; set_items st name items; commit st name + 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; 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 - init st.package; List.iter (produce st) st.files; commit st st.package + 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