- First commit of MaTeX:

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

diff --git a/matita/components/binaries/matex/engine.ml b/matita/components/binaries/matex/engine.ml
new file mode 100644 (file)
index 0000000..30d8333
--- /dev/null
+++ b/matita/components/binaries/matex/engine.ml
@@ -0,0 +1,129 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
+
+module F = Filename
+module L = List
+module S = String
+
+module U = NUri
+module R = NReference
+module C = NCic
+module P = NCicPp
+module E = NCicEnvironment
+
+module G = Options
+module T = TeX
+module O = TeXOutput
+
+let status = new P.status
+
+(* internal functions *******************************************************)
+
+let rec segments_of_string ss l s =
+   match try Some (S.index s '/') with Not_found -> None with
+      | None   -> s :: ss
+      | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
+
+let segments_of_uri u =
+   let s = U.string_of_uri u in
+   let s = F.chop_extension s in
+   let l = S.length s in
+   let i = S.index s ':' in
+   let s = S.sub s (i+2) (l-i-2) in
+   segments_of_string [] (l-i-2) s
+
+let rec mk_string sep r = function
+   | []      -> r 
+   | s :: ss -> mk_string sep (s ^ sep ^ r) ss 
+
+let alpha c s = s
+
+let malformed s =
+   failwith ("MaTeX: malformed term: " ^ s)
+
+let not_supported () =
+   failwith "MaTeX: object not supported"
+
+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)]
+   | C.Type _           -> malformed "1"
+
+let proc_gref r = T.Macro "GRef"
+
+let rec proc_term c = function
+   | C.Appl []
+   | C.Meta _
+   | C.Implicit _         -> malformed "2" 
+   | C.Rel m              ->
+      let name = L.nth c (m-1) in
+      [T.Macro "LRef"; T.arg name]
+   | C.Appl ts            ->
+      let riss = L.rev_map (proc_term c) ts in
+      T.Macro "Appl" :: T.mk_rev_args riss
+  | C.Prod (s, w, t)      ->
+      let s = alpha c s in
+      let is_w = proc_term c w in
+      let is_t = proc_term (s::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 (s::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 (s::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
+  | C.Const r             ->
+      [proc_gref r]
+  | C.Match (w, u, v, ts) ->
+      let is_w = [proc_gref 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 proc_term c t = try proc_term c t with
+   | E.ObjectNotFound _ 
+   | Failure "nth" 
+   | Invalid_argument "List.nth" -> malformed "3"
+
+let open_out_tex s =
+   open_out (F.concat !G.out_dir (s ^ T.file_ext))
+
+let proc_obj u =
+   let ss = segments_of_uri u in
+   let _, _, _, _, obj = E.get_checked_obj status u in 
+   match obj with
+      | C.Constant (_, _, None, u, _)   -> not_supported ()
+      | C.Constant (_, _, Some t, u, _) ->
+         let name = mk_string "." "body" ss in
+         let och = open_out_tex name in
+         O.out_text och (proc_term [] t);
+         O.out_text och T.newline;
+         close_out och;
+         let name = mk_string "." "type" ss in
+         let och = open_out_tex name in
+         O.out_text och (proc_term [] u);
+         O.out_text och T.newline;
+         close_out och
+      | C.Fixpoint (_, _, _)            -> not_supported ()
+      | C.Inductive (_, _, _, _)        -> not_supported ()
+
+(* interface functions ******************************************************)
+
+let process = proc_obj