aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/extraction/scheme.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/scheme.ml')
-rw-r--r--contrib/extraction/scheme.ml158
1 files changed, 79 insertions, 79 deletions
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 75af1b7bc..eaa47f5f9 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -22,38 +22,38 @@ open Common
(*s Scheme renaming issues. *)
-let keywords =
+let keywords =
List.fold_right (fun s -> Idset.add (id_of_string s))
- [ "define"; "let"; "lambda"; "lambdas"; "match";
- "apply"; "car"; "cdr";
- "error"; "delay"; "force"; "_"; "__"]
+ [ "define"; "let"; "lambda"; "lambdas"; "match";
+ "apply"; "car"; "cdr";
+ "error"; "delay"; "force"; "_"; "__"]
Idset.empty
-let preamble _ _ usf =
- str ";; This extracted scheme code relies on some additional macros\n" ++
+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 pr_id id =
let s = string_of_id id in
- for i = 0 to String.length s - 1 do
+ for i = 0 to String.length s - 1 do
if s.[i] = '\'' then s.[i] <- '~'
- done;
+ done;
str s
let paren = pp_par true
-let pp_abst st = function
+let pp_abst st = function
| [] -> assert false
| [id] -> paren (str "lambda " ++ paren (pr_id id) ++ spc () ++ st)
- | l -> paren
+ | l -> paren
(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
-let pp_apply st _ = function
- | [] -> st
+let pp_apply st _ = function
+ | [] -> st
| [a] -> hov 2 (paren (st ++ spc () ++ a))
- | args -> hov 2 (paren (str "@ " ++ st ++
+ | args -> hov 2 (paren (str "@ " ++ st ++
(prlist_strict (fun x -> spc () ++ x) args)))
(*s The pretty-printer for Scheme syntax *)
@@ -62,50 +62,50 @@ let pp_global k r = str (Common.pp_global k r)
(*s Pretty-printing of expressions. *)
-let rec pp_expr env args =
- let apply st = pp_apply st true args in
+let rec pp_expr env args =
+ let apply st = pp_apply st true args in
function
- | MLrel n ->
+ | 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 ->
+ | MLlam _ as a ->
let fl,a' = collect_lams a in
let fl,env' = push_vars fl env in
apply (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))
+ 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 ->
+ | MLglob r ->
apply (pp_global Term r)
| MLcons (i,r,args') ->
assert (args=[]);
- let st =
- str "`" ++
- paren (pp_global Cons r ++
+ let st =
+ str "`" ++
+ 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
+ in
+ if i = Coinductive then paren (str "delay " ++ st) else st
| MLcase ((i,_),t, pv) ->
- let e =
- if i <> Coinductive then pp_expr env [] t
+ let e =
+ if i <> Coinductive then pp_expr env [] t
else paren (str "force" ++ spc () ++ pp_expr env [] t)
- in
+ 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 ->
+ | MLexn s ->
(* An [MLexn] may be applied, but I don't really care. *)
paren (str "error" ++ spc () ++ qs s)
| MLdummy ->
@@ -114,36 +114,36 @@ let rec pp_expr env args =
pp_expr env args a
| MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
-and pp_cons_args env = function
- | MLcons (i,r,args) when i<>Coinductive ->
- paren (pp_global Cons r ++
+and pp_cons_args env = function
+ | MLcons (i,r,args) when i<>Coinductive ->
+ 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
-
-and pp_one_pat env (r,ids,t) =
+
+and pp_one_pat env (r,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
- let args =
- if ids = [] then mt ()
+ let args =
+ if ids = [] then mt ()
else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
- in
+ in
(pp_global Cons r ++ 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
+
+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
+ paren
(str "letrec " ++
- (v 0 (paren
+ (v 0 (paren
(prvect_with_sep fnl
- (fun (fi,ti) ->
+ (fun (fi,ti) ->
paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
(array_map2 (fun id b -> (id,b)) ids bl)) ++
fnl () ++
@@ -153,50 +153,50 @@ and pp_fix env j (ids,bl) args =
let pp_decl = function
| Dind _ -> mt ()
- | Dtype _ -> mt ()
+ | Dtype _ -> mt ()
| Dfix (rv, defs,_) ->
- let ppv = Array.map (pp_global Term) rv in
- prvect_with_sep fnl
- (fun (pi,ti) ->
- hov 2
- (paren (str "define " ++ pi ++ spc () ++
- (pp_expr (empty_env ()) [] ti))
+ let ppv = Array.map (pp_global Term) rv in
+ prvect_with_sep fnl
+ (fun (pi,ti) ->
+ hov 2
+ (paren (str "define " ++ pi ++ spc () ++
+ (pp_expr (empty_env ()) [] ti))
++ fnl ()))
(array_map2 (fun p b -> (p,b)) ppv defs) ++
fnl ()
| Dterm (r, a, _) ->
- if is_inline_custom r then mt ()
- else
- if is_custom r then
- hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
- str (find_custom r))) ++ fnl () ++ fnl ()
- else
+ if is_inline_custom r then mt ()
+ else
+ if is_custom r then
+ hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
+ str (find_custom r))) ++ fnl () ++ fnl ()
+ else
hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
-let pp_structure_elem = function
+let pp_structure_elem = function
| (l,SEdecl d) -> pp_decl d
- | (l,SEmodule m) ->
+ | (l,SEmodule m) ->
failwith "TODO: Scheme extraction of modules not implemented yet"
- | (l,SEmodtype m) ->
+ | (l,SEmodtype m) ->
failwith "TODO: Scheme extraction of modules not implemented yet"
-let pp_struct =
- let pp_sel (mp,sel) =
- push_visible mp None;
- let p = prlist_strict pp_structure_elem sel in
+let pp_struct =
+ let pp_sel (mp,sel) =
+ push_visible mp None;
+ 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;
+ 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;
+ sig_preamble = (fun _ _ _ -> mt ());
+ pp_sig = (fun _ -> mt ());
+ pp_decl = pp_decl;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 23:44:30 +0000