X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=da07dd235489890fa39b5ec31d2aa3e47bcdb415;hb=b519aa529779c0a4625eb43fa9557862d8cc6617;hp=2e81186ea7e91c75e7a51016ea94b20a8ca20eba;hpb=93cc2a2254a2620000377dfc99a7aaedf2b8ec63;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 2e81186ea..da07dd235 100644 --- a/helm/software/components/binaries/transcript/engine.ml +++ b/helm/software/components/binaries/transcript/engine.ml @@ -25,10 +25,11 @@ module R = Helm_registry module X = HExtlib -module T = Types -module G = Grafite module HG = Http_getter +module GA = GrafiteAst +module T = Types +module G = Grafite module O = Options type script = { @@ -52,6 +53,7 @@ type status = { 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; @@ -64,8 +66,9 @@ let default_script = { 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 @@ -82,8 +85,10 @@ let set_files st = | 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 + 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} @@ -104,24 +109,23 @@ let 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" + 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 - | _ -> failwith "unknown output type" + | s -> failwith ("unknown output type: " ^ s) 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 input_type, input_ext, excludes = + get_input_type "package.input_type" "package.theory_file" + in let st = { heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; @@ -137,6 +141,7 @@ let make registry = 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 = []; @@ -170,15 +175,15 @@ let is_ma st name = 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 + 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 = 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 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 -> "" @@ -193,6 +198,22 @@ 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 @@ -213,23 +234,30 @@ let produce st = | _ -> true in let get_items = match st.input_type with - | T.Gallina8 -> Gallina8Parser.items Gallina8Lexer.token - | T.Grafite -> GrafiteParser.items GrafiteLexer.token + | 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) -> + | 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, f)) - | 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) -> @@ -247,15 +275,15 @@ let produce st = | item -> path, Some item in let set_includes st name = - try require st name (List.assoc name st.includes) + 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 ^ st.input_ext) in - let ich = open_in file 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 @@ -266,12 +294,25 @@ let produce st = 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 + 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 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 + 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