explicit option for "open" code generation
authorhaftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 556835732a55b9232
parent 55682 def6575032df
child 55684 ee49b4f7edc8
explicit option for "open" code generation
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.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 @@ -329,13 +329,13 @@
     1.4  ];
     1.5  
     1.6  fun serialize_haskell module_prefix string_classes ctxt { module_name,
     1.7 -    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
     1.8 +    reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } exports program =
     1.9    let
    1.10  
    1.11      (* build program *)
    1.12      val reserved = fold (insert (op =) o fst) includes reserved_syms;
    1.13      val { deresolver, flat_program = haskell_program } = haskell_program_of_program
    1.14 -      ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
    1.15 +      ctxt module_prefix module_name (Name.make_context reserved) identifiers exports program;
    1.16  
    1.17      (* print statements *)
    1.18      fun deriving_show tyco =
     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 @@ -797,13 +797,13 @@
     2.4  
     2.5  fun serialize_ml print_ml_module print_ml_stmt ctxt
     2.6      { module_name, reserved_syms, identifiers, includes,
     2.7 -      class_syntax, tyco_syntax, const_syntax } program =
     2.8 +      class_syntax, tyco_syntax, const_syntax } exports program =
     2.9    let
    2.10  
    2.11      (* build program *)
    2.12      val { deresolver, hierarchical_program = ml_program } =
    2.13        ml_program_of_program ctxt module_name (Name.make_context reserved_syms)
    2.14 -        identifiers program;
    2.15 +        identifiers exports program;
    2.16  
    2.17      (* print statements *)
    2.18      fun print_stmt prefix_fragments (_, (export, stmt)) = print_ml_stmt
     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 @@ -16,7 +16,7 @@
     3.4      reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
     3.5      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
     3.6      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
     3.7 -      -> Code_Thingol.program
     3.8 +      -> Code_Symbol.T list -> Code_Thingol.program
     3.9        -> { deresolver: string -> Code_Symbol.T -> string,
    3.10             flat_program: flat_program }
    3.11  
    3.12 @@ -32,7 +32,7 @@
    3.13      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    3.14      cyclic_modules: bool, empty_data: 'b, memorize_data: Code_Symbol.T -> 'b -> 'b,
    3.15      modify_stmts: (Code_Symbol.T * Code_Thingol.stmt) list -> 'a option list }
    3.16 -      -> Code_Thingol.program
    3.17 +      -> Code_Symbol.T list -> Code_Thingol.program
    3.18        -> { deresolver: string list -> Code_Symbol.T -> string,
    3.19             hierarchical_program: ('a, 'b) hierarchical_program }
    3.20    val print_hierarchical: { print_module: string list -> string -> 'b -> 'c list -> 'c,
    3.21 @@ -101,7 +101,7 @@
    3.22  type flat_program = ((string * (export * Code_Thingol.stmt) option) Code_Symbol.Graph.T * (string * Code_Symbol.T list) list) Graph.T;
    3.23  
    3.24  fun flat_program ctxt { module_prefix, module_name, reserved,
    3.25 -    identifiers, empty_nsp, namify_stmt, modify_stmt } program =
    3.26 +    identifiers, empty_nsp, namify_stmt, modify_stmt } exports program =
    3.27    let
    3.28  
    3.29      (* building module name hierarchy *)
    3.30 @@ -214,7 +214,8 @@
    3.31    end;
    3.32  
    3.33  fun hierarchical_program ctxt { module_name, reserved, identifiers, empty_nsp,
    3.34 -      namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts } program =
    3.35 +      namify_module, namify_stmt, cyclic_modules, empty_data, memorize_data, modify_stmts }
    3.36 +      exports program =
    3.37    let
    3.38  
    3.39      (* building module name hierarchy *)
     4.1 --- a/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
     4.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Feb 23 10:33:43 2014 +0100
     4.3 @@ -199,7 +199,7 @@
     4.4      val program = Code_Thingol.consts_program thy consts;
     4.5      val (ml_modules, target_names) =
     4.6        Code_Target.produce_code_for thy
     4.7 -        target NONE module_name [] program (map Constant consts @ map Type_Constructor tycos);
     4.8 +        target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos);
     4.9      val ml_code = space_implode "\n\n" (map snd ml_modules);
    4.10      val (consts', tycos') = chop (length consts) target_names;
    4.11      val consts_map = map2 (fn const =>
    4.12 @@ -440,7 +440,7 @@
    4.13    |-> (fn ([Const (const, _)], _) =>
    4.14      Code_Target.set_printings (Constant (const,
    4.15        [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
    4.16 -  #> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated []));
    4.17 +  #> tap (fn thy => Code_Target.produce_code thy false [const] target NONE structure_generated []));
    4.18  
    4.19  fun process_file filepath (definienda, thy) =
    4.20    let
     5.1 --- a/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     5.2 +++ b/src/Tools/Code/code_scala.ML	Sun Feb 23 10:33:43 2014 +0100
     5.3 @@ -296,7 +296,7 @@
     5.4            end;
     5.5    in print_stmt end;
     5.6  
     5.7 -fun scala_program_of_program ctxt module_name reserved identifiers program =
     5.8 +fun scala_program_of_program ctxt module_name reserved identifiers exports program =
     5.9    let
    5.10      fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
    5.11        let
    5.12 @@ -343,17 +343,17 @@
    5.13        { module_name = module_name, reserved = reserved, identifiers = identifiers,
    5.14          empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
    5.15          namify_stmt = namify_stmt, cyclic_modules = true, empty_data = [],
    5.16 -        memorize_data = memorize_implicits, modify_stmts = map modify_stmt } program
    5.17 +        memorize_data = memorize_implicits, modify_stmts = map modify_stmt } exports program
    5.18    end;
    5.19  
    5.20  fun serialize_scala ctxt { module_name, reserved_syms, identifiers,
    5.21 -    includes, class_syntax, tyco_syntax, const_syntax } program =
    5.22 +    includes, class_syntax, tyco_syntax, const_syntax } exports program =
    5.23    let
    5.24  
    5.25      (* build program *)
    5.26      val { deresolver, hierarchical_program = scala_program } =
    5.27        scala_program_of_program ctxt module_name (Name.make_context reserved_syms)
    5.28 -        identifiers program;
    5.29 +        identifiers exports program;
    5.30  
    5.31      (* print statements *)
    5.32      fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
     6.1 --- a/src/Tools/Code/code_target.ML	Sun Feb 23 10:33:43 2014 +0100
     6.2 +++ b/src/Tools/Code/code_target.ML	Sun Feb 23 10:33:43 2014 +0100
     6.3 @@ -10,21 +10,21 @@
     6.4    val read_tyco: theory -> string -> string
     6.5  
     6.6    val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
     6.7 -    -> Code_Thingol.program -> Code_Symbol.T list -> unit
     6.8 +    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
     6.9    val produce_code_for: theory -> string -> int option -> string -> Token.T list
    6.10 -    -> Code_Thingol.program -> Code_Symbol.T list -> (string * string) list * string option list
    6.11 +    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
    6.12    val present_code_for: theory -> string -> int option -> string -> Token.T list
    6.13      -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
    6.14    val check_code_for: theory -> string -> bool -> Token.T list
    6.15 -    -> Code_Thingol.program -> Code_Symbol.T list -> unit
    6.16 +    -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
    6.17  
    6.18 -  val export_code: theory -> string list
    6.19 +  val export_code: theory -> bool -> string list
    6.20      -> (((string * string) * Path.T option) * Token.T list) list -> unit
    6.21 -  val produce_code: theory -> string list
    6.22 +  val produce_code: theory -> bool -> string list
    6.23      -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
    6.24    val present_code: theory -> string list -> Code_Symbol.T list
    6.25      -> string -> int option -> string -> Token.T list -> string
    6.26 -  val check_code: theory -> string list
    6.27 +  val check_code: theory -> bool -> string list
    6.28      -> ((string * bool) * Token.T list) list -> unit
    6.29  
    6.30    val generatedN: string
    6.31 @@ -177,6 +177,7 @@
    6.32      class_syntax: string -> string option,
    6.33      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    6.34      const_syntax: string -> Code_Printer.const_syntax option }
    6.35 +  -> Code_Symbol.T list
    6.36    -> Code_Thingol.program
    6.37    -> serialization;
    6.38  
    6.39 @@ -351,7 +352,7 @@
    6.40        const_syntax = Code_Symbol.lookup_constant_data printings,
    6.41        tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
    6.42        class_syntax = Code_Symbol.lookup_type_class_data printings },
    6.43 -      program)
    6.44 +      (syms_all, program))
    6.45    end;
    6.46  
    6.47  fun mount_serializer thy target some_width module_name args program syms =
    6.48 @@ -359,20 +360,20 @@
    6.49      val (default_width, data, modify) = activate_target thy target;
    6.50      val serializer = case the_description data
    6.51       of Fundamental seri => #serializer seri;
    6.52 -    val (prepared_serializer, prepared_program) =
    6.53 +    val (prepared_serializer, (prepared_syms, prepared_program)) =
    6.54        prepare_serializer thy serializer
    6.55          (the_reserved data) (the_identifiers data) (the_printings data)
    6.56          module_name args (modify program) syms
    6.57      val width = the_default default_width some_width;
    6.58 -  in (fn program => prepared_serializer program width, prepared_program) end;
    6.59 +  in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
    6.60  
    6.61 -fun invoke_serializer thy target some_width raw_module_name args program syms =
    6.62 +fun invoke_serializer thy target some_width raw_module_name args program all_public syms =
    6.63    let
    6.64      val module_name = if raw_module_name = "" then ""
    6.65        else (check_name true raw_module_name; raw_module_name)
    6.66 -    val (mounted_serializer, prepared_program) = mount_serializer thy
    6.67 +    val (mounted_serializer, (prepared_syms, prepared_program)) = mount_serializer thy
    6.68        target some_width module_name args program syms;
    6.69 -  in mounted_serializer prepared_program end;
    6.70 +  in mounted_serializer prepared_program (if all_public then prepared_syms else []) end;
    6.71  
    6.72  fun assert_module_name "" = error "Empty module name not allowed here"
    6.73    | assert_module_name module_name = module_name;
    6.74 @@ -386,23 +387,23 @@
    6.75  
    6.76  fun export_code_for thy some_path target some_width module_name args =
    6.77    export (using_master_directory thy some_path)
    6.78 -  oo invoke_serializer thy target some_width module_name args;
    6.79 +  ooo invoke_serializer thy target some_width module_name args;
    6.80  
    6.81  fun produce_code_for thy target some_width module_name args =
    6.82    let
    6.83      val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
    6.84 -  in fn program => fn syms =>
    6.85 -    produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms)
    6.86 +  in fn program => fn all_public => fn syms =>
    6.87 +    produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
    6.88    end;
    6.89  
    6.90  fun present_code_for thy target some_width module_name args =
    6.91    let
    6.92      val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
    6.93    in fn program => fn (syms, selects) =>
    6.94 -    present selects (serializer program syms)
    6.95 +    present selects (serializer program false syms)
    6.96    end;
    6.97  
    6.98 -fun check_code_for thy target strict args program syms =
    6.99 +fun check_code_for thy target strict args program all_public syms =
   6.100    let
   6.101      val { env_var, make_destination, make_command } =
   6.102        (#check o the_fundamental thy) target;
   6.103 @@ -410,7 +411,7 @@
   6.104        let
   6.105          val destination = make_destination p;
   6.106          val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
   6.107 -          generatedN args program syms);
   6.108 +          generatedN args program all_public syms);
   6.109          val cmd = make_command generatedN;
   6.110        in
   6.111          if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
   6.112 @@ -437,13 +438,14 @@
   6.113            Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))
   6.114        |> fold (curry (perhaps o try o
   6.115            Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
   6.116 -    val (program_code, deresolve) = produce (mounted_serializer program);
   6.117 +    val (program_code, deresolve) =
   6.118 +      produce (mounted_serializer program [Code_Symbol.value]);
   6.119      val value_name = the (deresolve Code_Symbol.value);
   6.120    in (program_code, value_name) end;
   6.121  
   6.122  fun evaluator thy target program syms =
   6.123    let
   6.124 -    val (mounted_serializer, prepared_program) =
   6.125 +    val (mounted_serializer, (_, prepared_program)) =
   6.126        mount_serializer thy target NONE generatedN [] program syms;
   6.127    in evaluation mounted_serializer prepared_program syms end;
   6.128  
   6.129 @@ -455,36 +457,38 @@
   6.130  fun prep_destination "" = NONE
   6.131    | prep_destination s = SOME (Path.explode s);
   6.132  
   6.133 -fun export_code thy cs seris =
   6.134 +fun export_code thy all_public cs seris =
   6.135    let
   6.136      val program = Code_Thingol.consts_program thy cs;
   6.137      val _ = map (fn (((target, module_name), some_path), args) =>
   6.138 -      export_code_for thy some_path target NONE module_name args program (map Constant cs)) seris;
   6.139 +      export_code_for thy some_path target NONE module_name args program all_public (map Constant cs)) seris;
   6.140    in () end;
   6.141  
   6.142 -fun export_code_cmd raw_cs seris thy = export_code thy
   6.143 -  (Code_Thingol.read_const_exprs thy raw_cs)
   6.144 -  ((map o apfst o apsnd) prep_destination seris);
   6.145 +fun export_code_cmd all_public raw_cs seris thy =
   6.146 +  export_code thy all_public
   6.147 +    (Code_Thingol.read_const_exprs thy raw_cs)
   6.148 +    ((map o apfst o apsnd) prep_destination seris);
   6.149  
   6.150 -fun produce_code thy cs target some_width some_module_name args =
   6.151 +fun produce_code thy all_public cs target some_width some_module_name args =
   6.152    let
   6.153      val program = Code_Thingol.consts_program thy cs;
   6.154 -  in produce_code_for thy target some_width some_module_name args program (map Constant cs) end;
   6.155 +  in produce_code_for thy target some_width some_module_name args program all_public (map Constant cs) end;
   6.156  
   6.157  fun present_code thy cs syms target some_width some_module_name args =
   6.158    let
   6.159      val program = Code_Thingol.consts_program thy cs;
   6.160    in present_code_for thy target some_width some_module_name args program (map Constant cs, syms) end;
   6.161  
   6.162 -fun check_code thy cs seris =
   6.163 +fun check_code thy all_public cs seris =
   6.164    let
   6.165      val program = Code_Thingol.consts_program thy cs;
   6.166      val _ = map (fn ((target, strict), args) =>
   6.167 -      check_code_for thy target strict args program (map Constant cs)) seris;
   6.168 +      check_code_for thy target strict args program all_public (map Constant cs)) seris;
   6.169    in () end;
   6.170  
   6.171 -fun check_code_cmd raw_cs seris thy = check_code thy
   6.172 -  (Code_Thingol.read_const_exprs thy raw_cs) seris;
   6.173 +fun check_code_cmd all_public raw_cs seris thy =
   6.174 +  check_code thy all_public
   6.175 +    (Code_Thingol.read_const_exprs thy raw_cs) seris;
   6.176  
   6.177  local
   6.178  
   6.179 @@ -639,21 +643,22 @@
   6.180  
   6.181  val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) [];
   6.182  
   6.183 -fun code_expr_inP raw_cs =
   6.184 +fun code_expr_inP all_public raw_cs =
   6.185    Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
   6.186      -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
   6.187      -- Scan.optional (@{keyword "file"} |-- Parse.name) ""
   6.188      -- code_expr_argsP))
   6.189 -      >> (fn seri_args => export_code_cmd raw_cs seri_args);
   6.190 +      >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
   6.191  
   6.192 -fun code_expr_checkingP raw_cs =
   6.193 +fun code_expr_checkingP all_public raw_cs =
   6.194    (@{keyword "checking"} |-- Parse.!!!
   6.195      (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true)
   6.196      -- code_expr_argsP)))
   6.197 -      >> (fn seri_args => check_code_cmd raw_cs seri_args);
   6.198 +      >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
   6.199  
   6.200 -val code_exprP = Scan.repeat1 Parse.term
   6.201 -  :|-- (fn raw_cs => (code_expr_checkingP raw_cs || code_expr_inP raw_cs));
   6.202 +val code_exprP = (Scan.optional (@{keyword "open"} |-- Scan.succeed true) false
   6.203 +  -- Scan.repeat1 Parse.term)
   6.204 +  :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
   6.205  
   6.206  val _ =
   6.207    Outer_Syntax.command @{command_spec "code_reserved"}