matita/components/ng_extraction/miniml.ml

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 (*s Target language for extraction: a core ML called MiniML. *)
  12
  13 open Coq
  14
  15 (* The [signature] type is used to know how many arguments a CIC
  16    object expects, and what these arguments will become in the ML
  17    object. *)
  18
  19 (* We eliminate from terms:  1) types 2) logical parts.
  20    [Kother] stands both for logical or other reasons
  21    (for instance user-declared implicit arguments w.r.t. extraction). *)
  22
  23 type kill_reason = Ktype | Kother
  24
  25 type sign = Keep | Kill of kill_reason
  26
  27
  28 (* Convention: outmost lambda/product gives the head of the list. *)
  29
  30 type signature = sign list
  31
  32 (*s ML type expressions. *)
  33
  34 type ml_type =
  35   | Tarr    of ml_type * ml_type
  36   | Tglob   of NReference.reference * ml_type list
  37   | Tvar    of int
  38   | Tvar'   of int (* same as Tvar, used to avoid clash *)
  39   | Tmeta   of ml_meta (* used during ML type reconstruction *)
  40   | Tdummy  of kill_reason
  41   | Tunknown
  42   | Taxiom
  43
  44 and ml_meta = { id : int; mutable contents : ml_type option }
  45
  46 (* ML type schema.
  47    The integer is the number of variable in the schema. *)
  48
  49 type ml_schema = int * ml_type
  50
  51 (*s ML inductive types. *)
  52
  53 type inductive_kind =
  54   | Singleton
  55   | Coinductive
  56   | Standard
  57   | Record of NReference.reference list
  58
  59 (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
  60    If the inductive is logical ([ip_logical = false]), then all other fields
  61    are unused. Otherwise,
  62    [ip_sign] is a signature concerning the arguments of the inductive,
  63    [ip_vars] contains the names of the type variables surviving in ML,
  64    [ip_types] contains the ML types of all constructors.
  65 *)
  66
  67 type ml_ind_packet = {
  68   ip_reference : NReference.reference;
  69   ip_consreferences : NReference.reference array;
  70   ip_typename : identifier;
  71   ip_consnames : identifier array;
  72   ip_logical : bool;
  73   ip_sign : signature;
  74   ip_vars : identifier list;
  75   ip_types : (ml_type list) array
  76 }
  77
  78 (* [ip_nparams] contains the number of parameters. *)
  79
  80 type ml_ind = {
  81   ind_kind : inductive_kind;
  82   ind_nparams : int;
  83   ind_packets : ml_ind_packet array;
  84 }
  85
  86 (*s ML terms. *)
  87
  88 type ml_ident =
  89   | Dummy
  90   | Id of identifier
  91   | Tmp of identifier
  92
  93 (** We now store some typing information on constructors
  94     and cases to avoid type-unsafe optimisations.
  95     For cases, we also store the set of branches to merge
  96     in a common pattern, either "_ -> c" or "x -> f x"
  97 *)
  98
  99 type constructor_info = {
 100   c_kind : inductive_kind;
 101   c_typs : ml_type list;
 102 }
 103
 104 type branch_same =
 105   | BranchNone
 106   | BranchFun of Intset.t
 107   | BranchCst of Intset.t
 108
 109 type match_info = {
 110   m_kind : inductive_kind;
 111   m_typs : ml_type list;
 112   m_same : branch_same
 113 }
 114
 115 type ml_branch = NReference.reference * ml_ident list * ml_ast
 116
 117 and ml_ast =
 118   | MLrel    of int
 119   | MLapp    of ml_ast * ml_ast list
 120   | MLlam    of ml_ident * ml_ast
 121   | MLletin  of ml_ident * ml_ast * ml_ast
 122   | MLglob   of NReference.reference
 123   | MLcons   of constructor_info * NReference.reference * ml_ast list
 124   | MLcase   of match_info * ml_ast * ml_branch array
 125   | MLfix    of int * identifier array * ml_ast array
 126   | MLexn    of string
 127   | MLdummy
 128   | MLaxiom
 129   | MLmagic  of ml_ast
 130
 131 (*s ML declarations. *)
 132
 133 type ml_decl =
 134   | Dind  of ml_ind
 135   | Dtype of NReference.reference * identifier list * ml_type
 136   | Dterm of NReference.reference * ml_ast * ml_type
 137   | Dfix  of NReference.reference array * ml_ast array * ml_type array
 138
 139 type ml_spec =
 140   | Sind  of ml_ind
 141   | Stype of NReference.reference * identifier list * ml_type option
 142   | Sval  of NReference.reference * ml_type
 143
 144 type ml_specif =
 145   | Spec of ml_spec
 146
 147 and ml_module_sig = (label * ml_specif) list
 148
 149 type ml_structure_elem =
 150   | SEdecl of ml_decl
 151
 152 and ml_module_structure = (label * ml_structure_elem) list
 153
 154 type ml_structure = module_path * ml_module_structure
 155
 156 type ml_signature = module_path * ml_module_sig
 157
 158 type unsafe_needs = {
 159   mldummy : bool;
 160   tdummy : bool;
 161   tunknown : bool;
 162   magic : bool
 163 }
 164
 165 type language_descr = {
 166   keywords : Idset.t;
 167
 168   (* Concerning the source file *)
 169   file_suffix : string;
 170   preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
 171   pp_struct : ml_structure -> std_ppcmds;
 172
 173   (* Concerning a possible interface file *)
 174   sig_suffix : string option;
 175   sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
 176   pp_sig : ml_signature -> std_ppcmds;
 177
 178   (* for an isolated declaration print *)
 179   pp_decl : ml_decl -> std_ppcmds;
 180
 181 }