]> matita.cs.unibo.it Git - helm.git/commitdiff
we started the infrastructure for the procedural rendering of proofs
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 12 Dec 2006 09:54:14 +0000 (09:54 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 12 Dec 2006 09:54:14 +0000 (09:54 +0000)
14 files changed:
helm/software/components/METAS/meta.helm-content_pres.src
helm/software/components/Makefile
helm/software/components/binaries/transcript/grafite.ml
helm/software/components/content_pres/.depend
helm/software/components/content_pres/Makefile
helm/software/components/content_pres/content2Procedural.ml [new file with mode: 0644]
helm/software/components/content_pres/content2Procedural.mli [new file with mode: 0644]
helm/software/components/content_pres/objPp.ml
helm/software/components/content_pres/objPp.mli
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/matita/matita.ml
helm/software/matita/matitaScript.ml

index 1706818e26a251bb235587862a28994505093630..1e76f9fe8137c9b781b1a07379479f8b4c667f1c 100644 (file)
@@ -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"
index cfe1fd51715ae0a16531cf796172c52ce74e0273..a700970af43c111a9e33140d70d2a5e8d893a09d 100644 (file)
@@ -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))
index cc1b465d789def257a3ffe75db030f11558c5480..dff9fcccde610ac830b8ff2e9b9b4e21537520bb 100644 (file)
@@ -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
index 2de502ee531e8f9cb5715f4afb030a450ded7be7..cddd3d80f9b12b81200a667e97959b30a152b238 100644 (file)
@@ -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 \
index 5613ff9ffc59abad275425c3ff72368cb0fd6ff9..497afc8d228e3be4bd8fb25a20034d4cd8435b4d 100644 (file)
@@ -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 (file)
index 0000000..e09ca0b
--- /dev/null
@@ -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 (file)
index 0000000..14cf247
--- /dev/null
@@ -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
+
index 1eb47dbabb5a899137e5e352871193112cfb378e..49936861f2b2f8bbd12c0ea19ac1b9cab068e630 100644 (file)
  * 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)
index e007c6e7c0bf4b1157cb6948c713b4341b616f75..9367661ec4c782ad2baca66b9579ef6c74f13aff 100644 (file)
@@ -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
index 9c5d56024917795facba7653bc89d1019a192754..8979129158b34bcd8a9ffa03577dca64bfb399e9 100644 (file)
@@ -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 *)
index f51cd0bcaf81ba03f5d57d7f51e732d36a78d757..efc0078862b6ad3bdc43a9a33699d6e3873d8a18 100644 (file)
@@ -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"
index fb0128edb0ceb63c423c53832d4eedb1681dd24a..a78ca811332486a2fced5260c7651f6aee9ae116 100644 (file)
@@ -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)
index 783b8c0231ed14654b623dd93891c248ca861e9c..5a638b48d79bb86fd39188b0c9cbe753aead9e63 100644 (file)
@@ -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
index 12f26036b4a1c20f829090e6ee254f74ed964f0d..1a128fb1c753bfa58cd30c1631997e0742614b41 100644 (file)
@@ -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