plus de commentaires

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

1 files changed, 29 insertions, 2 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 948d11b0d8..00556dd9b2 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -19,7 +19,7 @@ open Mlimport
    object expects, and what these arguments will become in the ML
    object. *)
    
-(* the flag [type_var] gives us information about an identifier
+(* The flag [type_var] gives us information about an identifier
    coming from a Lambda or a Product:
    \begin{itemize}
    \item [Varity] denotes identifiers of type an arity of sort $Set$
@@ -29,6 +29,10 @@ open Mlimport
    \item [Vdefault] represents the other cases 
    \end{itemize} *)
 
+(* Beware: we use signatures as stacks where the top element
+   (i.e. the first one) corresponds to the last abstraction encountered 
+   (i.e De Bruijn index 1) *) 
+
 type type_var = Varity | Vprop | Vdefault
 
 type signature = (type_var * identifier) list
@@ -58,11 +62,14 @@ type extraction_result =
 
 (*s Utility functions. *)
 
+(* Translation between [Type_extraction_result] and [type_var]. *)
+
 let v_of_t = function
   | Tprop -> Vprop
   | Tarity -> Varity
   | Tmltype _ -> Vdefault
 
+(* FIXME: to be moved somewhere else *)
 let array_foldi f a =
   let n = Array.length a in
   let rec fold i v = if i = n then v else fold (succ i) (f i a.(i) v) in
@@ -74,9 +81,15 @@ let id_of_name = function
   | Anonymous -> id_of_string "_"
   | Name id   -> id
 
+(* This function [params_of_sign] extracts the type parameters ('a in Caml)
+   from a signature. *)
+
 let params_of_sign = 
   List.fold_left (fun l v -> match v with Varity,id -> id :: l | _ -> l) []
 
+(* [get_arity c] returns [Some s] if [c] is an arity of sort [s], 
+   and [None] otherwise. *)
+(* FIXME: to be moved ? *)
 let rec get_arity env c =
   match kind_of_term (whd_betadeltaiota env Evd.empty c) with
     | IsProd (x,t,c0) -> get_arity (push_rel_assum (x,t) env) c0
@@ -84,6 +97,10 @@ let rec get_arity env c =
     | IsSort s -> Some s
     | _ -> None
 
+(* The next function transforms an arity into a signature. It is used 
+   for example with the types of inductive definitions, which are known
+   to be already in arity form. *)
+
 let signature_of_arity = 
   let rec sign_of acc env c = match kind_of_term c with
     | IsProd (n, t, c') ->
@@ -103,11 +120,17 @@ let signature_of_arity =
   sign_of []
 
 (* [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t]
-   returns the list [[a;b;...;z]]. *)
+   returns the list [[a;b;...;z]]. It is used when making the ML types
+   of inductive definitions. *)
+
 let rec list_of_ml_arrows = function
   | Tarr (a, b) -> a :: list_of_ml_arrows b
   | t -> []
 
+(* [renum_db] gives the new De Bruijn indices for variables in an ML term.
+   This translation is made according to a signature: only variables tagged
+   [Vdefault] are keeped *)
+	
 let renum_db sign n = 
   let rec renum = function
     | (1, (Vdefault,_)::_) -> 1
@@ -149,6 +172,10 @@ i*)
 
 (*s Extraction of a type. *)
 
+(* When calling [extract_type] we supposet that the type of [c] is an arity.
+   This is normaly checked in [extract_constr]. The signature [sign] is 
+   passed as an argument because FIXME *)
+
 let rec extract_type env sign c =
   let genv = Global.env() in
   let rec extract_rec env sign fl c args =