From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 contrib/extraction/miniml.mli | 159 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 159 insertions(+)
 create mode 100644 contrib/extraction/miniml.mli

(limited to 'contrib/extraction/miniml.mli')

diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
new file mode 100644
index 00000000..866ff847
--- /dev/null
+++ b/contrib/extraction/miniml.mli
@@ -0,0 +1,159 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: miniml.mli,v 1.46.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+
+(*s Target language for extraction: a core ML called MiniML. *)
+
+open Pp
+open Util
+open Names
+open Libnames
+
+(* The [signature] type is used to know how many arguments a CIC
+   object expects, and what these arguments will become in the ML
+   object. *)
+   
+(* Convention: outmost lambda/product gives the head of the list, 
+   and [true] means that the argument is to be kept. *)
+
+type signature = bool list
+
+(*s ML type expressions. *)
+
+type ml_type = 
+  | Tarr    of ml_type * ml_type
+  | Tglob   of global_reference * ml_type list 
+  | Tvar    of int
+  | Tvar'   of int (* same as Tvar, used to avoid clash *)
+  | Tmeta   of ml_meta (* used during ML type reconstruction *)
+  | Tdummy
+  | Tunknown
+  | Taxiom
+  | Tcustom of string
+
+and ml_meta = { id : int; mutable contents : ml_type option }
+
+(* ML type schema. 
+   The integer is the number of variable in the schema. *)
+
+type ml_schema = int * ml_type 
+
+(*s ML inductive types. *)
+
+type inductive_info = Record | Singleton | Coinductive | Standard
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. 
+   If the inductive is logical ([ip_logical = false]), then all other fields
+   are unused. Otherwise, 
+   [ip_sign] is a signature concerning the arguments of the inductive, 
+   [ip_vars] contains the names of the type variables surviving in ML, 
+   [ip_types] contains the ML types of all constructors.    
+*)
+
+type ml_ind_packet = { 
+  ip_typename : identifier; 
+  ip_consnames : identifier array; 
+  ip_logical : bool;
+  ip_sign : signature; 
+  ip_vars : identifier list; 
+  ip_types : (ml_type list) array }  
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type ml_ind = {
+  ind_info : inductive_info;
+  ind_nparams : int; 	       
+  ind_packets : ml_ind_packet array }
+
+(*s ML terms. *)
+
+type ml_ast = 
+  | MLrel    of int
+  | MLapp    of ml_ast * ml_ast list
+  | MLlam    of identifier * ml_ast
+  | MLletin  of identifier * ml_ast * ml_ast
+  | MLglob   of global_reference
+  | MLcons   of global_reference * ml_ast list
+  | MLcase   of ml_ast * (global_reference * identifier list * ml_ast) array
+  | MLfix    of int * identifier array * ml_ast array
+  | MLexn    of string
+  | MLdummy
+  | MLaxiom
+  | MLmagic  of ml_ast
+
+(*s ML declarations. *)
+
+type ml_decl = 
+  | Dind  of kernel_name * ml_ind
+  | Dtype of global_reference * identifier list * ml_type
+  | Dterm of global_reference * ml_ast * ml_type
+  | Dfix  of global_reference array * ml_ast array * ml_type array
+
+type ml_spec = 
+  | Sind  of kernel_name * ml_ind
+  | Stype of global_reference * identifier list * ml_type option 
+  | Sval  of global_reference * ml_type
+
+type ml_specif = 
+  | Spec of ml_spec 
+  | Smodule of ml_module_type
+  | Smodtype of ml_module_type
+
+and ml_module_type = 
+  | MTident of kernel_name
+  | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
+  | MTsig of mod_self_id * ml_module_sig
+
+and ml_module_sig = (label * ml_specif) list
+
+type ml_structure_elem = 
+  | SEdecl of ml_decl
+  | SEmodule of ml_module
+  | SEmodtype of ml_module_type
+
+and ml_module_expr =
+  | MEident of module_path
+  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr 
+  | MEstruct of mod_self_id * ml_module_structure
+  | MEapply of ml_module_expr * ml_module_expr
+
+and ml_module_structure = (label * ml_structure_elem) list
+
+and ml_module = 
+    { ml_mod_expr : ml_module_expr; 
+      ml_mod_type : ml_module_type }
+
+(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] 
+   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
+
+type ml_structure = (module_path * ml_module_structure) list
+
+type ml_signature = (module_path * ml_module_sig) list
+
+(*s Pretty-printing of MiniML in a given concrete syntax is parameterized
+    by a function [pp_global] that pretty-prints global references. 
+    The resulting pretty-printer is a module of type [Mlpp] providing
+    functions to print types, terms and declarations. *)
+
+module type Mlpp_param = sig
+  val globals : unit -> Idset.t
+  val pp_global : module_path list -> global_reference -> std_ppcmds
+  val pp_module : module_path list -> module_path -> std_ppcmds
+end
+
+module type Mlpp = sig
+  val pp_decl : module_path list -> ml_decl -> std_ppcmds
+  val pp_struct : ml_structure -> std_ppcmds
+  val pp_signature : ml_signature -> std_ppcmds
+end
+
+type extraction_params =  
+  { modular : bool; 
+    mod_name : identifier; 
+    to_appear : global_reference list }
-- 
cgit v1.2.3