]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/acic_procedural/proceduralTeX.ml
more comments
[helm.git] / helm / software / components / acic_procedural / proceduralTeX.ml
1 (* Copyright (C) 2003-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 module F   = Format
27 module C   = Cic
28 module DTI = DoubleTypeInference
29 module H   = ProceduralHelpers
30 module T   = ProceduralTypes
31
32 type sorts = (Cic.id, Cic2acic.sort_kind) Hashtbl.t
33
34 let num n =
35    if n < 2 then "" else
36    if n < 27 then String.make 1 (Char.chr (n - 2 + Char.code 'b')) else
37    assert false
38
39 let quote str =
40    Pcre.replace ~pat:"_" ~templ:"\\_" str
41
42 let xn frm = function
43    | C.Anonymous -> assert false
44    | C.Name r    -> F.fprintf frm "%s" (quote r)
45
46 let xr c frm j =
47    try match List.nth c (pred j) with
48       | Some (r, _) -> xn frm r
49       | None        -> assert false
50    with Invalid_argument "nth" -> assert false
51
52 let xs frm = function
53    | C.Set     -> F.fprintf frm "\\Set"
54    | C.Prop    -> F.fprintf frm "\\Prop"
55    | C.CProp _ -> F.fprintf frm "\\CProp"
56    | C.Type _  -> F.fprintf frm "\\Type"
57
58 let rec xt c frm = function
59    | C.Sort s                     ->
60       xs frm s  
61    | C.Const (i, [])              ->
62       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i None None))
63    | C.MutInd (i, n, [])          ->
64       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) None))
65    | C.MutConstruct (i, n, m, []) ->
66       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) (Some m)))
67    | C.Rel j                      ->
68       F.fprintf frm "\\LRef{%a}" (xr c) j
69    | C.Cast (t, u)                ->
70       F.fprintf frm "\\Cast{%a}{%a}" (xt c) u (xt c) t
71    | C.Appl (t :: vs)             ->
72       let z = num (List.length vs) in      
73       F.fprintf frm "\\%sAppl%a{%a}" z (xts c) vs (xt c) t
74    | C.MutCase (_, _, u, v, ts)   ->
75       let z = num (List.length ts) in
76       F.fprintf frm "\\%sCase{%a}{%a}%a" z (xt c) u (xt c) v (xts c) ts
77    | C.LetIn (r, v, w, t)         ->
78       let d = Some (r, C.Def (v, w)) :: c in
79       F.fprintf frm "\\Abbr{%a}{%a}{%a}" xn r (xt c) v (xt d) t
80    | C.Lambda (r, w, t)           ->
81       let d = Some (r, C.Decl w) :: c in
82       if DTI.does_not_occur 1 t then
83          F.fprintf frm "\\CFun{%a}{%a}" (xt c) w (xt d) t
84       else
85          F.fprintf frm "\\Abst{%a}{%a}{%a}" xn r (xt c) w (xt d) t
86    | C.Prod (r, w, t)             ->
87       let d = Some (r, C.Decl w) :: c in
88       if DTI.does_not_occur 1 t then
89          F.fprintf frm "\\LImp{%a}{%a}" (xt c) w (xt d) t
90       else if H.is_prop d t then
91          F.fprintf frm "\\LAll{%a}{%a}{%a}" xn r (xt c) w (xt d) t
92       else
93          F.fprintf frm "\\Prod{%a}{%a}{%a}" xn r (xt c) w (xt d) t
94    | C.Const _                    -> assert false
95    | C.MutInd _                   -> assert false
96    | C.MutConstruct _             -> assert false
97    | C.Var _                      -> assert false
98    | C.Fix _                      -> assert false
99    | C.CoFix _                    -> assert false
100    | C.Meta _                     -> assert false
101    | C.Implicit _                 -> assert false
102    | C.Appl []                    -> assert false
103
104 and xts c frm vs =
105    let map v = F.fprintf frm "{%a}" (xt c) v in
106    List.iter map vs
107
108 let tex_of_term frm c t = xt c frm t
109
110 let tex_of_obj frm = function
111    | C.InductiveDefinition (_, [], _, _) -> ()
112    | C.Constant (_, None, _, [], _)      -> ()
113    | C.Constant (_, Some t, _, [], _)    -> 
114       F.fprintf frm "%a@\n" (xt []) t
115    | C.Constant _                        -> assert false
116    | C.InductiveDefinition _             -> assert false
117    | C.Variable _                        -> assert false
118    | C.CurrentProof _                    -> assert false
119
120 let is_prop sorts id =
121    try match Hashtbl.find sorts id with
122       | `Prop -> true
123       | _     -> false
124    with Not_found -> false
125
126 let tex_of_annterm frm sorts t = 
127
128 let rec xat frm = function
129    | C.ASort (_, s)                   ->
130       xs frm s  
131    | C.AConst (_ ,i, [])              ->
132       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i None None))
133    | C.AMutInd (_, i, n, [])          ->
134       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) None))
135    | C.AMutConstruct (_, i, n, m, []) ->
136       F.fprintf frm "\\GRef{%s}" (quote (H.name_of_uri i (Some n) (Some m)))
137    | C.ARel (_,_, _, r)               ->
138       F.fprintf frm "\\LRef{%s}" (quote r)
139    | C.ACast (_, t, u)                ->
140       F.fprintf frm "\\Cast{%a}{%a}" xat u xat t
141    | C.AAppl (_, t :: vs)             ->
142       let z = num (List.length vs) in      
143       F.fprintf frm "\\%sAppl%a{%a}" z xats vs xat t
144    | C.AMutCase (_, _, _, u, v, ts)   ->
145       let z = num (List.length ts) in
146       F.fprintf frm "\\%sCase{%a}{%a}%a" z xat u xat v xats ts
147    | C.ALetIn (_, r, v, w, t)         ->
148       F.fprintf frm "\\Abbr{%a}{%a}{%a}" xn r xat v xat t
149    | C.ALambda (_, r, w, t)           ->
150       if DTI.does_not_occur 1 (H.cic t) then
151          F.fprintf frm "\\CFun{%a}{%a}" xat w xat t
152       else
153          F.fprintf frm "\\Abst{%a}{%a}{%a}" xn r xat w xat t
154    | C.AProd (id, r, w, t)            ->
155       if DTI.does_not_occur 1 (H.cic t) then
156          F.fprintf frm "\\LImp{%a}{%a}" xat w xat t
157       else if true then
158          F.fprintf frm "\\LAll{%a}{%a}{%a}" xn r xat w xat t
159       else
160          F.fprintf frm "\\Prod{%a}{%a}{%a}" xn r xat w xat t
161    | C.AConst _                       -> assert false
162    | C.AMutInd _                      -> assert false
163    | C.AMutConstruct _                -> assert false
164    | C.AVar _                         -> assert false
165    | C.AFix _                         -> assert false
166    | C.ACoFix _                       -> assert false
167    | C.AMeta _                        -> assert false
168    | C.AImplicit _                    -> assert false
169    | C.AAppl (_, [])                  -> assert false
170
171 and xats frm = function
172    | [] -> F.fprintf frm "{}"
173    | vs -> 
174       let map v = F.fprintf frm "{%a}" xat v in
175       List.iter map vs
176
177 in
178 xat frm t
179
180 let xx frm = function
181    | None   -> assert false
182    | Some r -> F.fprintf frm "%s" (quote r)
183
184 let xh how =
185    if how then "\\dx" else "\\sx"
186
187 let tex_of_steps frm sorts l =
188
189 let xat frm t = tex_of_annterm frm sorts t in
190
191 let rec xl frm = function
192    | []                                                    -> ()
193    | T.Note _ :: l 
194    | T.Statement _ :: l
195    | T.Qed _ :: l                                          ->
196       xl frm l
197    | T.Intros (_, [r], _) :: l                             ->
198       F.fprintf frm "\\Intro{%a}{%a}" xx r xl l
199    | T.LetIn (r, v, _) :: l                                ->
200       F.fprintf frm "\\Pose{%a}{%a}{%a}" xx r xat v xl l
201    | T.Change (u, _, None, _, _) :: l                      ->
202       F.fprintf frm "\\Change{%a}{}{%a}" xat u xl l
203    | T.Change (u, _, Some (s, _), _, _) :: l               ->
204       F.fprintf frm "\\Change{%a}{%s}{%a}" xat u (quote s) xl l
205    | T.Rewrite (b, t, None, _, _) :: l                     ->
206       F.fprintf frm "\\Rewrite{%s}{%a}{}{}{%a}" (xh b) xat t xl l
207    | T.Rewrite (b, t, Some (s1, Some s2), _, _) :: l       ->
208       F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
209          (xh b) xat t (quote s1) (quote s2) xl l
210    | T.Rewrite (b, t, Some (s1, None), _, _) :: l          ->
211       F.fprintf frm "\\Rewrite{%s}{%a}{%s}{%s}{%a}"
212          (xh b) xat t (quote s1) (quote s1) xl l
213    | T.Apply (t, _) :: T.Branch (ls, _) :: l               ->
214       let z = num (List.length ls) in
215       F.fprintf frm "\\%sApply{%a}%a" z xat t xls ls; xl frm l
216    | T.Apply (t, _) :: l                                   ->
217       F.fprintf frm "\\Apply{%a}{%a}" xat t xl l
218    | T.Cases (v, _, _) :: T.Branch (ls, _) :: l            ->
219       let z = num (List.length ls) in
220       F.fprintf frm "\\%sCases{%a}%a" z xat v xls ls; xl frm l
221    | T.Cases (v, _, _) :: l                                ->
222       F.fprintf frm "\\Cases{%a}{%a}" xat v xl l
223    | T.Elim (v, Some t, _, _) :: T.Branch (ls, _) :: l     ->
224       let z = num (List.length ls) in
225       F.fprintf frm "\\%sElim{%a}{%a}{}{}%a" z xat v xat t xls ls; xl frm l
226    | T.Elim (v, Some t, _, _) :: l                         ->
227       F.fprintf frm "\\Elim{%a}{%a}{}{}{%a}" xat v xat t xl l
228    | T.Cut (r, w, _) :: T.Branch ([l1; [T.Id _]], _) :: l2 ->
229       F.fprintf frm "\\Cut{%a}{%a}{%a}{%a}" xx r xat w xl l1 xl l2
230    | T.Inductive _ :: _                                    -> assert false
231    | T.Id _ :: _                                           -> assert false
232    | T.Clear _ :: _                                        -> assert false
233    | T.ClearBody _ :: _                                    -> assert false
234    | T.Branch _ :: _                                       -> assert false
235    | T.Intros _ :: _                                       -> assert false
236    | T.Elim _ :: _                                         -> assert false
237    | T.Cut _ :: _                                          -> assert false
238
239 and xls frm = function
240    | [] -> F.fprintf frm "{}"
241    | ls -> 
242       let map l = F.fprintf frm "{%a}" xl l in
243       List.iter map (List.rev ls)
244
245 in
246 F.fprintf frm "%a@\n" xl l