diff options
Diffstat (limited to 'contrib/extraction/scheme.ml')
-rw-r--r-- | contrib/extraction/scheme.ml | 202 |
1 files changed, 0 insertions, 202 deletions
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml deleted file mode 100644 index f4941a9c..00000000 --- a/contrib/extraction/scheme.ml +++ /dev/null @@ -1,202 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: scheme.ml 11559 2008-11-07 22:03:34Z letouzey $ i*) - -(*s Production of Scheme syntax. *) - -open Pp -open Util -open Names -open Nameops -open Libnames -open Miniml -open Mlutil -open Table -open Common - -(*s Scheme renaming issues. *) - -let keywords = - List.fold_right (fun s -> Idset.add (id_of_string s)) - [ "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" ++ - 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 - 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 - | [] -> 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) - -let pp_apply st _ = function - | [] -> st - | [a] -> hov 2 (paren (st ++ spc () ++ a)) - | args -> hov 2 (paren (str "@ " ++ st ++ - (prlist_strict (fun x -> spc () ++ x) args))) - -(*s The pretty-printer for Scheme syntax *) - -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 - 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 - 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)) - ++ spc () ++ hov 0 (pp_expr env' [] a2))))) - | MLglob r -> - apply (pp_global Term r) - | MLcons (i,r,args') -> - assert (args=[]); - 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 - | 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 "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 "error \"AXIOM TO BE REALIZED\"") - -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) = - let ids,env' = push_vars (List.rev ids) env in - let args = - if ids = [] then mt () - else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) - 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 - 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) ++ 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)))) - -(*s Pretty-printing of a declaration. *) - -let pp_decl = function - | Dind _ -> 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)) - ++ 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 - hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ - pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () - -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 = - 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; - sig_suffix = None; - sig_preamble = (fun _ _ _ -> mt ()); - pp_sig = (fun _ -> mt ()); - pp_decl = pp_decl; -} |