]> matita.cs.unibo.it Git - helm.git/commitdiff
implementation of the make algorithm, still unfinished.
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 3 Jan 2008 10:13:04 +0000 (10:13 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 3 Jan 2008 10:13:04 +0000 (10:13 +0000)
to be integrated with matitac to drop our beloved developments.

helm/software/make/main.ml [new file with mode: 0644]
helm/software/make/make.ml [new file with mode: 0644]
helm/software/make/make.mli [new file with mode: 0644]
helm/software/make/test/a.c [new file with mode: 0644]
helm/software/make/test/b.c [new file with mode: 0644]
helm/software/make/test/c.c [new file with mode: 0644]
helm/software/make/test/d.c [new file with mode: 0644]
helm/software/make/test/e.c [new file with mode: 0644]

diff --git a/helm/software/make/main.ml b/helm/software/make/main.ml
new file mode 100644 (file)
index 0000000..df20a35
--- /dev/null
@@ -0,0 +1,34 @@
+
+module F = struct
+        type source_object = string
+        type target_object = string
+        let string_of_source_object s = s
+        let string_of_target_object s = s
+        let target_of s = s ^ ".o"
+        let build t =
+          print_string ("build "^t^"\n"); flush stdout;
+          ignore(Unix.system ("touch "^target_of t))
+        ;;
+        let mtime_of_source_object s = 
+          try Some (Unix.stat s).Unix.st_mtime
+          with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = s -> 
+            prerr_endline ("Source file not found: "^s);assert false
+        ;;
+        let mtime_of_target_object t = 
+          try Some (Unix.stat t).Unix.st_mtime
+          with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = t -> None
+        ;;
+end
+
+module M = Make.Make(F)
+
+let deps = [
+  "a.c", [ "b.c"; "d.c" ];
+  "b.c", [ "c.c"; "d.c" ];
+  "c.c", [];
+  "d.c", ["e.c"];
+  "e.c", [];
+  ]
+;;
+
+M.make deps;;
diff --git a/helm/software/make/make.ml b/helm/software/make/make.ml
new file mode 100644 (file)
index 0000000..c243d79
--- /dev/null
@@ -0,0 +1,103 @@
+
+module type Format = sig
+
+        type source_object
+        type target_object
+
+        val target_of : source_object -> target_object
+        val string_of_source_object : source_object -> string
+        val string_of_target_object : target_object -> string
+
+        val build : source_object -> unit
+
+        val mtime_of_source_object : source_object -> float option
+        val mtime_of_target_object : target_object -> float option
+end
+
+module Make = functor (F:Format) -> struct
+
+  let prerr_endline _ = ();;
+
+  let younger_s_t a b = 
+    match F.mtime_of_source_object a, F.mtime_of_target_object b with
+    | Some a, Some b -> a < b
+    | _ -> false (* XXX check if correct *)
+  ;;
+  let younger_t_t a b = 
+    match F.mtime_of_target_object a, F.mtime_of_target_object b with
+    | Some a, Some b -> a < b
+    | _ -> false (* XXX check if correct *)
+  ;;
+
+  let is_built t = younger_s_t t (F.target_of t);;
+
+  let rec needs_build deps compiled (t,dependencies) =
+    prerr_endline ("Checking if "^F.string_of_source_object t^" needs to be built");
+    if List.mem t compiled then
+      (prerr_endline "already compiled";
+      false)
+    else
+    if not (is_built t) then
+      (prerr_endline (F.string_of_source_object t^
+       " is not built, thus needs to be built");
+      true)
+    else
+    try
+      let unsat =
+        List.find
+          (needs_build deps compiled) 
+          (List.map (fun x -> x, List.assoc x deps) dependencies)
+      in
+        prerr_endline 
+         (F.string_of_source_object t^" depends on "^F.string_of_source_object (fst unsat)^
+         " that needs to be built, thus needs to be built");
+        true
+    with Not_found ->
+      try 
+        let unsat = 
+          List.find (younger_t_t (F.target_of t)) (List.map F.target_of dependencies)
+        in
+          prerr_endline 
+           (F.string_of_source_object t^" depends on "^F.string_of_target_object
+           unsat^" and "^F.string_of_source_object t^".o is younger than "^
+           F.string_of_target_object unsat^", thus needs to be built");
+          true
+      with Not_found -> false
+  ;;
+
+  let is_buildable compiled deps (t,dependencies) =
+    prerr_endline ("Checking if "^F.string_of_source_object t^" is buildable");
+    let b = needs_build deps compiled (t,dependencies) in
+    if not b then
+      (prerr_endline (F.string_of_source_object t^
+       " does not need to be built, thus it not buildable");
+      false)
+    else
+    try  
+      let unsat =
+        List.find (needs_build deps compiled) 
+          (List.map (fun x -> x, List.assoc x deps) dependencies)
+      in
+        prerr_endline 
+          (F.string_of_source_object t^" depends on "^
+          F.string_of_source_object (fst unsat)^
+          " that needs build, thus is not buildable");
+        false
+    with Not_found -> 
+      prerr_endline 
+        ("None of "^F.string_of_source_object t^
+        " dependencies needs to be built, thus it is buildable");
+      true
+  ;;
+
+  let rec make compiled deps = 
+    let todo = List.filter (is_buildable compiled deps) deps in
+    if todo <> [] then 
+      (List.iter F.build (List.map fst todo);
+       make (compiled@List.map fst todo) deps)
+  ;;
+
+  let make deps = make [] deps
+
+end
+  
diff --git a/helm/software/make/make.mli b/helm/software/make/make.mli
new file mode 100644 (file)
index 0000000..8830a83
--- /dev/null
@@ -0,0 +1,18 @@
+
+module type Format =
+  sig
+    type source_object
+    type target_object
+    val target_of : source_object -> target_object
+    val string_of_source_object : source_object -> string
+    val string_of_target_object : target_object -> string
+    val build : source_object -> unit
+    val mtime_of_source_object : source_object -> float option
+    val mtime_of_target_object : target_object -> float option
+  end
+
+module Make :
+  functor (F : Format) ->
+    sig
+      val make : (F.source_object * F.source_object list) list -> unit
+    end
diff --git a/helm/software/make/test/a.c b/helm/software/make/test/a.c
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/software/make/test/b.c b/helm/software/make/test/b.c
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/software/make/test/c.c b/helm/software/make/test/c.c
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/software/make/test/d.c b/helm/software/make/test/d.c
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/software/make/test/e.c b/helm/software/make/test/e.c
new file mode 100644 (file)
index 0000000..e69de29