let cc = ref false (* activate conversion constraints *)
-let expand = ref false (* always expand global definitions *)
-
let indexes = ref false (* show de Bruijn indexes *)
let icm = ref 0 (* complexity measure of relocated terms *)
let debug_lexer = ref false (* output lexer debug information *)
-let manager_dir = ref "" (* output directory for manager *)
-
-let manager = ref Quiet (* manager *)
-
-let preamble = ref "" (* preamble file for manager *)
-
let alpha = ref "" (* prefix of numeric identifiers *)
let first = ref 0 (* begin trace here *)
let short = ref false (* short global constants *)
+IFDEF EXPAND THEN
+let expand = ref false (* always expand global definitions *)
+END
+
+IFDEF PREPROCESS THEN
+let preprocess = ref false (* preprocess source *)
+END
+
+IFDEF MANAGER THEN
+let manager_dir = ref "" (* output directory for manager *)
+let manager = ref Quiet (* manager *)
+let preamble = ref "" (* preamble file for manager *)
+END
+
let set_current_trace n =
ct := if !first <= n && n <= !last then !trace else 0
let clear () =
stage := 3; trace := 0; summary := false; export := false; first := 0; last := max_int;
xdir := ""; kernel := V3; si := false; extended := false; infinity := false; cover := "";
- expand := false; indexes := false; icm := 0; unquote := false; short := false;
+ indexes := false; icm := 0; unquote := false; short := false;
debug_parser := false; debug_lexer := false;
- manager_dir := ""; manager := Quiet
+ IFDEF EXPAND THEN expand := false ELSE () END;
+ IFDEF MANAGER THEN manager_dir := ""; manager := Quiet; preamble := "" ELSE () END;
+ IFDEF PREPROCESS THEN preprocess := false ELSE () END
V_______________________________________________________________ *)
module KF = Filename
+module KL = List
module KP = Printf
module KS = String
+module KT = String
module U = NUri
module C = Cps
| BagEntity _ -> st
| CrgEntity _ -> st
+IFDEF MANAGER THEN
+
let manager st output_entity = function
| BrgEntity entity ->
if output_entity st.kst entity then st else
| BagEntity _ -> st
| CrgEntity _ -> st
+END
+
(* extended lexer ***********************************************************)
type 'token lexer = {
(****************************************************************************)
let version = ref true
-let preprocess = ref false
let root = ref ""
let st = ref (initial_status ())
let streaming = ref false (* parsing style (temporary) *)
else st
in
if !G.export then export_entity st entity;
+IFDEF MANAGER THEN
match st.mst with
| None -> st
| Some (export_entity, _) -> manager st export_entity entity
+ELSE
+ st
+END
let process_1 st entity =
if !G.ct >= 3 then pp_progress entity;
| NoEntity -> assert false
in
let st = if !G.summary then count_input st entity else st in
- if !preprocess then process_input f st entity else f st entity
+IFDEF PREPROCESS THEN
+ if !G.preprocess then process_input f st entity else f st entity
+ELSE
+ f st entity
+END
let process_nostreaming st lexbuf input =
let id x = x in
(****************************************************************************)
+IFDEF PREPROCESS THEN
+
+let set_preprocess () =
+ if !G.trace >= 2 then begin G.preprocess := true; G.summary := true end
+
+END
+
+IFDEF MANAGER THEN
+
+let set_manager s = match KS.lowercase s with
+ | "v8" -> G.manager := G.Coq
+ | "ma2" -> G.manager := G.Matita
+ | "lp1" -> G.manager := G.LP1
+ | "lp2" -> G.manager := G.LP2
+ | "tj2" -> G.manager := G.TJ2
+ | "tj3" -> G.manager := G.TJ3
+ | s -> L.warn level (KP.sprintf "Unknown manager: %s" s)
+
+END
+
let process st name =
let process = if !streaming then process_streaming else process_nostreaming in
let input = type_of_input name in
st, input
let main =
- let print_version () = L.warn level (G.version_string ^ "\n"); exit 0 in
+ let print_version () =
+ let features = [
+(IFDEF EXPAND THEN "EXPAND" ELSE "" END);
+(IFDEF MANAGER THEN "MANAGER" ELSE "" END);
+(IFDEF PREPROCESS THEN "PREPROCESS" ELSE "" END);
+ ] in
+ let map s = s <> "" in
+ let features_string = KT.concat " " (KL.filter map features) in
+ L.warn level (KP.sprintf "%s [%s]" G.version_string features_string);
+ exit 0
+ in
let set_hierarchy s =
if H.set_graph s then () else
L.warn level (KP.sprintf "Unknown type hierarchy: %s" s)
if !G.trace > 0 && i = 0 then Y.utime_stamp "at exit";
G.trace := i;
if i <= 1 then G.summary := false;
- if i <= 1 then preprocess := false
+IFDEF PREPROCESS THEN
+ if i <= 1 then G.preprocess := false
+ELSE
+ ()
+END
in
let set_summary () =
if !G.trace >= 2 then G.summary := true
- in
- let set_preprocess () =
- if !G.trace >= 2 then begin preprocess := true; G.summary := true end
- in
- let set_manager s = match KS.lowercase s with
- | "v8" -> G.manager := G.Coq
- | "ma2" -> G.manager := G.Matita
- | "lp1" -> G.manager := G.LP1
- | "lp2" -> G.manager := G.LP2
- | "tj2" -> G.manager := G.TJ2
- | "tj3" -> G.manager := G.TJ3
- | s -> L.warn level (KP.sprintf "Unknown manager: %s" s)
in
let clear_options () =
- preprocess := false;
root := "";
G.clear (); H.clear (); O.clear_reductions ();
streaming := false;
version := true
in
+ let undefined opt () =
+ L.warn level (KP.sprintf "%s was compiled without the support for option %s" G.version_string opt);
+ exit 0
+ in
+ let arg_undefined opt = Arg.Unit (undefined opt) in
let process_file name =
if !G.trace >= 2 then L.warn 1 (KP.sprintf "Processing file: %s" name);
if !G.trace >= 2 then Y.utime_stamp "started";
let cover = KF.concat !root base_name in
if !G.stage <= 1 then G.kernel := G.V4;
G.cover := cover;
+IFDEF MANAGER THEN
begin match !G.manager with
| G.Coq -> st := {!st with mst = Some (BA.open_out base_name)}
| G.Matita -> st := {!st with mst = Some (BG.open_out base_name)}
| G.TJ2 -> st := {!st with mst = Some (BP.open_out_tj2 base_name)}
| G.TJ3 -> st := {!st with mst = Some (BP.open_out_tj3 base_name)}
| G.Quiet -> ()
- end;
+ end
+ELSE
+ ()
+END;
P.clear_marks ();
let sst, input = process (refresh_status !st) name in
st := begin match sst.mst with
if !G.trace >= 2 then Y.utime_stamp "processed";
if !G.summary then begin
AO.print_counters C.start !st.ac;
- if !preprocess then AO.print_process_counters C.start !st.pst;
+IFDEF PREPROCESS THEN
+ if !G.preprocess then AO.print_process_counters C.start !st.pst
+ELSE
+ ()
+END;
if !G.stage >= 1 then print_counters !st G.V4;
if !G.stage >= 2 then print_counters !st !G.kernel;
if !G.stage >= 3 then O.print_reductions ()
at_exit exit;
Arg.parse [
("-L", Arg.Set G.debug_lexer, help_L);
- ("-M", Arg.String ((:=) G.manager_dir), help_M);
+ ("-M", (IFDEF MANAGER THEN Arg.String ((:=) G.manager_dir) ELSE arg_undefined "-M" END), help_M);
("-O", Arg.String ((:=) G.xdir), help_O);
("-P", Arg.Set G.debug_parser, help_P);
("-T", Arg.Int set_trace, help_T);
("-b", Arg.Int ((:=) G.first), help_b);
("-d", Arg.Unit set_summary, help_d);
("-e", Arg.Int ((:=) G.last), help_e);
- ("-g", Arg.Set G.expand, help_g);
+ ("-g", (IFDEF EXPAND THEN Arg.Set G.expand ELSE arg_undefined "-g" END), help_g);
("-h", Arg.String set_hierarchy, help_h);
("-i", Arg.Set G.indexes, help_i);
("-k", Arg.String set_kernel, help_k);
("-l", Arg.Set G.cc, help_l);
- ("-m", Arg.String set_manager, help_m);
+ ("-m", (IFDEF MANAGER THEN Arg.String set_manager ELSE arg_undefined "-m" END), help_m);
("-n", Arg.Set G.short, help_n);
("-o", Arg.Set G.export, help_o);
- ("-p", Arg.String ((:=) G.preamble), help_p);
+ ("-p", (IFDEF MANAGER THEN Arg.String ((:=) G.preamble) ELSE arg_undefined "-p" END), help_p);
("-q", Arg.Set G.unquote, help_q);
("-r", Arg.String ((:=) root), help_r);
("-s", Arg.Int ((:=) G.stage), help_s);
("-u", Arg.Set G.si, help_u);
("-x", Arg.Set G.extended, help_x);
("-y", Arg.Set G.infinity, help_y);
- ("-0", Arg.Unit set_preprocess, help_0);
+ ("-0", (IFDEF PREPROCESS THEN Arg.Unit set_preprocess ELSE arg_undefined "-0" END), help_0);
("-1", Arg.Set streaming, help_1);
] process_file help
projects / helm.git / commitdiff