module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
+module DrgO = DrgOutput
module MBrg = MetaBrg
module BrgO = BrgOutput
module BrgR = BrgReduction
| _ -> st
let export_entity si g moch = function
+ | DrgEntity e -> X.export_entity DrgO.export_term si g e
| BrgEntity e -> X.old_export_entity BrgO.export_term si g e
| MetaEntity e ->
begin match moch with
| None -> ()
| Some och -> ML.write_entity C.start och e
end
- | _ -> ()
+ | BagEntity _ -> ()
let type_check f st si g k =
let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
let process_1 f st entity =
let st = count_entity st entity in
- export_entity !si !graph !moch entity;
+ if !export && !stage = 1 then export_entity !si !graph !moch entity;
if !stage > 1 then xlate (process_2 f) st entity else f st
let process_0 f st entity =
let rec process f book st = match book with
| [] -> f st
| entity :: tl ->
- process f tl (process_0 C.start st entity)
-(* process_0 (process f tl) st entity *) (* CPS variant of the above *)
+(* we exploit tail recursion rather than CPS *)
+ process f tl (process_0 C.start st entity)
(****************************************************************************)
close_in ich;
if !L.level > 0 then T.utime_stamp "parsed";
O.clear_reductions ();
+ let mk_uri =
+ if !stage < 2 then Drg.mk_uri else
+ match !kernel with
+ | Brg -> Brg.mk_uri
+ | Bag -> Bag.mk_uri
+ in
let cover = if !use_cover then base_name else "" in
let f st =
if !L.level > 0 then T.utime_stamp "processed";
if !L.level > 2 && !stage > 1 then print_counters st;
if !L.level > 2 && !stage > 1 then O.print_reductions ()
in
- process f book (initial_status Drg.mk_uri cover)
+ process f book (initial_status mk_uri cover)
in
let exit () =
close !moch;