1 (* Copyright (C) 2003-2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
30 module H = ProceduralHelpers
31 module T = ProceduralTypes
32 module P1 = Procedural1
33 module P2 = Procedural2
34 module X = ProceduralTeX
36 let tex_formatter = ref None
38 (* object costruction *******************************************************)
40 let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
42 let def_flavours = [`Definition; `Variant]
44 let get_flavour sorts params context v attrs =
45 let rec aux = function
47 if H.is_acic_proof sorts context v then List.hd th_flavours
48 else List.hd def_flavours
49 | `Flavour fl :: _ -> fl
52 let flavour_map x y = match x, y with
53 | None, G.IPAs flavour -> Some flavour
56 match List.fold_left flavour_map None params with
60 let rec is_record = function
62 | `Class (`Record fields) :: _ -> Some fields
63 | _ :: tl -> is_record tl
65 let proc_obj ?(info="") proc_proof sorts params context = function
66 | C.AConstant (_, _, s, Some v, t, [], attrs) ->
67 begin match get_flavour sorts params context v attrs with
68 | flavour when List.mem flavour th_flavours ->
69 let ast = proc_proof v in
70 let steps, nodes = T.count_steps 0 ast, T.count_nodes 0 ast in
72 if List.mem G.IPComments params then
73 Printf.sprintf "%s\n%s%s: %u\n%s: %u\n%s"
74 "COMMENTS" info "Tactics" steps "Final nodes" nodes "END"
78 T.Statement (flavour, Some s, t, None, "") :: ast @ [T.Qed text]
79 | flavour when List.mem flavour def_flavours ->
80 [T.Statement (flavour, Some s, t, Some v, "")]
82 failwith "not a theorem, definition, axiom or inductive type"
84 | C.AConstant (_, _, s, None, t, [], attrs) ->
85 [T.Statement (`Axiom, Some s, t, None, "")]
86 | C.AInductiveDefinition (_, types, [], lpsno, attrs) ->
87 begin match is_record attrs with
88 | None -> [T.Inductive (types, lpsno, "")]
89 | Some fs -> [T.Record (types, lpsno, fs, "")]
92 failwith "not a theorem, definition, axiom or inductive type"
94 (* interface functions ******************************************************)
96 let get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context =
97 let level_map x y = match x, y with
98 | None, G.IPLevel level -> Some level
101 match List.fold_left level_map None params with
105 (P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
108 (P1.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
111 "Procedural reconstruction level not supported: " ^
115 let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
118 get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params []
120 L.time_stamp "P : LEVEL 2 ";
121 HLog.debug "Procedural: level 2 transformation";
122 let steps = proc_obj ?info proc_proof ids_to_inner_sorts params [] anobj in
123 let _ = match !tex_formatter with
125 | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
127 L.time_stamp "P : RENDERING";
128 HLog.debug "Procedural: grafite rendering";
129 let r = List.rev (T.render_steps [] steps) in
130 L.time_stamp "P : DONE "; r
132 let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
135 get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context
137 HLog.debug "Procedural: level 2 transformation";
138 let steps = proc_proof annterm in
139 let _ = match !tex_formatter with
141 | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
143 HLog.debug "Procedural: grafite rendering";
144 List.rev (T.render_steps [] steps)
146 let rec is_debug n = function
148 | G.IPDebug debug :: _ -> n <= debug
149 | _ :: tl -> is_debug n tl