first matitadep snapshot

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 57893de42a9f16ff6280f9df743b2d2604fd1a46..c7b250a3b4789ae97a3e212e25019f7f9c205a8b 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -46,7 +46,7 @@ CCMOS =                               \
        matitacLib.cmo
 
 
-all: matita matitac matitatop cicbrowser
+all: matita matitac matitatop cicbrowser matitadep
 
 updater: $(LIB_DEPS)
        $(OCAMLC) $(PKGS) -linkpkg -o $@ updater.ml
@@ -56,7 +56,7 @@ CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
 CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
 LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
 LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
-opt: matita.opt matitac.opt cicbrowser.opt
+opt: matita.opt matitac.opt cicbrowser.opt matitadep.opt
 else
 opt:
        @echo "Native code compilation is disabled"
@@ -75,6 +75,11 @@ matitac.opt: $(LIBX_DEPS) $(CCMXS) matitac.ml
 matitatop: matitatop.ml $(LIB_DEPS) $(CCMOS)
        $(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
 
+matitadep: matitadep.ml $(LIB_DEPS) $(CCMOS)
+       $(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $<
+matitadep.opt: matitadep.ml $(LIB_DEPS) $(CCMXS)
+       $(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $<
+
 cicbrowser: matita
        @test -f $@ || ln -s $< $@
 cicbrowser.opt: matita.opt
@@ -96,7 +101,8 @@ matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
 clean:
        rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o   \
                matita matita.opt matitac matitac.opt   \
-               cicbrowser cicbrowser.opt
+               cicbrowser cicbrowser.opt       \
+               matitadep matitadep.opt
 distclean: clean
        rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
        rm -f config.log config.status Makefile buildTimeConf.ml

diff --git a/helm/matita/matitaDb.ml b/helm/matita/matitaDb.ml
index d4f5d01b1979246528a51eee128d46e4e175d214..423fa2b5a0b7ddba659d8f9c742f2ef2eda47283 100644 (file)
--- a/helm/matita/matitaDb.ml
+++ b/helm/matita/matitaDb.ml
@@ -146,13 +146,7 @@ let remove_uri uri =
     let l = ref [] in
     Mysql.iter rc (fun a -> match a.(0) with None ->()|Some a -> l := a:: !l);
     let l = List.sort Pervasives.compare !l in
-    let rec uniq = function 
-      | [] -> []
-      | h::[] -> [h]
-      | h1::h2::tl when h1 = h2 -> uniq (h2 :: tl) 
-      | h1::tl (* when h1 <> h2 *) -> h1 :: uniq tl
-    in
-    uniq l
+    MatitaMisc.list_uniq l
   with
     exn -> raise exn (* no errors should be accepted *)
 

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a28cdedf85ac214b3d56b854bb82ce454be9b19b..354b18ae54cd3156f72a4cdb9b6028c5056e6a80 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -224,7 +224,14 @@ let generate_projections uri fields status =
  
 let eval_command status cmd =
   match cmd with
-  | TacticAst.Set (loc, name, value) -> set_option status name value
+  | TacticAst.Set (loc, name, value) -> 
+      let value = 
+        if name = "baseuri" then
+          MatitaMisc.strip_trailing_slash value
+        else
+          value
+      in
+      set_option status name value
   | TacticAst.Drop loc -> raise Drop
   | TacticAst.Qed loc ->
       let uri, metasenv, bo, ty = 

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 73fdd4c54e2ef6a2c5bcc605ea593410f64549fa..ab077d9238d60d0dbb2ef14278fc160ada0277d9 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -57,6 +57,10 @@ let strip_trailing_blanks =
   let rex = Pcre.regexp "\\s*$" in
   fun s -> Pcre.replace ~rex s
 
+let strip_trailing_slash =
+  let rex = Pcre.regexp "/$" in
+  fun s -> Pcre.replace ~rex s
+
 let empty_mathml () =
   DomMisc.domImpl#createDocument ~namespaceURI:(Some DomMisc.mathml_ns)
     ~qualifiedName:(Gdome.domString "math") ~doctype:None
@@ -194,3 +198,13 @@ let unopt = function None -> failwith "unopt: None" | Some v -> v
 
 let image_path n = sprintf "%s/%s" BuildTimeConf.images_dir n
 
+let end_ma_RE = Pcre.regexp "\\.ma$"
+let obj_file_of_script f = Pcre.replace ~rex:end_ma_RE ~templ:".moo" f
+
+let rec list_uniq = function 
+  | [] -> []
+  | h::[] -> [h]
+  | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
+  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
+
+let end_ma_RE = Pcre.regexp "\\.ma$"

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index acbe3bac6c4a606c8904a48e49b60a41d42acc56..31efae031dc53eb9f7734958a61205d9dd4dc304 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -39,6 +39,9 @@ val is_proof_object: string -> bool
 val append_phrase_sep: string -> string
 
 val strip_trailing_blanks: string -> string
+val strip_trailing_slash: string -> string
+
+val list_uniq: 'a list -> 'a list (* uniq unix filter on lists *)
 
   (** @raise Failure *)
 val unopt: 'a option -> 'a
@@ -89,4 +92,5 @@ val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment
 
   (** given the base name of an image, returns its full path *)
 val image_path: string -> string
+val obj_file_of_script: string -> string
 

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index d57d211e21edde02b8c20beae7c5468f068e9bbb..4d04d371c8ea07f4de3d08122d13474d8f05c0fb 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -141,6 +141,7 @@ let main ~mode =
      begin
        MatitaLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
+         close_out (open_out (MatitaMisc.obj_file_of_script fname));
        exit 0
      end
   with 

diff --git a/helm/matita/matitadep.ml b/helm/matita/matitadep.ml
new file mode 100644 (file)
index 0000000..df6cff2
--- /dev/null
+++ b/helm/matita/matitadep.ml
@@ -0,0 +1,63 @@
+module TA = TacticAst 
+module U = UriManager
+
+let deps = Hashtbl.create (Array.length Sys.argv)
+let baseuri = ref []
+let aliases = Hashtbl.create (Array.length Sys.argv)
+
+(*
+let uri_of_alias = function 
+  | Ident_alias (_, uri)
+  | Symbol_alias (_, _, uri) 
+  | Number_alias (_, uri) -> uri 
+*)
+
+let buri alias = 
+  U.buri_of_uri (U.uri_of_string alias)
+
+let resolve alias =
+  try
+    Some (snd(List.find (fun (u, f) -> u = (buri alias)) !baseuri))
+  with
+  | Not_found -> None
+ 
+  (*** TODO MANCANO LE URI VERBATIM DENTRO GLI AST DEI TERMINI ****)
+
+let main () =
+  for i = 1 to Array.length Sys.argv - 1 do
+    let file = Sys.argv.(i) in
+    let ic = open_in file in
+    let stms = CicTextualParser2.parse_statements (Stream.of_channel ic) in
+    close_in ic;
+    let stms = 
+      List.iter 
+        (function
+        | TA.Executable (_, TA.Command (_, TA.Set (_, "baseuri", uri))) ->
+            let uri = MatitaMisc.strip_trailing_slash uri in
+            baseuri := (uri, file) :: !baseuri
+        | TA.Executable (_, TA.Command 
+            (_, TA.Alias (_, TA.Ident_alias(_, uri)))) -> 
+              Hashtbl.add aliases file uri
+        | _ -> ()) 
+      stms 
+    in
+    Hashtbl.iter 
+      (fun file alias -> 
+        let dep = resolve alias in
+        match dep with 
+        | None -> ()
+        | Some d -> Hashtbl.add deps file d)
+      aliases;
+  done;
+  for i = 1 to Array.length Sys.argv - 1 do
+    let file = Sys.argv.(i) in
+    let deps = Hashtbl.find_all deps file in
+    let deps = List.fast_sort Pervasives.compare deps in
+    let deps = MatitaMisc.list_uniq deps in
+    let deps = file :: deps in
+    Printf.printf "%s: %s\n" (MatitaMisc.obj_file_of_script file)
+      (String.concat " " deps)
+  done
+  
+
+let _ = main ()