-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"
metadata \
library \
acic_content \
- content_pres \
grafite \
+ content_pres \
cic_unification \
whelp \
tactics \
TAGS:
$(H)otags -vi -r .
+metas: $(filter-out METAS/META.helm-binaries, $(METAS))
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
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 \
cicNotationPres.mli \
boxPp.mli \
content2pres.mli \
+ content2Procedural.mli \
objPp.mli \
sequent2pres.mli \
$(NULL)
--- /dev/null
+(* 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 = []
--- /dev/null
+(* 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
+
* 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)
* 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
type print_kind = [ `Env | `Coer ]
+type style = Declarative
+ | Procedural
+
type 'term macro =
(* Whelp's stuff *)
| WHint of loc * 'term
(* 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 *)
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
(* 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"
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)
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
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 =
(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
projects / helm.git / commitdiff