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
21 module V = NCicTypeChecker
32 i: string; (* item name *)
33 n: string; (* reference name *)
34 s: int list; (* scope *)
35 c: C.context (* context for kernel calls *)
38 (* internal functions *******************************************************)
41 X.error ("engine: malformed stack: " ^ s)
44 X.error ("engine: malformed term: " ^ s)
47 X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
49 (* generic term processing *)
51 let rec rename s = function
53 | (s1, s2) :: _ when s1 = s -> s2
54 | _ :: tl -> rename s tl
59 rename s !G.alpha_gref
62 if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
65 let rec aux = function
67 if !G.log_missing then missing s l;
69 | (r, m, a, x) :: _ when r = s && a = l -> m, x
74 let get_head = function
76 let s, _ = K.resolve_reference c in
77 let l = L.length ts in
78 let macro, x = get_macro s l in
79 begin match macro with
83 let ts1, ts2 = X.split_at x ts in
84 Some (macro, s, ts1, ts2)
88 let proc_sort st is = function
89 | C.Prop -> T.Macro "PROP" :: is
90 | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
91 | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
92 | C.Type _ -> malformed "T1"
94 let rec proc_term st is = function
97 | C.Implicit _ -> malformed "T2"
99 let s = K.resolve_lref st.c m in
100 T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
102 begin match get_head ts with
104 let riss = L.rev_map (proc_term st []) ts in
105 T.Macro "APPL" :: T.mk_rev_args riss is
106 | Some (macro, s, [], ts)
107 | Some (macro, s, ts, []) ->
108 let riss = L.rev_map (proc_term st []) ts in
109 T.Macro macro :: T.free s :: T.mk_rev_args riss is
110 | Some (macro, s, ts1, ts2) ->
111 let riss1 = L.rev_map (proc_term st []) ts1 in
112 let riss2 = L.rev_map (proc_term st []) ts2 in
113 T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
115 | C.Prod (s, w, t) ->
116 let is_w = proc_term st [] w in
117 let c = K.add_dec s w st.c in
118 let is_t = proc_term {st with c=c} is t in
119 let macro = if K.not_prop1 c t then "PROD" else "FALL" in
120 T.Macro macro :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
121 | C.Lambda (s, w, t) ->
122 let is_w = proc_term st [] w in
123 let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
124 T.Macro "ABST" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
125 | C.LetIn (s, w, v, t) ->
126 let is_w = proc_term st [] w in
127 let is_v = proc_term st [] v in
128 let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
129 T.Macro "ABBR" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
133 let s, name = K.resolve_reference c in
134 let macro, _ = get_macro s 0 in
135 if macro = "" || macro = "APPL" then
136 T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
138 T.Macro macro :: T.free s :: is
139 | C.Match (w, u, v, ts) ->
140 let is_w = proc_term st [] (C.Const w) in
141 let is_u = proc_term st [] u in
142 let is_v = proc_term st [] v in
143 let riss = X.rev_mapi (proc_case st [] w) K.fst_con ts in
144 let macro = if ts = [] then "CAZE" else "CASE" in
145 T.Macro macro :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
147 and proc_case st is w i t =
148 let v = R.mk_constructor i w in
149 let is_v = proc_term st [] (C.Const v) in
150 let is_t = proc_term st [] t in
151 T.Macro "PAIR" :: T.Group is_v :: T.Group is_t :: is
153 let proc_term st is t = try proc_term st is t with
155 | Invalid_argument "List.nth"
157 | Failure "name_of_reference" -> malformed "T3"
159 (* proof processing *)
161 let typeof st = function
163 | t -> K.whd_typeof st.c t
167 n = ""; s = [1]; c = [];
170 let push st n = {st with
171 n = n; s = 1 :: st.s;
174 let next st f = {st with
176 n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
180 X.rev_map_concat string_of_int "." "" (L.tl st.s)
183 if st.n <> "" || L.tl st.s = [] then ris else
184 T.free (scope st) :: T.Macro "EXIT" :: ris
187 if st.n = "" then ris else
188 T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
190 let mk_dec st kind w s ris =
191 let w = if !G.no_types then [] else w in
192 T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
194 let mk_inferred st t ris =
195 let u = typeof st t in
196 let is_u = proc_term st [] u in
197 mk_dec st "DECL" is_u st.n ris
199 let rec proc_proof st ris t = match t with
204 | C.Prod _ -> malformed "P1"
206 | C.Rel _ -> proc_proof st ris (C.Appl [t])
207 | C.Lambda (s, w, t) ->
208 let is_w = proc_term st [] w in
209 let ris = mk_open st ris in
210 proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
211 | C.Appl (t0 :: ts) ->
212 let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
213 let ris = T.Macro "STEP" :: mk_inferred st t ris in
214 let tts = L.rev_map (proc_term st []) rts in
215 mk_exit st (T.rev_mk_args tts ris)
216 | C.Match (w, u, v, ts) ->
217 let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
218 let ris = T.Macro "DEST" :: mk_inferred st t ris in
219 let tts = L.rev_map (proc_term st []) rts in
220 mk_exit st (T.rev_mk_args tts ris)
221 | C.LetIn (s, w, v, t) ->
222 let is_w = proc_term st [] w in
223 let ris = mk_open st ris in
224 if K.not_prop1 st.c w then
225 let is_v = proc_term st [] v in
226 let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
227 proc_proof (next st (K.add_def s w v)) ris t
229 let ris_v = proc_proof (push st s) ris v in
230 proc_proof (next st (K.add_def s w v)) ris_v t
232 let proc_proof st rs t = try proc_proof st rs t with
234 | Invalid_argument "List.nth"
236 | Failure "name_of_reference" -> malformed "P2"
237 | V.TypeCheckerFailure s
238 | V.AssertFailure s -> malformed (Lazy.force s)
240 | Failure "tl" -> internal "P2"
242 (* top level processing *)
244 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
246 let proc_item item s ss t =
248 let tt = N.process_top_term s t in (* alpha-conversion *)
249 let is = [T.Macro "end"; T.arg item] in
250 note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
252 let proc_top_proof s ss t =
253 if !G.no_proofs then [] else
255 let t0 = A.process_top_term s t in (* anticipation *)
256 let tt = N.process_top_term s t0 in (* alpha-conversion *)
257 let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
258 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
261 let fname = s ^ T.file_ext in
262 begin match !G.list_och with
264 | Some och -> P.fprintf och "%s\n" fname
266 open_out (F.concat !G.out_dir fname)
268 let proc_pair s ss u = function
271 if K.not_prop1 [] u then proc_item "assumption"
272 else proc_item "axiom"
274 let name = X.rev_map_concat X.id "." "type" ss in
275 let och = open_out_tex name in
276 O.out_text och (text_u s name u);
280 if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
281 else proc_item "proposition", proc_top_proof
283 let name = X.rev_map_concat X.id "." "type" ss in
284 let och = open_out_tex name in
285 O.out_text och (text_u s name u);
287 let name = X.rev_map_concat X.id "." "body" ss in
288 let och = open_out_tex name in
289 O.out_text och (text_t s name t);
292 let proc_fun ss (r, s, i, u, t) =
293 proc_pair s (s :: ss) u (Some t)
295 let proc_constructor ss (r, s, u) =
296 proc_pair s (s :: ss) u None
298 let proc_type ss (r, s, u, cs) =
299 proc_pair s (s :: ss) u None;
300 L.iter (proc_constructor ss) cs
303 let ss = K.segments_of_uri u in
304 let _, _, _, _, obj = E.get_checked_obj G.status u in
306 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
307 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
308 | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts
310 (* interface functions ******************************************************)
312 let process = proc_obj