helm/ocaml/cic_transformations/cic2content.mli

   1 (* Copyright (C) 2000, 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 (**************************************************************************)
  27 (*                                                                        *)
  28 (*                           PROJECT HELM                                 *)
  29 (*                                                                        *)
  30 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
  31 (*                             16/62003                                   *)
  32 (*                                                                        *)
  33 (**************************************************************************)
  34
  35 type recursion_kind = NoRecursive | Recursive | CoRecursive;;
  36
  37 type
  38       'term proof =
  39       { proof_name : string option;
  40         proof_id   : string ;
  41         proof_kind : recursion_kind ;
  42         proof_context : ('term context_element) list ;
  43         proof_apply_context: ('term proof) list;
  44         proof_conclude : 'term conclude_item;
  45       }
  46 and
  47       'term context_element =
  48          Declaration of 'term declaration
  49        | Hypothesis of 'term declaration
  50        | Proof of 'term proof
  51        | Definition of 'term definition
  52        | Joint of 'term joint
  53 and
  54       'term declaration =
  55        { dec_name : string option;
  56          dec_id : string ;
  57          dec_inductive : bool;
  58          dec_aref : string;
  59          dec_type : 'term
  60        }
  61 and
  62       'term definition =
  63        { def_name : string option;
  64          def_id : string ;
  65          def_aref : string ;
  66          def_term : 'term
  67        }
  68 and
  69       'term joint =
  70        { joint_id : string ;
  71          joint_kind : recursion_kind ;
  72          joint_defs : 'term context_element list
  73        }
  74 and
  75       'term conclude_item =
  76        { conclude_id :string;
  77          conclude_aref : string;
  78          conclude_method : string;
  79          conclude_args : ('term arg) list ;
  80          conclude_conclusion : 'term option
  81        }
  82 and
  83       'term arg =
  84          Aux of int
  85        | Premise of premise
  86        | Term of 'term
  87        | ArgProof of 'term proof
  88        | ArgMethod of string (* ???? *)
  89 and
  90       premise =
  91        { premise_id: string;
  92          premise_xref : string ;
  93          premise_binder : string option;
  94          premise_n : int option;
  95        }
  96 ;;
  97
  98 val acic2content :
  99     int ref ->                                (* seed *)
 100     ?name:string option ->                    (* name *)
 101     ids_to_inner_sorts:(Cic.id, string) Hashtbl.t ->
 102                                               (* ids_to_inner_sorts *)
 103     ids_to_inner_types:(Cic.id, Cic2acic.anntypes) Hashtbl.t ->
 104                                               (* ids_to_inner_types *)
 105     Cic.annterm ->                            (* annotated term *)
 106     Cic.annterm proof