- transcript: we have now two styles of mma's from grafite:

[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 4504d2999e9f7b51646152dc316a1ac86c2cc6b6..91633836834a041f773e4f903e4dbf5ba3d57c22 100644 (file)
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -49,6 +49,8 @@ type status = {
    input_type: T.input_kind;
    output_type: T.output_kind;
    input_ext: string;
+   remove_lines: int;
+   excludes: string list;
    includes: (string * string) list;
    coercions: (string * string) list;
    files: string list;
@@ -74,12 +76,13 @@ let load_registry registry =
 let set_files st =
    let eof ich = try Some (input_line ich) with End_of_file -> None in
    let trim l = Filename.chop_extension (Str.string_after l 2) in 
-   let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.input_ext in
+   let cmd = Printf.sprintf "cd %s && find -name '*%s'" st.input_path st.input_ext in
    let ich = Unix.open_process_in cmd in
-   let rec aux files =
-      match eof ich with
-         | None   -> List.rev files
-        | Some l -> aux (trim l :: files)
+   let rec aux files = match eof ich with
+      | 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 
    let files = aux [] in
    let _ = Unix.close_process_in ich in
@@ -101,10 +104,11 @@ 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"
+   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]
         | _          -> failwith "unknown input type"
    in
    let get_output_type key =
@@ -114,14 +118,12 @@ let make registry =
         | _             -> failwith "unknown output type"
    in
    load_registry registry;
-   let input_type, input_ext = get_input_type "package.input_type" in 
-   let heading_lines = match input_type with
-      | T.Grafite -> 0
-      | _         -> R.get_int "transcript.heading_lines"
-   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 = heading_lines;
+      heading_lines = R.get_int "transcript.heading_lines";
       input_package = R.get_string "package.input_name";
       output_package = R.get_string "package.output_name";
       input_base_uri = R.get_string "package.input_base_uri";
@@ -131,6 +133,8 @@ let make registry =
       input_type = input_type;
       output_type = get_output_type "package.output_type";
       input_ext = input_ext;
+      remove_lines = R.get_int "package.heading_lines";
+      excludes = excludes;
       includes = get_pairs "package.include";
       coercions = get_pairs "package.coercion";
       files = [];
@@ -208,8 +212,8 @@ 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
@@ -236,15 +240,22 @@ let produce st =
         | T.Section (b, id, _) as item ->
            let path = if b then id :: path else List.tl path in
            path, Some item
+        | T.Verbatim s                 ->
+           let pat, templ = st.input_base_uri, st.output_base_uri in
+           path, Some (T.Verbatim (Pcre.replace ~pat ~templ s)) 
         | 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_ext) in
-      let ich = open_in file 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 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 
          let items = get_items lexbuf in close_in ich; 
@@ -254,12 +265,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 file
+           | _            -> require st name 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
+   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;
+         List.iter (produce st) st.files;
+         commit st st.input_package
+      | _            ->
+         List.iter (produce st) st.files;
+         commit st st.input_package