diff options
Diffstat (limited to 'plugins/extraction/scheme.ml')
| -rw-r--r-- | plugins/extraction/scheme.ml | 144 |
1 files changed, 72 insertions, 72 deletions
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index c341ec8d57..c41b0d7a02 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -50,13 +50,13 @@ 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) + (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))) + (prlist_strict (fun x -> spc () ++ x) args))) (*s The pretty-printer for Scheme syntax *) @@ -68,66 +68,66 @@ 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) + let id = get_db_name n env in apply (pr_id id) | MLapp (f,args') -> - let stl = List.map (pp_expr env []) args' in + 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 (List.map id_of_mlid fl) env in - apply (pp_abst (pp_expr env' [] a') (List.rev fl)) + let fl,a' = collect_lams a in + let fl,env' = push_vars (List.map id_of_mlid fl) env in + apply (pp_abst (pp_expr env' [] a') (List.rev fl)) | MLletin (id,a1,a2) -> - let i,env' = push_vars [id_of_mlid 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))))) + let i,env' = push_vars [id_of_mlid 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) + apply (pp_global Term r) | MLcons (_,r,args') -> - assert (List.is_empty args); - let st = - str "`" ++ - paren (pp_global Cons r ++ - (if List.is_empty args' then mt () else spc ()) ++ - prlist_with_sep spc (pp_cons_args env) args') - in - if is_coinductive r then paren (str "delay " ++ st) else st + assert (List.is_empty args); + let st = + str "`" ++ + paren (pp_global Cons r ++ + (if List.is_empty args' then mt () else spc ()) ++ + prlist_with_sep spc (pp_cons_args env) args') + in + if is_coinductive r then paren (str "delay " ++ st) else st | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.") | MLcase (_,_,pv) when not (is_regular_match pv) -> - user_err Pp.(str "Cannot handle general patterns in Scheme yet.") + user_err Pp.(str "Cannot handle general patterns in Scheme yet.") | MLcase (_,t,pv) when is_custom_match pv -> - let mkfun (ids,_,e) = - if not (List.is_empty ids) then named_lams (List.rev ids) e - else dummy_lams (ast_lift 1 e) 1 - in - apply - (paren - (hov 2 - (str (find_custom_match pv) ++ fnl () ++ - prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv - ++ pp_expr env [] t))) + let mkfun (ids,_,e) = + if not (List.is_empty ids) then named_lams (List.rev ids) e + else dummy_lams (ast_lift 1 e) 1 + in + apply + (paren + (hov 2 + (str (find_custom_match pv) ++ fnl () ++ + prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv + ++ pp_expr env [] t))) | MLcase (typ,t, pv) -> let e = - if not (is_coinductive_type typ) 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))) + if not (is_coinductive_type typ) 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 + 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) + (* 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. *) + str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> - pp_expr env args a + pp_expr env args a | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") | MLuint _ -> paren (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") @@ -137,8 +137,8 @@ let rec pp_expr env args = and pp_cons_args env = function | MLcons (_,r,args) when is_coinductive r -> paren (pp_global Cons r ++ - (if List.is_empty args then mt () else spc ()) ++ - prlist_with_sep spc (pp_cons_args env) args) + (if List.is_empty 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 (ids,p,t) = @@ -166,12 +166,12 @@ 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)))) + (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. *) @@ -180,29 +180,29 @@ let pp_decl = function | Dtype _ -> mt () | Dfix (rv, defs,_) -> let names = Array.map - (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv in prvecti - (fun i r -> - let void = is_inline_custom r || - (not (is_custom r) && + (fun i r -> + let void = is_inline_custom r || + (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false) - in - if void then mt () - else - hov 2 - (paren (str "define " ++ names.(i) ++ spc () ++ - (if is_custom r then str (find_custom r) - else pp_expr (empty_env ()) [] defs.(i))) - ++ fnl ()) ++ fnl ()) - rv + in + if void then mt () + else + hov 2 + (paren (str "define " ++ names.(i) ++ spc () ++ + (if is_custom r then str (find_custom r) + else pp_expr (empty_env ()) [] defs.(i))) + ++ fnl ()) ++ fnl ()) + rv | Dterm (r, a, _) -> if is_inline_custom r then mt () else - hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ - (if is_custom r then str (find_custom r) - else pp_expr (empty_env ()) [] a))) - ++ fnl2 () + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ + (if is_custom r then str (find_custom r) + else pp_expr (empty_env ()) [] a))) + ++ fnl2 () let rec pp_structure_elem = function | (l,SEdecl d) -> pp_decl d |