From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 15 Feb 2016 21:29:10 +0000 (+0000)
Subject: now every object is output in a LaTeX environment, not just proofs
X-Git-Tag: make_still_working~643
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=709537efda53c6189ed3e3e9877f1f93ac6d512a;p=helm.git

now every object is output in a LaTeX environment, not just proofs
---

diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index 184a6937c..01ab717f1 100644
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -31,8 +31,8 @@ let free s = Group [Free s]
 let mk_segs us =
    L.rev_map arg ("" :: (L.rev us))
 
-let mk_rev_args riss =
-   L.rev_map group ([] :: riss)
+let mk_rev_args riss is =
+   X.rev_map_append group ([] :: riss) is
 
 let rev_mk_args iss is =
    free "" :: X.rev_map_append group iss is
diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 6053456ca..5a1a3e345 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -34,8 +34,6 @@ type status = {
 
 (* internal functions *******************************************************)
 
-let alpha c s = s
-
 let internal s =
    X.error ("engine: malformed stack: " ^ s)
 
@@ -44,53 +42,50 @@ let malformed s =
 
 (* generic term processing *)
 
-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)]
+let proc_sort is = function
+   | C.Prop             -> T.Macro "PROP" :: is
+   | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
+   | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
    | C.Type _           -> malformed "T1"
 
-let rec proc_term c = function
+let rec proc_term is c = function
    | C.Appl []
    | C.Meta _
    | C.Implicit _           -> malformed "T2" 
    | C.Rel m                ->
       let name = K.resolve_lref c m in
-      [T.Macro "LREF"; T.arg name; T.free name]
+      T.Macro "LREF" :: T.arg name :: T.free name :: is
    | C.Appl ts              ->
-      let riss = L.rev_map (proc_term c) ts in
-      T.Macro "APPL" :: T.mk_rev_args riss
+      let riss = L.rev_map (proc_term [] c) ts in
+      T.Macro "APPL" :: T.mk_rev_args riss is
    | C.Prod (s, w, t)       ->
-      let s = alpha c s in
-      let is_w = proc_term c w in
-      let is_t = proc_term (K.add_dec s w c) t in
+      let is_w = proc_term [] c w in
+      let is_t = proc_term is (K.add_dec s w 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 (K.add_dec s w c) t in
+      let is_w = proc_term [] c w in
+      let is_t = proc_term is (K.add_dec s w 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 (K.add_def s w v c) t in
+   | C.LetIn (s, w, v, t)   ->
+      let is_w = proc_term [] c w in
+      let is_v = proc_term [] c v in
+      let is_t = proc_term is (K.add_def s w v 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
+      proc_sort is s
    | C.Const (R.Ref (u, r)) ->
       let ss = K.segments_of_uri u in
       let _, _, _, _, obj = E.get_checked_obj G.status u in  
       let ss, name = K.name_of_reference ss (obj, r) in
-      [T.Macro "GREF"; T.arg name; T.free (X.rev_map_concat X.id "." "type" ss)]
+      T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is
    | 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
-      T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
+      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
+      T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
 
-let proc_term c t = try proc_term c t with
+let proc_term is c t = try proc_term is c t with
    | E.ObjectNotFound _ 
    | Invalid_argument "List.nth"
    | Failure "nth" 
@@ -131,7 +126,7 @@ let mk_dec kind w s ris =
 
 let mk_inferred st c t ris =
    let u = typeof c t in
-   let is_u = proc_term c u in
+   let is_u = proc_term [] c u in
    mk_dec "DECL" is_u st.n ris
 
 let rec proc_proof st ris c t = match t with
@@ -142,27 +137,25 @@ let rec proc_proof st ris c t = match t with
    | C.Prod _              -> malformed "P1"
    | C.Const _
    | C.Rel _               -> proc_proof st ris c (C.Appl [t])
-   | C.Lambda (s, w, t)    -> 
-      let s = alpha c s in
-      let is_w = proc_term c w in
+   | C.Lambda (s, w, t)    ->
+      let is_w = proc_term [] c w in
       let ris = mk_open st ris in
       proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
    | C.Appl ts              ->
       let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
       let ris = T.Macro "STEP" :: mk_inferred st c t ris in
-      let tts = L.rev_map (proc_term c) rts in
+      let tts = L.rev_map (proc_term [] c) rts in
       mk_exit st (T.rev_mk_args tts ris)
    | C.Match (w, u, v, ts) ->
       let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
       let ris = T.Macro "DEST" :: mk_inferred st c t ris in
-      let tts = L.rev_map (proc_term c) rts in
+      let tts = L.rev_map (proc_term [] c) rts in
       mk_exit st (T.rev_mk_args tts ris)
    | C.LetIn (s, w, v, t)  -> 
-      let s = alpha c s in
-      let is_w = proc_term c w in
+      let is_w = proc_term [] c w in
       let ris = mk_open st ris in
       if A.not_prop1 c w then
-         let is_v = proc_term c v in
+         let is_v = proc_term [] c v in
          let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
          proc_proof (next st) ris (K.add_def s w v c) t
       else
@@ -181,31 +174,37 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with
 
 (* top level processing *)
 
-let proc_top_type s t = 
-   [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
-
-let proc_top_body s t = proc_term [] t
+let proc_item item s t =
+   let is = [T.Macro "end"; T.arg item] in
+   T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
 
 let proc_top_proof s t =
    let tt = A.process_top_term s t in (* anticipation *)
-   L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt)
+   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"] in
+   L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
 
 let open_out_tex s =
    open_out (F.concat !G.out_dir (s ^ T.file_ext))
 
-let proc_pair s ss u xt =
-   let name = X.rev_map_concat X.id "." "type" ss in
-   let och = open_out_tex name in
-   O.out_text och (proc_top_type s u);
-   close_out och;
-   match xt with
-      | None   -> ()
-      | Some t ->
-         let name = X.rev_map_concat X.id "." "body" ss in
-         let och = open_out_tex name in
-         let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
-         O.out_text och (text s t);
-         close_out och
+let proc_pair s ss u = function
+   | None   -> 
+      let name = X.rev_map_concat X.id "." "type" ss in
+      let och = open_out_tex name in
+         O.out_text och (proc_item "axiom" s u);
+      close_out och
+   | Some t ->
+      let text_u, text_t =
+         if A.not_prop1 [] u then proc_item "declaration", proc_item "definition"
+         else proc_item "proposition", proc_top_proof
+      in
+      let name = X.rev_map_concat X.id "." "type" ss in
+      let och = open_out_tex name in
+         O.out_text och (text_u s u);
+      close_out och;
+      let name = X.rev_map_concat X.id "." "body" ss in
+      let och = open_out_tex name in
+         O.out_text och (text_t s t);
+      close_out och
 
 let proc_fun ss (r, s, i, u, t) =
    proc_pair s (s :: ss) u (Some t)
diff --git a/matita/components/binaries/matex/test/matex.sty b/matita/components/binaries/matex/test/matex.sty
index 0785eea92..a37b00545 100644
--- a/matita/components/binaries/matex/test/matex.sty
+++ b/matita/components/binaries/matex/test/matex.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{matex}[2016/02/03 MaTeX Package]
+\ProvidesPackage{matex}[2016/02/15 MaTeX Package]
 \RequirePackage{xcolor}
 \ExecuteOptions{}
 \ProcessOptions*
@@ -21,11 +21,16 @@
 \newcommand*\ObjLabel[1]{\label{obj:#1}}
 \newcommand*\ObjRef[1]{\ref{obj:#1}}
 
-\newtheorem{prop}{Proposition}
-\newenvironment{proof}{\setlength\parindent{0pt}}{}
-\newenvironment{ma@step}[1]{\color{#1}}{\\}
+\newcommand*\ma@setlabel[2]{\setlabel{#1}\ObjLabel{#2}}
+\newcommand*\ma@thehead[2]{\textbf{#1 (#2)}\\}
+\newcommand*\ma@theneck[1]{\textsl{#1}\\}
 
-\newcommand*\Object[3]{\begin{prop}[#1]\hfil\\\setlabel{#1}\ObjLabel{#2}#3\end{prop}}
+\newenvironment{axiom}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Axiom}{#1}}{}
+\newenvironment{declaration}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Declaration}{#1}}{}
+\newenvironment{definition}[2]{}{}
+\newenvironment{proposition}[2]{\ma@setlabel{#1}{#2}\ma@thehead{Proposition}{#1}}{}
+\newenvironment{proof}[2]{\ma@theneck{Proof}}{}
+\newenvironment{ma@step}[1]{\color{#1}}{\\}
 
 \newcommand*\ma@tmp{}
 \newcommand*\ma@skip[4]{}