Extract Inductive is now possible toward non-inductive types (e.g. nat => int)

 For instance:

  Extract Inductive nat => int [ "0" "succ" ]
   "(fun fO fS n => if n=0 then fO () else fS (n-1))".

 See Extraction.v for more details and caveat.

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

9 files changed, 120 insertions, 13 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 277e3d539..65ab1a0b9 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -255,13 +255,49 @@ types and constructors.  For instance, the user may want to use the ML
 native boolean type instead of \Coq\ one.  The syntax is the following:
 
 \begin{description}
-\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots \str\ ].} ~\par
+\item{\tt Extract Inductive \qualid\ => \str\ [ \str\ \dots \str\ ]\
+{\it optstring}.} ~\par
   Give an ML extraction for the given inductive type. You must specify
   extractions for the type itself (first \str) and all its
-  constructors (between square brackets). The ML extraction must be an
-  ML recursive datatype.
+  constructors (between square brackets). If given, the final optional
+  string should contain a function emulating pattern-matching over this
+  inductive type. If this optional string is not given, the ML
+  extraction must be an ML inductive datatype, and the native
+  pattern-matching of the language will be used.
 \end{description}
 
+For an inductive type with $k$ constructor, the function used to
+emulate the match should expect $(k+1)$ arguments, first the $k$
+branches in functional form, and then the inductive element to
+destruct. For instance, the match branch \verb$| S n => foo$ gives the
+functional form \verb$(fun n -> foo)$. Note that a constructor with no
+argument is considered to have one unit argument, in order to block
+early evaluation of the branch: \verb$| O => bar$ leads to the functional
+form \verb$(fun () -> bar)$. For instance, when extracting {\tt nat}
+into {\tt int}, the code to provide has type:
+{\tt (unit->'a)->(int->'a)->int->'a}.
+    
+As for {\tt Extract Inductive}, this command should be used with care:
+\begin{itemize}
+\item The ML code provided by the user is currently \emph{not} checked at all by
+  extraction, even for syntax errors.
+
+\item Extracting an inductive type to a pre-existing ML inductive type
+is quite sound. But extracting to a general type (by providing an
+ad-hoc pattern-matching) will often \emph{not} be fully rigorously
+correct.  For instance, when extracting {\tt nat} to Ocaml's {\tt
+int}, it is theoretically possible to build {\tt nat} values that are
+larger than Ocaml's {\tt max\_int}. It is the user's responsability to
+be sure that no overflow or other bad events occur in practice.
+
+\item Translating an inductive type to an ML type does \emph{not}
+magically improve the asymptotic complexity of functions, even if the
+ML type is an efficient representation. For instance, when extracting
+{\tt nat} to Ocaml's {\tt int}, the function {\tt mult} stays
+quadratic. It might be interesting to associate this translation with
+some specific {\tt Extract Constant} when primitive counterparts exist.
+\end{itemize}
+
 \Example
 Typical examples are the following:
 \begin{coq_example}
@@ -278,6 +314,13 @@ Extract Inductive list => "list" [ "[]" "(::)" ].
 Extract Inductive prod => "(*)"  [ "(,)" ].
 \end{coq_example}
 
+As an example of translation to a non-inductive datatype, let's turn
+{\tt nat} into Ocaml's {\tt int} (see caveat above):
+\begin{coq_example}
+Extract Inductive nat => int [ "0" "succ" ]
+ "(fun fO fS n => if n=0 then fO () else fS (n-1))".
+\end{coq_example}
+
 \asubsection{Avoiding conflicts with existing filenames}
 
 \comindex{Extraction Blacklist}
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index f8354f52e..b2256c471 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -124,6 +124,7 @@ VERNAC COMMAND EXTEND ExtractionInlinedConstant
 END
 
 VERNAC COMMAND EXTEND ExtractionInductive
-| [ "Extract" "Inductive" global(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
-  -> [ extract_inductive x (id,idl) ]
+| [ "Extract" "Inductive" global(x) "=>"
+    mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
+  -> [ extract_inductive x id idl o ]
 END
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 84202d539..c1ed62b34 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -146,6 +146,14 @@ let rec pp_expr par env args =
 	assert (args=[]);
 	pp_par par (pp_global Cons r ++ spc () ++
 		    prlist_with_sep spc (pp_expr true env []) args')
+    | MLcase (_,t, pv) when is_custom_match pv ->
+	let mkfun (_,ids,e) =
+	  if ids <> [] then named_lams (List.rev ids) e
+	  else dummy_lams (ast_lift 1 e) 1
+	in
+	hov 2 (str (find_custom_match pv) ++ fnl () ++
+		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
+	       ++ pp_expr true env [] t)
     | MLcase ((_,factors),t, pv) ->
       	apply (pp_par par'
 		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index e936d2dbf..a1e59e2a0 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -96,15 +96,16 @@ type ml_ident =
   | Id of identifier
   | Tmp of identifier
 
-type ml_ast =
+type ml_branch = global_reference * ml_ident list * ml_ast
+
+and ml_ast =
   | MLrel    of int
   | MLapp    of ml_ast * ml_ast list
   | MLlam    of ml_ident * ml_ast
   | MLletin  of ml_ident * ml_ast * ml_ast
   | MLglob   of global_reference
   | MLcons   of inductive_info * global_reference * ml_ast list
-  | MLcase   of (inductive_info*case_info) * ml_ast *
-      (global_reference * ml_ident list * ml_ast) array
+  | MLcase   of (inductive_info*case_info) * ml_ast * ml_branch array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 42787a540..7e9cfbeed 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -88,7 +88,7 @@ val collect_lams : ml_ast -> ml_ident list * ml_ast
 val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast
 val remove_n_lams : int -> ml_ast -> ml_ast
 val nb_lams : ml_ast -> int
-
+val named_lams : ml_ident list -> ml_ast -> ml_ast
 val dummy_lams : ml_ast -> int -> ml_ast
 val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3d980e65f..137ae9047 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -219,6 +219,14 @@ let rec pp_expr par env args =
 	if str_global Cons r = "" (* hack Extract Inductive prod *)
 	then tuple
 	else pp_par par (pp_global Cons r ++ spc () ++ tuple)
+    | MLcase (_, t, pv) when is_custom_match pv ->
+	let mkfun (_,ids,e) =
+	  if ids <> [] then named_lams (List.rev ids) e
+	  else dummy_lams (ast_lift 1 e) 1
+	in
+	hov 2 (str (find_custom_match pv) ++ fnl () ++
+		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
+	       ++ pp_expr true env [] t)
     | MLcase ((i,factors), t, pv) ->
 	let expr = if i = Coinductive then
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -328,7 +336,7 @@ and pp_function env t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
-    | MLcase(i,MLrel 1,pv) when fst i=Standard ->
+    | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) ->
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 6a44812da..f7a0b5a53 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -94,7 +94,15 @@ let rec pp_expr env args =
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
 	if i = Coinductive then paren (str "delay " ++ st) else st
-    | MLcase ((i,_),t, pv) ->
+    | MLcase (_,t,pv) when is_custom_match pv ->
+	let mkfun (_,ids,e) =
+	  if ids <> [] then named_lams (List.rev ids) e
+	  else dummy_lams (ast_lift 1 e) 1
+	in
+	hov 2 (str (find_custom_match pv) ++ fnl () ++
+		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
+	       ++ pp_expr env [] t)
+     | MLcase ((i,_),t, pv) ->
 	let e =
 	  if i <> Coinductive then pp_expr env [] t
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 8ac6545bb..df61375c5 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -646,6 +646,24 @@ let find_custom r = snd (Refmap.find r !customs)
 
 let find_type_custom r = Refmap.find r !customs
 
+let custom_matchs = ref Refmap.empty
+
+let add_custom_match r s =
+  custom_matchs := Refmap.add r s !custom_matchs
+
+let indref_of_match pv =
+  if Array.length pv = 0 then raise Not_found;
+  match pv.(0) with
+    | (ConstructRef (ip,_), _, _) -> IndRef ip
+    | _ -> raise Not_found
+
+let is_custom_match pv =
+  try Refmap.mem (indref_of_match pv) !custom_matchs
+  with Not_found -> false
+
+let find_custom_match pv =
+  Refmap.find (indref_of_match pv) !custom_matchs
+
 (* Registration of operations for rollback. *)
 
 let (in_customs,_) =
@@ -663,6 +681,20 @@ let _ = declare_summary "ML extractions"
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap.empty) }
 
+let (in_custom_matchs,_) =
+  declare_object
+    {(default_object "ML extractions custom matchs") with
+       cache_function = (fun (_,(r,s)) -> add_custom_match r s);
+       load_function = (fun _ (_,(r,s)) -> add_custom_match r s);
+       classify_function = (fun o -> Substitute o);
+       subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
+    }
+
+let _ = declare_summary "ML extractions custom match"
+	  { freeze_function = (fun () -> !custom_matchs);
+	    unfreeze_function = ((:=) custom_matchs);
+	    init_function = (fun () -> custom_matchs := Refmap.empty) }
+
 (* Grammar entries. *)
 
 let extract_constant_inline inline r ids s =
@@ -683,7 +715,7 @@ let extract_constant_inline inline r ids s =
     | _ -> error_constant g
 
 
-let extract_inductive r (s,l) =
+let extract_inductive r s l optstr =
   check_inside_section ();
   let g = Nametab.global r in
   match g with
@@ -693,6 +725,8 @@ let extract_inductive r (s,l) =
 	if n <> List.length l then error_nb_cons ();
 	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
+	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
+	  optstr;
 	list_iter_i
 	  (fun j s ->
 	     let g = ConstructRef (ip,succ j) in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index f02e73190..49108cf52 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -135,6 +135,9 @@ val is_inline_custom : global_reference -> bool
 val find_custom : global_reference -> string
 val find_type_custom : global_reference -> string list * string
 
+val is_custom_match : ml_branch array -> bool
+val find_custom_match : ml_branch array -> string
+
 (*s Extraction commands. *)
 
 val extraction_language : lang -> unit
@@ -143,7 +146,8 @@ val print_extraction_inline : unit -> unit
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
-val extract_inductive : reference -> string * string list -> unit
+val extract_inductive :
+  reference -> string -> string list -> string option -> unit
 val extraction_implicit : reference -> int list -> unit
 
 (*s Table of blacklisted filenames *)