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
31 n: string; (* reference name *)
32 s: int list; (* scope *)
35 (* internal functions *******************************************************)
38 X.error ("engine: malformed stack: " ^ s)
41 X.error ("engine: malformed term: " ^ s)
43 (* generic term processing *)
45 let proc_sort is = function
46 | C.Prop -> T.Macro "PROP" :: is
47 | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
48 | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
49 | C.Type _ -> malformed "T1"
51 let rec proc_term is c = function
54 | C.Implicit _ -> malformed "T2"
56 let name = K.resolve_lref c m in
57 T.Macro "LREF" :: T.arg name :: T.free name :: is
59 let riss = L.rev_map (proc_term [] c) ts in
60 T.Macro "APPL" :: T.mk_rev_args riss is
62 let is_w = proc_term [] c w in
63 let is_t = proc_term is (K.add_dec s w c) t in
64 T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
65 | C.Lambda (s, w, t) ->
66 let is_w = proc_term [] c w in
67 let is_t = proc_term is (K.add_dec s w c) t in
68 T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
69 | C.LetIn (s, w, v, t) ->
70 let is_w = proc_term [] c w in
71 let is_v = proc_term [] c v in
72 let is_t = proc_term is (K.add_def s w v c) t in
73 T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
76 | C.Const (R.Ref (u, r)) ->
77 let ss = K.segments_of_uri u in
78 let _, _, _, _, obj = E.get_checked_obj G.status u in
79 let ss, name = K.name_of_reference ss (obj, r) in
80 T.Macro "GREF" :: T.arg name :: T.free (X.rev_map_concat X.id "." "type" ss) :: is
81 | C.Match (w, u, v, ts) ->
82 let is_w = proc_term [] c (C.Const w) in
83 let is_u = proc_term [] c u in
84 let is_v = proc_term [] c v in
85 let riss = L.rev_map (proc_term [] c) ts in
86 T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
88 let proc_term is c t = try proc_term is c t with
90 | Invalid_argument "List.nth"
92 | Failure "name_of_reference" -> malformed "T3"
94 (* proof processing *)
96 let typeof c = function
105 n = n; s = 1 :: st.s;
109 n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
113 X.rev_map_concat string_of_int "." "" (L.tl st.s)
116 if st.n <> "" || L.tl st.s = [] then ris else
117 T.free (scope st) :: T.Macro "EXIT" :: ris
120 if st.n = "" then ris else
121 T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
123 let mk_dec kind w s ris =
124 let w = if !G.no_types then [] else w in
125 T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
127 let mk_inferred st c t ris =
128 let u = typeof c t in
129 let is_u = proc_term [] c u in
130 mk_dec "DECL" is_u st.n ris
132 let rec proc_proof st ris c t = match t with
137 | C.Prod _ -> malformed "P1"
139 | C.Rel _ -> proc_proof st ris c (C.Appl [t])
140 | C.Lambda (s, w, t) ->
141 let is_w = proc_term [] c w in
142 let ris = mk_open st ris in
143 proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
144 | C.Appl (t0 :: ts) ->
145 let rts = X.rev_neg_filter (A.not_prop2 c) [t0] ts in
146 let ris = T.Macro "STEP" :: mk_inferred st c t ris in
147 let tts = L.rev_map (proc_term [] c) rts in
148 mk_exit st (T.rev_mk_args tts ris)
149 | C.Match (w, u, v, ts) ->
150 let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
151 let ris = T.Macro "DEST" :: mk_inferred st c t ris in
152 let tts = L.rev_map (proc_term [] c) rts in
153 mk_exit st (T.rev_mk_args tts ris)
154 | C.LetIn (s, w, v, t) ->
155 let is_w = proc_term [] c w in
156 let ris = mk_open st ris in
157 if A.not_prop1 c w then
158 let is_v = proc_term [] c v in
159 let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
160 proc_proof (next st) ris (K.add_def s w v c) t
162 let ris_v = proc_proof (push st s) ris c v in
163 proc_proof (next st) ris_v (K.add_def s w v c) t
165 let proc_proof rs c t = try proc_proof (init ()) rs c t with
167 | Invalid_argument "List.nth"
169 | Failure "name_of_reference" -> malformed "P2"
170 | V.TypeCheckerFailure s
171 | V.AssertFailure s -> malformed (Lazy.force s)
173 | Failure "tl" -> internal "P2"
175 (* top level processing *)
177 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
179 let proc_item item s t =
180 let is = [T.Macro "end"; T.arg item] in
181 note :: T.Macro "begin" :: T.arg item :: T.arg s :: T.free s :: proc_term is [] t
183 let proc_top_proof s t =
184 let tt = A.process_top_term s t in (* anticipation *)
185 let ris = [T.free s; T.arg s; T.arg "proof"; T.Macro "begin"; note] in
186 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof ris [] tt)
189 let fname = s ^ T.file_ext in
190 begin match !G.list_och with
192 | Some och -> P.fprintf och "%s\n" fname
194 open_out (F.concat !G.out_dir fname)
196 let proc_pair s ss u = function
198 let name = X.rev_map_concat X.id "." "type" ss in
199 let och = open_out_tex name in
200 O.out_text och (proc_item "axiom" s u);
204 if A.not_prop1 [] u then proc_item "declaration", proc_item "definition"
205 else proc_item "proposition", proc_top_proof
207 let name = X.rev_map_concat X.id "." "type" ss in
208 let och = open_out_tex name in
209 O.out_text och (text_u s u);
211 let name = X.rev_map_concat X.id "." "body" ss in
212 let och = open_out_tex name in
213 O.out_text och (text_t s t);
216 let proc_fun ss (r, s, i, u, t) =
217 proc_pair s (s :: ss) u (Some t)
219 let proc_constructor ss (r, s, u) =
220 proc_pair s (s :: ss) u None
222 let proc_type ss (r, s, u, cs) =
223 proc_pair s (s :: ss) u None;
224 L.iter (proc_constructor ss) cs
227 let ss = K.segments_of_uri u in
228 let _, _, _, _, obj = E.get_checked_obj G.status u in
230 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
231 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
232 | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts
234 (* interface functions ******************************************************)
236 let process = proc_obj