-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_entity entity = match !kernel, entity with
+ | Brg, CrgEntity e ->
+ let f e = (BrgEntity e) in Y.xlate f DBrg.brg_of_crg e
+ | Brg, MetaEntity e ->
+ let f e = (BrgEntity e) in Y.xlate f MBrg.brg_of_meta e
+ | Bag, MetaEntity e ->
+ let f e = (BagEntity e) in Y.xlate f MBag.bag_of_meta e
+ | _, entity -> entity
+
+let pp_progress e =
+ let f a u =
+ let s = U.string_of_uri u in
+ let err () = L.warn (P.sprintf "%s" s) in
+ let f i = L.warn (P.sprintf "[%u] %s" i s) in
+ Y.mark err f a
+ in
+ match e with
+ | CrgEntity e -> Y.common f e
+ | BrgEntity e -> Y.common f e
+ | BagEntity e -> Y.common f e
+ | MetaEntity e -> Y.common f e
+
+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 si g 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 ~si g entity
+ | BagEntity entity -> BagU.type_check ok ~si g 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 cc = ref false
+let export = ref false
+let graph = ref (H.graph_of_string C.err C.start "Z2")
+let old = ref false