extraction vers scheme

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

8 files changed, 280 insertions, 75 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index b6eae0a1da..149db49540 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -187,8 +187,11 @@ module OcamlModularPp = Ocaml.Make(ModularParams)
 module HaskellMonoPp = Haskell.Make(MonoParams)
 module HaskellModularPp = Haskell.Make(ModularParams)
 
+module SchemeMonoPp = Scheme.Make(MonoParams)
+
 let pp_comment s = match lang () with 
   | Haskell -> str "-- " ++ s ++ fnl () 
+  | Scheme -> str ";" ++ s ++ fnl () 
   | Ocaml | Toplevel -> str "(* " ++ s ++ str " *)" ++ fnl ()
 
 let pp_logical_ind r = 
@@ -204,6 +207,9 @@ let set_globals () = match lang () with
   | Haskell -> 
       keywords := Haskell.keywords;
       global_ids := Haskell.keywords
+  | Scheme -> 
+      keywords := Scheme.keywords;
+      global_ids := Scheme.keywords
   | _ -> ()
 
 (*s Extraction to a file. *)
@@ -213,6 +219,7 @@ let extract_to_file f prm decls =
   let preamble = match lang () with 
     | Ocaml -> Ocaml.preamble    
     | Haskell -> Haskell.preamble
+    | Scheme -> Scheme.preamble
     | _ -> assert false 
   in 
   let pp_decl = match lang (),prm.modular with 
@@ -220,6 +227,7 @@ let extract_to_file f prm decls =
     | Ocaml, _ -> OcamlModularPp.pp_decl
     | Haskell, false -> HaskellMonoPp.pp_decl    
     | Haskell, _ -> HaskellModularPp.pp_decl
+    | Scheme, _ -> SchemeMonoPp.pp_decl
     | _ -> assert false 
   in
   let used_modules = if prm.modular then 
@@ -227,7 +235,7 @@ let extract_to_file f prm decls =
   else Idset.empty
   in 
   let print_dummy = match lang() with 
-    | Ocaml -> decl_search MLdummy' decls
+    | Ocaml | Scheme -> decl_search MLdummy' decls
     | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls)
     | _ -> assert false 
   in 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 0076b99e05..6f825c9b25 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -17,6 +17,7 @@ open Nametab
 module ToplevelPp : Mlpp
 module OcamlMonoPp : Mlpp
 module HaskellMonoPp : Mlpp
+module SchemeMonoPp:Mlpp
 
 val is_long_module : dir_path -> global_reference -> bool
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index db2e7d4f93..cf595e8df6 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -212,35 +212,37 @@ let decl_in_r r0 = function
 let pp_decl d = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_decl d
   | Haskell -> HaskellMonoPp.pp_decl d
+  | Scheme -> SchemeMonoPp.pp_decl d
   | Toplevel -> ToplevelPp.pp_decl d
 
 let pp_ast a = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_ast a
   | Haskell -> HaskellMonoPp.pp_ast a
+  | Scheme -> SchemeMonoPp.pp_ast a
   | Toplevel -> ToplevelPp.pp_ast a
 
 let pp_type t = match lang () with 
   | Ocaml -> OcamlMonoPp.pp_type t
   | Haskell -> HaskellMonoPp.pp_type t
+  | Scheme -> SchemeMonoPp.pp_type t
   | Toplevel -> ToplevelPp.pp_type t
 
 let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
+  else if decl_is_logical_ind r then 
+    msgnl (pp_logical_ind r) 
+  else if decl_is_singleton r then 
+    msgnl (pp_singleton_ind r) 
   else
-    if decl_is_logical_ind r then 
-      msgnl (pp_logical_ind r) 
-    else if decl_is_singleton r then 
-      msgnl (pp_singleton_ind r) 
-    else
-      let prm = 
-	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
-      let decls = optimize prm (decl_of_refs [r]) in 
-      let d = list_last decls in
-      let d = if (decl_in_r r d) then d 
-      else List.find (decl_in_r r) decls
-      in msgnl (pp_decl d)
-
+    let prm = 
+      { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
+    let decls = optimize prm (decl_of_refs [r]) in 
+    let d = list_last decls in
+    let d = if (decl_in_r r d) then d 
+    else List.find (decl_in_r r) decls
+    in msgnl (pp_decl d)
+	 
 let extraction rawconstr =
   set_globals ();
   let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in
@@ -276,6 +278,7 @@ let extraction_rec = mono_extraction (None,id_of_string "Main")
 let lang_suffix () = match lang () with 
   | Ocaml -> ".ml"
   | Haskell -> ".hs"
+  | Scheme -> ".scm"
   | Toplevel -> assert false
 
 let filename f = 
@@ -284,14 +287,14 @@ let filename f =
     Some f,id_of_string (Filename.chop_suffix f s) 
   else Some (f^s),id_of_string f
 
-let lang_error () = 
-  errorlabstrm "extraction_language"
+let toplevel_error () = 
+  errorlabstrm "toplevel_extraction_language"
     (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." 
      ++ fnl () ++
      str "You should use Extraction Language Ocaml or Haskell before.") 
 
 let extraction_file f vl =
-  if lang () = Toplevel then lang_error () 
+  if lang () = Toplevel then toplevel_error () 
   else mono_extraction (filename f) vl
 
 (*s Extraction of a module. The vernacular command is 
@@ -308,39 +311,46 @@ let decl_in_m m = function
 let module_file_name m = match lang () with 
   | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
   | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
-  | Toplevel -> assert false
+  | _ -> assert false
 
-let extraction_module m =
-  if lang () = Toplevel then lang_error () 
-  else 
-    let dir_m = module_of_id m in 
-    let f = module_file_name m in
-    let prm = {modular=true; mod_name=m; to_appear=[]} in 
-    let rl = extract_module dir_m in 
-    let decls = optimize prm (decl_of_refs rl) in
-    let decls = add_ml_decls prm decls in 
-    check_one_module dir_m decls; 
-    let decls = List.filter (decl_in_m dir_m) decls in
-    extract_to_file (Some f) prm decls
+let scheme_error () = 
+  errorlabstrm "scheme_extraction_language"
+    (str "No Scheme modular extraction available yet." ++ fnl ())
 
+let extraction_module m =
+  match lang () with 
+    | Toplevel -> toplevel_error ()
+    | Scheme -> scheme_error ()
+    | _ -> 
+	let dir_m = module_of_id m in 
+	let f = module_file_name m in
+	let prm = {modular=true; mod_name=m; to_appear=[]} in 
+	let rl = extract_module dir_m in 
+	let decls = optimize prm (decl_of_refs rl) in
+	let decls = add_ml_decls prm decls in 
+	check_one_module dir_m decls; 
+	let decls = List.filter (decl_in_m dir_m) decls in
+	extract_to_file (Some f) prm decls
+	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
 let recursive_extraction_module m =
-  if lang () = Toplevel then lang_error () 
-  else 
-    let dir_m = module_of_id m in 
-    let modules,refs = 
-      modules_extract_env dir_m in
-    check_modules modules; 
-    let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-    let decls = optimize dummy_prm (decl_of_refs refs) in
-    let decls = add_ml_decls dummy_prm decls in
-    Dirset.iter 
-      (fun m ->
-	let short_m = snd (split_dirpath m) in
-	let f = module_file_name short_m in 
-	let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
-	let decls = List.filter (decl_in_m m) decls in
-	if decls <> [] then extract_to_file (Some f) prm decls)
-      modules
+  match lang () with 
+    | Toplevel -> toplevel_error () 
+    | Scheme -> scheme_error () 
+    | _ -> 
+	let dir_m = module_of_id m in 
+	let modules,refs = modules_extract_env dir_m in
+	check_modules modules; 
+	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+	let decls = optimize dummy_prm (decl_of_refs refs) in
+	let decls = add_ml_decls dummy_prm decls in
+	Dirset.iter 
+	  (fun m ->
+	     let short_m = snd (split_dirpath m) in
+	     let f = module_file_name short_m in 
+	     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
+	     let decls = List.filter (decl_in_m m) decls in
+	     if decls <> [] then extract_to_file (Some f) prm decls)
+	  modules
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 84f0f663b9..40f7c0fa69 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -26,6 +26,7 @@ open Extract_env
 VERNAC ARGUMENT EXTEND language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
+| [ "Scheme" ] -> [ Scheme ]
 | [ "Toplevel" ] -> [ Toplevel ]
 END
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
new file mode 100644
index 0000000000..e16e999f60
--- /dev/null
+++ b/contrib/extraction/scheme.ml
@@ -0,0 +1,182 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Production of Scheme syntax. *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Miniml
+open Table
+open Mlutil
+open Options
+open Nametab
+open Ocaml
+
+(*s Scheme renaming issues. *)
+
+let keywords =     
+  List.fold_right (fun s -> Idset.add (id_of_string s))
+    [ "define"; "let"; "lambda"; "lambdas"; "match-case"; 
+      "apply"; "car"; "cdr"; 
+      "error"; "delay"; "force"; "_"; "__"] 
+    Idset.empty
+    
+
+let preamble _ _ print_dummy = 
+  (if print_dummy then 
+     str "(define __ (lambda (_) __))" 
+     ++ fnl () ++ fnl()
+   else mt ())
+
+let paren st = str "(" ++ st ++ str ")"
+
+let pp_abst st = function 
+  | [] -> assert false
+  | [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
+  | l -> paren 
+	(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+
+(*s The pretty-printing functor. *)
+
+module Make = functor(P : Mlpp_param) -> struct
+
+let pp_global r env = P.pp_global r false (Some (snd env))
+let pp_global' r = P.pp_global r false None
+
+let rename_global r = P.rename_global r false 
+
+let empty_env () = [], P.globals()
+
+let rec apply st = function 
+  | [] -> st 
+  | a :: args -> apply (paren (st ++ spc () ++ a)) args 
+
+(*s Pretty-printing of expressions.  *)
+
+let rec pp_expr env args = 
+  let apply st = apply st args in 
+  function
+    | MLrel n -> 
+	let id = get_db_name n env in apply (pr_id id)
+    | MLapp (f,args') ->
+	let stl = List.map (pp_expr env []) args' in
+        pp_expr env (stl @ args) f
+    | MLlam _ as a -> 
+      	let fl,a' = collect_lams a in
+	let fl,env' = push_vars fl env in
+	pp_abst (pp_expr env' [] a') (List.rev fl)
+    | MLletin (id,a1,a2) ->
+	let i,env' = push_vars [id] env in
+	apply 
+	  (hv 0 
+	     (hov 2 
+		(paren 
+		   (str "let " ++ 
+		    paren 
+		      (paren 
+			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
+		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
+    | MLglob r -> 
+	apply (pp_global r env)
+    | MLcons (r,args') ->
+	assert (args=[]);
+	let st = 
+	  str "`" ++ 
+	  paren (pp_global r env ++ 
+		 (if args' = [] then mt () else (spc () ++ str ",")) ++
+		 prlist_with_sep 
+		   (fun () -> spc () ++ str ",") 
+		   (pp_expr env []) args')
+	in 
+	if Refset.mem r !cons_cofix then 
+	  paren (str "delay " ++ st)
+        else st 
+    | MLcase (t, pv) ->
+	let r,_,_ = pv.(0) in 
+	let e = if Refset.mem r !cons_cofix then 
+	  paren (str "force" ++ spc () ++ pp_expr env [] t)
+	else 
+	  pp_expr env [] t 	
+	in apply (v 3 (paren 
+			 (str "match-case " ++ e ++ fnl () ++ pp_pat env pv)))
+    | MLfix (i,ids,defs) ->
+	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+      	pp_fix env' i (Array.of_list (List.rev ids'),defs) args
+    | MLexn s -> 
+	(* An [MLexn] may be applied, but I don't really care. *)
+	paren (str "absurd")
+    | MLdummy ->
+	str "`_" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy' -> 
+	str "__" (* idem *)
+    | MLcast (a,t) ->
+	pp_expr env args a
+    | MLmagic a ->
+	pp_expr env args a
+
+
+and pp_one_pat env (r,ids,t) = 
+  let pp_arg id = str "?" ++ pr_id id in 
+  let ids,env' = push_vars (List.rev ids) env in
+  let args = 
+    if ids = [] then mt () 
+    else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
+  in 
+  (pp_global r env ++ args), (pp_expr env' [] t)
+  
+and pp_pat env pv = 
+  prvect_with_sep fnl  
+    (fun x -> let s1,s2 = pp_one_pat env x in 
+     hov 2 (str "((" ++ s1 ++ str ")" ++ spc () ++ s2 ++ str ")")) pv
+
+(*s names of the functions ([ids]) are already pushed in [env],
+    and passed here just for convenience. *)
+
+and pp_fix env j (ids,bl) args =
+    paren 
+      (str "letrec " ++
+       (v 0 (paren 
+	       (prvect_with_sep fnl
+		  (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
+	     fnl () ++
+      	     hov 2 (apply (pr_id (ids.(j))) args))))
+
+let pp_ast a = hov 0 (pp_expr (empty_env ()) [] a)
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl = function
+  | Dtype _ -> mt ()
+  | Dabbrev _ -> mt () 
+  | Dfix (rv, defs) ->
+      let ids = Array.map rename_global rv in 
+      let env = List.rev (Array.to_list ids), P.globals() in
+      prvect_with_sep 
+	fnl 
+	(fun (fi,ti) -> 
+	   hov 2 
+	     (paren (str "define " ++ pr_id fi ++ spc () ++ 
+		     (pp_expr env [] ti)) 
+	      ++ fnl ()))
+	(array_map2 (fun id b -> (id,b)) ids defs)
+  | Dglob (r, a) ->
+      hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++
+		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
+  | Dcustom (r,s) -> 
+      hov 2 (paren (str "define " ++ pp_global' r ++ spc () ++ str s) ++ fnl ())
+	
+let pp_type _ = mt () 
+
+end
+
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
new file mode 100644
index 0000000000..4a98e97694
--- /dev/null
+++ b/contrib/extraction/scheme.mli
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+(*s Some utility functions to be reused in module [Haskell]. *)
+
+open Pp
+open Miniml
+open Names
+open Nametab
+
+val keywords : Idset.t
+
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
+
+module Make : functor(P : Mlpp_param) -> Mlpp
+
+
+
+
+
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index ee7267f3f6..ff41f6528a 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -67,29 +67,9 @@ let check_constant r =
   else errorlabstrm "extract_constant"
 	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
 
-(*
-let string_of_varg = function
-  | VARG_IDENTIFIER id -> string_of_id id
-  | VARG_STRING s -> s
-  | _ -> assert false
-*)
-
-let no_such_reference q =
-  errorlabstrm "reference_of_varg" 
-    (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".")
-
-(*
-let reference_of_varg = function
-  | VARG_QUALID q -> 
-      (try Nametab.locate q with Not_found -> no_such_reference q)
-  | _ -> assert false
-
-let refs_of_vargl = List.map reference_of_varg
-*)
-
 (*s Target Language *)
 
-type lang = Ocaml | Haskell | Toplevel
+type lang = Ocaml | Haskell | Scheme | Toplevel
 
 let lang_ref = ref Ocaml
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 9fa7142ce8..6f30c1d81b 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -24,15 +24,9 @@ val optim :  unit -> bool
 
 module Refset : Set.S with type elt = global_reference
 
-(*s Auxiliary functions *) 
-		      
-val check_constant : global_reference -> global_reference
-
-(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*)
-
 (*s Target language. *)
 
-type lang = Ocaml | Haskell | Toplevel
+type lang = Ocaml | Haskell | Scheme | Toplevel
 
 val lang : unit -> lang 
 
@@ -67,3 +61,5 @@ val reset_extraction_inline : unit -> unit
 val extract_constant_inline : bool -> qualid located -> string -> unit
 
 val extract_inductive : qualid located -> string * string list -> unit
+
+