X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=da07dd235489890fa39b5ec31d2aa3e47bcdb415;hb=951e8fda6fbef9b4149e37e4d406b2f82fd64a98;hp=91633836834a041f773e4f903e4dbf5ba3d57c22;hpb=0137a346eaaf9ae7a0b23c7a3b4c6628073b7dfb;p=helm.git diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml index 916338368..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} @@ -109,13 +114,13 @@ let make registry = | "gallina8", _ -> T.Gallina8, ".v", [] | "grafite", "" -> T.Grafite "", ".ma", [] | "grafite", s -> T.Grafite s, ".ma", [s] - | _ -> failwith "unknown input type" + | 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, excludes = @@ -136,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 = []; @@ -169,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 -> "" @@ -192,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 @@ -219,16 +241,23 @@ let produce st = 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) -> @@ -246,7 +275,7 @@ 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 = @@ -267,21 +296,21 @@ let produce st = set_items st st.input_package (comment :: global_items); init name; begin match st.input_type with - | T.Grafite "" -> require st name file - | _ -> require st name st.input_package + | 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"; + 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 theory; + require st st.input_package false theory; List.iter (produce st) st.files; commit st st.input_package | _ ->