mise a jour commentaires'

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

2 files changed, 114 insertions, 113 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f190a0bffa..8233b9f41c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -141,9 +141,9 @@ 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 context: only variables corresponding 
-   to a real ML type are keeped *)
+(* [renum_db] gives the new de Bruijn indices for variables in an ML
+   term.  This translation is made according to a context: only
+   variables corresponding to a real ML type are keeped *)
 	
 let renum_db ctx n = 
   let rec renum = function
@@ -178,19 +178,19 @@ let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table
 
 (*s Extraction of a type. *)
 
-(* When calling [extract_type] we suppose that the type of [c] is an arity. 
-   This is for example checked in [extract_constr]. 
-   [c] might have $Prop$ as head symbol, or be of type an arity of sort $Prop$. 
+(* When calling [extract_type] we suppose that the type of [c] is an
+   arity.  This is for example checked in [extract_constr].  [c] might
+   have $Prop$ as head symbol, or be of type an arity of sort $Prop$.
    The context [ctx] is the extracted version of [env]. *)
 
 let rec extract_type env ctx c =
-  let genv = Global.env() in  (* QUESTION: inutile car env comme param? *)
   let rec extract_rec env ctx fl c args = 
-    (* In [extract_rec] we accumulate the two contexts, the generated flexible 
-       variables, and the arguments of c. *) 
+    (* We accumulate the two contexts, the generated flexible 
+       variables, and the arguments of [c]. *) 
     let ty = Typing.type_of env Evd.empty c in
     match get_arity env ty with 
-      | None -> assert false (* Cf. precondition. *)
+      | None -> 
+	  assert false (* Cf. precondition. *)
       | Some (Prop Null) ->
 	  Tprop (* [c] is of type an arity of sort $Prop$. *)
       | Some _ -> 
@@ -204,63 +204,65 @@ let rec extract_type env ctx c =
 	    | IsProd (n, t, d) ->
 		assert (args = []); (* A product can't be applied. *)
 		let id = id_of_name n in (* FIXME: capture problem *)
-		let t' = extract_rec env ctx fl t [] in (* Extraction of [t]. *)
-		let env' = push_rel (n,None,t) env in (* New context. *) 
-		let ctx' = (t',id) :: ctx in (* New extracted context. *)
-		let fl' = accum_flex t' fl in (* New flexible variables. *)
-		let d' = extract_rec env' ctx' fl' d [] in (* Extraction of [d]. *)
+		let t' = extract_rec env ctx fl t [] in
+		let env' = push_rel (n,None,t) env in
+		let ctx' = (t',id) :: ctx in
+		let fl' = accum_flex t' fl in
+		let d' = extract_rec env' ctx' fl' d [] in
 		  (match d' with
+ 		     (* If [t] and [c] give ML types, make an arrow type *) 
 		     | Tmltype (_, sign, fl'') -> 
 			 Tmltype (ml_arrow (t',d'), (v_of_t t',id)::sign, fl'')
-			   (* If [t] and [c] give ML types, we make an arrow type. *) 
 		     | et -> et)
 	    | IsLambda (n, t, d) ->
 		assert (args = []); (* [c] is now in head normal form. *)
 		let id = id_of_name n in (* FIXME: capture problem *)
-		let t' = extract_rec env ctx fl t [] in (* Extraction of [t].*)
-		let env' = push_rel (n,None,t) env in (* New context. *)
-		let ctx' = (t',id) :: ctx in (* New extracted context. *)
-		let fl' = accum_flex t' fl in (* New flexible variables. *)
-		let d' = extract_rec env' ctx' fl' d [] in (* Extraction of [d]. *)
+		let t' = extract_rec env ctx fl t [] in
+		let env' = push_rel (n,None,t) env in
+		let ctx' = (t',id) :: ctx in
+		let fl' = accum_flex t' fl in
+		let d' = extract_rec env' ctx' fl' d [] in
 		  (match d' with
 		     | Tmltype (ed, sign, fl'') ->
 			 Tmltype (ed, (v_of_t t',id)::sign, fl'')
-			   (* The extracted type is the extraction of [d], which may use a 
-			      type variable corresponding to the lambda. *)
 		     | et -> et)
 	    | IsApp (d, args') ->
+		(* We just accumulate the arguments. *)
 		extract_rec env ctx fl d (Array.to_list args' @ args)
-		  (* We just accumulate the arguments. *)
 	    | IsRel n ->
 		(match List.nth ctx (pred n) with
 		   | (Tprop | Tmltype _), _ -> assert false 
-			 (* If head symbol is a variable, it must be of type an arity, 
-			    and we already dealt with the case of an arity of sort $Prop$. *)
-		   | Tarity, id -> Tmltype (Tvar id, [], fl)
-			 (* A variable of type an arity gives an ML type variable. *))
+ 		       (* If head symbol is a variable, it must be of 
+			  type an arity, and we already dealt with the
+			  case of an arity of sort $Prop$. *)
+		   | Tarity, id -> Tmltype (Tvar id, [], fl))
 	    | IsConst (sp,a) ->
-		let cty = constant_type genv Evd.empty (sp,a) in 
-		  (* QUESTION: env plutot que genv ? *)
-		  if is_arity env Evd.empty cty then
-		    (match extract_constant sp with
-		       | Emltype (_, sc, flc) -> 
-			   extract_type_app env ctx fl (ConstRef sp,sc,flc) args
-		       | Eprop -> Tprop
-		       | Emlterm _ -> assert false (* The head symbol must be of type an arity. *))
-		  else 
-		    (* We can't keep as ML type abbreviation a CIC constant which type is 
-		       not an arity. So we reduce this constant. *)
-		    let cvalue = constant_value env (sp,a) in
-		      extract_rec env ctx fl (mkApp (cvalue, Array.of_list args)) []
+		let cty = constant_type env Evd.empty (sp,a) in 
+		if is_arity env Evd.empty cty then
+		  (match extract_constant sp with
+		     | Emltype (_, sc, flc) -> 
+			 extract_type_app 
+			   env ctx fl (ConstRef sp,sc,flc) args
+		     | Eprop -> 
+			 Tprop
+		     | Emlterm _ -> 
+			 assert false 
+			 (* The head symbol must be of type an arity. *))
+		else 
+		  (* We can't keep as ML type abbreviation a CIC constant 
+		     which type is not an arity: we reduce this constant. *)
+		  let cvalue = constant_value env (sp,a) in
+		  extract_rec 
+		    env ctx fl (mkApp (cvalue, Array.of_list args)) []
 	    | IsMutInd (spi,_) ->
 		let (si,fli) = extract_inductive spi in
-		  extract_type_app env ctx fl (IndRef spi,si,fli) args
+		extract_type_app env ctx fl (IndRef spi,si,fli) args
 	    | IsMutCase _ 
 	    | IsFix _ ->
 		let id = next_ident_away flexible_name fl in
-		  Tmltype (Tvar id, [], id :: fl)
-		    (* CIC type without counterpart in ML. We generate a fresh type variable and add
-		       it in the "flexible" list. Cf Obj.magic mechanism *)
+		Tmltype (Tvar id, [], id :: fl)
+		(* CIC type without counterpart in ML: we generate a 
+		   new flexible type variable. *) 
 	    | IsCast (c, _) ->
 		extract_rec env ctx fl c args
 	    | _ -> 
@@ -271,17 +273,16 @@ let rec extract_type env ctx c =
   and extract_type_app env ctx fl (r,sc,flc) args =
     let nargs = List.length args in
     assert (List.length sc >= nargs); 
-      (* [r] is of type an arity, so it can't be applied to more than n args, 
-	 where n is the number of products in this arity type. *)
+    (* [r] is of type an arity, so it can't be applied to more than n args, 
+       where n is the number of products in this arity type. *)
     let (sign_args,sign_rest) = list_chop nargs sc in
-      (* We split the signature in used and unused parts *)
     let (mlargs,fl') = 
       List.fold_right 
 	(fun (v,a) ((args,fl) as acc) -> match v with
-	   | (Vdefault | Vprop), _ -> acc (* Here we only keep arguments of type an arity. *)
+	   | (Vdefault | Vprop), _ -> acc
 	   | Varity,_ -> match extract_rec env ctx fl a [] with
 	       | Tarity -> (Miniml.Tarity :: args, fl) 
-		     (* we need to pass an argument, so we pass a dummy type [arity] *)
+  	         (* we pass a dummy type [arity] as argument *)
 	       | Tprop -> (Miniml.Tprop :: args, fl)
 	       | Tmltype (mla,_,fl') -> (mla :: args, fl'))
 	(List.combine sign_args args) 
@@ -294,66 +295,66 @@ let rec extract_type env ctx c =
   extract_rec env ctx [] c []
 
 
-(*s Extraction of a term. *)
-
-(* Preconditions: [c] has a type which is not an arity. 
-   This is normaly checked in [extract_constr] *)
+(*s Extraction of a term. 
+    Precondition: [c] has a type which is not an arity. 
+    This is normaly checked in [extract_constr] *)
 
 and extract_term c =
   let rec extract_rec env ctx c =
     let t = Typing.type_of env Evd.empty c in 
     let s = Typing.type_of env Evd.empty t in
-      if is_Prop (whd_betadeltaiota env Evd.empty s) then
-	Eprop (* Sort of [c] is $Prop$ *)
-	  (* We needn't check whether type of [c] is informative because of the precondition *)
-      else match kind_of_term c with
-	| IsLambda (n, t, d) ->
-	    let id = id_of_name n in
-	    let t' = extract_type env ctx t in 
-	    let env' = push_rel (n,None,t) env in
-	    let ctx' = (t',id) :: ctx in
-	    let d' = extract_rec env' ctx' d in 
-	      (match t' with
-		 | Tarity | Tprop -> d'
-		 | Tmltype _ -> match d' with
-		     | Emlterm a -> Emlterm (MLlam (id, a))
-		     | Eprop -> Eprop
-		     | Emltype _ -> assert false (* extract_type can't answer Emltype *))
-	| IsRel n ->
-	    (match List.nth ctx (pred n) with
-	       | Tarity,_ -> assert false (* Cf. precondition *)
-	       | Tprop,_ -> Eprop
-	       | Tmltype _, _ -> Emlterm (MLrel (renum_db ctx n))) 
-	    (* TODO : magic or not *) 
-	| IsApp (f,a) ->
-	    let tyf = Typing.type_of env Evd.empty f in
-	    let tyf = 
-	      if nb_prod tyf >= Array.length a then 
-		tyf 
-	      else 
-		whd_betadeltaiota env Evd.empty tyf 
-	    in
-	      (match extract_type env ctx tyf with
-		 | Tmltype (_,s,_) -> extract_app env ctx (f,s) (Array.to_list a) 
-		 | Tarity -> assert false (* Cf. precondition *)
-		 | Tprop -> Eprop)
-	| IsConst (sp,_) ->
-	    Emlterm (MLglob (ConstRef sp)) (* TODO eta-expansion *)
-	| IsMutConstruct (cp,_) ->
-	    Emlterm (MLglob (ConstructRef cp))
-	| IsMutCase _ ->
-	    failwith "todo"
-	| IsFix _ ->
-	    failwith "todo"
-	| IsLetIn (n, c1, t1, c2) ->
-	    failwith "todo"
-	      (*i	  (match get_arity env t1 with
-		| Some (Prop Null) -> *)
-	| IsCast (c, _) ->
-	    extract_rec env ctx c
-	| IsMutInd _ | IsProd _ | IsSort _ | IsVar _ 
-	| IsMeta _ | IsEvar _ | IsCoFix _ ->
-	    assert false 
+    (* The only non-informative case: [s] is [Prop] *)
+    if is_Prop (whd_betadeltaiota env Evd.empty s) then
+      Eprop
+    else match kind_of_term c with
+      | IsLambda (n, t, d) ->
+	  let id = id_of_name n in
+	  let t' = extract_type env ctx t in 
+	  let env' = push_rel (n,None,t) env in
+	  let ctx' = (t',id) :: ctx in
+	  let d' = extract_rec env' ctx' d in 
+	  (match t' with
+	     | Tarity | Tprop -> d'
+	     | Tmltype _ -> match d' with
+		 | Emlterm a -> Emlterm (MLlam (id, a))
+		 | Eprop -> Eprop
+		 | Emltype _ -> assert false 
+		     (* [extract_term] can't answer [Emltype] *))
+      | IsRel n ->
+	  (* TODO : magic or not *) 
+	  (match List.nth ctx (pred n) with
+	     | Tarity,_ -> assert false (* Cf. precondition *)
+	     | Tprop,_ -> Eprop
+	     | Tmltype _, _ -> Emlterm (MLrel (renum_db ctx n))) 
+      | IsApp (f,a) ->
+	  let tyf = Typing.type_of env Evd.empty f in
+	  let tyf = 
+	    if nb_prod tyf >= Array.length a then 
+	      tyf 
+	    else 
+	      whd_betadeltaiota env Evd.empty tyf 
+	  in
+	  (match extract_type env ctx tyf with
+	     | Tmltype (_,s,_) -> extract_app env ctx (f,s) (Array.to_list a) 
+	     | Tarity -> assert false (* Cf. precondition *)
+	     | Tprop -> Eprop)
+      | IsConst (sp,_) ->
+	  Emlterm (MLglob (ConstRef sp)) (* TODO eta-expansion *)
+      | IsMutConstruct (cp,_) ->
+	  Emlterm (MLglob (ConstructRef cp))
+      | IsMutCase _ ->
+	  failwith "todo"
+      | IsFix _ ->
+	  failwith "todo"
+      | IsLetIn (n, c1, t1, c2) ->
+	  failwith "todo"
+	    (*i	  (match get_arity env t1 with
+	      | Some (Prop Null) -> *)
+      | IsCast (c, _) ->
+	  extract_rec env ctx c
+      | IsMutInd _ | IsProd _ | IsSort _ | IsVar _ 
+      | IsMeta _ | IsEvar _ | IsCoFix _ ->
+	  assert false 
 
   and extract_app env ctx (f,sf) args =
     let nargs = List.length args in
@@ -382,16 +383,14 @@ and extract_constr_with_type c t =
   let genv = Global.env () in
   let s = Typing.type_of genv Evd.empty t in
   if is_Prop (whd_betadeltaiota genv Evd.empty s) then
-      Eprop (* sort of [c] is $Prop$ *)
+    Eprop
   else match get_arity genv t with
     | Some (Prop Null) -> 
-	Eprop (* type of [c] is an arity of sort $Prop$ *) 
+	Eprop
     | Some _ -> 
 	(match extract_type genv [] c with
-	   | Tprop -> Eprop (* [c] is an arity of sort $Prop$ *)
-	   | Tarity -> Emltype(Miniml.Tarity, [], [])
-	       (*i error "not an ML type"  *)
-	       (* [c] is any other arity *)
+	   | Tprop -> Eprop
+	   | Tarity -> Emltype(Miniml.Tarity, [], []) (* any other arity *)
 	   | Tmltype (t, sign, fl) -> Emltype (t, sign, fl))
     | None -> 
 	extract_term c
@@ -402,9 +401,10 @@ and extract_constr c =
 (*s Extraction of a constant. *)
 		
 and extract_constant sp =
+  (* TODO: Axioms *)
   let cb = Global.lookup_constant sp in
   let typ = cb.const_type in
-  let body = match cb.const_body with Some c -> c | None -> assert false in (* QUESTION: Axiomes ici ?*)
+  let body = match cb.const_body with Some c -> c | None -> assert false in
   extract_constr_with_type body typ
     
 (*s Extraction of an inductive. *)
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index f1f38202a3..d7c99f8662 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -25,4 +25,5 @@ Definition d := [X:Type]X->X.
 
 Extraction d.
 Extraction (d Set).
-Extraction [x:(d Set)]O.
\ No newline at end of file
+Extraction [x:(d Set)]O.
+Extraction (d nat).