- Const is now processed properly

diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index d5eb305dbd5cd61038321323290b9066d8edb470..c213d4d9629a689379f39cb0068e13bd4d2fbbfe 100644 (file)
--- 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 609772d47bdc607946f4e94085791ae16fc52db8..053c890bbde243977bee9140a7457eadf8ddf4bd 100644 (file)
--- 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 30d833317935253508fb550517c058f4c07b766d..4f31b07a274e6dd74470ac223248b49b1b80bb85 100644 (file)
--- 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 0312b6d1d30707718c66154afed2af1eebc1b117..195789fe3a64c888e34c2b9d020dd97a471840b2 100644 (file)
--- 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 1a075c37c66b95e51c1e83ff0d552fca5eeb459b..ddf18c40838abf537e74e295a431c646be81d9dc 100644 (file)
--- 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}