1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
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))
| [] -> ([],([],[],[],[]),[],[]),([],[]),([],[])
|
