]> matita.cs.unibo.it Git - helm.git/blob - matita/components/binaries/matex/engine.ml
- matex: minor improvements
[helm.git] / matita / components / binaries / matex / engine.ml
1 (*
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.                     
5     ||I||                                                                
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_______________________________________________________________ *)
11
12 module F = Filename
13 module L = List
14 module P = Printf
15 module S = String
16
17 module U = NUri
18 module R = NReference
19 module C = NCic
20 module E = NCicEnvironment
21 module V = NCicTypeChecker
22
23 module X = Ground
24 module G = Options
25 module K = Kernel
26 module T = TeX
27 module O = TeXOutput
28 module A = Anticipate
29 module N = Alpha
30
31 type status = {
32    i: string;   (* item name *)
33    n: string;   (* reference name *)
34    s: int list; (* scope *)
35    c: C.context (* context for kernel calls *)
36
37
38 (* internal functions *******************************************************)
39
40 let internal s =
41    X.error ("engine: malformed stack: " ^ s)
42
43 let malformed s =
44    X.error ("engine: malformed term: " ^ s)
45
46 let missing s l =
47    X.log (P.sprintf "engine: missing macro for %s (%u)" s l)
48
49 (* generic term processing *)
50
51 let rec rename s = function
52    | []                        -> s
53    | (s1, s2) :: _ when s1 = s -> s2
54    | _ :: tl                   -> rename s tl
55
56 let mk_lname s = s
57
58 let mk_gname s =
59    rename s !G.alpha_gref
60
61 let mk_ptr st name = 
62    if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
63
64 let get_macro s l =
65    let rec aux = function
66       | []                                    -> "", 0
67       | (r, m, a, x) :: _ when r = s && a = l -> m, x
68       | _ :: tl                               -> aux tl
69    in
70    aux !G.macro_gref
71
72 let get_head = function
73    | C.Const c :: ts ->
74       let s, _ = K.resolve_reference c in
75       let l = L.length ts in
76       let macro, x = get_macro s l in
77       begin match macro with      
78          | ""     -> 
79             if !G.log_missing then missing s l;
80             None
81          | "APPL" -> None
82          | _      -> 
83             let ts1, ts2 = X.split_at x ts in
84             Some (macro, s, ts1, ts2) 
85       end 
86    | _               -> None
87
88 let proc_sort st is = function
89    | C.Prop             -> T.Macro "PROP" :: is
90    | C.Type [`Type, u]  -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
91    | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is
92    | C.Type _           -> malformed "T1"
93
94 let rec proc_term st is = function
95    | C.Appl []
96    | C.Meta _
97    | C.Implicit _           -> malformed "T2" 
98    | C.Rel m                ->
99       let s = K.resolve_lref st.c m in
100       T.Macro "LREF" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: is
101    | C.Appl ts              ->
102       begin match get_head ts with
103          | None                      ->
104             let riss = L.rev_map (proc_term st []) ts in
105             T.Macro "APPL" :: T.mk_rev_args riss is
106          | Some (macro, s, [], ts)
107          | Some (macro, s, ts, [])   ->
108             let riss = L.rev_map (proc_term st []) ts in
109             T.Macro macro :: T.free s :: T.mk_rev_args riss is
110          | Some (macro, s, ts1, ts2) ->
111             let riss1 = L.rev_map (proc_term st []) ts1 in
112             let riss2 = L.rev_map (proc_term st []) ts2 in
113             T.Macro macro :: T.free s :: T.mk_rev_args riss1 (T.mk_rev_args riss2 is)
114       end
115    | C.Prod (s, w, t)       ->
116       let is_w = proc_term st [] w in
117       let c = K.add_dec s w st.c in
118       let is_t = proc_term {st with c=c} is t in
119       let macro = if K.not_prop1 c t then "PROD" else "FALL" in
120       T.Macro macro :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
121    | C.Lambda (s, w, t)     -> 
122       let is_w = proc_term st [] w in
123       let is_t = proc_term {st with c=K.add_dec s w st.c} is t in
124       T.Macro "ABST" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: is_t
125    | C.LetIn (s, w, v, t)   ->
126       let is_w = proc_term st [] w in
127       let is_v = proc_term st [] v in
128       let is_t = proc_term {st with c=K.add_def s w v st.c} is t in
129       T.Macro "ABBR" :: T.arg (mk_lname s) :: T.free (mk_ptr st s) :: T.Group is_w :: T.Group is_v :: is_t
130    | C.Sort s               ->
131       proc_sort st is s
132    | C.Const c              ->
133       let s, name = K.resolve_reference c in
134       T.Macro "GREF" :: T.arg (mk_gname name) :: T.free s :: is
135    | C.Match (w, u, v, ts)  ->
136       let is_w = proc_term st [] (C.Const w) in
137       let is_u = proc_term st [] u in
138       let is_v = proc_term st [] v in
139       let riss = X.rev_mapi (proc_case st [] w) K.fst_con ts in
140       let macro = if ts = [] then "CAZE" else "CASE" in
141       T.Macro macro :: T.Group is_w :: T.Group is_u :: T.Group is_v :: T.mk_rev_args riss is
142
143 and proc_case st is w i t =
144    let v = R.mk_constructor i w in
145    let is_v = proc_term st [] (C.Const v) in
146    let is_t = proc_term st [] t in
147    T.Macro "PAIR" :: T.Group is_v :: T.Group is_t :: is
148
149 let proc_term st is t = try proc_term st is t with
150    | E.ObjectNotFound _ 
151    | Invalid_argument "List.nth"
152    | Failure "nth" 
153    | Failure "name_of_reference" -> malformed "T3"
154
155 (* proof processing *)
156
157 let typeof st = function
158    | C.Appl [t]
159    | t          -> K.whd_typeof st.c t
160
161 let init i = {
162    i = i;
163    n =  ""; s = [1]; c = [];
164 }
165
166 let push st n = {st with
167    n = n; s = 1 :: st.s;
168 }
169
170 let next st f = {st with
171    c = f st.c;
172    n = ""; s = match st.s with [] -> failwith "hd" | i :: tl -> succ i :: tl
173 }
174
175 let scope st =
176    X.rev_map_concat string_of_int "." "" (L.tl st.s)
177
178 let mk_exit st ris =
179    if st.n <> "" || L.tl st.s = [] then ris else
180    T.free (scope st) :: T.Macro "EXIT" :: ris
181
182 let mk_open st ris =
183    if st.n = "" then ris else
184    T.free (scope st) :: T.free (mk_ptr st st.n) :: T.arg (mk_lname st.n) :: T.Macro "OPEN" :: ris
185
186 let mk_dec st kind w s ris =
187    let w = if !G.no_types then [] else w in
188    T.Group w :: T.free (mk_ptr st s) :: T.arg (mk_lname s) :: T.Macro kind :: ris
189
190 let mk_inferred st t ris =
191    let u = typeof st t in
192    let is_u = proc_term st [] u in
193    mk_dec st "DECL" is_u st.n ris
194
195 let rec proc_proof st ris t = match t with
196    | C.Appl []
197    | C.Meta _
198    | C.Implicit _  
199    | C.Sort _
200    | C.Prod _              -> malformed "P1"
201    | C.Const _
202    | C.Rel _               -> proc_proof st ris (C.Appl [t])
203    | C.Lambda (s, w, t)    ->
204       let is_w = proc_term st [] w in
205       let ris = mk_open st ris in
206       proc_proof (next st (K.add_dec s w)) (mk_dec st "PRIM" is_w s ris) t
207    | C.Appl (t0 :: ts)     ->
208       let rts = X.rev_neg_filter (K.not_prop2 st.c) [t0] ts in
209       let ris = T.Macro "STEP" :: mk_inferred st t ris in
210       let tts = L.rev_map (proc_term st []) rts in
211       mk_exit st (T.rev_mk_args tts ris)
212    | C.Match (w, u, v, ts) ->
213       let rts = X.rev_neg_filter (K.not_prop2 st.c) [v] ts in
214       let ris = T.Macro "DEST" :: mk_inferred st t ris in
215       let tts = L.rev_map (proc_term st []) rts in
216       mk_exit st (T.rev_mk_args tts ris)
217    | C.LetIn (s, w, v, t)  -> 
218       let is_w = proc_term st [] w in
219       let ris = mk_open st ris in
220       if K.not_prop1 st.c w then
221          let is_v = proc_term st [] v in
222          let ris = T.Group is_v :: T.Macro "BODY" :: mk_dec st "DECL" is_w s ris in
223          proc_proof (next st (K.add_def s w v)) ris t
224       else
225          let ris_v = proc_proof (push st s) ris v in
226          proc_proof (next st (K.add_def s w v)) ris_v t
227
228 let proc_proof st rs t = try proc_proof st rs t with 
229    | E.ObjectNotFound _ 
230    | Invalid_argument "List.nth"
231    | Failure "nth"
232    | Failure "name_of_reference" -> malformed "P2"
233    | V.TypeCheckerFailure s
234    | V.AssertFailure s           -> malformed (Lazy.force s)
235    | Failure "hd"
236    | Failure "tl"                -> internal "P2"
237
238 (* top level processing *)
239
240 let note = T.Note "This file was automatically generated by MaTeX: do not edit"
241
242 let proc_item item s ss t =
243    let st = init ss in
244    let tt = N.process_top_term s t in (* alpha-conversion *)
245    let is = [T.Macro "end"; T.arg item] in
246    note :: T.Macro "begin" :: T.arg item :: T.arg (mk_gname s) :: T.free ss :: proc_term st is tt
247
248 let proc_top_proof s ss t =
249    if !G.no_proofs then [] else
250    let st = init ss in
251    let t0 = A.process_top_term s t in  (* anticipation *)
252    let tt = N.process_top_term s t0 in (* alpha-conversion *)
253    let ris = [T.free ss; T.arg (mk_gname s); T.arg "proof"; T.Macro "begin"; note] in
254    L.rev (T.arg "proof" :: T.Macro "end" :: proc_proof st ris tt)
255
256 let open_out_tex s =
257    let fname = s ^ T.file_ext in
258    begin match !G.list_och with
259       | None     -> ()
260       | Some och -> P.fprintf och "%s\n" fname
261    end;
262    open_out (F.concat !G.out_dir fname)
263
264 let proc_pair s ss u = function
265    | None   -> 
266       let name = X.rev_map_concat X.id "." "type" ss in
267       let och = open_out_tex name in
268          O.out_text och (proc_item "axiom" s name u);
269       close_out och
270    | Some t ->
271       let text_u, text_t =
272          if K.not_prop1 [] u then proc_item "declaration", proc_item "definition"
273          else proc_item "proposition", proc_top_proof
274       in
275       let name = X.rev_map_concat X.id "." "type" ss in
276       let och = open_out_tex name in
277          O.out_text och (text_u s name u);
278       close_out och;
279       let name = X.rev_map_concat X.id "." "body" ss in
280       let och = open_out_tex name in
281          O.out_text och (text_t s name t);
282       close_out och
283
284 let proc_fun ss (r, s, i, u, t) =
285    proc_pair s (s :: ss) u (Some t)
286
287 let proc_constructor ss (r, s, u) =
288    proc_pair s (s :: ss) u None
289
290 let proc_type ss (r, s, u, cs) =
291    proc_pair s (s :: ss) u None;
292    L.iter (proc_constructor ss) cs
293
294 let proc_obj u =
295    let ss = K.segments_of_uri u in
296    let _, _, _, _, obj = E.get_checked_obj G.status u in 
297    match obj with 
298       | C.Constant (_, s, xt, u, _) -> proc_pair s ss u xt
299       | C.Fixpoint (_, fs, _)       -> L.iter (proc_fun ss) fs
300       | C.Inductive (_, _, ts, _)   -> L.iter (proc_type ss) ts
301
302 (* interface functions ******************************************************)
303
304 let process = proc_obj