From 2ffd7e47f1872878f6af4084074655da5cf3b23e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 21 Dec 2015 15:13:18 +0000 Subject: [PATCH] - First commit of MaTeX: an utility for typesetting the terms produced by matita il LaTeX - The AST nodes of terms are output as LaTeX macros - The user configures the desired rendering of terms by defining these macros in a LaTeX stylesheet - Each term inside objects is output in a separate file for easy inclusion in the main document - This softare originates from "coqpp", our appication with which Coq terms were typeset in UBLCS 2006-01 as of now, only Constant objects are accepted and Const is not processed properly --- matita/components/binaries/matex/Makefile | 16 +++ matita/components/binaries/matex/TeX.ml | 30 ++++ matita/components/binaries/matex/TeXOutput.ml | 33 +++++ .../components/binaries/matex/TeXOutput.mli | 12 ++ matita/components/binaries/matex/engine.ml | 129 ++++++++++++++++++ matita/components/binaries/matex/engine.mli | 12 ++ matita/components/binaries/matex/matex.ml | 65 +++++++++ matita/components/binaries/matex/options.ml | 31 +++++ matita/components/binaries/matex/options.mli | 16 +++ .../components/binaries/matex/test/matex.sty | 12 ++ .../components/binaries/matex/test/test.tex | 13 ++ 11 files changed, 369 insertions(+) create mode 100644 matita/components/binaries/matex/Makefile create mode 100644 matita/components/binaries/matex/TeX.ml create mode 100644 matita/components/binaries/matex/TeXOutput.ml create mode 100644 matita/components/binaries/matex/TeXOutput.mli create mode 100644 matita/components/binaries/matex/engine.ml create mode 100644 matita/components/binaries/matex/engine.mli create mode 100644 matita/components/binaries/matex/matex.ml create mode 100644 matita/components/binaries/matex/options.ml create mode 100644 matita/components/binaries/matex/options.mli create mode 100644 matita/components/binaries/matex/test/matex.sty create mode 100644 matita/components/binaries/matex/test/test.tex diff --git a/matita/components/binaries/matex/Makefile b/matita/components/binaries/matex/Makefile new file mode 100644 index 000000000..42e1360e2 --- /dev/null +++ b/matita/components/binaries/matex/Makefile @@ -0,0 +1,16 @@ +EXEC = matex +VERSION=0.1.0 + +REQUIRES = helm-ng_library + +include ../Makefile.common + +REGISTRY = $(RT_BASE_DIR)/matita.conf.xml + +OBJ = cic:/matita/lambdadelta/basic_1/pr0/pr0/pr0_confluence.con + +test: + @echo MaTeX $(OBJ) + $(H)./matex.native -O test $(REGISTRY) $(OBJ) + +.PHONY: test diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml new file mode 100644 index 000000000..d5eb305db --- /dev/null +++ b/matita/components/binaries/matex/TeX.ml @@ -0,0 +1,30 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = List + +type item = Free of string (* free text *) + | Macro of string (* macro *) + | Group of text (* group *) + +and text = item list (* structured text *) + +let file_ext = ".tex" + +let empty = [Free ""] + +let newline = [Free "%\n"] + +let arg s = Group [Free s] + +let mk_rev_args riss = + L.rev_map (fun t -> Group t) (empty :: riss) + diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml new file mode 100644 index 000000000..609772d47 --- /dev/null +++ b/matita/components/binaries/matex/TeXOutput.ml @@ -0,0 +1,33 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module L = List +module P = Printf +module S = String + +module T = TeX + +(* internal functions *******************************************************) + +let special = "_" + +let quote c = + if S.contains special c then '.' else c + +let rec out_item och = function + | T.Free s -> P.fprintf och "%s" (S.map quote s) + | T.Macro s -> P.fprintf och "\\%s" s + | T.Group t -> P.fprintf och "%%\n{%a}" out_text t + +(* interface functions ******************************************************) + +and out_text och t = + L.iter (out_item och) t diff --git a/matita/components/binaries/matex/TeXOutput.mli b/matita/components/binaries/matex/TeXOutput.mli new file mode 100644 index 000000000..86c7b5d42 --- /dev/null +++ b/matita/components/binaries/matex/TeXOutput.mli @@ -0,0 +1,12 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val out_text: out_channel -> TeX.text -> unit diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml new file mode 100644 index 000000000..30d833317 --- /dev/null +++ b/matita/components/binaries/matex/engine.ml @@ -0,0 +1,129 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module F = Filename +module L = List +module S = String + +module U = NUri +module R = NReference +module C = NCic +module P = NCicPp +module E = NCicEnvironment + +module G = Options +module T = TeX +module O = TeXOutput + +let status = new P.status + +(* internal functions *******************************************************) + +let rec segments_of_string ss l s = + match try Some (S.index s '/') with Not_found -> None with + | None -> s :: ss + | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1)) + +let segments_of_uri u = + let s = U.string_of_uri u in + let s = F.chop_extension s in + let l = S.length s in + let i = S.index s ':' in + let s = S.sub s (i+2) (l-i-2) in + segments_of_string [] (l-i-2) s + +let rec mk_string sep r = function + | [] -> r + | s :: ss -> mk_string sep (s ^ sep ^ r) ss + +let alpha c s = s + +let malformed s = + failwith ("MaTeX: malformed term: " ^ s) + +let not_supported () = + failwith "MaTeX: object not supported" + +let proc_sort = function + | C.Prop -> [T.Macro "Prop"] + | C.Type [`Type, u] -> [T.Macro "Type"; T.arg (U.string_of_uri u)] + | C.Type [`CProp, u] -> [T.Macro "Crop"; T.arg (U.string_of_uri u)] + | C.Type _ -> malformed "1" + +let proc_gref r = T.Macro "GRef" + +let rec proc_term c = function + | C.Appl [] + | C.Meta _ + | C.Implicit _ -> malformed "2" + | C.Rel m -> + let name = L.nth c (m-1) in + [T.Macro "LRef"; T.arg name] + | C.Appl ts -> + let riss = L.rev_map (proc_term c) ts in + T.Macro "Appl" :: T.mk_rev_args riss + | C.Prod (s, w, t) -> + let s = alpha c s in + let is_w = proc_term c w in + let is_t = proc_term (s::c) t in + T.Macro "Prod" :: T.arg s :: T.Group is_w :: is_t + | C.Lambda (s, w, t) -> + let s = alpha c s in + let is_w = proc_term c w in + let is_t = proc_term (s::c) t in + T.Macro "Abst" :: T.arg s :: T.Group is_w :: is_t + | C.LetIn (s, w, v, t) -> + let s = alpha c s in + let is_w = proc_term c w in + let is_v = proc_term c v in + let is_t = proc_term (s::c) t in + T.Macro "Abbr" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t + | C.Sort s -> + proc_sort s + | C.Const r -> + [proc_gref r] + | C.Match (w, u, v, ts) -> + let is_w = [proc_gref w] in + let is_u = proc_term c u in + let is_v = proc_term c v in + let riss = L.rev_map (proc_term c) ts in + T.Macro "Case" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss + +let proc_term c t = try proc_term c t with + | E.ObjectNotFound _ + | Failure "nth" + | Invalid_argument "List.nth" -> malformed "3" + +let open_out_tex s = + open_out (F.concat !G.out_dir (s ^ T.file_ext)) + +let proc_obj u = + let ss = segments_of_uri u in + let _, _, _, _, obj = E.get_checked_obj status u in + match obj with + | C.Constant (_, _, None, u, _) -> not_supported () + | C.Constant (_, _, Some t, u, _) -> + let name = mk_string "." "body" ss in + let och = open_out_tex name in + O.out_text och (proc_term [] t); + O.out_text och T.newline; + close_out och; + let name = mk_string "." "type" ss in + let och = open_out_tex name in + O.out_text och (proc_term [] u); + O.out_text och T.newline; + close_out och + | C.Fixpoint (_, _, _) -> not_supported () + | C.Inductive (_, _, _, _) -> not_supported () + +(* interface functions ******************************************************) + +let process = proc_obj diff --git a/matita/components/binaries/matex/engine.mli b/matita/components/binaries/matex/engine.mli new file mode 100644 index 000000000..9262be498 --- /dev/null +++ b/matita/components/binaries/matex/engine.mli @@ -0,0 +1,12 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val process: NUri.uri -> unit diff --git a/matita/components/binaries/matex/matex.ml b/matita/components/binaries/matex/matex.ml new file mode 100644 index 000000000..db1785c79 --- /dev/null +++ b/matita/components/binaries/matex/matex.ml @@ -0,0 +1,65 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module A = Arg +module F = Filename + +module U = NUri +module R = Helm_registry +module L = Librarian +module B = NCicLibrary +module C = NCicTypeChecker +module H = HLog + +module G = Options +module E = Engine +module O = TeXOutput + +let help_O = " Set this output directory" +let help_X = " Clear configuration and options" + +let help = "" + +(* internal functions *******************************************************) + +let trusted _ = true + +let no_log _ _ = () + +let init registry = + R.load_from registry; + if !G.no_init then begin + B.init (); + C.set_trust trusted; + H.set_log_callback no_log; + G.no_init := false; + end + +let is_registry s = + F.check_suffix s ".conf.xml" + +let no_init () = + failwith "MaTeX: registry not initialized" + +let malformed s = + failwith ("MaTeX: malformed argument: " ^ s) + +let process s = + if is_registry s then init s + else if !G.no_init then no_init () + else if L.is_uri s then E.process (U.uri_of_string s) + else malformed s + +let main = + A.parse [ + "-O", A.String ((:=) G.out_dir), help_O; + "-X", A.Unit G.clear, help_X; + ] process help diff --git a/matita/components/binaries/matex/options.ml b/matita/components/binaries/matex/options.ml new file mode 100644 index 000000000..dc094441e --- /dev/null +++ b/matita/components/binaries/matex/options.ml @@ -0,0 +1,31 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module F = Filename + +module R = Helm_registry + +(* internal *****************************************************************) + +let default_no_init = true + +let default_out_dir = F.current_dir_name + +(* interface ****************************************************************) + +let no_init = ref default_no_init + +let out_dir = ref default_out_dir + +let clear () = + R.clear (); + no_init := default_no_init; + out_dir := default_out_dir diff --git a/matita/components/binaries/matex/options.mli b/matita/components/binaries/matex/options.mli new file mode 100644 index 000000000..3cd2afa74 --- /dev/null +++ b/matita/components/binaries/matex/options.mli @@ -0,0 +1,16 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val no_init: bool ref + +val out_dir: string ref + +val clear: unit -> unit diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty new file mode 100644 index 000000000..0312b6d1d --- /dev/null +++ b/matita/components/binaries/matex/test/matex.sty @@ -0,0 +1,12 @@ +\newcommand*\Next[1]{\def\TMP{#1}\ifx\TMP\empty\let\next=\relax\else\ #1\let\next=\Next\fi\next} + +\newcommand*\Prop{PROP} +\newcommand*\Crop[1]{CROP} +\newcommand*\Type[1]{TYPE} +\newcommand*\LRef[1]{(L #1)} +\newcommand*\GRef{G} +\newcommand*\Abbr[3]{(D #1 #2 #3) } +\newcommand*\Abst[2]{(I #1 #2) } +\newcommand*\Prod[2]{(P #1 #2) } +\newcommand*\Appl{(A)\Next} +\newcommand*\Case[3]{(C #1 #2 #3)\Next} diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex new file mode 100644 index 000000000..1a075c37c --- /dev/null +++ b/matita/components/binaries/matex/test/test.tex @@ -0,0 +1,13 @@ +\documentclass{article} + +\usepackage{matex} + +\begin{document} + +\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type} + +\bigskip + +\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} + +\end{document} -- 2.39.2