- matex: support for alpha-conversion completed

[helm.git] / matita / components / binaries / matex / engine.ml

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 165986b473e9a115fc0d6068ae4255f6e00889e5..0174af613c5d7431801f5d975d59afac7caa5592 100644 (file)
--- 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 N = Alpha
 
 type status = {
    n: string;   (* reference name *)
@@ -95,7 +96,7 @@ let proc_term is c t = try proc_term is c t with
 
 let typeof c = function
    | C.Appl [t]
-   | t          -> A.typeof c t
+   | t          -> K.whd_typeof c t
 
 let init () = {
    n =  ""; s = [1]
@@ -142,19 +143,19 @@ let rec proc_proof st ris c t = match t with
       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 (t0 :: ts)     ->
-      let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in
+      let rts = X.rev_neg_filter (K.not_prop2 c) [t0] ts in
       let ris = T.Macro "STEP" :: mk_inferred st c t ris 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 rts = X.rev_neg_filter (K.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
       mk_exit st (T.rev_mk_args tts ris)
    | C.LetIn (s, w, v, t)  -> 
       let is_w = proc_term [] c w in
       let ris = mk_open st ris in
-      if A.not_prop1 c w then
+      if K.not_prop1 c w then
          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
@@ -176,13 +177,15 @@ let proc_proof rs c t = try proc_proof (init ()) rs c t with
 
 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
 
-let proc_item item s t =
+let proc_item item s ss t =
+   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 s :: proc_term is [] t
+   note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term is [] tt
 
-let proc_top_proof s t =
-   let tt = A.process_top_term s t in (* anticipation *)
-   let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
+let proc_top_proof s ss t =
+   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
    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
 
 let open_out_tex s =
@@ -197,20 +200,20 @@ 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);
+         O.out_text och (proc_item "axiom" s name u);
       close_out och
    | Some t ->
       let text_u, text_t =
-         if A.not_prop1 [] u then proc_item "declaration", proc_item "definition"
+         if K.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);
+         O.out_text och (text_u s name 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);
+         O.out_text och (text_t s name t);
       close_out och
 
 let proc_fun ss (r, s, i, u, t) =