From cfaa4ba59014ccb6046a2a672e97a5e88d7d2946 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 22 Jan 2004 15:23:01 +0000 Subject: [PATCH] Added all transformations for sequents. --- helm/ocaml/cic_transformations/.depend | 9 ++ helm/ocaml/cic_transformations/Makefile | 3 +- .../cic_transformations/applyStylesheets.ml | 5 + .../applyTransformation.ml | 77 +++++++++++++ .../applyTransformation.mli | 51 +++++++++ .../ocaml/cic_transformations/content2pres.ml | 41 +++++++ .../content_expressions.ml | 2 +- .../ocaml/cic_transformations/sequent2pres.ml | 107 ++++++++++++++++++ .../cic_transformations/sequent2pres.mli | 39 +++++++ 9 files changed, 332 insertions(+), 2 deletions(-) create mode 100644 helm/ocaml/cic_transformations/applyTransformation.ml create mode 100644 helm/ocaml/cic_transformations/applyTransformation.mli create mode 100644 helm/ocaml/cic_transformations/sequent2pres.ml create mode 100644 helm/ocaml/cic_transformations/sequent2pres.mli diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index c7ccf7049..3f0bc48d7 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -1,5 +1,6 @@ cexpr2pres.cmi: content_expressions.cmi mpresentation.cmi content2pres.cmi: mpresentation.cmi +sequent2pres.cmi: mpresentation.cmi cexpr2pres_hashtbl.cmi: content_expressions.cmi mpresentation.cmi cic2Xml.cmo: cic2Xml.cmi cic2Xml.cmx: cic2Xml.cmi @@ -13,6 +14,10 @@ content2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ content2pres.cmi content2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ content2pres.cmi +sequent2pres.cmo: cexpr2pres.cmi content_expressions.cmi mpresentation.cmi \ + sequent2pres.cmi +sequent2pres.cmx: cexpr2pres.cmx content_expressions.cmx mpresentation.cmx \ + sequent2pres.cmi cexpr2pres_hashtbl.cmo: cexpr2pres.cmi content_expressions.cmi \ mpresentation.cmi cexpr2pres_hashtbl.cmi cexpr2pres_hashtbl.cmx: cexpr2pres.cmx content_expressions.cmx \ @@ -27,3 +32,7 @@ applyStylesheets.cmo: cic2Xml.cmi misc.cmi sequentPp.cmi xml2Gdome.cmi \ applyStylesheets.cmi applyStylesheets.cmx: cic2Xml.cmx misc.cmx sequentPp.cmx xml2Gdome.cmx \ applyStylesheets.cmi +applyTransformation.cmo: content2pres.cmi misc.cmi mpresentation.cmi \ + sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi +applyTransformation.cmx: content2pres.cmx misc.cmx mpresentation.cmx \ + sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index 3a3630640..384a6f00e 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -4,8 +4,9 @@ PREDICATES = INTERFACE_FILES = cic2Xml.mli content_expressions.mli \ mpresentation.mli cexpr2pres.mli content2pres.mli \ + sequent2pres.mli \ cexpr2pres_hashtbl.mli misc.mli xml2Gdome.mli sequentPp.mli \ - applyStylesheets.mli + applyStylesheets.mli applyTransformation.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) EXTRA_OBJECTS_TO_INSTALL = EXTRA_OBJECTS_TO_CLEAN = diff --git a/helm/ocaml/cic_transformations/applyStylesheets.ml b/helm/ocaml/cic_transformations/applyStylesheets.ml index 82060587a..860a73297 100644 --- a/helm/ocaml/cic_transformations/applyStylesheets.ml +++ b/helm/ocaml/cic_transformations/applyStylesheets.ml @@ -182,3 +182,8 @@ let let output = apply_proof_stylesheets input ~explode_all in output ;; + + + + + diff --git a/helm/ocaml/cic_transformations/applyTransformation.ml b/helm/ocaml/cic_transformations/applyTransformation.ml new file mode 100644 index 000000000..c70f46c68 --- /dev/null +++ b/helm/ocaml/cic_transformations/applyTransformation.ml @@ -0,0 +1,77 @@ +(* 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/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 21/11/2003 *) +(* *) +(* *) +(***************************************************************************) + +let reload_stylesheets = ignore +;; + +let mml_of_cic_sequent metasenv sequent = + let asequent,ids_to_terms, + ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses = + Cic2acic.asequent_of_sequent metasenv sequent in + let content_sequent = Cic2content.map_sequent asequent in + let pres_sequent = + (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent) in + let xmlpres = Mpresentation.print_mpres pres_sequent in + Xml2Gdome.document_of_xml Misc.domImpl xmlpres, + (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) +;; + +let mml_of_cic_object ~explode_all uri acic + ids_to_inner_sorts ids_to_inner_types = + match acic with + Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> + let time1 = Sys.time () in + let content = + Cic2content.annobj2content + ~ids_to_inner_sorts ~ids_to_inner_types acic in + (* ContentPp.print_obj content; *) + let pres = Content2pres.content2pres ~ids_to_inner_sorts content in + let time2 = Sys.time () in + (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) + let xmlpres = Mpresentation.print_mpres pres in + let time25 = Sys.time () in + (* alternative: printing to file + prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); + Xml.pp xmlpres (Some "tmp"); + let time3 = Sys.time () in + prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); + end alternative *) + (try + Xml2Gdome.document_of_xml Misc.domImpl xmlpres + with (GdomeInit.DOMException (_,s)) as e -> + prerr_endline s; raise e) + | _ -> assert false +;; + diff --git a/helm/ocaml/cic_transformations/applyTransformation.mli b/helm/ocaml/cic_transformations/applyTransformation.mli new file mode 100644 index 000000000..4a1f08e31 --- /dev/null +++ b/helm/ocaml/cic_transformations/applyTransformation.mli @@ -0,0 +1,51 @@ +(* 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/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 21/11/2003 *) +(* *) +(* *) +(***************************************************************************) + +val reload_stylesheets: unit -> unit + +val mml_of_cic_sequent : + Cic.metasenv -> + int * Cic.context * Cic.term -> + Gdome.document * + ((Cic.id, Cic.term) Hashtbl.t * + (Cic.id, Cic.id option) Hashtbl.t * + (string, Cic.hypothesis) Hashtbl.t) + +val mml_of_cic_object : + explode_all:bool -> + UriManager.uri -> + Cic.annobj -> + (string, string) Hashtbl.t -> + (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml index af3999a39..c0cdc5c0f 100644 --- a/helm/ocaml/cic_transformations/content2pres.ml +++ b/helm/ocaml/cic_transformations/content2pres.ml @@ -436,6 +436,8 @@ and proof2pres term2pres p = (make_concl "we proved 1" conclusion))])]); | _ -> assert false) *) + else if (conclude.Con.conclude_method = "Case") then + case conclude else if (conclude.Con.conclude_method = "ByInduction") then byinduction conclude else if (conclude.Con.conclude_method = "Exists") then @@ -507,6 +509,44 @@ and proof2pres term2pres p = | Con.ArgMethod s -> P.Mtext ([],"method") + and case conclude = + let module P = Mpresentation in + let module Con = Content in + let proof_conclusion = + (match conclude.Con.conclude_conclusion with + None -> P.Mtext([],"No conclusion???") + | Some t -> term2pres t) in + let arg,args_for_cases = + (match conclude.Con.conclude_args with + Con.Aux(_)::Con.Aux(_)::Con.Term(_)::arg::tl -> + arg,tl + | _ -> assert false) in + let case_on = + let case_arg = + (match arg with + Con.Aux n -> + P.Mtext ([],"an aux???") + | Con.Premise prem -> + (match prem.Con.premise_binder with + None -> P.Mtext ([],"the previous result") + | Some n -> P.Mi([],n)) + | Con.Lemma lemma -> P.Mi([],lemma.Con.lemma_name) + | Con.Term t -> + term2pres t + | Con.ArgProof p -> + P.Mtext ([],"a proof???") + | Con.ArgMethod s -> + P.Mtext ([],"a method???")) in + (make_concl "we proceede by cases on" case_arg) in + let to_prove = + (make_concl "to prove" proof_conclusion) in + P.Mtable + ([None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"], + P.Mtr ([],[P.Mtd ([],case_on)]):: + P.Mtr ([],[P.Mtd ([],to_prove)]):: + (make_cases args_for_cases)) + and byinduction conclude = let module P = Mpresentation in let module Con = Content in @@ -894,3 +934,4 @@ let content2pres ~ids_to_inner_sorts = (Cexpr2pres.cexpr2pres_charcount (Content_expressions.acic2cexpr ids_to_inner_sorts p))) ;; + diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index b913bf0de..8b8d0361a 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -36,7 +36,7 @@ (* the type cexpr is inspired by OpenMath. A few primitive constructors have been added, in order to take into account some special features of functional expressions. Most notably: case, let in, let rec, and - explicit substitutons *) + explicit substitutions *) type cexpr = Symbol of string option * string * subst option * string option diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml new file mode 100644 index 000000000..4c47bc51a --- /dev/null +++ b/helm/ocaml/cic_transformations/sequent2pres.ml @@ -0,0 +1,107 @@ +(* 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/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 19/11/2003 *) +(* *) +(***************************************************************************) + +let p_mtr a b = Mpresentation.Mtr(a,b) +let p_mtd a b = Mpresentation.Mtd(a,b) +let p_mtable a b = Mpresentation.Mtable(a,b) +let p_mtext a b = Mpresentation.Mtext(a,b) +let p_mi a b = Mpresentation.Mi(a,b) +let p_mo a b = Mpresentation.Mo(a,b) +let p_mrow a b = Mpresentation.Mrow(a,b) +let p_mphantom a b = Mpresentation.Mphantom(a,b) + +let sequent2pres term2pres (_,_,context,ty) = + let module K = Content in + let module P = Mpresentation in + let make_tr r = + p_mtr [] [p_mtd [] r] in + let context2pres context = + let rec aux accum = + function + [] -> accum + | None::tl -> aux accum tl + | (Some (`Declaration d))::tl -> + let + { K.dec_name = dec_name ; + K.dec_id = dec_id ; + K.dec_type = ty } = d in + let r = + p_mrow [Some "helm", "xref", dec_id] + [ p_mi [] + (match dec_name with + None -> "_" + | Some n -> n) ; + p_mo [] ":" ; + term2pres ty] in + aux ((make_tr r)::accum) tl + | (Some (`Definition d))::tl -> + let + { K.def_name = def_name ; + K.def_id = def_id ; + K.def_term = bo } = d in + let r = + p_mrow [Some "helm", "xref", def_id] + [ p_mi [] + (match def_name with + None -> "_" + | Some n -> n) ; + p_mo [] ":=" ; + term2pres bo] in + aux ((make_tr r)::accum) tl + | _::_ -> assert false in + aux [] context in + let pres_context = + make_tr + (p_mtable + [None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"] + (context2pres context)) in + let pres_goal = + make_tr (term2pres ty) in + (p_mtable + [None,"align","baseline 1"; None,"equalrows","false"; + None,"columnalign","left"; None,"rowlines","solid"] + [pres_context;pres_goal]) +;; + +let sequent2pres ~ids_to_inner_sorts = + sequent2pres + (function p -> + (Cexpr2pres.cexpr2pres_charcount + (Content_expressions.acic2cexpr ids_to_inner_sorts p))) +;; + + + + diff --git a/helm/ocaml/cic_transformations/sequent2pres.mli b/helm/ocaml/cic_transformations/sequent2pres.mli new file mode 100644 index 000000000..7bb124225 --- /dev/null +++ b/helm/ocaml/cic_transformations/sequent2pres.mli @@ -0,0 +1,39 @@ +(* 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/. + *) + +(***************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 19/11/2003 *) +(* *) +(***************************************************************************) + +val sequent2pres : +ids_to_inner_sorts:(Cic.id, string) Hashtbl.t -> + Cic.annterm Content.conjecture -> Mpresentation.mpres + + -- 2.39.2