diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml (renamed from tools/coq_makefile.ml4) | 129 |
1 files changed, 3 insertions, 126 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml index edbe22e73..ca31a2bd0 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml @@ -8,19 +8,6 @@ (* créer un Makefile pour un développement Coq automatiquement *) -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 *) - let output_channel = ref stdout let makefile_name = ref "Makefile" let make_name = ref "" @@ -107,17 +94,6 @@ let is_prefix dir1 dir2 = let l2 = String.length dir2 in dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/') -let pre_canonize f = - let l = String.length f in - if l > 2 && f.[0] = '.' && f.[1] = '/' then - let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in - String.sub f n (l-n) - else f - -let post_canonize f = - let n = 1 + let i = ref (String.length f - 1) in while !i >= 0 && f.[!i] = '/' do decr i done; !i in - String.sub f 0 n - let physical_dir_of_logical_dir ldir = let le = String.length ldir - 1 in let pdir = if ldir.[le] = '.' then String.sub ldir 0 (le - 1) else String.copy ldir in @@ -407,32 +383,6 @@ let subdirs sds = :: "depend" :: "html" :: sds); print "\n\n" -(* 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 ((pre_canonize 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,pre_canonize 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,(pre_canonize 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,pre_canonize 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,pre_canonize 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,absolute_dir p)::i,r),d) - | RInclude (p,l) :: r -> - let t,(i,r),d = split_arguments r in (t,(i,(post_canonize p,l,absolute_dir 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)) - | [] -> ([],([],[],[],[]),[],[]),([],[]),([],[]) - let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles) other_targets inc = begin match vfiles with |[] -> () @@ -547,80 +497,6 @@ let all_target (vfiles, mlfiles, sps, sds) inc = custom sps; subdirs sds -let parse f = - let rec string = parser - | [< '' ' | '\n' | '\t' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string s) - | [< >] -> "" - and string2 = parser - | [< ''"' >] -> "" - | [< 'c; s >] -> (String.make 1 c)^(string2 s) - and skip_comment = parser - | [< ''\n'; s >] -> s - | [< 'c; s >] -> skip_comment s - | [< >] -> [< >] - and args = parser - | [< '' ' | '\n' | '\t'; s >] -> args s - | [< ''#'; s >] -> args (skip_comment s) - | [< ''"'; str = string2; s >] -> ("" ^ str) :: args s - | [< 'c; str = string; s >] -> ((String.make 1 c) ^ str) :: (args s) - | [< >] -> [] - in - let c = open_in f in - let res = 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") :: _ -> - usage () - | ("-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") :: _ -> - usage () - | "-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"] -> - usage () - | "-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 banner () = print (Printf.sprintf "############################################################################# @@ -682,9 +558,10 @@ let do_makefile args = |[] -> var := false |_::_ -> var := true in let (project_file,makefile,is_install,opt),l = - process_cmd_line (None,None,true,true) [] args in + try Project_file.process_cmd_line (None,None,true,true) [] args + with Project_file.Parsing_error -> usage () in let (v_f,(mli_f,ml4_f,ml_f,mllib_f),sps,sds as targets), inc, defs = - split_arguments l in + Project_file.split_arguments l in let () = match project_file with |None -> () |Some f -> make_name := f in let () = match makefile with |