diff options
Diffstat (limited to 'contrib/extraction/scheme.ml')
| -rw-r--r-- | contrib/extraction/scheme.ml | 75 |
1 files changed, 39 insertions, 36 deletions
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 7004a202..600f64db 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml 7651 2005-12-16 03:19:20Z letouzey $ i*) +(*i $Id: scheme.ml 10233 2007-10-17 23:29:08Z letouzey $ i*) (*s Production of Scheme syntax. *) @@ -18,7 +18,7 @@ open Libnames open Miniml open Mlutil open Table -open Ocaml +open Common (*s Scheme renaming issues. *) @@ -29,17 +29,11 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Idset.empty -let preamble _ _ (mldummy,_,_) _ = - str ";; This extracted scheme code relies on some additional macros" ++ - fnl () ++ - str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++ - fnl () ++ - str "(load \"macros_extr.scm\")" ++ - fnl () ++ fnl () ++ - (if mldummy then - str "(define __ (lambda (_) __))" - ++ fnl () ++ fnl() - else mt ()) +let preamble _ _ usf = + str ";; This extracted scheme code relies on some additional macros\n" ++ + str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++ + str "(load \"macros_extr.scm\")\n\n" ++ + (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = let s = string_of_id id in @@ -60,14 +54,11 @@ let pp_apply st _ = function | [] -> st | [a] -> hov 2 (paren (st ++ spc () ++ a)) | args -> hov 2 (paren (str "@ " ++ st ++ - (prlist (fun x -> spc () ++ x) args))) + (prlist_strict (fun x -> spc () ++ x) args))) -(*s The pretty-printing functor. *) +(*s The pretty-printer for Scheme syntax *) -module Make = functor(P : Mlpp_param) -> struct - -let pp_global r = P.pp_global [initial_path] r -let empty_env () = [], P.globals() +let pp_global k r = str (Common.pp_global k r) (*s Pretty-printing of expressions. *) @@ -95,17 +86,17 @@ let rec pp_expr env args = (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> - apply (pp_global r) + apply (pp_global Term r) | MLcons (i,r,args') -> assert (args=[]); let st = str "`" ++ - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args' = [] then mt () else spc ()) ++ 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 ((i,_),t, pv) -> let e = if i <> Coinductive then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) @@ -125,7 +116,7 @@ let rec pp_expr env args = and pp_cons_args env = function | MLcons (i,r,args) when i<>Coinductive -> - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) | e -> str "," ++ pp_expr env [] e @@ -137,7 +128,7 @@ and pp_one_pat env (r,ids,t) = if ids = [] then mt () else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) in - (pp_global r ++ args), (pp_expr env' [] t) + (pp_global Cons r ++ args), (pp_expr env' [] t) and pp_pat env pv = prvect_with_sep fnl @@ -160,11 +151,11 @@ and pp_fix env j (ids,bl) args = (*s Pretty-printing of a declaration. *) -let pp_decl _ = function +let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map pp_global rv in + let ppv = Array.map (pp_global Term) rv in prvect_with_sep fnl (fun (pi,ti) -> hov 2 @@ -177,23 +168,35 @@ let pp_decl _ = function if is_inline_custom r then mt () else if is_custom r then - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ str (find_custom r))) ++ fnl () ++ fnl () else - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () -let pp_structure_elem mp = function - | (l,SEdecl d) -> pp_decl mp d +let pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d | (l,SEmodule m) -> failwith "TODO: Scheme extraction of modules not implemented yet" | (l,SEmodtype m) -> failwith "TODO: Scheme extraction of modules not implemented yet" let pp_struct = - prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel) - -let pp_signature s = assert false - -end - + let pp_sel (mp,sel) = + push_visible mp; + let p = prlist_strict pp_structure_elem sel in + pop_visible (); p + in + prlist_strict pp_sel + +let scheme_descr = { + keywords = keywords; + file_suffix = ".scm"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} |