X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FsequentPp.ml;h=8cce6e1e39a116e8200bed2a35f2dc339e8841be;hb=70f855932359e26ca89deb11c22f9c9d26154827;hp=fb040dfd82dc71c8f8e9afc7f2fa161390b1f87c;hpb=3e0de84a7ef35919fc3c4722c525fcc6cbf68bb5;p=helm.git diff --git a/helm/gTopLevel/sequentPp.ml b/helm/gTopLevel/sequentPp.ml index fb040dfd8..8cce6e1e3 100644 --- a/helm/gTopLevel/sequentPp.ml +++ b/helm/gTopLevel/sequentPp.ml @@ -1,81 +1,115 @@ +(* 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! *) let print_context ctx = - let module P = ProofEngine in let print_name = function Cic.Name n -> n - | Cic.Anonimous -> "_" + | Cic.Anonymous -> "_" in List.fold_right - (fun i env -> - match i with - P.Declaration (n,t) -> - print_endline (print_name n ^ ":" ^ CicPp.pp t env) ; - flush stdout ; - n::env - | P.Definition (n,t) -> - print_endline (print_name n ^ ":=" ^ CicPp.pp t env) ; - flush stdout ; - n::env - ) ctx [] + (fun i (output,context) -> + let (newoutput,context') = + match i with + Some (n,Cic.Decl t) -> + print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context + | Some (n,Cic.Def t) -> + print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context + | None -> + "_ ?= _\n", None::context + in + output^newoutput,context' + ) ctx ("",[]) ;; exception NotImplemented;; - let print_sequent (context,goal) = - let module P = ProofEngine in - print_newline () ; - let pretty_printer_env_of_context = - print_context context - in - print_endline "----------------------" ; - print_endline (CicPp.pp goal pretty_printer_env_of_context) ; flush stdout + let print_sequent (metano,context,goal) = + "\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 print_sequent metasenv (context,goal) = + 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 let ids_to_father_ids = Hashtbl.create 503 in let ids_to_inner_sorts = Hashtbl.create 503 in let ids_to_inner_types = Hashtbl.create 503 in - let seed = ref 0 in - let acic_of_cic_env = - Cic2acic.acic_of_cic_env' seed ids_to_terms ids_to_father_ids + let ids_to_hypotheses = Hashtbl.create 11 in + let hypotheses_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,final_env = + let final_s,_,final_idrefs = (List.fold_right - (fun binding (s,env) -> - let b,n,t,cicbinding = + (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 - ProofEngine.Definition (n,t) -> "Def", n, t,Cic.Def t - | ProofEngine.Declaration (n,t) -> "Decl", n, t, Cic.Decl t - in - let acic = acic_of_cic_env env t in - [< s ; - X.xml_nempty b - ["name",(match n with Cic.Name n -> n | _ -> assert false)] - (Cic2Xml.print_term - (UriManager.uri_of_string "cic:/dummy.con") - ids_to_inner_sorts acic) - >],((n,cicbinding)::env) - ) context ([<>],[]) + (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 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 ~ids_to_inner_sorts acic) + >], (entry::context), (hid::idrefs) + | None -> + (* Invariant: "" is never looked up *) + [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs + ) context ([<>],[],[]) ) in - let acic = acic_of_cic_env final_env goal in - X.xml_nempty "Sequent" [] - [< 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_terms,ids_to_father_ids,ids_to_hypotheses ;; end ;;