haftmann@37745: (* Title: Tools/Code/code_target.ML haftmann@24219: Author: Florian Haftmann, TU Muenchen haftmann@24219: haftmann@38910: Generic infrastructure for target language data. haftmann@24219: *) haftmann@24219: haftmann@24219: signature CODE_TARGET = haftmann@24219: sig haftmann@36471: val cert_tyco: theory -> string -> string haftmann@36471: val read_tyco: theory -> string -> string haftmann@39057: val read_const_exprs: theory -> string list -> string list haftmann@36471: haftmann@38933: val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list haftmann@55147: -> Code_Thingol.program -> Code_Symbol.symbol list -> unit haftmann@38933: val produce_code_for: theory -> string -> int option -> string -> Token.T list haftmann@55147: -> Code_Thingol.program -> Code_Symbol.symbol list -> (string * string) list * string option list haftmann@38933: val present_code_for: theory -> string -> int option -> string -> Token.T list haftmann@55147: -> Code_Thingol.program -> Code_Symbol.symbol list * Code_Symbol.symbol list -> string haftmann@38918: val check_code_for: theory -> string -> bool -> Token.T list haftmann@55147: -> Code_Thingol.program -> Code_Symbol.symbol list -> unit haftmann@38918: haftmann@38918: val export_code: theory -> string list haftmann@38933: -> (((string * string) * Path.T option) * Token.T list) list -> unit haftmann@38929: val produce_code: theory -> string list haftmann@48568: -> string -> int option -> string -> Token.T list -> (string * string) list * string option list haftmann@55147: val present_code: theory -> string list -> Code_Symbol.symbol list haftmann@38933: -> string -> int option -> string -> Token.T list -> string haftmann@38918: val check_code: theory -> string list haftmann@38918: -> ((string * bool) * Token.T list) list -> unit haftmann@38918: haftmann@48568: val generatedN: string haftmann@55147: val evaluator: theory -> string -> Code_Thingol.program haftmann@55147: -> Code_Symbol.symbol list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm haftmann@48568: -> (string * string) list * string haftmann@41344: haftmann@28054: type serializer haftmann@34152: type literals = Code_Printer.literals haftmann@37822: val add_target: string * { serializer: serializer, literals: literals, wenzelm@41940: check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } wenzelm@41940: -> theory -> theory haftmann@28663: val extend_target: string * haftmann@55147: (string * (Code_Thingol.program -> Code_Thingol.program)) haftmann@28054: -> theory -> theory haftmann@28054: val assert_target: theory -> string -> string haftmann@38918: val the_literals: theory -> string -> literals haftmann@28054: type serialization wenzelm@36959: val parse_args: 'a parser -> Token.T list -> 'a haftmann@38916: val serialization: (int -> Path.T option -> 'a -> unit) haftmann@55147: -> (Code_Symbol.symbol list -> int -> 'a -> (string * string) list * (Code_Symbol.symbol -> string option)) haftmann@38925: -> 'a -> serialization haftmann@38918: val set_default_code_width: int -> theory -> theory haftmann@38917: haftmann@52137: type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl haftmann@52138: type identifier_data haftmann@52138: val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl haftmann@52138: -> theory -> theory haftmann@52137: type const_syntax = Code_Printer.const_syntax haftmann@34152: type tyco_syntax = Code_Printer.tyco_syntax haftmann@52137: val set_printings: (const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl haftmann@52137: -> theory -> theory haftmann@52137: val add_const_syntax: string -> string -> const_syntax option -> theory -> theory haftmann@52137: val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory haftmann@38923: val add_class_syntax: string -> class -> string option -> theory -> theory haftmann@38923: val add_instance_syntax: string -> class * string -> unit option -> theory -> theory haftmann@28054: val add_reserved: string -> string -> theory -> theory haftmann@33969: val add_include: string -> string * (string * string list) option -> theory -> theory haftmann@39646: haftmann@39750: val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit wenzelm@43564: wenzelm@43564: val setup: theory -> theory haftmann@24219: end; haftmann@24219: haftmann@28054: structure Code_Target : CODE_TARGET = haftmann@24219: struct haftmann@24219: haftmann@28054: open Basic_Code_Thingol; haftmann@34152: haftmann@34152: type literals = Code_Printer.literals; haftmann@52137: type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl = haftmann@52137: (string * (string * 'a option) list, string * (string * 'b option) list, haftmann@52137: class * (string * 'c option) list, (class * class) * (string * 'd option) list, haftmann@52137: (class * string) * (string * 'e option) list, haftmann@52137: string * (string * 'f option) list) Code_Symbol.attr; haftmann@52138: type identifier_data = (string, string, string, string, string, string) Code_Symbol.data; haftmann@52137: haftmann@34152: type tyco_syntax = Code_Printer.tyco_syntax; haftmann@37876: type const_syntax = Code_Printer.const_syntax; haftmann@34152: haftmann@24219: haftmann@52377: (** checking and parsing of symbols **) haftmann@52377: haftmann@52377: fun cert_const thy const = haftmann@52377: let haftmann@52377: val _ = if Sign.declared_const thy const then () haftmann@52377: else error ("No such constant: " ^ quote const); haftmann@52377: in const end; haftmann@52377: haftmann@52377: fun cert_tyco thy tyco = haftmann@52377: let haftmann@52377: val _ = if Sign.declared_tyname thy tyco then () haftmann@52377: else error ("No such type constructor: " ^ quote tyco); haftmann@52377: in tyco end; haftmann@52377: haftmann@52377: fun read_tyco thy = #1 o dest_Type haftmann@52377: o Proof_Context.read_type_name_proper (Proof_Context.init_global thy) true; haftmann@52377: haftmann@52377: fun cert_class thy class = haftmann@52377: let haftmann@52377: val _ = Axclass.get_info thy class; haftmann@52377: in class end; haftmann@52377: haftmann@52377: fun read_class thy = Proof_Context.read_class (Proof_Context.init_global thy); haftmann@52377: haftmann@52377: val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class; haftmann@52377: haftmann@52377: fun cert_inst thy (class, tyco) = haftmann@52377: (cert_class thy class, cert_tyco thy tyco); haftmann@52377: haftmann@52377: fun read_inst thy (raw_tyco, raw_class) = haftmann@55147: (read_tyco thy raw_tyco, read_class thy raw_class); haftmann@52377: haftmann@52377: val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class; haftmann@52377: haftmann@52377: fun cert_syms thy = haftmann@52377: Code_Symbol.map_attr (apfst (cert_const thy)) (apfst (cert_tyco thy)) haftmann@52377: (apfst (cert_class thy)) ((apfst o pairself) (cert_class thy)) (apfst (cert_inst thy)) I; haftmann@52377: haftmann@52377: fun read_syms thy = haftmann@52377: Code_Symbol.map_attr (apfst (Code.read_const thy)) (apfst (read_tyco thy)) haftmann@52377: (apfst (read_class thy)) ((apfst o pairself) (read_class thy)) (apfst (read_inst thy)) I; haftmann@52377: haftmann@52377: fun check_name is_module s = haftmann@52377: let haftmann@52377: val _ = if s = "" then error "Bad empty code name" else (); haftmann@52377: val xs = Long_Name.explode s; haftmann@52377: val xs' = if is_module haftmann@52377: then map (Name.desymbolize true) xs haftmann@52377: else if length xs < 2 haftmann@52377: then error ("Bad code name without module component: " ^ quote s) haftmann@52377: else haftmann@52377: let haftmann@52377: val (ys, y) = split_last xs; haftmann@52377: val ys' = map (Name.desymbolize true) ys; haftmann@52377: val y' = Name.desymbolize false y; haftmann@52377: in ys' @ [y'] end; haftmann@52377: in if xs' = xs haftmann@52377: then s haftmann@52377: else error ("Invalid code name: " ^ quote s ^ "\n" haftmann@52377: ^ "better try " ^ quote (Long_Name.implode xs')) haftmann@52377: end; haftmann@52377: haftmann@52377: haftmann@52137: (** serializations and serializer **) haftmann@52137: haftmann@52137: (* serialization: abstract nonsense to cover different destinies for generated code *) haftmann@24219: haftmann@55147: datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.symbol list; haftmann@55147: type serialization = int -> destination -> ((string * string) list * (Code_Symbol.symbol -> string option)) option; haftmann@27014: haftmann@39659: fun serialization output _ content width (Export some_path) = haftmann@39661: (output width some_path content; NONE) haftmann@39661: | serialization _ string content width Produce = haftmann@39661: string [] width content |> SOME haftmann@55147: | serialization _ string content width (Present syms) = haftmann@55147: string syms width content haftmann@48568: |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str) haftmann@39661: |> SOME; haftmann@39659: haftmann@39661: fun export some_path f = (f (Export some_path); ()); haftmann@39661: fun produce f = the (f Produce); haftmann@55147: fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms))))); haftmann@38917: haftmann@24219: haftmann@52137: (* serializers: functions producing serializations *) haftmann@28054: haftmann@39142: type serializer = Token.T list haftmann@52138: -> Proof.context haftmann@39142: -> { haftmann@52138: module_name: string, haftmann@38926: reserved_syms: string list, haftmann@52138: identifiers: identifier_data, haftmann@38926: includes: (string * Pretty.T) list, haftmann@38926: class_syntax: string -> string option, haftmann@38926: tyco_syntax: string -> Code_Printer.tyco_syntax option, haftmann@41342: const_syntax: string -> Code_Printer.activated_const_syntax option } haftmann@41342: -> Code_Thingol.program haftmann@28054: -> serialization; haftmann@27000: haftmann@52137: datatype description = haftmann@52137: Fundamental of { serializer: serializer, haftmann@38910: literals: literals, haftmann@37822: check: { env_var: string, make_destination: Path.T -> Path.T, wenzelm@41940: make_command: string -> string } } haftmann@38909: | Extension of string * haftmann@55147: (Code_Thingol.program -> Code_Thingol.program); haftmann@28054: haftmann@52137: haftmann@52137: (** theory data **) haftmann@52137: haftmann@28054: datatype target = Target of { haftmann@28054: serial: serial, haftmann@37821: description: description, haftmann@28054: reserved: string list, haftmann@52138: identifiers: identifier_data, haftmann@55149: printings: (Code_Printer.activated_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, haftmann@52137: (Pretty.T * string list)) Code_Symbol.data haftmann@28054: }; haftmann@27103: haftmann@52138: fun make_target ((serial, description), (reserved, (identifiers, printings))) = wenzelm@43564: Target { serial = serial, description = description, reserved = reserved, haftmann@52138: identifiers = identifiers, printings = printings }; haftmann@52138: fun map_target f (Target { serial, description, reserved, identifiers, printings }) = haftmann@52138: make_target (f ((serial, description), (reserved, (identifiers, printings)))); haftmann@37821: fun merge_target strict target (Target { serial = serial1, description = description, haftmann@52138: reserved = reserved1, identifiers = identifiers1, printings = printings1 }, haftmann@37821: Target { serial = serial2, description = _, haftmann@52138: reserved = reserved2, identifiers = identifiers2, printings = printings2 }) = haftmann@28054: if serial1 = serial2 orelse not strict then haftmann@52138: make_target ((serial1, description), (merge (op =) (reserved1, reserved2), haftmann@52138: (Code_Symbol.merge_data (identifiers1, identifiers2), haftmann@52138: Code_Symbol.merge_data (printings1, printings2)))) haftmann@28054: else haftmann@37821: error ("Incompatible targets: " ^ quote target); haftmann@27103: haftmann@37821: fun the_description (Target { description, ... }) = description; haftmann@28054: fun the_reserved (Target { reserved, ... }) = reserved; haftmann@52138: fun the_identifiers (Target { identifiers , ... }) = identifiers; haftmann@52137: fun the_printings (Target { printings, ... }) = printings; haftmann@27437: haftmann@34248: structure Targets = Theory_Data haftmann@34071: ( haftmann@54890: type T = target Symtab.table * int; haftmann@54890: val empty = (Symtab.empty, 80); haftmann@34071: val extend = I; haftmann@54890: fun merge ((target1, width1), (target2, width2)) : T = haftmann@54890: (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2)); haftmann@34071: ); haftmann@27436: haftmann@54890: fun assert_target thy target = if Symtab.defined (fst (Targets.get thy)) target haftmann@33969: then target haftmann@33969: else error ("Unknown code target language: " ^ quote target); haftmann@28054: haftmann@28054: fun put_target (target, seri) thy = haftmann@27304: let haftmann@54890: val lookup_target = Symtab.lookup (fst (Targets.get thy)); haftmann@28054: val _ = case seri haftmann@37821: of Extension (super, _) => if is_some (lookup_target super) then () haftmann@28054: else error ("Unknown code target language: " ^ quote super) haftmann@28054: | _ => (); haftmann@37821: val overwriting = case (Option.map the_description o lookup_target) target haftmann@28663: of NONE => false haftmann@37821: | SOME (Extension _) => true haftmann@37821: | SOME (Fundamental _) => (case seri haftmann@37821: of Extension _ => error ("Will not overwrite existing target " ^ quote target) haftmann@28663: | _ => true); haftmann@28663: val _ = if overwriting haftmann@28054: then warning ("Overwriting existing target " ^ quote target) wenzelm@43564: else (); haftmann@28054: in haftmann@28054: thy haftmann@54890: |> (Targets.map o apfst o Symtab.update) haftmann@52138: (target, make_target ((serial (), seri), haftmann@52138: ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) haftmann@28054: end; haftmann@27436: haftmann@37821: fun add_target (target, seri) = put_target (target, Fundamental seri); haftmann@28054: fun extend_target (target, (super, modify)) = haftmann@37821: put_target (target, Extension (super, modify)); haftmann@27436: haftmann@28054: fun map_target_data target f thy = haftmann@27436: let haftmann@28054: val _ = assert_target thy target; haftmann@28054: in haftmann@28054: thy haftmann@54890: |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f haftmann@28054: end; haftmann@27304: haftmann@28054: fun map_reserved target = haftmann@52138: map_target_data target o apfst; haftmann@52138: fun map_identifiers target = haftmann@52138: map_target_data target o apsnd o apfst; haftmann@52137: fun map_printings target = haftmann@52137: map_target_data target o apsnd o apsnd; haftmann@27000: haftmann@34248: fun set_default_code_width k = (Targets.map o apsnd) (K k); haftmann@34071: haftmann@27000: haftmann@34021: (** serializer usage **) haftmann@34021: haftmann@34021: (* montage *) haftmann@34021: haftmann@37822: fun the_fundamental thy = haftmann@34021: let haftmann@54890: val (targets, _) = Targets.get thy; haftmann@37822: fun fundamental target = case Symtab.lookup targets target haftmann@37821: of SOME data => (case the_description data haftmann@37822: of Fundamental data => data haftmann@37822: | Extension (super, _) => fundamental super) haftmann@34021: | NONE => error ("Unknown code target language: " ^ quote target); haftmann@37822: in fundamental end; haftmann@37822: haftmann@37822: fun the_literals thy = #literals o the_fundamental thy; haftmann@34021: haftmann@39817: fun collapse_hierarchy thy = haftmann@38927: let haftmann@54890: val (targets, _) = Targets.get thy; wenzelm@43564: fun collapse target = haftmann@38927: let haftmann@38927: val data = case Symtab.lookup targets target haftmann@38927: of SOME data => data haftmann@38927: | NONE => error ("Unknown code target language: " ^ quote target); haftmann@38927: in case the_description data haftmann@55147: of Fundamental _ => (I, data) haftmann@38927: | Extension (super, modify) => let haftmann@39817: val (modify', data') = collapse super haftmann@55147: in (modify' #> modify, merge_target false target (data', data)) end haftmann@38927: end; haftmann@39817: in collapse end; haftmann@39817: haftmann@39817: local haftmann@39817: haftmann@39817: fun activate_target thy target = haftmann@39817: let haftmann@54890: val (_, default_width) = Targets.get thy; haftmann@39817: val (modify, data) = collapse_hierarchy thy target; haftmann@54890: in (default_width, data, modify) end; haftmann@38927: haftmann@55147: fun project_program thy syms_hidden syms1 program2 = haftmann@38927: let wenzelm@42361: val ctxt = Proof_Context.init_global thy; haftmann@55147: val syms2 = subtract (op =) syms_hidden syms1; haftmann@55147: val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2; haftmann@55147: val syms4 = Code_Symbol.Graph.all_succs program3 syms2; haftmann@54890: val unimplemented = Code_Thingol.unimplemented program3; wenzelm@42359: val _ = haftmann@54889: if null unimplemented then () wenzelm@42359: else error ("No code equations for " ^ haftmann@54889: commas (map (Proof_Context.extern_const ctxt) unimplemented)); haftmann@55147: val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3; haftmann@55147: in (syms4, program4) end; haftmann@38927: haftmann@55149: fun prepare_serializer thy (serializer : serializer) reserved identifiers haftmann@55147: printings module_name args proto_program syms = haftmann@38927: let haftmann@55149: val syms_hidden = Code_Symbol.symbols_of printings; haftmann@55147: val (syms_all, program) = project_program thy syms_hidden syms proto_program; haftmann@39484: fun select_include (name, (content, cs)) = haftmann@55147: if null cs orelse exists (fn c => member (op =) syms_all (Code_Symbol.Constant c)) cs haftmann@39484: then SOME (name, content) else NONE; haftmann@52137: val includes = map_filter select_include (Code_Symbol.dest_module_data printings); haftmann@34021: in haftmann@52138: (serializer args (Proof_Context.init_global thy) { haftmann@52138: module_name = module_name, haftmann@38926: reserved_syms = reserved, haftmann@52138: identifiers = identifiers, haftmann@38926: includes = includes, haftmann@55149: const_syntax = Code_Symbol.lookup_constant_data printings, haftmann@55149: tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, haftmann@55149: class_syntax = Code_Symbol.lookup_type_class_data printings }, haftmann@41342: program) haftmann@34021: end; haftmann@34021: haftmann@55147: fun mount_serializer thy target some_width module_name args program syms = haftmann@34021: let haftmann@54890: val (default_width, data, modify) = activate_target thy target; haftmann@38921: val serializer = case the_description data haftmann@38927: of Fundamental seri => #serializer seri; haftmann@52138: val (prepared_serializer, prepared_program) = haftmann@55149: prepare_serializer thy serializer haftmann@52138: (the_reserved data) (the_identifiers data) (the_printings data) haftmann@55147: module_name args (modify program) syms haftmann@34071: val width = the_default default_width some_width; haftmann@41344: in (fn program => prepared_serializer program width, prepared_program) end; haftmann@41344: haftmann@55147: fun invoke_serializer thy target some_width module_name args program syms = haftmann@41344: let haftmann@53413: val check = if module_name = "" then I else check_name true; haftmann@41344: val (mounted_serializer, prepared_program) = mount_serializer thy haftmann@55147: target some_width (check module_name) args program syms; haftmann@41344: in mounted_serializer prepared_program end; haftmann@34021: haftmann@52138: fun assert_module_name "" = error "Empty module name not allowed here" haftmann@38933: | assert_module_name module_name = module_name; haftmann@38933: haftmann@48426: fun using_master_directory thy = haftmann@48426: Option.map (Path.append (File.pwd ()) o Path.append (Thy_Load.master_directory thy)); haftmann@48371: haftmann@34021: in haftmann@34021: haftmann@48568: val generatedN = "Generated_Code"; haftmann@48568: haftmann@39484: fun export_code_for thy some_path target some_width module_name args = haftmann@48371: export (using_master_directory thy some_path) haftmann@55147: oo invoke_serializer thy target some_width module_name args; haftmann@38918: haftmann@39484: fun produce_code_for thy target some_width module_name args = haftmann@39102: let haftmann@41344: val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; haftmann@55147: in fn program => fn syms => haftmann@55147: produce (serializer program syms) |> apsnd (fn deresolve => map deresolve syms) haftmann@39484: end; haftmann@38929: haftmann@39484: fun present_code_for thy target some_width module_name args = haftmann@39484: let haftmann@41344: val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args; haftmann@55147: in fn program => fn (syms, selects) => haftmann@55147: present selects (serializer program syms) haftmann@39484: end; haftmann@38918: haftmann@55147: fun check_code_for thy target strict args program syms = haftmann@37824: let haftmann@37824: val { env_var, make_destination, make_command } = haftmann@37824: (#check o the_fundamental thy) target; wenzelm@41939: fun ext_check p = wenzelm@43564: let haftmann@37824: val destination = make_destination p; haftmann@41344: val _ = export (SOME destination) (invoke_serializer thy target (SOME 80) haftmann@55147: generatedN args program syms); haftmann@48568: val cmd = make_command generatedN; wenzelm@43850: in wenzelm@43850: if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 haftmann@37824: then error ("Code check failed for " ^ target ^ ": " ^ cmd) haftmann@37824: else () haftmann@37824: end; wenzelm@43850: in wenzelm@43850: if getenv env_var = "" haftmann@37825: then if strict haftmann@37825: then error (env_var ^ " not set; cannot check code for " ^ target) haftmann@37825: else warning (env_var ^ " not set; skipped checking code for " ^ target) wenzelm@41939: else Isabelle_System.with_tmp_dir "Code_Test" ext_check haftmann@37824: end; haftmann@37824: haftmann@55147: fun evaluation mounted_serializer prepared_program syms ((vs, ty), t) = haftmann@41344: let haftmann@41344: val _ = if Code_Thingol.contains_dict_var t then haftmann@41344: error "Term to be evaluated contains free dictionaries" else (); wenzelm@43324: val v' = singleton (Name.variant_list (map fst vs)) "a"; haftmann@41344: val vs' = (v', []) :: vs; haftmann@55147: val ty' = ITyVar v' `-> ty; haftmann@41344: val program = prepared_program haftmann@55147: |> Code_Symbol.Graph.new_node (Code_Symbol.value, haftmann@55147: Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)) haftmann@55147: |> fold (curry (perhaps o try o haftmann@55147: Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; haftmann@41344: val (program_code, deresolve) = produce (mounted_serializer program); haftmann@55147: val value_name = the (deresolve Code_Symbol.value); haftmann@55147: in (program_code, value_name) end; haftmann@41344: haftmann@55147: fun evaluator thy target program syms = haftmann@41344: let haftmann@55147: val (mounted_serializer, prepared_program) = haftmann@55147: mount_serializer thy target NONE generatedN [] program syms; haftmann@55147: in evaluation mounted_serializer prepared_program syms end; haftmann@41344: haftmann@34021: end; (* local *) haftmann@34021: haftmann@34021: haftmann@34021: (* code generation *) haftmann@34021: haftmann@55147: fun read_const_exprs thy const_exprs = haftmann@34021: let haftmann@55147: val (cs1, cs2) = Code_Thingol.read_const_exprs thy const_exprs; haftmann@55147: val program = Code_Thingol.consts_program thy true cs2; haftmann@55147: val cs3 = Code_Thingol.implemented_deps program; haftmann@36271: in union (op =) cs3 cs1 end; haftmann@34021: haftmann@38918: fun prep_destination "" = NONE haftmann@38918: | prep_destination s = SOME (Path.explode s); haftmann@38918: haftmann@34021: fun export_code thy cs seris = haftmann@34021: let haftmann@55147: val program = Code_Thingol.consts_program thy false cs; haftmann@38918: val _ = map (fn (((target, module_name), some_path), args) => haftmann@55147: export_code_for thy some_path target NONE module_name args program (map Code_Symbol.Constant cs)) seris; haftmann@34021: in () end; haftmann@34021: haftmann@38918: fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) haftmann@38918: ((map o apfst o apsnd) prep_destination seris); haftmann@38918: haftmann@38929: fun produce_code thy cs target some_width some_module_name args = haftmann@38918: let haftmann@55147: val program = Code_Thingol.consts_program thy false cs; haftmann@55147: in produce_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs) end; haftmann@38929: haftmann@55147: fun present_code thy cs syms target some_width some_module_name args = haftmann@38929: let haftmann@55147: val program = Code_Thingol.consts_program thy false cs; haftmann@55147: in present_code_for thy target some_width some_module_name args program (map Code_Symbol.Constant cs, syms) end; haftmann@34021: haftmann@37824: fun check_code thy cs seris = haftmann@37824: let haftmann@55147: val program = Code_Thingol.consts_program thy false cs; haftmann@38918: val _ = map (fn ((target, strict), args) => haftmann@55147: check_code_for thy target strict args program (map Code_Symbol.Constant cs)) seris; haftmann@37824: in () end; haftmann@37824: haftmann@37824: fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris; haftmann@37824: haftmann@39480: local haftmann@39480: haftmann@39480: val parse_const_terms = Scan.repeat1 Args.term haftmann@39480: >> (fn ts => fn thy => map (Code.check_const thy) ts); haftmann@39480: haftmann@55147: fun parse_names category parse internalize mark_symbol = haftmann@39480: Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse haftmann@55147: >> (fn xs => fn thy => map (mark_symbol o internalize thy) xs); wenzelm@43564: haftmann@39480: val parse_consts = parse_names "consts" Args.term haftmann@55147: Code.check_const Code_Symbol.Constant; haftmann@39480: haftmann@39480: val parse_types = parse_names "types" (Scan.lift Args.name) haftmann@55147: Sign.intern_type Code_Symbol.Type_Constructor; haftmann@39480: haftmann@39480: val parse_classes = parse_names "classes" (Scan.lift Args.name) haftmann@55147: Sign.intern_class Code_Symbol.Type_Class; haftmann@39480: haftmann@39480: val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) haftmann@55147: (fn thy => fn (raw_tyco, raw_class) => (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class)) haftmann@55147: Code_Symbol.Class_Instance; haftmann@39480: haftmann@39480: in haftmann@39480: wenzelm@43564: val antiq_setup = wenzelm@43564: Thy_Output.antiquotation @{binding code_stmts} wenzelm@43564: (parse_const_terms -- wenzelm@43564: Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) wenzelm@43564: -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) wenzelm@43564: (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => wenzelm@43564: let val thy = Proof_Context.theory_of ctxt in wenzelm@43564: present_code thy (mk_cs thy) haftmann@55147: (maps (fn f => f thy) mk_stmtss) wenzelm@43564: target some_width "Example" [] wenzelm@43564: end); haftmann@39480: haftmann@39480: end; haftmann@39480: haftmann@34021: haftmann@28054: (** serializer configuration **) haftmann@27000: haftmann@52138: (* reserved symbol names *) haftmann@52138: haftmann@52138: fun add_reserved target sym thy = haftmann@52138: let haftmann@52138: val (_, data) = collapse_hierarchy thy target; haftmann@52138: val _ = if member (op =) (the_reserved data) sym haftmann@52138: then error ("Reserved symbol " ^ quote sym ^ " already declared") haftmann@52138: else (); haftmann@52138: in haftmann@52138: thy haftmann@52138: |> map_reserved target (insert (op =) sym) haftmann@52138: end; haftmann@52138: haftmann@52138: haftmann@52377: (* checking of syntax *) haftmann@52138: haftmann@55149: fun check_const_syntax thy target c syn = haftmann@52137: if Code_Printer.requires_args syn > Code.args_number thy c haftmann@52137: then error ("Too many arguments in syntax for constant " ^ quote c) haftmann@55149: else Code_Printer.activate_const_syntax thy (the_literals thy target) c syn; haftmann@52137: haftmann@55149: fun check_tyco_syntax thy target tyco syn = haftmann@52137: if fst syn <> Sign.arity_number thy tyco haftmann@52137: then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) haftmann@52137: else syn; haftmann@34071: haftmann@52138: haftmann@52138: (* custom symbol names *) haftmann@52138: wenzelm@52218: fun arrange_name_decls x = haftmann@52138: let haftmann@52138: fun arrange is_module (sym, target_names) = map (fn (target, some_name) => haftmann@52138: (target, (sym, Option.map (check_name is_module) some_name))) target_names; haftmann@52138: in haftmann@52138: Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false) wenzelm@52218: (arrange false) (arrange false) (arrange true) x haftmann@52138: end; haftmann@52138: haftmann@52138: fun cert_name_decls thy = cert_syms thy #> arrange_name_decls; haftmann@52138: haftmann@52138: fun read_name_decls thy = read_syms thy #> arrange_name_decls; haftmann@52138: haftmann@52138: fun set_identifier (target, sym_name) = map_identifiers target (Code_Symbol.set_data sym_name); haftmann@52138: haftmann@52138: fun gen_set_identifiers prep_name_decl raw_name_decls thy = haftmann@52138: fold set_identifier (prep_name_decl thy raw_name_decls) thy; haftmann@52138: haftmann@52138: val set_identifiers = gen_set_identifiers cert_name_decls; haftmann@52138: val set_identifiers_cmd = gen_set_identifiers read_name_decls; haftmann@52138: wenzelm@54312: fun add_module_alias_cmd target aliasses thy = haftmann@52435: let haftmann@52435: val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\""; haftmann@52435: in haftmann@52435: fold (fn (sym, name) => set_identifier wenzelm@54312: (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name)))) wenzelm@54312: aliasses thy haftmann@52435: end; haftmann@52138: haftmann@52138: haftmann@52138: (* custom printings *) haftmann@52138: haftmann@52137: fun arrange_printings prep_const thy = haftmann@52137: let haftmann@52137: fun arrange check (sym, target_syns) = haftmann@55149: map (fn (target, some_syn) => (target, (sym, Option.map (check thy target sym) some_syn))) target_syns; haftmann@52137: in haftmann@52137: Code_Symbol.maps_attr' haftmann@52137: (arrange check_const_syntax) (arrange check_tyco_syntax) haftmann@55149: (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) haftmann@55149: (arrange (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => haftmann@52137: (Code_Printer.str raw_content, map (prep_const thy) raw_cs))) haftmann@52137: end; haftmann@52137: haftmann@52137: fun cert_printings thy = cert_syms thy #> arrange_printings cert_const thy; haftmann@24219: haftmann@52137: fun read_printings thy = read_syms thy #> arrange_printings Code.read_const thy; haftmann@52137: haftmann@52137: fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn); haftmann@52137: haftmann@52137: fun gen_set_printings prep_print_decl raw_print_decls thy = haftmann@52137: fold set_printing (prep_print_decl thy raw_print_decls) thy; haftmann@52137: haftmann@52137: val set_printings = gen_set_printings cert_printings; haftmann@52137: val set_printings_cmd = gen_set_printings read_printings; haftmann@52137: haftmann@52137: fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy = haftmann@24992: let haftmann@52435: val _ = legacy_feature "prefer \"code_printing\" for custom serialisations" haftmann@52137: val x = prep_x thy raw_x; haftmann@55149: in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end; haftmann@28926: haftmann@52137: fun gen_add_const_syntax prep_const = haftmann@52137: gen_add_syntax Code_Symbol.Constant prep_const check_const_syntax; haftmann@52137: haftmann@52137: fun gen_add_tyco_syntax prep_tyco = haftmann@52137: gen_add_syntax Code_Symbol.Type_Constructor prep_tyco check_tyco_syntax; haftmann@52137: haftmann@52137: fun gen_add_class_syntax prep_class = haftmann@55149: gen_add_syntax Code_Symbol.Type_Class prep_class ((K o K o K) I); haftmann@24219: haftmann@52137: fun gen_add_instance_syntax prep_inst = haftmann@55149: gen_add_syntax Code_Symbol.Class_Instance prep_inst ((K o K o K) I); haftmann@52137: haftmann@52137: fun gen_add_include prep_const target (name, some_content) thy = haftmann@52137: gen_add_syntax Code_Symbol.Module (K I) haftmann@55149: (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs)) haftmann@52137: target name some_content thy; haftmann@52137: haftmann@52137: haftmann@27103: (* concrete syntax *) haftmann@27000: haftmann@34021: local haftmann@34021: haftmann@47576: fun zip_list (x :: xs) f g = haftmann@34152: f haftmann@37881: :|-- (fn y => haftmann@34152: fold_map (fn x => g |-- f >> pair x) xs haftmann@37881: :|-- (fn xys => pair ((x, y) :: xys))); haftmann@34152: haftmann@37881: fun process_multi_syntax parse_thing parse_syntax change = haftmann@37881: (Parse.and_list1 parse_thing wenzelm@46949: :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name -- haftmann@52068: (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"}))) haftmann@37881: >> (Toplevel.theory oo fold) haftmann@37881: (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns); haftmann@24219: haftmann@24219: in haftmann@24219: haftmann@52137: val add_reserved = add_reserved; haftmann@52137: val add_const_syntax = gen_add_const_syntax (K I); haftmann@52137: val add_tyco_syntax = gen_add_tyco_syntax cert_tyco; haftmann@38923: val add_class_syntax = gen_add_class_syntax cert_class; haftmann@38923: val add_instance_syntax = gen_add_instance_syntax cert_inst; haftmann@52137: val add_include = gen_add_include (K I); haftmann@24219: haftmann@52137: val add_const_syntax_cmd = gen_add_const_syntax Code.read_const; haftmann@52137: val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco; haftmann@38923: val add_class_syntax_cmd = gen_add_class_syntax read_class; haftmann@38923: val add_instance_syntax_cmd = gen_add_instance_syntax read_inst; haftmann@52137: val add_include_cmd = gen_add_include Code.read_const; haftmann@24219: haftmann@28054: fun parse_args f args = wenzelm@36959: case Scan.read Token.stopper f args haftmann@28054: of SOME x => x haftmann@28054: | NONE => error "Bad serializer arguments"; haftmann@28054: haftmann@28054: haftmann@27304: (** Isar setup **) haftmann@27103: haftmann@52137: fun parse_single_symbol_pragma parse_keyword parse_isa parse_target = haftmann@52434: parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\"} || @{keyword "=>"}) haftmann@52434: -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target))); haftmann@52137: haftmann@52137: fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = wenzelm@52801: parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const haftmann@52137: >> Code_Symbol.Constant haftmann@52377: || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco haftmann@52137: >> Code_Symbol.Type_Constructor haftmann@52377: || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class haftmann@52137: >> Code_Symbol.Type_Class haftmann@52137: || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel haftmann@52137: >> Code_Symbol.Class_Relation haftmann@52137: || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst haftmann@52137: >> Code_Symbol.Class_Instance haftmann@52137: || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module haftmann@52137: >> Code_Symbol.Module; haftmann@52137: haftmann@52137: fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = haftmann@52137: Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") haftmann@52137: (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); haftmann@52137: haftmann@52138: val code_expr_argsP = Scan.optional (@{keyword "("} |-- Args.parse --| @{keyword ")"}) []; haftmann@52138: haftmann@52434: fun code_expr_inP raw_cs = haftmann@52434: Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name haftmann@52434: -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" haftmann@52434: -- Scan.optional (@{keyword "file"} |-- Parse.name) "" haftmann@52434: -- code_expr_argsP)) haftmann@52434: >> (fn seri_args => export_code_cmd raw_cs seri_args); haftmann@52434: haftmann@52434: fun code_expr_checkingP raw_cs = haftmann@52434: (@{keyword "checking"} |-- Parse.!!! haftmann@52434: (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) haftmann@52434: -- code_expr_argsP))) haftmann@52434: >> (fn seri_args => check_code_cmd raw_cs seri_args); haftmann@52434: wenzelm@52801: val code_exprP = Scan.repeat1 Parse.term haftmann@52434: :|-- (fn raw_cs => (code_expr_checkingP raw_cs || code_expr_inP raw_cs)); haftmann@52138: haftmann@52138: val _ = haftmann@52138: Outer_Syntax.command @{command_spec "code_reserved"} haftmann@52138: "declare words as reserved for target language" haftmann@52138: (Parse.name -- Scan.repeat1 Parse.name haftmann@52138: >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)); haftmann@52138: haftmann@52138: val _ = haftmann@52138: Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols" haftmann@52138: (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name haftmann@52138: >> (Toplevel.theory o fold set_identifiers_cmd)); haftmann@52138: haftmann@52138: val _ = haftmann@52138: Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name" haftmann@52138: (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name) haftmann@52138: >> (fn (target, modlnames) => (Toplevel.theory o add_module_alias_cmd target) modlnames)); haftmann@52138: haftmann@52137: val _ = haftmann@52137: Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols" haftmann@52137: (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) haftmann@52137: Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) haftmann@52137: (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) []) haftmann@52137: >> (Toplevel.theory o fold set_printings_cmd)); haftmann@52137: haftmann@52137: val _ = haftmann@52137: Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant" wenzelm@52801: (process_multi_syntax Parse.term Code_Printer.parse_const_syntax haftmann@52137: add_const_syntax_cmd); haftmann@52137: haftmann@52137: val _ = haftmann@52137: Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor" haftmann@52377: (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax haftmann@52137: add_tyco_syntax_cmd); haftmann@52137: wenzelm@24867: val _ = wenzelm@46961: Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class" haftmann@52377: (process_multi_syntax Parse.class Parse.string wenzelm@46961: add_class_syntax_cmd); haftmann@24219: wenzelm@24867: val _ = wenzelm@46961: Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance" haftmann@52377: (process_multi_syntax parse_inst_ident (Parse.minus >> K ()) wenzelm@46961: add_instance_syntax_cmd); haftmann@24219: wenzelm@24867: val _ = wenzelm@46961: Outer_Syntax.command @{command_spec "code_include"} wenzelm@46961: "declare piece of code to be included in generated code" wenzelm@46961: (Parse.name -- Parse.name -- (Parse.text :|-- wenzelm@46961: (fn "-" => Scan.succeed NONE wenzelm@46961: | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME)) wenzelm@46961: >> (fn ((target, name), content_consts) => wenzelm@46961: (Toplevel.theory o add_include_cmd target) (name, content_consts))); haftmann@24992: haftmann@24992: val _ = wenzelm@46961: Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants" wenzelm@46961: (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); haftmann@30494: haftmann@24219: end; (*local*) haftmann@24219: haftmann@39646: haftmann@39646: (** external entrance point -- for codegen tool **) haftmann@39646: haftmann@39750: fun codegen_tool thyname cmd_expr = haftmann@39646: let haftmann@39646: val thy = Thy_Info.get_theory thyname; haftmann@39646: val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o haftmann@39646: (filter Token.is_proper o Outer_Syntax.scan Position.none); haftmann@39646: in case parse cmd_expr haftmann@39646: of SOME f => (writeln "Now generating code..."; f thy) haftmann@39646: | NONE => error ("Bad directive " ^ quote cmd_expr) haftmann@39646: end; haftmann@39646: wenzelm@43564: wenzelm@43564: (** theory setup **) wenzelm@43564: wenzelm@43564: val setup = antiq_setup; wenzelm@43564: haftmann@24219: end; (*struct*)