X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=da07dd235489890fa39b5ec31d2aa3e47bcdb415;hb=2bcf927f58bac034b8758173cdbd16cb7475de36;hp=9824426daf5497dceb4c62ec5590b3323a65cf1c;hpb=137a822662f81efbbeac7ddc833fc9ffe252a70e;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 9824426da..da07dd235 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -23,18 +23,22 @@ * http://cs.unibo.it/helm/. *) -module R = Helm_registry -module X = HExtlib +module R = Helm_registry +module X = HExtlib +module HG = Http_getter +module GA = GrafiteAst + module T = Types module G = Grafite +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 +47,13 @@ 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; + remove_lines: int; + excludes: string list; + includes: (string * string) list; + iparams: (string * string) list; coercions: (string * string) list; files: string list; requires: (string * string) list; @@ -51,13 +61,14 @@ type status = { } let default_script = { - name = ""; contents = [] + name = ""; is_ma = false; contents = [] } let default_scripts = 2 +let suffix = ".conf.xml" + let load_registry registry = - let suffix = ".conf.xml" in let registry = if Filename.check_suffix registry suffix then registry else registry ^ suffix @@ -67,14 +78,17 @@ 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) - in + 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 + if !O.sources = [] || List.mem l !O.sources then aux (l :: files) else + aux files + in let files = aux [] in let _ = Unix.close_process_in ich in {st with files = files} @@ -85,15 +99,34 @@ 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 key1 key2 = + match R.get_string key1, R.get_string key2 with + | "gallina8", _ -> T.Gallina8, ".v", [] + | "grafite", "" -> T.Grafite "", ".ma", [] + | "grafite", s -> T.Grafite s, ".ma", [s] + | s, _ -> failwith ("unknown input type: " ^ s) + in + let get_output_type key = + match R.get_string key with + | "procedural" -> T.Procedural + | "declarative" -> T.Declarative + | s -> failwith ("unknown output type: " ^ s) + in load_registry registry; + let input_type, input_ext, excludes = + get_input_type "package.input_type" "package.theory_file" + 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"; input_package = R.get_string "package.input_name"; @@ -102,12 +135,23 @@ 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"; - 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; + remove_lines = R.get_int "package.heading_lines"; + excludes = excludes; + includes = get_pairs "package.include"; + iparams = get_pairs "package.inline"; + 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,22 +167,23 @@ 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 contents = List.rev_append (X.list_uniq items) script.contents in + 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] +let require st name moo inc = + set_items st name [T.Include (moo, inc)] let get_coercion st str = try List.assoc str st.coercions with Not_found -> "" @@ -149,72 +194,125 @@ 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 get_iparams st name = + let debug debug = GA.IPDebug debug in + let map = function + | "comments" -> GA.IPComments + | "nodefaults" -> GA.IPNoDefaults + | "coercions" -> GA.IPCoercions + | "cr" -> GA.IPCR + | s -> + try Scanf.sscanf s "debug-%u" debug with + | Scanf.Scan_failure _ + | Failure _ + | End_of_file -> + failwith ("unknown inline parameter: " ^ s) + in + List.map map (X.list_assoc_all name st.iparams) + 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, params) -> 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)) - | T.Include s -> + in + let ext = G.string_of_inline_kind k in + let s = Filename.concat in_base_uri (obj ^ ext) in + let params = + params @ + get_iparams st "*" @ + get_iparams st ("*" ^ ext) @ + get_iparams st (Filename.concat name obj) + in + path, Some (T.Inline (b, k, s, p, f, params)) + | T.Include (moo, s) -> begin - try path, Some (T.Include (List.assoc s st.requires)) + try path, Some (T.Include (moo, List.assoc s st.requires)) with Not_found -> path, None end | T.Coercion (b, obj) -> let str = get_coercion st obj in - let base_uri = - if str <> "" then str else - if b then out_base_uri else in_base_uri - 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 - Printf.eprintf "processing file name: %s ...\n" name; flush stderr; - let file = Filename.concat st.input_path (name ^ st.script_ext) in - let ich = open_in file in + let set_includes st name = + try require st name true (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 in + let ich = open_in (file ^ st.input_ext) 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; - set_items st name local_items; commit st name + init name; + begin match st.input_type with + | T.Grafite "" -> require st name false file + | _ -> require st name false st.input_package + end; + 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.input_package; - List.iter (produce st) st.files; - commit st st.input_package + is_ma st st.input_package; + init st.input_package; require st st.input_package false "preamble"; + match st.input_type with + | T.Grafite "" -> + List.iter (produce st) st.files + | T.Grafite s -> + let theory = Filename.concat st.input_path s in + require st st.input_package false theory; + List.iter (produce st) st.files; + commit st st.input_package + | _ -> + List.iter (produce st) st.files; + commit st st.input_package