helm/software/components/acic_procedural/acic2Procedural.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 C  = Cic
  27 module L  = Librarian
  28 module G  = GrafiteAst
  29
  30 module H  = ProceduralHelpers
  31 module T  = ProceduralTypes
  32 module P1 = Procedural1
  33 module P2 = Procedural2
  34 module X  = ProceduralTeX
  35
  36 let tex_formatter = ref None
  37
  38 (* object costruction *******************************************************)
  39
  40 let th_flavours = [`Theorem; `Lemma; `Remark; `Fact]
  41
  42 let def_flavours = [`Definition; `Variant]
  43
  44 let get_flavour sorts params context v attrs =
  45    let rec aux = function
  46       | []               ->
  47          if H.is_acic_proof sorts context v then List.hd th_flavours
  48          else List.hd def_flavours
  49       | `Flavour fl :: _ -> fl
  50       | _ :: tl          -> aux tl
  51    in
  52    let flavour_map x y = match x, y with
  53       | None, G.IPAs flavour -> Some flavour
  54       | _                    -> x
  55    in
  56    match List.fold_left flavour_map None params with
  57       | Some fl -> fl
  58       | None    -> aux attrs
  59
  60 let rec is_record = function
  61    | []                           -> None
  62    | `Class (`Record fields) :: _ -> Some fields
  63    | _ :: tl                      -> is_record tl
  64
  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
  71             let text =
  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"
  75                else
  76                   ""
  77             in
  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, "")]
  81          | _                                  ->
  82             failwith "not a theorem, definition, axiom or inductive type"
  83       end
  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, "")]
  90       end
  91    | _                                          ->
  92       failwith "not a theorem, definition, axiom or inductive type"
  93
  94 (* interface functions ******************************************************)
  95
  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
  99       | _                     -> x
 100    in
 101    match List.fold_left level_map None params with
 102       | None
 103       | Some 2 ->
 104          P2.proc_proof
 105             (P2.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
 106       | Some 1 ->
 107          P1.proc_proof
 108             (P1.init ~ids_to_inner_sorts ~ids_to_inner_types params context)
 109       | Some n ->
 110          failwith (
 111             "Procedural reconstruction level not supported: " ^
 112             string_of_int n
 113          )
 114
 115 let procedural_of_acic_object ~ids_to_inner_sorts ~ids_to_inner_types
 116    ?info params anobj =
 117    let proc_proof =
 118       get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params []
 119    in
 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
 124       | None     -> ()
 125       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
 126    in
 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
 131
 132 let procedural_of_acic_term ~ids_to_inner_sorts ~ids_to_inner_types params
 133    context annterm =
 134    let proc_proof =
 135       get_proc_proof ~ids_to_inner_sorts ~ids_to_inner_types params context
 136    in
 137    HLog.debug "Procedural: level 2 transformation";
 138    let steps = proc_proof annterm in
 139    let _ = match !tex_formatter with
 140       | None     -> ()
 141       | Some frm -> X.tex_of_steps frm ids_to_inner_sorts steps
 142    in
 143    HLog.debug "Procedural: grafite rendering";
 144    List.rev (T.render_steps [] steps)
 145
 146 let rec is_debug n = function
 147    | []                   -> false
 148    | G.IPDebug debug :: _ -> n <= debug
 149    | _ :: tl              -> is_debug n tl