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

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
index 6053456ca..e9ec76e86 100644
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -26,71 +26,92 @@ module K = Kernel
 module T = TeX
 module O = TeXOutput
 module A = Anticipate
+module N = Alpha
 
 type status = {
+   i: string;   (* item name *)
    n: string;   (* reference name *)
    s: int list; (* scope *)
+   c: C.context (* context for kernel calls *)
 } 
 
 (* internal functions *******************************************************)
 
-let alpha c s = s
-
 let internal s =
    X.error ("engine: malformed stack: " ^ s)
 
 let malformed s =
    X.error ("engine: malformed term: " ^ s)
 
+let missing s =
+   X.log ("engine: missing macro for " ^ 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 mk_ptr st name = 
+   if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
+
+let get_macro s =
+   let rec aux = function
+      | []                        -> "", G.nan
+      | (r, m, a) :: _ when r = s -> m, a
+      | _ :: tl                   -> aux tl
+   in
+   aux !G.macro
+
+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 
+   | _               -> None
+
+let proc_sort st 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 st is = 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]
+      let name = K.resolve_lref st.c m in
+      T.Macro "LREF" :: T.arg name :: T.free (mk_ptr st name) :: is
    | C.Appl ts              ->
-      let riss = L.rev_map (proc_term c) ts in
-      T.Macro "APPL" :: T.mk_rev_args riss
+      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
    | 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
-      T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_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
    | 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
-      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
-      T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_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
+   | 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
    | C.Sort s               ->
-      proc_sort 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)]
+      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
    | 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 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 proc_term c t = try proc_term c t with
+let proc_term st is t = try proc_term st is t with
    | E.ObjectNotFound _ 
    | Invalid_argument "List.nth"
    | Failure "nth" 
@@ -98,19 +119,21 @@ let proc_term c t = try proc_term c t with
 
 (* proof processing *)
 
-let typeof c = function
+let typeof st = function
    | C.Appl [t]
-   | t          -> A.typeof c t
+   | t          -> K.whd_typeof st.c t
 
-let init () = {
-   n =  ""; s = [1]
+let init i = {
+   i = i;
+   n =  ""; s = [1]; c = [];
 }
 
-let push st n = {
+let push st n = {st with
    n = n; s = 1 :: st.s;
 }
 
-let next st = {
+let next st f = {st with
+   c = f st.c;
    n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
 }
 
@@ -123,53 +146,51 @@ let mk_exit st ris =
 
 let mk_open st ris =
    if st.n = "" then ris else
-   T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
+   T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg st.n :: T.Macro "OPEN" :: ris
 
-let mk_dec kind w s ris =
+let mk_dec st kind w s ris =
    let w = if !G.no_types then [] else w in
-   T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
+   T.Group w :: T.free (mk_ptr st s) :: T.arg s :: T.Macro kind :: ris
 
-let mk_inferred st c t ris =
-   let u = typeof c t in
-   let is_u = proc_term c u in
-   mk_dec "DECL" is_u st.n ris
+let mk_inferred st t ris =
+   let u = typeof st t in
+   let is_u = proc_term st [] u in
+   mk_dec st "DECL" is_u st.n ris
 
-let rec proc_proof st ris c t = match t with
+let rec proc_proof st ris t = match t with
    | C.Appl []
    | C.Meta _
    | C.Implicit _  
    | C.Sort _
    | 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.Rel _               -> proc_proof st ris (C.Appl [t])
+   | C.Lambda (s, w, t)    ->
+      let is_w = proc_term st [] 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
+      proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
+   | C.Appl (t0 :: ts)     ->
+      let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
+      let ris = T.Macro "STEP" :: mk_inferred st t ris in
+      let tts = L.rev_map (proc_term st []) 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 rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
+      let ris = T.Macro "DEST" :: mk_inferred st t ris in
+      let tts = L.rev_map (proc_term st []) 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 st [] 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 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
+      if K.not_prop1 st.c w then
+         let is_v = proc_term st [] v in
+         let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
+         proc_proof (next st (K.add_def s w v)) ris t
       else
-         let ris_v = proc_proof (push st s) ris c v in
-         proc_proof (next st) ris_v (K.add_def s w v c) t
+         let ris_v = proc_proof (push st s) ris v in
+         proc_proof (next st (K.add_def s w v)) ris_v t
 
-let proc_proof rs c t = try proc_proof (init ()) rs c t with 
+let proc_proof st rs t = try proc_proof st rs t with 
    | E.ObjectNotFound _ 
    | Invalid_argument "List.nth"
    | Failure "nth"
@@ -181,31 +202,48 @@ 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 note = T.Note "This file was automatically generated by MaTeX: do not edit"
 
-let proc_top_body s t = proc_term [] t
+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
 
-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 proc_top_proof s ss t =
+   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
+   L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st 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 fname = s ^ T.file_ext in
+   begin match !G.list_och with
+      | None     -> ()
+      | Some och -> P.fprintf och "%s\n" fname
+   end;
+   open_out (F.concat !G.out_dir fname)
+
+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 name u);
+      close_out och
+   | Some t ->
+      let text_u, text_t =
+         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 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 name t);
+      close_out och
 
 let proc_fun ss (r, s, i, u, t) =
    proc_pair s (s :: ss) u (Some t)