-let kernel_of_meta f st item = match !kernel with
- | Brg ->
- let f item = f st (BrgItem item) in
- MBrg.brg_of_meta f item
- | Bag ->
- let f item = f st (BagItem item) in
- MBag.bag_of_meta f item
-
-let count_item st = function
- | BrgItem item -> {st with brgc = count BrgO.count_item st.brgc item}
- | BagItem item -> {st with bagc = count BagO.count_item st.bagc item}
-
-let type_check f st g = function
- | BrgItem item ->
- let f _ = function
- | None -> f st None
- | Some (i, u, _) -> f st (Some (i, u))
- in
- BrgU.type_check f g item
- | BagItem item ->
- let f _ = function
- | None -> f st None
- | Some (i, u, _) -> f st (Some (i, u))
- in
- BagU.type_check f g item
+let xlate f st entity = match !kernel, entity with
+ | Brg, MetaEntity e ->
+ let f e = f st (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+ | Bag, MetaEntity e ->
+ let f e = f st (BagEntity e) in Y.xlate f MBag.bag_of_meta e
+ | _, entity -> f st entity
+
+let count_entity st = function
+ | MetaEntity e -> {st with mc = count MO.count_entity st.mc e}
+ | BrgEntity e -> {st with brgc = count BrgO.count_entity st.brgc e}
+ | BagEntity e -> {st with bagc = count BagO.count_entity st.bagc e}
+ | _ -> st
+
+let export_entity si g moch = function
+ | 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
+ | _ -> ()
+
+let type_check f st si g k =
+ let brg_err msg = brg_error "Type Error" msg; failwith "Interrupted" in
+ let ok _ (a, u, _) = f st a u in
+ match k with
+ | BrgEntity entity -> BrgU.type_check brg_err ok ~si g entity
+ | BagEntity entity -> BagU.type_check ok ~si g entity
+ | DrgEntity (a, u, _)
+ | MetaEntity (a, u, _) -> f st a u
+
+(****************************************************************************)
+
+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 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_3 f st a u =
+ if !progress then
+ let s = U.string_of_uri u in
+ let err () = L.warn (P.sprintf "%s" s); f st in
+ let f i = L.warn (P.sprintf "[%u] %s" i s); f st in
+ Y.mark err f a
+ else
+ f st