+let count_entity st = function
+ | MetaEntity e -> {st with mc = MO.count_entity C.start st.mc e}
+ | BrgEntity e -> {st with brgc = BrgO.count_entity C.start st.brgc e}
+ | 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
+ | MetaEntity e ->
+ begin match moch with
+ | None -> ()
+ | Some och -> ML.write_entity C.start och e
+ end
+ | BagEntity _ -> ()
+
+let type_check st k =
+ let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
+ let ok _ _ = st in
+ match k with
+ | BrgEntity entity -> BrgU.type_check brg_err ok st.kst entity
+ | BagEntity entity -> BagU.type_check ok st.kst entity
+ | CrgEntity _
+ | MetaEntity _ -> st
+
+(****************************************************************************)
+
+let stage = ref 3
+let moch = ref None
+let meta = ref false
+let progress = ref false
+let preprocess = ref false
+let use_cover = ref true
+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 !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 !stage > 1 then process_2 st (xlate_entity entity) else st
+
+let process_0 st entity =
+ let f st entity =
+ if !stage = 0 then st else
+ let frr mst = {st with mst = mst} in
+ let h mst e = process_1 {st with mst = mst} (MetaEntity e) in
+ let err dst = {st with dst = dst} in
+ let g dst e = process_1 {st with dst = dst} (CrgEntity e) in
+ if !old then MA.meta_of_aut frr h st.mst entity else
+ DA.crg_of_aut err g st.dst entity
+ in
+ let st =
+ if !L.level > 2 then {st with ac = AO.count_entity C.start st.ac entity}
+ else st
+ in
+ if !preprocess then process_entity f st entity else f st entity
+
+let rec process st = function
+ | [] -> st
+ | entity :: tl -> process (process_0 st entity) tl