three tags introduced so far: EXPAND, PREPROCESS, MANAGER
12 files changed:
INCLUDES = $(DIRECTORIES:%=-I %)
INCLUDES = $(DIRECTORIES:%=-I %)
-OCAMLDEP = $(OCAMLFIND) ocamldep -native $(INCLUDES)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES)
+CAMLP = -pp "camlp5o pa_macro.cmo $(CAMLPOPTIONS)"
+
+CAMLPOPTIONS = $(F:%=-D%)
+
+OCAMLDEP = $(OCAMLFIND) ocamldep $(CAMLP) -native $(INCLUDES)
+OCAMLOPT = $(OCAMLFIND) opt $(CAMLP) $(OCAMLOPTIONS) -linkpkg -package "$(REQUIRES)" $(INCLUDES)
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
TAR = tar -czf etc/$(MAIN:%=%.tgz)
OCAMLLEX = ocamllex.opt
OCAMLYACC = ocamlyacc -v
TAR = tar -czf etc/$(MAIN:%=%.tgz)
+Helena 0.8.3 M
+
+<compile-time feature> ::=
+
+EXPAND enable option -g (if unset, -g is disabled)
+MANAGER enable options -M -m -p (if unset, -m is disabled)
+PREPROCESS enable option (if unset, -0 is disabled)
* type "make" or "make opt" to compile the native executable
* type "make" or "make opt" to compile the native executable
+ with the desired features listed in the variable F
* type "make clean" to remove the products of compilation
* type "make clean" to remove the products of compilation
| D.ESort -> t
| D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t)
| _ ->
| D.ESort -> t
| D.EBind (D.ESort, a, b) -> D.TBind (E.compose a at, b, t)
| _ ->
- let e = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start at e else e in
+IFDEF MANAGER OR OBJS THEN
+ D.TProj (at, D.set_attrs C.start at e, t)
+ELSE
(* this is not tail recursive in the GRef branch *)
let rec xlate_term f st lst y lenv = function
(* this is not tail recursive in the GRef branch *)
let rec xlate_term f st lst y lenv = function
let a = E.compose av a in
f a (D.TAppl (a, x, v, gref))
| args ->
let a = E.compose av a in
f a (D.TAppl (a, x, v, gref))
| args ->
- let args = if !G.export || !G.manager <> G.Quiet then D.set_attrs C.start a args else args in
+IFDEF MANAGER OR OBJS THEN
+ f a (D.TProj (a, D.set_attrs C.start a args, gref))
+ELSE
f a (D.TProj (a, args, gref))
f a (D.TProj (a, args, gref))
in
let f args = C.list_fold_right f map2 args D.ESort in
D.sub_list_strict (D.fold_names f map1 args) cnt args
in
let f args = C.list_fold_right f map2 args D.ESort in
D.sub_list_strict (D.fold_names f map1 args) cnt args
(* decps *)
let set_entity entity =
(* decps *)
let set_entity entity =
let ra, na, uri, b = entity in
let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in
UH.add env uri entity0; entity
let ra, na, uri, b = entity in
let entity0 = if !G.expand then ra, {na with E.n_apix = 0}, uri, b else entity in
UH.add env uri entity0; entity
+ELSE
+ let _, _, uri, _ = entity in
+ UH.add env uri entity; entity
+END
let get_entity uri =
try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void
let get_entity uri =
try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void
module R = Alpha
module B = Brg
module R = Alpha
module B = Brg
(* Internal functions *******************************************************)
let ok = ref true
(* Internal functions *******************************************************)
let ok = ref true
out_preamble och;
out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
output_entity och, close_out och
out_preamble och;
out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
output_entity och, close_out och
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val open_out: string -> Brg.manager
val open_out: string -> Brg.manager
module R = Alpha
module B = Brg
module R = Alpha
module B = Brg
(* Internal functions *******************************************************)
let ok = ref true
(* Internal functions *******************************************************)
let ok = ref true
out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
out_include och "basics/pts";
output_entity och, close_out och
out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
out_include och "basics/pts";
output_entity och, close_out och
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val open_out: string -> Brg.manager
val open_out: string -> Brg.manager
module R = Alpha
module B = Brg
module R = Alpha
module B = Brg
(* Internal functions *******************************************************)
let ok = ref true
(* Internal functions *******************************************************)
let ok = ref true
out_clause och "module grundlagen.";
out_clause och "accumulate helena.";
output_entity_tj3 och, close_out_tj3 och
out_clause och "module grundlagen.";
out_clause och "accumulate helena.";
output_entity_tj3 och, close_out_tj3 och
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
val open_out_lp1: string -> Brg.manager
val open_out_lp2: string -> Brg.manager
val open_out_lp1: string -> Brg.manager
val open_out_lp2: string -> Brg.manager
val open_out_tj2: string -> Brg.manager
val open_out_tj3: string -> Brg.manager
val open_out_tj2: string -> Brg.manager
val open_out_tj3: string -> Brg.manager
let cc = ref false (* activate conversion constraints *)
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 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 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 alpha = ref "" (* prefix of numeric identifiers *)
let first = ref 0 (* begin trace here *)
let short = ref false (* short global constants *)
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 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 := "";
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;
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
V_______________________________________________________________ *)
module KF = Filename
module KP = Printf
module KS = String
module KP = Printf
module KS = String
module U = NUri
module C = Cps
module U = NUri
module C = Cps
| BagEntity _ -> st
| CrgEntity _ -> st
| BagEntity _ -> st
| CrgEntity _ -> st
let manager st output_entity = function
| BrgEntity entity ->
if output_entity st.kst entity then st else
let manager st output_entity = function
| BrgEntity entity ->
if output_entity st.kst entity then st else
| BagEntity _ -> st
| CrgEntity _ -> st
| BagEntity _ -> st
| CrgEntity _ -> st
(* extended lexer ***********************************************************)
type 'token lexer = {
(* extended lexer ***********************************************************)
type 'token lexer = {
(****************************************************************************)
let version = ref true
(****************************************************************************)
let version = ref true
-let preprocess = ref false
let root = ref ""
let st = ref (initial_status ())
let streaming = ref false (* parsing style (temporary) *)
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;
else st
in
if !G.export then export_entity st entity;
match st.mst with
| None -> st
| Some (export_entity, _) -> manager st export_entity entity
match st.mst with
| None -> st
| Some (export_entity, _) -> manager st export_entity entity
let process_1 st entity =
if !G.ct >= 3 then pp_progress entity;
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
| 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
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
let process st name =
let process = if !streaming then process_streaming else process_nostreaming in
let input = type_of_input name in
- 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)
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 !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_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 () =
in
let clear_options () =
root := "";
G.clear (); H.clear (); O.clear_reductions ();
streaming := false;
version := true
in
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 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;
let cover = KF.concat !root base_name in
if !G.stage <= 1 then G.kernel := G.V4;
G.cover := cover;
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)}
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 -> ()
| 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 -> ()
P.clear_marks ();
let sst, input = process (refresh_status !st) name in
st := begin match sst.mst with
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 !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 ()
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);
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);
("-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);
("-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);
("-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);
("-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);
("-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);
("-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
("-1", Arg.Set streaming, help_1);
] process_file help