# HG changeset patch # User haftmann # Date 1393148023 -3600 # Node ID 59244fc1a7ca915e8508e7188bcccf8d10fb492b # Parent aec339197a400263220301293d0084ee9e4e9b28 formal markup for public ingredients diff -r aec339197a40 -r 59244fc1a7ca src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Sun Feb 23 10:33:43 2014 +0100 +++ b/src/Tools/Code/code_haskell.ML Sun Feb 23 10:33:43 2014 +0100 @@ -355,13 +355,19 @@ deresolve (if string_classes then deriving_show else K false); (* print modules *) - fun print_module_frame module_name ps = + fun print_module_frame module_name exports ps = (module_name, Pretty.chunks2 ( - str ("module " ^ module_name ^ " where {") + concat [str "module", + case exports of + SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)] + | NONE => str module_name, + str "where {" + ] :: ps @| str "}" )); - fun print_qualified_import module_name = semicolon [str "import qualified", str module_name]; + fun print_qualified_import module_name = + semicolon [str "import qualified", str module_name]; val import_common_ps = enclose "import Prelude (" ");" (commas (map str (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified) @@ -371,14 +377,23 @@ fun print_module module_name (gr, imports) = let val deresolve = deresolver module_name; - fun print_import module_name = (semicolon o map str) ["import qualified", module_name]; + val deresolve_import = SOME o str o deresolve; + val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve; + fun print_import (sym, Code_Thingol.Fun _) = deresolve_import sym + | print_import (sym, Code_Thingol.Datatype _) = deresolve_import_attached sym + | print_import (sym, Code_Thingol.Class _) = deresolve_import_attached sym + | print_import (sym, Code_Thingol.Classinst _) = NONE; val import_ps = import_common_ps @ map (print_qualified_import o fst) imports; fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym of (_, NONE) => NONE - | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt))); - val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr); + | (_, SOME (export, stmt)) => + SOME (if export then print_import (sym, stmt) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt))); + val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr + |> map_filter print_stmt' + |> split_list + |> apfst (map_filter I); in - print_module_frame module_name + print_module_frame module_name (SOME export_ps) ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps) end; @@ -399,7 +414,7 @@ (fn width => fn destination => K () o map (write_module width destination)) (fn present => fn width => rpair (try (deresolver "")) o (map o apsnd) (format present width)) - (map (uncurry print_module_frame o apsnd single) includes + (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name)) ((flat o rev o Graph.strong_conn) haskell_program)) end; diff -r aec339197a40 -r 59244fc1a7ca src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Sun Feb 23 10:33:43 2014 +0100 +++ b/src/Tools/Code/code_ml.ML Sun Feb 23 10:33:43 2014 +0100 @@ -795,10 +795,10 @@ ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program; (* print statements *) - fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt + fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt tyco_syntax const_syntax (make_vars reserved_syms) (Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt - |> apfst SOME; + |> apfst (fn decl => if export then SOME decl else NONE); (* print modules *) fun print_module _ base _ xs = diff -r aec339197a40 -r 59244fc1a7ca src/Tools/Code/code_namespace.ML --- a/src/Tools/Code/code_namespace.ML Sun Feb 23 10:33:43 2014 +0100 +++ b/src/Tools/Code/code_namespace.ML Sun Feb 23 10:33:43 2014 +0100 @@ -18,7 +18,7 @@ datatype ('a, 'b) node = Dummy - | Stmt of 'a + | Stmt of bool * 'a | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T) type ('a, 'b) hierarchical_program val hierarchical_program: Proof.context @@ -32,7 +32,7 @@ -> { deresolver: string list -> Code_Symbol.T -> string, hierarchical_program: ('a, 'b) hierarchical_program } val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c, - print_stmt: string list -> Code_Symbol.T * 'a -> 'c, + print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c, lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c } -> ('a, 'b) hierarchical_program -> 'c list end; @@ -82,7 +82,7 @@ (** flat program structure **) -type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T; +type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T; fun flat_program ctxt { module_prefix, module_name, reserved, identifiers, empty_nsp, namify_stmt, modify_stmt } program = @@ -102,7 +102,7 @@ val (module_name, base) = prep_sym sym; in Graph.default_node (module_name, (Code_Symbol.Graph.empty, [])) - #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt))) + #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (true, stmt)))) end; fun add_dep sym sym' = let @@ -116,7 +116,7 @@ { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program; (* name declarations and statement modifications *) - fun declare sym (base, stmt) (gr, nsp) = + fun declare sym (base, (_, stmt)) (gr, nsp) = let val (base', nsp') = namify_stmt stmt base nsp; val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr; @@ -125,7 +125,8 @@ |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym)) (prioritize sym_priority (Code_Symbol.Graph.keys gr)) |> fst - |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt; + |> (Code_Symbol.Graph.map o K o apsnd) + (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt)); val flat_program = proto_program |> (Graph.map o K o apfst) declarations; @@ -162,11 +163,13 @@ datatype ('a, 'b) node = Dummy - | Stmt of 'a + | Stmt of bool * 'a | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T); type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T; +fun the_stmt (Stmt (export, stmt)) = (export, stmt); + fun map_module_content f (Module content) = Module (f content); fun map_module [] = I @@ -206,7 +209,7 @@ let val (name_fragments, base) = prep_sym sym; in - (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt))) + (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt)))) end; fun add_dep sym sym' = let @@ -244,18 +247,18 @@ in (nsps', nodes') end; val (nsps', nodes') = (nsps, nodes) |> fold (declare (K namify_module)) module_fragments - |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms; + |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms; fun select_syms syms = case filter (member (op =) stmt_syms) syms of [] => NONE | syms => SOME syms; - fun select_stmt (sym, SOME stmt) = SOME (sym, stmt) + fun select_stmt (sym, (export, SOME stmt)) = SOME (sym, (export, stmt)) | select_stmt _ = NONE; fun modify_stmts' syms = let - val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms; + val (exports, stmts) = map_split (the_stmt o snd o Code_Symbol.Graph.get_node nodes) syms; val stmts' = modify_stmts (syms ~~ stmts); val stmts'' = stmts' @ replicate (length syms - length stmts') NONE; - in map_filter select_stmt (syms ~~ stmts'') end; + in map_filter select_stmt (syms ~~ (exports ~~ stmts'')) end; val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes; val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content) | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes'; diff -r aec339197a40 -r 59244fc1a7ca src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Sun Feb 23 10:33:43 2014 +0100 +++ b/src/Tools/Code/code_scala.ML Sun Feb 23 10:33:43 2014 +0100 @@ -145,26 +145,28 @@ |> single |> enclose "(" ")" end; + fun privatize false = concat o cons (str "private") + | privatize true = concat; fun print_context tyvars vs sym = applify "[" "]" (fn (v, sort) => (Pretty.block o map str) (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort)) NOBR ((str o deresolve) sym) vs; - fun print_defhead tyvars vars const vs params tys ty = - Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) => + fun print_defhead export tyvars vars const vs params tys ty = + privatize export [str "def", constraint (applify "(" ")" (fn (param, ty) => constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty)) NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty), - str " ="]; - fun print_def const (vs, ty) [] = + str "="]; + fun print_def export const (vs, ty) [] = let val (tys, ty') = Code_Thingol.unfold_fun ty; val params = Name.invent (snd reserved) "a" (length tys); val tyvars = intro_tyvars vs reserved; val vars = intro_vars params reserved; in - concat [print_defhead tyvars vars const vs params tys ty', + concat [print_defhead export tyvars vars const vs params tys ty', str ("sys.error(\"" ^ const ^ "\")")] end - | print_def const (vs, ty) eqs = + | print_def export const (vs, ty) eqs = let val tycos = fold (fn ((ts, t), _) => fold Code_Thingol.add_tyconames (t :: ts)) eqs []; @@ -196,7 +198,7 @@ tuplify (map (print_term tyvars true some_thm vars' NOBR) ts), str "=>", print_rhs vars' eq] end; - val head = print_defhead tyvars vars2 const vs params tys' ty'; + val head = print_defhead export tyvars vars2 const vs params tys' ty'; in if simple then concat [head, print_rhs vars2 (hd eqs)] else @@ -206,14 +208,14 @@ (map print_clause eqs) end; val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant; - fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) = - print_def const (vs, ty) (filter (snd o snd) raw_eqs) - | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) = + fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) = + print_def export const (vs, ty) (filter (snd o snd) raw_eqs) + | print_stmt (Type_Constructor tyco, (export, Code_Thingol.Datatype (vs, cos))) = let val tyvars = intro_tyvars (map (rpair []) vs) reserved; fun print_co ((co, vs_args), tys) = concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR - ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args) + ((privatize export o map str) ["final", "case", "class", deresolve_const co]) vs_args) @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) (Name.invent_names (snd reserved) "a" tys))), str "extends", @@ -222,10 +224,10 @@ ]; in Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars) - NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs + NOBR ((privatize export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs :: map print_co cos) end - | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) = + | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) = let val tyvars = intro_tyvars [(v, [class])] reserved; fun add_typarg s = Pretty.block @@ -244,7 +246,7 @@ val auxs = Name.invent (snd proto_vars) "a" (length tys); val vars = intro_vars auxs proto_vars; in - concat [str "def", constraint (Pretty.block [applify "(" ")" + privatize export [str "def", constraint (Pretty.block [applify "(" ")" (fn (aux, ty) => constraint ((str o lookup_var vars) aux) (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam)) (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ", @@ -255,14 +257,14 @@ in Pretty.chunks ( (Pretty.block_enclose - (concat ([str "trait", (add_typarg o deresolve_class) class] + (privatize export ([str "trait", (add_typarg o deresolve_class) class] @ the_list (print_super_classes classrels) @ [str "{"]), str "}") (map print_classparam_val classparams)) :: map print_classparam_def classparams ) end - | print_stmt (sym, Code_Thingol.Classinst - { class, tyco, vs, inst_params, superinst_params, ... }) = + | print_stmt (sym, (export, Code_Thingol.Classinst + { class, tyco, vs, inst_params, superinst_params, ... })) = let val tyvars = intro_tyvars vs reserved; val classtyp = (class, tyco `%% map (ITyVar o fst) vs); @@ -279,12 +281,12 @@ val aux_abstr1 = abstract_using aux_dom1; val aux_abstr2 = abstract_using aux_dom2; in - concat ([str "val", print_method classparam, str "="] + privatize export ([str "val", print_method classparam, str "="] @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)) end; in - Pretty.block_enclose (concat [str "implicit def", + Pretty.block_enclose (privatize export [str "implicit def", constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp), str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}") (map print_classparam_instance (inst_params @ superinst_params))