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 n: string; (* reference name *)
33 s: int list; (* scope *)
36 (* internal functions *******************************************************)
39 X.error ("engine: malformed stack: " ^ s)
42 X.error ("engine: malformed term: " ^ s)
44 (* generic term processing *)
46 let proc_sort is = function
47 | C.Prop -> T.Macro "PROP" :: is
48 | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
49 | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
50 | C.Type _ -> malformed "T1"
52 let rec proc_term is c = function
55 | C.Implicit _ -> malformed "T2"
57 let name = K.resolve_lref c m in
58 T.Macro "LREF" :: T.arg name :: T.free name :: is
60 let riss = L.rev_map (proc_term [] c) ts in
61 T.Macro "APPL" :: T.mk_rev_args riss is
63 let is_w = proc_term [] c w in
64 let is_t = proc_term is (K.add_dec s w c) t in
65 T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
66 | C.Lambda (s, w, t) ->
67 let is_w = proc_term [] c w in
68 let is_t = proc_term is (K.add_dec s w c) t in
69 T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
70 | C.LetIn (s, w, v, t) ->
71 let is_w = proc_term [] c w in
72 let is_v = proc_term [] c v in
73 let is_t = proc_term is (K.add_def s w v c) t in
74 T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
77 | C.Const (R.Ref (u, r)) ->
78 let ss = K.segments_of_uri u in
79 let _, _, _, _, obj = E.get_checked_obj G.status u in
80 let ss, name = K.name_of_reference ss (obj, r) in
81 T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is
82 | C.Match (w, u, v, ts) ->
83 let is_w = proc_term [] c (C.Const w) in
84 let is_u = proc_term [] c u in
85 let is_v = proc_term [] c v in
86 let riss = L.rev_map (proc_term [] c) ts in
87 T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
89 let proc_term is c t = try proc_term is c t with
91 | Invalid_argument "List.nth"
93 | Failure "name_of_reference" -> malformed "T3"
95 (* proof processing *)
97 let typeof c = function
99 | t -> K.whd_typeof c t
106 n = n; s = 1 :: st.s;
110 n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
114 X.rev_map_concat string_of_int "." "" (L.tl st.s)
117 if st.n <> "" || L.tl st.s = [] then ris else
118 T.free (scope st) :: T.Macro "EXIT" :: ris
121 if st.n = "" then ris else
122 T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
124 let mk_dec kind w s ris =
125 let w = if !G.no_types then [] else w in
126 T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
128 let mk_inferred st c t ris =
129 let u = typeof c t in
130 let is_u = proc_term [] c u in
131 mk_dec "DECL" is_u st.n ris
133 let rec proc_proof st ris c t = match t with
138 | C.Prod _ -> malformed "P1"
140 | C.Rel _ -> proc_proof st ris c (C.Appl [t])
141 | C.Lambda (s, w, t) ->
142 let is_w = proc_term [] c w in
143 let ris = mk_open st ris in
144 proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
145 | C.Appl (t0 :: ts) ->
146 let rts = X.rev_neg_filter (K.not_prop2 c) [t0] ts in
147 let ris = T.Macro "STEP" :: mk_inferred st c t ris in
148 let tts = L.rev_map (proc_term [] c) rts in
149 mk_exit st (T.rev_mk_args tts ris)
150 | C.Match (w, u, v, ts) ->
151 let rts = X.rev_neg_filter (K.not_prop2 c) [v] ts in
152 let ris = T.Macro "DEST" :: mk_inferred st c t ris in
153 let tts = L.rev_map (proc_term [] c) rts in
154 mk_exit st (T.rev_mk_args tts ris)
155 | C.LetIn (s, w, v, t) ->
156 let is_w = proc_term [] c w in
157 let ris = mk_open st ris in
158 if K.not_prop1 c w then
159 let is_v = proc_term [] c v in
160 let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
161 proc_proof (next st) ris (K.add_def s w v c) t
163 let ris_v = proc_proof (push st s) ris c v in
164 proc_proof (next st) ris_v (K.add_def s w v c) t
166 let proc_proof rs c t = try proc_proof (init ()) rs c t with
168 | Invalid_argument "List.nth"
170 | Failure "name_of_reference" -> malformed "P2"
171 | V.TypeCheckerFailure s
172 | V.AssertFailure s -> malformed (Lazy.force s)
174 | Failure "tl" -> internal "P2"
176 (* top level processing *)
178 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
180 let proc_item item s ss t =
181 let tt = N.process_top_term s t in (* alpha-conversion *)
182 let is = [T.Macro "end"; T.arg item] in
183 note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free ss :: proc_term is [] tt
185 let proc_top_proof s ss t =
186 let t0 = A.process_top_term s t in (* anticipation *)
187 let tt = N.process_top_term s t0 in (* alpha-conversion *)
188 let ris = [T.free ss; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
189 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
192 let fname = s ^ T.file_ext in
193 begin match !G.list_och with
195 | Some och -> P.fprintf och "%s\n" fname
197 open_out (F.concat !G.out_dir fname)
199 let proc_pair s ss u = function
201 let name = X.rev_map_concat X.id "." "type" ss in
202 let och = open_out_tex name in
203 O.out_text och (proc_item "axiom" s name u);
207 if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
208 else proc_item "proposition", proc_top_proof
210 let name = X.rev_map_concat X.id "." "type" ss in
211 let och = open_out_tex name in
212 O.out_text och (text_u s name u);
214 let name = X.rev_map_concat X.id "." "body" ss in
215 let och = open_out_tex name in
216 O.out_text och (text_t s name t);
219 let proc_fun ss (r, s, i, u, t) =
220 proc_pair s (s :: ss) u (Some t)
222 let proc_constructor ss (r, s, u) =
223 proc_pair s (s :: ss) u None
225 let proc_type ss (r, s, u, cs) =
226 proc_pair s (s :: ss) u None;
227 L.iter (proc_constructor ss) cs
230 let ss = K.segments_of_uri u in
231 let _, _, _, _, obj = E.get_checked_obj G.status u in
233 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
234 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
235 | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts
237 (* interface functions ******************************************************)
239 let process = proc_obj