X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagOutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fbasic_ag%2FbagOutput.ml;h=0000000000000000000000000000000000000000;hb=95872555aaa040a22ad2d93cb1278f79e20da70c;hp=feebca464a05bf92fbd2af4d78381dd639511e7a;hpb=4025c3f5b36025380dcad84bb7a97045d08652f6;p=helm.git diff --git a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml b/helm/software/lambda-delta/src/basic_ag/bagOutput.ml deleted file mode 100644 index feebca464..000000000 --- a/helm/software/lambda-delta/src/basic_ag/bagOutput.ml +++ /dev/null @@ -1,159 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module P = Printf -module F = Format -module U = NUri -module L = Log -module G = Options -module E = Entity -module J = Marks -module H = Hierarchy -module XD = XmlCrg -module Z = Bag -module ZD = BagCrg - -type counters = { - eabsts: int; - eabbrs: int; - tsorts: int; - tlrefs: int; - tgrefs: int; - tcasts: int; - tappls: int; - tabsts: int; - tabbrs: int -} - -let initial_counters = { - eabsts = 0; eabbrs = 0; tsorts = 0; tlrefs = 0; tgrefs = 0; - tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0 -} - -let rec count_term_binder f c = function - | Z.Abst w -> - let c = {c with tabsts = succ c.tabsts} in - count_term f c w - | Z.Abbr v -> - let c = {c with tabbrs = succ c.tabbrs} in - count_term f c v - | Z.Void -> f c - -and count_term f c = function - | Z.Sort _ -> - f {c with tsorts = succ c.tsorts} - | Z.LRef _ -> - f {c with tlrefs = succ c.tlrefs} - | Z.GRef _ -> - f {c with tgrefs = succ c.tgrefs} - | Z.Cast (v, t) -> - let c = {c with tcasts = succ c.tcasts} in - let f c = count_term f c t in - count_term f c v - | Z.Appl (v, t) -> - let c = {c with tappls = succ c.tappls} in - let f c = count_term f c t in - count_term f c v - | Z.Bind (_, _, b, t) -> - let f c = count_term_binder f c b in - count_term f c t - -let count_entity f c = function - | _, _, E.Abst (_, w) -> - let c = {c with eabsts = succ c.eabsts} in - count_term f c w - | _, _, E.Abbr v -> - let c = {c with eabbrs = succ c.eabbrs} in - count_term f c v - | _, _, E.Void -> assert false - -let print_counters f c = - let terms = - c.tsorts + c.tgrefs + c.tgrefs + c.tcasts + c.tappls + c.tabsts + - c.tabbrs - in - let items = c.eabsts + c.eabbrs in - let locations = J.locations () in - L.warn (P.sprintf " Kernel representation summary (basic_ag)"); - L.warn (P.sprintf " Total entry items: %7u" items); - L.warn (P.sprintf " Declaration items: %7u" c.eabsts); - L.warn (P.sprintf " Definition items: %7u" c.eabbrs); - L.warn (P.sprintf " Total term items: %7u" terms); - L.warn (P.sprintf " Sort items: %7u" c.tsorts); - L.warn (P.sprintf " Local reference items: %7u" c.tlrefs); - L.warn (P.sprintf " Global reference items: %7u" c.tgrefs); - L.warn (P.sprintf " Explicit Cast items: %7u" c.tcasts); - L.warn (P.sprintf " Application items: %7u" c.tappls); - L.warn (P.sprintf " Abstraction items: %7u" c.tabsts); - L.warn (P.sprintf " Abbreviation items: %7u" c.tabbrs); - L.warn (P.sprintf " Total binder locations: %7u" locations); - f () - -let name err frm a = - let f n = function - | true -> F.fprintf frm "%s" n - | false -> F.fprintf frm "-%s" n - in - E.name err f a - -let res a l frm = - let err () = F.fprintf frm "@[#%u@]" l in - if !G.indexes then err () else name err frm a - -let rec pp_term c frm = function - | Z.Sort h -> - let err () = F.fprintf frm "@[*%u@]" h in - let f s = F.fprintf frm "@[%s@]" s in - H.string_of_sort err f h - | Z.LRef i -> - let err () = F.fprintf frm "@[#%u@]" i in - let f a _ = name err frm a in - if !G.indexes then err () else Z.get err f c i - | Z.GRef s -> F.fprintf frm "@[$%s@]" (U.string_of_uri s) - | Z.Cast (u, t) -> - F.fprintf frm "@[{%a}.%a@]" (pp_term c) u (pp_term c) t - | Z.Appl (v, t) -> - F.fprintf frm "@[(%a).%a@]" (pp_term c) v (pp_term c) t - | Z.Bind (a, l, Z.Abst w, t) -> - let f cc = - F.fprintf frm "@[[%t:%a].%a@]" (res a l) (pp_term c) w (pp_term cc) t - in - Z.push "output abst" f c a l (Z.Abst w) - | Z.Bind (a, l, Z.Abbr v, t) -> - let f cc = - F.fprintf frm "@[[%t=%a].%a@]" (res a l) (pp_term c) v (pp_term cc) t - in - Z.push "output abbr" f c a l (Z.Abbr v) - | Z.Bind (a, l, Z.Void, t) -> - let f cc = F.fprintf frm "@[[%t].%a@]" (res a l) (pp_term cc) t in - Z.push "output void" f c a l Z.Void - -let pp_lenv frm c = - let pp_entry frm = function - | a, l, Z.Abst w -> - F.fprintf frm "@,@[%t : %a@]" (res a l) (pp_term c) w - | a, l, Z.Abbr v -> - F.fprintf frm "@,@[%t = %a@]" (res a l) (pp_term c) v - | a, l, Z.Void -> - F.fprintf frm "@,%t" (res a l) - in - let iter map frm l = List.iter (map frm) l in - let f es = F.fprintf frm "%a" (iter pp_entry) (List.rev es) in - Z.contents f c - -let specs = { - L.pp_term = pp_term; L.pp_lenv = pp_lenv -} - -(* term xml printing ********************************************************) - -let export_term = - ZD.crg_of_bag XD.export_term