extraction des types et des inductifs

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

6 files changed, 439 insertions, 101 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 74a7455f9..9e0f23c2d 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -1,2 +1,5 @@
 
-Declare ML Module "extraction.cmo".
+Declare ML Module "ocaml.cmo" "extraction.cmo".
+
+Grammar vernac vernac : ast :=
+  extr_constr [ "Extraction" constrarg($c) "." ] -> [(Extraction $c)].
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 616648143..aa7fadc67 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -8,6 +8,7 @@ open Term
 open Declarations
 open Environ
 open Reduction
+open Inductive
 open Instantiate
 open Miniml
 open Mlimport
@@ -26,102 +27,178 @@ type extraction_result =
   | Emltype of ml_type * signature * identifier list
   | Emlterm of ml_ast
 
+(*s Utility functions. *)
+
+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
+  fold 0
+
 let flexible_name = id_of_string "flex"
 
 let id_of_name = function
   | Anonymous -> id_of_string "_"
   | Name id   -> id
 
-(*s Extraction of a type. *)
+let params_of_sign = 
+  List.fold_left (fun l v -> match v with Vskip,_ -> l | _,id -> id :: l) []
 
-let rec extract_type c =
-  let genv = Global.env() in
-  let rec extract_rec env sign fl c args = match kind_of_term (whd_beta c) with
-    | IsProd (n, t, d) ->
-	assert (args = []);
-	let id = id_of_name n in (* FIXME: capture problem *)
+let signature_of_arity = 
+  let rec sign_of acc env c = match kind_of_term c with
+    | IsProd (n, t, c') ->
 	let env' = push_rel (n,None,t) env in
-	(match extract_rec env sign fl t [] with
-	   | Tarity ->
-	       extract_rec env' ((Varity,id) :: sign) fl d []
-	   | Tmltype (t', _, fl') ->
-	       (match extract_rec env' ((Vskip,id) :: sign) fl' d [] with
-		  | Tarity -> Tarity
-		  | Tmltype (d', sign', fl'') -> 
-		      Tmltype (Tarr (t', d'), sign', fl'')))
-    | IsSort (Prop Null) ->
-	assert (args = []);
-	Tmltype (Tprop, [], [])
-    | IsSort _ ->
-	assert (args = []);
-	Tarity
-    | IsApp (d, args') ->
-	extract_rec env sign fl d (Array.to_list args' @ args)
-    | IsRel n ->
-	(match List.nth sign (pred n) with
-	   | Vskip, id -> Tmltype (Tvar id, sign, id :: fl)
-	   | Varity, id -> Tmltype (Tvar id, sign, fl))
-    | IsConst (sp,a) ->
-	let cty = constant_type genv Evd.empty (sp,a) in
-	if is_arity genv Evd.empty cty then
-	  (match extract_constant sp with
-	     | Emltype (_, sc, flc) ->
-		 assert (List.length sc = List.length args);
-		 let (mlargs,fl') = 
-		   List.fold_left 
-		     (fun ((args,fl) as acc) (v,a) -> match v with
-			| Vskip,_ -> acc
-			| Varity,_ -> match extract_rec env sign fl a [] with
-			    | Tarity -> assert false
-			    | Tmltype (mla,_,fl') -> (mla :: args, fl')
-		     )
-		     ([],fl) (List.combine sc args)
-		 in
-		 let flc = List.map (fun i -> Tvar i) flc in
-		 Tmltype (Tapp ((Tglob (ConstRef sp)) :: mlargs @ flc), 
-			  sign, fl')
-	     | Emlterm _ -> 
-		 assert false)
-	else
-	  failwith "todo: expanse c, reduce and apply recursively"
-    | IsMutInd _ ->
-	failwith "todo"
-    | IsMutCase _ 
-    | IsFix _ ->
-	let id = next_ident_away flexible_name fl in
-	Tmltype (Tvar id, sign, id :: fl)
-    | IsCast (c, _) ->
-	extract_rec env sign fl c args
-    | _ -> 
+	let id = id_of_name n in
+	sign_of 
+	  (((if is_arity env Evd.empty t then Varity else Vskip), id) :: acc)
+	  env' c'
+    | IsSort _ -> 
+	acc
+    | _ ->
 	assert false
   in
-  extract_rec (Global.env()) [] [] c []
+  sign_of []
+
+(* [list_of_ml_arrows] applied to the ML type [a->b->...->z->t]
+   returns the list [[a;b;...:z]]. *)
+let rec list_of_ml_arrows = function
+  | Tarr (a, b) -> a :: list_of_ml_arrows b
+  | t -> []
+
+(*s Tables to keep the extraction of inductive types and constructors. *)
+
+type inductive_extraction_result = signature * identifier list
+
+let inductive_extraction_table = 
+  ref (Gmap.empty : (inductive_path, inductive_extraction_result) Gmap.t)
+
+let add_inductive_extraction i e = 
+  inductive_extraction_table := Gmap.add i e !inductive_extraction_table
+
+let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table
+
+type constructor_extraction_result = ml_type list * signature
+
+let constructor_extraction_table = 
+  ref (Gmap.empty : (constructor_path, constructor_extraction_result) Gmap.t)
+
+let add_constructor_extraction c e = 
+  constructor_extraction_table := Gmap.add c e !constructor_extraction_table
+
+let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table
+
+(*i FIXME
+let inductive_declaration_table =
+  ref (Gmap.empty : (section_path, ml_ind list) Gmap.t)
+
+let add_inductive_declaration sp d = 
+  inductive_declaration_table := Gmap.add
+i*)
+
+(*s Extraction of a type. *)
+
+let rec extract_type env c =
+  let genv = Global.env() in
+  let rec extract_rec env sign fl c args = 
+    let ty = Typing.type_of env Evd.empty c in
+    if is_Prop (whd_betadeltaiota env Evd.empty ty) then
+      Tmltype (Tprop, [], fl)
+    else
+      match kind_of_term (whd_betaiota c) with
+	| IsProd (n, t, d) ->
+	    assert (args = []);
+	    let id = id_of_name n in (* FIXME: capture problem *)
+	    let env' = push_rel (n,None,t) env in
+	    (match extract_rec env sign fl t [] with
+	       | Tarity ->
+		   extract_rec env' ((Varity,id) :: sign) fl d []
+	       | Tmltype (t', _, fl') ->
+		   (match extract_rec env' ((Vskip,id) :: sign) fl' d [] with
+		      | Tarity -> Tarity
+		      | Tmltype (d', sign', fl'') -> 
+			  Tmltype (Tarr (t', d'), sign', fl'')))
+	| IsLambda (n, t, d) ->
+	    assert (args = []);
+	    let id = id_of_name n in (* FIXME: capture problem *)
+	    let env' = push_rel (n,None,t) env in
+	    (match extract_rec env sign fl t [] with
+	       | Tarity ->
+		   extract_rec env' ((Varity,id) :: sign) fl d []
+	       | Tmltype (t', _, fl') ->
+		   extract_rec env' ((Vskip,id) :: sign) fl' d [])
+	| IsSort (Prop Null) ->
+	    assert (args = []);
+	    Tmltype (Tprop, [], [])
+	| IsSort _ ->
+	    assert (args = []);
+	    Tarity
+	| IsApp (d, args') ->
+	    extract_rec env sign fl d (Array.to_list args' @ args)
+	| IsRel n ->
+	    (match List.nth sign (pred n) with
+	       | Vskip, id -> Tmltype (Tvar id, sign, id :: fl)
+	       | Varity, id -> Tmltype (Tvar id, sign, fl))
+	| IsConst (sp,a) ->
+	    let cty = constant_type genv 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 sign fl (ConstRef sp,sc,flc) args
+		 | Emlterm _ -> assert false)
+	    else
+	      let cvalue = constant_value env (sp,a) in
+	      extract_rec env sign fl (mkApp (cvalue, Array.of_list args)) []
+	| IsMutInd (spi,_) ->
+	    let (si,fli) = extract_inductive spi in
+	    extract_type_app env sign fl (IndRef spi,si,fli) args
+	| IsMutCase _ 
+	| IsFix _ ->
+	    let id = next_ident_away flexible_name fl in
+	    Tmltype (Tvar id, sign, id :: fl)
+	| IsCast (c, _) ->
+	    extract_rec env sign fl c args
+	| _ -> 
+	    assert false
+  and extract_type_app env sign fl (r,sc,flc) args =
+    let nargs = List.length args in
+    assert (List.length sc >= nargs);
+    let (mlargs,fl') = 
+      List.fold_right 
+	(fun (v,a) ((args,fl) as acc) -> match v with
+	   | Vskip,_ -> acc
+	   | Varity,_ -> match extract_rec env sign fl a [] with
+	       | Tarity -> assert false
+	       | Tmltype (mla,_,fl') -> (mla :: args, fl'))
+	(List.combine (list_firstn nargs (List.rev sc)) args)
+	([],fl)
+    in
+    let flc = List.map (fun i -> Tvar i) flc in
+    Tmltype (Tapp ((Tglob r) :: mlargs @ flc), sign, fl')
+  in
+  extract_rec env [] [] c []
+
 
 (*s Extraction of a term. *)
 
 and extract_term c =
   failwith "todo"
-(*i
-  let rec extract_rec env c = match kind_of_term (whd_beta c) with
-    | _ -> 
-	failwith "todo"
-    | IsSort _ | IsXtra _ | IsVar _ | IsMeta _ ->
-	assert false 
-  in
-  extract_rec (Global.env()) c
-i*)
+    (*i
+      let rec extract_rec env c = match kind_of_term (whd_beta c) with
+      | _ -> 
+      failwith "todo"
+      | IsSort _ | IsXtra _ | IsVar _ | IsMeta _ ->
+      assert false 
+      in
+      extract_rec (Global.env()) c
+      i*)
 
 (*s Extraction of a constr. *)
 
 and extract_constr_with_type c t =
-  let redt = whd_betadeltaiota (Global.env()) Evd.empty t in
-  if isSort redt then begin
-    if is_Prop redt then
-      Emltype (Tprop, [], [])
-    else
-      match extract_type c with
-	| Tarity -> error "not an ML type"
-	| Tmltype (t, sign, fl) -> Emltype (t, sign, fl)
+  let genv = Global.env () in
+  if is_arity genv Evd.empty t then begin
+    match extract_type genv c with
+      | Tarity -> error "not an ML type"
+      | Tmltype (t, sign, fl) -> Emltype (t, sign, fl)
   end else 
     let t = extract_term c in
     Emlterm t
@@ -136,28 +213,102 @@ and extract_constant sp =
   let typ = cb.const_type in
   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. *)
 
-and extract_inductive sp =
-  let mib = Global.lookup_mind sp in
-  failwith "todo"
-  (* Dtype ... *)
+and extract_inductive ((sp,_) as i) =
+  extract_mib sp;
+  lookup_inductive_extraction i
+
+and extract_constructor (((sp,_),_) as c) =
+  extract_mib sp;
+  lookup_constructor_extraction c
+
+and extract_mib sp =
+  if not (Gmap.mem (sp,0) !inductive_extraction_table) then begin
+    let mib = Global.lookup_mind sp in
+    let genv = Global.env () in
+    (* first pass: we store inductive signatures together with empty flex. *)
+    Array.iteri
+      (fun i ib -> add_inductive_extraction (sp,i) 
+	   (signature_of_arity genv ib.mind_nf_arity, []))
+      mib.mind_packets;
+    (* second pass: we extract constructors arities and we accumulate
+       all flexible variables. *)
+    let fl = 
+      array_foldi
+	(fun i ib fl ->
+	   let mis = build_mis ((sp,i),[||]) mib in
+	   array_foldi
+	     (fun j _ fl -> 
+		let t = mis_constructor_type (succ j) mis in
+		match extract_type genv t with
+		  | Tarity -> assert false
+		  | Tmltype (mlt, s, f) -> 
+		      let l = list_of_ml_arrows mlt in
+		      add_constructor_extraction ((sp,i),succ j) (l,s);
+		      f @ fl)
+	     ib.mind_nf_lc fl)
+	mib.mind_packets []
+    in
+    (* third pass: we update the inductive flexible variables. *)
+    for i = 0 to mib.mind_ntypes - 1 do
+      let (s,_) = lookup_inductive_extraction (sp,i) in
+      add_inductive_extraction (sp,i) (s,fl)
+    done
+  end
 
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
-and extract_reference = function
-  | ConstRef sp -> extract_constant sp
-  | IndRef (sp,_) -> extract_inductive sp
-  | VarRef _ | ConstructRef _ -> assert false
+and extract_inductive_declaration sp =
+  extract_mib sp;
+  let mib = Global.lookup_mind sp in
+  let one_constructor ind j id = 
+    let (t,_) = lookup_constructor_extraction (ind,succ j) in (id, t)
+  in
+  let one_inductive i ip =
+    let (s,fl) = lookup_inductive_extraction (sp,i) in
+    (params_of_sign s @ fl, ip.mind_typename, 
+     Array.to_list (Array.mapi (one_constructor (sp,i)) ip.mind_consnames))
+  in
+  Dtype (Array.to_list (Array.mapi one_inductive mib.mind_packets))
 
 (*s ML declaration from a reference. *)
 
-let params_of_sign = 
-  List.fold_left (fun l v -> match v with Vskip,_ -> l | _,id -> id :: l) []
+let extract_declaration = function
+  | ConstRef sp -> 
+      let id = basename sp in (* FIXME *)
+      (match extract_constant sp with
+	 | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt)
+	 | Emlterm t -> Dglob (id, t))
+  | IndRef (sp,_) -> extract_inductive_declaration sp
+  | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
+  | VarRef _ -> assert false
+
+(*s Registration of vernac commands for extraction. *)
+
+module Pp = Ocaml.Make(struct let pp_global = Printer.pr_global end)
+
+open Vernacinterp
+
+let _ = 
+  vinterp_add "Extraction"
+    (function 
+       | [VARG_CONSTR ast] ->
+	   (fun () -> 
+	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
+	      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)))
+		| IsMutInd (ind,_) ->
+		    mSGNL (Pp.pp_decl (extract_declaration (IndRef ind)))
+		| IsMutConstruct (cs,_) ->
+		    mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs)))
+		(* Otherwise, output the ML type or expression *)
+		| _ ->
+		    match extract_constr c with
+		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
+		      | Emlterm a -> mSGNL (Pp.pp_ast a))
+       | _ -> assert false)
 
-let extract_declaration r = 
-  let id = basename (Global.sp_of_global r) in (* FIXME *)
-  match extract_reference r with
-    | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt)
-    | Emlterm t -> Dglob (id, t)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b42091289..3e6c9c275 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -19,8 +19,6 @@ type extraction_result =
 
 val extract_constr : constr -> extraction_result
 
-val extract_reference : global_reference -> extraction_result
-
 (*s ML declaration corresponding to a Coq reference. *)
 
 val extract_declaration : global_reference -> ml_decl
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 8493b308e..3d4c7e8f6 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -1,14 +1,17 @@
 
 (*i $Id$ i*)
 
+open Pp
 open Names
 open Term
 
-(* identifiers of type are either parameters or type names. *)
+(*s Target language for extraction: a core ML called MiniML. *)
+
+(*s Identifiers of type are either parameters or type names. *)
 
 type ml_typeid = identifier
 
-(* ML type expressions. *)
+(*s ML type expressions. *)
 
 type ml_type = 
   | Tvar  of ml_typeid
@@ -17,11 +20,11 @@ type ml_type =
   | Tglob of global_reference
   | Tprop
       
-(* ML inductive types. *)
+(*s ML inductive types. *)
 
 type ml_ind = identifier list * identifier * (identifier * ml_type list) list
 
-(* ML terms. *)
+(*s ML terms. *)
 
 type ml_ast = 
   | MLrel   of int
@@ -35,10 +38,25 @@ type ml_ast =
   | MLcast  of ml_ast * ml_type
   | MLmagic of ml_ast
 
-(* ML declarations. *)
+(*s ML declarations. *)
 
 type ml_decl = 
   | Dtype   of ml_ind list
   | Dabbrev of identifier * (identifier list) * ml_type
   | Dglob   of identifier * ml_ast
 
+(*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 pp_global : global_reference -> std_ppcmds
+end
+
+module type Mlpp = sig
+  val pp_type : ml_type -> std_ppcmds
+  val pp_ast : ml_ast -> std_ppcmds
+  val pp_decl : ml_decl -> std_ppcmds
+end
+
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
new file mode 100644
index 000000000..b3e2557ae
--- /dev/null
+++ b/contrib/extraction/ocaml.ml
@@ -0,0 +1,159 @@
+
+(*i $Id$ i*)
+
+(*s Production of Ocaml syntax. *)
+
+open Pp
+open Util
+open Names
+open Term
+open Miniml
+
+(*s Some utility functions. *)
+
+let string s = [< 'sTR s >]
+
+let open_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)
+  | l -> l
+
+let pp_tuple f = function
+  | [] -> [< >]
+  | [x] -> f x
+  | l -> [< 'sTR "(";
+      	    prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
+	    'sTR ")" >]
+
+let space_if = function true -> [< 'sPC >] | false -> [<>]
+
+(*s The pretty-printing functor. *)
+
+module Make = functor(P : Mlpp_param) -> struct
+
+(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
+    are needed or not. *)
+
+let pp_type t =
+  let rec pp_rec par = function
+    | Tvar id -> 
+	string ("'" ^ string_of_id id)
+    | Tapp l ->
+	(match collapse_type_app l with
+	   | [] -> assert false
+	   | [t] -> pp_rec par 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; 
+	   pp_rec false t2; close_par par >]
+    | Tglob r -> 
+	P.pp_global r
+    | Tprop ->
+	string "prop"
+  in 
+  hOV 0 (pp_rec false t)
+
+(*s Pretty-printing of expressions. [par] indicates whether
+    parentheses are needed or not. [env] is the list of names for the
+    de Bruijn variables. [args] is the list of collected arguments
+    (already pretty-printed). *)
+
+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;
+                     close_par par >] 
+  in
+  function
+    | MLrel n -> 
+	apply (pr_id (List.nth env (pred n)))
+    | MLapp (f,args') ->
+	let stl = List.map (pp_expr true env []) args' in
+        pp_expr par env (stl @ args) f
+    | MLlam (id,a) -> 
+	failwith "todo"
+	(*i
+      	let fl,a' = collect_lambda a in
+	let fl = rename_bvars env fl in
+	let st = [< abst (List.rev fl) ; pp_rec false (fl@env) [] a' >] in
+	if args = [] then
+          [< open_par par; st; close_par par >]
+        else
+          apply [< 'sTR "("; st; 'sTR ")" >]
+        i*)
+    | 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;
+	   pp_tuple (pp_expr true env []) args'; close_par par >]
+    | MLcase (t, pv) ->
+      	apply
+      	  [< 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
+    | MLexn id -> 
+	[< open_par par; 'sTR "failwith"; 'sPC; 
+	   'qS (string_of_id id); close_par par >]
+    | MLcast (a,t) ->
+	[< open_par true; pp_expr false env args a; 'sPC; 'sTR ":"; 'sPC; 
+	   pp_type t; close_par true >]
+    | MLmagic a ->
+	[< open_par true; 'sTR "Obj.magic"; 'sPC; 
+	   pp_expr false env args a; close_par true >]
+
+and pp_pat env pv = failwith "todo"
+
+and pp_fix par env f args = failwith "todo"
+
+let pp_ast = pp_expr false [] []
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let pp_parameters l = 
+  [< pp_tuple (fun id -> string ("'" ^ string_of_id id)) l; space_if (l<>[]) >]
+
+let pp_one_inductive (pl,name,cl) =
+  let pp_constructor (id,l) =
+    [< pr_id id;
+       match l with
+         | [] -> [< >] 
+	 | _  -> [< 'sTR " of " ;
+      	       	    prlist_with_sep 
+		      (fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >] 
+  in
+  [< pp_parameters pl; pr_id name; 'sTR " ="; 'fNL; 
+     v 0 [< 'sTR "    " ;
+	    prlist_with_sep (fun () -> [< 'fNL ; 'sTR "  | ">])
+                            (fun c -> hOV 2 (pp_constructor c)) cl >] >]
+
+let pp_inductive il =
+  [< 'sTR "type " ;
+     prlist_with_sep 
+       (fun () -> [< 'fNL ; 'sTR "and " >])
+       (fun i -> pp_one_inductive i)
+       il;
+     'fNL >]
+
+let pp_decl = function
+  | Dtype i -> 
+      hOV 0 (pp_inductive i)
+  | Dabbrev (id, l, t) ->
+      hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
+	       pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >]
+  | Dglob (id, a) ->
+      hOV 0 [< 'sTR "let"; 'sPC; pr_id id; 'sPC; 'sTR "="; 'sPC; pp_ast a >]
+
+end
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
new file mode 100644
index 000000000..be80e419a
--- /dev/null
+++ b/contrib/extraction/ocaml.mli
@@ -0,0 +1,9 @@
+
+(*i $Id$ i*)
+
+(*s Production of Ocaml syntax. *)
+
+open Miniml
+
+module Make : functor(P : Mlpp_param) -> Mlpp
+