- hExtlib: new function "list_assoc_all"

[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..3184aad369dc353383123c52121a14b7bc7cd0ed 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;
@@ -109,13 +111,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 +138,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 = [];
@@ -192,6 +195,13 @@ 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 map = function
+      | "nodefaults" -> GA.IPNoDefaults
+      | s            -> 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,13 +229,15 @@ 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))
+           let full_s = Filename.concat in_base_uri s in
+           let params = params @ get_iparams st (Filename.concat name obj) in
+           path, Some (T.Inline (b, k, full_s, p, f, params))
         | T.Include s                  ->
            begin 
               try path, Some (T.Include (List.assoc s st.requires))