- some depend files fixed

[helm.git] / helm / software / components / binaries / transcript / engine.ml

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index 91633836834a041f773e4f903e4dbf5ba3d57c22..da07dd235489890fa39b5ec31d2aa3e47bcdb415 100644 (file)
--- 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
       | _            ->