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; (* object name *)
32 s: int list; (* scope *)
35 (* internal functions *******************************************************)
40 X.error ("engine: malformed term: " ^ s)
42 let not_supported () =
43 X.error "engine: object not supported"
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_concat "." "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 *)
106 let w = if !G.no_types then [] else w in
107 T.Group w :: T.free s :: T.arg s :: T.Macro "DECL" :: is
109 let rec proc_proof st ris c t = match t with
114 | C.Prod _ -> malformed "P1"
116 | C.Rel _ -> proc_proof st ris c (C.Appl [t])
117 | C.Lambda (s, w, t) ->
119 let is_w = proc_term c w in
120 proc_proof st (T.Macro "PRIM" :: mk_dec is_w s ris) (K.add_dec s w c) t
122 let rts = X.rev_neg_filter (A.not_prop2 c) [] ts in
123 let ris = T.Macro "STEP" :: ris in
124 let tts = L.rev_map (proc_term c) rts in
125 T.rev_mk_args tts ris
126 | C.Match (w, u, v, ts) ->
127 let rts = X.rev_neg_filter (A.not_prop2 c) [v] ts in
128 let ris = T.Macro "DEST" :: ris in
129 let tts = L.rev_map (proc_term c) rts in
130 T.rev_mk_args tts ris
131 | C.LetIn (s, w, v, t) ->
133 let is_w = proc_term c w in
134 if A.not_prop1 c w then
135 let is_v = proc_term c v in
136 proc_proof st (T.Group is_v :: T.Macro "BODY" :: mk_dec is_w s ris) (K.add_def s w v c) t
138 let ris_v = proc_proof st ris c v in
139 proc_proof st (mk_dec is_w s ris_v) (K.add_def s w v c) t
141 let proc_proof c t = try proc_proof (init "") [] c t with
143 | Invalid_argument "List.nth"
145 | Failure "name_of_reference" -> malformed "P2"
146 | V.TypeCheckerFailure s
147 | V.AssertFailure s -> malformed (Lazy.force s)
149 (* top level processing *)
151 let proc_top_type s t =
152 [T.Macro "Object"; T.arg s; T.free s; T.Group (proc_term [] t)]
154 let proc_top_body s t = proc_term [] t
156 let proc_top_proof s t =
157 let tt = A.process_top_term s t in (* anticipation *)
158 L.rev (proc_proof [] tt)
161 open_out (F.concat !G.out_dir (s ^ T.file_ext))
163 let proc_pair s ss u xt =
164 let name = X.rev_concat "." "type" ss in
165 let och = open_out_tex name in
166 O.out_text och (proc_top_type s u);
171 let name = X.rev_concat "." "body" ss in
172 let och = open_out_tex name in
173 let text = if A.not_prop1 [] u then proc_top_body else proc_top_proof in
174 O.out_text och (text s t);
177 let proc_fun ss (r, s, i, u, t) =
178 proc_pair s (s :: ss) u (Some t)
181 let ss = K.segments_of_uri u in
182 let _, _, _, _, obj = E.get_checked_obj G.status u in
184 | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
185 | C.Fixpoint (_, fs, _) -> L.iter (proc_fun ss) fs
186 | C.Inductive (_, _, _, _) -> not_supported ()
188 (* interface functions ******************************************************)
190 let process = proc_obj