helm/ocaml/cic_transformations/commandAst.ml

   1 (* Copyright (C) 2004, 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://helm.cs.unibo.it/
  24  *)
  25
  26 type location = CicAst.location
  27
  28   (* TODO do we need this at the ast level? *)
  29   (* in Coq these are all synonymous except definition which is transparent *)
  30 type thm_flavour =
  31   [ `Definition
  32   | `Fact
  33   | `Goal
  34   | `Lemma
  35   | `Remark
  36   | `Theorem
  37   ]
  38
  39 type 'term command =
  40   | Theorem of location *
  41       thm_flavour * string option * 'term * 'term option
  42       (* flavour, name, type, body
  43        * - name is absent when an unnamed theorem is being proved, tipically in
  44        *   interactive usage
  45        * - body is present when its given along with the command, otherwise it
  46        *   will be given in proof editing mode using the tactical language
  47        *)
  48   | Proof of location
  49   | Qed of location *
  50       string option
  51       (* name.
  52        * Name is needed when theorem was started without providing a name
  53        *)
  54
  55 module Script =
  56   struct
  57
  58     type 'term thm_body =
  59         (** body via tactic applications *)
  60       | Tactics of location *
  61           ('term, string) TacticAst.tactic TacticAst.tactical list
  62       | Verbatim of location * 'term  (** body via verbatim term *)
  63
  64     type 'term script_entry =
  65       | Theorem of thm_flavour * string * 'term * 'term thm_body
  66           (* flavour, name, type, body *)
  67
  68     type 'term script = 'term script_entry list
  69
  70   end
  71
  72 (**/**)
  73
  74 (** Just for debugging: not real pretty printers *)
  75
  76 open Printf
  77
  78 let pp_flavour = function
  79   | `Definition -> "Definition"
  80   | `Fact -> "Fact"
  81   | `Goal -> "Goal"
  82   | `Lemma -> "Lemma"
  83   | `Remark -> "Remark"
  84   | `Theorem -> "Theorem"
  85
  86 let pp_command = function
  87   | Theorem (_, flavour, name, typ, body) ->
  88       sprintf "%s %s: %s %s."
  89         (pp_flavour flavour)
  90         (match name with None -> "" | Some name -> name)
  91         (CicAstPp.pp_term typ)
  92         (match body with
  93         | None -> ""
  94         | Some body -> "\\def " ^ CicAstPp.pp_term body)
  95   | Proof _ -> "Proof."
  96   | Qed (_, name) ->
  97       (match name with None -> "Qed." | Some name -> sprintf "Save %s." name)
  98
  99 let pp_script_entry = function
 100   | Script.Theorem (flavour, name, typ, body) ->
 101       sprintf "%s %s: %s%s"
 102         (pp_flavour flavour) name (CicAstPp.pp_term typ)
 103         (match body with
 104         | Script.Tactics (_, tacs) ->
 105             ".\n" ^
 106             (String.concat "\n" (List.map TacticAstPp.pp_tactical tacs)) ^
 107             "\nQed.\n"
 108         | Script.Verbatim (_, body) ->
 109             " \\def " ^ CicAstPp.pp_term body ^ ".\n")
 110
 111 let pp_script script = String.concat "\n\n" (List.map pp_script_entry script)
 112