X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FsequentPp.ml;h=8cce6e1e39a116e8200bed2a35f2dc339e8841be;hb=70f855932359e26ca89deb11c22f9c9d26154827;hp=df504e75a248f4a8fc5433681a9e90e33dd7adf3;hpb=b57c31a1593872c181249135bc05ebd9a72f523b;p=helm.git diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index df504e75a..8cce6e1e3 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2000-2002, 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/. + *) + module TextualPp = struct (* It also returns the pretty-printing context! *) @@ -5,7 +30,7 @@ module TextualPp = let print_name = function Cic.Name n -> n - | Cic.Anonimous -> "_" + | Cic.Anonymous -> "_" in List.fold_right (fun i (output,context) -> @@ -25,18 +50,19 @@ module TextualPp = exception NotImplemented;; let print_sequent (metano,context,goal) = - let module P = ProofEngine in - "\n" ^ - let (output,pretty_printer_context_of_context) = print_context context in - output ^ - "---------------------- ?" ^ string_of_int metano ^ "\n" ^ - CicPp.pp goal pretty_printer_context_of_context + "\n" ^ + let (output,pretty_printer_context_of_context) = print_context context in + output ^ + "---------------------- ?" ^ string_of_int metano ^ "\n" ^ + CicPp.pp goal pretty_printer_context_of_context ;; end ;; module XmlPp = struct + let dtdname = "http://localhost:8081/getdtd?uri=cic.dtd";; + let print_sequent metasenv (metano,context,goal) = let module X = Xml in let ids_to_terms = Hashtbl.create 503 in @@ -45,41 +71,43 @@ module XmlPp = let ids_to_inner_types = Hashtbl.create 503 in let ids_to_hypotheses = Hashtbl.create 11 in let hypotheses_seed = ref 0 in - let seed = ref 0 in + let sequent_id = "i0" in + let seed = ref 1 in (* 'i0' is used for the whole sequent *) let acic_of_cic_context = Cic2acic.acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts ids_to_inner_types metasenv in - let final_s,_ = + let final_s,_,final_idrefs = (List.fold_right - (fun binding (s,context) -> + (fun binding (s,context,idrefs) -> let hid = "h" ^ string_of_int !hypotheses_seed in Hashtbl.add ids_to_hypotheses hid binding ; incr hypotheses_seed ; match binding with (Some (n,(Cic.Def t as b)) as entry) | (Some (n,(Cic.Decl t as b)) as entry) -> - let acic = acic_of_cic_context context t in + let acic = acic_of_cic_context context idrefs t None in [< s ; X.xml_nempty (match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def") ["name",(match n with Cic.Name n -> n | _ -> assert false); "id",hid] - (Cic2Xml.print_term - (UriManager.uri_of_string "cic:/dummy.con") - ids_to_inner_sorts acic) - >], (entry::context) + (Cic2Xml.print_term ~ids_to_inner_sorts acic) + >], (entry::context), (hid::idrefs) | None -> - [< s ; X.xml_empty "Hidden" [] >], (None::context) - ) context ([<>],[]) + (* Invariant: "" is never looked up *) + [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs + ) context ([<>],[],[]) ) in - let acic = acic_of_cic_context context goal in - X.xml_nempty "Sequent" ["no",string_of_int metano] - [< final_s ; - Xml.xml_nempty "Goal" [] - (Cic2Xml.print_term (UriManager.uri_of_string "cic:/dummy.con") - ids_to_inner_sorts acic) + let acic = acic_of_cic_context context final_idrefs goal None in + [< X.xml_cdata "\n" ; + X.xml_cdata ("\n"); + X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id] + [< final_s ; + Xml.xml_nempty "Goal" [] + (Cic2Xml.print_term ~ids_to_inner_sorts acic) + >] >], ids_to_terms,ids_to_father_ids,ids_to_hypotheses ;;