ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mli

The .mli only acknowledges the current API. I'm not guilty your honor!

3 files changed, 281 insertions, 0 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index c73ae9b904..71f728291e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -32,3 +32,4 @@ CUnix
 Envars
 Aux_file
 Monad
+CoqProject_file
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
new file mode 100644
index 0000000000..d32273bc20
--- /dev/null
+++ b/lib/coqProject_file.ml4
@@ -0,0 +1,212 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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") *)
+  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
+  | V of string  (* V file : foo.v -> (V "foo") *)
+  | Arg of string
+  | Special of string * string * bool * string
+    (* file, dependencies, is_phony, command *)
+  | Subdir of string
+  | Def of string * string (* X=foo -> Def ("X","foo") *)
+  | MLInclude of string (* -I physicalpath *)
+  | Include of string * string (* -Q physicalpath logicalpath *)
+  | RInclude of string * string (* -R physicalpath logicalpath *)
+
+type install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+  | UnspecInstall
+
+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)
+  | [< >] -> raise Parsing_error
+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 orig_dir ((project_file,makefile,install,opt) as opts) l = function
+  | [] -> opts, l
+  | ("-h"|"--help") :: _ ->
+    raise Parsing_error
+  | ("-no-opt"|"-byte") :: r ->
+    process_cmd_line orig_dir (project_file,makefile,install,false) l r
+  | ("-full"|"-opt") :: r ->
+    process_cmd_line orig_dir (project_file,makefile,install,true) l r
+  | "-impredicative-set" :: r ->
+    Feedback.msg_warning (Pp.str "Please now use \"-arg -impredicative-set\" instead of \"-impredicative-set\" alone to be more uniform.");
+    process_cmd_line orig_dir opts (Arg "-impredicative-set" :: l) r
+  | "-no-install" :: r ->
+    Feedback.msg_warning (Pp.(++) (Pp.str "Option -no-install is deprecated.") (Pp.(++) (Pp.spc ()) (Pp.str "Use \"-install none\" instead")));
+    process_cmd_line orig_dir (project_file,makefile,NoInstall,opt) l r
+  | "-install" :: d :: r ->
+    if install <> UnspecInstall then Feedback.msg_warning (Pp.str "-install sets more than once.");
+    let install =
+      match d with
+	| "user" -> UserInstall
+	| "none" -> NoInstall
+	| "global" -> TraditionalInstall
+	| _ -> Feedback.msg_warning (Pp.(++) (Pp.str "invalid option '") (Pp.(++) (Pp.str d) (Pp.str "' passed to -install.")));
+          install
+    in
+    process_cmd_line orig_dir (project_file,makefile,install,opt) l r
+  | "-custom" :: com :: dependencies :: file :: r ->
+    Feedback.msg_warning (Pp.app
+    (Pp.str "Please now use \"-extra[-phony] result deps command\" instead of \"-custom command deps result\".")
+    (Pp.pr_arg Pp.str "It follows makefile target declaration order and has a clearer semantic.")
+    );
+    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
+  | "-extra" :: file :: dependencies :: com :: r ->
+    process_cmd_line orig_dir opts (Special (file,dependencies,false,com) :: l) r
+  | "-extra-phony" :: target :: dependencies :: com :: r ->
+    process_cmd_line orig_dir opts (Special (target,dependencies,true,com) :: l) r
+  | "-Q" :: d :: lp :: r ->
+    process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r
+  | "-I" :: d :: r ->
+    process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r
+  | "-R" :: p :: lp :: r ->
+    process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r
+  | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ ->
+    raise Parsing_error
+  | "-f" :: file :: r ->
+    let file = CUnix.remove_path_dot (CUnix.correct_path file orig_dir) in
+    let () = match project_file with
+      | None -> ()
+      | Some _ -> Feedback.msg_warning (Pp.str
+	"Several features will not work with multiple project files.")
+    in
+    let (opts',l') = process_cmd_line (Filename.dirname file) (Some file,makefile,install,opt) l (parse file) in
+      process_cmd_line orig_dir opts' l' r
+  | ["-f"] ->
+    raise Parsing_error
+  | "-o" :: file :: r ->
+      begin try
+	let _ = String.index file '/' in
+	  raise Parsing_error
+      with Not_found ->
+	let () = match makefile with
+	  |None -> ()
+	  |Some f ->
+	     Feedback.msg_warning (Pp.(++) (Pp.str "Only one output file is genererated. ") (Pp.(++) (Pp.str f) (Pp.str " will not be.")))
+	in process_cmd_line orig_dir (project_file,Some file,install,opt) l r
+      end
+  | v :: "=" :: def :: r ->
+    process_cmd_line orig_dir opts (Def (v,def) :: l) r
+  | "-arg" :: a :: r ->
+    process_cmd_line orig_dir opts (Arg a :: l) r
+  | f :: r ->
+      let f = CUnix.correct_path f orig_dir in
+	process_cmd_line orig_dir 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 if (Filename.check_suffix f ".mlpack") then MLPACK f
+	  else Subdir f) :: l) r
+
+let process_cmd_line orig_dir opts l args =
+  let (opts, l) = process_cmd_line orig_dir opts l args in
+  opts, List.rev l
+
+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,mlpack),special,subdir),(ml_inc,q_inc,r_inc),(args,defs)) *)
+let split_arguments args =
+  List.fold_right
+    (fun a ((v,(mli,ml4,ml,mllib,mlpack as m),o,s as t),
+            (ml_inc,q_inc,r_inc as i),(args,defs as d)) ->
+     match a with
+     | V n ->
+        ((CUnix.remove_path_dot n::v,m,o,s),i,d)
+     | ML n ->
+        ((v,(mli,ml4,CUnix.remove_path_dot n::ml,mllib,mlpack),o,s),i,d)
+     | MLI n ->
+        ((v,(CUnix.remove_path_dot n::mli,ml4,ml,mllib,mlpack),o,s),i,d)
+     | ML4 n ->
+        ((v,(mli,CUnix.remove_path_dot n::ml4,ml,mllib,mlpack),o,s),i,d)
+     | MLLIB n ->
+        ((v,(mli,ml4,ml,CUnix.remove_path_dot n::mllib,mlpack),o,s),i,d)
+     | MLPACK n ->
+        ((v,(mli,ml4,ml,mllib,CUnix.remove_path_dot n::mlpack),o,s),i,d)
+     | Special (n,dep,is_phony,c) ->
+        ((v,m,(n,dep,is_phony,c)::o,s),i,d)
+     | Subdir n ->
+        ((v,m,o,n::s),i,d)
+     | MLInclude p ->
+        let ml_new = (CUnix.remove_path_dot (post_canonize p),
+                      CUnix.canonical_path_name p) in
+        (t,(ml_new::ml_inc,q_inc,r_inc),d)
+     | Include (p,l) ->
+        let q_new = (CUnix.remove_path_dot (post_canonize p),l,
+		     CUnix.canonical_path_name p) in
+        (t,(ml_inc,q_new::q_inc,r_inc),d)
+     | RInclude (p,l) ->
+        let r_new = (CUnix.remove_path_dot (post_canonize p),l,
+		     CUnix.canonical_path_name p) in
+        (t,(ml_inc,q_inc,r_new::r_inc),d)
+     | Def (v,def) ->
+        (t,i,(args,(v,def)::defs))
+     | Arg a ->
+        (t,i,(a::args,defs)))
+    args (([],([],[],[],[],[]),[],[]),([],[],[]),([],[]))
+
+let read_project_file f =
+  split_arguments
+    (snd (process_cmd_line (Filename.dirname f) (Some f, None, NoInstall, true) [] (parse f)))
+
+let args_from_project file project_files default_name =
+  let build_cmd_line ml_inc i_inc r_inc args =
+    List.fold_right (fun (_,i) o -> "-I" :: i :: o) ml_inc
+      (List.fold_right (fun (_,l,i) o -> "-Q" :: i :: l :: o) i_inc
+        (List.fold_right (fun (_,l,p) o -> "-R" :: p :: l :: o) r_inc
+	  (List.fold_right (fun a o -> parse_args (Stream.of_string a) @ o) args [])))
+  in try
+      let (fname,(_,(ml_inc,i_inc,r_inc),(args,_))) = List.hd project_files in
+	fname, build_cmd_line ml_inc i_inc r_inc args
+    with Failure _ ->
+      let rec find_project_file dir = try
+	let fname = Filename.concat dir default_name in
+	let ((v_files,_,_,_),(ml_inc,i_inc,r_inc),(args,_)) =
+          read_project_file fname in
+	fname, build_cmd_line ml_inc i_inc r_inc args
+      with Sys_error s ->
+	let newdir = Filename.dirname dir in
+	  if dir = newdir then "",[] else find_project_file newdir
+      in find_project_file (Filename.dirname file)
+
+(* vim:set ft=ocaml: *)
diff --git a/lib/coqProject_file.mli b/lib/coqProject_file.mli
new file mode 100644
index 0000000000..36513dbde5
--- /dev/null
+++ b/lib/coqProject_file.mli
@@ -0,0 +1,68 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+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") *)
+  | MLPACK of string (* MLLIB file : foo.mlpack -> (MLLIB "foo.mlpack") *)
+  | V of string  (* V file : foo.v -> (V "foo") *)
+  | Arg of string
+  | Special of string * string * bool * string
+    (* file, dependencies, is_phony, command *)
+  | Subdir of string
+  | Def of string * string (* X=foo -> Def ("X","foo") *)
+  | MLInclude of string (* -I physicalpath *)
+  | Include of string * string (* -Q physicalpath logicalpath *)
+  | RInclude of string * string (* -R physicalpath logicalpath *)
+
+type install =
+  | NoInstall
+  | TraditionalInstall
+  | UserInstall
+  | UnspecInstall
+
+exception Parsing_error
+
+val args_from_project : 
+           string ->
+           (string *
+            ('a *
+             (('b * string) list * ('c * string * string) list *
+              ('d * string * string) list) *
+             (string list * 'e)))
+           list -> string -> string * string list
+
+val read_project_file :
+           string ->
+           (string list *
+            (string list * string list * string list * string list *
+             string list) *
+            (string * string * bool * string) list * string list) *
+           ((string * string) list * (string * string * string) list *
+            (string * string * string) list) *
+           (string list * (string * string) list)
+
+val process_cmd_line :
+           string ->
+           string option * string option * install * bool ->
+           target list ->
+           string list ->
+           (string option * string option * install * bool) * target list
+
+val split_arguments :
+           target list ->
+           (string list *
+            (string list * string list * string list * string list *
+             string list) *
+            (string * string * bool * string) list * string list) *
+           ((string * string) list * (string * string * string) list *
+            (string * string * string) list) *
+           (string list * (string * string) list)
+