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 (* generic term processing *)
47 let proc_sort = function
48 | C.Prop -> [T.Macro "PROP"]
49 | C.Type [`Type, u] -> [T.Macro "TYPE"; T.arg (U.string_of_uri u)]
50 | C.Type [`CProp, u] -> [T.Macro "CROP"; T.arg (U.string_of_uri u)]
51 | C.Type _ -> malformed "T1"
53 let rec proc_term c = function
56 | C.Implicit _ -> malformed "T2"
58 let name = K.resolve_lref c m in
59 [T.Macro "LREF"; T.arg name; T.free name]
61 let riss = L.rev_map (proc_term c) ts in
62 T.Macro "APPL" :: T.mk_rev_args riss
65 let is_w = proc_term c w in
66 let is_t = proc_term (K.add_dec s w c) t in
67 T.Macro "PROD" :: T.arg s :: T.Group is_w :: is_t
68 | C.Lambda (s, w, t) ->
70 let is_w = proc_term c w in
71 let is_t = proc_term (K.add_dec s w c) t in
72 T.Macro "ABST" :: T.arg s :: T.Group is_w :: is_t
73 | C.LetIn (s, w, v, t) ->
75 let is_w = proc_term c w in
76 let is_v = proc_term c v in
77 let is_t = proc_term (K.add_def s w v c) t in
78 T.Macro "ABBR" :: T.arg s :: T.Group is_w :: T.Group is_v :: is_t
81 | C.Const (R.Ref (u, r)) ->
82 let ss = K.segments_of_uri u in
83 let _, _, _, _, obj = E.get_checked_obj G.status u in
84 let ss, name = K.name_of_reference ss (obj, r) in
85 [T.Macro "GREF"; T.arg name; T.free (X.rev_map_concat X.id "." "type" ss)]
86 | C.Match (w, u, v, ts) ->
87 let is_w = proc_term c (C.Const w) in
88 let is_u = proc_term c u in
89 let is_v = proc_term c v in
90 let riss = L.rev_map (proc_term c) ts in
91 T.Macro "CASE" :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss
93 let proc_term c t = try proc_term c t with
95 | Invalid_argument "List.nth"
97 | Failure "name_of_reference" -> malformed "T3"
99 (* proof processing *)
101 let typeof c = function
110 n = n; s = 1 :: st.s;
114 n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
118 X.rev_map_concat string_of_int "." "" (L.tl st.s)
121 if st.n <> "" || L.tl st.s = [] then ris else
122 T.free (scope st) :: T.Macro "EXIT" :: ris
125 if st.n = "" then ris else
126 T.free (scope st) :: T.free st.n :: T.arg st.n :: T.Macro "OPEN" :: ris
128 let mk_dec kind w s ris =
129 let w = if !G.no_types then [] else w in
130 T.Group w :: T.free s :: T.arg s :: T.Macro kind :: ris
132 let mk_inferred st c t ris =
133 let u = typeof c t in
134 let is_u = proc_term c u in
135 mk_dec "DECL" is_u st.n ris
137 let rec proc_proof st ris c t = match t with
142 | C.Prod _ -> malformed "P1"
144 | C.Rel _ -> proc_proof st ris c (C.Appl [t])
145 | C.Lambda (s, w, t) ->
147 let is_w = proc_term c w in
148 let ris = mk_open st ris in
149 proc_proof (next st) (mk_dec "PRIM" is_w s ris) (K.add_dec s w c) t
151 let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
152 let ris = T.Macro "STEP" :: 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.Match (w, u, v, ts) ->
156 let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
157 let ris = T.Macro "DEST" :: mk_inferred st c t ris in
158 let tts = L.rev_map (proc_term c) rts in
159 mk_exit st (T.rev_mk_args tts ris)
160 | C.LetIn (s, w, v, t) ->
162 let is_w = proc_term c w in
163 let ris = mk_open st ris in
164 if A.not_prop1 c w then
165 let is_v = proc_term c v in
166 let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec "DECL" is_w s ris in
167 proc_proof (next st) ris (K.add_def s w v c) t
169 let ris_v = proc_proof (push st s) ris c v in
170 proc_proof (next st) ris_v (K.add_def s w v c) t
172 let proc_proof rs c t = try proc_proof (init ()) rs c t with
174 | Invalid_argument "List.nth"
176 | Failure "name_of_reference" -> malformed "P2"
177 | V.TypeCheckerFailure s
178 | V.AssertFailure s -> malformed (Lazy.force s)
180 | Failure "tl" -> internal "P2"
182 (* top level processing *)
184 let proc_top_type s t =
185 [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
187 let proc_top_body s t = proc_term [] t
189 let proc_top_proof s t =
190 let tt = A.process_top_term s t in (* anticipation *)
191 L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof [T.arg "proof"; T.Macro "begin"] [] tt)
194 open_out (F.concat !G.out_dir (s ^ T.file_ext))
196 let proc_pair s ss u xt =
197 let name = X.rev_map_concat X.id "." "type" ss in
198 let och = open_out_tex name in
199 O.out_text och (proc_top_type s u);
204 let name = X.rev_map_concat X.id "." "body" ss in
205 let och = open_out_tex name in
206 let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
207 O.out_text och (text s t);
210 let proc_fun ss (r, s, i, u, t) =
211 proc_pair s (s :: ss) u (Some t)
213 let proc_constructor ss (r, s, u) =
214 proc_pair s (s :: ss) u None
216 let proc_type ss (r, s, u, cs) =
217 proc_pair s (s :: ss) u None;
218 L.iter (proc_constructor ss) cs
221 let ss = K.segments_of_uri u in
222 let _, _, _, _, obj = E.get_checked_obj G.status u in
224 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
225 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
226 | C.Inductive (_, _, ts, _) -> L.iter (proc_type ss) ts
228 (* interface functions ******************************************************)
230 let process = proc_obj