|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(*s Production of Haskell syntax. *)
open Pp
open CErrors
open Util
open Names
open Globnames
open Table
open Miniml
open Mlutil
open Common
(*s Haskell renaming issues. *)
let pr_lower_id id = str (String.uncapitalize_ascii (Id.to_string id))
let pr_upper_id id = str (String.capitalize_ascii (Id.to_string id))
let keywords =
List.fold_right (fun s -> Id.Set.add (Id.of_string s))
[ "Any"; "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
"if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
"let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
"as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
Id.Set.empty
let pp_comment s = str "-- " ++ s ++ fnl ()
let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
(* Note: do not shorten [str "foo" ++ fnl ()] into [str "foo\n"],
the '\n' character interacts badly with the Format boxing mechanism *)
let preamble mod_name comment used_modules usf =
let pp_import mp = str ("import qualified "^ string_of_modfile mp) ++ fnl ()
in
(if not (usf.magic || usf.tunknown) then mt ()
else
str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}" ++ fnl2 ())
++
(match comment with
| None -> mt ()
| Some com -> pp_bracket_comment com ++ fnl2 ())
++
str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
str "import qualified Prelude" ++ fnl () ++
prlist pp_import used_modules ++ fnl ()
++
(if not (usf.magic || usf.tunknown) then mt ()
else
str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
str "import qualified GHC.Base" ++ fnl () ++
str "#else" ++ fnl () ++
str "-- HUGS" ++ fnl () ++
str "import qualified IOExts" ++ fnl () ++
str "#endif" ++ fnl2 ())
++
(if not usf.magic then mt ()
else
str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
str "unsafeCoerce :: a -> b" ++ fnl () ++
str "unsafeCoerce = GHC.Base.unsafeCoerce#" ++ fnl () ++
str "#else" ++ fnl () ++
str "-- HUGS" ++ fnl () ++
str "unsafeCoerce :: a -> b" ++ fnl () ++
str "unsafeCoerce = IOExts.unsafeCoerce" ++ fnl () ++
str "#endif" ++ fnl2 ())
++
(if not usf.tunknown then mt ()
else
str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
str "type Any = GHC.Base.Any" ++ fnl () ++
str "#else" ++ fnl () ++
str "-- HUGS" ++ fnl () ++
str "type Any = ()" ++ fnl () ++
str "#endif" ++ fnl2 ())
++
(if not usf.mldummy then mt ()
else
str "__ :: any" ++ fnl () ++
str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
let pp_abst = function
| [] -> (mt ())
| l -> (str "\\" ++
prlist_with_sep (fun () -> (str " ")) Id.print l ++
str " ->" ++ spc ())
(*s The pretty-printer for haskell syntax *)
let pp_global k r =
if is_inline_custom r then str (find_custom r)
else str (Common.pp_global k r)
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ -> assert false
| Tvar i ->
(try Id.print (List.nth vl (pred i))
with Failure _ -> (str "a" ++ int i))
| Tglob (r,[]) -> pp_global Type r
| Tglob (IndRef(kn,0),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)
| Tarr (t1,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 ()
in
hov 0 (pp_rec par t)
(*s Pretty-printing of expressions. [par] indicates whether
parentheses are needed or not. [env] is the list of names for the
de Bruijn variables. [args] is the list of collected arguments
(already pretty-printed). *)
let expr_needs_par = function
| MLlam _ -> true
| MLcase _ -> false (* now that we use the case ... of { ... } syntax *)
| _ -> false
let rec pp_expr par env args =
let apply st = pp_apply st par args
and apply2 st = pp_apply2 st par args in
function
| MLrel n ->
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
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
| 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))
| MLglob 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
| 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)
| MLcase (typ,t,pv) ->
apply2
(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
| MLexn 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)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
| MLuint _ ->
pp_par par (str "Prelude.error \"EXTRACTION OF UINT NOT IMPLEMENTED\"")
and pp_cons_pat par r ppl =
pp_par par
(pp_global Cons r ++ space_if (not (List.is_empty ppl)) ++ prlist_with_sep spc identity ppl)
and pp_gen_pat par ids env = function
| Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
| Pusual r -> pp_cons_pat par r (List.map Id.print ids)
| Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l
| Pwild -> str "_"
| Prel n -> Id.print (get_db_name n env)
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)
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 ()))
pv
(*s names of the functions ([ids]) are already pushed in [env],
and passed here just for convenience. *)
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 "}") ++
fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args))
and pp_function env f t =
let bl,t' = collect_lams t in
let bl,env' = push_vars (List.map id_of_mlid bl) env in
(f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
hov 2 (pp_expr false env' [] t'))
(*s Pretty-printing of inductive types declaration. *)
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)
let pp_singleton kn packet =
let name = pp_global Type (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)))
let pp_one_ind ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
(pp_global Cons r ++
match l with
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
(fun () -> (str " ")) (pp_type true pl) l))
in
str (if Array.is_empty cv then "type " else "data ") ++
pp_global Type (IndRef ip) ++
prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
if Array.is_empty cv then str " () -- empty inductive"
else
(fnl () ++ str " " ++
v 0 (str " " ++
prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor
(Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
let rec pp_ind first kn i ind =
if i >= Array.length ind.ind_packets then
if first then mt () else fnl ()
else
let ip = (kn,i) in
let p = ind.ind_packets.(i) in
if is_custom (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
else
pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++
pp_ind false kn (i+1) ind
(*s Pretty-printing of a declaration. *)
let pp_decl = function
| Dind (kn,i) when i.ind_kind == Singleton ->
pp_singleton kn i.ind_packets.(0) ++ fnl ()
| Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
| 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 ()
| Dfix (rv, defs, typs) ->
let names = Array.map
(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) &&
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
| 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 rec pp_structure_elem = function
| (l,SEdecl d) -> pp_decl d
| (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
| (l,SEmodtype m) -> mt ()
(* for the moment we simply discard module type *)
and pp_module_expr = function
| MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel
| MEfunctor _ -> mt ()
(* for the moment we simply discard unapplied functors *)
| MEident _ | MEapply _ -> assert false
(* should be expanded in extract_env *)
let pp_struct =
let pp_sel (mp,sel) =
push_visible mp [];
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
prlist_strict pp_sel
let haskell_descr = {
keywords = keywords;
file_suffix = ".hs";
file_naming = string_of_modfile;
preamble = preamble;
pp_struct = pp_struct;
sig_suffix = None;
sig_preamble = (fun _ _ _ _ -> mt ());
pp_sig = (fun _ -> mt ());
pp_decl = pp_decl;
}
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
