Creation of ide/project_file.ml4

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14433 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 153 insertions, 0 deletions

diff --git a/ide/ide.mllib b/ide/ide.mllib
index 8d32605101..8f3a6c353a 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -22,4 +22,5 @@ Coq
 Coq_commands
 Command_windows
 Coqide_ui
+Project_file
 Coqide
diff --git a/ide/minilib.ml b/ide/minilib.ml
index dcadc81f58..71956cf8f6 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -74,3 +74,31 @@ let home =
 
 let coqlib = ref ""
 let coqtop_path = ref ""
+
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p =
+  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+  let n = String.length curdir in
+  if String.length p > n && String.sub p 0 n = curdir then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    p
+
+let strip_path p =
+  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+  let n = String.length cwd in
+  if String.length p > n && String.sub p 0 n = cwd then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    remove_path_dot p
+
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  try
+    Sys.chdir p;
+    let p' = Sys.getcwd () in
+    Sys.chdir current;
+    p'
+  with Sys_error _ ->
+    (* We give up to find a canonical name and just simplify it... *)
+    strip_path p
diff --git a/ide/minilib.mli b/ide/minilib.mli
index 1daa60e1a2..2128b7d867 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -25,3 +25,6 @@ val home : string
 
 val coqlib : string ref
 val coqtop_path : string ref
+
+val strip_path : string -> string
+val canonical_path_name : string -> string
diff --git a/ide/project_file.ml4 b/ide/project_file.ml4
new file mode 100644
index 0000000000..ef39b904c6
--- /dev/null
+++ b/ide/project_file.ml4
@@ -0,0 +1,121 @@
+type target =
+  | ML of string (* ML file : foo.ml -> (ML "foo.ml") *)
+  | MLI of string (* MLI file : foo.mli -> (MLI "foo.mli") *)
+  | ML4 of string (* ML4 file : foo.ml4 -> (ML4 "foo.ml4") *)
+  | MLLIB of string (* MLLIB file : foo.mllib -> (MLLIB "foo.mllib") *)
+  | V of string  (* V file : foo.v -> (V "foo") *)
+  | Arg of string
+  | Special of string * string * string (* file, dependencies, command *)
+  | Subdir of string
+  | Def of string * string (* X=foo -> Def ("X","foo") *)
+  | Include of string
+  | RInclude of string * string (* -R physicalpath logicalpath *)
+
+
+exception Parsing_error
+let rec parse_string = parser
+  | [< '' ' | '\n' | '\t' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string s)
+  | [< >] -> ""
+and parse_string2 = parser
+  | [< ''"' >] -> ""
+  | [< 'c; s >] -> (String.make 1 c)^(parse_string2 s)
+and parse_skip_comment = parser
+  | [< ''\n'; s >] -> s
+  | [< 'c; s >] -> parse_skip_comment s
+  | [< >] -> [< >]
+and parse_args = parser
+  | [< '' ' | '\n' | '\t'; s >] -> parse_args s
+  | [< ''#'; s >] -> parse_args (parse_skip_comment s)
+  | [< ''"'; str = parse_string2; s >] -> ("" ^ str) :: parse_args s
+  | [< 'c; str = parse_string; s >] -> ((String.make 1 c) ^ str) :: (parse_args s)
+  | [< >] -> []
+
+
+let parse f =
+  let c = open_in f in
+  let res = parse_args (Stream.of_channel c) in
+    close_in c;
+    res
+
+let rec process_cmd_line ((project_file,makefile,install,opt) as opts) l = function
+  | [] -> opts,List.rev l
+  | ("-h"|"--help") :: _ ->
+    raise Parsing_error
+  | ("-no-opt"|"-byte") :: r ->
+    process_cmd_line (project_file,makefile,install,false) l r
+  | ("-full"|"-opt") :: r ->
+    process_cmd_line (project_file,makefile,install,true) l r
+  | "-impredicative-set" :: r ->
+    prerr_string "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.\n";
+    process_cmd_line opts (Arg "-impredicative_set" :: l) r
+  | "-no-install" :: r ->
+    if not install then prerr_string "Warning: -no-install sets more than once.\n";
+    process_cmd_line (project_file,makefile,false,opt) l r
+  | "-custom" :: com :: dependencies :: file :: r ->
+    process_cmd_line opts (Special (file,dependencies,com) :: l) r
+  | "-I" :: d :: r ->
+    process_cmd_line opts (Include d :: l) r
+  | "-R" :: p :: lp :: r ->
+    process_cmd_line opts (RInclude (p,lp) :: l) r
+  | ("-I"|"-custom") :: _ ->
+    raise Parsing_error
+  | "-f" :: file :: r ->
+    let () = match project_file with
+      | None -> ()
+      | Some _ -> prerr_string
+	"Warning: Several features will not work with multiple project files.\n"
+    in process_cmd_line (Some file,makefile,install,opt) l ((parse file)@r)
+  | ["-f"] ->
+    raise Parsing_error
+  | "-o" :: file :: r ->
+    let () = match makefile with
+      |None -> ()
+      |Some f ->
+	prerr_string "Warning: Only one output file in genererated. ";
+	prerr_string f; prerr_string " will not.\n"
+    in process_cmd_line (project_file,Some file,install,opt) l r
+  | v :: "=" :: def :: r ->
+    process_cmd_line opts (Def (v,def) :: l) r
+  | "-arg" :: a :: r ->
+    process_cmd_line opts (Arg a :: l) r
+  | f :: r ->
+    process_cmd_line opts ((
+      if Filename.check_suffix f ".v" then V f
+      else if (Filename.check_suffix f ".ml") then ML f
+      else if (Filename.check_suffix f ".ml4") then ML4 f
+      else if (Filename.check_suffix f ".mli") then MLI f
+      else if (Filename.check_suffix f ".mllib") then MLLIB f
+      else Subdir f) :: l) r
+
+let rec post_canonize f =
+  if Filename.basename f = Filename.current_dir_name
+  then let dir = Filename.dirname f in
+    if dir = Filename.current_dir_name then f else post_canonize dir
+  else f
+
+(* Return: ((v,(mli,ml4,ml,mllib),special,subdir),(i_inc,r_inc),(args,defs)) *)
+let rec split_arguments = function
+  | V n :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((Minilib.strip_path n::v,m,o,s),i,d)
+  | ML n :: r ->
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,Minilib.strip_path n::ml,mllib),o,s),i,d)
+  | MLI n :: r ->
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(Minilib.strip_path n::mli,ml4,ml,mllib),o,s),i,d)
+  | ML4 n :: r ->
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,Minilib.strip_path n::ml4,ml,mllib),o,s),i,d)
+  | MLLIB n :: r ->
+      let (v,(mli,ml4,ml,mllib),o,s),i,d = split_arguments r in ((v,(mli,ml4,ml,Minilib.strip_path n::mllib),o,s),i,d)
+  | Special (n,dep,c) :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d)
+  | Subdir n :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d)
+  | Include p :: r ->
+      let t,(i,r),d = split_arguments r in (t,((post_canonize p,Minilib.canonical_path_name p)::i,r),d)
+  | RInclude (p,l) :: r ->
+      let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,Minilib.canonical_path_name p)::r),d)
+  | Def (v,def) :: r ->
+      let t,i,(args,defs) = split_arguments r in (t,i,(args,(v,def)::defs))
+  | Arg a :: r ->
+      let t,i,(args,defs) = split_arguments r in (t,i,(a::args,defs))
+  | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[])