formal markup for public ingredients
authorhaftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 5567959244fc1a7ca
parent 55678 aec339197a40
child 55680 bc5edc5dbf18
formal markup for public ingredients
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sun Feb 23 10:33:43 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Feb 23 10:33:43 2014 +0100
     1.3 @@ -355,13 +355,19 @@
     1.4        deresolve (if string_classes then deriving_show else K false);
     1.5  
     1.6      (* print modules *)
     1.7 -    fun print_module_frame module_name ps =
     1.8 +    fun print_module_frame module_name exports ps =
     1.9        (module_name, Pretty.chunks2 (
    1.10 -        str ("module " ^ module_name ^ " where {")
    1.11 +        concat [str "module",
    1.12 +          case exports of
    1.13 +            SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
    1.14 +          | NONE => str module_name,
    1.15 +          str "where {"
    1.16 +        ]
    1.17          :: ps
    1.18          @| str "}"
    1.19        ));
    1.20 -    fun print_qualified_import module_name = semicolon [str "import qualified", str module_name];
    1.21 +    fun print_qualified_import module_name =
    1.22 +      semicolon [str "import qualified", str module_name];
    1.23      val import_common_ps =
    1.24        enclose "import Prelude (" ");" (commas (map str
    1.25          (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
    1.26 @@ -371,14 +377,23 @@
    1.27      fun print_module module_name (gr, imports) =
    1.28        let
    1.29          val deresolve = deresolver module_name;
    1.30 -        fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
    1.31 +        val deresolve_import = SOME o str o deresolve;
    1.32 +        val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
    1.33 +        fun print_import (sym, Code_Thingol.Fun _) = deresolve_import sym
    1.34 +          | print_import (sym, Code_Thingol.Datatype _) = deresolve_import_attached sym
    1.35 +          | print_import (sym, Code_Thingol.Class _) = deresolve_import_attached sym
    1.36 +          | print_import (sym, Code_Thingol.Classinst _) = NONE;
    1.37          val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
    1.38          fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
    1.39           of (_, NONE) => NONE
    1.40 -          | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
    1.41 -        val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
    1.42 +          | (_, SOME (export, stmt)) =>
    1.43 +              SOME (if export then print_import (sym, stmt) else NONE, markup_stmt sym (print_stmt deresolve (sym, stmt)));
    1.44 +        val (export_ps, body_ps) = (flat o rev o Code_Symbol.Graph.strong_conn) gr
    1.45 +          |> map_filter print_stmt'
    1.46 +          |> split_list
    1.47 +          |> apfst (map_filter I);
    1.48        in
    1.49 -        print_module_frame module_name
    1.50 +        print_module_frame module_name (SOME export_ps)
    1.51            ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
    1.52        end;
    1.53  
    1.54 @@ -399,7 +414,7 @@
    1.55        (fn width => fn destination => K () o map (write_module width destination))
    1.56        (fn present => fn width => rpair (try (deresolver ""))
    1.57          o (map o apsnd) (format present width))
    1.58 -      (map (uncurry print_module_frame o apsnd single) includes
    1.59 +      (map (fn (module_name, content) => print_module_frame module_name NONE [content]) includes
    1.60          @ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
    1.61            ((flat o rev o Graph.strong_conn) haskell_program))
    1.62    end;
     2.1 --- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     2.2 +++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
     2.3 @@ -795,10 +795,10 @@
     2.4        ml_program_of_program ctxt module_name (Name.make_context reserved_syms) identifiers program;
     2.5  
     2.6      (* print statements *)
     2.7 -    fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
     2.8 +    fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
     2.9        tyco_syntax const_syntax (make_vars reserved_syms)
    2.10        (Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt
    2.11 -      |> apfst SOME;
    2.12 +      |> apfst (fn decl => if export then SOME decl else NONE);
    2.13  
    2.14      (* print modules *)
    2.15      fun print_module _ base _ xs =
     3.1 --- a/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     3.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Feb 23 10:33:43 2014 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4  
     3.5    datatype ('a, 'b) node =
     3.6        Dummy
     3.7 -    | Stmt of 'a
     3.8 +    | Stmt of bool * 'a
     3.9      | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T)
    3.10    type ('a, 'b) hierarchical_program
    3.11    val hierarchical_program: Proof.context
    3.12 @@ -32,7 +32,7 @@
    3.13        -> { deresolver: string list -> Code_Symbol.T -> string,
    3.14             hierarchical_program: ('a, 'b) hierarchical_program }
    3.15    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    3.16 -    print_stmt: string list -> Code_Symbol.T * 'a -> 'c,
    3.17 +    print_stmt: string list -> Code_Symbol.T * (bool * 'a) -> 'c,
    3.18      lift_markup: (Pretty.T -> Pretty.T) -> 'c -> 'c }
    3.19        -> ('a, 'b) hierarchical_program -> 'c list
    3.20  end;
    3.21 @@ -82,7 +82,7 @@
    3.22  
    3.23  (** flat program structure **)
    3.24  
    3.25 -type flat_program = ((string * Code_Thingol.stmt option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.26 +type flat_program = ((string * (bool * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.27  
    3.28  fun flat_program ctxt { module_prefix, module_name, reserved,
    3.29      identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    3.30 @@ -102,7 +102,7 @@
    3.31          val (module_name, base) = prep_sym sym;
    3.32        in
    3.33          Graph.default_node (module_name, (Code_Symbol.Graph.empty, []))
    3.34 -        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, stmt)))
    3.35 +        #> (Graph.map_node module_name o apfst) (Code_Symbol.Graph.new_node (sym, (base, (true, stmt))))
    3.36        end;
    3.37      fun add_dep sym sym' =
    3.38        let
    3.39 @@ -116,7 +116,7 @@
    3.40        { empty = Graph.empty, add_stmt = add_stmt, add_dep = add_dep } program;
    3.41  
    3.42      (* name declarations and statement modifications *)
    3.43 -    fun declare sym (base, stmt) (gr, nsp) = 
    3.44 +    fun declare sym (base, (_, stmt)) (gr, nsp) = 
    3.45        let
    3.46          val (base', nsp') = namify_stmt stmt base nsp;
    3.47          val gr' = (Code_Symbol.Graph.map_node sym o apfst) (K base') gr;
    3.48 @@ -125,7 +125,8 @@
    3.49        |> fold (fn sym => declare sym (Code_Symbol.Graph.get_node gr sym))
    3.50            (prioritize sym_priority (Code_Symbol.Graph.keys gr))
    3.51        |> fst
    3.52 -      |> (Code_Symbol.Graph.map o K o apsnd) modify_stmt;
    3.53 +      |> (Code_Symbol.Graph.map o K o apsnd)
    3.54 +        (fn (export, stmt) => Option.map (pair export) (modify_stmt stmt));
    3.55      val flat_program = proto_program
    3.56        |> (Graph.map o K o apfst) declarations;
    3.57  
    3.58 @@ -162,11 +163,13 @@
    3.59  
    3.60  datatype ('a, 'b) node =
    3.61      Dummy
    3.62 -  | Stmt of 'a
    3.63 +  | Stmt of bool * 'a
    3.64    | Module of ('b * (string * ('a, 'b) node) Code_Symbol.Graph.T);
    3.65  
    3.66  type ('a, 'b) hierarchical_program = (string * ('a, 'b) node) Code_Symbol.Graph.T;
    3.67  
    3.68 +fun the_stmt (Stmt (export, stmt)) = (export, stmt);
    3.69 +
    3.70  fun map_module_content f (Module content) = Module (f content);
    3.71  
    3.72  fun map_module [] = I
    3.73 @@ -206,7 +209,7 @@
    3.74        let
    3.75          val (name_fragments, base) = prep_sym sym;
    3.76        in
    3.77 -        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt stmt)))
    3.78 +        (map_module name_fragments o apsnd) (Code_Symbol.Graph.new_node (sym, (base, Stmt (true, stmt))))
    3.79        end;
    3.80      fun add_dep sym sym' =
    3.81        let
    3.82 @@ -244,18 +247,18 @@
    3.83            in (nsps', nodes') end;
    3.84          val (nsps', nodes') = (nsps, nodes)
    3.85            |> fold (declare (K namify_module)) module_fragments
    3.86 -          |> fold (declare (namify_stmt o (fn Stmt stmt => stmt))) stmt_syms;
    3.87 +          |> fold (declare (namify_stmt o snd o the_stmt)) stmt_syms;
    3.88          fun select_syms syms = case filter (member (op =) stmt_syms) syms
    3.89           of [] => NONE
    3.90            | syms => SOME syms;
    3.91 -        fun select_stmt (sym, SOME stmt) = SOME (sym, stmt)
    3.92 +        fun select_stmt (sym, (export, SOME stmt)) = SOME (sym, (export, stmt))
    3.93            | select_stmt _ = NONE;
    3.94          fun modify_stmts' syms =
    3.95            let
    3.96 -            val stmts = map ((fn Stmt stmt => stmt) o snd o Code_Symbol.Graph.get_node nodes) syms;
    3.97 +            val (exports, stmts) = map_split (the_stmt o snd o Code_Symbol.Graph.get_node nodes) syms;
    3.98              val stmts' = modify_stmts (syms ~~ stmts);
    3.99              val stmts'' = stmts' @ replicate (length syms - length stmts') NONE;
   3.100 -          in map_filter select_stmt (syms ~~ stmts'') end;
   3.101 +          in map_filter select_stmt (syms ~~ (exports ~~ stmts'')) end;
   3.102          val stmtss' = (maps modify_stmts' o map_filter select_syms o Code_Symbol.Graph.strong_conn) nodes;
   3.103          val nodes'' = Code_Symbol.Graph.map (fn sym => apsnd (fn Module content => Module (make_declarations nsps' content)
   3.104              | _ => case AList.lookup (op =) stmtss' sym of SOME stmt => Stmt stmt | _ => Dummy)) nodes';
     4.1 --- a/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     4.2 +++ b/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     4.3 @@ -145,26 +145,28 @@
     4.4              |> single
     4.5              |> enclose "(" ")"
     4.6            end;
     4.7 +    fun privatize false = concat o cons (str "private")
     4.8 +      | privatize true = concat;
     4.9      fun print_context tyvars vs sym = applify "[" "]"
    4.10        (fn (v, sort) => (Pretty.block o map str)
    4.11          (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
    4.12            NOBR ((str o deresolve) sym) vs;
    4.13 -    fun print_defhead tyvars vars const vs params tys ty =
    4.14 -      Pretty.block [str "def ", constraint (applify "(" ")" (fn (param, ty) =>
    4.15 +    fun print_defhead export tyvars vars const vs params tys ty =
    4.16 +      privatize export [str "def", constraint (applify "(" ")" (fn (param, ty) =>
    4.17          constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
    4.18            NOBR (print_context tyvars vs (Constant const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
    4.19 -            str " ="];
    4.20 -    fun print_def const (vs, ty) [] =
    4.21 +            str "="];
    4.22 +    fun print_def export const (vs, ty) [] =
    4.23            let
    4.24              val (tys, ty') = Code_Thingol.unfold_fun ty;
    4.25              val params = Name.invent (snd reserved) "a" (length tys);
    4.26              val tyvars = intro_tyvars vs reserved;
    4.27              val vars = intro_vars params reserved;
    4.28            in
    4.29 -            concat [print_defhead tyvars vars const vs params tys ty',
    4.30 +            concat [print_defhead export tyvars vars const vs params tys ty',
    4.31                str ("sys.error(\"" ^ const ^ "\")")]
    4.32            end
    4.33 -      | print_def const (vs, ty) eqs =
    4.34 +      | print_def export const (vs, ty) eqs =
    4.35            let
    4.36              val tycos = fold (fn ((ts, t), _) =>
    4.37                fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
    4.38 @@ -196,7 +198,7 @@
    4.39                    tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
    4.40                    str "=>", print_rhs vars' eq]
    4.41                end;
    4.42 -            val head = print_defhead tyvars vars2 const vs params tys' ty';
    4.43 +            val head = print_defhead export tyvars vars2 const vs params tys' ty';
    4.44            in if simple then
    4.45              concat [head, print_rhs vars2 (hd eqs)]
    4.46            else
    4.47 @@ -206,14 +208,14 @@
    4.48                (map print_clause eqs)
    4.49            end;
    4.50      val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
    4.51 -    fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    4.52 -          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
    4.53 -      | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, cos)) =
    4.54 +    fun print_stmt (Constant const, (export, Code_Thingol.Fun (((vs, ty), raw_eqs), _))) =
    4.55 +          print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
    4.56 +      | print_stmt (Type_Constructor tyco, (export, Code_Thingol.Datatype (vs, cos))) =
    4.57            let
    4.58              val tyvars = intro_tyvars (map (rpair []) vs) reserved;
    4.59              fun print_co ((co, vs_args), tys) =
    4.60                concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
    4.61 -                ((concat o map str) ["final", "case", "class", deresolve_const co]) vs_args)
    4.62 +                ((privatize export o map str) ["final", "case", "class", deresolve_const co]) vs_args)
    4.63                  @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
    4.64                    (Name.invent_names (snd reserved) "a" tys))),
    4.65                  str "extends",
    4.66 @@ -222,10 +224,10 @@
    4.67                ];
    4.68            in
    4.69              Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
    4.70 -              NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    4.71 +              NOBR ((privatize export o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
    4.72                  :: map print_co cos)
    4.73            end
    4.74 -      | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
    4.75 +      | print_stmt (Type_Class class, (export, Code_Thingol.Class (v, (classrels, classparams)))) =
    4.76            let
    4.77              val tyvars = intro_tyvars [(v, [class])] reserved;
    4.78              fun add_typarg s = Pretty.block
    4.79 @@ -244,7 +246,7 @@
    4.80                  val auxs = Name.invent (snd proto_vars) "a" (length tys);
    4.81                  val vars = intro_vars auxs proto_vars;
    4.82                in
    4.83 -                concat [str "def", constraint (Pretty.block [applify "(" ")"
    4.84 +                privatize export [str "def", constraint (Pretty.block [applify "(" ")"
    4.85                    (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
    4.86                    (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
    4.87                    (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
    4.88 @@ -255,14 +257,14 @@
    4.89            in
    4.90              Pretty.chunks (
    4.91                (Pretty.block_enclose
    4.92 -                (concat ([str "trait", (add_typarg o deresolve_class) class]
    4.93 +                (privatize export ([str "trait", (add_typarg o deresolve_class) class]
    4.94                    @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
    4.95                  (map print_classparam_val classparams))
    4.96                :: map print_classparam_def classparams
    4.97              )
    4.98            end
    4.99 -      | print_stmt (sym, Code_Thingol.Classinst
   4.100 -          { class, tyco, vs, inst_params, superinst_params, ... }) =
   4.101 +      | print_stmt (sym, (export, Code_Thingol.Classinst
   4.102 +          { class, tyco, vs, inst_params, superinst_params, ... })) =
   4.103            let
   4.104              val tyvars = intro_tyvars vs reserved;
   4.105              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
   4.106 @@ -279,12 +281,12 @@
   4.107                  val aux_abstr1 = abstract_using aux_dom1;
   4.108                  val aux_abstr2 = abstract_using aux_dom2;
   4.109                in
   4.110 -                concat ([str "val", print_method classparam, str "="]
   4.111 +                privatize export ([str "val", print_method classparam, str "="]
   4.112                    @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
   4.113                      (const, map (IVar o SOME) auxs))
   4.114                end;
   4.115            in
   4.116 -            Pretty.block_enclose (concat [str "implicit def",
   4.117 +            Pretty.block_enclose (privatize export [str "implicit def",
   4.118                constraint (print_context tyvars vs sym) (print_dicttyp tyvars classtyp),
   4.119                str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
   4.120                  (map print_classparam_instance (inst_params @ superinst_params))