diff options
Diffstat (limited to 'contrib/extraction/scheme.ml')
| -rw-r--r-- | contrib/extraction/scheme.ml | 78 |
1 files changed, 51 insertions, 27 deletions
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 61045304..4a881da2 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,v 1.9.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*) (*s Production of Scheme syntax. *) @@ -24,17 +24,30 @@ open Ocaml let keywords = List.fold_right (fun s -> Idset.add (id_of_string s)) - [ "define"; "let"; "lambda"; "lambdas"; "match-case"; + [ "define"; "let"; "lambda"; "lambdas"; "match"; "apply"; "car"; "cdr"; "error"; "delay"; "force"; "_"; "__"] Idset.empty -let preamble _ _ (mldummy,_,_) = +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 pr_id id = + let s = string_of_id id in + for i = 0 to String.length s - 1 do + if s.[i] = '\'' then s.[i] <- '~' + done; + str s + let paren = pp_par true let pp_abst st = function @@ -43,6 +56,12 @@ let pp_abst st = function | l -> paren (str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st) +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))) + (*s The pretty-printing functor. *) module Make = functor(P : Mlpp_param) -> struct @@ -63,7 +82,7 @@ let rec pp_expr env args = | 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) + apply (pp_abst (pp_expr env' [] a') (List.rev fl)) | MLletin (id,a1,a2) -> let i,env' = push_vars [id] env in apply @@ -77,46 +96,46 @@ let rec pp_expr env args = ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> apply (pp_global r) - | MLcons (r,args') -> + | MLcons (i,r,args') -> assert (args=[]); let st = str "`" ++ paren (pp_global r ++ - (if args' = [] then mt () else (spc () ++ str ",")) ++ - prlist_with_sep - (fun () -> spc () ++ str ",") - (pp_expr env []) args') + (if args' = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args 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))) + if i = Coinductive then paren (str "delay " ++ st) else st + | MLcase (i,t, pv) -> + let e = + if i <> Coinductive then pp_expr env [] t + else paren (str "force" ++ spc () ++ pp_expr env [] t) + in + apply (v 3 (paren (str "match " ++ 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") + paren (str "error" ++ spc () ++ qs s) | MLdummy -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> pp_expr env args a - | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n") + | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") + +and pp_cons_args env = function + | MLcons (i,r,args) when i<>Coinductive -> + paren (pp_global r ++ + (if args = [] then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args) + | e -> str "," ++ pp_expr env [] e 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)) + else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) in (pp_global r ++ args), (pp_expr env' [] t) @@ -133,7 +152,8 @@ and pp_fix env j (ids,bl) args = (str "letrec " ++ (v 0 (paren (prvect_with_sep fnl - (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti))) + (fun (fi,ti) -> + paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti))) (array_map2 (fun id b -> (id,b)) ids bl)) ++ fnl () ++ hov 2 (pp_apply (pr_id (ids.(j))) true args)))) @@ -156,8 +176,12 @@ let pp_decl _ = function | Dterm (r, a, _) -> if is_inline_custom r then mt () else - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ - pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () + if is_custom r then + hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + str (find_custom r))) ++ fnl () ++ fnl () + else + hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () let pp_structure_elem mp = function | (l,SEdecl d) -> pp_decl mp d |