From 21679cd1397d9c51519dbe439c29c1683b91ec64 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 4 Jan 2016 12:33:52 +0000 Subject: [PATCH] - Const is now processed properly --- matita/components/binaries/matex/TeX.ml | 8 +++- matita/components/binaries/matex/TeXOutput.ml | 2 +- matita/components/binaries/matex/engine.ml | 47 ++++++++++++++----- .../components/binaries/matex/test/matex.sty | 12 +++-- .../components/binaries/matex/test/test.tex | 4 +- 5 files changed, 51 insertions(+), 22 deletions(-) diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml index d5eb305db..c213d4d96 100644 --- a/matita/components/binaries/matex/TeX.ml +++ b/matita/components/binaries/matex/TeX.ml @@ -23,8 +23,12 @@ let empty = [Free ""] let newline = [Free "%\n"] +let group s = Group s + let arg s = Group [Free s] let mk_rev_args riss = - L.rev_map (fun t -> Group t) (empty :: riss) - + L.rev_map group (empty :: riss) + +let mk_segs us = + L.rev_map arg ("" :: (L.rev us)) diff --git a/matita/components/binaries/matex/TeXOutput.ml b/matita/components/binaries/matex/TeXOutput.ml index 609772d47..053c890bb 100644 --- a/matita/components/binaries/matex/TeXOutput.ml +++ b/matita/components/binaries/matex/TeXOutput.ml @@ -17,7 +17,7 @@ module T = TeX (* internal functions *******************************************************) -let special = "_" +let special = "\\{}$&#^_~%" (* LaTeX reserves these characters *) let quote c = if S.contains special c then '.' else c diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml index 30d833317..4f31b07a2 100644 --- a/matita/components/binaries/matex/engine.ml +++ b/matita/components/binaries/matex/engine.ml @@ -58,40 +58,61 @@ let proc_sort = function | 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 proc_gref ss = function + | C.Constant _ , R.Decl -> + T.Macro "GRef" :: T.mk_segs ("type" :: ss) + | C.Constant _ , R.Def _ -> + T.Macro "GRef" :: T.mk_segs ("body" :: ss) + | C.Inductive (_, _, us, _), R.Ind (_, i, _) -> + let _, name, _, _ = L.nth us i in + T.Macro "IRef" :: T.mk_segs (name :: ss) + | C.Inductive (_, _, us, _), R.Con (i, j, _) -> + let _, _, _, ts = L.nth us i in + let _, name, _ = L.nth ts (pred j) in + T.Macro "IRef" :: T.mk_segs (name :: ss) + | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) -> + let _, name, _, _, _ = L.nth ts i in + T.Macro "IRef" :: T.mk_segs (name :: ss) + | C.Fixpoint (_, ts, _) , R.CoFix i -> + let _, name, _, _, _ = L.nth ts i in + T.Macro "IRef" :: T.mk_segs (name :: ss) + | _ -> + malformed "2" let rec proc_term c = function | C.Appl [] | C.Meta _ - | C.Implicit _ -> malformed "2" - | C.Rel m -> + | C.Implicit _ -> malformed "3" + | C.Rel m -> let name = L.nth c (m-1) in [T.Macro "LRef"; T.arg name] - | C.Appl ts -> + | 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) -> + | 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) -> + | 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) -> + | 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 -> + | 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 + | C.Const (R.Ref (u, r)) -> + let ss = segments_of_uri u in + let _, _, _, _, obj = E.get_checked_obj status u in + proc_gref ss (obj, r) + | C.Match (w, u, v, ts) -> + let is_w = proc_term c (C.Const 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 @@ -100,7 +121,7 @@ let rec proc_term c = function let proc_term c t = try proc_term c t with | E.ObjectNotFound _ | Failure "nth" - | Invalid_argument "List.nth" -> malformed "3" + | Invalid_argument "List.nth" -> malformed "4" let open_out_tex s = open_out (F.concat !G.out_dir (s ^ T.file_ext)) diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty index 0312b6d1d..195789fe3 100644 --- a/matita/components/binaries/matex/test/matex.sty +++ b/matita/components/binaries/matex/test/matex.sty @@ -1,12 +1,16 @@ -\newcommand*\Next[1]{\def\TMP{#1}\ifx\TMP\empty\let\next=\relax\else\ #1\let\next=\Next\fi\next} +\newcommand*\Skip[1]{} +\newcommand*\Next[2]{\def\TMP{#2}\ifx\TMP\empty\let\next=\Skip\else #1{#2}\let\next=\Next\fi\next #1} + +\newcommand*\Visit[1]{ #1} \newcommand*\Prop{PROP} \newcommand*\Crop[1]{CROP} \newcommand*\Type[1]{TYPE} \newcommand*\LRef[1]{(L #1)} -\newcommand*\GRef{G} +\newcommand*\GRef[2]{(G #2)\Next\Skip} +\newcommand*\IRef[1]{(J #1)\Next\Skip} \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} +\newcommand*\Appl{(A)\Next\Visit} +\newcommand*\Case[3]{(C #1 #2 #3)\Next\Visit} diff --git a/matita/components/binaries/matex/test/test.tex b/matita/components/binaries/matex/test/test.tex index 1a075c37c..ddf18c408 100644 --- a/matita/components/binaries/matex/test/test.tex +++ b/matita/components/binaries/matex/test/test.tex @@ -6,8 +6,8 @@ \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.type} -\bigskip +% \bigskip -\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} +% \input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body} \end{document} -- 2.39.2