X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fbinaries%2Ftranscript%2Fengine.ml;h=3184aad369dc353383123c52121a14b7bc7cd0ed;hb=cfb41205e930ede65c1d19ec7ec6f252e0803d55;hp=f4b0c1e3747c4b616ca7e4ad6b3b45aaaa411dbb;hpb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;p=helm.git

diff --git a/helm/software/components/binaries/transcript/engine.ml b/helm/software/components/binaries/transcript/engine.ml
index f4b0c1e37..3184aad36 100644
--- a/helm/software/components/binaries/transcript/engine.ml
+++ b/helm/software/components/binaries/transcript/engine.ml
@@ -23,10 +23,14 @@
  * 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 HG = Http_getter
+module GA = GrafiteAst
+
+module T  = Types
+module G  = Grafite
+module O = Options
 
 type script = {
    name    : string;
@@ -43,8 +47,13 @@ type status = {
    output_base_uri: string;
    input_path: string;
    output_path: string;
-   input_type: string;
+   input_type: T.input_kind;
    output_type: T.output_kind;
+   input_ext: string;
+   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;
@@ -68,13 +77,14 @@ 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_type 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 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
@@ -88,18 +98,31 @@ 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_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]
+	 | 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 = 
+      get_input_type "package.input_type" "package.theory_file"
+   in 
    let st = {
       heading_path = R.get_string "transcript.heading_path";
       heading_lines = R.get_int "transcript.heading_lines";
@@ -109,16 +132,22 @@ let make cwd registry =
       output_base_uri = R.get_string "package.output_base_uri";
       input_path = R.get_string "package.input_path";
       output_path = R.get_string "package.output_path";
-      input_type = R.get_string "package.input_type";
+      input_type = input_type;
       output_type = get_output_type "package.output_type";
-      coercions = get_coercions "package.coercion";
+      input_ext = input_ext;
+      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 = [];
       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;
+      input_path = Filename.concat !O.cwd st.input_path;
+      output_path = Filename.concat !O.cwd st.output_path
    } in
    prerr_endline "reading file names ...";
    let st = set_files st in
@@ -146,7 +175,7 @@ let set_items st name items =
    let contents = List.rev_append items script.contents in
    st.scripts.(i) <- {script with name = name; contents = contents}
    
-let set_heading st name =
+let set_heading st name = 
    let heading = st.heading_path, st.heading_lines in
    set_items st name [T.Heading heading] 
    
@@ -166,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
@@ -185,17 +221,23 @@ let produce st =
       | T.Notation (false, _) -> false
       | _                     -> true
    in
+   let get_items = match st.input_type with
+      | 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
       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, 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))
+	    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))
@@ -210,27 +252,50 @@ 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
-      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
+      let set_includes st name =
+      	 try require st name (List.assoc name st.includes) 
+	 with Not_found -> ()
+      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 = V8Parser.items V8Lexer.token lexbuf in
-         close_in ich; 
+         let items = get_items lexbuf in close_in ich; 
 	 let _, rev_items = X.list_rev_map_filter_fold filter [] items in
 	 let items = List.rev rev_items in
 	 let local_items, global_items = List.partition partition items in
 	 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_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