L'extraction c'est magic cvs -n up

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3199 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 59 insertions, 15 deletions

diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 854e3b5e4..bd02958bc 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -12,7 +12,7 @@ open Names
 open Term
 open Libnames
 open Miniml
-
+open Util
 
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
@@ -25,39 +25,82 @@ val id_of_name : name -> identifier
     the list [idn;...;id1] and the term [t]. *)
 
 val collect_lams : ml_ast -> identifier list * ml_ast
-
 val collect_n_lams : int -> ml_ast -> identifier list * ml_ast
-
 val nb_lams : ml_ast -> int
 
 (*s [anonym_lams a n] creates [n] anonymous [MLlam] in front of [a] *)
 
 val anonym_lams : ml_ast -> int -> ml_ast
-
 val dummy_lams : ml_ast -> int -> ml_ast
-
 val named_lams : identifier list -> ml_ast -> ml_ast
+val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast
+
+val eta_args_sign : int -> bool list -> ml_ast list 
+
+(*s Utility functions over ML types with meta. *)
+
+val reset_meta_count : unit -> unit
+val new_meta : 'a -> ml_type
+
+val instantiation : ml_schema -> ml_type
+
+val needs_magic : ml_type * ml_type -> bool
+val put_magic_if : bool -> ml_ast -> ml_ast
+val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
+
+(*s ML type environment. *)
+
+module Mlenv : sig 
+  type t 
+  val empty : t
+    
+  (* get the n-th more recently entered schema and instantiate it. *) 
+  val get : t -> int -> ml_type
 
-(*s Utility functions over ML types. [update_args sp vl t] puts [vl]
-   as arguments behind every inductive types [(sp,_)]. *)
+  (* Adding a type in an environment, after generalizing free meta *)
+  val push_gen : t -> ml_type -> t
+
+  (* Adding a type with no [Tvar] *)
+  val push_type : t -> ml_type -> t
+     
+  (* Adding a type with no [Tvar] nor [Tmeta] *)
+  val push_std_type : t -> ml_type -> t
+end
+
+(*s Utility functions over ML types without meta *)
 
 val kn_of_r : global_reference -> kernel_name
 
 val type_mem_kn : kernel_name -> ml_type -> bool
 
-(*s Utility functions over ML terms. [occurs n t] checks whether [Rel
-    n] occurs (freely) in [t]. [ml_lift] is de Bruijn
-    lifting. *)
+val type_maxvar : ml_type -> int
 
-val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+val type_decomp : ml_type -> ml_type list * ml_type
+val type_recomp : ml_type list * ml_type -> ml_type
+
+val var2var' : ml_type -> ml_type 
 
-val occurs : int -> ml_ast -> bool
+val type_subst : int -> ml_type -> ml_type -> ml_type
+val type_subst_all : ml_type list -> ml_type -> ml_type 
 
-val ml_lift : int -> ml_ast -> ml_ast
+type abbrev_map = global_reference -> ml_type option
 
-val ml_subst : ml_ast -> ml_ast -> ml_ast
+val type_expand : abbrev_map -> ml_type -> ml_type 
+val type_eq : abbrev_map -> ml_type -> ml_type -> bool
+val type_neq : abbrev_map -> ml_type -> ml_type -> bool
+val type_to_sign : abbrev_map -> ml_type -> bool list
+val type_expunge : abbrev_map -> ml_type -> ml_type
 
-val ml_pop : ml_ast -> ml_ast
+
+(*s Utility functions over ML terms. [ast_occurs n t] checks whether [Rel
+    n] occurs (freely) in [t]. [ml_lift] is de Bruijn
+    lifting. *)
+
+val ast_iter : (ml_ast -> unit) -> ml_ast -> unit 
+val ast_occurs : int -> ml_ast -> bool
+val ast_lift : int -> ml_ast -> ml_ast
+val ast_subst : ml_ast -> ml_ast -> ml_ast
+val ast_pop : ml_ast -> ml_ast
 
 (*s Some transformations of ML terms. [optimize] simplify
     all beta redexes (when the argument does not occur, it is just
@@ -71,6 +114,7 @@ val optimize :
 (* Misc. *)
 
 val decl_search : ml_ast -> ml_decl list -> bool
+val decl_type_search : ml_type -> ml_decl list -> bool
 
 val add_ml_decls : 
   extraction_params -> ml_decl list -> ml_decl list