auxiliary executables (xoa, matitadep, probe, matex) ported to dune

[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 8ed2a3d5709254b4afc044e75e2a113db6cd5646..aef5180257f64b7e44578e066b8f5caacc11326c 100644 (file)
--- a/matita/components/binaries/matex/engine.ml
+++ b/matita/components/binaries/matex/engine.ml
@@ -12,7 +12,7 @@
 module F = Filename
 module L = List
 module P = Printf
-module S = String
+(* module S = String *)
 
 module U = NUri
 module R = NReference
@@ -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,8 +44,8 @@ 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 *)
 
@@ -63,23 +64,29 @@ let mk_ptr st name =
 
 let get_macro s l =
    let rec aux = function
-      | []                                 -> ""
-      | (r, m, a) :: _ when r = s && a = l -> m
-      | _ :: 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_gref
 
 let get_head = function
    | C.Const c :: ts ->
       let s, _ = K.resolve_reference c in
-      let macro = get_macro s (L.length ts) in
-      if macro <> "" then Some (macro, s, ts) else begin 
-         if !G.log_missing then missing s;
-         None
+      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
+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
@@ -94,12 +101,17 @@ let rec proc_term st is = function
       T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
    | C.Appl ts              ->
       begin match get_head ts with
-         | 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
-         | None                ->
+         | 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
@@ -120,7 +132,11 @@ let rec proc_term st is = function
       proc_sort st is s
    | C.Const c              ->
       let s, name = K.resolve_reference c in
-      T.Macro "GREF" :: T.arg (mk_gname 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
@@ -198,7 +214,7 @@ let rec proc_proof st ris t = match t with
       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) ->
+   | C.Match (_w, _u, v, ts) ->
       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
@@ -235,6 +251,7 @@ let proc_item item s ss t =
    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 *)
@@ -250,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 =
@@ -269,13 +290,13 @@ let proc_pair s ss u = function
          O.out_text och (text_t s name t);
       close_out och
 
-let proc_fun ss (r, s, i, u, t) =
+let proc_fun ss (_r, s, _i, u, t) =
    proc_pair s (s :: ss) u (Some t)
 
-let proc_constructor ss (r, s, u) =
+let proc_constructor ss (_r, s, u) =
    proc_pair s (s :: ss) u None
 
-let proc_type ss (r, s, u, cs) =
+let proc_type ss (_r, s, u, cs) =
    proc_pair s (s :: ss) u None;
    L.iter (proc_constructor ss) cs