From 34259adcd8a36e85f3224c7074c74aef878f1856 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 12 Dec 2006 09:54:14 +0000 Subject: [PATCH] we started the infrastructure for the procedural rendering of proofs --- .../METAS/meta.helm-content_pres.src | 2 +- helm/software/components/Makefile | 3 +- .../components/binaries/transcript/grafite.ml | 2 +- helm/software/components/content_pres/.depend | 8 +++-- .../software/components/content_pres/Makefile | 1 + .../content_pres/content2Procedural.ml | 26 +++++++++++++++ .../content_pres/content2Procedural.mli | 32 +++++++++++++++++++ .../software/components/content_pres/objPp.ml | 15 +++++++-- .../components/content_pres/objPp.mli | 4 +-- .../software/components/grafite/grafiteAst.ml | 5 ++- .../components/grafite/grafiteAstPp.ml | 11 +++++-- .../grafite_parser/grafiteParser.ml | 12 +++++-- helm/software/matita/matita.ml | 2 +- helm/software/matita/matitaScript.ml | 4 +-- 14 files changed, 108 insertions(+), 19 deletions(-) create mode 100644 helm/software/components/content_pres/content2Procedural.ml create mode 100644 helm/software/components/content_pres/content2Procedural.mli diff --git a/helm/software/components/METAS/meta.helm-content_pres.src b/helm/software/components/METAS/meta.helm-content_pres.src index 1706818e2..1e76f9fe8 100644 --- a/helm/software/components/METAS/meta.helm-content_pres.src +++ b/helm/software/components/METAS/meta.helm-content_pres.src @@ -1,4 +1,4 @@ -requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex" +requires="helm-acic_content helm-syntax_extensions camlp4.gramlib ulex helm-grafite" version="0.0.1" archive(byte)="content_pres.cma" archive(native)="content_pres.cmxa" diff --git a/helm/software/components/Makefile b/helm/software/components/Makefile index cfe1fd517..a700970af 100644 --- a/helm/software/components/Makefile +++ b/helm/software/components/Makefile @@ -23,8 +23,8 @@ MODULES = \ metadata \ library \ acic_content \ - content_pres \ grafite \ + content_pres \ cic_unification \ whelp \ tactics \ @@ -143,3 +143,4 @@ tags: TAGS TAGS: $(H)otags -vi -r . +metas: $(filter-out METAS/META.helm-binaries, $(METAS)) diff --git a/helm/software/components/binaries/transcript/grafite.ml b/helm/software/components/binaries/transcript/grafite.ml index cc1b465d7..dff9fcccd 100644 --- a/helm/software/components/binaries/transcript/grafite.ml +++ b/helm/software/components/binaries/transcript/grafite.ml @@ -82,7 +82,7 @@ let coercion value = command_of_obj (G.Coercion (floc, UM.uri_of_string value, true, 0)) let inline (uri, prefix) = - command_of_macro (G.Inline (floc, uri, prefix)) + command_of_macro (G.Inline (floc, G.Declarative, uri, prefix)) let commit och items = let trd (_, _, x) = x in diff --git a/helm/software/components/content_pres/.depend b/helm/software/components/content_pres/.depend index 2de502ee5..cddd3d80f 100644 --- a/helm/software/components/content_pres/.depend +++ b/helm/software/components/content_pres/.depend @@ -30,8 +30,12 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -objPp.cmo: content2pres.cmi cicNotationPres.cmi boxPp.cmi objPp.cmi -objPp.cmx: content2pres.cmx cicNotationPres.cmx boxPp.cmx objPp.cmi +content2Procedural.cmo: content2Procedural.cmi +content2Procedural.cmx: content2Procedural.cmi +objPp.cmo: content2pres.cmi content2Procedural.cmi cicNotationPres.cmi \ + boxPp.cmi objPp.cmi +objPp.cmx: content2pres.cmx content2Procedural.cmx cicNotationPres.cmx \ + boxPp.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/helm/software/components/content_pres/Makefile b/helm/software/components/content_pres/Makefile index 5613ff9ff..497afc8d2 100644 --- a/helm/software/components/content_pres/Makefile +++ b/helm/software/components/content_pres/Makefile @@ -12,6 +12,7 @@ INTERFACE_FILES = \ cicNotationPres.mli \ boxPp.mli \ content2pres.mli \ + content2Procedural.mli \ objPp.mli \ sequent2pres.mli \ $(NULL) diff --git a/helm/software/components/content_pres/content2Procedural.ml b/helm/software/components/content_pres/content2Procedural.ml new file mode 100644 index 000000000..e09ca0b03 --- /dev/null +++ b/helm/software/components/content_pres/content2Procedural.ml @@ -0,0 +1,26 @@ +(* Copyright (C) 2003-2005, 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/. + *) + +let content2procedural ~ids_to_inner_sorts prefix annterm = [] diff --git a/helm/software/components/content_pres/content2Procedural.mli b/helm/software/components/content_pres/content2Procedural.mli new file mode 100644 index 000000000..14cf247dd --- /dev/null +++ b/helm/software/components/content_pres/content2Procedural.mli @@ -0,0 +1,32 @@ +(* 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/. + *) + +val content2procedural: + ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t -> string -> + Cic.annterm Content.cobj -> + (CicNotationPt.term, CicNotationPt.term, + CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string) + GrafiteAst.statement list + diff --git a/helm/software/components/content_pres/objPp.ml b/helm/software/components/content_pres/objPp.ml index 1eb47dbab..49936861f 100644 --- a/helm/software/components/content_pres/objPp.ml +++ b/helm/software/components/content_pres/objPp.ml @@ -23,8 +23,17 @@ * http://helm.cs.unibo.it/ *) -let obj_to_string n obj = +let obj_to_string n style prefix obj = let aobj,_,_,ids_to_inner_sorts,ids_to_inner_types,_,_ = Cic2acic.acic_object_of_cic_object obj in let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in - let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in - BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) + match style with + | GrafiteAst.Declarative -> + let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in + BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj) + | GrafiteAst.Procedural -> + let term_pp = CicNotationPp.pp_term in + let lazy_term_pp = CicNotationPp.pp_term in + let obj_pp = CicNotationPp.pp_obj in + let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in + let script = Content2Procedural.content2procedural ~ids_to_inner_sorts prefix cobj in + String.concat "" (List.map aux script) diff --git a/helm/software/components/content_pres/objPp.mli b/helm/software/components/content_pres/objPp.mli index e007c6e7c..9367661ec 100644 --- a/helm/software/components/content_pres/objPp.mli +++ b/helm/software/components/content_pres/objPp.mli @@ -23,5 +23,5 @@ * http://helm.cs.unibo.it/ *) -val obj_to_string: int -> Cic.obj -> string - +(* columns, rendering style, name prefix, object *) +val obj_to_string: int -> GrafiteAst.style -> string -> Cic.obj -> string diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 9c5d56024..897912915 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -106,6 +106,9 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] +type style = Declarative + | Procedural + type 'term macro = (* Whelp's stuff *) | WHint of loc * 'term @@ -116,7 +119,7 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc - | Inline of loc * string * string (* URI or base-uri, name prefix *) + | Inline of loc * style * string * string (* URI or base-uri, name prefix *) (** To be increased each time the command type below changes, used for "safe" * marshalling *) diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index f51cd0bca..efc007886 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -193,6 +193,13 @@ let pp_arg ~term_pp arg = let pp_macro ~term_pp = let term_pp = pp_arg ~term_pp in + let style_pp = function + | Declarative -> "" + | Procedural -> "procedural " + in + let prefix_pp prefix = + if prefix = "" then "" else sprintf " \"%s\"" prefix + in function (* Whelp *) | WInstance (_, term) -> "whelp instance " ^ term_pp term @@ -203,8 +210,8 @@ let pp_macro ~term_pp = (* real macros *) | Check (_, term) -> sprintf "check %s" (term_pp term) | Hint _ -> "hint" - | Inline (_, suri, "") -> sprintf "inline \"%s\"" suri - | Inline (_, suri, prefix) -> sprintf "inline \"%s\" \"%s\"" suri prefix + | Inline (_, style, suri, prefix) -> + sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) let pp_associativity = function | Gramext.LeftA -> "left associative" diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index fb0128edb..a78ca8113 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -411,9 +411,15 @@ EXTEND macro: [ [ [ IDENT "check" ]; t = term -> GrafiteAst.Check (loc, t) - | [ IDENT "inline"]; suri = QSTRING; prefix = OPT QSTRING -> - let prefix = match prefix with None -> "" | Some prefix -> prefix in - GrafiteAst.Inline (loc,suri,prefix) + | [ IDENT "inline"]; + style = OPT [ IDENT "procedural" ]; + suri = QSTRING; prefix = OPT QSTRING -> + let style = match style with + | None -> GrafiteAst.Declarative + | Some _ -> GrafiteAst.Procedural + in + let prefix = match prefix with None -> "" | Some prefix -> prefix in + GrafiteAst.Inline (loc,style,suri,prefix) | [ IDENT "hint" ] -> GrafiteAst.Hint loc | [ IDENT "whelp"; "match" ] ; t = term -> GrafiteAst.WMatch (loc,t) diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml index 783b8c023..5a638b48d 100644 --- a/helm/software/matita/matita.ml +++ b/helm/software/matita/matita.ml @@ -173,7 +173,7 @@ let _ = addDebugItem "Print current proof (natural language) to stderr" (fun _ -> prerr_endline - (ObjPp.obj_to_string 120 + (ObjPp.obj_to_string 120 GrafiteAst.Declarative "" (match (MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status with diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 12f26036b..1a128fb1c 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -288,7 +288,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let t_and_ty = Cic.Cast (term,ty) in guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv)); [], "", parsed_text_length - | TA.Inline (_,suri,prefix) -> + | TA.Inline (_,style,suri,prefix) -> let dbd = LibraryDb.instance () in let uris = let sql_pat = @@ -328,7 +328,7 @@ prerr_endline "Fine sorting"; (fun uri -> prerr_endline ("Stampo " ^ UriManager.string_of_uri uri); try - ObjPp.obj_to_string 80 + ObjPp.obj_to_string 78 style prefix (* FG: mi pare meglio 78 *) (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri)) with _ (* BRRRRRRRRR *) -> "ERRORE IN STAMPA DI " ^ UriManager.string_of_uri uri -- 2.39.2