1.1 --- a/src/Tools/Code/code_target.ML Tue Sep 03 15:24:39 2019 +0200
1.2 +++ b/src/Tools/Code/code_target.ML Tue Sep 03 16:10:31 2019 +0200
1.3 @@ -9,31 +9,43 @@
1.4 val cert_tyco: Proof.context -> string -> string
1.5 val read_tyco: Proof.context -> string -> string
1.6
1.7 - val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list
1.8 - -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
1.9 - val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list
1.10 - -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list
1.11 - val present_code_for: Proof.context -> string -> int option -> string -> Token.T list
1.12 + datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
1.13 + val next_export: theory -> string * theory
1.14 +
1.15 + val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string
1.16 + -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list
1.17 + -> local_theory -> local_theory
1.18 + val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
1.19 + -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
1.20 + val present_code_for: Proof.context -> string -> string -> int option -> Token.T list
1.21 -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string
1.22 - val check_code_for: Proof.context -> string -> bool -> Token.T list
1.23 - -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit
1.24 + val check_code_for: string -> bool -> Token.T list
1.25 + -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
1.26
1.27 - val export_code: Proof.context -> bool -> string list
1.28 - -> (((string * string) * Path.T option) * Token.T list) list -> unit
1.29 + val export_code: bool -> string list
1.30 + -> (((string * string) * ({physical: bool} * (Path.T * Position.T)) option) * Token.T list) list
1.31 + -> local_theory -> local_theory
1.32 + val export_code_cmd: bool -> string list
1.33 + -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list
1.34 + -> local_theory -> local_theory
1.35 val produce_code: Proof.context -> bool -> string list
1.36 - -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
1.37 + -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
1.38 val present_code: Proof.context -> string list -> Code_Symbol.T list
1.39 - -> string -> int option -> string -> Token.T list -> string
1.40 - val check_code: Proof.context -> bool -> string list
1.41 - -> ((string * bool) * Token.T list) list -> unit
1.42 + -> string -> string -> int option -> Token.T list -> string
1.43 + val check_code: bool -> string list -> ((string * bool) * Token.T list) list
1.44 + -> local_theory -> local_theory
1.45
1.46 + val codeN: string
1.47 val generatedN: string
1.48 + val code_path: Path.T -> Path.T
1.49 + val code_export_message: theory -> unit
1.50 + val export: Path.binding -> string -> theory -> theory
1.51 val compilation_text: Proof.context -> string -> Code_Thingol.program
1.52 -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
1.53 - -> (string * string) list * string
1.54 + -> (string list * string) list * string
1.55 val compilation_text': Proof.context -> string -> string option -> Code_Thingol.program
1.56 -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
1.57 - -> ((string * string) list * string) * (Code_Symbol.T -> string option)
1.58 + -> ((string list * string) list * string) * (Code_Symbol.T -> string option)
1.59
1.60 type serializer
1.61 type literals = Code_Printer.literals
1.62 @@ -43,17 +55,13 @@
1.63 val add_language: string * language -> theory -> theory
1.64 val add_derived_target: string * ancestry -> theory -> theory
1.65 val the_literals: Proof.context -> string -> literals
1.66 - type serialization
1.67 val parse_args: 'a parser -> Token.T list -> 'a
1.68 - val serialization: (int -> Path.T option -> 'a -> unit)
1.69 - -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option))
1.70 - -> 'a -> serialization
1.71 val default_code_width: int Config.T
1.72
1.73 type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
1.74 val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
1.75 -> theory -> theory
1.76 - val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
1.77 + val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, string * Code_Symbol.T list) symbol_attr_decl
1.78 -> theory -> theory
1.79 val add_reserved: string -> string -> theory -> theory
1.80 end;
1.81 @@ -99,7 +107,7 @@
1.82 val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class;
1.83 in class end;
1.84
1.85 -val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class;
1.86 +val parse_classrel_ident = Parse.class --| \<^keyword>\<open><\<close> -- Parse.class;
1.87
1.88 fun cert_inst ctxt (class, tyco) =
1.89 (cert_class ctxt class, cert_tyco ctxt tyco);
1.90 @@ -107,13 +115,21 @@
1.91 fun read_inst ctxt (raw_tyco, raw_class) =
1.92 (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class);
1.93
1.94 -val parse_inst_ident = Parse.name --| @{keyword "::"} -- Parse.class;
1.95 +val parse_inst_ident = Parse.name --| \<^keyword>\<open>::\<close> -- Parse.class;
1.96
1.97 fun cert_syms ctxt =
1.98 + Code_Symbol.map_attr (cert_const ctxt) (cert_tyco ctxt)
1.99 + (cert_class ctxt) (apply2 (cert_class ctxt)) (cert_inst ctxt) I;
1.100 +
1.101 +fun read_syms ctxt =
1.102 + Code_Symbol.map_attr (read_const ctxt) (read_tyco ctxt)
1.103 + (Proof_Context.read_class ctxt) (apply2 (Proof_Context.read_class ctxt)) (read_inst ctxt) I;
1.104 +
1.105 +fun cert_syms' ctxt =
1.106 Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt))
1.107 (apfst (cert_class ctxt)) ((apfst o apply2) (cert_class ctxt)) (apfst (cert_inst ctxt)) I;
1.108
1.109 -fun read_syms ctxt =
1.110 +fun read_syms' ctxt =
1.111 Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt))
1.112 (apfst (Proof_Context.read_class ctxt)) ((apfst o apply2) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I;
1.113
1.114 @@ -138,49 +154,27 @@
1.115 end;
1.116
1.117
1.118 -(** serializations and serializer **)
1.119 +(** theory data **)
1.120
1.121 -(* serialization: abstract nonsense to cover different destinies for generated code *)
1.122 -
1.123 -datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list;
1.124 -type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option;
1.125 -
1.126 -fun serialization output _ content width (Export some_path) =
1.127 - (output width some_path content; NONE)
1.128 - | serialization _ string content width Produce =
1.129 - string [] width content |> SOME
1.130 - | serialization _ string content width (Present syms) =
1.131 - string syms width content
1.132 - |> (apfst o map o apsnd) Output.output
1.133 - |> SOME;
1.134 -
1.135 -fun export some_path f = (f (Export some_path); ());
1.136 -fun produce f = the (f Produce);
1.137 -fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms)))));
1.138 -
1.139 -
1.140 -(* serializers: functions producing serializations *)
1.141 +datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
1.142
1.143 type serializer = Token.T list
1.144 -> Proof.context
1.145 -> {
1.146 - module_name: string,
1.147 reserved_syms: string list,
1.148 identifiers: Code_Printer.identifiers,
1.149 includes: (string * Pretty.T) list,
1.150 class_syntax: string -> string option,
1.151 tyco_syntax: string -> Code_Printer.tyco_syntax option,
1.152 - const_syntax: string -> Code_Printer.const_syntax option }
1.153 + const_syntax: string -> Code_Printer.const_syntax option,
1.154 + module_name: string }
1.155 + -> Code_Thingol.program
1.156 -> Code_Symbol.T list
1.157 - -> Code_Thingol.program
1.158 - -> serialization;
1.159 -
1.160 -
1.161 -(** theory data **)
1.162 + -> pretty_modules * (Code_Symbol.T -> string option);
1.163
1.164 type language = {serializer: serializer, literals: literals,
1.165 check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
1.166 - evaluation_args: Token.T list};
1.167 + evaluation_args: Token.T list};
1.168
1.169 type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
1.170
1.171 @@ -190,31 +184,38 @@
1.172
1.173 structure Targets = Theory_Data
1.174 (
1.175 - type T = (target * Code_Printer.data) Symtab.table;
1.176 - val empty = Symtab.empty;
1.177 - val extend = I;
1.178 - fun merge (targets1, targets2) : T =
1.179 - Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
1.180 - if #serial target1 = #serial target2 then
1.181 - ({serial = #serial target1, language = #language target1,
1.182 - ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
1.183 - Code_Printer.merge_data (data1, data2))
1.184 - else error ("Incompatible targets: " ^ quote target_name)
1.185 - ) (targets1, targets2)
1.186 + type T = (target * Code_Printer.data) Symtab.table * int;
1.187 + val empty = (Symtab.empty, 0);
1.188 + fun extend (targets, _) = (targets, 0);
1.189 + fun merge ((targets1, _), (targets2, _)) : T =
1.190 + let val targets' =
1.191 + Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
1.192 + if #serial target1 = #serial target2 then
1.193 + ({serial = #serial target1, language = #language target1,
1.194 + ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
1.195 + Code_Printer.merge_data (data1, data2))
1.196 + else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2)
1.197 + in (targets', 0) end;
1.198 );
1.199
1.200 -fun exists_target thy = Symtab.defined (Targets.get thy);
1.201 -fun lookup_target_data thy = Symtab.lookup (Targets.get thy);
1.202 +val exists_target = Symtab.defined o #1 o Targets.get;
1.203 +val lookup_target_data = Symtab.lookup o #1 o Targets.get;
1.204 fun assert_target thy target_name =
1.205 if exists_target thy target_name
1.206 then target_name
1.207 else error ("Unknown code target language: " ^ quote target_name);
1.208
1.209 +fun next_export thy =
1.210 + let
1.211 + val thy' = (Targets.map o apsnd) (fn i => i + 1) thy;
1.212 + val i = #2 (Targets.get thy');
1.213 + in ("export" ^ string_of_int i, thy') end;
1.214 +
1.215 fun fold1 f xs = fold f (tl xs) (hd xs);
1.216
1.217 fun join_ancestry thy target_name =
1.218 let
1.219 - val _ = assert_target thy target_name;
1.220 + val _ = assert_target thy target_name;
1.221 val the_target_data = the o lookup_target_data thy;
1.222 val (target, this_data) = the_target_data target_name;
1.223 val ancestry = #ancestry target;
1.224 @@ -224,14 +225,14 @@
1.225 val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
1.226 in (modify, (target, data)) end;
1.227
1.228 - fun allocate_target target_name target thy =
1.229 +fun allocate_target target_name target thy =
1.230 let
1.231 val _ = if exists_target thy target_name
1.232 then error ("Attempt to overwrite existing target " ^ quote target_name)
1.233 else ();
1.234 in
1.235 thy
1.236 - |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))
1.237 + |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))
1.238 end;
1.239
1.240 fun add_language (target_name, language) =
1.241 @@ -254,30 +255,102 @@
1.242 merge_ancestry (ancestry, ancestry')) ancestries;
1.243 in
1.244 allocate_target target_name {serial = #serial supremum, language = #language supremum,
1.245 - ancestry = ancestry} thy
1.246 + ancestry = ancestry} thy
1.247 end;
1.248 -
1.249 +
1.250 fun map_data target_name f thy =
1.251 let
1.252 val _ = assert_target thy target_name;
1.253 in
1.254 thy
1.255 - |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
1.256 + |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
1.257 end;
1.258
1.259 -fun map_reserved target_name =
1.260 - map_data target_name o @{apply 3 (1)};
1.261 -fun map_identifiers target_name =
1.262 - map_data target_name o @{apply 3 (2)};
1.263 -fun map_printings target_name =
1.264 - map_data target_name o @{apply 3 (3)};
1.265 +fun map_reserved target_name = map_data target_name o @{apply 3(1)};
1.266 +fun map_identifiers target_name = map_data target_name o @{apply 3(2)};
1.267 +fun map_printings target_name = map_data target_name o @{apply 3(3)};
1.268 +
1.269 +
1.270 +(** serializers **)
1.271 +
1.272 +val codeN = "code";
1.273 +val generatedN = "Generated_Code";
1.274 +
1.275 +val code_path = Path.append (Path.basic codeN);
1.276 +fun code_export_message thy = writeln (Export.message thy (Path.basic codeN));
1.277 +
1.278 +fun export binding content thy =
1.279 + let
1.280 + val thy' = thy |> Generated_Files.add_files (binding, content);
1.281 + val _ = Export.export thy' binding [content];
1.282 + in thy' end;
1.283 +
1.284 +local
1.285 +
1.286 +fun export_logical (file_prefix, file_pos) format pretty_modules =
1.287 + let
1.288 + fun binding path = Path.binding (path, file_pos);
1.289 + val prefix = code_path file_prefix;
1.290 + in
1.291 + (case pretty_modules of
1.292 + Singleton (ext, p) => export (binding (Path.ext ext prefix)) (format p)
1.293 + | Hierarchy modules =>
1.294 + fold (fn (names, p) =>
1.295 + export (binding (Path.append prefix (Path.make names))) (format p)) modules)
1.296 + #> tap code_export_message
1.297 + end;
1.298 +
1.299 +fun export_physical root format pretty_modules =
1.300 + (case pretty_modules of
1.301 + Singleton (_, p) => File.write root (format p)
1.302 + | Hierarchy code_modules =>
1.303 + (Isabelle_System.mkdirs root;
1.304 + List.app (fn (names, p) =>
1.305 + File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
1.306 +
1.307 +in
1.308 +
1.309 +fun export_result some_file format (pretty_code, _) thy =
1.310 + (case some_file of
1.311 + NONE =>
1.312 + let val (file_prefix, thy') = next_export thy;
1.313 + in export_logical (Path.basic file_prefix, Position.none) format pretty_code thy' end
1.314 + | SOME ({physical = false}, file_prefix) =>
1.315 + export_logical file_prefix format pretty_code thy
1.316 + | SOME ({physical = true}, (file, _)) =>
1.317 + let
1.318 + val root = File.full_path (Resources.master_directory thy) file;
1.319 + val _ = File.check_dir (Path.dir root);
1.320 + val _ = export_physical root format pretty_code;
1.321 + in thy end);
1.322 +
1.323 +fun produce_result syms width pretty_modules =
1.324 + let val format = Code_Printer.format [] width in
1.325 + (case pretty_modules of
1.326 + (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms)
1.327 + | (Hierarchy code_modules, deresolve) =>
1.328 + ((map o apsnd) format code_modules, map deresolve syms))
1.329 + end;
1.330 +
1.331 +fun present_result selects width (pretty_modules, _) =
1.332 + let val format = Code_Printer.format selects width in
1.333 + (case pretty_modules of
1.334 + Singleton (_, p) => format p
1.335 + | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
1.336 + end;
1.337 +
1.338 +end;
1.339
1.340
1.341 (** serializer usage **)
1.342
1.343 (* technical aside: pretty printing width *)
1.344
1.345 -val default_code_width = Attrib.setup_config_int @{binding "default_code_width"} (K 80);
1.346 +val default_code_width = Attrib.setup_config_int \<^binding>\<open>default_code_width\<close> (K 80);
1.347 +
1.348 +fun default_width ctxt = Config.get ctxt default_code_width;
1.349 +
1.350 +val the_width = the_default o default_width;
1.351
1.352
1.353 (* montage *)
1.354 @@ -294,119 +367,116 @@
1.355 fun activate_target ctxt target_name =
1.356 let
1.357 val thy = Proof_Context.theory_of ctxt;
1.358 - val (modify, target_data) = join_ancestry thy target_name;
1.359 - in (target_data, modify) end;
1.360 + val (modify, (target, data)) = join_ancestry thy target_name;
1.361 + val serializer = (#serializer o #language) target;
1.362 + in { serializer = serializer, data = data, modify = modify } end;
1.363
1.364 -fun project_program ctxt syms_hidden syms1 program2 =
1.365 +fun project_program_for_syms ctxt syms_hidden syms1 program1 =
1.366 let
1.367 val syms2 = subtract (op =) syms_hidden syms1;
1.368 - val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2;
1.369 - val syms4 = Code_Symbol.Graph.all_succs program3 syms2;
1.370 - val unimplemented = Code_Thingol.unimplemented program3;
1.371 + val program2 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program1;
1.372 + val unimplemented = Code_Thingol.unimplemented program2;
1.373 val _ =
1.374 if null unimplemented then ()
1.375 else error ("No code equations for " ^
1.376 commas (map (Proof_Context.markup_const ctxt) unimplemented));
1.377 - val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3;
1.378 - in (syms4, program4) end;
1.379 + val syms3 = Code_Symbol.Graph.all_succs program2 syms2;
1.380 + val program3 = Code_Symbol.Graph.restrict (member (op =) syms3) program2;
1.381 + in program3 end;
1.382
1.383 -fun prepare_serializer ctxt (serializer : serializer) reserved identifiers
1.384 - printings module_name args proto_program syms =
1.385 +fun project_includes_for_syms syms includes =
1.386 + let
1.387 + fun select_include (name, (content, cs)) =
1.388 + if null cs orelse exists (member (op =) syms) cs
1.389 + then SOME (name, content) else NONE;
1.390 + in map_filter select_include includes end;
1.391 +
1.392 +fun prepare_serializer ctxt target_name module_name args proto_program syms =
1.393 let
1.394 - val syms_hidden = Code_Symbol.symbols_of printings;
1.395 - val (syms_all, program) = project_program ctxt syms_hidden syms proto_program;
1.396 - fun select_include (name, (content, cs)) =
1.397 - if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs
1.398 - then SOME (name, content) else NONE;
1.399 - val includes = map_filter select_include (Code_Symbol.dest_module_data printings);
1.400 - in
1.401 - (serializer args ctxt {
1.402 - module_name = module_name,
1.403 - reserved_syms = reserved,
1.404 - identifiers = identifiers,
1.405 + val { serializer, data, modify } = activate_target ctxt target_name;
1.406 + val printings = Code_Printer.the_printings data;
1.407 + val _ = if module_name = "" then () else (check_name true module_name; ())
1.408 + val hidden_syms = Code_Symbol.symbols_of printings;
1.409 + val prepared_program = project_program_for_syms ctxt hidden_syms syms proto_program;
1.410 + val prepared_syms = subtract (op =) hidden_syms syms;
1.411 + val all_syms = Code_Symbol.Graph.all_succs proto_program syms;
1.412 + val includes = project_includes_for_syms all_syms
1.413 + (Code_Symbol.dest_module_data printings);
1.414 + val prepared_serializer = serializer args ctxt {
1.415 + reserved_syms = Code_Printer.the_reserved data,
1.416 + identifiers = Code_Printer.the_identifiers data,
1.417 includes = includes,
1.418 const_syntax = Code_Symbol.lookup_constant_data printings,
1.419 tyco_syntax = Code_Symbol.lookup_type_constructor_data printings,
1.420 - class_syntax = Code_Symbol.lookup_type_class_data printings },
1.421 - (subtract (op =) syms_hidden syms, program))
1.422 + class_syntax = Code_Symbol.lookup_type_class_data printings,
1.423 + module_name = module_name };
1.424 + in
1.425 + (prepared_serializer o modify, (prepared_program, prepared_syms))
1.426 end;
1.427
1.428 -fun mount_serializer ctxt target_name some_width module_name args program syms =
1.429 +fun invoke_serializer ctxt target_name module_name args program all_public syms =
1.430 let
1.431 - val default_width = Config.get ctxt default_code_width;
1.432 - val ((target, data), modify) = activate_target ctxt target_name;
1.433 - val serializer = (#serializer o #language) target;
1.434 - val (prepared_serializer, (prepared_syms, prepared_program)) =
1.435 - prepare_serializer ctxt serializer
1.436 - (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
1.437 - (Code_Printer.the_printings data)
1.438 - module_name args (modify program) syms
1.439 - val width = the_default default_width some_width;
1.440 - in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
1.441 -
1.442 -fun invoke_serializer ctxt target_name some_width raw_module_name args program all_public syms =
1.443 - let
1.444 - val module_name = if raw_module_name = "" then ""
1.445 - else (check_name true raw_module_name; raw_module_name)
1.446 - val (mounted_serializer, (prepared_syms, prepared_program)) =
1.447 - mount_serializer ctxt target_name some_width module_name args program syms;
1.448 + val (prepared_serializer, (prepared_program, prepared_syms)) =
1.449 + prepare_serializer ctxt target_name module_name args program syms;
1.450 + val exports = if all_public then [] else prepared_syms;
1.451 in
1.452 Code_Preproc.timed_exec "serializing"
1.453 - (fn () => mounted_serializer prepared_program (if all_public then [] else prepared_syms)) ctxt
1.454 + (fn () => prepared_serializer prepared_program exports) ctxt
1.455 end;
1.456
1.457 fun assert_module_name "" = error "Empty module name not allowed here"
1.458 | assert_module_name module_name = module_name;
1.459
1.460 -val using_master_directory =
1.461 - Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
1.462 -
1.463 in
1.464
1.465 -val generatedN = "Generated_Code";
1.466 +fun export_code_for some_file target_name module_name some_width args program all_public cs lthy =
1.467 + let
1.468 + val format = Code_Printer.format [] (the_width lthy some_width);
1.469 + val res = invoke_serializer lthy target_name module_name args program all_public cs;
1.470 + in Local_Theory.background_theory (export_result some_file format res) lthy end;
1.471
1.472 -fun export_code_for ctxt some_path target_name some_width module_name args =
1.473 - export (using_master_directory ctxt some_path)
1.474 - ooo invoke_serializer ctxt target_name some_width module_name args;
1.475 -
1.476 -fun produce_code_for ctxt target_name some_width module_name args =
1.477 +fun produce_code_for ctxt target_name module_name some_width args =
1.478 let
1.479 - val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
1.480 + val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
1.481 in fn program => fn all_public => fn syms =>
1.482 - produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms)
1.483 + produce_result syms (the_width ctxt some_width)
1.484 + (serializer program all_public syms)
1.485 end;
1.486
1.487 -fun present_code_for ctxt target_name some_width module_name args =
1.488 +fun present_code_for ctxt target_name module_name some_width args =
1.489 let
1.490 - val serializer = invoke_serializer ctxt target_name some_width (assert_module_name module_name) args;
1.491 + val serializer = invoke_serializer ctxt target_name (assert_module_name module_name) args;
1.492 in fn program => fn (syms, selects) =>
1.493 - present selects (serializer program false syms)
1.494 + present_result selects (the_width ctxt some_width) (serializer program false syms)
1.495 end;
1.496
1.497 -fun check_code_for ctxt target_name strict args program all_public syms =
1.498 +fun check_code_for target_name strict args program all_public syms lthy =
1.499 let
1.500 - val { env_var, make_destination, make_command } =
1.501 - (#check o the_language ctxt) target_name;
1.502 + val { env_var, make_destination, make_command } = #check (the_language lthy target_name);
1.503 + val format = Code_Printer.format [] 80;
1.504 fun ext_check p =
1.505 let
1.506 val destination = make_destination p;
1.507 - val _ = export (SOME destination) (invoke_serializer ctxt target_name (SOME 80)
1.508 - generatedN args program all_public syms);
1.509 + val lthy' = lthy
1.510 + |> Local_Theory.background_theory
1.511 + (export_result (SOME ({physical = true}, (destination, Position.none))) format
1.512 + (invoke_serializer lthy target_name generatedN args program all_public syms));
1.513 val cmd = make_command generatedN;
1.514 + val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
1.515 in
1.516 - if Isabelle_System.bash ("cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
1.517 + if Isabelle_System.bash context_cmd <> 0
1.518 then error ("Code check failed for " ^ target_name ^ ": " ^ cmd)
1.519 - else ()
1.520 + else lthy'
1.521 end;
1.522 in
1.523 - if not (env_var = "") andalso getenv env_var = ""
1.524 - then if strict
1.525 + if not (env_var = "") andalso getenv env_var = "" then
1.526 + if strict
1.527 then error (env_var ^ " not set; cannot check code for " ^ target_name)
1.528 - else warning (env_var ^ " not set; skipped checking code for " ^ target_name)
1.529 + else (warning (env_var ^ " not set; skipped checking code for " ^ target_name); lthy)
1.530 else Isabelle_System.with_tmp_dir "Code_Test" ext_check
1.531 end;
1.532
1.533 -fun dynamic_compilation_text mounted_serializer prepared_program syms all_public ((vs, ty), t) =
1.534 +fun dynamic_compilation_text prepared_serializer width prepared_program syms all_public ((vs, ty), t) =
1.535 let
1.536 val _ = if Code_Thingol.contains_dict_var t then
1.537 error "Term to be evaluated contains free dictionaries" else ();
1.538 @@ -418,49 +488,62 @@
1.539 Code_Thingol.Fun (((vs', ty'), [(([IVar (SOME "dummy")], t), (NONE, true))]), NONE))
1.540 |> fold (curry (perhaps o try o
1.541 Code_Symbol.Graph.add_edge) Code_Symbol.value) syms;
1.542 - val (program_code, deresolve) =
1.543 - produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value]));
1.544 - val value_name = the (deresolve Code_Symbol.value);
1.545 - in ((program_code, value_name), deresolve) end;
1.546 + val (pretty_code, deresolve) =
1.547 + prepared_serializer program (if all_public then [] else [Code_Symbol.value]);
1.548 + val (compilation_code, [SOME value_name]) =
1.549 + produce_result [Code_Symbol.value] width (pretty_code, deresolve);
1.550 + in ((compilation_code, value_name), deresolve) end;
1.551
1.552 fun compilation_text' ctxt target_name some_module_name program syms =
1.553 let
1.554 + val width = default_width ctxt;
1.555 val evaluation_args = the_evaluation_args ctxt target_name;
1.556 - val (mounted_serializer, (_, prepared_program)) =
1.557 - mount_serializer ctxt target_name NONE (the_default generatedN some_module_name) evaluation_args program syms;
1.558 + val (prepared_serializer, (prepared_program, _)) =
1.559 + prepare_serializer ctxt target_name (the_default generatedN some_module_name) evaluation_args program syms;
1.560 in
1.561 Code_Preproc.timed_exec "serializing"
1.562 - (fn () => dynamic_compilation_text mounted_serializer prepared_program syms) ctxt
1.563 + (fn () => dynamic_compilation_text prepared_serializer width prepared_program syms) ctxt
1.564 end;
1.565
1.566 fun compilation_text ctxt target_name program syms =
1.567 fst oo compilation_text' ctxt target_name NONE program syms
1.568 -
1.569 +
1.570 end; (* local *)
1.571
1.572
1.573 (* code generation *)
1.574
1.575 -fun prep_destination (s, pos) =
1.576 - if s = "" then NONE
1.577 +fun prep_destination (location, (s, pos)) =
1.578 + if location = {physical = false}
1.579 + then (location, Path.explode_pos (s, pos))
1.580 else
1.581 let
1.582 + val _ =
1.583 + if s = ""
1.584 + then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument")
1.585 + else ();
1.586 + val _ =
1.587 + legacy_feature
1.588 + (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
1.589 + Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
1.590 val _ = Position.report pos Markup.language_path;
1.591 - val path = Path.explode s;
1.592 + val path = #1 (Path.explode_pos (s, pos));
1.593 val _ = Position.report pos (Markup.path (Path.smart_implode path));
1.594 - in SOME path end;
1.595 + in (location, (path, pos)) end;
1.596
1.597 -fun export_code ctxt all_public cs seris =
1.598 +fun export_code all_public cs seris lthy =
1.599 let
1.600 - val program = Code_Thingol.consts_program ctxt cs;
1.601 - val _ = map (fn (((target_name, module_name), some_path), args) =>
1.602 - export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
1.603 - in () end;
1.604 + val program = Code_Thingol.consts_program lthy cs;
1.605 + in
1.606 + (seris, lthy) |-> fold (fn (((target_name, module_name), some_file), args) =>
1.607 + export_code_for some_file target_name module_name NONE args
1.608 + program all_public (map Constant cs))
1.609 + end;
1.610
1.611 -fun export_code_cmd all_public raw_cs seris ctxt =
1.612 - export_code ctxt all_public
1.613 - (Code_Thingol.read_const_exprs ctxt raw_cs)
1.614 - ((map o apfst o apsnd) prep_destination seris);
1.615 +fun export_code_cmd all_public raw_cs seris lthy =
1.616 + let
1.617 + val cs = Code_Thingol.read_const_exprs lthy raw_cs;
1.618 + in export_code all_public cs ((map o apfst o apsnd o Option.map) prep_destination seris) lthy end;
1.619
1.620 fun produce_code ctxt all_public cs target_name some_width some_module_name args =
1.621 let
1.622 @@ -472,55 +555,16 @@
1.623 val program = Code_Thingol.consts_program ctxt cs;
1.624 in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
1.625
1.626 -fun check_code ctxt all_public cs seris =
1.627 +fun check_code all_public cs seris lthy =
1.628 let
1.629 - val program = Code_Thingol.consts_program ctxt cs;
1.630 - val _ = map (fn ((target_name, strict), args) =>
1.631 - check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris;
1.632 - in () end;
1.633 + val program = Code_Thingol.consts_program lthy cs;
1.634 + in
1.635 + (seris, lthy) |-> fold (fn ((target_name, strict), args) =>
1.636 + check_code_for target_name strict args program all_public (map Constant cs))
1.637 + end;
1.638
1.639 -fun check_code_cmd all_public raw_cs seris ctxt =
1.640 - check_code ctxt all_public
1.641 - (Code_Thingol.read_const_exprs ctxt raw_cs) seris;
1.642 -
1.643 -local
1.644 -
1.645 -val parse_const_terms = Scan.repeat1 Args.term
1.646 - >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts);
1.647 -
1.648 -fun parse_names category parse internalize mark_symbol =
1.649 - Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse
1.650 - >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs);
1.651 -
1.652 -val parse_consts = parse_names "consts" Args.term
1.653 - (Code.check_const o Proof_Context.theory_of) Constant;
1.654 -
1.655 -val parse_types = parse_names "types" (Scan.lift Args.name)
1.656 - (Sign.intern_type o Proof_Context.theory_of) Type_Constructor;
1.657 -
1.658 -val parse_classes = parse_names "classes" (Scan.lift Args.name)
1.659 - (Sign.intern_class o Proof_Context.theory_of) Type_Class;
1.660 -
1.661 -val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
1.662 - (fn ctxt => fn (raw_tyco, raw_class) =>
1.663 - let
1.664 - val thy = Proof_Context.theory_of ctxt;
1.665 - in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance;
1.666 -
1.667 -in
1.668 -
1.669 -val _ = Theory.setup
1.670 - (Thy_Output.antiquotation_raw @{binding code_stmts}
1.671 - (parse_const_terms --
1.672 - Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances)
1.673 - -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
1.674 - (fn ctxt => fn ((mk_cs, mk_stmtss), (target_name, some_width)) =>
1.675 - Latex.string
1.676 - (present_code ctxt (mk_cs ctxt)
1.677 - (maps (fn f => f ctxt) mk_stmtss)
1.678 - target_name some_width "Example" [])));
1.679 -
1.680 -end;
1.681 +fun check_code_cmd all_public raw_cs seris lthy =
1.682 + check_code all_public (Code_Thingol.read_const_exprs lthy raw_cs) seris lthy;
1.683
1.684
1.685 (** serializer configuration **)
1.686 @@ -563,9 +607,9 @@
1.687 (arrange false) (arrange false) (arrange true) x
1.688 end;
1.689
1.690 -fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls;
1.691 +fun cert_name_decls ctxt = cert_syms' ctxt #> arrange_name_decls;
1.692
1.693 -fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls;
1.694 +fun read_name_decls ctxt = read_syms' ctxt #> arrange_name_decls;
1.695
1.696 fun set_identifier (target_name, sym_name) = map_identifiers target_name (Code_Symbol.set_data sym_name);
1.697
1.698 @@ -578,7 +622,7 @@
1.699
1.700 (* custom printings *)
1.701
1.702 -fun arrange_printings prep_const ctxt =
1.703 +fun arrange_printings prep_syms ctxt =
1.704 let
1.705 fun arrange check (sym, target_syns) =
1.706 map (fn (target_name, some_syn) =>
1.707 @@ -587,14 +631,14 @@
1.708 Code_Symbol.maps_attr'
1.709 (arrange check_const_syntax) (arrange check_tyco_syntax)
1.710 (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
1.711 - (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) =>
1.712 + (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) =>
1.713 (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
1.714 - map (prep_const ctxt) raw_cs)))
1.715 + map (prep_syms ctxt) raw_syms)))
1.716 end;
1.717
1.718 -fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt;
1.719 +fun cert_printings ctxt = cert_syms' ctxt #> arrange_printings cert_syms ctxt;
1.720
1.721 -fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt;
1.722 +fun read_printings ctxt = read_syms' ctxt #> arrange_printings read_syms ctxt;
1.723
1.724 fun set_printing (target_name, sym_syn) = map_printings target_name (Code_Symbol.set_data sym_syn);
1.725
1.726 @@ -615,67 +659,125 @@
1.727
1.728 (** Isar setup **)
1.729
1.730 +val (constantK, type_constructorK, type_classK, class_relationK, class_instanceK, code_moduleK) =
1.731 + (\<^keyword>\<open>constant\<close>, \<^keyword>\<open>type_constructor\<close>, \<^keyword>\<open>type_class\<close>,
1.732 + \<^keyword>\<open>class_relation\<close>, \<^keyword>\<open>class_instance\<close>, \<^keyword>\<open>code_module\<close>);
1.733 +
1.734 +local
1.735 +
1.736 +val parse_constants = constantK |-- Scan.repeat1 Parse.term >> map Constant;
1.737 +
1.738 +val parse_type_constructors = type_constructorK |-- Scan.repeat1 Parse.type_const >> map Type_Constructor;
1.739 +
1.740 +val parse_classes = type_classK |-- Scan.repeat1 Parse.class >> map Type_Class;
1.741 +
1.742 +val parse_class_relations = class_relationK |-- Scan.repeat1 parse_classrel_ident >> map Class_Relation;
1.743 +
1.744 +val parse_instances = class_instanceK |-- Scan.repeat1 parse_inst_ident >> map Class_Instance;
1.745 +
1.746 +val parse_simple_symbols = Scan.repeats1 (parse_constants || parse_type_constructors || parse_classes
1.747 + || parse_class_relations || parse_instances);
1.748 +
1.749 fun parse_single_symbol_pragma parse_keyword parse_isa parse_target =
1.750 - parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
1.751 - -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target)));
1.752 + parse_keyword |-- Parse.!!! (parse_isa --| (\<^keyword>\<open>\<rightharpoonup>\<close> || \<^keyword>\<open>=>\<close>)
1.753 + -- Parse.and_list1 (\<^keyword>\<open>(\<close> |-- (Parse.name --| \<^keyword>\<open>)\<close> -- Scan.option parse_target)));
1.754
1.755 fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
1.756 - parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
1.757 + parse_single_symbol_pragma constantK Parse.term parse_const
1.758 >> Constant
1.759 - || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
1.760 + || parse_single_symbol_pragma type_constructorK Parse.type_const parse_tyco
1.761 >> Type_Constructor
1.762 - || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class
1.763 + || parse_single_symbol_pragma type_classK Parse.class parse_class
1.764 >> Type_Class
1.765 - || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel
1.766 + || parse_single_symbol_pragma class_relationK parse_classrel_ident parse_classrel
1.767 >> Class_Relation
1.768 - || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst
1.769 + || parse_single_symbol_pragma class_instanceK parse_inst_ident parse_inst
1.770 >> Class_Instance
1.771 - || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module
1.772 - >> Code_Symbol.Module;
1.773 + || parse_single_symbol_pragma code_moduleK Parse.name parse_module
1.774 + >> Module;
1.775
1.776 fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
1.777 Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma")
1.778 (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module));
1.779
1.780 -val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) [];
1.781 +val code_expr_argsP = Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.args --| \<^keyword>\<open>)\<close>) [];
1.782
1.783 -fun code_expr_inP all_public raw_cs =
1.784 - Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name
1.785 - -- Scan.optional (@{keyword "module_name"} |-- Parse.name) ""
1.786 - -- Scan.optional (@{keyword "file"} |-- Parse.position Parse.path) ("", Position.none)
1.787 +fun code_expr_inP (all_public, raw_cs) =
1.788 + Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
1.789 + -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
1.790 + -- Scan.option
1.791 + ((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true})
1.792 + -- Parse.!!! (Parse.position Parse.path))
1.793 -- code_expr_argsP))
1.794 >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
1.795
1.796 -fun code_expr_checkingP all_public raw_cs =
1.797 - (@{keyword "checking"} |-- Parse.!!!
1.798 - (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true)
1.799 - -- code_expr_argsP)))
1.800 +fun code_expr_checkingP (all_public, raw_cs) =
1.801 + (\<^keyword>\<open>checking\<close> |-- Parse.!!!
1.802 + (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\<open>?\<close> >> K false) true) -- code_expr_argsP)))
1.803 >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
1.804
1.805 -val code_exprP = (Scan.optional (@{keyword "open"} |-- Scan.succeed true) false
1.806 - -- Scan.repeat1 Parse.term)
1.807 - :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
1.808 +in
1.809
1.810 val _ =
1.811 - Outer_Syntax.command @{command_keyword code_reserved}
1.812 + Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
1.813 "declare words as reserved for target language"
1.814 (Parse.name -- Scan.repeat1 Parse.name
1.815 >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
1.816
1.817 val _ =
1.818 - Outer_Syntax.command @{command_keyword code_identifier} "declare mandatory names for code symbols"
1.819 + Outer_Syntax.command \<^command_keyword>\<open>code_identifier\<close> "declare mandatory names for code symbols"
1.820 (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name
1.821 >> (Toplevel.theory o fold set_identifiers_cmd));
1.822
1.823 val _ =
1.824 - Outer_Syntax.command @{command_keyword code_printing} "declare dedicated printing for code symbols"
1.825 + Outer_Syntax.command \<^command_keyword>\<open>code_printing\<close> "declare dedicated printing for code symbols"
1.826 (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
1.827 Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
1.828 - (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [])
1.829 + (Parse.text -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
1.830 >> (Toplevel.theory o fold set_printings_cmd));
1.831
1.832 val _ =
1.833 - Outer_Syntax.command @{command_keyword export_code} "generate executable code for constants"
1.834 - (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of)));
1.835 + Outer_Syntax.local_theory \<^command_keyword>\<open>export_code\<close> "generate executable code for constants"
1.836 + (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term
1.837 + :|-- (fn args => (code_expr_checkingP args || code_expr_inP args)));
1.838 +
1.839 +end;
1.840 +
1.841 +local
1.842 +
1.843 +val parse_const_terms = Args.theory -- Scan.repeat1 Args.term
1.844 + >> uncurry (fn thy => map (Code.check_const thy));
1.845 +
1.846 +fun parse_symbols keyword parse internalize mark_symbol =
1.847 + Scan.lift (keyword --| Args.colon) |-- Args.theory -- Scan.repeat1 parse
1.848 + >> uncurry (fn thy => map (mark_symbol o internalize thy));
1.849 +
1.850 +val parse_consts = parse_symbols constantK Args.term
1.851 + Code.check_const Constant;
1.852 +
1.853 +val parse_types = parse_symbols type_constructorK (Scan.lift Args.name)
1.854 + Sign.intern_type Type_Constructor;
1.855 +
1.856 +val parse_classes = parse_symbols type_classK (Scan.lift Args.name)
1.857 + Sign.intern_class Type_Class;
1.858 +
1.859 +val parse_instances = parse_symbols class_instanceK (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name))
1.860 + (fn thy => fn (raw_tyco, raw_class) =>
1.861 + (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) Class_Instance;
1.862 +
1.863 +in
1.864 +
1.865 +val _ = Theory.setup
1.866 + (Thy_Output.antiquotation_raw \<^binding>\<open>code_stmts\<close>
1.867 + (parse_const_terms --
1.868 + Scan.repeats (parse_consts || parse_types || parse_classes || parse_instances)
1.869 + -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
1.870 + (fn ctxt => fn ((consts, symbols), (target_name, some_width)) =>
1.871 + present_code ctxt consts symbols
1.872 + target_name "Example" some_width []
1.873 + |> trim_line
1.874 + |> Thy_Output.verbatim (Config.put Document_Antiquotation.thy_output_display true ctxt)));
1.875 +
1.876 +end;
1.877
1.878 end; (*struct*)