eta-expansion des constructeurs si necessaire (a posteriori en miniML)

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

8 files changed, 227 insertions, 75 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 66b41a0faa..4aebbe7b91 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -18,6 +18,7 @@ open Reduction
 open Inductive
 open Instantiate
 open Miniml
+open Mlutil
 open Mlimport
 open Closure
 
@@ -100,7 +101,7 @@ let array_foldi f a =
 let flexible_name = id_of_string "flex"
 
 let id_of_name = function
-  | Anonymous -> id_of_string "_"
+  | Anonymous -> id_of_string "x"
   | Name id   -> id
 
 (* This function [params_of_sign] extracts the type parameters ('a in Caml)
@@ -205,6 +206,14 @@ let rec push_many_rels_ctx env ctx = function
 let fix_environment env ctx fl tl =
   push_many_rels_ctx env ctx (List.combine fl (Array.to_list tl))
 
+(* Test for the application of a constructor *)
+
+let rec is_constructor_app c = match kind_of_term c with
+  | IsApp (c,_) -> is_constructor_app c
+  | IsCast (c,_) -> is_constructor_app c
+  | IsMutConstruct _ -> true
+  | _ -> false
+
 (* Decomposition of a type beginning with at least n products when reduced *)
 
 let decompose_prod_reduce n env c = 
@@ -213,22 +222,22 @@ let decompose_prod_reduce n env c =
       c 
     else 
       whd_betadeltaiota env Evd.empty c 
-  in decompose_prod_n n c
+  in 
+  decompose_prod_n n c
 
 (* Decomposition of a function expecting n arguments at least. We eta-expanse
    if needed *)
 
 let decompose_lam_eta n env c = 
   let dif = n - (nb_lam c) in 
-  if (dif <= 0) then 
+  if dif <= 0 then 
     decompose_lam_n n c
   else 
     let tyc = Typing.type_of env Evd.empty c in
     let (type_binders,_) = decompose_prod_reduce n env tyc in
     let (binders, e) = decompose_lam c in 
     let binders = (list_firstn dif type_binders) @ binders in 
-    let e =
-      applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
+    let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in
     (binders, e)
 
 
@@ -432,7 +441,11 @@ and extract_term_with_type env ctx c t =
     | IsConst (sp,_) ->
 	Rmlterm (MLglob (ConstRef sp))
     | IsMutConstruct (cp,_) ->
-	Rmlterm (MLglob (ConstructRef cp)) (* TODO eta-expansion *)
+	let (_,s) = extract_constructor cp in
+	let n = 
+	  List.fold_left (fun n (v,_) -> if v = Vdefault then n+1 else n) 0 s 
+	in
+	Rmlterm (MLcons (ConstructRef cp,n,[]))
     | IsMutCase ((ni,(ip,cnames,_,_,_)),p,c,br) ->
 	let extract_branch j b =
 	  let (_,s) = extract_constructor (ip,succ j) in
@@ -441,8 +454,9 @@ and extract_term_with_type env ctx c t =
 	  let (binders,e) = decompose_lam_eta ni.(j) env b in
 	  let binders = List.rev binders in
 	  let (env',ctx') = push_many_rels_ctx env ctx binders in
-	  (* Some patological cases need an extract_constr here 
-	     rather than an extract_term. See exemples in test_extraction.v *)
+	  (* Some patological cases need an [extract_constr] here 
+	     rather than an [extract_term]. See exemples in 
+	     [test_extraction.v] *)
 	  let e' = match extract_constr env' ctx' e with
 	    | Eprop -> MLprop
 	    | Emltype _ -> MLarity
@@ -456,10 +470,10 @@ and extract_term_with_type env ctx c t =
 	  in
 	  (cnames.(j), ids, e')
 	in
-	(* c has an  inductive type, not an arity type *)
+	(* [c] has an  inductive type, not an arity type *)
 	(match extract_term env ctx c with
 	   | Rmlterm a -> Rmlterm (MLcase (a, Array.mapi extract_branch br))
-	   | Rprop -> (* Singlaton elimination *)
+	   | Rprop -> (* Singleton elimination *)
 	       assert (Array.length br = 1);
 	       let (c,ids,e) = extract_branch 0 br.(0) in 	  
 	       Rmlterm e)
@@ -472,7 +486,7 @@ and extract_term_with_type env ctx c t =
 	    | Emlterm a -> a
 	in
 	let ei = array_map_to_list extract_fix_body ci in
-	Rmlterm (MLfix (i, true, List.map id_of_name fi, ei))
+	Rmlterm (MLfix (i, List.map id_of_name fi, ei))
     | IsLetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
 	let env' = push_rel (n,Some c1,t1) env in
@@ -622,7 +636,15 @@ let extract_declaration = function
 
 (*s Registration of vernac commands for extraction. *)
 
-module Pp = Ocaml.Make(struct let pp_global = Printer.pr_global end)
+module ToplevelParams = struct
+  let pp_type_global = Printer.pr_global
+  let pp_global = Printer.pr_global
+end
+
+module Pp = Ocaml.Make(ToplevelParams)
+
+let pp_ast a = Pp.pp_ast (uncurrify_ast a)
+let pp_decl d = Pp.pp_decl (uncurrify_decl d)
 
 open Vernacinterp
 
@@ -635,16 +657,16 @@ let _ =
 	      match kind_of_term c with
 		(* If it is a global reference, then output the declaration *)
 		| IsConst (sp,_) -> 
-		    mSGNL (Pp.pp_decl (extract_declaration (ConstRef sp)))
+		    mSGNL (pp_decl (extract_declaration (ConstRef sp)))
 		| IsMutInd (ind,_) ->
-		    mSGNL (Pp.pp_decl (extract_declaration (IndRef ind)))
+		    mSGNL (pp_decl (extract_declaration (IndRef ind)))
 		| IsMutConstruct (cs,_) ->
-		    mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs)))
+		    mSGNL (pp_decl (extract_declaration (ConstructRef cs)))
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
 		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
-		      | Emlterm a -> mSGNL (Pp.pp_ast a)
+		      | Emlterm a -> mSGNL (pp_ast a)
 		      | Eprop -> message "prop")
        | _ -> assert false)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 95b81fe108..66993d4885 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -14,14 +14,10 @@ open Term
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
-(*s Identifiers of type are either parameters or type names. *)
-
-type ml_typeid = identifier
-
 (*s ML type expressions. *)
 
 type ml_type = 
-  | Tvar  of ml_typeid
+  | Tvar  of identifier
   | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
   | Tglob of global_reference
@@ -40,9 +36,9 @@ type ml_ast =
   | MLlam   of identifier * ml_ast
   | MLletin of identifier * ml_ast * ml_ast
   | MLglob  of global_reference
-  | MLcons  of int * identifier * ml_ast list
+  | MLcons  of global_reference * int * ml_ast list
   | MLcase  of ml_ast * (identifier * identifier list * ml_ast) array
-  | MLfix   of int * bool * (identifier list) * (ml_ast list)
+  | MLfix   of int * (identifier list) * (ml_ast list)
   | MLexn   of identifier
   | MLprop
   | MLarity
@@ -62,6 +58,7 @@ type ml_decl =
     functions to print types, terms and declarations. *)
 
 module type Mlpp_param = sig
+  val pp_type_global : global_reference -> std_ppcmds
   val pp_global : global_reference -> std_ppcmds
 end
 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 33c1e32bfe..9d66a820ce 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -15,9 +15,92 @@ let rec occurs k = function
       (List.exists (fun (k',t') -> occurs (k+k') t')
       	 (array_map_to_list (fun (_,l,t') -> 
       	       	           let k' = List.length l in (k',t')) pv))
-  | MLfix(_,_,l,cl)  -> let k' = List.length l in occurs_list (k+k') cl
+  | MLfix(_,l,cl)  -> let k' = List.length l in occurs_list (k+k') cl
   | _                -> false
 
 and occurs_list k l =
   List.exists (fun t -> occurs k t) l
 
+(* map over ML asts *)
+
+let rec ast_map f = function
+  | MLapp (a,al) -> MLapp (f a, List.map f al)
+  | MLlam (id,a) -> MLlam (id, f a)
+  | MLletin (id,a,b) -> MLletin (id, f a, f b)
+  | MLcons (c,n,al)  -> MLcons (c, n, List.map f al)
+  | MLcase (a,eqv) -> (MLcase (f a, Array.map (ast_map_eqn f) eqv))
+  | MLfix (fi,ids,al) -> MLfix (fi, ids, List.map f al)
+  | MLcast (a,t) -> MLcast (f a, t)
+  | MLmagic a -> MLmagic (f a)
+  | a -> a
+
+and ast_map_eqn f (c,ids,a) = (c,ids,f a)
+
+(*s Lifting on terms [ml_lift : int -> ml_ast -> ml_ast]
+    [ml_lift k M] lifts the binding depth of [M] across [k] bindings. *)
+
+let ml_liftn k n c = 
+  let rec liftrec n = function
+    | MLrel i as c -> if i < n then c else MLrel (i+k)
+    | MLlam (id,t) -> MLlam (id, liftrec (n+1) t)
+    | MLletin (id,a,b) -> MLletin (id, liftrec n a, liftrec (n+1) b)
+    | MLcase(t,pl) -> 
+	MLcase (liftrec n t,
+      	       	Array.map (fun (id,idl,p) -> 
+			     let k = List.length idl in
+			     (id, idl, liftrec (n+k) p)) pl)
+    | MLfix (n0,idl,pl) -> 
+	MLfix (n0,idl,
+	       let k = List.length idl in List.map (liftrec (n+k)) pl)
+    | a -> ast_map (liftrec n) a
+  in 
+  if k = 0 then c else liftrec n c
+
+let ml_lift k c = ml_liftn k 1 c
+
+let pop c = ml_lift (-1) c
+
+(*s [uncurrify] uncurrifies the applications of constructors *)
+
+let rec is_constructor_app = function
+  | MLcons _ -> true
+  | MLapp (a,_) -> is_constructor_app a
+  | _ -> false
+
+let rec decomp_app = function
+  | MLapp (f,args) -> 
+      let (c,n,args') = decomp_app f in (c, n, args' @ args)
+  | MLcons (c,n,args) ->
+      (c,n,args)
+  | _ ->
+      assert false
+
+let anonymous = Names.id_of_string "x"
+
+let rec n_lam n a =
+  if n = 0 then a else MLlam (anonymous, n_lam (pred n) a)
+
+let eta_expanse c n args =
+  let dif = n - List.length args in
+  assert (dif >= 0);
+  if dif > 0 then
+    let rels = List.rev_map (fun n -> MLrel n) (interval 1 dif) in
+    n_lam dif (MLcons (c, n, (List.map (ml_lift dif) args) @ rels))
+  else
+    MLcons (c,n,args)
+
+let rec uncurrify_ast a = match a with
+  | MLapp (f,_) when is_constructor_app f -> 
+      let (c,n,args) = decomp_app a in
+      let args' = List.map uncurrify_ast args in
+      eta_expanse c n args'
+  | MLcons (c,n,args) ->
+      let args' = List.map uncurrify_ast args in
+      eta_expanse c n args'
+  | _ -> 
+      ast_map uncurrify_ast a
+
+let uncurrify_decl = function
+ | Dglob (id, a) -> Dglob (id, uncurrify_ast a)
+ | d -> d
+
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 224236fecf..16cb332262 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -2,3 +2,8 @@
 open Miniml
 
 val occurs : int -> ml_ast -> bool
+
+val ml_lift : int -> ml_ast -> ml_ast
+
+val uncurrify_ast : ml_ast -> ml_ast
+val uncurrify_decl : ml_decl -> ml_decl
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index cae4a873e0..e7d77904c7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -20,12 +20,12 @@ open Miniml
 
 let string s = [< 'sTR s >]
 
-let open_par = function true -> string "(" | false -> [<>]
+let open_par = function true -> string "(" | false -> [< >]
 
-let close_par = function true -> string ")" | false -> [<>]
+let close_par = function true -> string ")" | false -> [< >]
 
 let rec collapse_type_app = function
-  | (Tapp l1) :: l2 -> collapse_type_app (l1@l2)
+  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
   | l -> l
 
 let pp_tuple f = function
@@ -42,7 +42,7 @@ let pp_boxed_tuple f = function
       	    hOV 0 [< prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
 		     'sTR ")" >] >]
 
-let space_if = function true -> [< 'sPC >] | false -> [<>]
+let space_if = function true -> [< 'sPC >] | false -> [< >]
 
 (* collect_lambda MLlam(id1,...MLlam(idn,t)...) = [id1;...;idn],t *)
 
@@ -87,10 +87,10 @@ let pp_type t =
 	   | t::l -> [< open_par par; pp_tuple (pp_rec false) l; 
 			space_if (l <>[]); pp_rec false t; close_par par >])
     | Tarr (t1,t2) ->
-	[< open_par par; pp_rec true t1; 'sPC; 'sTR"->"; 'sPC; 
+	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
 	   pp_rec false t2; close_par par >]
     | Tglob r -> 
-	P.pp_global r
+	P.pp_type_global r
     | Tprop ->
 	string "prop"
     | Tarity ->
@@ -107,7 +107,7 @@ let rec pp_expr par env args =
   let apply st = match args with
     | [] -> st
     | _  -> hOV 2 [< open_par par; st; 'sPC;
-                     prlist_with_sep (fun () -> [<'sPC>]) (fun s -> s) args;
+                     prlist_with_sep (fun () -> [< 'sPC >]) (fun s -> s) args;
                      close_par par >] 
   in
   function
@@ -119,7 +119,7 @@ let rec pp_expr par env args =
     | MLlam _ as a -> 
       	let fl,a' = collect_lambda a in
 	let fl = rename_bvars env fl in
-	let st = [< abst (List.rev fl); pp_expr false (fl@env) [] a' >] in
+	let st = [< abst (List.rev fl); pp_expr false (fl @ env) [] a' >] in
 	if args = [] then
           [< open_par par; st; close_par par >]
         else
@@ -129,25 +129,25 @@ let rec pp_expr par env args =
 	hOV 0 [< hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC;
 			  pp_expr false env [] a1; 'sPC; 'sTR "in" >];
 		 'sPC;
-		 pp_expr false (id'@env) [] a2 >] 
+		 pp_expr false (id' @ env) [] a2 >] 
     | MLglob r -> 
 	apply (P.pp_global r)
-    | MLcons (_,id,[]) ->
-	pr_id id
-    | MLcons (_,id,[a]) ->
-	[< open_par par; pr_id id; 'sPC; pp_expr true env [] a;
-	   pp_expr true env [] a ; close_par par >]
-    | MLcons (_,id,args') ->
-	[< open_par par; pr_id id; 'sPC;
+    | MLcons (r,_,[]) ->
+	P.pp_global r
+    | MLcons (r,_,[a]) ->
+	[< open_par par; P.pp_global r; 'sPC;
+	   pp_expr true env [] a; close_par par >]
+    | MLcons (r,_,args') ->
+	[< open_par par; P.pp_global r; 'sPC;
 	   pp_tuple (pp_expr true env []) args'; close_par par >]
     | MLcase (t, pv) ->
       	apply
-      	  [< if args<>[] then [< 'sTR"(" >]  else open_par par;
+      	  [< if args <> [] then [< 'sTR "(" >]  else open_par par;
       	     v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with";
-		    'fNL; 'sTR "  "; pp_pat env pv >] ;
-	     if args<>[] then [< 'sTR")" >] else close_par par >]
-    | MLfix (i,b,idl,al) ->
-      	pp_fix par env (i,b,idl,al) args
+		    'fNL; 'sTR "  "; pp_pat env pv >];
+	     if args <> [] then [< 'sTR ")" >] else close_par par >]
+    | MLfix (i,idl,al) ->
+      	pp_fix par env true (i,idl,al) args
     | MLexn id -> 
 	[< open_par par; 'sTR "failwith"; 'sPC; 
 	   'qS (string_of_id id); close_par par >]
@@ -170,24 +170,19 @@ and pp_pat env pv =
       | MLcase _ -> true
       | _        -> false 
     in
-    hOV 2 [< 'sTR(string_of_id name) ;
+    hOV 2 [< pr_id name;
 	     begin match ids with 
-		 [] -> [< >]
-	       | _  -> 
-      		   [< 'sTR " ";
-		      pp_boxed_tuple
-			(fun id -> [< 'sTR(string_of_id id) >]) 
-			(List.rev ids) >]
-	     end ;
-	     'sTR" ->" ; 'sPC ; pp_expr par (ids@env) [] t
-          >]
+	       | [] -> [< >]
+	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id ids >]
+	     end;
+	     'sTR " ->"; 'sPC; pp_expr par (List.rev ids @ env) [] t >]
   in 
-  [< prvect_with_sep (fun () -> [< 'fNL ; 'sTR"| " >]) pp_one_pat pv >]
+  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
 
-and pp_fix par env (j,in_p,fid,bl) args =
+and pp_fix par env in_p (j,fid,bl) args =
   let env' = (List.rev fid) @ env in
   [< open_par par; 
-     v 0 [< 'sTR"let rec " ;
+     v 0 [< 'sTR "let rec " ;
 	    prlist_with_sep
       	      (fun () -> [< 'fNL; 'sTR "and " >])
 	      (fun (fi,ti) -> pp_function env' fi ti)
@@ -214,18 +209,18 @@ and pp_function env f t =
   match t' with 
     | MLcase(MLrel 1,pv) ->
 	if is_function pv then
-	  [< 'sTR(string_of_id f) ; pr_binding (List.rev (List.tl bl)) ;
-       	     'sTR" = function" ; 'fNL ;
-	     v 0 [< 'sTR"  " ; pp_pat (bl@env) pv >] >]
+	  [< pr_id f; pr_binding (List.rev (List.tl bl)) ;
+       	     'sTR " = function"; 'fNL;
+	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
 	else
-          [< 'sTR(string_of_id f) ; pr_binding (List.rev bl) ; 
-             'sTR" = match " ;
-	     'sTR(string_of_id (List.hd bl)) ; 'sTR" with" ; 'fNL ;
-	     v 0 [< 'sTR"  " ; pp_pat (bl@env) pv >] >]
+          [< pr_id f; pr_binding (List.rev bl); 
+             'sTR " = match ";
+	     pr_id (List.hd bl); 'sTR " with"; 'fNL;
+	     v 0 [< 'sTR "  "; pp_pat (bl @ env) pv >] >]
 	  
-    | _ -> [< 'sTR(string_of_id f) ; pr_binding (List.rev bl) ;
-	      'sTR" =" ; 'fNL ; 'sTR"  " ;
-	      hOV 2 (pp_expr false (bl@env) [] t') >]
+    | _ -> [< pr_id f; pr_binding (List.rev bl);
+	      'sTR " ="; 'fNL; 'sTR "  ";
+	      hOV 2 (pp_expr false (bl @ env) [] t') >]
 	
 let pp_ast a = hOV 0 (pp_expr false [] [] a)
 
@@ -244,8 +239,8 @@ let pp_one_inductive (pl,name,cl) =
 		      (fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >] 
   in
   [< pp_parameters pl; pr_id name; 'sTR " ="; 'fNL; 
-     v 0 [< 'sTR "    " ;
-	    prlist_with_sep (fun () -> [< 'fNL ; 'sTR "  | ">])
+     v 0 [< 'sTR "    ";
+	    prlist_with_sep (fun () -> [< 'fNL; 'sTR "  | " >])
                             (fun c -> hOV 2 (pp_constructor c)) cl >] >]
 
 let pp_inductive il =
@@ -262,15 +257,29 @@ let pp_decl = function
   | Dabbrev (id, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
 	       pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >]
-  | Dglob (id, MLfix (n,_,idl,l)) ->
+  | Dglob (id, MLfix (n,idl,l)) ->
       let id' = List.nth idl n in
       if id = id' then
-	[<  hOV 2 (pp_fix false [] (n,false,idl,l) []) >]
+	[<  hOV 2 (pp_fix false [] false (n,idl,l) []) >]
       else
 	[< 'sTR "let "; pr_id id; 'sTR " ="; 'fNL;
 	   v 0 [< 'sTR "  "; 
-		  hOV 2 (pp_fix false [] (n,true,idl,l) []); 'fNL >] >]
+		  hOV 2 (pp_fix false [] true (n,idl,l) []); 'fNL >] >]
   | Dglob (id, a) ->
       hOV 0 [< 'sTR "let "; pp_function [] id a >]
 
 end
+
+(*s Renaming issues. *)
+
+module OcamlParams = struct
+
+let pp_type_global r = failwith "todo" 
+
+let pp_global r = failwith "todo"
+
+end
+
+(*s The ocaml pretty-printing module. *)
+
+module Pp = Make(OcamlParams)
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index ff8dce97fe..6a2834bb7d 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -8,9 +8,13 @@
 
 (*i $Id$ i*)
 
-(*s Production of Ocaml syntax. *)
+(*s Production of Ocaml syntax. We export both a functor to be used for 
+    extraction in the Coq toplevel and a module [Pp] to be used for
+    production of Ocaml files. *)
 
 open Miniml
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
+module Pp : Mlpp
+
diff --git a/contrib/extraction/rename.mli b/contrib/extraction/rename.mli
new file mode 100644
index 0000000000..9ed0c475ca
--- /dev/null
+++ b/contrib/extraction/rename.mli
@@ -0,0 +1,21 @@
+
+(* Renaming issues. *)
+
+open Names
+open Term
+open Miniml
+
+type renaming_function = Idset.t -> name -> identifier
+
+module type Renaming = sig
+  val rename_type_parameter : renaming_function
+  val rename_type : renaming_function
+  val rename_term : renaming_function
+  val rename_global_type : renaming_function
+  val rename_global_constructor : renaming_function
+  val rename_global_term : renaming_function
+end
+
+module Make : functor(R : Renaming) -> sig
+
+end
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 451ffafeff..89064abb7f 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -92,4 +92,15 @@ Extraction sumbool_rec.
 
 Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O.
 
-Extraction horibilis.
\ No newline at end of file
+Extraction horibilis.
+
+Inductive predicate : Type := 
+  | Atom : Prop -> predicate
+  | And  : predicate -> predicate -> predicate.
+
+Extraction predicate.
+
+(* eta-expansions *)
+Inductive t : Set := c : nat->nat->nat->nat->t.
+Extraction (c O).
+Extraction (c O (S O)).