unificatiom hints with premises

[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 f4b0c1e3747c4b616ca7e4ad6b3b45aaaa411dbb..ccf07423f6dd5cc14b5af35f6ede71356a5bbc2f 100644 (file)
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -23,10 +23,13 @@
  * http://cs.unibo.it/helm/.
  *)
 
-module R = Helm_registry
-module X = HExtlib
-module T = Types
-module G = Grafite
+module R  = Helm_registry
+module X  = HExtlib
+module T  = Types
+module G  = Grafite
+module HG = Http_getter
+
+module O = Options
 
 type script = {
    name    : string;
@@ -45,6 +48,7 @@ type status = {
    output_path: string;
    input_type: string;
    output_type: T.output_kind;
+   includes: (string * string) list;
    coercions: (string * string) list;
    files: string list;
    requires: (string * string) list;
@@ -88,11 +92,14 @@ let set_requires st =
 let init () = 
    let transcript_dir = Filename.dirname Sys.argv.(0) in
    let default_registry = Filename.concat transcript_dir "transcript" in
-   load_registry default_registry
+   let matita_registry = Filename.concat !O.cwd "matita" in
+   load_registry default_registry;
+   load_registry matita_registry;
+   HG.init ()
 
-let make cwd registry =
+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_output_type key =
       match R.get_string key with
          | "procedural"  -> T.Procedural
@@ -111,14 +118,15 @@ let make cwd registry =
       output_path = R.get_string "package.output_path";
       input_type = R.get_string "package.input_type";
       output_type = get_output_type "package.output_type";
-      coercions = get_coercions "package.coercion";
+      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 cwd st.heading_path;
-      output_path = Filename.concat cwd st.output_path;
+      heading_path = Filename.concat !O.cwd st.heading_path;
+      output_path = Filename.concat !O.cwd st.output_path;
    } in
    prerr_endline "reading file names ...";
    let st = set_files st in
@@ -189,13 +197,13 @@ 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)      -> 
+         | 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))
+           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))
@@ -212,6 +220,10 @@ let produce st =
            path, Some item
         | item                         -> path, Some item
       in
+      let set_includes st name =
+        try require st name (List.assoc name st.includes) 
+        with Not_found -> ()
+      in
       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
       let file = Filename.concat st.input_path (name ^ st.input_type) in
       let ich = open_in file in
@@ -225,7 +237,7 @@ 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;
+        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