2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
20 module E = NCicEnvironment
26 let status = new P.status
28 (* internal functions *******************************************************)
30 let rec segments_of_string ss l s =
31 match try Some (S.index s '/') with Not_found -> None with
33 | Some i -> segments_of_string (S.sub s 0 i :: ss) (l-i-1) (S.sub s (i+1) (l-i-1))
35 let segments_of_uri u =
36 let s = U.string_of_uri u in
37 let s = F.chop_extension s in
39 let i = S.index s ':' in
40 let s = S.sub s (i+2) (l-i-2) in
41 segments_of_string [] (l-i-2) s
43 let rec mk_string sep r = function
45 | s :: ss -> mk_string sep (s ^ sep ^ r) ss
50 failwith ("MaTeX: malformed term: " ^ s)
52 let not_supported () =
53 failwith "MaTeX: object not supported"
55 let proc_sort = function
56 | C.Prop -> [T.Macro "Prop"]
57 | C.Type [`Type, u] -> [T.Macro "Type"; T.arg (U.string_of_uri u)]
58 | C.Type [`CProp, u] -> [T.Macro "Crop"; T.arg (U.string_of_uri u)]
59 | C.Type _ -> malformed "1"
61 let proc_gref ss = function
62 | C.Constant _ , R.Decl ->
63 T.Macro "GRef" :: T.mk_segs ("type" :: ss)
64 | C.Constant _ , R.Def _ ->
65 T.Macro "GRef" :: T.mk_segs ("body" :: ss)
66 | C.Inductive (_, _, us, _), R.Ind (_, i, _) ->
67 let _, name, _, _ = L.nth us i in
68 T.Macro "IRef" :: T.mk_segs (name :: ss)
69 | C.Inductive (_, _, us, _), R.Con (i, j, _) ->
70 let _, _, _, ts = L.nth us i in
71 let _, name, _ = L.nth ts (pred j) in
72 T.Macro "IRef" :: T.mk_segs (name :: ss)
73 | C.Fixpoint (_, ts, _) , R.Fix (i, _, _) ->
74 let _, name, _, _, _ = L.nth ts i in
75 T.Macro "IRef" :: T.mk_segs (name :: ss)
76 | C.Fixpoint (_, ts, _) , R.CoFix i ->
77 let _, name, _, _, _ = L.nth ts i in
78 T.Macro "IRef" :: T.mk_segs (name :: ss)
82 let rec proc_term c = function
85 | C.Implicit _ -> malformed "3"
87 let name = L.nth c (m-1) in
88 [T.Macro "LRef"; T.arg name]
90 let riss = L.rev_map (proc_term c) ts in
91 T.Macro "Appl" :: T.mk_rev_args riss
94 let is_w = proc_term c w in
95 let is_t = proc_term (s::c) t in
96 T.Macro "Prod" :: T.arg s :: T.Group is_w :: is_t
97 | C.Lambda (s, w, t) ->
99 let is_w = proc_term c w in
100 let is_t = proc_term (s::c) t in
101 T.Macro "Abst" :: T.arg s :: T.Group is_w :: is_t
102 | C.LetIn (s, w, v, t) ->
104 let is_w = proc_term c w in
105 let is_v = proc_term c v in
106 let is_t = proc_term (s::c) t in
107 T.Macro "Abbr" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
110 | C.Const (R.Ref (u, r)) ->
111 let ss = segments_of_uri u in
112 let _, _, _, _, obj = E.get_checked_obj status u in
113 proc_gref ss (obj, r)
114 | C.Match (w, u, v, ts) ->
115 let is_w = proc_term c (C.Const w) in
116 let is_u = proc_term c u in
117 let is_v = proc_term c v in
118 let riss = L.rev_map (proc_term c) ts in
119 T.Macro "Case" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
121 let proc_term c t = try proc_term c t with
124 | Invalid_argument "List.nth" -> malformed "4"
127 open_out (F.concat !G.out_dir (s ^ T.file_ext))
130 let ss = segments_of_uri u in
131 let _, _, _, _, obj = E.get_checked_obj status u in
133 | C.Constant (_, _, None, u, _) -> not_supported ()
134 | C.Constant (_, _, Some t, u, _) ->
135 let name = mk_string "." "body" ss in
136 let och = open_out_tex name in
137 O.out_text och (proc_term [] t);
138 O.out_text och T.newline;
140 let name = mk_string "." "type" ss in
141 let och = open_out_tex name in
142 O.out_text och (proc_term [] u);
143 O.out_text och T.newline;
145 | C.Fixpoint (_, _, _) -> not_supported ()
146 | C.Inductive (_, _, _, _) -> not_supported ()
148 (* interface functions ******************************************************)
150 let process = proc_obj