X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Ftoplevel%2FmetaOutput.ml;h=2d5bc3ad5c946ac3bbab196e9e0c6d92ac3d42cf;hb=c45c77de154323feaf5bf6aee98c86b95361b9ae;hp=7a15d07c250c5fa844958d63beeaab9a5b104384;hpb=973b0b1fd5f44b96a3c367a9756f28b75b9fa30b;p=helm.git diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml index 7a15d07c2..2d5bc3ad5 100644 --- a/helm/software/lambda-delta/toplevel/metaOutput.ml +++ b/helm/software/lambda-delta/toplevel/metaOutput.ml @@ -1,29 +1,18 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - +(* + ||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 M = Meta type counters = { @@ -84,29 +73,25 @@ let print_counters f c = let terms = c.tsorts + c.tgrefs + c.tgrefs + c.tappls + c.tabsts in let pars = c.pabsts + c.pappls in let items = c.eabsts + c.eabbrs in - Printf.printf " Intermediate representation summary\n"; - Printf.printf " Total entry items: %6u\n" items; - Printf.printf " Declaration items: %6u\n" c.eabsts; - Printf.printf " Definition items: %6u\n" c.eabbrs; - Printf.printf " Total parameter items: %6u\n" pars; - Printf.printf " Application items: %6u\n" c.pappls; - Printf.printf " Abstraction items: %6u\n" c.pabsts; - Printf.printf " Total term items: %6u\n" terms; - Printf.printf " Sort items: %6u\n" c.tsorts; - Printf.printf " Local reference items: %6u\n" c.tlrefs; - Printf.printf " Global reference items: %6u\n" c.tgrefs; - Printf.printf " Application items: %6u\n" c.tappls; - Printf.printf " Abstraction items: %6u\n" c.tabsts; - flush stdout; f () + L.warn (P.sprintf " Intermediate representation summary"); + L.warn (P.sprintf " Total entry items: %6u" items); + L.warn (P.sprintf " Declaration items: %6u" c.eabsts); + L.warn (P.sprintf " Definition items: %6u" c.eabbrs); + L.warn (P.sprintf " Total parameter items: %6u" pars); + L.warn (P.sprintf " Application items: %6u" c.pappls); + L.warn (P.sprintf " Abstraction items: %6u" c.pabsts); + L.warn (P.sprintf " Total term items: %6u" terms); + L.warn (P.sprintf " Sort items: %6u" c.tsorts); + L.warn (P.sprintf " Local reference items: %6u" c.tlrefs); + L.warn (P.sprintf " Global reference items: %6u" c.tgrefs); + L.warn (P.sprintf " Application items: %6u" c.tappls); + L.warn (P.sprintf " Abstraction items: %6u" c.tabsts); + f () let string_of_sort = function | true -> "Type" | false -> "Prop" -let string_of_qid (id, path) = - let path = String.concat "/" path in - Filename.concat path id - let string_of_transparent = function | true -> "=" | false -> "~" @@ -124,17 +109,17 @@ let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args and pp_term frm = function | M.Sort s -> F.fprintf frm "@[*%s@]" (string_of_sort s) - | M.LRef i -> - F.fprintf frm "@[#%u@]" i - | M.GRef (l, qid, ts) -> - F.fprintf frm "@[%u@@$%s%a@]" l (string_of_qid qid) pp_args ts + | M.LRef (l, i) -> + F.fprintf frm "@[%u@@#%u@]" l i + | M.GRef (l, uri, ts) -> + F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts | M.Appl (v, t) -> F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t | M.Abst (id, w, t) -> F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t -let pp_par frm (qid, w) = - F.fprintf frm "%s:%a" (string_of_qid qid) pp_term w +let pp_par frm (id, w) = + F.fprintf frm "%s:%a" id pp_term w let pp_pars = pp_list pp_par "[" "," "]" @@ -143,9 +128,9 @@ let pp_body frm = function | Some (trans, t) -> F.fprintf frm "%s%a" (string_of_transparent trans) pp_term t -let pp_entry frm (l, pars, qid, u, body) = +let pp_entry frm (l, pars, uri, u, body) = F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!" - l (string_of_qid qid) pp_pars pars pp_body body pp_term u + l (U.string_of_uri uri) pp_pars pars pp_body body pp_term u let pp_item f frm = function | Some entry -> pp_entry frm entry; f ()