let brg_error s msg =
L.error BrgR.specs (L.Warn s :: L.Loc :: msg); flush_all ()
-let initial_status mk_uri cover g expand si = {
+let initial_status mk_uri cover expand si = {
ac = AO.initial_counters;
mc = MO.initial_counters;
brgc = BrgO.initial_counters;
dst = DA.initial_status (mk_uri si cover);
tst = DT.initial_status (mk_uri si cover);
ast = AP.initial_status;
- kst = Y.initial_status g expand si
+ kst = Y.initial_status expand si
}
(* kernel related ***********************************************************)
| BagEntity e -> {st with bagc = BagO.count_entity C.start st.bagc e}
| _ -> st
-let export_entity si g moch = function
- | CrgEntity e -> X.export_entity DO.export_term si g e
- | BrgEntity e -> X.export_entity BrgO.export_term si g e
+let export_entity si moch = function
+ | CrgEntity e -> X.export_entity DO.export_term si e
+ | BrgEntity e -> X.export_entity BrgO.export_term si e
| MetaEntity e ->
begin match moch with
| None -> ()
type input = Text | Automath
-type input_entity = TxtEntity of Txt.entity
- | AutEntity of Aut.entity
+type input_entity = TxtEntity of Txt.command
+ | AutEntity of Aut.command
let type_of_input name =
if F.check_suffix name ".hln" then Text
- else if F.check_suffix name ".aut" then Automath
+ else if F.check_suffix name ".aut" then
+ let _ = H.set_sorts 0 ["Set"; "Prop"] in
+ assert (H.set_graph "Z2");
+ Automath
else begin
L.warn (P.sprintf "Unknown file type: %s" name); exit 2
end
let process_input f st = function
| AutEntity e ->
let f ast e = f {st with ast = ast} (AutEntity e) in
- AP.process_entity f st.ast e
+ AP.process_command f st.ast e
| xe -> f st xe
let count_input st = function
- | AutEntity e -> {st with ac = AO.count_entity C.start st.ac e}
+ | AutEntity e -> {st with ac = AO.count_command C.start st.ac e}
| xe -> st
(****************************************************************************)
let meta = ref false
let progress = ref false
let preprocess = ref false
-let use_cover = ref true
+let root = ref ""
let si = ref false
let expand = ref false
let cc = ref false
let export = ref false
-let graph = ref (H.graph_of_string C.err C.start "Z2")
let old = ref false
let process_2 st entity =
let st = if !L.level > 2 then count_entity st entity else st in
- if !export then export_entity !si !graph !moch entity;
+ if !export then export_entity !si !moch entity;
if !stage > 2 then type_check st entity else st
let process_1 st entity =
if !progress then pp_progress entity;
let st = if !L.level > 2 then count_entity st entity else st in
- if !export && !stage = 1 then export_entity !si !graph !moch entity;
+ if !export && !stage = 1 then export_entity !si !moch entity;
if !stage > 1 then process_2 st (xlate_entity entity) else st
let process_0 st entity =
let main =
try
let version_string = "Helena 0.8.1 M - February 2010" in
+ let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_hierarchy s =
- let err () = L.warn (P.sprintf "Unknown type hierarchy: %s" s) in
- let f g = graph := g in
- H.graph_of_string err f s
+ if H.set_graph s then () else
+ L.warn (P.sprintf "Unknown type hierarchy: %s" s)
in
let set_kernel = function
| "brg" -> kernel := Brg
| s -> L.warn (P.sprintf "Unknown kernel version: %s" s)
in
let set_summary i = L.level := i in
- let print_version () = L.warn (version_string ^ "\n"); exit 0 in
let set_stage i = stage := i in
let set_meta_file name =
let f och = moch := Some och in
ML.open_out f name
in
- let unquote () =
- AL.unquote := true
- in
+ let set_root s = root := s in
let close = function
| None -> ()
| Some och -> ML.close_out C.start och
| Brg -> Brg.mk_uri
| Bag -> Bag.mk_uri
in
- let cover = if !use_cover then base_name else "" in
- let st = initial_status mk_uri cover !graph !expand !si in
+ let cover = F.concat !root base_name in
+ let st = initial_status mk_uri cover !expand !si in
let st, input = process st name in
if !L.level > 0 then T.utime_stamp "processed";
if !L.level > 2 then begin
let help_o = " use old abstract language instead of crg" in
let help_p = " preprocess Automath source" in
let help_q = " disable quotation of identifiers" in
- let help_r = " disable initial segment of URI hierarchy" in
+ let help_r = "<string> set initial segment of URI hierarchy" in
let help_s = "<number> set translation stage (see above)" in
let help_u = " activate sort inclusion" in
let help_x = " export kernel entities (XML)" in
L.box 0; L.box_err ();
- let _ = H.set_sorts ["Set"; "Prop"] 0 in
at_exit exit;
Arg.parse [
("-S", Arg.Int set_summary, help_S);
("-m", Arg.Set meta, help_m);
("-o", Arg.Set old, help_o);
("-p", Arg.Set preprocess, help_p);
- ("-q", Arg.Unit unquote, help_q);
- ("-r", Arg.Clear use_cover, help_r);
+ ("-q", Arg.Set AL.unquote, help_q);
+ ("-r", Arg.String set_root, help_r);
("-s", Arg.Int set_stage, help_s);
("-u", Arg.Set si, help_u);
("-x", Arg.Set export, help_x)