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 *******************************************************)
40 X.error ("engine: malformed stack: " ^ s)
43 X.error ("engine: malformed term: " ^ s)
45 let not_supported () =
46 X.error "engine: object not supported"
48 (* generic term processing *)
50 let proc_sort = function
51 | C.Prop -> [T.Macro "PROP"]
52 | C.Type [`Type, u] -> [T.Macro "TYPE"; T.arg (U.string_of_uri u)]
53 | C.Type [`CProp, u] -> [T.Macro "CROP"; T.arg (U.string_of_uri u)]
54 | C.Type _ -> malformed "T1"
56 let rec proc_term c = function
59 | C.Implicit _ -> malformed "T2"
61 let name = K.resolve_lref c m in
62 [T.Macro "LREF"; T.arg name; T.free name]
64 let riss = L.rev_map (proc_term c) ts in
65 T.Macro "APPL" :: T.mk_rev_args riss
68 let is_w = proc_term c w in
69 let is_t = proc_term (K.add_dec s w c) t in
70 T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
71 | C.Lambda (s, w, t) ->
73 let is_w = proc_term c w in
74 let is_t = proc_term (K.add_dec s w c) t in
75 T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
76 | C.LetIn (s, w, v, t) ->
78 let is_w = proc_term c w in
79 let is_v = proc_term c v in
80 let is_t = proc_term (K.add_def s w v c) t in
81 T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
84 | C.Const (R.Ref (u, r)) ->
85 let ss = K.segments_of_uri u in
86 let _, _, _, _, obj = E.get_checked_obj G.status u in
87 let ss, name = K.name_of_reference ss (obj, r) in
88 [T.Macro "GREF"; T.arg name; T.free (X.rev_map_concat X.id "." "type" ss)]
89 | C.Match (w, u, v, ts) ->
90 let is_w = proc_term c (C.Const w) in
91 let is_u = proc_term c u in
92 let is_v = proc_term c v in
93 let riss = L.rev_map (proc_term c) ts in
94 T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
96 let proc_term c t = try proc_term c t with
98 | Invalid_argument "List.nth"
100 | Failure "name_of_reference" -> malformed "T3"
102 (* proof processing *)
104 let typeof c = function
113 n = n; s = 1 :: st.s;
117 n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
121 X.rev_map_concat string_of_int "." "" (L.tl st.s)
124 if st.n <> "" || L.tl st.s = [] then ris else
125 T.free (scope st) :: T.Macro "EXIT" :: ris
128 if st.n = "" then ris else
129 T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
132 let w = if !G.no_types then [] else w in
133 T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: ris
135 let mk_inferred st c t ris =
136 let u = typeof c t in
137 let is_u = proc_term c u in
140 let rec proc_proof st ris c t = match t with
145 | C.Prod _ -> malformed "P1"
147 | C.Rel _ -> proc_proof st ris c (C.Appl [t])
148 | C.Lambda (s, w, t) ->
150 let is_w = proc_term c w in
151 let ris = mk_open st ris in
152 proc_proof (next st) (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
154 let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
155 let ris = T.Macro "STEP" :: mk_inferred st c t ris in
156 let tts = L.rev_map (proc_term c) rts in
157 mk_exit st (T.rev_mk_args tts ris)
158 | C.Match (w, u, v, ts) ->
159 let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
160 let ris = T.Macro "DEST" :: mk_inferred st c t ris in
161 let tts = L.rev_map (proc_term c) rts in
162 mk_exit st (T.rev_mk_args tts ris)
163 | C.LetIn (s, w, v, t) ->
165 let is_w = proc_term c w in
166 let ris = mk_open st ris in
167 if A.not_prop1 c w then
168 let is_v = proc_term c v in
169 proc_proof (next st) (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
171 let ris_v = proc_proof (push st s) ris c v in
172 proc_proof (next st) ris_v (K.add_def s w v c) t
174 let proc_proof rs c t = try proc_proof (init ()) rs c t with
176 | Invalid_argument "List.nth"
178 | Failure "name_of_reference" -> malformed "P2"
179 | V.TypeCheckerFailure s
180 | V.AssertFailure s -> malformed (Lazy.force s)
182 | Failure "tl" -> internal "P2"
184 (* top level processing *)
186 let proc_top_type s t =
187 [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
189 let proc_top_body s t = proc_term [] t
191 let proc_top_proof s t =
192 let tt = A.process_top_term s t in (* anticipation *)
193 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt)
196 open_out (F.concat !G.out_dir (s ^ T.file_ext))
198 let proc_pair s ss u xt =
199 let name = X.rev_map_concat X.id "." "type" ss in
200 let och = open_out_tex name in
201 O.out_text och (proc_top_type s u);
206 let name = X.rev_map_concat X.id "." "body" ss in
207 let och = open_out_tex name in
208 let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
209 O.out_text och (text s t);
212 let proc_fun ss (r, s, i, u, t) =
213 proc_pair s (s :: ss) u (Some t)
216 let ss = K.segments_of_uri u in
217 let _, _, _, _, obj = E.get_checked_obj G.status u in
219 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
220 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
221 | C.Inductive (_, _, _, _) -> not_supported ()
223 (* interface functions ******************************************************)
225 let process = proc_obj