diff options
Diffstat (limited to 'plugins/extraction/haskell.ml')
| -rw-r--r-- | plugins/extraction/haskell.ml | 204 |
1 files changed, 102 insertions, 102 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 4769bef475..f0053ba6b5 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -110,15 +110,15 @@ let rec pp_type par vl t = with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (GlobRef.IndRef(kn,0),l) - when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> - pp_type true vl (List.hd l) + when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> + pp_type true vl (List.hd l) | Tglob (r,l) -> - pp_par par - (pp_global Type r ++ spc () ++ - prlist_with_sep spc (pp_type true vl) l) + pp_par par + (pp_global Type r ++ spc () ++ + prlist_with_sep spc (pp_type true vl) l) | Tarr (t1,t2) -> - pp_par par - (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) + pp_par par + (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) | Tdummy _ -> str "()" | Tunknown -> str "Any" | Taxiom -> str "() -- AXIOM TO BE REALIZED" ++ fnl () @@ -141,77 +141,77 @@ let rec pp_expr par env args = and apply2 st = pp_apply2 st par args in function | MLrel n -> - let id = get_db_name n env in + let id = get_db_name n env in (* Try to survive to the occurrence of a Dummy rel. TODO: we should get rid of this hack (cf. BZ#592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in apply (Id.print id) | MLapp (f,args') -> - let stl = List.map (pp_expr true env []) args' in + let stl = List.map (pp_expr true env []) args' in pp_expr par 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 - let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in - apply2 st + let fl,a' = collect_lams a in + let fl,env' = push_vars (List.map id_of_mlid fl) env in + let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in + apply2 st | MLletin (id,a1,a2) -> - let i,env' = push_vars [id_of_mlid id] env in - let pp_id = Id.print (List.hd i) - and pp_a1 = pp_expr false env [] a1 - and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in - let pp_def = - str "let {" ++ cut () ++ - hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}") - in - apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ - spc () ++ hov 0 pp_a2)) + let i,env' = push_vars [id_of_mlid id] env in + let pp_id = Id.print (List.hd i) + and pp_a1 = pp_expr false env [] a1 + and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in + let pp_def = + str "let {" ++ cut () ++ + hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}") + in + apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++ + spc () ++ hov 0 pp_a2)) | MLglob r -> - apply (pp_global Term r) + apply (pp_global Term r) | MLcons (_,r,a) as c -> assert (List.is_empty args); begin match a with - | _ when is_native_char c -> pp_native_char c - | [] -> pp_global Cons r - | [a] -> - pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) - | _ -> - pp_par par (pp_global Cons r ++ spc () ++ - prlist_with_sep spc (pp_expr true env []) a) - end + | _ when is_native_char c -> pp_native_char c + | [] -> pp_global Cons r + | [a] -> + pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) + | _ -> + pp_par par (pp_global Cons r ++ spc () ++ + prlist_with_sep spc (pp_expr true env []) a) + end | MLtuple l -> assert (List.is_empty args); pp_boxed_tuple (pp_expr true env []) l | MLcase (_,t, pv) when is_custom_match pv -> if not (is_regular_match pv) then - user_err Pp.(str "Cannot mix yet user-given match and general patterns."); - 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 - let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in - let inner = - str (find_custom_match pv) ++ fnl () ++ - prvect pp_branch pv ++ - pp_expr true env [] t - in - apply2 (hov 2 inner) + user_err Pp.(str "Cannot mix yet user-given match and general patterns."); + 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 + let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in + let inner = + str (find_custom_match pv) ++ fnl () ++ + prvect pp_branch pv ++ + pp_expr true env [] t + in + apply2 (hov 2 inner) | MLcase (typ,t,pv) -> apply2 - (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ - fnl () ++ pp_pat env pv)) + (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++ + fnl () ++ pp_pat env pv)) | MLfix (i,ids,defs) -> - let ids',env' = push_vars (List.rev (Array.to_list ids)) env in - pp_fix par 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 par env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> - (* An [MLexn] may be applied, but I don't really care. *) - pp_par par (str "Prelude.error" ++ spc () ++ qs s) + (* An [MLexn] may be applied, but I don't really care. *) + pp_par par (str "Prelude.error" ++ spc () ++ qs s) | MLdummy k -> (* An [MLdummy] may be applied, but I don't really care. *) (match msg_of_implicit k with | "" -> str "__" | s -> str "__" ++ spc () ++ pp_bracket_comment (str s)) | MLmagic a -> - pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) + pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") | MLuint _ -> pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"") @@ -232,16 +232,16 @@ and pp_gen_pat par ids env = function and pp_one_pat env (ids,p,t) = let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in hov 2 (str " " ++ - pp_gen_pat false (List.rev ids') env' p ++ - str " ->" ++ spc () ++ - pp_expr (expr_needs_par t) env' [] t) + pp_gen_pat false (List.rev ids') env' p ++ + str " ->" ++ spc () ++ + pp_expr (expr_needs_par t) env' [] t) and pp_pat env pv = prvecti (fun i x -> pp_one_pat env pv.(i) ++ if Int.equal i (Array.length pv - 1) then str "}" else - (str ";" ++ fnl ())) + (str ";" ++ fnl ())) pv (*s names of the functions ([ids]) are already pushed in [env], @@ -251,10 +251,10 @@ and pp_fix par env i (ids,bl) args = pp_par par (v 0 (v 1 (str "let {" ++ fnl () ++ - prvect_with_sep (fun () -> str ";" ++ fnl ()) - (fun (fi,ti) -> pp_function env (Id.print fi) ti) - (Array.map2 (fun a b -> a,b) ids bl) ++ - str "}") ++ + prvect_with_sep (fun () -> str ";" ++ fnl ()) + (fun (fi,ti) -> pp_function env (Id.print fi) ti) + (Array.map2 (fun a b -> a,b) ids bl) ++ + str "}") ++ fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args)) and pp_function env f t = @@ -269,17 +269,17 @@ and pp_function env f t = let pp_logical_ind packet = pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc Id.print packet.ip_consnames) + prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = let name = pp_global Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ - prlist_with_sep spc Id.print l ++ - (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ - pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ - pp_comment (str "singleton inductive, whose constructor was " ++ - Id.print packet.ip_consnames.(0))) + prlist_with_sep spc Id.print l ++ + (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_comment (str "singleton inductive, whose constructor was " ++ + Id.print packet.ip_consnames.(0))) let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in @@ -288,8 +288,8 @@ let pp_one_ind ip pl cv = match l with | [] -> (mt ()) | _ -> (str " " ++ - prlist_with_sep - (fun () -> (str " ")) (pp_type true pl) l)) + prlist_with_sep + (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.is_empty cv then "type " else "data ") ++ pp_global Type (GlobRef.IndRef ip) ++ @@ -298,7 +298,7 @@ let pp_one_ind ip pl cv = else (fnl () ++ str " " ++ v 0 (str " " ++ - prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor + prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv))) let rec pp_ind first kn i ind = @@ -310,10 +310,10 @@ let rec pp_ind first kn i ind = if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind else if p.ip_logical then - pp_logical_ind p ++ pp_ind first kn (i+1) ind + pp_logical_ind p ++ pp_ind first kn (i+1) ind else - pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ - pp_ind false kn (i+1) ind + pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ + pp_ind false kn (i+1) ind (*s Pretty-printing of a declaration. *) @@ -325,45 +325,45 @@ let pp_decl = function | Dtype (r, l, t) -> if is_inline_custom r then mt () else - let l = rename_tvars keywords l in - let st = - try - let ids,s = find_type_custom r in - prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s - with Not_found -> - prlist (fun id -> Id.print id ++ str " ") l ++ - if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () - else str "=" ++ spc () ++ pp_type false l t - in - hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () + let l = rename_tvars keywords l in + let st = + try + let ids,s = find_type_custom r in + prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s + with Not_found -> + prlist (fun id -> Id.print id ++ str " ") l ++ + if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () + else str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () | Dfix (rv, defs, typs) -> 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 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++ - (if is_custom r then - (names.(i) ++ str " = " ++ str (find_custom r)) - else - (pp_function (empty_env ()) names.(i) defs.(i))) - ++ fnl2 ()) - rv + in + if void then mt () + else + hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++ + (if is_custom r then + (names.(i) ++ str " = " ++ str (find_custom r)) + else + (pp_function (empty_env ()) names.(i) defs.(i))) + ++ fnl2 ()) + rv | Dterm (r, a, t) -> if is_inline_custom r then mt () else - let e = pp_global Term r in - hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++ - if is_custom r then - hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) - else - hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) + let e = pp_global Term r in + hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++ + if is_custom r then + hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) + else + hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) let rec pp_structure_elem = function | (l,SEdecl d) -> pp_decl d |