src/Tools/Code/code_target.ML
changeset 41342 3519e0dd8f75
parent 41307 bb8468ae414e
child 41344 d990badc97a3
equal deleted inserted replaced
41339:481c89fabcbc 41342:3519e0dd8f75
   116     reserved_syms: string list,
   116     reserved_syms: string list,
   117     includes: (string * Pretty.T) list,
   117     includes: (string * Pretty.T) list,
   118     module_alias: string -> string option,
   118     module_alias: string -> string option,
   119     class_syntax: string -> string option,
   119     class_syntax: string -> string option,
   120     tyco_syntax: string -> Code_Printer.tyco_syntax option,
   120     tyco_syntax: string -> Code_Printer.tyco_syntax option,
   121     const_syntax: string -> Code_Printer.activated_const_syntax option,
   121     const_syntax: string -> Code_Printer.activated_const_syntax option }
   122     program: Code_Thingol.program }
   122   -> Code_Thingol.program
   123   -> serialization;
   123   -> serialization;
   124 
   124 
   125 datatype description = Fundamental of { serializer: serializer,
   125 datatype description = Fundamental of { serializer: serializer,
   126       literals: literals,
   126       literals: literals,
   127       check: { env_var: string, make_destination: Path.T -> Path.T,
   127       check: { env_var: string, make_destination: Path.T -> Path.T,
   311     val _ = if null empty_funs then () else error ("No code equations for "
   311     val _ = if null empty_funs then () else error ("No code equations for "
   312       ^ commas (map (Sign.extern_const thy) empty_funs));
   312       ^ commas (map (Sign.extern_const thy) empty_funs));
   313     val program4 = Graph.subgraph (member (op =) names4) program3;
   313     val program4 = Graph.subgraph (member (op =) names4) program3;
   314   in (names4, program4) end;
   314   in (names4, program4) end;
   315 
   315 
   316 fun invoke_serializer thy abortable serializer literals reserved all_includes
   316 fun prepare_serializer thy abortable serializer literals reserved all_includes
   317     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   317     module_alias proto_class_syntax proto_instance_syntax proto_tyco_syntax proto_const_syntax
   318     module_name args naming proto_program names =
   318     module_name args naming proto_program names =
   319   let
   319   let
   320     val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
   320     val (names_hidden, (class_syntax, tyco_syntax, const_syntax)) =
   321       activate_symbol_syntax thy literals naming
   321       activate_symbol_syntax thy literals naming
   326        of SOME name => member (op =) names_all name
   326        of SOME name => member (op =) names_all name
   327         | NONE => false) cs
   327         | NONE => false) cs
   328       then SOME (name, content) else NONE;
   328       then SOME (name, content) else NONE;
   329     val includes = map_filter select_include (Symtab.dest all_includes);
   329     val includes = map_filter select_include (Symtab.dest all_includes);
   330   in
   330   in
   331     serializer args {
   331     (serializer args {
   332       labelled_name = Code_Thingol.labelled_name thy proto_program,
   332       labelled_name = Code_Thingol.labelled_name thy proto_program,
   333       reserved_syms = reserved,
   333       reserved_syms = reserved,
   334       includes = includes,
   334       includes = includes,
   335       module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
   335       module_alias = if module_name = "" then Symtab.lookup module_alias else K (SOME module_name),
   336       class_syntax = Symtab.lookup class_syntax,
   336       class_syntax = Symtab.lookup class_syntax,
   337       tyco_syntax = Symtab.lookup tyco_syntax,
   337       tyco_syntax = Symtab.lookup tyco_syntax,
   338       const_syntax = Symtab.lookup const_syntax,
   338       const_syntax = Symtab.lookup const_syntax },
   339       program = program }
   339       program)
   340   end;
   340   end;
   341 
   341 
   342 fun mount_serializer thy target some_width module_name args =
   342 fun mount_serializer thy target some_width module_name args naming program names =
   343   let
   343   let
   344     val (default_width, abortable, data, modify) = activate_target thy target;
   344     val (default_width, abortable, data, modify) = activate_target thy target;
   345     val serializer = case the_description data
   345     val serializer = case the_description data
   346      of Fundamental seri => #serializer seri;
   346      of Fundamental seri => #serializer seri;
   347     val reserved = the_reserved data;
   347     val reserved = the_reserved data;
   348     val module_alias = the_module_alias data 
   348     val module_alias = the_module_alias data 
   349     val { class, instance, tyco, const } = the_symbol_syntax data;
   349     val { class, instance, tyco, const } = the_symbol_syntax data;
   350     val literals = the_literals thy target;
   350     val literals = the_literals thy target;
       
   351     val (prepared_serializer, prepared_program) = prepare_serializer thy
       
   352       abortable serializer literals reserved (the_includes data) module_alias
       
   353         class instance tyco const module_name args
       
   354           naming (modify naming program) names
   351     val width = the_default default_width some_width;
   355     val width = the_default default_width some_width;
   352   in fn naming => fn program => fn names =>
   356   in prepared_serializer prepared_program width end;
   353     invoke_serializer thy abortable serializer literals reserved
       
   354       (the_includes data) module_alias class instance tyco const module_name args
       
   355         naming (modify naming program) names width
       
   356   end;
       
   357 
   357 
   358 fun assert_module_name "" = error ("Empty module name not allowed.")
   358 fun assert_module_name "" = error ("Empty module name not allowed.")
   359   | assert_module_name module_name = module_name;
   359   | assert_module_name module_name = module_name;
   360 
   360 
   361 in
   361 in