X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Fengine.ml;h=324d114a949302b28788952074f9962714b80871;hb=cc6fcb70ca4f3cf01205ed722d75a2fdb2aaf779;hp=e9ec76e86b1198dabbdeaf3179c7eeb4e995af8b;hpb=348f1670b30f52db99187b2e92b45348e18ebbbe;p=helm.git

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index e9ec76e86..324d114a9 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -26,6 +26,7 @@ module K = Kernel
 module T = TeX
 module O = TeXOutput
 module A = Anticipate
+module M = Meta
 module N = Alpha
 
 type status = {
@@ -43,27 +44,46 @@ let internal s =
 let malformed s =
    X.error ("engine: malformed term: " ^ s)
 
-let missing s =
-   X.log ("engine: missing macro for " ^ s)
+let missing s l =
+   X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
 
 (* generic term processing *)
 
+let rec rename s = function
+   | []                        -> s
+   | (s1, s2) :: _ when s1 = s -> s2
+   | _ :: tl                   -> rename s tl
+
+let mk_lname s = s
+
+let mk_gname s =
+   rename s !G.alpha_gref
+
 let mk_ptr st name = 
    if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
 
-let get_macro s =
+let get_macro s l =
    let rec aux = function
-      | []                        -> "", G.nan
-      | (r, m, a) :: _ when r = s -> m, a
-      | _ :: tl                   -> aux tl
+      | []                                    -> 
+         if !G.log_missing then missing s l;
+         "", 0
+      | (r, m, a, x) :: _ when r = s && a = l -> m, x
+      | _ :: tl                               -> aux tl
    in
-   aux !G.macro
+   aux !G.macro_gref
 
 let get_head = function
    | C.Const c :: ts ->
       let s, _ = K.resolve_reference c in
-      let macro, arity = get_macro s in
-      if arity = L.length ts then  Some (macro, ts) else begin missing s; None end 
+      let l = L.length ts in
+      let macro, x = get_macro s l in
+      begin match macro with      
+         | ""
+         | "APPL" -> None
+         | _      -> 
+            let ts1, ts2 = X.split_at x ts in
+            Some (macro, s, ts1, ts2) 
+      end 
    | _               -> None
 
 let proc_sort st is = function
@@ -77,39 +97,59 @@ let rec proc_term st is = function
    | C.Meta _
    | C.Implicit _           -> malformed "T2" 
    | C.Rel m                ->
-      let name = K.resolve_lref st.c m in
-      T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
+      let s = K.resolve_lref st.c m in
+      T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
    | C.Appl ts              ->
-      let macro, ts = match get_head ts with
-         | Some (macro, ts) -> macro, ts
-         | None             -> "APPL", ts
-      in
-      let riss = L.rev_map (proc_term st []) ts in
-      T.Macro macro :: T.mk_rev_args riss is
+      begin match get_head ts with
+         | None                      ->
+            let riss = L.rev_map (proc_term st []) ts in
+            T.Macro "APPL" :: T.mk_rev_args riss is
+         | Some (macro, s, [], ts)
+         | Some (macro, s, ts, [])   ->
+            let riss = L.rev_map (proc_term st []) ts in
+            T.Macro macro :: T.free s :: T.mk_rev_args riss is
+         | Some (macro, s, ts1, ts2) ->
+            let riss1 = L.rev_map (proc_term st []) ts1 in
+            let riss2 = L.rev_map (proc_term st []) ts2 in
+            T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
+      end
    | C.Prod (s, w, t)       ->
       let is_w = proc_term st [] w in
-      let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
-      T.Macro "PROD" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
+      let c = K.add_dec s w st.c in
+      let is_t = proc_term {st with c=c} is t in
+      let macro = if K.not_prop1 c t then "PROD" else "FALL" in
+      T.Macro macro :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
    | C.Lambda (s, w, t)     -> 
       let is_w = proc_term st [] w in
       let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
-      T.Macro "ABST" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
+      T.Macro "ABST" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
    | C.LetIn (s, w, v, t)   ->
       let is_w = proc_term st [] w in
       let is_v = proc_term st [] v in
       let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
-      T.Macro "ABBR" :: T.arg s :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
+      T.Macro "ABBR" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
    | C.Sort s               ->
       proc_sort st is s
    | C.Const c              ->
       let s, name = K.resolve_reference c in
-      T.Macro "GREF" :: T.arg name :: T.free s :: is
+      let macro, _ = get_macro s 0 in
+      if macro = "" || macro = "APPL" then
+         T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
+      else
+         T.Macro macro :: T.free s :: is
    | C.Match (w, u, v, ts)  ->
       let is_w = proc_term st [] (C.Const w) in
       let is_u = proc_term st [] u in
       let is_v = proc_term st [] v in
-      let riss = L.rev_map (proc_term st []) ts in
-      T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
+      let riss = X.rev_mapi (proc_case st [] w) K.fst_con ts in
+      let macro = if ts = [] then "CAZE" else "CASE" in
+      T.Macro macro :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
+
+and proc_case st is w i t =
+   let v = R.mk_constructor i w in
+   let is_v = proc_term st [] (C.Const v) in
+   let is_t = proc_term st [] t in
+   T.Macro "PAIR" :: T.Group is_v :: T.Group is_t :: is
 
 let proc_term st is t = try proc_term st is t with
    | E.ObjectNotFound _ 
@@ -146,11 +186,11 @@ let mk_exit st ris =
 
 let mk_open st ris =
    if st.n = "" then ris else
-   T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris
+   T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
 
 let mk_dec st kind w s ris =
    let w = if !G.no_types then [] else w in
-   T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris
+   T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
 
 let mk_inferred st t ris =
    let u = typeof st t in
@@ -208,13 +248,14 @@ let proc_item item s ss t =
    let st = init ss in
    let tt = N.process_top_term s t in (* alpha-conversion *)
    let is = [T.Macro "end"; T.arg item] in
-   note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term st is tt
+   note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
 
 let proc_top_proof s ss t =
+   if !G.no_proofs then [] else
    let st = init ss in
    let t0 = A.process_top_term s t in  (* anticipation *)
    let tt = N.process_top_term s t0 in (* alpha-conversion *)
-   let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
+   let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
 
 let open_out_tex s =
@@ -226,10 +267,14 @@ let open_out_tex s =
    open_out (F.concat !G.out_dir fname)
 
 let proc_pair s ss u = function
-   | None   -> 
+   | None   ->
+      let text_u =
+         if K.not_prop1 [] u then proc_item "assumption"
+         else proc_item "axiom" 
+      in
       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 name u);
+         O.out_text och (text_u s name u);
       close_out och
    | Some t ->
       let text_u, text_t =